diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 6e7024b3f..05190f217 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -37,13 +37,13 @@ def init_project_def(): add_lib('nlsat_tactic', ['nlsat', 'sat_tactic', 'arith_tactics'], 'nlsat/tactic') add_lib('subpaving_tactic', ['core_tactics', 'subpaving'], 'math/subpaving/tactic') add_lib('aig_tactic', ['tactic'], 'tactic/aig') - add_lib('solver', ['model', 'tactic']) + add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') + add_lib('solver', ['model', 'tactic', 'proofs']) add_lib('ackermannization', ['model', 'rewriter', 'ast', 'solver', 'tactic'], 'ackermannization') add_lib('interp', ['solver']) add_lib('cmd_context', ['solver', 'rewriter', 'interp']) add_lib('extra_cmds', ['cmd_context', 'subpaving_tactic', 'arith_tactics'], 'cmd_context/extra_cmds') add_lib('smt2parser', ['cmd_context', 'parser_util'], 'parsers/smt2') - add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') add_lib('fpa', ['ast', 'util', 'rewriter', 'model'], 'ast/fpa') add_lib('pattern', ['normal_forms', 'smt2parser', 'rewriter'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'rewriter'], 'ast/rewriter/bit_blaster') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 6f3052f6e..d44e8f416 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -72,6 +72,7 @@ IS_FREEBSD=False IS_OPENBSD=False IS_CYGWIN=False IS_CYGWIN_MINGW=False +IS_MSYS2=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -152,6 +153,9 @@ def is_cygwin(): def is_cygwin_mingw(): return IS_CYGWIN_MINGW +def is_msys2(): + return IS_MSYS2 + def norm_path(p): return os.path.expanduser(os.path.normpath(p)) @@ -227,7 +231,7 @@ def rmf(fname): def exec_compiler_cmd(cmd): r = exec_cmd(cmd) - if is_windows() or is_cygwin_mingw(): + if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2(): rmf('a.exe') else: rmf('a.out') @@ -606,6 +610,13 @@ elif os.name == 'posix': IS_CYGWIN=True if (CC != None and "mingw" in CC): IS_CYGWIN_MINGW=True + elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'): + IS_MSYS2=True + if os.uname()[4] == 'x86_64': + LINUX_X64=True + else: + LINUX_X64=False + def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1229,7 +1240,7 @@ def get_so_ext(): sysname = os.uname()[0] if sysname == 'Darwin': return 'dylib' - elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD': + elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): return 'so' elif sysname == 'CYGWIN': return 'dll' @@ -1783,6 +1794,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'openbsd') elif IS_CYGWIN: t = t.replace('PLATFORM', 'cygwin') + elif IS_MSYS2: + t = t.replace('PLATFORM', 'win32') else: t = t.replace('PLATFORM', 'win32') out.write(t) @@ -1875,7 +1888,6 @@ class MLComponent(Component): def _init_ocamlfind_paths(self): """ Initialises self.destdir and self.ldconf - Do not call this from the MLComponent constructor because OCAMLFIND has not been checked at that point """ @@ -2446,7 +2458,7 @@ def mk_config(): if sysname == 'Darwin': SO_EXT = '.dylib' SLIBFLAGS = '-dynamiclib' - elif sysname == 'Linux': + elif sysname == 'Linux' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'): CXXFLAGS = '%s -D_LINUX_' % CXXFLAGS OS_DEFINES = '-D_LINUX_' SO_EXT = '.so' @@ -2466,10 +2478,10 @@ def mk_config(): SO_EXT = '.so' SLIBFLAGS = '-shared' elif sysname[:6] == 'CYGWIN': - CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS + CXXFLAGS = '%s -D_CYGWIN' % CXXFLAGS OS_DEFINES = '-D_CYGWIN' - SO_EXT = '.dll' - SLIBFLAGS = '-shared' + SO_EXT = '.dll' + SLIBFLAGS = '-shared' else: raise MKException('Unsupported platform: %s' % sysname) if is64(): @@ -3160,7 +3172,6 @@ class MakeRuleCmd(object): """ These class methods provide a convenient way to emit frequently needed commands used in Makefile rules - Note that several of the method are meant for use during ``make install`` and ``make uninstall``. These methods correctly use ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable @@ -3336,10 +3347,8 @@ def configure_file(template_file_path, output_file_path, substitutions): Read a template file ``template_file_path``, perform substitutions found in the ``substitutions`` dictionary and write the result to the output file ``output_file_path``. - The template file should contain zero or more template strings of the form ``@NAME@``. - The substitutions dictionary maps old strings (without the ``@`` symbols) to their replacements. """ diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 3dbd0bc69..98c1bdfed 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1683,7 +1683,7 @@ ast * ast_manager::register_node_core(ast * n) { bool contains = m_ast_table.contains(n); CASSERT("nondet_bug", contains || slow_not_contains(n)); #endif - + #if 0 static unsigned counter = 0; counter++; @@ -1719,12 +1719,6 @@ ast * ast_manager::register_node_core(ast * n) { n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - static unsigned count = 0; - if (n->m_id == 404) { - ++count; - //if (count == 2) SASSERT(false); - } - TRACE("ast", tout << "Object " << n->m_id << " was created.\n";); TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";); // increment reference counters @@ -2626,7 +2620,7 @@ bool ast_manager::is_fully_interp(sort * s) const { proof * ast_manager::mk_proof(family_id fid, decl_kind k, unsigned num_args, expr * const * args) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(fid, k, num_args, args); } @@ -2842,23 +2836,20 @@ proof * ast_manager::mk_distributivity(expr * s, expr * r) { } proof * ast_manager::mk_rewrite(expr * s, expr * t) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t)); } proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t)); } proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_eq(s, t)); @@ -2866,44 +2857,38 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr } proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q)); } proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q)); } proof * ast_manager::mk_push_quant(quantifier * q, expr * e) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e)); } proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e)); } proof * ast_manager::mk_der(quantifier * q, expr * e) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e)); } proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; vector params; for (unsigned i = 0; i < num_bind; ++i) { params.push_back(parameter(binding[i])); @@ -2937,9 +2922,8 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const { } proof * ast_manager::mk_def_axiom(expr * ax) { - SASSERT(proofs_enabled()); if (proofs_disabled()) - return m_undef_proof; + return nullptr; return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax); } @@ -3077,7 +3061,7 @@ proof * ast_manager::mk_def_intro(expr * new_def) { proof * ast_manager::mk_apply_defs(expr * n, expr * def, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(n, def)); @@ -3110,7 +3094,7 @@ bool ast_manager::check_nnf_proof_parents(unsigned num_proofs, proof * const * p proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; check_nnf_proof_parents(num_proofs, proofs); ptr_buffer args; args.append(num_proofs, (expr**) proofs); @@ -3120,7 +3104,7 @@ proof * ast_manager::mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; check_nnf_proof_parents(num_proofs, proofs); ptr_buffer args; args.append(num_proofs, (expr**) proofs); @@ -3130,7 +3114,7 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(s, t)); @@ -3139,7 +3123,7 @@ proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof proof * ast_manager::mk_skolemization(expr * q, expr * e) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(is_bool(q)); SASSERT(is_bool(e)); return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e)); @@ -3147,7 +3131,7 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) { proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; args.append(num_proofs, (expr**) proofs); args.push_back(mk_oeq(s, t)); @@ -3156,7 +3140,7 @@ proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof proof * ast_manager::mk_and_elim(proof * p, unsigned i) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(has_fact(p)); SASSERT(is_and(get_fact(p))); CTRACE("mk_and_elim", i >= to_app(get_fact(p))->get_num_args(), tout << "i: " << i << "\n" << mk_pp(get_fact(p), *this) << "\n";); @@ -3167,7 +3151,7 @@ proof * ast_manager::mk_and_elim(proof * p, unsigned i) { proof * ast_manager::mk_not_or_elim(proof * p, unsigned i) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; SASSERT(has_fact(p)); SASSERT(is_not(get_fact(p))); SASSERT(is_or(to_app(get_fact(p))->get_arg(0))); @@ -3190,7 +3174,7 @@ proof * ast_manager::mk_th_lemma( ) { if (proofs_disabled()) - return m_undef_proof; + return nullptr; ptr_buffer args; vector parameters; diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index e4a875005..0139cb0f0 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -44,6 +44,7 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len) co return mk_string(m, str.c_str()); } else if (!s.bare_str()) { + len = 4; return mk_string(m, "null"); } else { diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index f5f72674d..2abd6d467 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -351,7 +351,6 @@ void rewriter_tpl::process_app(app * t, frame & fr) { if (is_ground(def)) { m_r = def; if (ProofGen) { - SASSERT(def_pr); m_pr = m().mk_transitivity(m_pr, def_pr); } } @@ -510,7 +509,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { new_no_pats = q->get_no_patterns(); } if (ProofGen) { - quantifier * new_q = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body); + quantifier_ref new_q(m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body), m()); m_pr = q == new_q ? 0 : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos)); m_r = new_q; proof_ref pr2(m()); diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index c9ad8fd56..5dc2283ae 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -1575,6 +1575,7 @@ namespace Duality { */ int RPFP::SubtermTruth(hash_map &memo, const Term &f) { + TRACE("duality", tout << f << "\n";); if (memo.find(f) != memo.end()) { return memo[f]; } @@ -1657,83 +1658,6 @@ namespace Duality { ands and, or, not. Returns result in memo. */ -#if 0 - int RPFP::GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos){ - if(memo[labpos].find(f) != memo[labpos].end()){ - return memo[labpos][f]; - } - int res; - if(f.is_app()){ - int nargs = f.num_args(); - decl_kind k = f.decl().get_decl_kind(); - if(k == Implies){ - res = GetLabelsRec(memo,f.arg(1) || !f.arg(0), labels, labpos); - goto done; - } - if(k == And) { - res = 1; - for(int i = 0; i < nargs; i++){ - int ar = GetLabelsRec(memo,f.arg(i), labels, labpos); - if(ar == 0){ - res = 0; - goto done; - } - if(ar == 2)res = 2; - } - goto done; - } - else if(k == Or) { - res = 0; - for(int i = 0; i < nargs; i++){ - int ar = GetLabelsRec(memo,f.arg(i), labels, labpos); - if(ar == 1){ - res = 1; - goto done; - } - if(ar == 2)res = 2; - } - goto done; - } - else if(k == Not) { - int ar = GetLabelsRec(memo,f.arg(0), labels, !labpos); - res = (ar == 0) ? 1 : ((ar == 1) ? 0 : 2); - goto done; - } - } - { - bool pos; std::vector names; - if(f.is_label(pos,names)){ - res = GetLabelsRec(memo,f.arg(0), labels, labpos); - if(pos == labpos && res == (pos ? 1 : 0)) - for(unsigned i = 0; i < names.size(); i++) - labels.push_back(names[i]); - goto done; - } - } - { - expr bv = dualModel.eval(f); - if(bv.is_app() && bv.decl().get_decl_kind() == Equal && - bv.arg(0).is_array()){ - bv = EvalArrayEquality(bv); - } - // Hack!!!! array equalities can occur negatively! - if(bv.is_app() && bv.decl().get_decl_kind() == Not && - bv.arg(0).decl().get_decl_kind() == Equal && - bv.arg(0).arg(0).is_array()){ - bv = dualModel.eval(!EvalArrayEquality(bv.arg(0))); - } - if(eq(bv,ctx.bool_val(true))) - res = 1; - else if(eq(bv,ctx.bool_val(false))) - res = 0; - else - res = 2; - } - done: - memo[labpos][f] = res; - return res; - } -#endif void RPFP::GetLabelsRec(hash_map &memo, const Term &f, std::vector &labels, hash_set *done, bool truth) { @@ -1748,8 +1672,13 @@ namespace Duality { } if (k == Iff) { int b = SubtermTruth(memo, f.arg(0)); - if (b == 2) - throw "disaster in GetLabelsRec"; + if (b == 2) { + goto done; + // bypass error + std::ostringstream os; + os << "disaster in SubtermTruth processing " << f; + throw default_exception(os.str()); + } GetLabelsRec(memo, f.arg(1), labels, done, truth ? b : !b); goto done; } @@ -1825,8 +1754,11 @@ namespace Duality { } if (k == Iff) { int b = SubtermTruth(memo, f.arg(0)); - if (b == 2) - throw "disaster in ImplicantRed"; + if (b == 2) { + std::ostringstream os; + os << "disaster in SubtermTruth processing " << f; + throw default_exception(os.str()); + } ImplicantRed(memo, f.arg(1), lits, done, truth ? b : !b, dont_cares); goto done; } diff --git a/src/muz/dataflow/dataflow.h b/src/muz/dataflow/dataflow.h index 5e91a0149..6f3010940 100644 --- a/src/muz/dataflow/dataflow.h +++ b/src/muz/dataflow/dataflow.h @@ -62,8 +62,7 @@ namespace datalog { rule_set::decl2rules m_body2rules; void init_bottom_up() { - for (rule_set::iterator it = m_rules.begin(); it != m_rules.end(); ++it) { - rule* cur = *it; + for (rule* cur : m_rules) { for (unsigned i = 0; i < cur->get_uninterpreted_tail_size(); ++i) { func_decl *d = cur->get_decl(i); rule_set::decl2rules::obj_map_entry *e = m_body2rules.insert_if_not_there2(d, 0); @@ -83,31 +82,25 @@ namespace datalog { } void init_top_down() { - const func_decl_set& output_preds = m_rules.get_output_predicates(); - for (func_decl_set::iterator I = output_preds.begin(), - E = output_preds.end(); I != E; ++I) { - func_decl* sym = *I; + for (func_decl* sym : m_rules.get_output_predicates()) { TRACE("dl", tout << sym->get_name() << "\n";); const rule_vector& output_rules = m_rules.get_predicate_rules(sym); - for (unsigned i = 0; i < output_rules.size(); ++i) { - m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, output_rules[i]); + for (rule* r : output_rules) { + m_facts.insert_if_not_there2(sym, Fact())->get_data().m_value.init_down(m_context, r); m_todo[m_todo_idx].insert(sym); } } } void step_bottom_up() { - for(todo_set::iterator I = m_todo[m_todo_idx].begin(), - E = m_todo[m_todo_idx].end(); I!=E; ++I) { + for (func_decl* f : m_todo[m_todo_idx]) { ptr_vector * rules; - if (!m_body2rules.find(*I, rules)) + if (!m_body2rules.find(f, rules)) continue; - - for (ptr_vector::iterator I2 = rules->begin(), - E2 = rules->end(); I2 != E2; ++I2) { - func_decl* head_sym = (*I2)->get_head()->get_decl(); - fact_reader tail_facts(m_facts, *I2); - bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, *I2, tail_facts); + for (rule* r : *rules) { + func_decl* head_sym = r->get_head()->get_decl(); + fact_reader tail_facts(m_facts, r); + bool new_info = m_facts.insert_if_not_there2(head_sym, Fact())->get_data().m_value.propagate_up(m_context, r, tail_facts); if (new_info) { m_todo[!m_todo_idx].insert(head_sym); } @@ -119,15 +112,11 @@ namespace datalog { } void step_top_down() { - for(todo_set::iterator I = m_todo[m_todo_idx].begin(), - E = m_todo[m_todo_idx].end(); I!=E; ++I) { - func_decl* head_sym = *I; + for (func_decl* head_sym : m_todo[m_todo_idx]) { // We can't use a reference here because we are changing the map while using the reference const Fact head_fact = m_facts.get(head_sym, Fact::null_fact); const rule_vector& deps = m_rules.get_predicate_rules(head_sym); - const unsigned deps_size = deps.size(); - for (unsigned i = 0; i < deps_size; ++i) { - rule *trg_rule = deps[i]; + for (rule* trg_rule : deps) { fact_writer writer(m_facts, trg_rule, m_todo[!m_todo_idx]); // Generate new facts head_fact.propagate_down(m_context, trg_rule, writer); @@ -146,16 +135,13 @@ namespace datalog { dataflow_engine(typename Fact::ctx_t& ctx, const rule_set& rules) : m_rules(rules), m_todo_idx(0), m_context(ctx) {} ~dataflow_engine() { - for (rule_set::decl2rules::iterator it = m_body2rules.begin(); it != m_body2rules.end(); ++it) { - dealloc(it->m_value); - } + for (auto & kv : m_body2rules) + dealloc(kv.m_value); } void dump(std::ostream& outp) { obj_hashtable visited; - for (rule_set::iterator I = m_rules.begin(), - E = m_rules.end(); I != E; ++I) { - const rule* r = *I; + for (rule const* r : m_rules) { func_decl* head_decl = r->get_decl(); obj_hashtable::entry *dummy; if (visited.insert_if_not_there_core(head_decl, dummy)) { @@ -194,30 +180,30 @@ namespace datalog { iterator end() const { return m_facts.end(); } void join(const dataflow_engine& oth) { - for (typename fact_db::iterator I = oth.m_facts.begin(), - E = oth.m_facts.end(); I != E; ++I) { + for (auto const& kv : oth.m_facts) { typename fact_db::entry* entry; - if (m_facts.insert_if_not_there_core(I->m_key, entry)) { - entry->get_data().m_value = I->m_value; - } else { - entry->get_data().m_value.join(m_context, I->m_value); + if (m_facts.insert_if_not_there_core(kv.m_key, entry)) { + entry->get_data().m_value = kv.m_value; + } + else { + entry->get_data().m_value.join(m_context, kv.m_value); } } } void intersect(const dataflow_engine& oth) { - vector to_delete; - for (typename fact_db::iterator I = m_facts.begin(), - E = m_facts.end(); I != E; ++I) { + ptr_vector to_delete; + for (auto const& kv : m_facts) { - if (typename fact_db::entry *entry = oth.m_facts.find_core(I->m_key)) { - I->m_value.intersect(m_context, entry->get_data().m_value); - } else { - to_delete.push_back(I->m_key); + if (typename fact_db::entry *entry = oth.m_facts.find_core(kv.m_key)) { + kv.m_value.intersect(m_context, entry->get_data().m_value); + } + else { + to_delete.push_back(kv.m_key); } } - for (unsigned i = 0; i < to_delete.size(); ++i) { - m_facts.erase(to_delete[i]); + for (func_decl* f : to_delete) { + m_facts.erase(f); } } }; diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index cab19c8ef..8194379b8 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -134,8 +134,8 @@ public: {return m_solver.get_num_assumptions();} virtual expr * get_assumption(unsigned idx) const {return m_solver.get_assumption(idx);} - virtual std::ostream &display(std::ostream &out) const - { return m_solver.display(out); } + virtual std::ostream &display(std::ostream &out, unsigned n, expr* const* es) const + { return m_solver.display(out, n, es); } /* check_sat_result interface */ diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index 546b7df5b..7fb17329e 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -74,15 +74,6 @@ inline std::ostream& operator<<(std::ostream& out, pp_level const& p) } -struct scoped_watch { - stopwatch &m_sw; - scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw) - { - if(reset) { m_sw.reset(); } - m_sw.start (); - } - ~scoped_watch () {m_sw.stop ();} -}; typedef ptr_vector app_vector; diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp index 89b9fb531..938e8cb94 100644 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ b/src/muz/spacer/spacer_virtual_solver.cpp @@ -189,15 +189,16 @@ void virtual_solver::push_core() m_context.push(); } } -void virtual_solver::pop_core(unsigned n) -{ +void virtual_solver::pop_core(unsigned n) { SASSERT(!m_pushed || get_scope_level() > 0); if (m_pushed) { SASSERT(!m_in_delay_scope); m_context.pop(n); m_pushed = get_scope_level() - n > 0; - } else - { m_in_delay_scope = get_scope_level() - n > 0; } + } + else { + m_in_delay_scope = get_scope_level() - n > 0; + } } void virtual_solver::get_unsat_core(ptr_vector &r) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 31188bf43..3ea0e305a 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -21,6 +21,7 @@ Author: #include "muz/dataflow/dataflow.h" #include "muz/dataflow/reachability.h" #include "ast/ast_pp.h" +#include "ast/ast_util.h" #include "tactic/extension_model_converter.h" namespace datalog { @@ -33,20 +34,28 @@ namespace datalog { rule_set * mk_coi_filter::bottom_up(rule_set const & source) { dataflow_engine engine(source.get_manager(), source); engine.run_bottom_up(); + func_decl_set unreachable; scoped_ptr res = alloc(rule_set, m_context); res->inherit_predicates(source); - for (rule_set::iterator it = source.begin(); it != source.end(); ++it) { - rule * r = *it; - + for (rule* r : source) { bool new_tail = false; bool contained = true; + m_new_tail.reset(); + m_new_tail_neg.reset(); for (unsigned i = 0; i < r->get_uninterpreted_tail_size(); ++i) { - if (m_context.has_facts(r->get_decl(i))) { + func_decl* decl_i = r->get_decl(i); + if (m_context.has_facts(decl_i)) { return 0; } + bool reachable = engine.get_fact(decl_i).is_reachable(); + + if (!reachable) { + unreachable.insert(decl_i); + } + if (r->is_neg_tail(i)) { - if (!engine.get_fact(r->get_decl(i)).is_reachable()) { + if (!reachable) { if (!new_tail) { for (unsigned j = 0; j < i; ++j) { m_new_tail.push_back(r->get_tail(j)); @@ -60,10 +69,9 @@ namespace datalog { m_new_tail_neg.push_back(true); } } - else { SASSERT(!new_tail); - if (!engine.get_fact(r->get_decl(i)).is_reachable()) { + if (!reachable) { contained = false; break; } @@ -78,24 +86,26 @@ namespace datalog { res->add_rule(r); } } - m_new_tail.reset(); - m_new_tail_neg.reset(); } if (res->get_num_rules() == source.get_num_rules()) { TRACE("dl", tout << "No transformation\n";); res = 0; - } else { + } + else { res->close(); } - + // set to false each unreached predicate - if (m_context.get_model_converter()) { + if (res && m_context.get_model_converter()) { extension_model_converter* mc0 = alloc(extension_model_converter, m); - for (dataflow_engine::iterator it = engine.begin(); it != engine.end(); it++) { - if (!it->m_value.is_reachable()) { - mc0->insert(it->m_key, m.mk_false()); + for (auto const& kv : engine) { + if (!kv.m_value.is_reachable()) { + mc0->insert(kv.m_key, m.mk_false()); } } + for (func_decl* f : unreachable) { + mc0->insert(f, m.mk_false()); + } m_context.add_model_converter(mc0); } CTRACE("dl", 0 != res, res->display(tout);); @@ -109,9 +119,7 @@ namespace datalog { scoped_ptr res = alloc(rule_set, m_context); res->inherit_predicates(source); - rule_set::iterator rend = source.end(); - for (rule_set::iterator rit = source.begin(); rit != rend; ++rit) { - rule * r = *rit; + for (rule * r : source) { func_decl * pred = r->get_decl(); if (engine.get_fact(pred).is_reachable()) { res->add_rule(r); @@ -125,14 +133,12 @@ namespace datalog { res = 0; } if (res && m_context.get_model_converter()) { - func_decl_set::iterator end = pruned_preds.end(); - func_decl_set::iterator it = pruned_preds.begin(); extension_model_converter* mc0 = alloc(extension_model_converter, m); - for (; it != end; ++it) { - const rule_vector& rules = source.get_predicate_rules(*it); + for (func_decl* f : pruned_preds) { + const rule_vector& rules = source.get_predicate_rules(f); expr_ref_vector fmls(m); - for (unsigned i = 0; i < rules.size(); ++i) { - app* head = rules[i]->get_head(); + for (rule * r : rules) { + app* head = r->get_head(); expr_ref_vector conj(m); for (unsigned j = 0; j < head->get_num_args(); ++j) { expr* arg = head->get_arg(j); @@ -140,11 +146,9 @@ namespace datalog { conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg)); } } - fmls.push_back(m.mk_and(conj.size(), conj.c_ptr())); + fmls.push_back(mk_and(conj)); } - expr_ref fml(m); - fml = m.mk_or(fmls.size(), fmls.c_ptr()); - mc0->insert(*it, fml); + mc0->insert(f, mk_or(fmls)); } m_context.add_model_converter(mc0); } diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 69b62083f..49b48e68f 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -47,8 +47,9 @@ namespace opt { m_dump_benchmarks(false), m_first(true), m_was_unknown(false) { + solver::updt_params(p); m_params.updt_params(p); - if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { + if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) { m_params.m_relevancy_lvl = 0; } // m_params.m_auto_config = false; diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index be418cbc4..191c49294 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -69,7 +69,7 @@ class inc_sat_solver : public solver { public: inc_sat_solver(ast_manager& m, params_ref const& p): m(m), m_solver(p, m.limit(), 0), - m_params(p), m_optimize_model(false), + m_optimize_model(false), m_fmls(m), m_asmsf(m), m_fmls_head(0), @@ -79,7 +79,7 @@ public: m_dep_core(m), m_unknown("no reason given") { m_params.set_bool("elim_vars", false); - m_solver.updt_params(m_params); + updt_params(p); init_preprocess(); } @@ -237,7 +237,7 @@ public: sat::solver::collect_param_descrs(r); } virtual void updt_params(params_ref const & p) { - m_params = p; + solver::updt_params(p); m_params.set_bool("elim_vars", false); m_solver.updt_params(m_params); m_optimize_model = m_params.get_bool("optimize_model", false); diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index dd92f250a..56600266a 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -511,11 +511,14 @@ void asserted_formulas::update_substitution(expr* n, proof* pr) { } TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";); } - if (m.is_not(n, n1)) { - m_scoped_substitution.insert(n1, m.mk_false(), m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr); + proof_ref pr1(m); + if (m.is_not(n, n1)) { + pr1 = m.proofs_enabled() ? m.mk_iff_false(pr) : nullptr; + m_scoped_substitution.insert(n1, m.mk_false(), pr1); } else { - m_scoped_substitution.insert(n, m.mk_true(), m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr); + pr1 = m.proofs_enabled() ? m.mk_iff_true(pr) : nullptr; + m_scoped_substitution.insert(n, m.mk_true(), pr1); } } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c508a65cb..7b508c7d8 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4389,7 +4389,8 @@ namespace smt { subst.push_back(arg); } expr_ref bodyr(m); - var_subst sub(m, false); + var_subst sub(m, true); + TRACE("context", tout << expr_ref(q, m) << " " << subst << "\n";); sub(body, subst.size(), subst.c_ptr(), bodyr); func_decl* f = to_app(fn)->get_decl(); func_interp* fi = alloc(func_interp, m, f->get_arity()); diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index d624a5c9a..1f9ad3ef7 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -29,9 +29,8 @@ Notes: namespace smt { - class solver : public solver_na2as { + class smt_solver : public solver_na2as { smt_params m_smt_params; - params_ref m_params; smt::kernel m_context; progress_callback * m_callback; symbol m_logic; @@ -42,28 +41,24 @@ namespace smt { obj_map m_name2assertion; public: - solver(ast_manager & m, params_ref const & p, symbol const & l) : + smt_solver(ast_manager & m, params_ref const & p, symbol const & l) : solver_na2as(m), m_smt_params(p), - m_params(p), m_context(m, m_smt_params), m_minimizing_core(false), m_core_extend_patterns(false), m_core_extend_patterns_max_distance(UINT_MAX), - m_core_extend_nonlocal_patterns(false) { + m_core_extend_nonlocal_patterns(false) { m_logic = l; if (m_logic != symbol::null) m_context.set_logic(m_logic); - smt_params_helper smth(p); - m_core_extend_patterns = smth.core_extend_patterns(); - m_core_extend_patterns_max_distance = smth.core_extend_patterns_max_distance(); - m_core_extend_nonlocal_patterns = smth.core_extend_nonlocal_patterns(); + updt_params(p); } virtual solver * translate(ast_manager & m, params_ref const & p) { ast_translation translator(get_manager(), m); - solver * result = alloc(solver, m, p, m_logic); + smt_solver * result = alloc(smt_solver, m, p, m_logic); smt::kernel::copy(m_context, result->m_context); for (auto & kv : m_name2assertion) @@ -73,13 +68,13 @@ namespace smt { return result; } - virtual ~solver() { + virtual ~smt_solver() { dec_ref_values(get_manager(), m_name2assertion); } virtual void updt_params(params_ref const & p) { + solver::updt_params(p); m_smt_params.updt_params(p); - m_params.copy(p); m_context.updt_params(p); smt_params_helper smth(p); m_core_extend_patterns = smth.core_extend_patterns(); @@ -146,9 +141,9 @@ namespace smt { } struct scoped_minimize_core { - solver& s; + smt_solver& s; expr_ref_vector m_assumptions; - scoped_minimize_core(solver& s) : s(s), m_assumptions(s.m_assumptions) { + scoped_minimize_core(smt_solver& s) : s(s), m_assumptions(s.m_assumptions) { s.m_minimizing_core = true; s.m_assumptions.reset(); } @@ -165,7 +160,7 @@ namespace smt { r.push_back(m_context.get_unsat_core_expr(i)); } - if (m_minimizing_core && smt_params_helper(m_params).core_minimize()) { + if (m_minimizing_core && smt_params_helper(get_params()).core_minimize()) { scoped_minimize_core scm(*this); mus mus(*this); mus.add_soft(r.size(), r.c_ptr()); @@ -346,22 +341,16 @@ namespace smt { void add_nonlocal_pattern_literals_to_core(ptr_vector & core) { ast_manager & m = get_manager(); - - obj_map::iterator it = m_name2assertion.begin(); - obj_map::iterator end = m_name2assertion.end(); - for (unsigned i = 0; it != end; it++, i++) { - expr_ref name(it->m_key, m); - expr_ref assrtn(it->m_value, m); + for (auto const& kv : m_name2assertion) { + expr_ref name(kv.m_key, m); + expr_ref assrtn(kv.m_value, m); if (!core.contains(name)) { func_decl_set pattern_fds, body_fds; collect_pattern_fds(assrtn, pattern_fds); collect_body_func_decls(assrtn, body_fds); - func_decl_set::iterator pit = pattern_fds.begin(); - func_decl_set::iterator pend= pattern_fds.end(); - for (; pit != pend; pit++) { - func_decl * fd = *pit; + for (func_decl *fd : pattern_fds) { if (!body_fds.contains(fd)) { core.insert(name); break; @@ -374,7 +363,7 @@ namespace smt { }; solver * mk_smt_solver(ast_manager & m, params_ref const & p, symbol const & logic) { - return alloc(smt::solver, m, p, logic); + return alloc(smt::smt_solver, m, p, logic); } class smt_solver_factory : public solver_factory { diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h index 203dd24d2..59f5521c5 100644 --- a/src/smt/theory_diff_logic_def.h +++ b/src/smt/theory_diff_logic_def.h @@ -683,7 +683,9 @@ void theory_diff_logic::set_neg_cycle_conflict() { vector params; if (get_manager().proofs_enabled()) { params.push_back(parameter(symbol("farkas"))); - params.resize(lits.size()+1, parameter(rational(1))); + for (unsigned i = 0; i <= lits.size(); ++i) { + params.push_back(parameter(rational(1))); + } } ctx.set_conflict( diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index fb191626f..a1f0f9777 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -166,14 +166,18 @@ namespace smt { } } - void theory_str::assert_axiom(expr * e) { + void theory_str::assert_axiom(expr * _e) { if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } - if (get_manager().is_true(e)) return; - TRACE("str", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;); + if (get_manager().is_true(_e)) return; context & ctx = get_context(); + ast_manager& m = get_manager(); + TRACE("str", tout << "asserting " << mk_ismt2_pp(_e, m) << std::endl;); + expr_ref e(_e, m); + //th_rewriter rw(m); + //rw(e); if (!ctx.b_internalized(e)) { ctx.internalize(e, false); } @@ -1422,104 +1426,6 @@ namespace smt { assert_axiom(finalAxiom); } - void theory_str::instantiate_axiom_Substr(enode * e) { - context & ctx = get_context(); - ast_manager & m = get_manager(); - - app * expr = e->get_owner(); - if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up Substr axiom for " << mk_pp(expr, m) << std::endl;); - return; - } - axiomatized_terms.insert(expr); - - TRACE("str", tout << "instantiate Substr axiom for " << mk_pp(expr, m) << std::endl;); - - expr_ref substrBase(expr->get_arg(0), m); - expr_ref substrPos(expr->get_arg(1), m); - expr_ref substrLen(expr->get_arg(2), m); - SASSERT(substrBase); - SASSERT(substrPos); - SASSERT(substrLen); - - expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m); - expr_ref minusOne(m_autil.mk_numeral(rational::minus_one(), true), m); - SASSERT(zero); - SASSERT(minusOne); - - expr_ref_vector argumentsValid_terms(m); - // pos >= 0 - argumentsValid_terms.push_back(m_autil.mk_ge(substrPos, zero)); - // pos < strlen(base) - // --> pos + -1*strlen(base) < 0 - argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge( - m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)), - zero))); - - // len >= 0 - argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero)); - - expr_ref argumentsValid(mk_and(argumentsValid_terms), m); - SASSERT(argumentsValid); - ctx.internalize(argumentsValid, false); - - // (pos+len) >= strlen(base) - // --> pos + len + -1*strlen(base) >= 0 - expr_ref lenOutOfBounds(m_autil.mk_ge( - m_autil.mk_add(substrPos, substrLen, m_autil.mk_mul(minusOne, mk_strlen(substrBase))), - zero), m); - SASSERT(lenOutOfBounds); - ctx.internalize(argumentsValid, false); - - // Case 1: pos < 0 or pos >= strlen(base) or len < 0 - // ==> (Substr ...) = "" - expr_ref case1_premise(mk_not(m, argumentsValid), m); - SASSERT(case1_premise); - ctx.internalize(case1_premise, false); - expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); - SASSERT(case1_conclusion); - ctx.internalize(case1_conclusion, false); - expr_ref case1(rewrite_implication(case1_premise, case1_conclusion), m); - SASSERT(case1); - - // Case 2: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) >= strlen(base) - // ==> base = t0.t1 AND len(t0) = pos AND (Substr ...) = t1 - expr_ref t0(mk_str_var("t0"), m); - expr_ref t1(mk_str_var("t1"), m); - expr_ref case2_conclusion(m.mk_and( - ctx.mk_eq_atom(substrBase, mk_concat(t0,t1)), - ctx.mk_eq_atom(mk_strlen(t0), substrPos), - ctx.mk_eq_atom(expr, t1)), m); - expr_ref case2(rewrite_implication(m.mk_and(argumentsValid, lenOutOfBounds), case2_conclusion), m); - SASSERT(case2); - - // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base) - // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3 - - expr_ref t2(mk_str_var("t2"), m); - expr_ref t3(mk_str_var("t3"), m); - expr_ref t4(mk_str_var("t4"), m); - expr_ref_vector case3_conclusion_terms(m); - case3_conclusion_terms.push_back(ctx.mk_eq_atom(substrBase, mk_concat(t2, mk_concat(t3, t4)))); - case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t2), substrPos)); - case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen)); - case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3)); - expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); - expr_ref case3(rewrite_implication(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m); - SASSERT(case3); - - ctx.internalize(case1, false); - ctx.internalize(case2, false); - ctx.internalize(case3, false); - - expr_ref finalAxiom(m.mk_and(case1, case2, case3), m); - SASSERT(finalAxiom); - assert_axiom(finalAxiom); - } - -#if 0 - // rewrite - // requires to add th_rewriter to assert_axiom to enforce normal form. void theory_str::instantiate_axiom_Substr(enode * e) { context & ctx = get_context(); ast_manager & m = get_manager(); @@ -1551,6 +1457,7 @@ namespace smt { argumentsValid_terms.push_back(mk_not(m, m_autil.mk_ge( m_autil.mk_add(substrPos, m_autil.mk_mul(minusOne, substrLen)), zero))); + // len >= 0 argumentsValid_terms.push_back(m_autil.mk_ge(substrLen, zero)); @@ -1564,7 +1471,7 @@ namespace smt { // Case 1: pos < 0 or pos >= strlen(base) or len < 0 // ==> (Substr ...) = "" - expr_ref case1_premise(mk_not(m, argumentsValid), m); + expr_ref case1_premise(m.mk_not(argumentsValid), m); expr_ref case1_conclusion(ctx.mk_eq_atom(expr, mk_string("")), m); expr_ref case1(m.mk_implies(case1_premise, case1_conclusion), m); @@ -1580,6 +1487,7 @@ namespace smt { // Case 3: (pos >= 0 and pos < strlen(base) and len >= 0) and (pos+len) < strlen(base) // ==> base = t2.t3.t4 AND len(t2) = pos AND len(t3) = len AND (Substr ...) = t3 + expr_ref t2(mk_str_var("t2"), m); expr_ref t3(mk_str_var("t3"), m); expr_ref t4(mk_str_var("t4"), m); @@ -1589,13 +1497,24 @@ namespace smt { case3_conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(t3), substrLen)); case3_conclusion_terms.push_back(ctx.mk_eq_atom(expr, t3)); expr_ref case3_conclusion(mk_and(case3_conclusion_terms), m); - expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, mk_not(m, lenOutOfBounds)), case3_conclusion), m); + expr_ref case3(m.mk_implies(m.mk_and(argumentsValid, m.mk_not(lenOutOfBounds)), case3_conclusion), m); - assert_axiom(case1); - assert_axiom(case2); - assert_axiom(case3); + { + th_rewriter rw(m); + + expr_ref case1_rw(case1, m); + rw(case1_rw); + assert_axiom(case1_rw); + + expr_ref case2_rw(case2, m); + rw(case2_rw); + assert_axiom(case2_rw); + + expr_ref case3_rw(case3, m); + rw(case3_rw); + assert_axiom(case3_rw); + } } -#endif void theory_str::instantiate_axiom_Replace(enode * e) { context & ctx = get_context(); @@ -1636,13 +1555,17 @@ namespace smt { // false branch expr_ref elseBranch(ctx.mk_eq_atom(result, expr->get_arg(0)), m); + th_rewriter rw(m); + expr_ref breakdownAssert(m.mk_ite(condAst, m.mk_and(thenItems.size(), thenItems.c_ptr()), elseBranch), m); - assert_axiom(breakdownAssert); - - SASSERT(breakdownAssert); + expr_ref breakdownAssert_rw(breakdownAssert, m); + rw(breakdownAssert_rw); + assert_axiom(breakdownAssert_rw); expr_ref reduceToResult(ctx.mk_eq_atom(expr, result), m); - assert_axiom(reduceToResult); + expr_ref reduceToResult_rw(reduceToResult, m); + rw(reduceToResult_rw); + assert_axiom(reduceToResult_rw); } void theory_str::instantiate_axiom_str_to_int(enode * e) { @@ -4752,12 +4675,10 @@ namespace smt { bool theory_str::get_arith_value(expr* e, rational& val) const { context& ctx = get_context(); ast_manager & m = get_manager(); - - // safety - if (!ctx.e_internalized(e)) { + // safety + if (!ctx.e_internalized(e)) { return false; - } - + } // if an integer constant exists in the eqc, it should be the root enode * en_e = ctx.get_enode(e); enode * root_e = en_e->get_root(); @@ -10509,6 +10430,9 @@ namespace smt { // iterate parents if (standAlone) { // I hope this works! + if (!ctx.e_internalized(freeVar)) { + ctx.internalize(freeVar, false); + } enode * e_freeVar = ctx.get_enode(freeVar); enode_vector::iterator it = e_freeVar->begin_parents(); for (; it != e_freeVar->end_parents(); ++it) { diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt index 56864a691..1ffdc35e1 100644 --- a/src/solver/CMakeLists.txt +++ b/src/solver/CMakeLists.txt @@ -6,6 +6,7 @@ z3_add_component(solver smt_logics.cpp solver.cpp solver_na2as.cpp + solver_pool.cpp solver2tactic.cpp tactic2solver.cpp COMPONENT_DEPENDENCIES diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 8f37224ad..81e10e443 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -147,6 +147,7 @@ public: } virtual void updt_params(params_ref const & p) { + solver::updt_params(p); m_solver1->updt_params(p); m_solver2->updt_params(p); updt_local_params(p); @@ -280,8 +281,8 @@ public: return m_solver2->get_assumption(idx - c1); } - virtual std::ostream& display(std::ostream & out) const { - return m_solver1->display(out); + virtual std::ostream& display(std::ostream & out, unsigned n, expr* const* es) const { + return m_solver1->display(out, n, es); } virtual void collect_statistics(statistics & st) const { diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index cb7864268..bf53cb669 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -34,11 +34,12 @@ expr * solver::get_assertion(unsigned idx) const { return 0; } -std::ostream& solver::display(std::ostream & out) const { +std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assumptions) const { expr_ref_vector fmls(get_manager()); get_assertions(fmls); ast_pp_util visitor(get_manager()); visitor.collect(fmls); + visitor.collect(n, assumptions); visitor.display_decls(out); visitor.display_asserts(out, fmls, true); return out; diff --git a/src/solver/solver.h b/src/solver/solver.h index 00e3cf8e9..0a406455b 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -43,6 +43,7 @@ public: - results based on check_sat_result API */ class solver : public check_sat_result { + params_ref m_params; public: virtual ~solver() {} @@ -54,7 +55,12 @@ public: /** \brief Update the solver internal settings. */ - virtual void updt_params(params_ref const & p) { } + virtual void updt_params(params_ref const & p) { m_params.copy(p); } + + /** + \brief Retrieve set of parameters set on solver. + */ + virtual params_ref const& get_params() { return m_params; } /** \brief Store in \c r a description of the configuration @@ -175,7 +181,7 @@ public: /** \brief Display the content of this solver. */ - virtual std::ostream& display(std::ostream & out) const; + virtual std::ostream& display(std::ostream & out, unsigned n = 0, expr* const* assumptions = nullptr) const; class scoped_push { solver& s; diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp new file mode 100644 index 000000000..c6c85ec29 --- /dev/null +++ b/src/solver/solver_pool.cpp @@ -0,0 +1,320 @@ +/** +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + solver_pool.cpp + +Abstract: + + Maintain a pool of solvers + +Author: + + Nikolaj Bjorner + +Notes: + +--*/ + +#include "solver/solver_pool.h" +#include "solver/solver_na2as.h" +#include "ast/proofs/proof_utils.h" +#include "ast/ast_util.h" + +class pool_solver : public solver_na2as { + solver_pool& m_pool; + app_ref m_pred; + proof_ref m_proof; + ref m_base; + expr_ref_vector m_assertions; + unsigned m_head; + expr_ref_vector m_flat; + bool m_pushed; + bool m_in_delayed_scope; + unsigned m_dump_counter; + + bool is_virtual() const { return !m.is_true(m_pred); } +public: + pool_solver(solver* b, solver_pool& pool, app_ref& pred): + solver_na2as(pred.get_manager()), + m_pool(pool), + m_pred(pred), + m_proof(m), + m_base(b), + m_assertions(m), + m_head(0), + m_flat(m), + m_pushed(false), + m_in_delayed_scope(false), + m_dump_counter(0) { + if (is_virtual()) { + solver_na2as::assert_expr(m.mk_true(), pred); + } + } + + virtual ~pool_solver() { + if (m_pushed) pop(get_scope_level()); + if (is_virtual()) { + m_pred = m.mk_not(m_pred); + m_base->assert_expr(m_pred); + } + } + + solver* base_solver() { return m_base.get(); } + + virtual solver* translate(ast_manager& m, params_ref const& p) { UNREACHABLE(); return nullptr; } + virtual void updt_params(params_ref const& p) { solver::updt_params(p); m_base->updt_params(p); } + virtual void collect_param_descrs(param_descrs & r) { m_base->collect_param_descrs(r); } + virtual void collect_statistics(statistics & st) const { m_base->collect_statistics(st); } + + virtual void get_unsat_core(ptr_vector & r) { + m_base->get_unsat_core(r); + unsigned j = 0; + for (unsigned i = 0; i < r.size(); ++i) + if (m_pred != r[i]) + r[j++] = r[i]; + r.shrink(j); + } + + virtual unsigned get_num_assumptions() const { + unsigned sz = solver_na2as::get_num_assumptions(); + return is_virtual() ? sz - 1 : sz; + } + + virtual proof * get_proof() { + scoped_watch _t_(m_pool.m_proof_watch); + if (!m_proof.get()) { + elim_aux_assertions pc(m_pred); + m_proof = m_base->get_proof(); + pc(m, m_proof, m_proof); + } + return m_proof; + } + + void internalize_assertions() { + SASSERT(!m_pushed || m_head == m_assertions.size()); + for (unsigned sz = m_assertions.size(); m_head < sz; ++m_head) { + expr_ref f(m); + f = m.mk_implies(m_pred, (m_assertions.get(m_head))); + m_base->assert_expr(f); + } + } + + virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) { + SASSERT(!m_pushed || get_scope_level() > 0); + m_proof.reset(); + scoped_watch _t_(m_pool.m_check_watch); + m_pool.m_stats.m_num_checks++; + + stopwatch sw; + sw.start(); + internalize_assertions(); + lbool res = m_base->check_sat(num_assumptions, assumptions); + sw.stop(); + switch (res) { + case l_true: + m_pool.m_check_sat_watch.add(sw); + m_pool.m_stats.m_num_sat_checks++; + break; + case l_undef: + m_pool.m_check_undef_watch.add(sw); + m_pool.m_stats.m_num_undef_checks++; + break; + default: + break; + } + set_status(res); + + if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) { + std::stringstream file_name; + file_name << "virt_solver"; + if (is_virtual()) { file_name << "_" << m_pred->get_decl()->get_name(); } + file_name << "_" << (m_dump_counter++) << ".smt2"; + + std::ofstream out(file_name.str().c_str()); + if (!out) { verbose_stream() << "could not open file " << file_name.str() << " for output\n"; } + + out << "(set-info :status "; + switch (res) { + case l_true: out << "sat"; break; + case l_false: out << "unsat"; break; + case l_undef: out << "unknown"; break; + } + out << ")\n"; + m_base->display(out, num_assumptions, assumptions); + bool first = true; + out << "(check-sat"; + for (unsigned i = 0; i < num_assumptions; ++i) { + out << " " << mk_pp(assumptions[i], m); + } + out << ")"; + out << "(exit)\n"; + ::statistics st; + m_base->collect_statistics(st); + st.update("time", sw.get_seconds()); + st.display_smt2(out); + out.close(); + } + return res; + } + + virtual void push_core() { + SASSERT(!m_pushed || get_scope_level() > 0); + if (m_in_delayed_scope) { + // second push + internalize_assertions(); + m_base->push(); + m_pushed = true; + m_in_delayed_scope = false; + } + + if (!m_pushed) { + m_in_delayed_scope = true; + } + else { + SASSERT(m_pushed); + SASSERT(!m_in_delayed_scope); + m_base->push(); + } + } + + virtual void pop_core(unsigned n) { + SASSERT(!m_pushed || get_scope_level() > 0); + if (m_pushed) { + SASSERT(!m_in_delayed_scope); + m_base->pop(n); + m_pushed = get_scope_level() - n > 0; + } + else { + m_in_delayed_scope = get_scope_level() - n > 0; + } + } + + virtual void assert_expr(expr * e) { + SASSERT(!m_pushed || get_scope_level() > 0); + if (m.is_true(e)) return; + if (m_in_delayed_scope) { + internalize_assertions(); + m_base->push(); + m_pushed = true; + m_in_delayed_scope = false; + } + + if (m_pushed) { + m_base->assert_expr(e); + } + else { + m_flat.push_back(e); + flatten_and(m_flat); + m_assertions.append(m_flat); + m_flat.reset(); + } + } + + virtual void get_model(model_ref & _m) { m_base->get_model(_m); } + + virtual expr * get_assumption(unsigned idx) const { + return solver_na2as::get_assumption(idx + is_virtual()); + } + + virtual std::string reason_unknown() const { return m_base->reason_unknown(); } + virtual void set_reason_unknown(char const* msg) { return m_base->set_reason_unknown(msg); } + virtual void get_labels(svector & r) { return m_base->get_labels(r); } + virtual void set_progress_callback(progress_callback * callback) { m_base->set_progress_callback(callback); } + + virtual ast_manager& get_manager() const { return m_base->get_manager(); } + + void refresh(solver* new_base) { + SASSERT(!m_pushed); + m_head = 0; + m_base = new_base; + } + + void reset() { + SASSERT(!m_pushed); + m_head = 0; + m_assertions.reset(); + m_pool.refresh(m_base.get()); + } +}; + +solver_pool::solver_pool(solver* base_solver, unsigned num_solvers_per_pool): + m_base_solver(base_solver), + m_num_solvers_per_pool(num_solvers_per_pool), + m_num_solvers_in_last_pool(0) +{} + + +ptr_vector solver_pool::get_base_solvers() const { + ptr_vector solvers; + for (solver* s0 : m_solvers) { + pool_solver* s = dynamic_cast(s0); + if (!solvers.contains(s->base_solver())) { + solvers.push_back(s->base_solver()); + } + } + return solvers; +} + +void solver_pool::collect_statistics(statistics &st) const { + ptr_vector solvers = get_base_solvers(); + for (solver* s : solvers) s->collect_statistics(st); + st.update("time.pool_solver.smt.total", m_check_watch.get_seconds()); + st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds()); + st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds()); + st.update("time.pool_solver.proof", m_proof_watch.get_seconds()); + st.update("pool_solver.checks", m_stats.m_num_checks); + st.update("pool_solver.checks.sat", m_stats.m_num_sat_checks); + st.update("pool_solver.checks.undef", m_stats.m_num_undef_checks); +} + +void solver_pool::reset_statistics() { +#if 0 + ptr_vector solvers = get_base_solvers(); + for (solver* s : solvers) { + s->reset_statistics(); + } +#endif + m_stats.reset(); + m_check_sat_watch.reset(); + m_check_undef_watch.reset(); + m_check_watch.reset(); + m_proof_watch.reset(); +} + +solver* solver_pool::mk_solver() { + ref base_solver; + ast_manager& m = m_base_solver->get_manager(); + if (m_solvers.empty() || m_num_solvers_in_last_pool == m_num_solvers_per_pool) { + base_solver = m_base_solver->translate(m, m_base_solver->get_params()); + m_num_solvers_in_last_pool = 0; + } + else { + base_solver = dynamic_cast(m_solvers.back())->base_solver(); + } + m_num_solvers_in_last_pool++; + std::stringstream name; + name << "vsolver#" << m_solvers.size(); + app_ref pred(m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()), m); + pool_solver* solver = alloc(pool_solver, base_solver.get(), *this, pred); + m_solvers.push_back(solver); + return solver; +} + +void solver_pool::reset_solver(solver* s) { + pool_solver* ps = dynamic_cast(s); + SASSERT(ps); + if (ps) ps->reset(); +} + +void solver_pool::refresh(solver* base_solver) { + ast_manager& m = m_base_solver->get_manager(); + ref new_base = m_base_solver->translate(m, m_base_solver->get_params()); + for (solver* s0 : m_solvers) { + pool_solver* s = dynamic_cast(s0); + if (base_solver == s->base_solver()) { + s->refresh(new_base.get()); + } + } +} diff --git a/src/solver/solver_pool.h b/src/solver/solver_pool.h new file mode 100644 index 000000000..d676ca54d --- /dev/null +++ b/src/solver/solver_pool.h @@ -0,0 +1,69 @@ +/** +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + solver_pool.h + +Abstract: + + Maintain a pool of solvers + +Author: + + Nikolaj Bjorner + Arie Gurfinkel + +Notes: + + This is a revision of spacer_virtual_solver by Arie Gurfinkel + +--*/ +#ifndef SOLVER_POOL_H_ +#define SOLVER_POOL_H_ + +#include "solver/solver.h" +#include "util/stopwatch.h" + +class pool_solver; + +class solver_pool { + + friend class pool_solver; + + struct stats { + unsigned m_num_checks; + unsigned m_num_sat_checks; + unsigned m_num_undef_checks; + stats() { reset(); } + void reset() { memset(this, 0, sizeof(*this)); } + }; + + ref m_base_solver; + unsigned m_num_solvers_per_pool; + unsigned m_num_solvers_in_last_pool; + sref_vector m_solvers; + stats m_stats; + + stopwatch m_check_watch; + stopwatch m_check_sat_watch; + stopwatch m_check_undef_watch; + stopwatch m_proof_watch; + + void refresh(solver* s); + + ptr_vector get_base_solvers() const; + +public: + solver_pool(solver* base_solver, unsigned num_solvers_per_pool); + + void collect_statistics(statistics &st) const; + void reset_statistics(); + + solver* mk_solver(); + + void reset_solver(solver* s); +}; + + +#endif diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index d7e7fbb6e..a24f1d4c7 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -37,7 +37,6 @@ class tactic2solver : public solver_na2as { ref m_result; tactic_ref m_tactic; symbol m_logic; - params_ref m_params; bool m_produce_models; bool m_produce_proofs; bool m_produce_unsat_cores; @@ -85,7 +84,7 @@ tactic2solver::tactic2solver(ast_manager & m, tactic * t, params_ref const & p, m_tactic = t; m_logic = logic; - m_params = p; + solver::updt_params(p); m_produce_models = produce_models; m_produce_proofs = produce_proofs; @@ -96,7 +95,7 @@ tactic2solver::~tactic2solver() { } void tactic2solver::updt_params(params_ref const & p) { - m_params.append(p); + solver::updt_params(p); } void tactic2solver::collect_param_descrs(param_descrs & r) { @@ -129,7 +128,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass m_result = alloc(simple_check_sat_result, m); m_tactic->cleanup(); m_tactic->set_logic(m_logic); - m_tactic->updt_params(m_params); // parameters are allowed to overwrite logic. + m_tactic->updt_params(get_params()); // parameters are allowed to overwrite logic. goal_ref g = alloc(goal, m, m_produce_proofs, m_produce_models, m_produce_unsat_cores); unsigned sz = m_assertions.size(); diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index 9401f74c1..ec4c21fe8 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -399,8 +399,8 @@ void bv_size_reduction_tactic::operator()(goal_ref const & g, void bv_size_reduction_tactic::cleanup() { - imp * d = alloc(imp, m_imp->m); - std::swap(d, m_imp); - dealloc(d); + ast_manager & m = m_imp->m; + m_imp->~imp(); + new (m_imp) imp(m); } diff --git a/src/tactic/bv/max_bv_sharing_tactic.cpp b/src/tactic/bv/max_bv_sharing_tactic.cpp index b0affeb4b..becaed276 100644 --- a/src/tactic/bv/max_bv_sharing_tactic.cpp +++ b/src/tactic/bv/max_bv_sharing_tactic.cpp @@ -307,9 +307,10 @@ public: } virtual void cleanup() { - imp * d = alloc(imp, m_imp->m(), m_params); - std::swap(d, m_imp); - dealloc(d); + ast_manager & m = m_imp->m(); + params_ref p = std::move(m_params); + m_imp->~imp(); + new (m_imp) imp(m, p); } }; diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 7baac0b99..607ecbd79 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -255,8 +255,9 @@ public: virtual void cleanup() { ast_manager & m = m_imp->m; - dealloc(m_imp); - m_imp = alloc(imp, m, m_params); + params_ref p = std::move(m_params); + m_imp->~imp(); + new (m_imp) imp(m, p); } }; diff --git a/src/tactic/core/simplify_tactic.cpp b/src/tactic/core/simplify_tactic.cpp index 9deff968e..de1fcc99c 100644 --- a/src/tactic/core/simplify_tactic.cpp +++ b/src/tactic/core/simplify_tactic.cpp @@ -111,9 +111,9 @@ void simplify_tactic::operator()(goal_ref const & in, void simplify_tactic::cleanup() { ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + params_ref p = std::move(m_params); + m_imp->~imp(); + new (m_imp) imp(m, p); } unsigned simplify_tactic::get_num_steps() const { diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 2f66d7a53..58078e106 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -33,7 +33,6 @@ Notes: class bounded_int2bv_solver : public solver_na2as { ast_manager& m; - params_ref m_params; mutable bv_util m_bv; mutable arith_util m_arith; mutable expr_ref_vector m_assertions; @@ -53,7 +52,6 @@ public: bounded_int2bv_solver(ast_manager& m, params_ref const& p, solver* s): solver_na2as(m), m(m), - m_params(p), m_bv(m), m_arith(m), m_assertions(m), @@ -63,6 +61,7 @@ public: m_rewriter_ctx(m, p), m_rewriter(m, m_rewriter_ctx) { + solver::updt_params(p); m_bounds.push_back(alloc(bound_manager, m)); } @@ -131,7 +130,7 @@ public: return m_solver->check_sat(num_assumptions, assumptions); } - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 5880302d9..dd0ee7c4b 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -33,7 +33,6 @@ Notes: class enum2bv_solver : public solver_na2as { ast_manager& m; - params_ref m_params; ref m_solver; enum2bv_rewriter m_rewriter; @@ -42,10 +41,10 @@ public: enum2bv_solver(ast_manager& m, params_ref const& p, solver* s): solver_na2as(m), m(m), - m_params(p), m_solver(s), m_rewriter(m, p) { + solver::updt_params(p); } virtual ~enum2bv_solver() {} @@ -78,7 +77,7 @@ public: return m_solver->check_sat(num_assumptions, assumptions); } - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp index 81cc43685..a06ff77c0 100644 --- a/src/tactic/portfolio/pb2bv_solver.cpp +++ b/src/tactic/portfolio/pb2bv_solver.cpp @@ -26,7 +26,6 @@ Notes: class pb2bv_solver : public solver_na2as { ast_manager& m; - params_ref m_params; mutable expr_ref_vector m_assertions; mutable ref m_solver; mutable pb2bv_rewriter m_rewriter; @@ -36,11 +35,11 @@ public: pb2bv_solver(ast_manager& m, params_ref const& p, solver* s): solver_na2as(m), m(m), - m_params(p), m_assertions(m), m_solver(s), m_rewriter(m, p) { + solver::updt_params(p); } virtual ~pb2bv_solver() {} @@ -70,7 +69,7 @@ public: return m_solver->check_sat(num_assumptions, assumptions); } - virtual void updt_params(params_ref const & p) { m_solver->updt_params(p); } + virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); } virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index e89da3631..df2791a8f 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -70,8 +70,8 @@ public: const unsigned sz = g->size(); for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i)); scoped_ptr uffree_solver = setup_sat(); - scoped_ptr imp = alloc(lackr, m, m_p, m_st, flas, uffree_solver.get()); - const lbool o = imp->operator()(); + lackr imp(m, m_p, m_st, flas, uffree_solver.get()); + const lbool o = imp.operator()(); flas.reset(); // report result goal_ref resg(alloc(goal, *g, true)); @@ -79,8 +79,8 @@ public: if (o != l_undef) result.push_back(resg.get()); // report model if (g->models_enabled() && (o == l_true)) { - model_ref abstr_model = imp->get_model(); - mc = mk_qfufbv_ackr_model_converter(m, imp->get_info(), abstr_model); + model_ref abstr_model = imp.get_model(); + mc = mk_qfufbv_ackr_model_converter(m, imp.get_info(), abstr_model); } } diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index 7f2ed3245..9ba707af0 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -185,4 +185,15 @@ public: #endif +struct scoped_watch { + stopwatch &m_sw; + scoped_watch (stopwatch &sw, bool reset=false): m_sw(sw) { + if (reset) m_sw.reset(); + m_sw.start(); + } + ~scoped_watch() { + m_sw.stop (); + } +}; + #endif