mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

Wired qe::mbp into spacer

Browse source 
use option fixedpoint.spacer.native_mbp=true to use it
This commit is contained in:
Arie Gurfinkel 2018-05-25 11:18:26 -07:00
parent 7e9f7d2cfe
commit a8438e081e
1 changed files with 55 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -90,33 +90,33 @@ namespace spacer {
if (!m_model) { return; } if (!m_model) { return; }
m_mev = alloc(model_evaluator, *m_model); m_mev = alloc(model_evaluator, *m_model);
} }
bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) { bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) {
m_mev->set_model_completion (model_completion); m_mev->set_model_completion (model_completion);
try { try {
m_mev->operator() (e, result); m_mev->operator() (e, result);
return true; return true;
} }
catch (model_evaluator_exception &ex) { catch (model_evaluator_exception &ex) {
(void)ex; (void)ex;
TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";); TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";);
return false; return false;
} }
} }
bool model_evaluator_util::eval(const expr_ref_vector &v, bool model_evaluator_util::eval(const expr_ref_vector &v,
expr_ref& res, bool model_completion) { expr_ref& res, bool model_completion) {
expr_ref e(m); expr_ref e(m);
e = mk_and (v); e = mk_and (v);
return eval(e, res, model_completion); return eval(e, res, model_completion);
} }
bool model_evaluator_util::is_true(const expr_ref_vector &v) { bool model_evaluator_util::is_true(const expr_ref_vector &v) {
expr_ref res(m); expr_ref res(m);
return eval (v, res, false) && m.is_true (res); return eval (v, res, false) && m.is_true (res);
} }
bool model_evaluator_util::is_false(expr *x) { bool model_evaluator_util::is_false(expr *x) {
expr_ref res(m); expr_ref res(m);
return eval(x, res, false) && m.is_false (res); return eval(x, res, false) && m.is_false (res);
@ -126,7 +126,7 @@ namespace spacer {
expr_ref res(m); expr_ref res(m);
return eval(x, res, false) && m.is_true (res); return eval(x, res, false) && m.is_true (res);
} }
void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) {
ast_manager& m = fml.get_manager(); ast_manager& m = fml.get_manager();
expr_ref_vector conjs(m); expr_ref_vector conjs(m);
@ -172,16 +172,16 @@ namespace spacer {
SASSERT(orig_size <= 1 + conjs.size()); SASSERT(orig_size <= 1 + conjs.size());
if (i + 1 == orig_size) { if (i + 1 == orig_size) {
// no-op. // no-op.
} }
else if (orig_size <= conjs.size()) { else if (orig_size <= conjs.size()) {
// no-op // no-op
} }
else { else {
SASSERT(orig_size == 1 + conjs.size()); SASSERT(orig_size == 1 + conjs.size());
--orig_size; --orig_size;
--i; --i;
} }
} }
else { else {
conjs[i] = tmp; conjs[i] = tmp;
} }
@ -199,7 +199,7 @@ namespace spacer {
ast_manager& m; ast_manager& m;
public: public:
ite_hoister(ast_manager& m): m(m) {} ite_hoister(ast_manager& m): m(m) {}
br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) {
if (m.is_ite(f)) { if (m.is_ite(f)) {
return BR_FAILED; return BR_FAILED;
@ -234,7 +234,7 @@ namespace spacer {
} }
ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {}
}; };
class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> { class ite_hoister_star : public rewriter_tpl<ite_hoister_cfg> {
ite_hoister_cfg m_cfg; ite_hoister_cfg m_cfg;
public: public:
@ -242,7 +242,7 @@ namespace spacer {
rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg), rewriter_tpl<ite_hoister_cfg>(m, false, m_cfg),
m_cfg(m, p) {} m_cfg(m, p) {}
}; };
void hoist_non_bool_if(expr_ref& fml) { void hoist_non_bool_if(expr_ref& fml) {
ast_manager& m = fml.get_manager(); ast_manager& m = fml.get_manager();
scoped_no_proof _sp(m); scoped_no_proof _sp(m);
@ -274,7 +274,7 @@ namespace spacer {
bool is_arith_expr(expr *e) const { bool is_arith_expr(expr *e) const {
return is_app(e) && a.get_family_id() == to_app(e)->get_family_id(); return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
} }
bool is_offset(expr* e) const { bool is_offset(expr* e) const {
if (a.is_numeral(e)) { if (a.is_numeral(e)) {
return true; return true;
@ -358,7 +358,7 @@ namespace spacer {
!a.is_mul(lhs) && !a.is_mul(lhs) &&
!a.is_mul(rhs); !a.is_mul(rhs);
} }
bool test_term(expr* e) const { bool test_term(expr* e) const {
if (m.is_bool(e)) { if (m.is_bool(e)) {
return true; return true;
@ -403,9 +403,9 @@ namespace spacer {
public: public:
test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {} test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {}
void test_for_utvpi() { m_test_for_utvpi = true; } void test_for_utvpi() { m_test_for_utvpi = true; }
void operator()(expr* e) { void operator()(expr* e) {
if (!m_is_dl) { if (!m_is_dl) {
return; return;
@ -422,7 +422,7 @@ namespace spacer {
m_is_dl = test_term(a->get_arg(i)); m_is_dl = test_term(a->get_arg(i));
} }
} }
if (!m_is_dl) { if (!m_is_dl) {
char const* msg = "non-diff: "; char const* msg = "non-diff: ";
if (m_test_for_utvpi) { if (m_test_for_utvpi) {
@ -431,10 +431,10 @@ namespace spacer {
IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";);
} }
} }
bool is_dl() const { return m_is_dl; } bool is_dl() const { return m_is_dl; }
}; };
bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
test_diff_logic test(m); test_diff_logic test(m);
expr_fast_mark1 mark; expr_fast_mark1 mark;
@ -443,7 +443,7 @@ namespace spacer {
} }
return test.is_dl(); return test.is_dl();
} }
bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) {
test_diff_logic test(m); test_diff_logic test(m);
test.test_for_utvpi(); test.test_for_utvpi();
@ -455,7 +455,7 @@ 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* M, expr_ref& fml) { model* M, expr_ref& fml) {
expr_safe_replace sub (m); expr_safe_replace sub (m);
@ -487,11 +487,25 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
<< "(pop)\n" << "(pop)\n"
<< "(exit)\n"; << "(exit)\n";
} }
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,
bool dont_sub) {
params_ref p;
p.set_bool("reduce_all_selects", reduce_all_selects);
p.set_bool("dont_sub", dont_sub);
qe::mbp mbp(m, p);
// TODO: deal with const
model *mdl = const_cast<model*>(M.get());
mbp.spacer(vars, *mdl, fml);
}
/* /*
* eliminate simple equalities using qe_lite * eliminate simple equalities using qe_lite
* 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 (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, const model_ref& M, bool reduce_all_selects, bool use_native_mbp,
bool dont_sub) { bool dont_sub) {
th_rewriter rw (m); th_rewriter rw (m);
@ -506,7 +520,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
flatten_and (fml, flat); flatten_and (fml, flat);
fml = mk_and(flat); fml = mk_and(flat);
} }
// uncomment for benchmarks // uncomment for benchmarks
//to_mbp_benchmark(verbose_stream(), fml, vars); //to_mbp_benchmark(verbose_stream(), fml, vars);
@ -523,7 +537,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
qe_lite qe(m, p, false); qe_lite qe(m, p, false);
qe (vars, fml); qe (vars, fml);
rw (fml); rw (fml);
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
tout << "After qe_lite:\n"; tout << "After qe_lite:\n";
tout << mk_pp (fml, m) << "\n"; tout << mk_pp (fml, m) << "\n";
@ -531,7 +545,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
SASSERT (!m.is_false (fml)); SASSERT (!m.is_false (fml));
// 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)) {
@ -545,7 +559,7 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
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);
@ -555,13 +569,13 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
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:\n";
tout << array_vars;); tout << array_vars;);
vars.reset (); vars.reset ();
// project arrays // project arrays
{ {
scoped_no_proof _sp (m); scoped_no_proof _sp (m);
@ -572,14 +586,14 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
srw (fml); srw (fml);
SASSERT (!m.is_false (fml)); SASSERT (!m.is_false (fml));
} }
TRACE ("spacer_mbp", TRACE ("spacer_mbp",
tout << "extended model:\n"; tout << "extended model:\n";
model_pp (tout, *M); model_pp (tout, *M);
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; }
} }
@ -656,6 +670,15 @@ void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars)
} }
} }
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,
bool dont_sub) {
if (use_native_mbp)
qe_project_z3(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub);
else
qe_project_spacer(m, vars, fml, M, 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)
{ {
if (conjs.empty()) { return; } if (conjs.empty()) { return; }