diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 0a5be7893..b27bd724e 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -636,8 +636,8 @@ void lemma::mk_insts(expr_ref_vector &out, expr* e) pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): pm(pm), m(pm.get_manager()), ctx(ctx), m_head(head, m), - m_sig(m), m_solver(pm, ctx.get_params(), head->get_name()), - m_reach_solver (pm.mk_solver2()), + m_sig(m), + m_reach_solver (ctx.mk_solver2()), m_pobs(*this), m_frames(*this), m_reach_facts(), m_rf_init_sz(0), @@ -645,6 +645,8 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): m_all_init(false), m_reach_case_vars(m) { + m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(), + ctx.get_params(), head->get_name()); init_sig (); app_ref v(m); std::stringstream name; @@ -670,7 +672,7 @@ std::ostream& pred_transformer::display(std::ostream& out) const void pred_transformer::collect_statistics(statistics& st) const { - m_solver.collect_statistics(st); + m_solver->collect_statistics(st); // -- number of times a lemma has been propagated to a higher level // -- during push @@ -700,7 +702,7 @@ void pred_transformer::collect_statistics(statistics& st) const void pred_transformer::reset_statistics() { - m_solver.reset_statistics(); + m_solver->reset_statistics(); //m_reachable.reset_statistics(); m_stats.reset(); m_initialize_watch.reset (); @@ -727,7 +729,7 @@ void pred_transformer::ensure_level(unsigned level) while (m_frames.size() <= level) { m_frames.add_frame (); - m_solver.add_level (); + m_solver->add_level (); } } @@ -913,10 +915,10 @@ void pred_transformer::add_lemma_core(lemma* lemma, bool ground_only) if (is_infty_level(lvl)) { m_stats.m_num_invariants++; } if (lemma->is_ground()) { - if (is_infty_level(lvl)) { m_solver.assert_expr(l); } + if (is_infty_level(lvl)) { m_solver->assert_expr(l); } else { ensure_level (lvl); - m_solver.assert_expr (l, lvl); + m_solver->assert_expr (l, lvl); } } @@ -963,10 +965,10 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child, TRACE("spacer_detail", tout << "child property: " << mk_pp(inst.get (j), m) << "\n";); if (is_infty_level(lvl)) { - m_solver.assert_expr(inst.get(j)); + m_solver->assert_expr(inst.get(j)); } else { - m_solver.assert_expr(inst.get(j), lvl); + m_solver->assert_expr(inst.get(j), lvl); } } } @@ -1195,18 +1197,18 @@ void pred_transformer::propagate_to_infinity (unsigned level) bool pred_transformer::is_blocked (pob &n, unsigned &uses_level) { ensure_level (n.level ()); - prop_solver::scoped_level _sl (m_solver, n.level ()); - m_solver.set_core (nullptr); - m_solver.set_model (nullptr); + prop_solver::scoped_level _sl (*m_solver, n.level ()); + m_solver->set_core (nullptr); + m_solver->set_model (nullptr); expr_ref_vector post(m), _aux(m); post.push_back (n.post ()); // this only uses the lemmas at the current level // transition relation is irrelevant // XXX quic3: not all lemmas are asserted at the post-condition - lbool res = m_solver.check_assumptions (post, _aux, _aux, + lbool res = m_solver->check_assumptions (post, _aux, _aux, 0, nullptr, 0); - if (res == l_false) { uses_level = m_solver.uses_level(); } + if (res == l_false) { uses_level = m_solver->uses_level(); } return res == l_false; } @@ -1282,12 +1284,12 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, ensure_level(n.level()); // prepare the solver - prop_solver::scoped_level _sl(m_solver, n.level()); - prop_solver::scoped_subset_core _sc (m_solver, !n.use_farkas_generalizer ()); - prop_solver::scoped_weakness _sw(m_solver, 0, + prop_solver::scoped_level _sl(*m_solver, n.level()); + prop_solver::scoped_subset_core _sc (*m_solver, !n.use_farkas_generalizer ()); + prop_solver::scoped_weakness _sw(*m_solver, 0, ctx.weak_abs() ? n.weakness() : UINT_MAX); - m_solver.set_core(core); - m_solver.set_model(model); + m_solver->set_core(core); + m_solver->set_model(model); expr_ref_vector post (m), reach_assumps (m); post.push_back (n.post ()); @@ -1327,7 +1329,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, // result is either sat (with some reach assumps) or // unsat (even with no reach assumps) expr *bg = m_extend_lit.get (); - lbool is_sat = m_solver.check_assumptions (post, reach_assumps, + lbool is_sat = m_solver->check_assumptions (post, reach_assumps, m_transition_clause, 1, &bg, 0); TRACE ("spacer", @@ -1362,7 +1364,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core, } } ); - uses_level = m_solver.uses_level(); + uses_level = m_solver->uses_level(); return l_false; } UNREACHABLE(); @@ -1426,22 +1428,22 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem, conj.push_back(mk_not(m, lemma_expr)); flatten_and (conj); - prop_solver::scoped_level _sl(m_solver, level); - prop_solver::scoped_subset_core _sc (m_solver, true); - prop_solver::scoped_weakness _sw (m_solver, 1, + prop_solver::scoped_level _sl(*m_solver, level); + prop_solver::scoped_subset_core _sc (*m_solver, true); + prop_solver::scoped_weakness _sw (*m_solver, 1, ctx.weak_abs() ? lem->weakness() : UINT_MAX); model_ref mdl; model_ref *mdl_ref_ptr = nullptr; if (ctx.get_params().spacer_ctp()) {mdl_ref_ptr = &mdl;} - m_solver.set_core(core); - m_solver.set_model(mdl_ref_ptr); + m_solver->set_core(core); + m_solver->set_model(mdl_ref_ptr); expr * bg = m_extend_lit.get (); - lbool r = m_solver.check_assumptions (conj, aux, m_transition_clause, + lbool r = m_solver->check_assumptions (conj, aux, m_transition_clause, 1, &bg, 1); if (r == l_false) { - solver_level = m_solver.uses_level (); + solver_level = m_solver->uses_level (); lem->reset_ctp(); - if (level < m_solver.uses_level()) {m_stats.m_num_lemma_level_jump++;} + if (level < m_solver->uses_level()) {m_stats.m_num_lemma_level_jump++;} SASSERT (level <= solver_level); } else if (r == l_true) { @@ -1461,21 +1463,21 @@ bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state, states = mk_and(state); states = m.mk_not(states); mk_assumptions(head(), states, conj); - prop_solver::scoped_level _sl(m_solver, level); - prop_solver::scoped_subset_core _sc (m_solver, true); - prop_solver::scoped_weakness _sw (m_solver, 1, + prop_solver::scoped_level _sl(*m_solver, level); + prop_solver::scoped_subset_core _sc (*m_solver, true); + prop_solver::scoped_weakness _sw (*m_solver, 1, ctx.weak_abs() ? weakness : UINT_MAX); - m_solver.set_core(&core); - m_solver.set_model (nullptr); + m_solver->set_core(&core); + m_solver->set_model (nullptr); expr_ref_vector aux (m); conj.push_back (m_extend_lit); - lbool res = m_solver.check_assumptions (state, aux, + lbool res = m_solver->check_assumptions (state, aux, m_transition_clause, conj.size (), conj.c_ptr (), 1); if (res == l_false) { state.reset(); state.append(core); - uses_level = m_solver.uses_level(); + uses_level = m_solver->uses_level(); } TRACE ("core_array_eq", tout << "check_inductive: " @@ -1518,8 +1520,8 @@ void pred_transformer::initialize(decl2rel const& pts) rw(m_transition); rw(m_init); - m_solver.assert_expr (m_transition); - m_solver.assert_expr (m_init, 0); + m_solver->assert_expr (m_transition); + m_solver->assert_expr (m_init, 0); TRACE("spacer", tout << "Initial state: " << mk_pp(m_init, m) << "\n"; tout << "Transition: " << mk_pp(m_transition, m) << "\n";); @@ -1790,7 +1792,7 @@ app* pred_transformer::extend_initial (expr *e) // -- extend the initial condition ic = m.mk_or (m_extend_lit, e, v); - m_solver.assert_expr (ic); + m_solver->assert_expr (ic); // -- remember the new extend literal m_extend_lit = m.mk_not (v); @@ -2076,7 +2078,7 @@ context::context(fixedpoint_params const& params, m_params(params), m(m), m_context(nullptr), - m_pm(params.pdr_max_num_contexts(), m), + m_pm(m), m_query_pred(m), m_query(nullptr), m_pob_queue(), @@ -2090,8 +2092,19 @@ context::context(fixedpoint_params const& params, m_weak_abs(params.spacer_weak_abs()), m_use_restarts(params.spacer_restarts()), m_restart_initial_threshold(params.spacer_restart_initial_threshold()), - m_json_marshaller(this) -{} + m_json_marshaller(this) { + ref pool0_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); + ref pool1_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); + ref pool2_base = + mk_smt_solver(m, params_ref::get_empty(), symbol::null); + + unsigned max_num_contexts = params.pdr_max_num_contexts(); + m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts); + m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts); + m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts); +} context::~context() { @@ -2370,9 +2383,9 @@ void context::init_global_smt_params() { // fparams.m_pi_use_database = true; } - m_pm.updt_params0(p); - m_pm.updt_params1(p); - m_pm.updt_params2(p); + m_pool0->updt_params(p); + m_pool1->updt_params(p); + m_pool2->updt_params(p); } void context::init_lemma_generalizers() { @@ -3598,6 +3611,10 @@ bool context::create_children(pob& n, datalog::rule const& r, void context::collect_statistics(statistics& st) const { + m_pool0->collect_statistics(st); + m_pool1->collect_statistics(st); + m_pool2->collect_statistics(st); + decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); for (it = m_rels.begin(); it != end; ++it) { it->m_value->collect_statistics(st); @@ -3639,7 +3656,6 @@ void context::collect_statistics(statistics& st) const st.update("spacer.random_seed", m_params.spacer_random_seed()); st.update("spacer.lemmas_imported", m_stats.m_num_lemmas_imported); st.update("spacer.lemmas_discarded", m_stats.m_num_lemmas_discarded); - m_pm.collect_statistics(st); for (unsigned i = 0; i < m_lemma_generalizers.size(); ++i) { m_lemma_generalizers[i]->collect_statistics(st); @@ -3648,12 +3664,15 @@ void context::collect_statistics(statistics& st) const void context::reset_statistics() { + m_pool0->reset_statistics(); + m_pool1->reset_statistics(); + m_pool2->reset_statistics(); + decl2rel::iterator it = m_rels.begin(), end = m_rels.end(); for (it = m_rels.begin(); it != end; ++it) { it->m_value->reset_statistics(); } m_stats.reset(); - m_pm.reset_statistics(); for (unsigned i = 0; i < m_lemma_generalizers.size(); ++i) { m_lemma_generalizers[i]->reset_statistics(); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 77836a389..55e8cbafe 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -290,7 +290,7 @@ class pred_transformer { func_decl_ref_vector m_sig; // signature ptr_vector m_use; // places where 'this' is referenced. ptr_vector m_rules; // rules used to derive transformer - prop_solver m_solver; // solver context + scoped_ptr m_solver; // solver context ref m_reach_solver; // context for reachability facts pobs m_pobs; // proof obligations created so far frames m_frames; // frames with lemmas @@ -796,6 +796,13 @@ class context { ast_manager& m; datalog::context* m_context; manager m_pm; + + // three solver pools for different queries + scoped_ptr m_pool0; + scoped_ptr m_pool1; + scoped_ptr m_pool2; + + decl2rel m_rels; // Map from relation predicate to fp-operator. func_decl_ref m_query_pred; pred_transformer* m_query; @@ -928,6 +935,13 @@ public: void new_pob_eh(pob *p); bool is_inductive(); + + + // three different solvers with three different sets of parameters + // different solvers are used for different types of queries in spacer + solver* mk_solver0() {return m_pool0->mk_solver();} + solver* mk_solver1() {return m_pool1->mk_solver();} + solver* mk_solver2() {return m_pool2->mk_solver();} }; inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();} diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index d55f74b90..719bf7862 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -176,19 +176,8 @@ static std::vector state_suffixes() { return res; } -manager::manager(unsigned max_num_contexts, ast_manager& manager) : +manager::manager(ast_manager& manager) : m(manager), m_mux(m, state_suffixes()) { - - ref pool0_base = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); - ref pool1_base = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); - ref pool2_base = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); - - m_pool0 = alloc(solver_pool, pool0_base.get(), max_num_contexts); - m_pool1 = alloc(solver_pool, pool1_base.get(), max_num_contexts); - m_pool2 = alloc(solver_pool, pool2_base.get(), max_num_contexts); } diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index b8783369d..2149395ef 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -79,10 +79,6 @@ class manager { // manager of multiplexed names sym_mux m_mux; - // three solver pools for different queries - scoped_ptr m_pool0; - scoped_ptr m_pool1; - scoped_ptr m_pool2; unsigned n_index() const { return 0; } unsigned o_index(unsigned i) const { return i + 1; } @@ -90,7 +86,7 @@ class manager { void add_new_state(func_decl * s); public: - manager(unsigned max_num_contexts, ast_manager & manager); + manager(ast_manager & manager); ast_manager& get_manager() const { return m; } @@ -152,29 +148,6 @@ public: unsigned tgt_idx, bool homogenous = true) const {m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous);} - - // three different solvers with three different sets of parameters - // different solvers are used for different types of queries in spacer - solver* mk_solver0() {return m_pool0->mk_solver();} - void updt_params0(const params_ref &p) {m_pool0->updt_params(p);} - - solver* mk_solver1() {return m_pool1->mk_solver();} - void updt_params1(const params_ref &p) {m_pool1->updt_params(p);} - - solver* mk_solver2() {return m_pool2->mk_solver();} - void updt_params2(const params_ref &p) {m_pool2->updt_params(p);} - - void collect_statistics(statistics& st) const { - m_pool0->collect_statistics(st); - m_pool1->collect_statistics(st); - m_pool2->collect_statistics(st); - } - - void reset_statistics() { - m_pool0->reset_statistics(); - m_pool1->reset_statistics(); - m_pool2->reset_statistics(); - } }; /** Skolem constants for quantified spacer */ diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 7be4443e3..d8d7fec97 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -40,9 +40,10 @@ Revision History: namespace spacer { -prop_solver::prop_solver(spacer::manager& pm, +prop_solver::prop_solver(ast_manager &m, + solver *solver0, solver *solver1, fixedpoint_params const& p, symbol const& name) : - m(pm.get_manager()), + m(m), m_name(name), m_ctx(nullptr), m_pos_level_atoms(m), @@ -55,8 +56,8 @@ prop_solver::prop_solver(spacer::manager& pm, m_use_push_bg(p.spacer_keep_proxy()) { - m_solvers[0] = pm.mk_solver0(); - m_solvers[1] = pm.mk_solver1(); + m_solvers[0] = solver0; + m_solvers[1] = solver1; m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), p.spacer_iuc(), diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index 337f24825..ecc838d1a 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -29,19 +29,21 @@ Revision History: #include "smt/smt_kernel.h" #include "util/util.h" #include "util/vector.h" -#include "muz/spacer/spacer_manager.h" +#include "solver/solver.h" #include "muz/spacer/spacer_iuc_solver.h" +#include "muz/spacer/spacer_util.h" struct fixedpoint_params; namespace spacer { +typedef ptr_vector decl_vector; class prop_solver { private: ast_manager& m; symbol m_name; - solver* m_solvers[2]; + ref m_solvers[2]; scoped_ptr m_contexts[2]; iuc_solver * m_ctx; decl_vector m_level_preds; @@ -73,7 +75,7 @@ private: public: - prop_solver(spacer::manager &manager, + prop_solver(ast_manager &m, solver *solver0, solver* solver1, fixedpoint_params const& p, symbol const& name); @@ -142,7 +144,7 @@ public: solver *sol; scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) : sol(nullptr) { - sol = ps.m_solvers[solver_id == 0 ? 0 : 0 /* 1 */]; + sol = ps.m_solvers[solver_id == 0 ? 0 : 0 /* 1 */].get(); if (!sol) return; sol->push_params();