From 7931bd1dfca80c92f27aa7351f1b8c1d9581764f 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/ast/ast_util.cpp | 7 + src/ast/ast_util.h | 2 + src/muz/spacer/spacer_util.cpp | 232 ++++++++++++------------ src/qe/qe_arith.cpp | 5 +- src/qe/qe_mbp.cpp | 313 ++++++++++++++++++++++++++++----- src/qe/qe_mbp.h | 16 +- 6 files changed, 402 insertions(+), 173 deletions(-) diff --git a/src/ast/ast_util.cpp b/src/ast/ast_util.cpp index 92a539d88..e2783051a 100644 --- a/src/ast/ast_util.cpp +++ b/src/ast/ast_util.cpp @@ -307,6 +307,13 @@ void flatten_and(expr* fml, expr_ref_vector& result) { flatten_and(result); } +void flatten_and(expr_ref& fml) { + expr_ref_vector fmls(fml.get_manager()); + fmls.push_back(fml); + flatten_and(fmls); + fml = mk_and(fmls); +} + void flatten_or(expr_ref_vector& result) { ast_manager& m = result.get_manager(); expr* e1, *e2, *e3; diff --git a/src/ast/ast_util.h b/src/ast/ast_util.h index 446854f5e..12c11c141 100644 --- a/src/ast/ast_util.h +++ b/src/ast/ast_util.h @@ -150,6 +150,8 @@ expr_ref mk_distinct(expr_ref_vector const& args); void flatten_and(expr_ref_vector& result); +void flatten_and(expr_ref& fml); + void flatten_and(expr* fml, expr_ref_vector& result); void flatten_or(expr_ref_vector& result); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index b4e5e7710..030f2a386 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -479,9 +479,8 @@ namespace spacer { th_rewriter rw (m); TRACE ("spacer_mbp", tout << "Before projection:\n"; - tout << mk_pp (fml, m) << "\n"; - tout << "Vars:\n"; - for (app* v : vars) tout << mk_pp(v, m) << "\n";); + tout << fml << "\n"; + tout << "Vars:\n" << vars;); { // Ensure that top-level AND of fml is flat @@ -498,47 +497,40 @@ 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"; - tout << "Vars:\n"; - for (unsigned i = 0; i < vars.size(); ++i) { - tout << mk_pp(vars.get (i), 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)); - bool has_bool_vars = false; // sort out vars into bools, arith (int/real), and arrays - for (unsigned i = 0; i < vars.size (); i++) { - if (m.is_bool (vars.get (i))) { + for (app* v : vars) { + if (m.is_bool (v)) { // obtain the interpretation of the ith var using model completion - VERIFY (M->eval (vars.get (i), bval, true)); - bool_sub.insert (vars.get (i), bval); - has_bool_vars = true; - } else if (arr_u.is_array(vars.get(i))) { - array_vars.push_back (vars.get (i)); + VERIFY (M->eval (v, bval, true)); + bool_sub.insert (v, bval); + } else if (arr_u.is_array(v)) { + array_vars.push_back (v); } else { - SASSERT (ari_u.is_int (vars.get (i)) || ari_u.is_real (vars.get (i))); - arith_vars.push_back (vars.get (i)); + SASSERT (ari_u.is_int (v) || ari_u.is_real (v)); + arith_vars.push_back (v); } } // substitute Booleans - if (has_bool_vars) { + if (!bool_sub.empty()) { bool_sub (fml); // -- bool_sub is not simplifying rw (fml); SASSERT (!m.is_false (fml)); - TRACE ("spacer_mbp", - tout << "Projected Booleans:\n" << mk_pp (fml, m) << "\n"; - ); + TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); bool_sub.reset (); } @@ -571,40 +563,31 @@ namespace spacer { // project reals and ints if (!arith_vars.empty ()) { - TRACE ("spacer_mbp", - tout << "Arith vars:\n"; - for (unsigned i = 0; i < arith_vars.size (); ++i) { - tout << mk_pp (arith_vars.get (i), m) << "\n"; - } - ); - + 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) { - 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 { + + 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 { scoped_no_proof _sp (m); qe::arith_project (*M.get (), arith_vars, fml); } - + TRACE ("spacer_mbp", - tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n"; - tout << "Remaining arith vars:\n"; - for (unsigned i = 0; i < arith_vars.size (); i++) { - tout << mk_pp (arith_vars.get (i), 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)); } @@ -632,8 +615,9 @@ namespace spacer { ); vars.reset (); - if (dont_sub && !arith_vars.empty ()) - { vars.append(arith_vars); } + if (dont_sub && !arith_vars.empty ()) { + vars.append(arith_vars); + } } @@ -713,15 +697,15 @@ 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; - + expr_ref_vector m_todo; expr_mark m_visited; - + void add_literal (expr *e, expr_ref_vector &out) { SASSERT (m.is_bool (e)); @@ -763,37 +747,37 @@ class implicant_picker { 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))) { @@ -802,9 +786,9 @@ class implicant_picker { } } } - } 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))) { @@ -813,52 +797,52 @@ class implicant_picker { } } } - } 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()); } + { m_todo.append(a->get_num_args(), a->get_args()); } else - { add_literal(a, out); } + { 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.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); + 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_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"; UNREACHABLE(); } } - - 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); do { app *a = to_app(m_todo.back()); @@ -867,31 +851,31 @@ class implicant_picker { m_visited.mark(a, true); } 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); bool is_true = m_mev.is_true (e); - + 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 (); return is_true; } - + public: implicant_picker (model_evaluator_util &mev) : m_mev (mev), m (m_mev.get_ast_manager ()), m_arith(m), m_todo(m) {} - + 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) @@ -1144,6 +1128,7 @@ struct adhoc_rewriter_rpp : public default_rewriter_cfg { } }; + mk_epp::mk_epp(ast *t, ast_manager &m, unsigned indent, unsigned num_vars, char const * var_prefix) : mk_pp (t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) { @@ -1189,14 +1174,13 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array (m), m_var (v, m), m_res (res) {} void operator() (var *n) {} void operator() (quantifier *n) {} - void operator() (app *n) - { + void operator() (app *n) { 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); } } } }; @@ -1204,29 +1188,29 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) { ast_manager &m = fml.get_manager (); - + expr_ref val(m); mev.eval (var, val, false); - + TRACE ("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp (var, m) << "\n" << "fml: " << mk_pp (fml, m) << "\n";); expr_ref_vector terms (m); index_term_finder finder (m, var, terms); for_each_expr (finder, fml); - - + + TRACE ("mbqi_project_verbose", tout << "terms:\n"; for (unsigned i = 0, e = terms.size (); i < e; ++i) 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); - + TRACE ("mbqi_project_verbose", tout << "term: " << mk_pp (term, m) << " tval: " << mk_pp (tval, m) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 6ea4118a0..969d22a81 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -352,10 +352,7 @@ namespace qe { real_vars.push_back(tids.find(v)); } else { - if (i != j) { - vars[j] = v; - } - ++j; + vars[j++] = v; } } vars.resize(j); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 432569ff9..0b4574951 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -18,17 +18,20 @@ Revision History: --*/ +#include "ast/rewriter/expr_safe_replace.h" +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/occurs.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/expr_functors.h" +#include "ast/for_each_expr.h" +#include "ast/scoped_proof.h" #include "qe/qe_mbp.h" #include "qe/qe_arith.h" #include "qe/qe_arrays.h" #include "qe/qe_datatypes.h" -#include "ast/rewriter/expr_safe_replace.h" -#include "ast/ast_pp.h" -#include "ast/ast_util.h" -#include "ast/rewriter/th_rewriter.h" -#include "model/model_v2_pp.h" -#include "ast/expr_functors.h" -#include "ast/for_each_expr.h" +#include "qe/qe_lite.h" +#include "model/model_pp.h" #include "model/model_evaluator.h" @@ -122,11 +125,17 @@ void project_plugin::push_back(expr_ref_vector& lits, expr* e) { class mbp::impl { - ast_manager& m; - th_rewriter m_rw; + ast_manager& m; + params_ref m_params; + 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; + bool m_dont_sub; void add_plugin(project_plugin* p) { family_id fid = p->get_family_id(); @@ -258,42 +267,122 @@ class mbp::impl { return found_bool; } - void project_bools(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + void project_bools(model& mdl, app_ref_vector& vars, expr_ref_vector& fmls) { expr_safe_replace sub(m); expr_ref val(m); + model_evaluator eval(mdl, m_params); + eval.set_model_completion(true); unsigned j = 0; for (unsigned i = 0; i < vars.size(); ++i) { app* var = vars[i].get(); if (m.is_bool(var)) { - VERIFY(model.eval(var, val)); - sub.insert(var, val); + sub.insert(var, eval(var)); } else { - if (j != i) { - vars[j] = vars[i].get(); - } - ++j; + vars[j++] = var; } } - if (j != vars.size()) { - vars.resize(j); - j = 0; - for (unsigned i = 0; i < fmls.size(); ++i) { - sub(fmls[i].get(), val); - m_rw(val); - if (!m.is_true(val)) { - TRACE("qe", tout << mk_pp(fmls[i].get(), m) << " -> " << val << "\n";); - fmls[i] = val; - if (j != i) { - fmls[j] = fmls[i].get(); - } - ++j; - } - } - if (j != fmls.size()) { - fmls.resize(j); + if (j == vars.size()) { + return; + } + vars.shrink(j); + 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)) { + 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; + array_util m_array; + app_ref m_var; + expr_ref_vector& m_res; + + index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res): + m(mgr), m_array (m), m_var (v, m), m_res (res) {} + + void operator() (var *n) {} + void operator() (quantifier *n) {} + void operator() (app *n) { + expr *e1, *e2; + if (m_array.is_select (n)) { + for (unsigned i = 1; i < n->get_num_args(); ++i) { + expr * arg = n->get_arg(i); + if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) + m_res.push_back (arg); + } + } + 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); + } + } + }; + + bool project_var (model_evaluator& eval, app* var, expr_ref& fml) { + expr_ref val = eval(var); + + TRACE ("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp (var, m) << "\n" << "fml: " << fml << "\n";); + expr_ref_vector terms (m); + index_term_finder finder (m, var, terms); + for_each_expr (finder, fml); + + TRACE ("mbqi_project_verbose", tout << "terms:\n" << terms;); + + for (expr * term : terms) { + expr_ref tval = eval(term); + + TRACE ("mbqi_project_verbose", tout << "term: " << mk_pp (term, m) << " tval: " << tval << " val: " << val << "\n";); + + // -- if the term does not contain an occurrence of var + // -- and is in the same equivalence class in the model + if (tval == val && !occurs (var, term)) { + TRACE ("mbqi_project", + tout << "MBQI: replacing " << mk_pp (var, m) << " with " << mk_pp (term, m) << "\n";); + expr_safe_replace sub(m); + sub.insert (var, term); + sub (fml); + return true; + } + } + + TRACE ("mbqi_project", + tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << fml << "\n";); + + return false; + } + + void project_vars (model &M, app_ref_vector &vars, expr_ref &fml) { + model_evaluator eval(M); + eval.set_model_completion(false); + // -- evaluate to initialize eval cache + (void) eval (fml); + unsigned j = 0; + for (unsigned i = 0; i < vars.size (); ++i) { + app* v = vars.get(i); + if (!project_var (eval, v, fml)) { + vars[j++] = v; + } + } + vars.shrink(j); } public: @@ -426,7 +515,7 @@ public: m_bool_visited.reset(); } - impl(ast_manager& m):m(m), m_rw(m) { + impl(ast_manager& m, params_ref const& p):m(m), m_params(p), m_rw(m) { add_plugin(alloc(arith_project_plugin, m)); add_plugin(alloc(datatype_project_plugin, m)); add_plugin(alloc(array_project_plugin, m)); @@ -436,13 +525,20 @@ public: std::for_each(m_plugins.begin(), m_plugins.end(), delete_proc()); } + void updt_params(params_ref const& p) { + m_params.append(p); + m_reduce_all_selects = m_params.get_bool("reduce_all_selects", false); + m_native_mbp = m_params.get_bool("native_mbp", false); + m_dont_sub = m_params.get_bool("dont_sub", false); + } + void preprocess_solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { extract_literals(model, fmls); bool change = true; while (change && !vars.empty()) { change = solve(model, vars, fmls); - for (unsigned i = 0; i < m_plugins.size(); ++i) { - if (m_plugins[i] && m_plugins[i]->solve(model, vars, fmls)) { + for (auto* p : m_plugins) { + if (p && p->solve(model, vars, fmls)) { change = true; } } @@ -451,8 +547,8 @@ public: bool validate_model(model& model, expr_ref_vector const& fmls) { expr_ref val(m); - for (unsigned i = 0; i < fmls.size(); ++i) { - VERIFY(model.eval(fmls[i], val) && m.is_true(val)); + for (expr * f : fmls) { + VERIFY(model.eval(f, val) && m.is_true(val)); } return true; } @@ -469,8 +565,7 @@ public: while (progress && !vars.empty() && !fmls.empty()) { app_ref_vector new_vars(m); progress = false; - for (unsigned i = 0; i < m_plugins.size(); ++i) { - project_plugin* p = m_plugins[i]; + for (project_plugin * p : m_plugins) { if (p) { (*p)(model, vars, fmls); } @@ -517,28 +612,158 @@ public: TRACE("qe", tout << vars << " " << fmls << "\n";); } + void do_qe_lite(app_ref_vector& vars, expr_ref& fml) { + qe_lite qe(m, m_params, false); + qe (vars, fml); + m_rw (fml); + TRACE ("qe", tout << "After qe_lite:\n" << fml << "\n" << "Vars:\n" << vars;); + SASSERT (!m.is_false (fml)); + } + + void do_qe_bool(model& mdl, app_ref_vector& vars, expr_ref& fml) { + expr_ref_vector fmls(m); + fmls.push_back(fml); + project_bools(mdl, vars, fmls); + fml = mk_and(fmls); + } + + void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) { + TRACE ("qe", tout << "Before projection:\n" << fml << "\n" << "Vars:\n" << vars;); + + model_evaluator eval(mdl, m_params); + eval.set_model_completion(true); + app_ref_vector arith_vars (m); + app_ref_vector array_vars (m); + array_util arr_u (m); + arith_util ari_u (m); + + flatten_and(fml); + + do_qe_lite(vars, fml); + + while (!vars.empty()) { + + do_qe_bool(mdl, vars, fml); + + // sort out vars into bools, arith (int/real), and arrays + for (app* v : vars) { + if (arr_u.is_array(v)) { + array_vars.push_back (v); + } + else if (ari_u.is_int (v) || ari_u.is_real (v)) { + arith_vars.push_back (v); + } + else { + NOT_IMPLEMENTED_YET(); + } + } + + TRACE ("qe", tout << "Array vars:\n" << array_vars;); + + vars.reset (); + + // project arrays + if (!array_vars.empty()) { + NOT_IMPLEMENTED_YET(); + // qe::array_project (mdl, array_vars, fml, vars, m_reduce_all_selects); + SASSERT (array_vars.empty ()); + m_rw (fml); + SASSERT (!m.is_false (fml)); + } + + TRACE ("qe", + tout << "extended model:\n"; + model_pp (tout, mdl); + tout << "Auxiliary variables of index and value sorts:\n"; + tout << vars; + ); + + } + // project reals and ints + if (!arith_vars.empty ()) { + TRACE ("qe", tout << "Arith vars:\n" << arith_vars;); + + if (m_native_mbp) { + expr_ref_vector fmls(m); + flatten_and (fml, fmls); + + (*this)(true, arith_vars, mdl, fmls); + fml = mk_and (fmls); + SASSERT (arith_vars.empty ()); + } + else { + NOT_IMPLEMENTED_YET(); + // qe::arith_project (mdl, arith_vars, fml); + } + + TRACE ("qe", + tout << "Projected arith vars:\n" << fml << "\n"; + tout << "Remaining arith vars:\n" << arith_vars << "\n";); + SASSERT (!m.is_false (fml)); + } + + if (!arith_vars.empty ()) { + project_vars (mdl, arith_vars, fml); + } + + // substitute any remaining arith vars + if (!m_dont_sub && !arith_vars.empty ()) { + subst_vars (eval, arith_vars, fml); + TRACE ("qe", tout << "After substituting remaining arith vars:\n" << fml << "\n";); + // an extra round of simplification because subst_vars is not simplifying + m_rw(fml); + arith_vars.reset(); + } + + SASSERT(eval.is_true(fml)); + + vars.reset (); + vars.append(arith_vars); + } + }; -mbp::mbp(ast_manager& m) { - m_impl = alloc(impl, m); +mbp::mbp(ast_manager& m, params_ref const& p) { + scoped_no_proof _sp (m); + m_impl = alloc(impl, m, p); } mbp::~mbp() { dealloc(m_impl); } + +void mbp::updt_params(params_ref const& p) { + m_impl->updt_params(p); +} + +void mbp::get_param_descrs(param_descrs & r) { + r.insert("reduce_all_selects", CPK_BOOL, "(default: false) reduce selects"); + r.insert("native_mbp", CPK_BOOL, "(default: false) switch between native and spacer tailored mbp"); + r.insert("dont_sub", CPK_BOOL, "(default: false) disable substitution of values for free variables"); +} void mbp::operator()(bool force_elim, app_ref_vector& vars, model& mdl, expr_ref_vector& fmls) { + scoped_no_proof _sp (fmls.get_manager()); (*m_impl)(force_elim, vars, mdl, fmls); } +void mbp::spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) { + scoped_no_proof _sp (fml.get_manager()); + m_impl->spacer(vars, mdl, fml); +} + void mbp::solve(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { + scoped_no_proof _sp (fmls.get_manager()); m_impl->preprocess_solve(model, vars, fmls); } void mbp::extract_literals(model& model, expr_ref_vector& lits) { + scoped_no_proof _sp (lits.get_manager()); m_impl->extract_literals(model, lits); } + opt::inf_eps mbp::maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { + scoped_no_proof _sp (fmls.get_manager()); return m_impl->maximize(fmls, mdl, t, ge, gt); } diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index d1695843c..12b03791a 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -52,9 +52,13 @@ namespace qe { class impl; impl * m_impl; public: - mbp(ast_manager& m); + mbp(ast_manager& m, params_ref const& p = params_ref()); ~mbp(); + + void updt_params(params_ref const& p); + + static void get_param_descrs(param_descrs & r); /** \brief @@ -80,6 +84,16 @@ namespace qe { Maximize objective t under current model for constraints in fmls. */ opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt); + + /** + \brief + Apply spacer friendly MBP. + Use parameters to control behavior. + - reduce_all_selects (false) + - native_mbp (false) - to be deprecated + - dont_sub (false) + */ + void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml); }; }