diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 969d22a81..f663d1b6c 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -299,20 +299,19 @@ namespace qe { obj_map tids; expr_ref_vector pinned(m); unsigned j = 0; + TRACE("qe", tout << "fmls: " << fmls << "\n";); for (unsigned i = 0; i < fmls.size(); ++i) { - expr* fml = fmls[i].get(); + expr * fml = fmls.get(i); if (!linearize(mbo, eval, fml, fmls, tids)) { - if (i != j) { - fmls[j] = fmls[i].get(); - } - ++j; + fmls[j++] = fml; } else { - TRACE("qe", tout << mk_pp(fml, m) << "\n";); + TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";); pinned.push_back(fml); } } - fmls.resize(j); + fmls.shrink(j); + TRACE("qe", tout << "linearized: " << fmls << "\n";); // fmls holds residue, // mbo holds linear inequalities that are in scope @@ -328,13 +327,13 @@ namespace qe { if (is_arith(v) && !tids.contains(v)) { rational r; expr_ref val = eval(v); - a.is_numeral(val, r); + VERIFY(a.is_numeral(val, r)); TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";); tids.insert(v, mbo.add_var(r, a.is_int(v))); } } for (expr* fml : fmls) { - fmls_mark.mark(fml); + mark_rec(fmls_mark, fml); } ptr_vector index2expr; for (auto& kv : tids) { @@ -346,8 +345,7 @@ namespace qe { } j = 0; unsigned_vector real_vars; - for (unsigned i = 0; i < vars.size(); ++i) { - app* v = vars[i].get(); + for (app* v : vars) { if (is_arith(v) && !fmls_mark.is_marked(v)) { real_vars.push_back(tids.find(v)); } @@ -355,7 +353,7 @@ namespace qe { vars[j++] = v; } } - vars.resize(j); + vars.shrink(j); TRACE("qe", tout << "remaining vars: " << vars << "\n"; for (unsigned v : real_vars) { tout << "v" << v << " " << mk_pp(index2expr[v], m) << "\n"; @@ -391,8 +389,7 @@ namespace qe { CTRACE("qe", !m.is_true(val), tout << "Evaluated unit " << t << " to " << val << "\n";); continue; } - for (j = 0; j < r.m_vars.size(); ++j) { - var const& v = r.m_vars[j]; + for (var const& v : r.m_vars) { t = index2expr[v.m_id]; if (!v.m_coeff.is_one()) { t = a.mk_mul(a.mk_numeral(v.m_coeff, a.is_int(t)), t); @@ -418,11 +415,9 @@ namespace qe { break; } } - fmls.push_back(t); - + fmls.push_back(t); val = eval(t); CTRACE("qe", !m.is_true(val), tout << "Evaluated " << t << " to " << val << "\n";); - } } diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index f7b8898c1..305fb47b6 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -1390,9 +1390,9 @@ namespace qe { array_project_eqs_util pe (m); pe (mdl, arr_vars, fml, aux_vars); TRACE ("qe", - tout << "Projected array eqs:\n" << fml << "\n"; - tout << "Remaining array vars:\n" << arr_vars; - tout << "Aux vars:\n" << aux_vars; + tout << "Projected array eqs: " << fml << "\n"; + tout << "Remaining array vars: " << arr_vars << "\n"; + tout << "Aux vars: " << aux_vars << "\n"; ); // 2. reduce selects @@ -1406,8 +1406,8 @@ namespace qe { ps (mdl, arr_vars, fml, aux_vars); TRACE ("qe", - tout << "Projected array selects:\n" << fml << "\n"; - tout << "All aux vars:\n" << aux_vars; + tout << "Projected array selects: " << fml << "\n"; + tout << "All aux vars: " << aux_vars << "\n"; ); } diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index bc9ac8c41..b1c92cb8c 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -77,42 +77,6 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) { return expr_ref(nullptr, m); } -void project_plugin::partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits) { - ast_manager& m = vals.get_manager(); - expr_ref val(m); - expr_ref_vector trail(m), reps(m); - obj_map roots; - for (unsigned i = 0; i < vals.size(); ++i) { - expr* v = vals[i], *root; - VERIFY (model.eval(v, val)); - if (roots.find(val, root)) { - lits.push_back(m.mk_eq(v, root)); - } - else { - roots.insert(val, v); - trail.push_back(val); - reps.push_back(v); - } - } - if (reps.size() > 1) { - lits.push_back(mk_distinct(reps)); - } -} - -#if 0 -void project_plugin::partition_args(model& model, app_ref_vector const& selects, expr_ref_vector& lits) { - ast_manager& m = selects.get_manager(); - if (selects.empty()) return; - unsigned num_args = selects[0]->get_decl()->get_arity(); - for (unsigned j = 1; j < num_args; ++j) { - expr_ref_vector args(m); - for (unsigned i = 0; i < selects.size(); ++i) { - args.push_back(selects[i]->get_arg(j)); - } - project_plugin::partition_values(model, args, lits); - } -} -#endif void project_plugin::erase(expr_ref_vector& lits, unsigned& i) { lits[i] = lits.back(); @@ -136,7 +100,6 @@ class mbp::impl { // parameters bool m_reduce_all_selects; - bool m_native_mbp; bool m_dont_sub; void add_plugin(project_plugin* p) { @@ -324,8 +287,7 @@ class mbp::impl { 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); + for (expr * arg : *n) { if (m.get_sort(arg) == m.get_sort(m_var) && arg != m_var) m_res.push_back (arg); } @@ -378,8 +340,7 @@ class mbp::impl { // -- evaluate to initialize eval cache (void) eval (fml); unsigned j = 0; - for (unsigned i = 0; i < vars.size (); ++i) { - app* v = vars.get(i); + for (app * v : vars) { if (!project_var (eval, v, fml)) { vars[j++] = v; } @@ -389,7 +350,6 @@ class mbp::impl { public: - opt::inf_eps maximize(expr_ref_vector const& fmls, model& mdl, app* t, expr_ref& ge, expr_ref& gt) { arith_project_plugin arith(m); return arith.maximize(fmls, mdl, t, ge, gt); @@ -530,7 +490,6 @@ public: 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); } @@ -549,6 +508,7 @@ public: bool validate_model(model& model, expr_ref_vector const& fmls) { expr_ref val(m); + model_evaluator eval(model); for (expr * f : fmls) { VERIFY(model.eval(f, val) && m.is_true(val)); } @@ -677,27 +637,20 @@ public: tout << "extended model:\n"; model_pp (tout, mdl); tout << "Auxiliary variables of index and value sorts:\n"; - tout << vars; + tout << vars << "\n"; ); } // project reals and ints if (!arith_vars.empty ()) { - TRACE ("qe", tout << "Arith vars:\n" << arith_vars;); + TRACE ("qe", tout << "Arith vars: " << arith_vars << "\n";); - 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); - } + expr_ref_vector fmls(m); + flatten_and (fml, fmls); + (*this)(true, arith_vars, mdl, fmls); + fml = mk_and (fmls); + TRACE ("qe", tout << "Projected arith vars:\n" << fml << "\n"; tout << "Remaining arith vars:\n" << arith_vars << "\n";); @@ -740,7 +693,6 @@ void mbp::updt_params(params_ref const& 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"); } diff --git a/src/qe/qe_mbp.h b/src/qe/qe_mbp.h index 665e25d48..25a95e885 100644 --- a/src/qe/qe_mbp.h +++ b/src/qe/qe_mbp.h @@ -40,8 +40,6 @@ namespace qe { virtual void operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { }; static expr_ref pick_equality(ast_manager& m, model& model, expr* t); - static void partition_values(model& model, expr_ref_vector const& vals, expr_ref_vector& lits); - //static void partition_args(model& model, app_ref_vector const& sels, expr_ref_vector& lits); static void erase(expr_ref_vector& lits, unsigned& i); static void push_back(expr_ref_vector& lits, expr* lit); static void mark_rec(expr_mark& visited, expr* e);