From 1d795e9a5e9d0a72cefffbf9102b53a8b8bef895 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 23 Oct 2012 13:10:41 -0700 Subject: [PATCH] trying new build infrastructure on linux Signed-off-by: Leonardo de Moura --- scripts/mk_util.py | 42 ++++++++++++++++++++++----------- src/api/smtparser.cpp | 2 +- src/ast/ast_smt2_pp.cpp | 43 ---------------------------------- src/ast/ast_smt2_pp.h | 6 +---- src/muz_qe/pdr_context.cpp | 4 ++-- src/muz_qe/pdr_context.h | 2 +- src/muz_qe/pdr_quantifiers.cpp | 4 ++-- src/muz_qe/pdr_util.cpp | 8 ++++--- src/muz_qe/qe_lite.cpp | 2 +- 9 files changed, 41 insertions(+), 72 deletions(-) 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(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 const& formulas) { m_cfg(m, p) {} }; - template class rewriter_tpl; - - 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 const& formulas) { } } + +template class rewriter_tpl; + + + 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; } }