diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 6ebc2720d..bab63d798 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -22,6 +22,7 @@ if os.name == 'nt':
IS_WINDOW=True
CXX='cl'
MAKE='nmake'
+SHOW_CPPS = True
LIB_KIND = 0
EXE_KIND = 1
@@ -133,17 +134,18 @@ class Component:
out.write('%s: ' % include_node)
self.add_cpp_h_deps(out, include)
out.write('\n')
- out.write(' @echo done > %s\n' % include_node)
+ out.write('\t@echo done > %s\n' % include_node)
def add_cpp_rules(self, out, include_defs, cppfile):
self.add_rule_for_each_include(out, cppfile)
- objfile = '%s/%s.$(OBJ)' % (self.build_dir, os.path.splitext(cppfile)[0])
+ objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
srcfile = '%s/%s' % (self.to_src_dir, cppfile)
out.write('%s: ' % objfile)
self.add_cpp_h_deps(out, cppfile)
out.write('\n')
- flags = 'CXXFLAGS_OPT'
- out.write(' @$(CXX) $(%s) $(%s) $(CXXOUTFLAG)%s %s\n' % (include_defs, flags, objfile, srcfile))
+ if SHOW_CPPS:
+ out.write('\t@echo %s\n' % cppfile)
+ out.write('\t@$(CXX) $(CXXFLAGS) $(%s) $(CXX_OUT_FLAG)%s %s\n' % (include_defs, objfile, srcfile))
def mk_makefile(self, out):
include_defs = mk_fresh_name('includes')
@@ -166,22 +168,33 @@ class LibComponent(Component):
objs = []
for cppfile in glob.glob(os.path.join(self.src_dir, '*.cpp')):
cppfile = os.path.basename(cppfile)
- objfile = '%s/%s.$(OBJ)' % (self.build_dir, os.path.splitext(cppfile)[0])
+ objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
objs.append(objfile)
- libfile = '%s/%s.$(LIB)' % (self.build_dir, self.name)
+ libfile = '%s/%s$(LIB_EXT)' % (self.build_dir, self.name)
out.write('%s:' % libfile)
for obj in objs:
out.write(' ')
out.write(obj)
out.write('\n')
- out.write(' @$(MKLIB) $(MKLIB_OPT) $(MKLIBOUTFLAG)%s' % libfile)
+ out.write('\t@$(AR) $(AR_FLAGS) $(AR_OUTFLAG)%s' % libfile)
for obj in objs:
out.write(' ')
out.write(obj)
out.write('\n')
out.write('%s: %s\n\n' % (self.name, libfile))
+def comp_components(c1, c2):
+ id1 = _Name2Component[c1].id
+ id2 = _Name2Component[c2].id
+ if id1 < id2: return -1
+ if id2 > id1: return 1
+ return 0
+
+# Sort components based on definition time
+def sort_components(cnames):
+ return sorted(cnames, cmp=comp_components)
+
class ExeComponent(Component):
def __init__(self, name, exe_name, path, deps):
Component.__init__(self, name, EXE_KIND, path, deps)
@@ -194,27 +207,28 @@ class ExeComponent(Component):
Component.mk_makefile(self, out)
# generate rule for exe
- exefile = '%s.$(EXE)' % self.exe_name
+ exefile = '%s$(EXE_EXT)' % self.exe_name
out.write('%s:' % exefile)
- for dep in self.deps:
+ deps = sort_components(self.deps)
+ for dep in deps:
c_dep = _Name2Component[dep]
- out.write(' %s/%s.lib' % (c_dep.build_dir, c_dep.name))
+ out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
objs = []
for cppfile in glob.glob(os.path.join(self.src_dir, '*.cpp')):
cppfile = os.path.basename(cppfile)
- objfile = '%s/%s.$(OBJ)' % (self.build_dir, os.path.splitext(cppfile)[0])
+ objfile = '%s/%s$(OBJ_EXT)' % (self.build_dir, os.path.splitext(cppfile)[0])
objs.append(objfile)
for obj in objs:
out.write(' ')
out.write(obj)
out.write('\n')
- out.write(' $(MKEXE) $(EXEOUTFLAG)%s $(EXEFLAGS_OPT)' % exefile)
+ out.write('\t$(LINK) $(LINK_OUT_FLAG)%s $(LINK_FLAGS)' % exefile)
for obj in objs:
out.write(' ')
out.write(obj)
- for dep in self.deps:
+ for dep in deps:
c_dep = _Name2Component[dep]
- out.write(' %s/%s.lib' % (c_dep.build_dir, c_dep.name))
+ out.write(' %s/%s$(LIB_EXT)' % (c_dep.build_dir, c_dep.name))
out.write('\n')
out.write('%s: %s\n\n' % (self.name, exefile))
diff --git a/src/api/smtparser.cpp b/src/api/smtparser.cpp
index 55d49aa66..04f9ba619 100644
--- a/src/api/smtparser.cpp
+++ b/src/api/smtparser.cpp
@@ -46,7 +46,7 @@ Revision History:
#include "str_hashtable.h"
#include "front_end_params.h"
#include "stopwatch.h"
-front_end_params& Z3_API Z3_get_parameters(__in Z3_context c);
+front_end_params& Z3_API Z3_get_parameters(Z3_context c);
class id_param_info {
symbol m_string;
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index c4044d0d4..dcc7a1a0d 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -30,49 +30,6 @@ using namespace format_ns;
#define MAX_INDENT 16
#define SMALL_INDENT 2
-bool is_smt2_simple_symbol_char(char s) {
- return
- ('0' <= s && s <= '9') ||
- ('a' <= s && s <= 'z') ||
- ('A' <= s && s <= 'Z') ||
- s == '~' || s == '!' || s == '@' || s == '$' || s == '%' || s == '^' || s == '&' ||
- s == '*' || s == '_' || s == '-' || s == '+' || s == '=' || s == '<' || s == '>' ||
- s == '.' || s == '?' || s == '/';
-}
-
-bool is_smt2_quoted_symbol(char const * s) {
- if (s == 0)
- return false;
- if ('0' <= s[0] && s[0] <= '9')
- return true;
- unsigned len = static_cast<unsigned>(strlen(s));
- for (unsigned i = 0; i < len; i++)
- if (!is_smt2_simple_symbol_char(s[i]))
- return true;
- return false;
-}
-
-bool is_smt2_quoted_symbol(symbol const & s) {
- if (s.is_numerical())
- return false;
- return is_smt2_quoted_symbol(s.bare_str());
-}
-
-std::string mk_smt2_quoted_symbol(symbol const & s) {
- SASSERT(is_smt2_quoted_symbol(s));
- string_buffer<> buffer;
- buffer.append('|');
- char const * str = s.bare_str();
- while (*str) {
- if (*str == '|' || *str == '\\')
- buffer.append('\\');
- buffer.append(*str);
- str++;
- }
- buffer.append('|');
- return std::string(buffer.c_str());
-}
-
format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) const {
ast_manager & m = get_manager();
if (is_smt2_quoted_symbol(s)) {
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index a3550323a..048dd8d67 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -29,11 +29,7 @@ Revision History:
#include"array_decl_plugin.h"
#include"float_decl_plugin.h"
#include"dl_decl_plugin.h"
-
-bool is_smt2_simple_symbol_char(char c);
-bool is_smt2_quoted_symbol(char const * s);
-bool is_smt2_quoted_symbol(symbol const & s);
-std::string mk_smt2_quoted_symbol(symbol const & s);
+#include"smt2_util.h"
class smt2_pp_environment {
protected:
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index b9ae51859..06df0ff7e 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -712,14 +712,14 @@ namespace pdr {
pred_transformer& p = pt();
ast_manager& m = p.get_manager();
manager& pm = p.get_pdr_manager();
- TRACE("pdr", model_v2_pp(tout, model()););
+ TRACE("pdr", model_v2_pp(tout, get_model()););
func_decl* f = p.head();
unsigned arity = f->get_arity();
expr_ref_vector args(m);
func_decl_ref v(m);
for (unsigned i = 0; i < arity; ++i) {
v = pm.o2n(p.sig(i),0);
- expr* e = model().get_const_interp(v);
+ expr* e = get_model().get_const_interp(v);
if (e) {
args.push_back(e);
}
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index fe8bc8e90..e1bd42667 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -196,7 +196,7 @@ namespace pdr {
pred_transformer& pt() const { return m_pt; }
model_node* parent() const { return m_parent; }
model* model_ptr() const { return m_model.get(); }
- model const& model() const { return *m_model; }
+ model const& get_model() const { return *m_model; }
unsigned index() const;
bool is_closed() const { return m_closed; }
diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp
index a4e6a0ac1..1a9a6e0e0 100644
--- a/src/muz_qe/pdr_quantifiers.cpp
+++ b/src/muz_qe/pdr_quantifiers.cpp
@@ -418,10 +418,10 @@ namespace pdr {
// nodes from leaves that are repeated
// inside the search tree don't have models.
//
- if (!(&node.model())) {
+ if (!(&node.get_model())) {
return;
}
- m_current_rule = &pt.find_rule(node.model());
+ m_current_rule = &pt.find_rule(node.get_model());
m_current_pt = &pt;
m_current_node = &node;
if (!m_current_rule) {
diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp
index 1ec358fe1..3e1ebac46 100644
--- a/src/muz_qe/pdr_util.cpp
+++ b/src/muz_qe/pdr_util.cpp
@@ -908,9 +908,6 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
m_cfg(m, p) {}
};
- template class rewriter_tpl<ite_hoister_cfg>;
-
-
void hoist_non_bool_if(expr_ref& fml) {
ast_manager& m = fml.get_manager();
datalog::scoped_no_proof _sp(m);
@@ -1039,3 +1036,8 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
}
}
+
+template class rewriter_tpl<pdr::ite_hoister_cfg>;
+
+
+
diff --git a/src/muz_qe/qe_lite.cpp b/src/muz_qe/qe_lite.cpp
index d295327da..93a3dbfbf 100644
--- a/src/muz_qe/qe_lite.cpp
+++ b/src/muz_qe/qe_lite.cpp
@@ -498,7 +498,7 @@ public:
unsigned j = 0;
for (unsigned i = 0; i < vars.size(); ++i) {
if (used.contains(vars.size()-i-1)) {
- vars[j] = vars[i];
+ vars.set(j, vars.get(i));
++j;
}
}