From 402234757e073717d339d795205c2f8b192967d2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 May 2018 13:06:47 -0700 Subject: [PATCH] updates to mbqi Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_util.cpp | 196 ++++++++++++++++----------------- src/qe/qe_mbp.cpp | 32 +++--- 2 files changed, 114 insertions(+), 114 deletions(-) diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 7b1a2a07c..90e0542fa 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); @@ -488,7 +488,7 @@ namespace spacer { flatten_and (fml, flat); fml = mk_and(flat); } - + app_ref_vector arith_vars (m); app_ref_vector array_vars (m); array_util arr_u (m); @@ -497,19 +497,19 @@ namespace spacer { expr_ref bval (m); while (true) { - params_ref p; - 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"; + params_ref p; + 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"; tout << "Vars:\n" << 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)) { @@ -523,7 +523,7 @@ namespace spacer { arith_vars.push_back (v); } } - + // substitute Booleans if (!bool_sub.empty()) { bool_sub (fml); @@ -533,13 +533,13 @@ namespace spacer { 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); @@ -550,14 +550,14 @@ namespace spacer { 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; } } @@ -572,21 +572,21 @@ namespace spacer { // tout << "After second qelite: " << // mk_pp (fml, m) << "\n";); - if (use_native_mbp) { - qe::mbp mbp (m); - expr_ref_vector fmls(m); - flatten_and (fml, fmls); + if (use_native_mbp) { + qe::mbp mbp (m); + expr_ref_vector fmls(m); + flatten_and (fml, fmls); - mbp (true, arith_vars, *M.get (), fmls); - fml = mk_and (fmls); - SASSERT (arith_vars.empty ()); - } else { + mbp (true, arith_vars, *M.get (), fmls); + fml = mk_and (fmls); + SASSERT (arith_vars.empty ()); + } else { scoped_no_proof _sp (m); spacer_qe::arith_project (*M.get (), arith_vars, fml); } TRACE ("spacer_mbp", - tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n"; + tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n"; tout << "Remaining arith vars:\n" << arith_vars << "\n";); SASSERT (!m.is_false (fml)); } @@ -697,7 +697,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) } namespace { - class implicant_picker { +class implicant_picker { model_evaluator_util &m_mev; ast_manager &m; arith_util m_arith; @@ -747,37 +747,37 @@ namespace { out.push_back (res); } - void process_app(app *a, expr_ref_vector &out) - { - if (m_visited.is_marked(a)) { return; } + void process_app(app *a, expr_ref_vector &out) + { + if (m_visited.is_marked(a)) { return; } SASSERT (m.is_bool (a)); expr_ref v(m); m_mev.eval (a, v, false); - if (!m.is_true(v) && !m.is_false(v)) { return; } + if (!m.is_true(v) && !m.is_false(v)) { return; } expr *na, *f1, *f2, *f3; if (a->get_family_id() != m.get_basic_family_id()) - { add_literal(a, out); } + { add_literal(a, out); } else if (is_uninterp_const(a)) - { add_literal(a, out); } + { add_literal(a, out); } else if (m.is_not(a, na) && m.is_not(na, na)) - { m_todo.push_back(na); } + { m_todo.push_back(na); } else if (m.is_not(a, na)) - { m_todo.push_back(na); } + { m_todo.push_back(na); } else if (m.is_distinct(a)) { if (m.is_false(v)) m_todo.push_back (qe::project_plugin::pick_equality(m, *m_mev.get_model(), a)); else if (a->get_num_args() == 2) - { add_literal(a, out); } + { add_literal(a, out); } else 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)) { if (m.is_true(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } + { m_todo.append(a->get_num_args(), a->get_args()); } else if (m.is_false(v)) { for (unsigned i = 0, sz = a->get_num_args (); i < sz; ++i) { if (m_mev.is_false(a->get_arg(i))) { @@ -786,9 +786,9 @@ namespace { } } } - } else if (m.is_or(a)) { + } else if (m.is_or(a)) { if (m.is_false(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } + { m_todo.append(a->get_num_args(), a->get_args()); } else if (m.is_true(v)) { for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i) { if (m_mev.is_true(a->get_arg(i))) { @@ -797,39 +797,39 @@ namespace { } } } - } else if (m.is_iff(a, f1, f2) || m.is_eq(a, f1, f2) || - (m.is_true(v) && m.is_not(a, na) && m.is_xor (na, f1, f2))) { + } else if (m.is_iff(a, f1, f2) || m.is_eq(a, f1, f2) || + (m.is_true(v) && m.is_not(a, na) && m.is_xor (na, 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))) - { m_todo.append(a->get_num_args(), a->get_args()); } - else - { add_literal(a, out); } - } - } else if (m.is_ite(a, f1, f2, f3)) { - if (m.are_equal(f2, f3)) { m_todo.push_back(f2); } - else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { - m_todo.push_back(f2); - m_todo.push_back(f3); - } else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { - m_todo.push_back(f2); - m_todo.push_back(f3); - } else if (m_mev.is_true(f1)) { - m_todo.push_back(f1); - m_todo.push_back(f2); - } else if (m_mev.is_false(f1)) { - m_todo.push_back(f1); - m_todo.push_back(f3); - } - } else if (m.is_xor(a, f1, f2)) { m_todo.append(a->get_num_args(), a->get_args()); } + else + { add_literal(a, out); } + } + } else if (m.is_ite(a, f1, f2, f3)) { + if (m.are_equal(f2, f3)) { m_todo.push_back(f2); } + else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { + m_todo.push_back(f2); + m_todo.push_back(f3); + } else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { + m_todo.push_back(f2); + m_todo.push_back(f3); + } else if (m_mev.is_true(f1)) { + m_todo.push_back(f1); + m_todo.push_back(f2); + } else if (m_mev.is_false(f1)) { + m_todo.push_back(f1); + m_todo.push_back(f3); + } + } else if (m.is_xor(a, f1, f2)) + { m_todo.append(a->get_num_args(), a->get_args()); } else if (m.is_implies(a, f1, f2)) { if (m.is_true (v)) { - if (m_mev.is_true(f2)) { m_todo.push_back(f2); } - else if (m_mev.is_false(f1)) { m_todo.push_back(f1); } + if (m_mev.is_true(f2)) { m_todo.push_back(f2); } + else if (m_mev.is_false(f1)) { m_todo.push_back(f1); } } else if (m.is_false(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } - } else if (m.is_true(a) || m.is_false(a)) { /* nothing */ } + { m_todo.append(a->get_num_args(), a->get_args()); } + } else if (m.is_true(a) || m.is_false(a)) { /* nothing */ } else { verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n"; @@ -837,10 +837,10 @@ namespace { } } - void pick_literals(expr *e, expr_ref_vector &out) - { + void pick_literals(expr *e, expr_ref_vector &out) + { SASSERT(m_todo.empty()); - if (m_visited.is_marked(e)) { return; } + if (m_visited.is_marked(e)) { return; } SASSERT(is_app(e)); m_todo.push_back(e); @@ -852,8 +852,8 @@ namespace { } while (!m_todo.empty()); } - 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(); expr_ref e(m); e = mk_and (in); @@ -861,7 +861,7 @@ namespace { for (unsigned i = 0, sz = in.size (); i < sz; ++i) { if (is_true || m_mev.is_true(in.get(i))) - { pick_literals(in.get(i), out); } + { pick_literals(in.get(i), out); } } m_visited.reset (); @@ -875,7 +875,7 @@ namespace { void operator() (expr_ref_vector &in, expr_ref_vector& out) {pick_implicant (in, out);} }; -} + } void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res) @@ -1178,9 +1178,9 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { expr *e1, *e2; if (m_array.is_select (n) && n->get_arg (1) != m_var) { m_res.push_back (n->get_arg (1)); - } else if (m.is_eq(n, e1, e2)) { - if (e1 == m_var) { m_res.push_back(e2); } - else if (e2 == m_var) { m_res.push_back(e1); } + } else if (m.is_eq(n, e1, e2)) { + if (e1 == m_var) { m_res.push_back(e2); } + else if (e2 == m_var) { m_res.push_back(e1); } } } }; @@ -1206,7 +1206,7 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { tout << i << ": " << mk_pp (terms.get (i), m) << "\n"; ); - for (unsigned i = 0, e = terms.size(); i < e; ++i) { + for (unsigned i = 0, e = terms.size(); i < e; ++i) { expr* term = terms.get (i); expr_ref tval (m); mev.eval (term, tval, false); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index a6bdbd1dc..f90c32342 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -125,13 +125,13 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) { class mbp::impl { - ast_manager& m; + ast_manager& m; params_ref m_params; - th_rewriter m_rw; + th_rewriter m_rw; ptr_vector m_plugins; - expr_mark m_visited; - expr_mark m_bool_visited; - + expr_mark m_visited; + expr_mark m_bool_visited; + // parameters bool m_reduce_all_selects; bool m_native_mbp; @@ -280,33 +280,33 @@ class mbp::impl { } else { vars[j++] = var; + } } - } if (j == vars.size()) { return; } vars.shrink(j); - j = 0; - for (unsigned i = 0; i < fmls.size(); ++i) { + j = 0; + for (unsigned i = 0; i < fmls.size(); ++i) { expr* fml = fmls[i].get(); sub(fml, val); - m_rw(val); - if (!m.is_true(val)) { + m_rw(val); + if (!m.is_true(val)) { TRACE("qe", tout << mk_pp(fml, m) << " -> " << val << "\n";); fmls[j++] = val; - } - } + } + } fmls.shrink(j); - } + } void subst_vars(model_evaluator& eval, app_ref_vector const& vars, expr_ref& fml) { expr_safe_replace sub (m); for (app * v : vars) { sub.insert(v, eval(v)); - } + } sub(fml); - } + } struct index_term_finder { ast_manager& m; @@ -731,7 +731,7 @@ mbp::mbp(ast_manager& m, params_ref const& p) { mbp::~mbp() { dealloc(m_impl); } - + void mbp::updt_params(params_ref const& p) { m_impl->updt_params(p); }