diff --git a/src/solver/combined_solver.cpp b/src/solver/combined_solver.cpp index 858885d9d..e19d7a1e3 100644 --- a/src/solver/combined_solver.cpp +++ b/src/solver/combined_solver.cpp @@ -194,7 +194,7 @@ public: m_use_solver1_results = false; if (get_num_assumptions() != 0 || - num_assumptions > 0 || // assumptions were provided + num_assumptions > 0 || // assumptions were provided m_ignore_solver1) { // must use incremental solver switch_inc_mode(); diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 01c45ee44..704038ffd 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -23,12 +23,11 @@ Notes: #include"ast_smt2_pp.h" solver_na2as::solver_na2as(ast_manager & m): - m_manager(m) { + m(m), + m_assumptions(m) { } -solver_na2as::~solver_na2as() { - restore_assumptions(0); -} +solver_na2as::~solver_na2as() {} void solver_na2as::assert_expr(expr * t, expr * a) { if (a == 0) { @@ -36,20 +35,19 @@ void solver_na2as::assert_expr(expr * t, expr * a) { } else { SASSERT(is_uninterp_const(a)); - SASSERT(m_manager.is_bool(a)); - TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, m_manager) << "\n" << mk_ismt2_pp(a, m_manager) << "\n";); - m_manager.inc_ref(a); + SASSERT(m.is_bool(a)); + TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, m) << "\n" << mk_ismt2_pp(a, m) << "\n";); m_assumptions.push_back(a); - expr_ref new_t(m_manager); - new_t = m_manager.mk_implies(a, t); + expr_ref new_t(m); + new_t = m.mk_implies(a, t); assert_expr(new_t); } } struct append_assumptions { - ptr_vector & m_assumptions; + expr_ref_vector & m_assumptions; unsigned m_old_sz; - append_assumptions(ptr_vector & _m_assumptions, + append_assumptions(expr_ref_vector & _m_assumptions, unsigned num_assumptions, expr * const * assumptions): m_assumptions(_m_assumptions) { @@ -82,10 +80,6 @@ void solver_na2as::pop(unsigned n) { } void solver_na2as::restore_assumptions(unsigned old_sz) { - // SASSERT(old_sz == 0); - for (unsigned i = old_sz; i < m_assumptions.size(); i++) { - m_manager.dec_ref(m_assumptions[i]); - } m_assumptions.shrink(old_sz); } diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 644d217ee..019468fd7 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -25,8 +25,8 @@ Notes: #include"solver.h" class solver_na2as : public solver { - ast_manager & m_manager; - ptr_vector m_assumptions; + ast_manager & m; + expr_ref_vector m_assumptions; unsigned_vector m_scopes; void restore_assumptions(unsigned old_sz); public: diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index d266548d5..90beabf24 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -26,7 +26,7 @@ Revision History: class propagate_values_tactic : public tactic { struct imp { - ast_manager & m_manager; + ast_manager & m; th_rewriter m_r; scoped_ptr m_subst; goal * m_goal; @@ -36,13 +36,15 @@ class propagate_values_tactic : public tactic { bool m_modified; imp(ast_manager & m, params_ref const & p): - m_manager(m), + m(m), m_r(m, p), m_goal(0), m_occs(m, true /* track atoms */) { updt_params_core(p); } + ~imp() { } + void updt_params_core(params_ref const & p) { m_max_rounds = p.get_uint("max_rounds", 4); } @@ -51,32 +53,28 @@ class propagate_values_tactic : public tactic { m_r.updt_params(p); updt_params_core(p); } - - ast_manager & m() const { return m_manager; } bool is_shared(expr * t) { return m_occs.is_shared(t); } - bool is_shared_neg(expr * t, expr * & atom) { - if (!m().is_not(t)) + bool is_shared_neg(expr * t, expr * & atom) { + if (!m.is_not(t, atom)) return false; - atom = to_app(t)->get_arg(0); return is_shared(atom); } bool is_shared_eq(expr * t, expr * & lhs, expr * & value) { - if (!m().is_eq(t)) + expr* arg1, *arg2; + if (!m.is_eq(t, arg1, arg2)) return false; - expr * arg1 = to_app(t)->get_arg(0); - expr * arg2 = to_app(t)->get_arg(1); - if (m().is_value(arg1) && is_shared(arg2)) { + if (m.is_value(arg1) && is_shared(arg2)) { lhs = arg2; value = arg1; return true; } - if (m().is_value(arg2) && is_shared(arg1)) { + if (m.is_value(arg2) && is_shared(arg1)) { lhs = arg1; value = arg2; return true; @@ -87,15 +85,15 @@ class propagate_values_tactic : public tactic { void push_result(expr * new_curr, proof * new_pr) { if (m_goal->proofs_enabled()) { proof * pr = m_goal->pr(m_idx); - new_pr = m().mk_modus_ponens(pr, new_pr); + new_pr = m.mk_modus_ponens(pr, new_pr); } - expr_dependency_ref new_d(m()); + expr_dependency_ref new_d(m); if (m_goal->unsat_core_enabled()) { new_d = m_goal->dep(m_idx); expr_dependency * used_d = m_r.get_used_dependencies(); if (used_d != 0) { - new_d = m().mk_join(new_d, used_d); + new_d = m.mk_join(new_d, used_d); m_r.reset_used_dependencies(); } } @@ -103,34 +101,34 @@ class propagate_values_tactic : public tactic { m_goal->update(m_idx, new_curr, new_pr, new_d); if (is_shared(new_curr)) { - m_subst->insert(new_curr, m().mk_true(), m().mk_iff_true(new_pr), new_d); + m_subst->insert(new_curr, m.mk_true(), m.mk_iff_true(new_pr), new_d); } expr * atom; if (is_shared_neg(new_curr, atom)) { - m_subst->insert(atom, m().mk_false(), m().mk_iff_false(new_pr), new_d); + m_subst->insert(atom, m.mk_false(), m.mk_iff_false(new_pr), new_d); } expr * lhs, * value; if (is_shared_eq(new_curr, lhs, value)) { - TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m()) << "\n";); + TRACE("shallow_context_simplifier_bug", tout << "found eq:\n" << mk_ismt2_pp(new_curr, m) << "\n";); m_subst->insert(lhs, value, new_pr, new_d); } } void process_current() { expr * curr = m_goal->form(m_idx); - expr_ref new_curr(m()); - proof_ref new_pr(m()); + expr_ref new_curr(m); + proof_ref new_pr(m); if (!m_subst->empty()) { m_r(curr, new_curr, new_pr); } else { new_curr = curr; - if (m().proofs_enabled()) - new_pr = m().mk_reflexivity(curr); + if (m.proofs_enabled()) + new_pr = m.mk_reflexivity(curr); } - TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m()) << "\n---->\n" << mk_ismt2_pp(new_curr, m()) << "\n";); + TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";); push_result(new_curr, new_pr); if (new_curr != curr) @@ -148,25 +146,26 @@ class propagate_values_tactic : public tactic { m_goal = g.get(); bool forward = true; - expr_ref new_curr(m()); - proof_ref new_pr(m()); + expr_ref new_curr(m); + proof_ref new_pr(m); unsigned size = m_goal->size(); m_idx = 0; m_modified = false; unsigned round = 0; + if (m_goal->inconsistent()) goto end; if (m_max_rounds == 0) goto end; - m_subst = alloc(expr_substitution, m(), g->unsat_core_enabled(), g->proofs_enabled()); + m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled()); m_r.set_substitution(m_subst.get()); m_occs(*m_goal); while (true) { - TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display(tout);); + TRACE("propagate_values", tout << "while(true) loop\n"; m_goal->display_with_dependencies(tout);); if (forward) { for (; m_idx < size; m_idx++) { process_current(); @@ -255,15 +254,14 @@ public: } virtual void cleanup() { - ast_manager & m = m_imp->m(); - imp * d = alloc(imp, m, m_params); - std::swap(d, m_imp); - dealloc(d); + ast_manager & m = m_imp->m; + dealloc(m_imp); + m_imp = alloc(imp, m, m_params); } }; tactic * mk_propagate_values_tactic(ast_manager & m, params_ref const & p) { - return clean(alloc(propagate_values_tactic, m, p)); + return alloc(propagate_values_tactic, m, p); } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index d79bd2ed1..0d276ba72 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -131,19 +131,19 @@ public: SASSERT(r1_size > 0); if (r1_size == 1) { if (r1[0]->is_decided()) { - result.push_back(r1[0]); - if (models_enabled) mc = mc1; + result.push_back(r1[0]); + if (models_enabled) mc = mc1; SASSERT(!pc); SASSERT(!core); return; } - goal_ref r1_0 = r1[0]; - m_t2->operator()(r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); - if (proofs_enabled) pc = concat(pc1.get(), pc.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); - } - else { - if (cores_enabled) core = core1; + goal_ref r1_0 = r1[0]; + m_t2->operator()(r1_0, result, mc, pc, core); + if (models_enabled) mc = concat(mc1.get(), mc.get()); + if (proofs_enabled) pc = concat(pc1.get(), pc.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); + } + else { + if (cores_enabled) core = core1; proof_converter_ref_buffer pc_buffer; model_converter_ref_buffer mc_buffer; sbuffer sz_buffer; @@ -179,16 +179,16 @@ public: SASSERT(!core2); if (models_enabled) mc_buffer.push_back(0); if (proofs_enabled) pc_buffer.push_back(proof2proof_converter(m, r2[0]->pr(0))); - if (models_enabled || proofs_enabled) sz_buffer.push_back(0); + if (models_enabled || proofs_enabled) sz_buffer.push_back(0); if (cores_enabled) core = m.mk_join(core.get(), r2[0]->dep(0)); } } else { - result.append(r2.size(), r2.c_ptr()); - if (models_enabled) mc_buffer.push_back(mc2.get()); - if (proofs_enabled) pc_buffer.push_back(pc2.get()); - if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); - if (cores_enabled) core = m.mk_join(core.get(), core2.get()); + result.append(r2.size(), r2.c_ptr()); + if (models_enabled) mc_buffer.push_back(mc2.get()); + if (proofs_enabled) pc_buffer.push_back(pc2.get()); + if (models_enabled || proofs_enabled) sz_buffer.push_back(r2.size()); + if (cores_enabled) core = m.mk_join(core.get(), core2.get()); } } @@ -651,12 +651,12 @@ public: } goal_ref r1_0 = r1[0]; m_t2->operator()(r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc1.get(), mc.get()); - if (proofs_enabled) pc = concat(pc1.get(), pc.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); + if (models_enabled) mc = concat(mc1.get(), mc.get()); + if (proofs_enabled) pc = concat(pc1.get(), pc.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); } else { - if (cores_enabled) core = core1; + if (cores_enabled) core = core1; scoped_ptr_vector managers; tactic_ref_vector ts2; @@ -670,8 +670,8 @@ public: ts2.push_back(m_t2->translate(*new_m)); } - proof_converter_ref_buffer pc_buffer; - model_converter_ref_buffer mc_buffer; + proof_converter_ref_buffer pc_buffer; + model_converter_ref_buffer mc_buffer; scoped_ptr_vector core_buffer; scoped_ptr_vector goals_vect; @@ -687,7 +687,7 @@ public: std::string ex_msg; #pragma omp parallel for - for (int i = 0; i < static_cast(r1_size); i++) { + for (int i = 0; i < static_cast(r1_size); i++) { ast_manager & new_m = *(managers[i]); goal_ref new_g = g_copies[i]; @@ -772,7 +772,7 @@ public: md = alloc(model, m); apply(mc2, md, 0); apply(mc1, md, i); - mc = model2model_converter(md.get()); + mc = model2model_converter(md.get()); } SASSERT(!pc); SASSERT(!core); } @@ -969,9 +969,9 @@ class repeat_tactical : public unary_tactical { m_t->operator()(in, r1, mc1, pc1, core1); if (is_equal(orig_in, *(in.get()))) { result.push_back(r1[0]); - if (models_enabled) mc = mc1; - if (proofs_enabled) pc = pc1; - if (cores_enabled) core = core1; + if (models_enabled) mc = mc1; + if (proofs_enabled) pc = pc1; + if (cores_enabled) core = core1; return; } } @@ -980,18 +980,18 @@ class repeat_tactical : public unary_tactical { if (r1_size == 1) { if (r1[0]->is_decided()) { result.push_back(r1[0]); - if (models_enabled) mc = mc1; + if (models_enabled) mc = mc1; SASSERT(!pc); SASSERT(!core); return; } goal_ref r1_0 = r1[0]; - operator()(depth+1, r1_0, result, mc, pc, core); - if (models_enabled) mc = concat(mc.get(), mc1.get()); - if (proofs_enabled) pc = concat(pc.get(), pc1.get()); - if (cores_enabled) core = m.mk_join(core1.get(), core); + operator()(depth+1, r1_0, result, mc, pc, core); + if (models_enabled) mc = concat(mc.get(), mc1.get()); + if (proofs_enabled) pc = concat(pc.get(), pc1.get()); + if (cores_enabled) core = m.mk_join(core1.get(), core); } - else { - if (cores_enabled) core = core1; + else { + if (cores_enabled) core = core1; proof_converter_ref_buffer pc_buffer; model_converter_ref_buffer mc_buffer; sbuffer sz_buffer;