mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 12:53:38 +00:00
Code Activity

Switch spacer::qe_project to new model API

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-16 13:58:58 -07:00
parent fffc8489bf
commit 5e65b37f25
5 changed files with 54 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

2
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 ());

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

@ -265,7 +265,7 @@ 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, *mev.get_model(),
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();
@ -294,7 +294,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, *mev.get_model(),
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);
} }
@ -398,7 +398,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, *mev.get_model(),
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);
@ -1267,7 +1267,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);
@ -3617,7 +3617,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, *mev.get_model(), false, true /* force or skolemize */);
} }
@ -3685,7 +3685,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, *mev.get_model (), 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 ());

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

@ -530,7 +530,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);

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

@ -128,17 +128,11 @@ namespace spacer {
} }
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); sub(fml);
for (app * v : vars) {
expr_ref val (m);
VERIFY(mev.eval (v, val, true));
sub.insert (v, val);
}
sub (fml);
} }
void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) { void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) {
@ -161,16 +155,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 +170,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,30 +213,29 @@ 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 {
SASSERT (ari_u.is_int (v) || ari_u.is_real (v)); SASSERT (ari_u.is_int(v) || ari_u.is_real(v));
arith_vars.push_back (v); arith_vars.push_back(v);
} }
} }
// substitute Booleans // substitute Booleans
if (!bool_sub.empty()) { if (!bool_sub.empty()) {
bool_sub (fml); bool_sub(fml);
// -- bool_sub is not simplifying // -- bool_sub is not simplifying
rw (fml); rw (fml);
SASSERT (!m.is_false (fml)); SASSERT(!m.is_false (fml));
TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); TRACE("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; );
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 +244,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 +252,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 +263,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 +298,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 +324,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) {

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

@ -121,11 +121,15 @@ 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);