mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
Switch rest of spacer to new model API and remove mev_util
This commit is contained in:
Arie Gurfinkel
parent
a222b6d41f
commit
4204b6ede2
|
|
@ -36,7 +36,6 @@ Notes:
|
|||
#include "muz/base/dl_rule_set.h"
|
||||
#include "smt/tactic/unit_subsumption_tactic.h"
|
||||
#include "model/model_smt2_pp.h"
|
||||
#include "model/model_evaluator.h"
|
||||
#include "muz/transforms/dl_mk_rule_inliner.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
|
|
@ -356,12 +355,10 @@ pob *derivation::create_next_child ()
|
|||
// this is possible if m_post was weakened for some reason
|
||||
model_ref mdl;
|
||||
if (!pt.is_must_reachable(mk_and(summaries), &mdl)) { return nullptr; }
|
||||
mdl->set_model_completion(false);
|
||||
|
||||
model_evaluator_util mev (m);
|
||||
mev.set_model (*mdl);
|
||||
// find must summary used
|
||||
|
||||
reach_fact *rf = pt.get_used_rf (*mev.get_model(), true);
|
||||
reach_fact *rf = pt.get_used_rf (*mdl, true);
|
||||
|
||||
// get an implicant of the summary
|
||||
expr_ref_vector u(m), lits(m);
|
||||
|
|
@ -2883,7 +2880,6 @@ expr_ref context::get_ground_sat_answer()
|
|||
// smt context to obtain local cexes
|
||||
ref<solver> cex_ctx =
|
||||
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
|
||||
model_evaluator_util mev (m);
|
||||
|
||||
// preorder traversal of the query derivation tree
|
||||
for (unsigned curr = 0; curr < pts.size (); curr++) {
|
||||
|
|
@ -2936,8 +2932,7 @@ expr_ref context::get_ground_sat_answer()
|
|||
model_ref local_mdl;
|
||||
cex_ctx->get_model (local_mdl);
|
||||
cex_ctx->pop (1);
|
||||
|
||||
model_evaluator mev(*local_mdl);
|
||||
local_mdl->set_model_completion(true);
|
||||
for (unsigned i = 0; i < child_pts.size(); i++) {
|
||||
pred_transformer& ch_pt = *(child_pts.get(i));
|
||||
unsigned sig_size = ch_pt.sig_size();
|
||||
|
|
@ -2946,7 +2941,7 @@ expr_ref context::get_ground_sat_answer()
|
|||
for (unsigned j = 0; j < sig_size; j++) {
|
||||
expr_ref sig_arg(m), sig_val(m);
|
||||
sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i));
|
||||
VERIFY(mev.eval (sig_arg, sig_val, true));
|
||||
sig_val = (*local_mdl)(sig_arg);
|
||||
ground_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val));
|
||||
ground_arg_vals.push_back(sig_val);
|
||||
}
|
||||
|
|
@ -3166,7 +3161,7 @@ bool context::is_reachable(pob &n)
|
|||
|
||||
// used in case n is unreachable
|
||||
unsigned uses_level = infty_level ();
|
||||
model_ref model;
|
||||
model_ref mdl;
|
||||
|
||||
// used in case n is reachable
|
||||
bool is_concrete;
|
||||
|
|
@ -3177,7 +3172,7 @@ bool context::is_reachable(pob &n)
|
|||
|
||||
unsigned saved = n.level ();
|
||||
n.m_level = infty_level ();
|
||||
lbool res = n.pt().is_reachable(n, nullptr, &model,
|
||||
lbool res = n.pt().is_reachable(n, nullptr, &mdl,
|
||||
uses_level, is_concrete, r,
|
||||
reach_pred_used, num_reuse_reach);
|
||||
n.m_level = saved;
|
||||
|
|
@ -3191,11 +3186,9 @@ bool context::is_reachable(pob &n)
|
|||
SASSERT(res == l_true);
|
||||
SASSERT(is_concrete);
|
||||
|
||||
model_evaluator_util mev (m);
|
||||
mev.set_model(*model);
|
||||
// -- update must summary
|
||||
if (r && r->get_uninterpreted_tail_size () > 0) {
|
||||
reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r);
|
||||
reach_fact_ref rf = n.pt().mk_rf (n, *mdl, *r);
|
||||
n.pt ().add_rf (rf.get ());
|
||||
}
|
||||
|
||||
|
|
@ -3322,6 +3315,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
|
||||
lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r,
|
||||
reach_pred_used, num_reuse_reach);
|
||||
if (model) model->set_model_completion(false);
|
||||
checkpoint ();
|
||||
IF_VERBOSE (1, verbose_stream () << "." << std::flush;);
|
||||
switch (res) {
|
||||
|
|
@ -3330,13 +3324,11 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
// update stats
|
||||
m_stats.m_num_reuse_reach += num_reuse_reach;
|
||||
|
||||
model_evaluator_util mev (m);
|
||||
mev.set_model (*model);
|
||||
// must-reachable
|
||||
if (is_concrete) {
|
||||
// -- update must summary
|
||||
if (r && r->get_uninterpreted_tail_size() > 0) {
|
||||
reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r);
|
||||
reach_fact_ref rf = n.pt().mk_rf (n, *model, *r);
|
||||
checkpoint ();
|
||||
n.pt ().add_rf (rf.get ());
|
||||
checkpoint ();
|
||||
|
|
@ -3374,7 +3366,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
// create a child of n
|
||||
|
||||
out.push_back(&n);
|
||||
VERIFY(create_children (n, *r, mev, reach_pred_used, out));
|
||||
VERIFY(create_children (n, *r, *model, reach_pred_used, out));
|
||||
IF_VERBOSE(1, verbose_stream () << " U "
|
||||
<< std::fixed << std::setprecision(2)
|
||||
<< watch.get_seconds () << "\n";);
|
||||
|
|
@ -3449,12 +3441,10 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
|
|||
SASSERT(m_weak_abs);
|
||||
m_stats.m_expand_pob_undef++;
|
||||
if (r && r->get_uninterpreted_tail_size() > 0) {
|
||||
model_evaluator_util mev(m);
|
||||
mev.set_model(*model);
|
||||
// do not trust reach_pred_used
|
||||
for (unsigned i = 0, sz = reach_pred_used.size(); i < sz; ++i)
|
||||
{ reach_pred_used[i] = false; }
|
||||
has_new_child = create_children(n,*r,mev,reach_pred_used, out);
|
||||
has_new_child = create_children(n, *r, *model, reach_pred_used, out);
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << " UNDEF "
|
||||
<< std::fixed << std::setprecision(2)
|
||||
|
|
@ -3640,7 +3630,7 @@ reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r)
|
|||
\brief create children states from model cube.
|
||||
*/
|
||||
bool context::create_children(pob& n, datalog::rule const& r,
|
||||
model_evaluator_util &mev,
|
||||
model &mdl,
|
||||
const vector<bool> &reach_pred_used,
|
||||
pob_ref_buffer &out)
|
||||
{
|
||||
|
|
@ -3649,7 +3639,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
|
||||
TRACE("spacer",
|
||||
tout << "Model:\n";
|
||||
model_smt2_pp(tout, m, *mev.get_model (), 0);
|
||||
model_smt2_pp(tout, m, mdl, 0);
|
||||
tout << "\n";
|
||||
tout << "Transition:\n" << mk_pp(pt.get_transition(r), m) << "\n";
|
||||
tout << "Pob:\n" << mk_pp(n.post(), m) << "\n";);
|
||||
|
|
@ -3665,7 +3655,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
forms.push_back(pt.get_transition(r));
|
||||
forms.push_back(n.post());
|
||||
|
||||
compute_implicant_literals (*mev.get_model(), forms, lits);
|
||||
compute_implicant_literals (mdl, forms, lits);
|
||||
expr_ref phi = mk_and (lits);
|
||||
|
||||
// primed variables of the head
|
||||
|
|
@ -3680,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
// skolems of the pob
|
||||
n.get_skolems(vars);
|
||||
|
||||
n.pt().mbp(vars, phi, *mev.get_model (), true, use_ground_pob());
|
||||
n.pt().mbp(vars, phi, mdl, true, use_ground_pob());
|
||||
//qe::reduce_array_selects (*mev.get_model (), phi1);
|
||||
SASSERT (!m_ground_pob || vars.empty ());
|
||||
|
||||
|
|
@ -3694,7 +3684,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
|
||||
if (m_use_gpdr && preds.size() > 1) {
|
||||
SASSERT(vars.empty());
|
||||
return gpdr_create_split_children(n, r, phi, mev.get_model(), out);
|
||||
return gpdr_create_split_children(n, r, phi, mdl, out);
|
||||
}
|
||||
|
||||
derivation *deriv = alloc(derivation, n, r, phi, vars);
|
||||
|
|
@ -3717,7 +3707,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
|
||||
const ptr_vector<app> *aux = nullptr;
|
||||
expr_ref sum(m);
|
||||
sum = pt.get_origin_summary (*mev.get_model(), prev_level(n.level()),
|
||||
sum = pt.get_origin_summary (mdl, prev_level(n.level()),
|
||||
j, reach_pred_used[j], &aux);
|
||||
if (!sum) {
|
||||
dealloc(deriv);
|
||||
|
|
@ -3727,7 +3717,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
}
|
||||
|
||||
// create post for the first child and add to queue
|
||||
pob* kid = deriv->create_first_child (*mev.get_model());
|
||||
pob* kid = deriv->create_first_child (mdl);
|
||||
|
||||
// -- failed to create derivation, cleanup and bail out
|
||||
if (!kid) {
|
||||
|
|
@ -3744,8 +3734,8 @@ bool context::create_children(pob& n, datalog::rule const& r,
|
|||
// -- not satisfy 'T && phi'. It is possible to recover from
|
||||
// -- that more gracefully. For now, we just remove the
|
||||
// -- derivation completely forcing it to be recomputed
|
||||
if (m_weak_abs && (!mev.is_true(pt.get_transition(r)) ||
|
||||
!mev.is_true(n.post())))
|
||||
if (m_weak_abs && (!mdl.is_true(pt.get_transition(r)) ||
|
||||
!mdl.is_true(n.post())))
|
||||
{ kid->reset_derivation(); }
|
||||
|
||||
out.push_back(kid);
|
||||
|
|
|
|||
|
|
@ -940,7 +940,7 @@ class context {
|
|||
bool gpdr_check_reachability(unsigned lvl, model_search &ms);
|
||||
bool gpdr_create_split_children(pob &n, const datalog::rule &r,
|
||||
expr *trans,
|
||||
model_ref &mdl,
|
||||
model &mdl,
|
||||
pob_ref_buffer &out);
|
||||
|
||||
// Functions used by search.
|
||||
|
|
@ -952,7 +952,7 @@ class context {
|
|||
bool is_reachable(pob &n);
|
||||
lbool expand_pob(pob &n, pob_ref_buffer &out);
|
||||
bool create_children(pob& n, const datalog::rule &r,
|
||||
model_evaluator_util &mdl,
|
||||
model &mdl,
|
||||
const vector<bool>& reach_pred_used,
|
||||
pob_ref_buffer &out);
|
||||
|
||||
|
|
|
|||
|
|
@ -306,7 +306,7 @@ bool context::gpdr_check_reachability(unsigned lvl, model_search &ms) {
|
|||
|
||||
bool context::gpdr_create_split_children(pob &n, const datalog::rule &r,
|
||||
expr *trans,
|
||||
model_ref &mdl,
|
||||
model &mdl,
|
||||
pob_ref_buffer &out) {
|
||||
pred_transformer &pt = n.pt();
|
||||
ptr_vector<func_decl> preds;
|
||||
|
|
@ -330,7 +330,7 @@ bool context::gpdr_create_split_children(pob &n, const datalog::rule &r,
|
|||
expr_ref_vector lits(m);
|
||||
flatten_and(trans, lits);
|
||||
vector<expr_ref_vector> res(preds.size(), expr_ref_vector(m));
|
||||
_mbc(pmap, lits, *mdl.get(), res);
|
||||
_mbc(pmap, lits, mdl, res);
|
||||
|
||||
// pick an order to process children
|
||||
unsigned_vector kid_order;
|
||||
|
|
|
|||
|
|
@ -69,64 +69,6 @@ Notes:
|
|||
|
||||
namespace spacer {
|
||||
|
||||
/////////////////////////
|
||||
// model_evaluator_util
|
||||
//
|
||||
|
||||
model_evaluator_util::model_evaluator_util(ast_manager& m) :
|
||||
m(m), m_mev(nullptr) {
|
||||
reset (nullptr);
|
||||
}
|
||||
|
||||
model_evaluator_util::~model_evaluator_util() {reset (nullptr);}
|
||||
|
||||
|
||||
void model_evaluator_util::reset(model* model) {
|
||||
if (m_mev) {
|
||||
dealloc(m_mev);
|
||||
m_mev = nullptr;
|
||||
}
|
||||
m_model = model;
|
||||
if (m_model)
|
||||
m_mev = alloc(model_evaluator, *m_model);
|
||||
}
|
||||
|
||||
bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) {
|
||||
m_mev->set_model_completion (model_completion);
|
||||
try {
|
||||
m_mev->operator() (e, result);
|
||||
return true;
|
||||
}
|
||||
catch (model_evaluator_exception &ex) {
|
||||
(void)ex;
|
||||
TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";);
|
||||
return false;
|
||||
}
|
||||
}
|
||||
|
||||
bool model_evaluator_util::eval(const expr_ref_vector &v,
|
||||
expr_ref& res, bool model_completion) {
|
||||
expr_ref e(m);
|
||||
e = mk_and (v);
|
||||
return eval(e, res, model_completion);
|
||||
}
|
||||
|
||||
|
||||
bool model_evaluator_util::is_true(const expr_ref_vector &v) {
|
||||
expr_ref res(m);
|
||||
return eval (v, res, false) && m.is_true (res);
|
||||
}
|
||||
|
||||
bool model_evaluator_util::is_false(expr *x) {
|
||||
expr_ref res(m);
|
||||
return eval(x, res, false) && m.is_false (res);
|
||||
}
|
||||
|
||||
bool model_evaluator_util::is_true(expr *x) {
|
||||
expr_ref res(m);
|
||||
return eval(x, res, false) && m.is_true (res);
|
||||
}
|
||||
|
||||
void subst_vars(ast_manager& m,
|
||||
app_ref_vector const& vars, model& mdl, expr_ref& fml) {
|
||||
model::scoped_model_completion _sc_(mdl, true);
|
||||
|
|
@ -876,36 +818,36 @@ namespace {
|
|||
}
|
||||
};
|
||||
|
||||
bool mbqi_project_var(model_evaluator_util &mev, app* var, expr_ref &fml) {
|
||||
bool mbqi_project_var(model &mdl, app* var, expr_ref &fml) {
|
||||
ast_manager &m = fml.get_manager();
|
||||
model::scoped_model_completion _sc_(mdl, false);
|
||||
|
||||
expr_ref val(m);
|
||||
mev.eval(var, val, false);
|
||||
val = mdl(var);
|
||||
|
||||
TRACE("mbqi_project_verbose",
|
||||
tout << "MBQI: var: " << mk_pp(var, m) << "\n"
|
||||
<< "fml: " << fml << "\n";);
|
||||
tout << "MBQI: var: " << mk_pp(var, m) << "\n"
|
||||
<< "fml: " << fml << "\n";);
|
||||
expr_ref_vector terms(m);
|
||||
index_term_finder finder(m, var, terms);
|
||||
for_each_expr(finder, fml);
|
||||
|
||||
TRACE("mbqi_project_verbose",
|
||||
tout << "terms:\n" << terms << "\n";);
|
||||
TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";);
|
||||
|
||||
for(expr * term : terms) {
|
||||
expr_ref tval(m);
|
||||
mev.eval(term, tval, false);
|
||||
tval = mdl(term);
|
||||
|
||||
TRACE("mbqi_project_verbose",
|
||||
tout << "term: " << mk_pp(term, m)
|
||||
<< " tval: " << tval
|
||||
<< " val: " << mk_pp(val, m) << "\n";);
|
||||
<< " tval: " << tval << " val: " << val << "\n";);
|
||||
|
||||
// -- if the term does not contain an occurrence of var
|
||||
// -- and is in the same equivalence class in the model
|
||||
if (tval == val && !occurs(var, term)) {
|
||||
TRACE("mbqi_project",
|
||||
tout << "MBQI: replacing " << mk_pp(var, m) << " with " << mk_pp(term, m) << "\n";);
|
||||
tout << "MBQI: replacing " << mk_pp(var, m)
|
||||
<< " with " << mk_pp(term, m) << "\n";);
|
||||
expr_safe_replace sub(m);
|
||||
sub.insert(var, term);
|
||||
sub(fml);
|
||||
|
|
@ -914,23 +856,23 @@ namespace {
|
|||
}
|
||||
|
||||
TRACE("mbqi_project",
|
||||
tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";);
|
||||
tout << "MBQI: failed to eliminate " << mk_pp(var, m)
|
||||
<< " from " << fml << "\n";);
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void mbqi_project(model &M, app_ref_vector &vars, expr_ref &fml) {
|
||||
void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml) {
|
||||
ast_manager &m = fml.get_manager();
|
||||
model_evaluator_util mev(m);
|
||||
mev.set_model(M);
|
||||
expr_ref tmp(m);
|
||||
model::scoped_model_completion _sc_(mdl, false);
|
||||
// -- evaluate to initialize mev cache
|
||||
mev.eval(fml, tmp, false);
|
||||
tmp = mdl(fml);
|
||||
tmp.reset();
|
||||
|
||||
unsigned j = 0;
|
||||
for(app* v : vars)
|
||||
if (!mbqi_project_var(mev, v, fml))
|
||||
if (!mbqi_project_var(mdl, v, fml))
|
||||
vars[j++] = v;
|
||||
vars.shrink(j);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,7 +40,6 @@ Revision History:
|
|||
|
||||
class model;
|
||||
class model_core;
|
||||
class model_evaluator;
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
|
@ -79,33 +78,6 @@ namespace spacer {
|
|||
typedef ptr_vector<func_decl> decl_vector;
|
||||
typedef obj_hashtable<func_decl> func_decl_set;
|
||||
|
||||
// TBD: deprecate
|
||||
class model_evaluator_util {
|
||||
ast_manager& m;
|
||||
model_ref m_model;
|
||||
model_evaluator* m_mev;
|
||||
|
||||
/// initialize with a given model. All previous state is lost. model can be NULL
|
||||
void reset (model *model);
|
||||
public:
|
||||
model_evaluator_util(ast_manager& m);
|
||||
~model_evaluator_util();
|
||||
|
||||
void set_model(model &model) {reset (&model);}
|
||||
model_ref &get_model() {return m_model;}
|
||||
ast_manager& get_ast_manager() const {return m;}
|
||||
|
||||
public:
|
||||
bool is_true (const expr_ref_vector &v);
|
||||
bool is_false(expr* x);
|
||||
bool is_true(expr* x);
|
||||
|
||||
bool eval (const expr_ref_vector &v, expr_ref &result, bool model_completion);
|
||||
/// evaluates an expression
|
||||
bool eval (expr *e, expr_ref &result, bool model_completion);
|
||||
// expr_ref eval(expr* e, bool complete=true);
|
||||
};
|
||||
|
||||
/**
|
||||
\brief hoist non-boolean if expressions.
|
||||
*/
|
||||
|
|
@ -146,7 +118,7 @@ namespace spacer {
|
|||
*/
|
||||
void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars);
|
||||
|
||||
void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml);
|
||||
void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml);
|
||||
|
||||
bool contains_selects (expr* fml, ast_manager& m);
|
||||
void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);
|
||||
|
|
|
|||
Loading…
Reference in a new issue