mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-06-17 09:40:40 -07:00
parent 66e6dc78a3 6bc14afa5e
commit 190428ab3f
8 changed files with 303 additions and 410 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/api/api_qe.cpp
View file

@ -62,7 +62,7 @@ extern "C"
expr_ref result (mk_c(c)->m ()); expr_ref result (mk_c(c)->m ());
result = to_expr (body); result = to_expr (body);
model_ref model (to_model_ref (m)); model_ref model (to_model_ref (m));
spacer::qe_project (mk_c(c)->m (), vars, result, model); spacer::qe_project (mk_c(c)->m (), vars, result, *model);
mk_c(c)->save_ast_trail (result.get ()); mk_c(c)->save_ast_trail (result.get ());
return of_expr (result.get ()); return of_expr (result.get ());
@ -119,11 +119,8 @@ extern "C"
facts.push_back (to_expr (fml)); facts.push_back (to_expr (fml));
flatten_and (facts); flatten_and (facts);
spacer::model_evaluator_util mev (mk_c(c)->m());
mev.set_model (*model);
expr_ref_vector lits (mk_c(c)->m()); expr_ref_vector lits (mk_c(c)->m());
spacer::compute_implicant_literals (mev, facts, lits); spacer::compute_implicant_literals (*model, facts, lits);
expr_ref result (mk_c(c)->m ()); expr_ref result (mk_c(c)->m ());
result = mk_and (lits); result = mk_and (lits);

5
src/api/python/z3/z3.py
View file

@ -8858,7 +8858,10 @@ class FPNumRef(FPRef):
1.25 1.25
""" """
def significand_as_long(self): def significand_as_long(self):
return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast()) ptr = (ctypes.c_ulonglong * 1)()
if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr):
raise Z3Exception("error retrieving the significand of a numeral.")
return ptr[0]
"""The significand of the numeral as a bit-vector expression. """The significand of the numeral as a bit-vector expression.

7
src/model/model.h
View file

@ -24,6 +24,9 @@ Revision History:
#include "util/ref.h" #include "util/ref.h"
#include "ast/ast_translation.h" #include "ast/ast_translation.h"
class model;
typedef ref<model> model_ref;
class model : public model_core { class model : public model_core {
protected: protected:
typedef obj_map<sort, ptr_vector<expr>*> sort2universe; typedef obj_map<sort, ptr_vector<expr>*> sort2universe;
@ -82,12 +85,10 @@ public:
m_old_completion(m.m_mev.get_model_completion()), m_model(m) { m_old_completion(m.m_mev.get_model_completion()), m_model(m) {
m.set_model_completion(c); m.set_model_completion(c);
} }
#if 0
scoped_model_completion(model_ref& m, bool c): scoped_model_completion(model_ref& m, bool c):
m_old_completion(m->m_mev.get_model_completion()), m_model(*m.get()) { m_old_completion(m->m_mev.get_model_completion()), m_model(*m.get()) {
m->set_model_completion(c); m->set_model_completion(c);
} }
#endif
~scoped_model_completion() { ~scoped_model_completion() {
m_model.set_model_completion(m_old_completion); m_model.set_model_completion(m_old_completion);
} }
@ -96,7 +97,5 @@ public:
}; };
typedef ref<model> model_ref;
#endif /* MODEL_H_ */ #endif /* MODEL_H_ */

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

@ -36,7 +36,6 @@ Notes:
#include "muz/base/dl_rule_set.h" #include "muz/base/dl_rule_set.h"
#include "smt/tactic/unit_subsumption_tactic.h" #include "smt/tactic/unit_subsumption_tactic.h"
#include "model/model_smt2_pp.h" #include "model/model_smt2_pp.h"
#include "model/model_evaluator.h"
#include "muz/transforms/dl_mk_rule_inliner.h" #include "muz/transforms/dl_mk_rule_inliner.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/ast_ll_pp.h" #include "ast/ast_ll_pp.h"
@ -195,10 +194,10 @@ void derivation::add_premise (pred_transformer &pt,
pob *derivation::create_first_child (model_evaluator_util &mev) { pob *derivation::create_first_child (model &mdl) {
if (m_premises.empty()) { return nullptr; } if (m_premises.empty()) { return nullptr; }
m_active = 0; m_active = 0;
return create_next_child(mev); return create_next_child(mdl);
} }
void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) { void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) {
@ -236,7 +235,7 @@ void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res)
sub(fml, res); sub(fml, res);
} }
pob *derivation::create_next_child (model_evaluator_util &mev) pob *derivation::create_next_child(model &mdl)
{ {
timeit _timer (is_trace_enabled("spacer_timeit"), timeit _timer (is_trace_enabled("spacer_timeit"),
"spacer::derivation::create_next_child", "spacer::derivation::create_next_child",
@ -265,13 +264,13 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
verbose_stream ()); verbose_stream ());
vars.append(m_evars); vars.append(m_evars);
m_evars.reset(); m_evars.reset();
pt().mbp(vars, m_trans, mev.get_model(), pt().mbp(vars, m_trans, mdl,
true, pt().get_context().use_ground_pob()); true, pt().get_context().use_ground_pob());
m_evars.append (vars); m_evars.append (vars);
vars.reset(); vars.reset();
} }
if (!mev.is_true (m_premises[m_active].get_summary())) { if (!mdl.is_true(m_premises[m_active].get_summary())) {
IF_VERBOSE(1, verbose_stream() << "Summary unexpectendly not true\n";); IF_VERBOSE(1, verbose_stream() << "Summary unexpectendly not true\n";);
return nullptr; return nullptr;
} }
@ -294,7 +293,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
verbose_stream ()); verbose_stream ());
// include m_evars in case they can eliminated now as well // include m_evars in case they can eliminated now as well
vars.append(m_evars); vars.append(m_evars);
pt().mbp(vars, post, mev.get_model(), pt().mbp(vars, post, mdl,
true, pt().get_context().use_ground_pob()); true, pt().get_context().use_ground_pob());
//qe::reduce_array_selects (*mev.get_model (), post); //qe::reduce_array_selects (*mev.get_model (), post);
} }
@ -337,7 +336,6 @@ pob *derivation::create_next_child ()
// construct a new model consistent with the must summary of m_active premise // construct a new model consistent with the must summary of m_active premise
pred_transformer &pt = m_premises[m_active].pt (); pred_transformer &pt = m_premises[m_active].pt ();
model_ref model;
ast_manager &m = get_ast_manager (); ast_manager &m = get_ast_manager ();
manager &pm = get_manager (); manager &pm = get_manager ();
@ -355,18 +353,17 @@ pob *derivation::create_next_child ()
// if not true, bail out, the must summary of m_active is not strong enough // if not true, bail out, the must summary of m_active is not strong enough
// this is possible if m_post was weakened for some reason // this is possible if m_post was weakened for some reason
if (!pt.is_must_reachable(mk_and(summaries), &model)) { return nullptr; } 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 (*model);
// find must summary used // find must summary used
reach_fact *rf = pt.get_used_rf (*mdl, true);
reach_fact *rf = pt.get_used_rf (mev, true);
// get an implicant of the summary // get an implicant of the summary
expr_ref_vector u(m), lits(m); expr_ref_vector u(m), lits(m);
u.push_back (rf->get ()); u.push_back (rf->get ());
compute_implicant_literals (mev, u, lits); compute_implicant_literals (*mdl, u, lits);
expr_ref v(m); expr_ref v(m);
v = mk_and (lits); v = mk_and (lits);
@ -398,7 +395,7 @@ pob *derivation::create_next_child ()
if (!vars.empty ()) { if (!vars.empty ()) {
vars.append(m_evars); vars.append(m_evars);
m_evars.reset(); m_evars.reset();
this->pt().mbp(vars, m_trans, mev.get_model(), this->pt().mbp(vars, m_trans, *mdl,
true, this->pt().get_context().use_ground_pob()); true, this->pt().get_context().use_ground_pob());
// keep track of implicitly quantified variables // keep track of implicitly quantified variables
m_evars.append (vars); m_evars.append (vars);
@ -408,7 +405,7 @@ pob *derivation::create_next_child ()
m_active++; m_active++;
return create_next_child (mev); return create_next_child (*mdl);
} }
/// derivation::premise /// derivation::premise
@ -795,27 +792,24 @@ bool pred_transformer::is_must_reachable(expr* state, model_ref* model)
reach_fact* pred_transformer::get_used_rf (model_evaluator_util& mev, reach_fact* pred_transformer::get_used_rf (model& mdl, bool all) {
bool all) {
expr_ref v (m); expr_ref v (m);
model::scoped_model_completion _sc_(mdl, false);
for (auto *rf : m_reach_facts) { for (auto *rf : m_reach_facts) {
if (!all && rf->is_init()) continue; if (!all && rf->is_init()) continue;
VERIFY(mev.eval (rf->tag(), v, false)); if (mdl.is_false(rf->tag())) return rf;
if (m.is_false(v)) return rf;
} }
UNREACHABLE(); UNREACHABLE();
return nullptr; return nullptr;
} }
reach_fact *pred_transformer::get_used_origin_rf (model_evaluator_util& mev, reach_fact *pred_transformer::get_used_origin_rf(model& mdl, unsigned oidx) {
unsigned oidx) {
expr_ref b(m), v(m); expr_ref b(m), v(m);
model::scoped_model_completion _sc_(mdl, false);
for (auto *rf : m_reach_facts) { for (auto *rf : m_reach_facts) {
pm.formula_n2o (rf->tag(), v, oidx); pm.formula_n2o (rf->tag(), v, oidx);
VERIFY(mev.eval (v, b, false)); if (mdl.is_false(v)) return rf;
if (m.is_false (b)) return rf;
} }
UNREACHABLE(); UNREACHABLE();
return nullptr; return nullptr;
@ -1139,12 +1133,13 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
* *
* returns an implicant of the summary * returns an implicant of the summary
*/ */
expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, expr_ref pred_transformer::get_origin_summary (model &mdl,
unsigned level, unsigned level,
unsigned oidx, unsigned oidx,
bool must, bool must,
const ptr_vector<app> **aux) const ptr_vector<app> **aux)
{ {
model::scoped_model_completion _sc_(mdl, false);
expr_ref_vector summary (m); expr_ref_vector summary (m);
expr_ref v(m); expr_ref v(m);
@ -1153,7 +1148,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
// -- no auxiliary variables in lemmas // -- no auxiliary variables in lemmas
*aux = nullptr; *aux = nullptr;
} else { // find must summary to use } else { // find must summary to use
reach_fact *f = get_used_origin_rf (mev, oidx); reach_fact *f = get_used_origin_rf(mdl, oidx);
summary.push_back (f->get ()); summary.push_back (f->get ());
*aux = &f->aux_vars (); *aux = &f->aux_vars ();
} }
@ -1167,13 +1162,11 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
} }
// bail out of if the model is insufficient // bail out of if the model is insufficient
if (!mev.is_true(summary)) if (!mdl.is_true(summary)) return expr_ref(m);
return expr_ref(m);
// -- pick an implicant // -- pick an implicant
expr_ref_vector lits(m); expr_ref_vector lits(m);
compute_implicant_literals (mev, summary, lits); compute_implicant_literals (mdl, summary, lits);
return mk_and(lits); return mk_and(lits);
} }
@ -1267,7 +1260,7 @@ bool pred_transformer::is_qblocked (pob &n) {
} }
void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, model &mdl,
bool reduce_all_selects, bool force) { bool reduce_all_selects, bool force) {
scoped_watch _t_(m_mbp_watch); scoped_watch _t_(m_mbp_watch);
qe_project(m, vars, fml, mdl, reduce_all_selects, use_native_mbp(), !force); qe_project(m, vars, fml, mdl, reduce_all_selects, use_native_mbp(), !force);
@ -2887,7 +2880,6 @@ expr_ref context::get_ground_sat_answer()
// smt context to obtain local cexes // smt context to obtain local cexes
ref<solver> cex_ctx = ref<solver> cex_ctx =
mk_smt_solver(m, params_ref::get_empty(), symbol::null); mk_smt_solver(m, params_ref::get_empty(), symbol::null);
model_evaluator_util mev (m);
// preorder traversal of the query derivation tree // preorder traversal of the query derivation tree
for (unsigned curr = 0; curr < pts.size (); curr++) { for (unsigned curr = 0; curr < pts.size (); curr++) {
@ -2940,8 +2932,7 @@ expr_ref context::get_ground_sat_answer()
model_ref local_mdl; model_ref local_mdl;
cex_ctx->get_model (local_mdl); cex_ctx->get_model (local_mdl);
cex_ctx->pop (1); cex_ctx->pop (1);
local_mdl->set_model_completion(true);
model_evaluator mev(*local_mdl);
for (unsigned i = 0; i < child_pts.size(); i++) { for (unsigned i = 0; i < child_pts.size(); i++) {
pred_transformer& ch_pt = *(child_pts.get(i)); pred_transformer& ch_pt = *(child_pts.get(i));
unsigned sig_size = ch_pt.sig_size(); unsigned sig_size = ch_pt.sig_size();
@ -2950,7 +2941,7 @@ expr_ref context::get_ground_sat_answer()
for (unsigned j = 0; j < sig_size; j++) { for (unsigned j = 0; j < sig_size; j++) {
expr_ref sig_arg(m), sig_val(m); expr_ref sig_arg(m), sig_val(m);
sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i)); 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_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val));
ground_arg_vals.push_back(sig_val); ground_arg_vals.push_back(sig_val);
} }
@ -3170,7 +3161,7 @@ bool context::is_reachable(pob &n)
// used in case n is unreachable // used in case n is unreachable
unsigned uses_level = infty_level (); unsigned uses_level = infty_level ();
model_ref model; model_ref mdl;
// used in case n is reachable // used in case n is reachable
bool is_concrete; bool is_concrete;
@ -3181,7 +3172,7 @@ bool context::is_reachable(pob &n)
unsigned saved = n.level (); unsigned saved = n.level ();
n.m_level = infty_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, uses_level, is_concrete, r,
reach_pred_used, num_reuse_reach); reach_pred_used, num_reuse_reach);
n.m_level = saved; n.m_level = saved;
@ -3195,11 +3186,9 @@ bool context::is_reachable(pob &n)
SASSERT(res == l_true); SASSERT(res == l_true);
SASSERT(is_concrete); SASSERT(is_concrete);
model_evaluator_util mev (m);
mev.set_model(*model);
// -- update must summary // -- update must summary
if (r && r->get_uninterpreted_tail_size () > 0) { if (r && r->get_uninterpreted_tail_size () > 0) {
reach_fact_ref rf = n.pt().mk_rf (n, mev, *r); reach_fact_ref rf = n.pt().mk_rf (n, *mdl, *r);
n.pt ().add_rf (rf.get ()); n.pt ().add_rf (rf.get ());
} }
@ -3326,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, lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r,
reach_pred_used, num_reuse_reach); reach_pred_used, num_reuse_reach);
if (model) model->set_model_completion(false);
checkpoint (); checkpoint ();
IF_VERBOSE (1, verbose_stream () << "." << std::flush;); IF_VERBOSE (1, verbose_stream () << "." << std::flush;);
switch (res) { switch (res) {
@ -3334,13 +3324,11 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
// update stats // update stats
m_stats.m_num_reuse_reach += num_reuse_reach; m_stats.m_num_reuse_reach += num_reuse_reach;
model_evaluator_util mev (m);
mev.set_model (*model);
// must-reachable // must-reachable
if (is_concrete) { if (is_concrete) {
// -- update must summary // -- update must summary
if (r && r->get_uninterpreted_tail_size() > 0) { if (r && r->get_uninterpreted_tail_size() > 0) {
reach_fact_ref rf = n.pt().mk_rf (n, mev, *r); reach_fact_ref rf = n.pt().mk_rf (n, *model, *r);
checkpoint (); checkpoint ();
n.pt ().add_rf (rf.get ()); n.pt ().add_rf (rf.get ());
checkpoint (); checkpoint ();
@ -3378,7 +3366,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
// create a child of n // create a child of n
out.push_back(&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 " IF_VERBOSE(1, verbose_stream () << " U "
<< std::fixed << std::setprecision(2) << std::fixed << std::setprecision(2)
<< watch.get_seconds () << "\n";); << watch.get_seconds () << "\n";);
@ -3453,12 +3441,10 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
SASSERT(m_weak_abs); SASSERT(m_weak_abs);
m_stats.m_expand_pob_undef++; m_stats.m_expand_pob_undef++;
if (r && r->get_uninterpreted_tail_size() > 0) { if (r && r->get_uninterpreted_tail_size() > 0) {
model_evaluator_util mev(m);
mev.set_model(*model);
// do not trust reach_pred_used // do not trust reach_pred_used
for (unsigned i = 0, sz = reach_pred_used.size(); i < sz; ++i) for (unsigned i = 0, sz = reach_pred_used.size(); i < sz; ++i)
{ reach_pred_used[i] = false; } { 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 " IF_VERBOSE(1, verbose_stream() << " UNDEF "
<< std::fixed << std::setprecision(2) << std::fixed << std::setprecision(2)
@ -3554,8 +3540,7 @@ bool context::propagate(unsigned min_prop_lvl,
return false; return false;
} }
reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r)
const datalog::rule& r)
{ {
SASSERT(&n.pt() == this); SASSERT(&n.pt() == this);
timeit _timer1 (is_trace_enabled("spacer_timeit"), timeit _timer1 (is_trace_enabled("spacer_timeit"),
@ -3576,7 +3561,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
pred_transformer& ch_pt = ctx.get_pred_transformer (pred); pred_transformer& ch_pt = ctx.get_pred_transformer (pred);
// get a reach fact of body preds used in the model // get a reach fact of body preds used in the model
expr_ref o_ch_reach (m); expr_ref o_ch_reach (m);
reach_fact *kid = ch_pt.get_used_origin_rf (mev, i); reach_fact *kid = ch_pt.get_used_origin_rf(mdl, i);
child_reach_facts.push_back (kid); child_reach_facts.push_back (kid);
pm.formula_n2o (kid->get (), o_ch_reach, i); pm.formula_n2o (kid->get (), o_ch_reach, i);
path_cons.push_back (o_ch_reach); path_cons.push_back (o_ch_reach);
@ -3599,7 +3584,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
if (ctx.reach_dnf()) { if (ctx.reach_dnf()) {
expr_ref_vector u(m), lits(m); expr_ref_vector u(m), lits(m);
u.push_back (res); u.push_back (res);
compute_implicant_literals (mev, u, lits); compute_implicant_literals (mdl, u, lits);
res = mk_and (lits); res = mk_and (lits);
} }
@ -3617,7 +3602,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
timeit _timer1 (is_trace_enabled("spacer_timeit"), timeit _timer1 (is_trace_enabled("spacer_timeit"),
"mk_rf::qe_project", "mk_rf::qe_project",
verbose_stream ()); verbose_stream ());
mbp(vars, res, mev.get_model(), false, true /* force or skolemize */); mbp(vars, res, mdl, false, true /* force or skolemize */);
} }
@ -3645,7 +3630,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev,
\brief create children states from model cube. \brief create children states from model cube.
*/ */
bool context::create_children(pob& n, datalog::rule const& r, bool context::create_children(pob& n, datalog::rule const& r,
model_evaluator_util &mev, model &mdl,
const vector<bool> &reach_pred_used, const vector<bool> &reach_pred_used,
pob_ref_buffer &out) pob_ref_buffer &out)
{ {
@ -3654,7 +3639,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
TRACE("spacer", TRACE("spacer",
tout << "Model:\n"; tout << "Model:\n";
model_smt2_pp(tout, m, *mev.get_model (), 0); model_smt2_pp(tout, m, mdl, 0);
tout << "\n"; tout << "\n";
tout << "Transition:\n" << mk_pp(pt.get_transition(r), m) << "\n"; tout << "Transition:\n" << mk_pp(pt.get_transition(r), m) << "\n";
tout << "Pob:\n" << mk_pp(n.post(), m) << "\n";); tout << "Pob:\n" << mk_pp(n.post(), m) << "\n";);
@ -3670,7 +3655,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
forms.push_back(pt.get_transition(r)); forms.push_back(pt.get_transition(r));
forms.push_back(n.post()); forms.push_back(n.post());
compute_implicant_literals (mev, forms, lits); compute_implicant_literals (mdl, forms, lits);
expr_ref phi = mk_and (lits); expr_ref phi = mk_and (lits);
// primed variables of the head // primed variables of the head
@ -3685,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
// skolems of the pob // skolems of the pob
n.get_skolems(vars); 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); //qe::reduce_array_selects (*mev.get_model (), phi1);
SASSERT (!m_ground_pob || vars.empty ()); SASSERT (!m_ground_pob || vars.empty ());
@ -3699,7 +3684,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
if (m_use_gpdr && preds.size() > 1) { if (m_use_gpdr && preds.size() > 1) {
SASSERT(vars.empty()); 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); derivation *deriv = alloc(derivation, n, r, phi, vars);
@ -3722,7 +3707,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
const ptr_vector<app> *aux = nullptr; const ptr_vector<app> *aux = nullptr;
expr_ref sum(m); expr_ref sum(m);
sum = pt.get_origin_summary (mev, prev_level(n.level()), sum = pt.get_origin_summary (mdl, prev_level(n.level()),
j, reach_pred_used[j], &aux); j, reach_pred_used[j], &aux);
if (!sum) { if (!sum) {
dealloc(deriv); dealloc(deriv);
@ -3732,7 +3717,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
} }
// create post for the first child and add to queue // create post for the first child and add to queue
pob* kid = deriv->create_first_child (mev); pob* kid = deriv->create_first_child (mdl);
// -- failed to create derivation, cleanup and bail out // -- failed to create derivation, cleanup and bail out
if (!kid) { if (!kid) {
@ -3749,8 +3734,8 @@ bool context::create_children(pob& n, datalog::rule const& r,
// -- not satisfy 'T && phi'. It is possible to recover from // -- not satisfy 'T && phi'. It is possible to recover from
// -- that more gracefully. For now, we just remove the // -- that more gracefully. For now, we just remove the
// -- derivation completely forcing it to be recomputed // -- derivation completely forcing it to be recomputed
if (m_weak_abs && (!mev.is_true(pt.get_transition(r)) || if (m_weak_abs && (!mdl.is_true(pt.get_transition(r)) ||
!mev.is_true(n.post()))) !mdl.is_true(n.post())))
{ kid->reset_derivation(); } { kid->reset_derivation(); }
out.push_back(kid); out.push_back(kid);

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

@ -440,10 +440,10 @@ public:
bool is_must_reachable(expr* state, model_ref* model = nullptr); bool is_must_reachable(expr* state, model_ref* model = nullptr);
/// \brief Returns reachability fact active in the given model /// \brief Returns reachability fact active in the given model
/// all determines whether initial reachability facts are included as well /// all determines whether initial reachability facts are included as well
reach_fact *get_used_rf(model_evaluator_util& mev, bool all = true); reach_fact *get_used_rf(model& mdl, bool all = true);
/// \brief Returns reachability fact active in the origin of the given model /// \brief Returns reachability fact active in the origin of the given model
reach_fact* get_used_origin_rf(model_evaluator_util &mev, unsigned oidx); reach_fact* get_used_origin_rf(model &mdl, unsigned oidx);
expr_ref get_origin_summary(model_evaluator_util &mev, expr_ref get_origin_summary(model &mdl,
unsigned level, unsigned oidx, bool must, unsigned level, unsigned oidx, bool must,
const ptr_vector<app> **aux); const ptr_vector<app> **aux);
@ -472,8 +472,7 @@ public:
/// initialize reachability facts using initial rules /// initialize reachability facts using initial rules
void init_rfs (); void init_rfs ();
reach_fact *mk_rf(pob &n, model_evaluator_util &mev, reach_fact *mk_rf(pob &n, model &mdl, const datalog::rule &r);
const datalog::rule &r);
void add_rf (reach_fact *fact); // add reachability fact void add_rf (reach_fact *fact); // add reachability fact
reach_fact* get_last_rf () const { return m_reach_facts.back (); } reach_fact* get_last_rf () const { return m_reach_facts.back (); }
expr* get_last_rf_tag () const; expr* get_last_rf_tag () const;
@ -530,7 +529,7 @@ public:
bool is_qblocked (pob &n); bool is_qblocked (pob &n);
/// \brief interface to Model Based Projection /// \brief interface to Model Based Projection
void mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, void mbp(app_ref_vector &vars, expr_ref &fml, model &mdl,
bool reduce_all_selects, bool force = false); bool reduce_all_selects, bool force = false);
void updt_solver(prop_solver *solver); void updt_solver(prop_solver *solver);
@ -740,7 +739,7 @@ class derivation {
app_ref_vector m_evars; app_ref_vector m_evars;
/// -- create next child using given model as the guide /// -- create next child using given model as the guide
/// -- returns NULL if there is no next child /// -- returns NULL if there is no next child
pob* create_next_child (model_evaluator_util &mev); pob* create_next_child (model &mdl);
/// existentially quantify vars and skolemize the result /// existentially quantify vars and skolemize the result
void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res); void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res);
public: public:
@ -752,7 +751,7 @@ public:
/// creates the first child. Must be called after all the premises /// creates the first child. Must be called after all the premises
/// are added. The model must be valid for the premises /// are added. The model must be valid for the premises
/// Returns NULL if no child exits /// Returns NULL if no child exits
pob *create_first_child (model_evaluator_util &mev); pob *create_first_child (model &mdl);
/// Create the next child. Must summary of the currently active /// Create the next child. Must summary of the currently active
/// premise must be consistent with the transition relation /// premise must be consistent with the transition relation
@ -941,7 +940,7 @@ class context {
bool gpdr_check_reachability(unsigned lvl, model_search &ms); bool gpdr_check_reachability(unsigned lvl, model_search &ms);
bool gpdr_create_split_children(pob &n, const datalog::rule &r, bool gpdr_create_split_children(pob &n, const datalog::rule &r,
expr *trans, expr *trans,
model_ref &mdl, model &mdl,
pob_ref_buffer &out); pob_ref_buffer &out);
// Functions used by search. // Functions used by search.
@ -953,7 +952,7 @@ class context {
bool is_reachable(pob &n); bool is_reachable(pob &n);
lbool expand_pob(pob &n, pob_ref_buffer &out); lbool expand_pob(pob &n, pob_ref_buffer &out);
bool create_children(pob& n, const datalog::rule &r, bool create_children(pob& n, const datalog::rule &r,
model_evaluator_util &mdl, model &mdl,
const vector<bool>& reach_pred_used, const vector<bool>& reach_pred_used,
pob_ref_buffer &out); pob_ref_buffer &out);

4
src/muz/spacer/spacer_pdr.cpp
View file

@ -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, bool context::gpdr_create_split_children(pob &n, const datalog::rule &r,
expr *trans, expr *trans,
model_ref &mdl, model &mdl,
pob_ref_buffer &out) { pob_ref_buffer &out) {
pred_transformer &pt = n.pt(); pred_transformer &pt = n.pt();
ptr_vector<func_decl> preds; 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); expr_ref_vector lits(m);
flatten_and(trans, lits); flatten_and(trans, lits);
vector<expr_ref_vector> res(preds.size(), expr_ref_vector(m)); 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 // pick an order to process children
unsigned_vector kid_order; unsigned_vector kid_order;

234
src/muz/spacer/spacer_util.cpp
View file

@ -69,75 +69,11 @@ Notes:
namespace spacer { 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, void subst_vars(ast_manager& m,
app_ref_vector const& vars, app_ref_vector const& vars, model& mdl, expr_ref& fml) {
model* M, expr_ref& fml) { model::scoped_model_completion _sc_(mdl, true);
expr_safe_replace sub(m); expr_safe_replace sub(m);
model_evaluator_util mev (m); for (app * v : vars) sub.insert (v, mdl(v));
mev.set_model(*M);
for (app * v : vars) {
expr_ref val (m);
VERIFY(mev.eval (v, val, true));
sub.insert (v, val);
}
sub(fml); sub(fml);
} }
@ -161,16 +97,14 @@ namespace spacer {
} }
void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml, void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
const model_ref& M, bool reduce_all_selects, bool use_native_mbp, model & mdl, bool reduce_all_selects, bool use_native_mbp,
bool dont_sub) { bool dont_sub) {
params_ref p; params_ref p;
p.set_bool("reduce_all_selects", reduce_all_selects); p.set_bool("reduce_all_selects", reduce_all_selects);
p.set_bool("dont_sub", dont_sub); p.set_bool("dont_sub", dont_sub);
qe::mbp mbp(m, p); qe::mbp mbp(m, p);
// TODO: deal with const mbp.spacer(vars, mdl, fml);
model *mdl = const_cast<model*>(M.get());
mbp.spacer(vars, *mdl, fml);
} }
/* /*
@ -178,7 +112,7 @@ namespace spacer {
* then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays
*/ */
void qe_project_spacer (ast_manager& m, app_ref_vector& vars, expr_ref& fml, void qe_project_spacer (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
const model_ref& M, bool reduce_all_selects, bool use_native_mbp, model& mdl, bool reduce_all_selects, bool use_native_mbp,
bool dont_sub) { bool dont_sub) {
th_rewriter rw (m); th_rewriter rw (m);
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
@ -221,9 +155,10 @@ namespace spacer {
// sort out vars into bools, arith (int/real), and arrays // sort out vars into bools, arith (int/real), and arrays
for (app* v : vars) { for (app* v : vars) {
if (m.is_bool (v)) { if (m.is_bool (v)) {
// obtain the interpretation of the ith var using model completion // obtain the interpretation of the ith var
VERIFY (M->eval (v, bval, true)); // using model completion
bool_sub.insert (v, bval); model::scoped_model_completion _sc_(mdl, true);
bool_sub.insert (v, mdl(v));
} else if (arr_u.is_array(v)) { } else if (arr_u.is_array(v)) {
array_vars.push_back(v); array_vars.push_back(v);
} else { } else {
@ -242,9 +177,7 @@ namespace spacer {
bool_sub.reset(); bool_sub.reset();
} }
TRACE ("spacer_mbp", TRACE ("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;);
tout << "Array vars:\n";
tout << array_vars;);
vars.reset (); vars.reset ();
@ -253,7 +186,7 @@ namespace spacer {
scoped_no_proof _sp (m); scoped_no_proof _sp (m);
// -- local rewriter that is aware of current proof mode // -- local rewriter that is aware of current proof mode
th_rewriter srw(m); th_rewriter srw(m);
spacer_qe::array_project (*M.get (), array_vars, fml, vars, reduce_all_selects); spacer_qe::array_project (mdl, array_vars, fml, vars, reduce_all_selects);
SASSERT (array_vars.empty ()); SASSERT (array_vars.empty ());
srw (fml); srw (fml);
SASSERT (!m.is_false (fml)); SASSERT (!m.is_false (fml));
@ -261,10 +194,9 @@ namespace spacer {
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
tout << "extended model:\n"; tout << "extended model:\n";
model_pp (tout, *M); model_pp (tout, mdl);
tout << "Auxiliary variables of index and value sorts:\n"; tout << "Auxiliary variables of index and value sorts:\n";
tout << vars; tout << vars;);
);
if (vars.empty()) { break; } if (vars.empty()) { break; }
} }
@ -273,39 +205,32 @@ namespace spacer {
if (!arith_vars.empty ()) { if (!arith_vars.empty ()) {
TRACE ("spacer_mbp", tout << "Arith vars:\n" << arith_vars;); TRACE ("spacer_mbp", tout << "Arith vars:\n" << arith_vars;);
// XXX Does not seem to have an effect
// qe_lite qe(m);
// qe (arith_vars, fml);
// TRACE ("spacer_mbp",
// tout << "After second qelite: " <<
// mk_pp (fml, m) << "\n";);
if (use_native_mbp) { if (use_native_mbp) {
qe::mbp mbp (m); qe::mbp mbp (m);
expr_ref_vector fmls(m); expr_ref_vector fmls(m);
flatten_and (fml, fmls); flatten_and (fml, fmls);
mbp (true, arith_vars, *M.get (), fmls); mbp (true, arith_vars, mdl, fmls);
fml = mk_and(fmls); fml = mk_and(fmls);
SASSERT(arith_vars.empty ()); SASSERT(arith_vars.empty ());
} else { } else {
scoped_no_proof _sp (m); scoped_no_proof _sp (m);
spacer_qe::arith_project (*M.get (), arith_vars, fml); spacer_qe::arith_project (mdl, arith_vars, fml);
} }
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n"; tout << "Projected arith vars:\n" << fml << "\n";
tout << "Remaining arith vars:\n" << arith_vars << "\n";); tout << "Remaining arith vars:\n" << arith_vars << "\n";);
SASSERT (!m.is_false (fml)); SASSERT (!m.is_false (fml));
} }
if (!arith_vars.empty ()) { if (!arith_vars.empty ()) {
mbqi_project (*M.get(), arith_vars, fml); mbqi_project (mdl, arith_vars, fml);
} }
// substitute any remaining arith vars // substitute any remaining arith vars
if (!dont_sub && !arith_vars.empty ()) { if (!dont_sub && !arith_vars.empty ()) {
subst_vars (m, arith_vars, M.get(), fml); subst_vars (m, arith_vars, mdl, fml);
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
tout << "After substituting remaining arith vars:\n"; tout << "After substituting remaining arith vars:\n";
tout << mk_pp (fml, m) << "\n"; tout << mk_pp (fml, m) << "\n";
@ -315,11 +240,9 @@ namespace spacer {
} }
DEBUG_CODE ( DEBUG_CODE (
model_evaluator_util mev (m); model_evaluator mev(mdl);
expr_ref v(m); mev.set_model_completion(false);
mev.set_model(*M.get()); SASSERT(mev.is_true(fml));
SASSERT (mev.eval (fml, v, false));
SASSERT (m.is_true (v));
); );
vars.reset (); vars.reset ();
@ -343,12 +266,14 @@ namespace spacer {
} }
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
const model_ref& M, bool reduce_all_selects, bool use_native_mbp, model &mdl, bool reduce_all_selects, bool use_native_mbp,
bool dont_sub) { bool dont_sub) {
if (use_native_mbp) if (use_native_mbp)
qe_project_z3(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); qe_project_z3(m, vars, fml, mdl,
reduce_all_selects, use_native_mbp, dont_sub);
else else
qe_project_spacer(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); qe_project_spacer(m, vars, fml, mdl,
reduce_all_selects, use_native_mbp, dont_sub);
} }
void expand_literals(ast_manager &m, expr_ref_vector& conjs) { void expand_literals(ast_manager &m, expr_ref_vector& conjs) {
@ -405,19 +330,21 @@ namespace spacer {
namespace { namespace {
class implicant_picker { class implicant_picker {
model_evaluator_util &m_mev; model &m_model;
ast_manager &m; ast_manager &m;
arith_util m_arith; arith_util m_arith;
expr_ref_vector m_todo; expr_ref_vector m_todo;
expr_mark m_visited; expr_mark m_visited;
// add literal to the implicant
// applies lightweight normalization
void add_literal(expr *e, expr_ref_vector &out) { void add_literal(expr *e, expr_ref_vector &out) {
SASSERT(m.is_bool(e)); SASSERT(m.is_bool(e));
expr_ref res(m), v(m); expr_ref res(m), v(m);
m_mev.eval (e, v, false); v = m_model(e);
// the literal must have a value
SASSERT(m.is_true(v) || m.is_false(v)); SASSERT(m.is_true(v) || m.is_false(v));
res = m.is_false(v) ? m.mk_not(e) : e; res = m.is_false(v) ? m.mk_not(e) : e;
@ -425,7 +352,8 @@ namespace {
if (m.is_distinct(res)) { if (m.is_distinct(res)) {
// --(distinct a b) == (not (= a b)) // --(distinct a b) == (not (= a b))
if (to_app(res)->get_num_args() == 2) { if (to_app(res)->get_num_args() == 2) {
res = m.mk_eq (to_app(res)->get_arg(0), to_app(res)->get_arg(1)); res = m.mk_eq(to_app(res)->get_arg(0),
to_app(res)->get_arg(1));
res = m.mk_not(res); res = m.mk_not(res);
} }
} }
@ -434,38 +362,35 @@ namespace {
if (m.is_not(res, nres)) { if (m.is_not(res, nres)) {
// --(not (xor a b)) == (= a b) // --(not (xor a b)) == (= a b)
if (m.is_xor(nres, f1, f2)) if (m.is_xor(nres, f1, f2))
{ res = m.mk_eq(f1, f2); } res = m.mk_eq(f1, f2);
// -- split arithmetic inequality // -- split arithmetic inequality
else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) { else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) {
expr_ref u(m); expr_ref u(m);
u = m_arith.mk_lt(f1, f2); u = m_arith.mk_lt(f1, f2);
if (m_mev.eval (u, v, false) && m.is_true (v)) res = m_model.is_true(u) ? u : m_arith.mk_lt(f2, f1);
{ res = u; }
else
{ res = m_arith.mk_lt(f2, f1); }
} }
} }
if (!m_mev.is_true (res)) { if (!m_model.is_true(res)) {
verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n"; verbose_stream() << "Bad literal: " << res << "\n";
} }
SASSERT (m_mev.is_true (res)); SASSERT(m_model.is_true(res));
out.push_back(res); out.push_back(res);
} }
void process_app(app *a, expr_ref_vector &out) { void process_app(app *a, expr_ref_vector &out) {
if (m_visited.is_marked(a)) { return; } if (m_visited.is_marked(a)) return;
SASSERT(m.is_bool(a)); SASSERT(m.is_bool(a));
expr_ref v(m); expr_ref v(m);
m_mev.eval (a, v, false); v = m_model(a);
bool is_true = m.is_true(v); bool is_true = m.is_true(v);
if (!is_true && !m.is_false(v)) return; if (!is_true && !m.is_false(v)) return;
expr *na, *f1, *f2, *f3; expr *na, *f1, *f2, *f3;
if (m.is_true(a) || m.is_false(a)) { SASSERT(!m.is_false(a));
if (m.is_true(a)) {
// noop // noop
} }
else if (a->get_family_id() != m.get_basic_family_id()) { else if (a->get_family_id() != m.get_basic_family_id()) {
@ -479,14 +404,15 @@ namespace {
} }
else if (m.is_distinct(a)) { else if (m.is_distinct(a)) {
if (!is_true) { if (!is_true) {
f1 = qe::project_plugin::pick_equality(m, *m_mev.get_model(), a); f1 = qe::project_plugin::pick_equality(m, m_model, a);
m_todo.push_back(f1); m_todo.push_back(f1);
} }
else if (a->get_num_args() == 2) { else if (a->get_num_args() == 2) {
add_literal(a, out); add_literal(a, out);
} }
else { else {
m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), a->get_args())); m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(),
a->get_args()));
} }
} }
else if (m.is_and(a)) { else if (m.is_and(a)) {
@ -495,7 +421,7 @@ namespace {
} }
else { else {
for(expr* e : *a) { for(expr* e : *a) {
if (m_mev.is_false(e)) { if (m_model.is_false(e)) {
m_todo.push_back(e); m_todo.push_back(e);
break; break;
} }
@ -507,16 +433,18 @@ namespace {
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
else { else {
for(expr * e : *a) { for(expr * e : *a) {
if (m_mev.is_true(e)) { if (m_model.is_true(e)) {
m_todo.push_back(e); m_todo.push_back(e);
break; break;
} }
} }
} }
} }
else if (m.is_eq(a, f1, f2) || (is_true && m.is_not(a, na) && m.is_xor (na, f1, f2))) { else if (m.is_eq(a, f1, f2) ||
(is_true && m.is_not(a, na) && m.is_xor(na, f1, f2))) {
if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) { if (!m.are_equal(f1, f2) && !m.are_distinct(f1, f2)) {
if (m.is_bool(f1) && (!is_uninterp_const(f1) || !is_uninterp_const(f2))) if (m.is_bool(f1) &&
(!is_uninterp_const(f1) || !is_uninterp_const(f2)))
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
else else
add_literal(a, out); add_literal(a, out);
@ -526,19 +454,19 @@ namespace {
if (m.are_equal(f2, f3)) { if (m.are_equal(f2, f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
} }
else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { else if (m_model.is_true(f2) && m_model.is_true(f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { else if (m_model.is_false(f2) && m_model.is_false(f3)) {
m_todo.push_back(f2); m_todo.push_back(f2);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
else if (m_mev.is_true(f1)) { else if (m_model.is_true(f1)) {
m_todo.push_back(f1); m_todo.push_back(f1);
m_todo.push_back(f2); m_todo.push_back(f2);
} }
else if (m_mev.is_false(f1)) { else if (m_model.is_false(f1)) {
m_todo.push_back(f1); m_todo.push_back(f1);
m_todo.push_back(f3); m_todo.push_back(f3);
} }
@ -548,16 +476,18 @@ namespace {
} }
else if (m.is_implies(a, f1, f2)) { else if (m.is_implies(a, f1, f2)) {
if (is_true) { if (is_true) {
if (m_mev.is_true(f2)) if (m_model.is_true(f2))
m_todo.push_back(f2); m_todo.push_back(f2);
else if (m_mev.is_false(f1)) else if (m_model.is_false(f1))
m_todo.push_back(f1); m_todo.push_back(f1);
} }
else else
m_todo.append(a->get_num_args(), a->get_args()); m_todo.append(a->get_num_args(), a->get_args());
} }
else { else {
IF_VERBOSE(0, verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n"); IF_VERBOSE(0,
verbose_stream() << "Unexpected expression: "
<< mk_pp(a, m) << "\n");
UNREACHABLE(); UNREACHABLE();
} }
} }
@ -579,10 +509,10 @@ namespace {
bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) { bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) {
m_visited.reset(); m_visited.reset();
bool is_true = m_mev.is_true (in); bool is_true = m_model.is_true(in);
for(expr* e : in) { for(expr* e : in) {
if (is_true || m_mev.is_true(e)) { if (is_true || m_model.is_true(e)) {
pick_literals(e, out); pick_literals(e, out);
} }
} }
@ -592,16 +522,18 @@ namespace {
public: public:
implicant_picker (model_evaluator_util &mev) : implicant_picker(model &mdl) :
m_mev (mev), m (m_mev.get_ast_manager ()), m_arith(m), m_todo(m) {} m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {}
void operator()(expr_ref_vector &in, expr_ref_vector& out) { void operator()(expr_ref_vector &in, expr_ref_vector& out) {
model::scoped_model_completion _sc_(m_model, false);
pick_implicant(in, out); pick_implicant(in, out);
} }
}; };
} }
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, void compute_implicant_literals(model &mdl,
expr_ref_vector &formula,
expr_ref_vector &res) { expr_ref_vector &res) {
// flatten the formula and remove all trivial literals // flatten the formula and remove all trivial literals
@ -611,7 +543,7 @@ namespace {
flatten_and(formula); flatten_and(formula);
if (formula.empty()) {return;} if (formula.empty()) {return;}
implicant_picker ipick (mev); implicant_picker ipick(mdl);
ipick(formula, res); ipick(formula, res);
} }
@ -886,11 +818,12 @@ 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(); ast_manager &m = fml.get_manager();
model::scoped_model_completion _sc_(mdl, false);
expr_ref val(m); expr_ref val(m);
mev.eval (var, val, false); val = mdl(var);
TRACE("mbqi_project_verbose", TRACE("mbqi_project_verbose",
tout << "MBQI: var: " << mk_pp(var, m) << "\n" tout << "MBQI: var: " << mk_pp(var, m) << "\n"
@ -899,23 +832,22 @@ namespace {
index_term_finder finder(m, var, terms); index_term_finder finder(m, var, terms);
for_each_expr(finder, fml); for_each_expr(finder, fml);
TRACE ("mbqi_project_verbose", TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";);
tout << "terms:\n" << terms << "\n";);
for(expr * term : terms) { for(expr * term : terms) {
expr_ref tval(m); expr_ref tval(m);
mev.eval (term, tval, false); tval = mdl(term);
TRACE("mbqi_project_verbose", TRACE("mbqi_project_verbose",
tout << "term: " << mk_pp(term, m) tout << "term: " << mk_pp(term, m)
<< " tval: " << tval << " tval: " << tval << " val: " << val << "\n";);
<< " val: " << mk_pp (val, m) << "\n";);
// -- if the term does not contain an occurrence of var // -- if the term does not contain an occurrence of var
// -- and is in the same equivalence class in the model // -- and is in the same equivalence class in the model
if (tval == val && !occurs(var, term)) { if (tval == val && !occurs(var, term)) {
TRACE("mbqi_project", 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); expr_safe_replace sub(m);
sub.insert(var, term); sub.insert(var, term);
sub(fml); sub(fml);
@ -924,23 +856,23 @@ namespace {
} }
TRACE("mbqi_project", 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; 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(); ast_manager &m = fml.get_manager();
model_evaluator_util mev(m);
mev.set_model (M);
expr_ref tmp(m); expr_ref tmp(m);
model::scoped_model_completion _sc_(mdl, false);
// -- evaluate to initialize mev cache // -- evaluate to initialize mev cache
mev.eval (fml, tmp, false); tmp = mdl(fml);
tmp.reset(); tmp.reset();
unsigned j = 0; unsigned j = 0;
for(app* v : vars) for(app* v : vars)
if (!mbqi_project_var (mev, v, fml)) if (!mbqi_project_var(mdl, v, fml))
vars[j++] = v; vars[j++] = v;
vars.shrink(j); vars.shrink(j);
} }

44
src/muz/spacer/spacer_util.h
View file

@ -40,7 +40,6 @@ Revision History:
class model; class model;
class model_core; class model_core;
class model_evaluator;
namespace spacer { namespace spacer {
@ -79,33 +78,6 @@ namespace spacer {
typedef ptr_vector<func_decl> decl_vector; typedef ptr_vector<func_decl> decl_vector;
typedef obj_hashtable<func_decl> func_decl_set; 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. \brief hoist non-boolean if expressions.
*/ */
@ -121,15 +93,21 @@ namespace spacer {
* 3. use MBP for remaining array and arith variables * 3. use MBP for remaining array and arith variables
* 4. for any remaining arith variables, substitute using M * 4. for any remaining arith variables, substitute using M
*/ */
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, void qe_project (ast_manager& m, app_ref_vector& vars,
const model_ref& M, bool reduce_all_selects=false, bool native_mbp=false, expr_ref& fml, model &mdl,
bool reduce_all_selects=false,
bool native_mbp=false,
bool dont_sub=false); bool dont_sub=false);
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map); // deprecate
void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml,
model_ref& M, expr_map& map);
// TBD: sort out // TBD: sort out
void expand_literals(ast_manager &m, expr_ref_vector& conjs); void expand_literals(ast_manager &m, expr_ref_vector& conjs);
void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res); void compute_implicant_literals(model &mdl,
expr_ref_vector &formula,
expr_ref_vector &res);
void simplify_bounds (expr_ref_vector &lemmas); void simplify_bounds (expr_ref_vector &lemmas);
void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false); void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false);
@ -140,7 +118,7 @@ namespace spacer {
*/ */
void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars); 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); bool contains_selects (expr* fml, ast_manager& m);
void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m);