mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Moved pool_solvers from spacer::manager into spacer::context

Browse source
This commit is contained in:
Arie Gurfinkel 2018-05-31 14:48:01 -07:00
parent 451d42319b
commit 0b387cd7eb
6 changed files with 94 additions and 96 deletions
Download patch file Download diff file Expand all files Collapse all files

113
src/muz/spacer/spacer_context.cpp
View file

@ -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<solver> pool0_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> pool1_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> 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();

16
src/muz/spacer/spacer_context.h
View file

@ -290,7 +290,7 @@ class pred_transformer {
func_decl_ref_vector m_sig; // signature
ptr_vector<pred_transformer> m_use; // places where 'this' is referenced.
ptr_vector<datalog::rule> m_rules; // rules used to derive transformer
prop_solver m_solver; // solver context
scoped_ptr<prop_solver> m_solver; // solver context
ref<solver> 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<solver_pool> m_pool0;
scoped_ptr<solver_pool> m_pool1;
scoped_ptr<solver_pool> 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 ();}

13
src/muz/spacer/spacer_manager.cpp
View file

@ -176,19 +176,8 @@ static std::vector<std::string> 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<solver> pool0_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> pool1_base =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
ref<solver> 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);
}

29
src/muz/spacer/spacer_manager.h
View file

@ -79,10 +79,6 @@ class manager {
// manager of multiplexed names
sym_mux m_mux;
// three solver pools for different queries
scoped_ptr<solver_pool> m_pool0;
scoped_ptr<solver_pool> m_pool1;
scoped_ptr<solver_pool> 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 */

9
src/muz/spacer/spacer_prop_solver.cpp
View file

@ -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(),

10
src/muz/spacer/spacer_prop_solver.h
View file

@ -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<func_decl> decl_vector;
class prop_solver {
private:
ast_manager& m;
symbol m_name;
solver* m_solvers[2];
ref<solver> m_solvers[2];
scoped_ptr<iuc_solver> 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();