From eee96ec312ee6dee685051cf2ca216cf28c060b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 15 Feb 2025 14:11:20 -0800 Subject: [PATCH] bug fixes and cleanup in projection functions spacer would drop variables of sorts not handled by main loop. - projection with witness needs to disable qel style preprocessing to ensure witnesses are returned. - add euf plugin to handle uninterpreted sorts (and then uninterpreted functions) --- genaisrc/.gitignore | 4 ++ src/muz/spacer/spacer_util.cpp | 79 +++++++++++++++------------- src/qe/mbp/CMakeLists.txt | 1 + src/qe/mbp/mbp_basic_tg.h | 2 +- src/qe/mbp/mbp_euf.cpp | 85 ++++++++++++++++++++++++++++++ src/qe/mbp/mbp_euf.h | 30 +++++++++++ src/qe/mbp/mbp_plugin.cpp | 2 +- src/qe/mbp/mbp_plugin.h | 7 ++- src/qe/mbp/mbp_term_graph.cpp | 3 +- src/qe/mbp/mbp_term_graph.h | 32 ++++++------ src/qe/mbp/mbp_tg_plugins.h | 16 +++--- src/qe/qe_mbp.cpp | 96 +++++++++++++++++++--------------- 12 files changed, 249 insertions(+), 108 deletions(-) create mode 100644 genaisrc/.gitignore create mode 100644 src/qe/mbp/mbp_euf.cpp create mode 100644 src/qe/mbp/mbp_euf.h diff --git a/genaisrc/.gitignore b/genaisrc/.gitignore new file mode 100644 index 000000000..6641d96c0 --- /dev/null +++ b/genaisrc/.gitignore @@ -0,0 +1,4 @@ +# auto-generated +genaiscript.d.ts +tsconfig.json +jsconfig.json \ No newline at end of file diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 3959bd655..87865fac4 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -152,6 +152,7 @@ void qe_project_z3(ast_manager &m, app_ref_vector &vars, expr_ref &fml, params_ref p; p.set_bool("reduce_all_selects", reduce_all_selects); p.set_bool("dont_sub", dont_sub); + TRACE("qe", tout << "qe-project-z3\n"); qe::mbproj mbp(m, p); mbp.spacer(vars, mdl, fml); @@ -167,8 +168,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, bool dont_sub) { th_rewriter rw(m); TRACE("spacer_mbp", tout << "Before projection:\n"; tout << fml << "\n"; - tout << "Vars:\n" - << vars;); + tout << "Vars:" << vars << "\n";); { // Ensure that top-level AND of fml is flat @@ -182,6 +182,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, app_ref_vector arith_vars(m); app_ref_vector array_vars(m); + app_ref_vector other_vars(m); array_util arr_u(m); arith_util ari_u(m); expr_safe_replace bool_sub(m); @@ -194,8 +195,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, rw(fml); TRACE("spacer_mbp", tout << "After qe_lite:\n"; - tout << mk_pp(fml, m) << "\n"; tout << "Vars:\n" - << vars;); + tout << mk_pp(fml, m) << "\nVars:" << vars << "\n";); SASSERT(!m.is_false(fml)); @@ -206,12 +206,13 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, // using model completion model::scoped_model_completion _sc_(mdl, true); bool_sub.insert(v, mdl(v)); - } else if (arr_u.is_array(v)) { - array_vars.push_back(v); - } else { - SASSERT(ari_u.is_int(v) || ari_u.is_real(v)); - arith_vars.push_back(v); } + else 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 + other_vars.push_back(v); } // substitute Booleans @@ -220,8 +221,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, // -- bool_sub is not simplifying rw(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(); } @@ -230,7 +230,7 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, vars.reset(); // project arrays - { + if (!array_vars.empty()) { scoped_no_proof _sp(m); // -- local rewriter that is aware of current proof mode th_rewriter srw(m); @@ -243,14 +243,15 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, TRACE("spacer_mbp", tout << "extended model:\n"; model_pp(tout, mdl); tout << "Auxiliary variables of index and value sorts:\n"; - tout << vars;); + tout << vars << "\n";); - if (vars.empty()) { break; } + if (vars.empty()) + break; } // project reals and ints if (!arith_vars.empty()) { - TRACE("spacer_mbp", tout << "Arith vars:\n" << arith_vars;); + TRACE("spacer_mbp", tout << "Arith vars:" << arith_vars << "\n";); if (use_native_mbp) { qe::mbproj mbp(m); @@ -260,19 +261,19 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, mbp(true, arith_vars, mdl, fmls); fml = mk_and(fmls); SASSERT(arith_vars.empty()); - } else { + } + else { scoped_no_proof _sp(m); spacer_qe::arith_project(mdl, arith_vars, fml); } - TRACE("spacer_mbp", tout << "Projected arith vars:\n" - << fml << "\n"; - tout << "Remaining arith vars:\n" - << arith_vars << "\n";); + TRACE("spacer_mbp", tout << "Projected arith vars: "<< fml << "\n"; + tout << "Remaining arith vars:" << arith_vars << "\n";); SASSERT(!m.is_false(fml)); } - if (!arith_vars.empty()) { mbqi_project(mdl, arith_vars, fml); } + if (!arith_vars.empty()) + mbqi_project(mdl, arith_vars, fml); // substitute any remaining arith vars if (!dont_sub && !arith_vars.empty()) { @@ -289,26 +290,30 @@ void qe_project_spacer(ast_manager &m, app_ref_vector &vars, expr_ref &fml, SASSERT(mev.is_true(fml));); vars.reset(); - if (dont_sub && !arith_vars.empty()) { vars.append(arith_vars); } + vars.append(other_vars); + if (dont_sub && !arith_vars.empty()) + vars.append(arith_vars); + TRACE("qe", tout << "after projection: " << fml << ": " << vars << "\n"); } static expr *apply_accessor(ast_manager &m, ptr_vector const &acc, unsigned j, func_decl *f, expr *c) { - if (is_app(c) && to_app(c)->get_decl() == f) { + if (is_app(c) && to_app(c)->get_decl() == f) return to_app(c)->get_arg(j); - } else { + else return m.mk_app(acc[j], c); - } } void qe_project(ast_manager &m, app_ref_vector &vars, expr_ref &fml, model &mdl, bool reduce_all_selects, bool use_native_mbp, bool dont_sub) { - if (use_native_mbp) - qe_project_z3(m, vars, fml, mdl, reduce_all_selects, use_native_mbp, - dont_sub); - else + if (!use_native_mbp) qe_project_spacer(m, vars, fml, mdl, reduce_all_selects, use_native_mbp, dont_sub); + + if (!vars.empty()) + qe_project_z3(m, vars, fml, mdl, reduce_all_selects, use_native_mbp, + dont_sub); + } void expand_literals(ast_manager &m, expr_ref_vector &conjs) { @@ -329,12 +334,14 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) { conjs[i] = arith.mk_le(e1, e2); if (i + 1 == conjs.size()) { conjs.push_back(arith.mk_ge(e1, e2)); - } else { + } + else { conjs.push_back(conjs[i + 1].get()); conjs[i + 1] = arith.mk_ge(e1, e2); } ++i; - } else if ((m.is_eq(e, c, val) && is_app(val) && + } + else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))) { @@ -346,8 +353,9 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) { conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j))); } - } else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || - (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { + } + else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || + (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { rational two(2); for (unsigned j = 0; j < bv_size; ++j) { parameter p(j); @@ -355,11 +363,10 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) { bv.mk_extract(j, j, c)); if ((r % two).is_zero()) { e = m.mk_not(e); } r = div(r, two); - if (j == 0) { + if (j == 0) conjs[i] = e; - } else { + else conjs.push_back(e); - } } } } diff --git a/src/qe/mbp/CMakeLists.txt b/src/qe/mbp/CMakeLists.txt index a5c7e7702..26b928f2b 100644 --- a/src/qe/mbp/CMakeLists.txt +++ b/src/qe/mbp/CMakeLists.txt @@ -6,6 +6,7 @@ z3_add_component(mbp mbp_basic_tg.cpp mbp_datatypes.cpp mbp_dt_tg.cpp + mbp_euf.cpp mbp_qel.cpp mbp_qel_util.cpp mbp_plugin.cpp diff --git a/src/qe/mbp/mbp_basic_tg.h b/src/qe/mbp/mbp_basic_tg.h index af7c624c0..28af8354a 100644 --- a/src/qe/mbp/mbp_basic_tg.h +++ b/src/qe/mbp/mbp_basic_tg.h @@ -27,7 +27,7 @@ class mbp_basic_tg : public mbp_tg_plugin { struct impl; impl *m_impl; - public: +public: mbp_basic_tg(ast_manager &man, mbp::term_graph &tg, model &mdl, obj_hashtable &vars_set, expr_sparse_mark &seen); // iterate through all terms in m_tg and apply all basic MBP rules once diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp new file mode 100644 index 000000000..632d7a7df --- /dev/null +++ b/src/qe/mbp/mbp_euf.cpp @@ -0,0 +1,85 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +--*/ + + +#include "ast/ast_util.h" +#include "ast/for_each_expr.h" +#include "qe/mbp/mbp_euf.h" +#include "qe/mbp/mbp_term_graph.h" + +namespace mbp { + euf_project_plugin::euf_project_plugin(ast_manager& m): project_plugin(m) { + + } + + euf_project_plugin::~euf_project_plugin() { + + } + + bool euf_project_plugin::project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { + return false; + } + + family_id euf_project_plugin::get_family_id() { + return basic_family_id; + } + + bool euf_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { + return false; + } + + bool euf_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) { + if (vars.empty()) + return false; + flatten_and(lits); + expr_mark var_set; + auto is_pure = [&](expr_mark& var_set, expr* v) { + return all_of(subterms::all(expr_ref(v, m)), [&](expr* w) { return !var_set.is_marked(w); }); + }; + for (auto v : vars) + var_set.mark(v, true); + unsigned has_def = false; +#if 1 + // solve trivial equations + for (auto e : lits) { + expr* x = nullptr, *y = nullptr; + if (m.is_eq(e, x, y) && var_set.is_marked(x) && is_pure(var_set, y)) { + vars.erase(to_app(x)); + defs.push_back({ expr_ref(x, m), expr_ref(y, m) }); + has_def = true; + } + else if (m.is_eq(e, y, x) && var_set.is_marked(x) && is_pure(var_set, y)) { + vars.erase(to_app(x)); + defs.push_back({ expr_ref(x, m), expr_ref(y, m) }); + has_def = true; + } + } + if (has_def) + return true; +#endif + + // check if there is a variable of uninterp sort + if (all_of(vars, [&](expr* v) { return !m.is_uninterp(v->get_sort()); })) + return has_def; + + term_graph tg(m); + tg.add_lits(lits); + for (auto v : vars) + if (m.is_uninterp(v->get_sort())) + tg.add_var(v); + + // + // now what: + /// walk all subterms of lits. + // push in partitions by value. + // add equations from model + // compute repr from tg. + // + + + return has_def; + } + +} diff --git a/src/qe/mbp/mbp_euf.h b/src/qe/mbp/mbp_euf.h new file mode 100644 index 000000000..f74e27f7d --- /dev/null +++ b/src/qe/mbp/mbp_euf.h @@ -0,0 +1,30 @@ + +/*++ +Copyright (c) 2025 Microsoft Corporation + +--*/ + + +#pragma once + +#include "model/model.h" +#include "qe/mbp/mbp_plugin.h" + +namespace mbp { + + class euf_project_plugin : public project_plugin { + public: + euf_project_plugin(ast_manager& m); + ~euf_project_plugin() override; + + bool project1(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) override; + bool solve(model& model, app_ref_vector& vars, expr_ref_vector& lits) override { return false; } + family_id get_family_id() override; + bool operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) override; + bool project(model& model, app_ref_vector& vars, expr_ref_vector& lits, vector& defs) override; + void saturate(model& model, func_decl_ref_vector const& shared, expr_ref_vector& lits) override { UNREACHABLE(); } + + }; + +}; + diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index 2584a4ce1..f560714d5 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -205,7 +205,7 @@ namespace mbp { else extract_bools(eval, fmls, i, fml, true); } - TRACE("qe", tout << fmls << "\n";); + TRACE("qe", tout << "fmls: " << fmls << "\n";); } void project_plugin::extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned idx, expr* fml, bool is_true) { diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index 5cf91098b..fb9be76dc 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -21,6 +21,7 @@ Revision History: #pragma once #include "ast/ast.h" +#include "ast/ast_pp.h" #include "util/params.h" #include "model/model.h" #include "math/simplex/model_based_opt.h" @@ -32,11 +33,12 @@ namespace mbp { struct def { expr_ref var, term; - def(const expr_ref& v, expr_ref& t): var(v), term(t) {} }; class project_plugin { + protected: ast_manager& m; + private: expr_mark m_visited; ptr_vector m_to_visit; expr_mark m_bool_visited; @@ -110,3 +112,6 @@ namespace mbp { }; } +inline std::ostream& operator<<(std::ostream& out, mbp::def const& d) { + return out << d.var << " -> " << d.term << "\n"; +} diff --git a/src/qe/mbp/mbp_term_graph.cpp b/src/qe/mbp/mbp_term_graph.cpp index 6ecaa5de2..e9a729d53 100644 --- a/src/qe/mbp/mbp_term_graph.cpp +++ b/src/qe/mbp/mbp_term_graph.cpp @@ -1018,8 +1018,7 @@ void term_graph::to_lits(expr_ref_vector &lits, bool all_equalities, void term_graph::to_lits_qe_lite(expr_ref_vector &lits, std::function *non_core) { DEBUG_CODE(for (auto t : m_terms) SASSERT(t->get_repr());); - DEBUG_CODE(for (auto t - : m_terms) + DEBUG_CODE(for (auto t : m_terms) SASSERT(!t->is_cgr() || t->get_repr()->is_cgr());); is_non_core not_in_core(non_core); check_pred contains_nc(not_in_core, m, false); diff --git a/src/qe/mbp/mbp_term_graph.h b/src/qe/mbp/mbp_term_graph.h index 58afcaf02..c5808939d 100644 --- a/src/qe/mbp/mbp_term_graph.h +++ b/src/qe/mbp/mbp_term_graph.h @@ -32,10 +32,10 @@ Notes: #include "util/plugin_manager.h" namespace mbp { -namespace is_ground_ns { -struct proc; -struct found; -} // namespace is_ground_ns + namespace is_ground_ns { + struct proc; + struct found; + } // namespace is_ground_ns class term; class term_graph { @@ -246,16 +246,16 @@ private: bool makes_cycle(term *t); }; -namespace is_ground_ns { -struct found {}; -struct proc { - term_graph::is_variable_proc &m_is_var; - proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {} - void operator()(var *n) const {} - void operator()(app const *n) const { - if (m_is_var.contains(n->get_decl())) throw found(); - } - void operator()(quantifier *n) const {} -}; -} // namespace is_ground_ns + namespace is_ground_ns { + struct found {}; + struct proc { + term_graph::is_variable_proc &m_is_var; + proc(term_graph::is_variable_proc &is_var) : m_is_var(is_var) {} + void operator()(var *n) const {} + void operator()(app const *n) const { + if (m_is_var.contains(n->get_decl())) throw found(); + } + void operator()(quantifier *n) const {} + }; + } // namespace is_ground_ns } // namespace mbp diff --git a/src/qe/mbp/mbp_tg_plugins.h b/src/qe/mbp/mbp_tg_plugins.h index ab4a54333..3850f11ca 100644 --- a/src/qe/mbp/mbp_tg_plugins.h +++ b/src/qe/mbp/mbp_tg_plugins.h @@ -23,12 +23,12 @@ Revision History: #include "util/obj_hashtable.h" class mbp_tg_plugin { - public: - // iterate through all terms in m_tg and apply all theory MBP rules once - // returns true if any rules were applied - virtual bool apply() { return false; }; - virtual ~mbp_tg_plugin() = default; - virtual void use_model() { }; - virtual void get_new_vars(app_ref_vector*&) { }; - virtual family_id get_family_id() const { return null_family_id; }; +public: + // iterate through all terms in m_tg and apply all theory MBP rules once + // returns true if any rules were applied + virtual bool apply() { return false; }; + virtual ~mbp_tg_plugin() = default; + virtual void use_model() { }; + virtual void get_new_vars(app_ref_vector*&) { }; + virtual family_id get_family_id() const { return null_family_id; }; }; diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 1a7013723..e8ce2777b 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -37,6 +37,7 @@ Revision History: #include "qe/lite/qel.h" #include "qe/mbp/mbp_arith.h" #include "qe/mbp/mbp_arrays.h" +#include "qe/mbp/mbp_euf.h" #include "qe/mbp/mbp_qel.h" #include "qe/mbp/mbp_datatypes.h" @@ -352,6 +353,7 @@ public: add_plugin(alloc(mbp::arith_project_plugin, m)); add_plugin(alloc(mbp::datatype_project_plugin, m)); add_plugin(alloc(mbp::array_project_plugin, m)); + add_plugin(alloc(mbp::euf_project_plugin, m)); updt_params(p); } @@ -392,18 +394,18 @@ public: flatten_and(fml, fmls); } else { - extract_literals(model, vars, fmls); - bool change = true; - while (change && !vars.empty()) { - change = solve(model, vars, fmls); - for (auto* p : m_plugins) { - if (p && p->solve(model, vars, fmls)) { - change = true; + extract_literals(model, vars, fmls); + bool change = true; + while (change && !vars.empty()) { + change = solve(model, vars, fmls); + for (auto* p : m_plugins) { + if (p && p->solve(model, vars, fmls)) { + change = true; + } } } } } - } bool validate_model(model& model, expr_ref_vector const& fmls) { for (expr* f : fmls) { @@ -419,24 +421,27 @@ public: return any_of(subterms::all(e), [&](expr* c) { return seq.is_char(c) || seq.is_seq(c); }); } void operator()(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector* defs = nullptr) { - //don't use mbp_qel on some theories where model evaluation is - //incomplete This is not a limitation of qel. Fix this either by - //making mbp choices less dependent on the model evaluation methods - //or fix theory rewriters to make terms evaluation complete - if (m_use_qel && !has_unsupported_th(fmls) && !defs) { - bool dsub = m_dont_sub; - m_dont_sub = !force_elim; - expr_ref fml(m); - fml = mk_and(fmls); - spacer_qel(vars, model, fml); - fmls.reset(); - flatten_and(fml, fmls); - m_dont_sub = dsub; - } - else { - mbp(force_elim, vars, model, fmls, defs); - } + //don't use mbp_qel on some theories where model evaluation is + //incomplete This is not a limitation of qel. Fix this either by + //making mbp choices less dependent on the model evaluation methods + //or fix theory rewriters to make terms evaluation complete + if (m_use_qel && !has_unsupported_th(fmls) && !defs) { + bool dsub = m_dont_sub; + m_dont_sub = !force_elim; + expr_ref fml(m); + fml = mk_and(fmls); + spacer_qel(vars, model, fml); + fmls.reset(); + flatten_and(fml, fmls); + m_dont_sub = dsub; + TRACE("qe", tout << "spacer-qel " << vars << " " << fml << "\n"); } + else { + mbp(force_elim, vars, model, fmls, defs); + TRACE("qe", tout << "mbp " << vars << " " << fmls << "\n"; + if (defs) { tout << "defs: "; for (auto const& d : *defs) tout << d << "\n"; tout << "\n";}); + } + } void mbp(bool force_elim, app_ref_vector& vars, model& model, expr_ref_vector& fmls, vector* defs) { SASSERT(validate_model(model, fmls)); @@ -444,9 +449,12 @@ public: app_ref var(m); expr_ref_vector unused_fmls(m); bool progress = true; - preprocess_solve(model, vars, fmls); + TRACE("qe", tout << "eliminate vars: " << vars << "fmls: " << fmls << "\n"); + if (!defs) + preprocess_solve(model, vars, fmls); filter_variables(model, vars, fmls, unused_fmls); project_bools(model, vars, fmls); + TRACE("qe", tout << "eliminate vars: " << vars << "\nfmls: " << fmls << "\nunused: " << unused_fmls <<"\n"); while (progress && !vars.empty() && !fmls.empty() && m.limit().inc()) { app_ref_vector new_vars(m); progress = false; @@ -455,10 +463,12 @@ public: unsigned sz = defs->size(); p->project(model, vars, fmls, *defs); progress |= sz < defs->size(); + TRACE("qe", tout << "after project " << m.get_family_name(p->get_family_id()) << ": " << vars << "\n"); } else if (p) (*p)(model, vars, fmls); } + TRACE("qe", tout << "projecting " << vars << "\n"); while (!vars.empty() && !fmls.empty() && !defs && m.limit().inc()) { var = vars.back(); vars.pop_back(); @@ -491,16 +501,17 @@ public: if (!m.limit().inc()) return; vars.append(new_vars); - if (progress) { + if (progress && !defs) preprocess_solve(model, vars, fmls); - } + TRACE("qe", tout << "looping " << vars << "\n"); + } if (fmls.empty()) { vars.reset(); } fmls.append(unused_fmls); SASSERT(validate_model(model, fmls)); - TRACE("qe", tout << vars << " " << fmls << "\n";); + TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n";); } void do_qe_lite(app_ref_vector& vars, expr_ref& fml) { @@ -529,16 +540,16 @@ public: fml = mk_and(fmls); } - void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) { - flatten_and(fml); - mbp::mbp_qel mbptg(m, m_params); - mbptg(vars, fml, mdl); - if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml); - m_rw(fml); - TRACE("qe", tout << "After mbp_tg:\n" - << fml << " models " << mdl.is_true(fml) << "\n" - << "Vars: " << vars << "\n";); - } + void qel_project(app_ref_vector &vars, model &mdl, expr_ref &fml, bool reduce_all_selects) { + flatten_and(fml); + mbp::mbp_qel mbptg(m, m_params); + mbptg(vars, fml, mdl); + if (reduce_all_selects) rewrite_read_over_write(fml, mdl, fml); + m_rw(fml); + TRACE("qe", tout << "After mbp_tg:\n" + << fml << " models " << mdl.is_true(fml) << "\n" + << "Vars: " << vars << "\n";); + } void spacer_qel(app_ref_vector& vars, model& mdl, expr_ref& fml) { TRACE("qe", tout << "Before projection:\n" << fml << "\n" << "Vars: " << vars << "\n";); @@ -600,12 +611,11 @@ public: } void spacer(app_ref_vector& vars, model& mdl, expr_ref& fml) { - if (m_use_qel) { + TRACE("qe", tout << "spacer " << m_use_qel << " " << fml << " " << vars << "\n"); + if (m_use_qel) spacer_qel(vars, mdl, fml); - } - else { + else spacer_qe_lite(vars, mdl, fml); - } } void spacer_qe_lite(app_ref_vector& vars, model& mdl, expr_ref& fml) {