From a8438e081eaad149e20ee0c82f070246aee086f9 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Fri, 25 May 2018 11:18:26 -0700 Subject: [PATCH] Wired qe::mbp into spacer use option fixedpoint.spacer.native_mbp=true to use it --- src/muz/spacer/spacer_util.cpp | 87 +++++++++++++++++++++------------- 1 file changed, 55 insertions(+), 32 deletions(-) diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index b45e0de4a..3eaeb098e 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -90,33 +90,33 @@ namespace spacer { if (!m_model) { return; } 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); @@ -126,7 +126,7 @@ namespace spacer { expr_ref res(m); return eval(x, res, false) && m.is_true (res); } - + void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); @@ -172,16 +172,16 @@ namespace spacer { SASSERT(orig_size <= 1 + conjs.size()); if (i + 1 == orig_size) { // no-op. - } + } else if (orig_size <= conjs.size()) { // no-op - } + } else { SASSERT(orig_size == 1 + conjs.size()); --orig_size; --i; } - } + } else { conjs[i] = tmp; } @@ -199,7 +199,7 @@ namespace spacer { ast_manager& m; public: ite_hoister(ast_manager& m): m(m) {} - + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { if (m.is_ite(f)) { return BR_FAILED; @@ -234,7 +234,7 @@ namespace spacer { } ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} }; - + class ite_hoister_star : public rewriter_tpl { ite_hoister_cfg m_cfg; public: @@ -242,7 +242,7 @@ namespace spacer { rewriter_tpl(m, false, m_cfg), m_cfg(m, p) {} }; - + void hoist_non_bool_if(expr_ref& fml) { ast_manager& m = fml.get_manager(); scoped_no_proof _sp(m); @@ -274,7 +274,7 @@ namespace spacer { bool is_arith_expr(expr *e) const { return is_app(e) && a.get_family_id() == to_app(e)->get_family_id(); } - + bool is_offset(expr* e) const { if (a.is_numeral(e)) { return true; @@ -358,7 +358,7 @@ namespace spacer { !a.is_mul(lhs) && !a.is_mul(rhs); } - + bool test_term(expr* e) const { if (m.is_bool(e)) { return true; @@ -403,9 +403,9 @@ namespace spacer { public: 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 operator()(expr* e) { if (!m_is_dl) { return; @@ -422,7 +422,7 @@ namespace spacer { m_is_dl = test_term(a->get_arg(i)); } } - + if (!m_is_dl) { char const* msg = "non-diff: "; if (m_test_for_utvpi) { @@ -431,10 +431,10 @@ namespace spacer { IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); } } - + bool is_dl() const { return m_is_dl; } }; - + bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { test_diff_logic test(m); expr_fast_mark1 mark; @@ -443,7 +443,7 @@ namespace spacer { } return test.is_dl(); } - + bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { test_diff_logic test(m); 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, model* M, expr_ref& fml) { 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" << "(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(M.get()); + mbp.spacer(vars, *mdl, fml); +} + /* * eliminate simple equalities using qe_lite * 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, bool dont_sub) { 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); fml = mk_and(flat); } - + // uncomment for benchmarks //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 (vars, fml); rw (fml); - + TRACE ("spacer_mbp", tout << "After qe_lite:\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)); - + // sort out vars into bools, arith (int/real), and arrays for (app* v : vars) { 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); } } - + // substitute Booleans if (!bool_sub.empty()) { 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"; ); bool_sub.reset (); } - + TRACE ("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;); - + vars.reset (); - + // project arrays { 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); SASSERT (!m.is_false (fml)); } - + TRACE ("spacer_mbp", tout << "extended model:\n"; model_pp (tout, *M); tout << "Auxiliary variables of index and value sorts:\n"; tout << vars; ); - + 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) { if (conjs.empty()) { return; }