From 335d672bf1f923b8782d89da2b60339a29c742e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Jun 2018 23:23:19 -0700 Subject: [PATCH] fix #1675, regression in core processing in maxres Signed-off-by: Nikolaj Bjorner --- src/api/api_model.cpp | 3 +- src/cmd_context/basic_cmds.cpp | 4 +- src/model/model.cpp | 8 +- src/model/model.h | 5 +- src/model/model_core.h | 2 +- src/model/model_implicant.cpp | 18 ++- src/model/model_smt2_pp.cpp | 5 + src/model/model_smt2_pp.h | 1 + src/muz/bmc/dl_bmc_engine.cpp | 25 ++-- src/muz/spacer/spacer_context.cpp | 6 +- src/muz/spacer/spacer_legacy_mbp.cpp | 5 +- src/muz/spacer/spacer_legacy_mev.cpp | 17 ++- src/muz/spacer/spacer_qe_project.cpp | 18 ++- src/muz/spacer/spacer_sat_answer.cpp | 7 +- src/muz/spacer/spacer_unsat_core_plugin.cpp | 2 +- src/muz/tab/tab_context.cpp | 3 +- src/nlsat/tactic/nlsat_tactic.cpp | 5 +- src/opt/maxres.cpp | 146 ++++++++------------ src/opt/maxsmt.cpp | 15 +- src/opt/opt_context.cpp | 63 ++++----- src/opt/optsmt.cpp | 2 +- src/opt/pb_sls.cpp | 10 +- src/opt/sortmax.cpp | 6 +- src/opt/wmax.cpp | 8 +- src/parsers/smt2/smt2parser.cpp | 4 +- src/qe/qe_arrays.cpp | 7 +- src/qe/qe_datatypes.cpp | 3 +- src/qe/qe_mbp.cpp | 6 +- src/qe/qsat.cpp | 20 +-- src/sat/tactic/goal2sat.cpp | 4 +- src/sat/tactic/goal2sat.h | 2 +- src/shell/opt_frontend.cpp | 6 +- src/smt/mam.cpp | 38 ++--- src/smt/smt_consequences.cpp | 7 +- src/smt/smt_implied_equalities.cpp | 2 +- src/solver/mus.cpp | 3 +- src/solver/solver.cpp | 3 +- src/tactic/generic_model_converter.cpp | 15 +- src/tactic/generic_model_converter.h | 2 +- src/tactic/horn_subsume_model_converter.cpp | 3 +- src/tactic/model_converter.cpp | 21 ++- src/tactic/model_converter.h | 2 +- src/tactic/sls/sls_engine.cpp | 35 ++--- 43 files changed, 246 insertions(+), 321 deletions(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 6318283c6..7eb7d2fdd 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -166,7 +166,8 @@ extern "C" { CHECK_IS_EXPR(t, Z3_FALSE); model * _m = to_model_ref(m); expr_ref result(mk_c(c)->m()); - _m->eval(to_expr(t), result, model_completion == Z3_TRUE); + model::scoped_model_completion _scm(*_m, model_completion == Z3_TRUE); + result = (*_m)(to_expr(t)); mk_c(c)->save_ast_trail(result.get()); *v = of_ast(result.get()); RETURN_Z3_model_eval Z3_TRUE; diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 4e5202fd8..846fb1ded 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -138,8 +138,8 @@ ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { macro_decls const & _m = kv.m_value; for (auto md : _m) { if (md.m_domain.size() == 0 && ctx.m().is_bool(md.m_body)) { - expr_ref val(ctx.m()); - m->eval(md.m_body, val, true); + model::scoped_model_completion _scm(*m, true); + expr_ref val = (*m)(md.m_body); if (ctx.m().is_true(val) || ctx.m().is_false(val)) { if (first) first = false; diff --git a/src/model/model.cpp b/src/model/model.cpp index 9ac971afe..6ddf9765c 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -66,12 +66,10 @@ model * model::copy() const { return m; } -// Remark: eval is for backward compatibility. We should use model_evaluator. -bool model::eval(expr * e, expr_ref & result, bool model_completion) { - model_evaluator ev(*this); - ev.set_model_completion(model_completion); +bool model::eval_expr(expr * e, expr_ref & result, bool model_completion) { + scoped_model_completion _smc(*this, model_completion); try { - ev(e, result); + result = (*this)(e); return true; } catch (model_evaluator_exception & ex) { diff --git a/src/model/model.h b/src/model/model.h index 429e7b51a..9399be285 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -46,8 +46,7 @@ public: model * copy() const; - bool eval(func_decl * f, expr_ref & r) const { return model_core::eval(f, r); } - bool eval(expr * e, expr_ref & result, bool model_completion = false); + bool eval_expr(expr * e, expr_ref & result, bool model_completion = false); expr * get_some_value(sort * s) override; ptr_vector const & get_universe(sort * s) const override; @@ -93,8 +92,6 @@ public: m_model.set_model_completion(m_old_completion); } }; - - }; diff --git a/src/model/model_core.h b/src/model/model_core.h index 400b2fcab..3f1e92bad 100644 --- a/src/model/model_core.h +++ b/src/model/model_core.h @@ -40,7 +40,7 @@ public: virtual ~model_core(); ast_manager & get_manager() const { return m_manager; } - ast_manager& m() { return m_manager; } + ast_manager& m() const { return m_manager; } unsigned get_num_decls() const { return m_decls.size(); } func_decl * get_decl(unsigned i) const { return m_decls[i]; } diff --git a/src/model/model_implicant.cpp b/src/model/model_implicant.cpp index 0cdd80c11..375834477 100644 --- a/src/model/model_implicant.cpp +++ b/src/model/model_implicant.cpp @@ -535,9 +535,8 @@ bool model_implicant::extract_array_func_interp(expr* a, vector */ void model_implicant::eval_array_eq(app* e, expr* arg1, expr* arg2) { TRACE("pdr", tout << "array equality: " << mk_pp(e, m) << "\n";); - expr_ref v1(m), v2(m); - m_model->eval(arg1, v1); - m_model->eval(arg2, v2); + expr_ref v1 = (*m_model)(arg1); + expr_ref v2 = (*m_model)(arg2); if (v1 == v2) { set_true(e); return; @@ -587,8 +586,8 @@ void model_implicant::eval_array_eq(app* e, expr* arg1, expr* arg2) { args2.append(store[i].size()-1, store[i].c_ptr()); s1 = m_array.mk_select(args1.size(), args1.c_ptr()); s2 = m_array.mk_select(args2.size(), args2.c_ptr()); - m_model->eval(s1, w1); - m_model->eval(s2, w2); + w1 = (*m_model)(s1); + w2 = (*m_model)(s2); if (w1 == w2) { continue; } @@ -621,9 +620,9 @@ void model_implicant::eval_eq(app* e, expr* arg1, expr* arg2) { eval_array_eq(e, arg1, arg2); } else if (is_x(arg1) || is_x(arg2)) { - expr_ref eq(m), vl(m); + expr_ref eq(m); eq = m.mk_eq(arg1, arg2); - m_model->eval(eq, vl); + expr_ref vl = (*m_model)(eq); if (m.is_true(vl)) { set_bool(e, true); } @@ -837,8 +836,7 @@ bool model_implicant::check_model(ptr_vector const& formulas) { eval_basic(curr); } else { - expr_ref vl(m); - m_model->eval(curr, vl); + expr_ref vl = (*m_model)(curr); assign_value(curr, vl); } @@ -884,7 +882,7 @@ expr_ref model_implicant::eval(model_ref& model, func_decl* d) { expr_ref model_implicant::eval(model_ref& model, expr* e) { expr_ref result(m); m_model = model; - VERIFY(m_model->eval(e, result, true)); + result = (*m_model)(e); if (m_array.is_array(e)) { vector stores; expr_ref_vector args(m); diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index 152cbc8d3..bc1900ba7 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -302,3 +302,8 @@ void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, u pp_consts(out, *(ctx.get()), md, indent); pp_funs(out, *(ctx.get()), md, indent); } + +std::ostream& operator<<(std::ostream& out, model_core const& m) { + model_smt2_pp(out, m.m(), m, 0); + return out; +} diff --git a/src/model/model_smt2_pp.h b/src/model/model_smt2_pp.h index c43e26ca6..b38bd631d 100644 --- a/src/model/model_smt2_pp.h +++ b/src/model/model_smt2_pp.h @@ -25,5 +25,6 @@ Revision History: void model_smt2_pp(std::ostream & out, ast_printer_context & ctx, model_core const & m, unsigned indent); void model_smt2_pp(std::ostream & out, ast_manager & m, model_core const & md, unsigned indent); +std::ostream& operator<<(std::ostream& out, model_core const& m); #endif diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index c7657a0d7..97432f544 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -228,10 +228,9 @@ namespace datalog { expr_ref eval_q(model_ref& model, func_decl* f, unsigned i) { func_decl_ref fn = mk_q_func_decl(f); - expr_ref t(m), result(m); + expr_ref t(m); t = m.mk_app(mk_q_func_decl(f).get(), mk_q_num(i)); - model->eval(t, result); - return result; + return (*model)(t); } expr_ref eval_q(model_ref& model, expr* t, unsigned i) { @@ -240,8 +239,7 @@ namespace datalog { num = mk_q_num(i); expr* nums[1] = { num }; vs(t, 1, nums, tmp); - model->eval(tmp, result); - return result; + return (*model)(tmp); } lbool get_model() { @@ -258,7 +256,7 @@ namespace datalog { func_decl* pred = b.m_query_pred; dl_decl_util util(m); T = m.mk_const(symbol("T"), mk_index_sort()); - md->eval(T, vl); + vl = (*md)(T); VERIFY (m_bv.is_numeral(vl, num, bv_size)); SASSERT(num.is_unsigned()); level = num.get_unsigned(); @@ -505,8 +503,7 @@ namespace datalog { func_decl_ref rule_i = mk_level_rule(pred, i, level); TRACE("bmc", rls[i]->display(b.m_ctx, tout << "Checking rule " << mk_pp(rule_i, m) << " ");); prop_r = m.mk_app(rule_i, prop->get_num_args(), prop->get_args()); - md->eval(prop_r, prop_v); - if (m.is_true(prop_v)) { + if (md->is_true(prop_r)) { r = rls[i]; break; } @@ -527,8 +524,7 @@ namespace datalog { return pr; } for (unsigned j = 0; j < sub.size(); ++j) { - md->eval(sub[j].get(), tmp); - sub[j] = tmp; + sub[j] = (*md)(sub[j].get()); } svector > positions; @@ -1062,8 +1058,7 @@ namespace datalog { return pr; } for (unsigned j = 0; j < sub.size(); ++j) { - md->eval(sub[j].get(), tmp); - sub[j] = tmp; + sub[j] = (*md)(sub.get(j)); } rule_ref rl(b.m_ctx.get_rule_manager()); rl = rules[i]; @@ -1116,7 +1111,7 @@ namespace datalog { bool check_model(model_ref& md, expr* trace) { expr_ref trace_val(m), eq(m); - md->eval(trace, trace_val); + trace_val = (*md)(trace); eq = m.mk_eq(trace, trace_val); b.m_solver.push(); b.m_solver.assert_expr(eq); @@ -1135,8 +1130,8 @@ namespace datalog { void mk_answer(model_ref& md, expr_ref& trace, expr_ref& path) { IF_VERBOSE(2, model_smt2_pp(verbose_stream(), m, *md, 0);); - md->eval(trace, trace); - md->eval(path, path); + trace = (*md)(trace); + path = (*md)(path); IF_VERBOSE(2, verbose_stream() << mk_pp(trace, m) << "\n"; for (unsigned i = 0; i < b.m_solver.size(); ++i) { verbose_stream() << mk_pp(b.m_solver.get_formula(i), m) << "\n"; diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index b917f8cc1..f3ceee9c8 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1398,7 +1398,7 @@ bool pred_transformer::is_ctp_blocked(lemma *lem) { expr_ref lemmas(m), val(m); lemmas = pt.get_formulas(lem->level()); pm.formula_n2o(lemmas.get(), lemmas, i); - if (ctp->eval(lemmas, val) && m.is_false(val)) {return false;} + if (ctp->is_false(lemmas)) return false; } // lem is blocked by ctp since none of the lemmas at the previous @@ -2440,13 +2440,13 @@ bool context::validate() get_rule_manager (). display_smt2(r, tout) << "\n";); - model->eval(r.get_head(), tmp); + tmp = (*model)(r.get_head()); expr_ref_vector fmls(m); fmls.push_back(m.mk_not(tmp)); unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); for (unsigned j = 0; j < utsz; ++j) { - model->eval(r.get_tail(j), tmp); + tmp = (*model)(r.get_tail(j)); fmls.push_back(tmp); } for (unsigned j = utsz; j < tsz; ++j) { diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp index d52228d8a..76b543f04 100644 --- a/src/muz/spacer/spacer_legacy_mbp.cpp +++ b/src/muz/spacer/spacer_legacy_mbp.cpp @@ -71,10 +71,11 @@ void qe_project(ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& expr_substitution sub(m); proof_ref pr(m.mk_asserted(m.mk_true()), m); expr_ref bval(m); + model::scoped_model_completion _scm(*M, true); for (unsigned i = 0; i < vars.size(); i++) { if (m.is_bool(vars.get(i))) { // obtain the interpretation of the ith var using model completion - VERIFY(M->eval(vars.get(i), bval, true)); + bval = (*M)(vars.get(i)); sub.insert(vars.get(i), bval, pr); } else { arith_vars.push_back(vars.get(i)); @@ -106,7 +107,7 @@ void qe_project(ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& tout << "Projected arith vars:\n" << mk_pp(fml, m) << "\n"; ); } - SASSERT(M->eval(fml, bval, true) && m.is_true(bval)); // M |= fml + SASSERT(M->is_true(fml)); vars.reset(); vars.append(arith_vars); } diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp index 5feaed1fa..b62b24b0d 100644 --- a/src/muz/spacer/spacer_legacy_mev.cpp +++ b/src/muz/spacer/spacer_legacy_mev.cpp @@ -461,8 +461,8 @@ void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) { TRACE("old_spacer", tout << "array equality: " << mk_pp(e, m) << "\n";); expr_ref v1(m), v2(m); - m_model->eval(arg1, v1); - m_model->eval(arg2, v2); + v1 = (*m_model)(arg1); + v2 = (*m_model)(arg2); if (v1 == v2) { set_true(e); return; @@ -510,8 +510,8 @@ void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) args2.append(store[i].size() - 1, store[i].c_ptr()); s1 = m_array.mk_select(args1.size(), args1.c_ptr()); s2 = m_array.mk_select(args2.size(), args2.c_ptr()); - m_model->eval(s1, w1); - m_model->eval(s2, w2); + w1 = (*m_model)(s1); + w2 = (*m_model)(s2); if (w1 == w2) { continue; } @@ -729,7 +729,7 @@ void model_evaluator::eval_fmls(ptr_vector const& formulas) eval_basic(curr); } else { expr_ref vl(m); - m_model->eval(curr, vl); + vl = eval(m_model, curr); assign_value(curr, vl); } @@ -798,11 +798,10 @@ expr_ref model_evaluator::eval(const model_ref& model, func_decl* d) return result; } -expr_ref model_evaluator::eval(const model_ref& model, expr* e) -{ - expr_ref result(m); +expr_ref model_evaluator::eval(const model_ref& model, expr* e){ m_model = model.get(); - VERIFY(m_model->eval(e, result, true)); + model::scoped_model_completion _scm(m_model, true); + expr_ref result = (*m_model)(e); if (m_array.is_array(e)) { vector stores; expr_ref_vector args(m); diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 1bf670a7a..ed5a0215c 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -378,7 +378,7 @@ namespace spacer_qe { rational r; cx = mk_mul (c, m_var->x()); cxt = mk_add (cx, t); - VERIFY(mdl.eval(cxt, val, true)); + val = mdl(cxt); VERIFY(a.is_numeral(val, r)); SASSERT (r > rational::zero () || r < rational::zero ()); if (r > rational::zero ()) { @@ -464,8 +464,7 @@ namespace spacer_qe { m_strict.reset(); m_eq.reset (); - expr_ref var_val (m); - VERIFY (mdl.eval (m_var->x(), var_val, true)); + expr_ref var_val = mdl(m_var->x()); unsigned eq_idx = lits.size (); for (unsigned i = 0; i < lits.size(); ++i) { @@ -492,7 +491,7 @@ namespace spacer_qe { rational r; cx = mk_mul (c, m_var->x()); cxt = mk_add (cx, t); - VERIFY(mdl.eval(cxt, val, true)); + val = mdl(cxt); VERIFY(a.is_numeral(val, r)); if (is_eq) { @@ -738,7 +737,7 @@ namespace spacer_qe { rational r; cx = mk_mul (m_coeffs[max_t], m_var->x()); cxt = mk_add (cx, m_terms.get (max_t)); - VERIFY(mdl.eval(cxt, val, true)); + val = mdl(cxt); VERIFY(a.is_numeral(val, r)); // get the offset from the smallest/largest possible value for x @@ -796,13 +795,13 @@ namespace spacer_qe { // evaluate x in mdl rational r_x; - VERIFY(mdl.eval(m_var->x (), val, true)); + val = mdl(m_var->x ()); VERIFY(a.is_numeral (val, r_x)); for (unsigned i = 0; i < m_terms.size(); ++i) { rational const& ac = m_coeffs[i]; if (!m_eq[i] && ac.is_pos() == do_pos) { - VERIFY(mdl.eval(m_terms.get (i), val, true)); + val = mdl(m_terms.get (i)); VERIFY(a.is_numeral(val, r)); r /= abs(ac); // skip the literal if false in the model @@ -955,8 +954,7 @@ namespace spacer_qe { new_var = m.mk_fresh_const ("mod_var", d->get_range ()); eqs.push_back (m.mk_eq (new_var, new_term)); // obtain value of new_term in mdl - expr_ref val (m); - mdl.eval (new_term, val, true); + expr_ref val = mdl(new_term); // use the variable from now on new_term = new_var; changed = true; @@ -1413,7 +1411,7 @@ namespace spacer_qe { app_ref val_const (m.mk_fresh_const ("sel", val_sort), m); m_aux_vars.push_back (val_const); // extend M to include val_const - expr_ref val (m); + expr_ref val(m); m_mev.eval (*M, a_new, val); M->register_decl (val_const->get_decl (), val); // add equality diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp index 09553de89..30241230f 100644 --- a/src/muz/spacer/spacer_sat_answer.cpp +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -65,10 +65,11 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { SASSERT(res == l_true); model_ref mdl; m_solver->get_model(mdl); + model::scoped_model_completion _scm(mdl, true); for (unsigned i = 0, sz = query.sig_size(); i < sz; ++i) { expr_ref arg(m), val(m); arg = m.mk_const(m_pm.o2n(query.sig(i), 0)); - mdl->eval(arg, val, true); + val = (*mdl)(arg); qsubst.push_back(val); } } @@ -141,11 +142,13 @@ void ground_sat_answer_op::mk_children(frame &fr, vector &todo) { void ground_sat_answer_op::mk_child_subst_from_model(func_decl *pred, unsigned j, model_ref &mdl, expr_ref_vector &subst) { + + model::scoped_model_completion _scm(mdl, true); pred_transformer &pt = m_ctx.get_pred_transformer(pred); for (unsigned i = 0, sz = pt.sig_size(); i < sz; ++i) { expr_ref arg(m), val(m); arg = m.mk_const(m_pm.o2o(pt.sig(i), 0, j)); - mdl->eval(arg, val, true); + val = (*mdl)(arg); subst.push_back(val); } } diff --git a/src/muz/spacer/spacer_unsat_core_plugin.cpp b/src/muz/spacer/spacer_unsat_core_plugin.cpp index b96ef3037..8fb5feeef 100644 --- a/src/muz/spacer/spacer_unsat_core_plugin.cpp +++ b/src/muz/spacer/spacer_unsat_core_plugin.cpp @@ -472,7 +472,7 @@ namespace spacer { for (unsigned j = 0; j < matrix.num_cols(); ++j) { expr_ref evaluation(m); - model.get()->eval(bounded_vectors[j][k].get(), evaluation, false); + evaluation = (*model)(bounded_vectors[j][k].get()); if (!util.is_zero(evaluation)) { coeff_lits.push_back(std::make_pair(rational(1), ordered_basis[j])); } diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp index 2fb329ff4..7200b3522 100644 --- a/src/muz/tab/tab_context.cpp +++ b/src/muz/tab/tab_context.cpp @@ -693,13 +693,12 @@ namespace tb { m_solver.assert_expr(postcond); lbool is_sat = m_solver.check(); if (is_sat == l_true) { - expr_ref tmp(m); expr* n; model_ref mdl; m_solver.get_model(mdl); for (unsigned i = 0; i < fmls.size(); ++i) { n = fmls[i].get(); - if (mdl->eval(n, tmp) && m.is_false(tmp)) { + if (mdl->is_false(n)) { m_refs.push_back(normalize(n)); m_sat_lits.insert(m_refs.back()); } diff --git a/src/nlsat/tactic/nlsat_tactic.cpp b/src/nlsat/tactic/nlsat_tactic.cpp index 1392df3f6..5e536bbe6 100644 --- a/src/nlsat/tactic/nlsat_tactic.cpp +++ b/src/nlsat/tactic/nlsat_tactic.cpp @@ -83,9 +83,8 @@ class nlsat_tactic : public tactic { bool eval_model(model& model, goal& g) { unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { - expr_ref val(m); - if (model.eval(g.form(i), val) && !m.is_true(val)) { - TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << val << "\n";); + if (!model.is_true(g.form(i))) { + TRACE("nlsat", tout << mk_pp(g.form(i), m) << " -> " << model(g.form(i)) << "\n";); return false; } } diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 6c71c6238..912a64038 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -175,10 +175,11 @@ public: void new_assumption(expr* e, rational const& w) { IF_VERBOSE(13, verbose_stream() << "new assumption " << mk_pp(e, m) << " " << w << "\n";); - TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n";); m_asm2weight.insert(e, w); m_asms.push_back(e); m_trail.push_back(e); + TRACE("opt", tout << "insert: " << mk_pp(e, m) << " : " << w << "\n"; + tout << m_asms << " " << "\n"; ); } void trace() { @@ -192,7 +193,7 @@ public: trace(); if (is_sat != l_true) return is_sat; while (m_lower < m_upper) { - TRACE("opt", + TRACE("opt_verbose", display_vec(tout, m_asms); s().display(tout); tout << "\n"; @@ -204,7 +205,12 @@ public: } switch (is_sat) { case l_true: - SASSERT(is_true(m_asms)); + CTRACE("opt", !m_model->is_true(m_asms), + tout << *m_model; + tout << "assumptions: "; + for (expr* a : m_asms) tout << mk_pp(a, m) << " -> " << (*m_model)(a) << " "; + tout << "\n";); + SASSERT(m_model->is_true(m_asms)); found_optimum(); return l_true; case l_false: @@ -276,8 +282,7 @@ public: /** Give preference to cores that have large minmal values. */ - sort_assumptions(asms); - + sort_assumptions(asms); m_last_index = std::min(m_last_index, asms.size()-1); m_last_index = 0; unsigned index = m_last_index>0?m_last_index-1:0; @@ -290,8 +295,6 @@ public: index = next_index(asms, index); } first = false; - IF_VERBOSE(3, verbose_stream() << "hill climb " << index << "\n";); - // IF_VERBOSE(3, verbose_stream() << "weight: " << get_weight(asms[0].get()) << " " << get_weight(asms[index-1].get()) << " num soft: " << index << "\n";); m_last_index = index; is_sat = check_sat(index, asms.c_ptr()); } @@ -307,8 +310,9 @@ public: if (r == l_true) { model_ref mdl; s().get_model(mdl); + TRACE("opt", tout << *mdl;); if (mdl.get()) { - update_assignment(mdl.get()); + update_assignment(mdl); } } return r; @@ -318,7 +322,7 @@ public: IF_VERBOSE(1, verbose_stream() << "found optimum\n";); m_lower.reset(); for (unsigned i = 0; i < m_soft.size(); ++i) { - m_assignment[i] = is_true(m_soft[i]); + m_assignment[i] = m_model->is_true(m_soft[i]); if (!m_assignment[i]) { m_lower += m_weights[i]; } @@ -347,7 +351,6 @@ public: lbool get_cores(vector& cores) { // assume m_s is unsat. lbool is_sat = l_false; - expr_ref_vector asms(m_asms); cores.reset(); exprs core; while (is_sat == l_false) { @@ -370,6 +373,10 @@ public: m_lower = m_upper; return l_true; } + // 1. remove all core literals from m_asms + // 2. re-add literals of higher weight than min-weight. + // 3. 'core' stores the core literals that are split afterwards + remove_soft(core, m_asms); split_core(core); cores.push_back(core); if (core.size() >= m_max_core_size) { @@ -378,15 +385,14 @@ public: if (cores.size() >= m_max_num_cores) { break; } - remove_soft(core, asms); - is_sat = check_sat_hill_climb(asms); + is_sat = check_sat_hill_climb(m_asms); } TRACE("opt", tout << "num cores: " << cores.size() << "\n"; for (auto const& c : cores) { display_vec(tout, c); } - tout << "num satisfying: " << asms.size() << "\n";); + tout << "num satisfying: " << m_asms.size() << "\n";); return is_sat; } @@ -394,7 +400,7 @@ public: void get_current_correction_set(exprs& cs) { model_ref mdl; s().get_model(mdl); - update_assignment(mdl.get()); + update_assignment(mdl); get_current_correction_set(mdl.get(), cs); } @@ -402,10 +408,10 @@ public: cs.reset(); if (!mdl) return; for (expr* a : m_asms) { - if (is_false(mdl, a)) { + if (mdl->is_false(a)) { cs.push_back(a); } - TRACE("opt", expr_ref tmp(m); mdl->eval(a, tmp, true); tout << mk_pp(a, m) << ": " << tmp << "\n";); + // TRACE("opt", tout << mk_pp(a, m) << ": " << (*mdl)(a) << "\n";); } TRACE("opt", display_vec(tout << "new correction set: ", cs);); } @@ -444,7 +450,7 @@ public: ++m_stats.m_num_cs; expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set);); - remove_core(corr_set); + remove_soft(corr_set, m_asms); rational w = split_core(corr_set); cs_max_resolve(corr_set, w); IF_VERBOSE(2, verbose_stream() << "(opt.maxres.correction-set " << corr_set.size() << ")\n";); @@ -484,18 +490,13 @@ public: void update_model(expr* def, expr* value) { SASSERT(is_uninterp_const(def)); if (m_csmodel) { - expr_ref val(m); - SASSERT(m_csmodel.get()); - if (m_csmodel->eval(value, val, true)) { - m_csmodel->register_decl(to_app(def)->get_decl(), val); - } + m_csmodel->register_decl(to_app(def)->get_decl(), (*m_csmodel)(value)); } } void process_unsat(exprs const& core) { IF_VERBOSE(3, verbose_stream() << "(maxres cs model valid: " << (m_csmodel.get() != nullptr) << " cs size:" << m_correction_set_size << " core: " << core.size() << ")\n";); expr_ref fml(m); - remove_core(core); SASSERT(!core.empty()); rational w = core_weight(core); TRACE("opt", display_vec(tout << "minimized core: ", core);); @@ -536,7 +537,7 @@ public: w = m_mus.get_best_model(mdl); } if (mdl.get() && w < m_upper) { - update_assignment(mdl.get()); + update_assignment(mdl); } return nullptr != mdl.get(); } @@ -707,10 +708,11 @@ public: s().assert_expr(fml); } - void update_assignment(model* mdl) { + void update_assignment(model_ref & mdl) { + mdl->set_model_completion(true); unsigned correction_set_size = 0; for (expr* a : m_asms) { - if (is_false(mdl, a)) { + if (mdl->is_false(a)) { ++correction_set_size; } } @@ -719,41 +721,45 @@ public: m_correction_set_size = correction_set_size; } + TRACE("opt", tout << *mdl;); + rational upper(0); - expr_ref tmp(m); + unsigned i = 0; for (expr* s : m_soft) { - if (!is_true(mdl, s)) { + TRACE("opt", tout << mk_pp(s, m) << ": " << (*mdl)(s) << " " << m_weights[i] << "\n";); + if (!mdl->is_true(s)) { upper += m_weights[i]; } ++i; } if (upper > m_upper) { + TRACE("opt", tout << "new upper: " << upper << " vs existing upper: " << m_upper << "\n";); return; } - if (!m_c.verify_model(m_index, mdl, upper)) { + if (!m_c.verify_model(m_index, mdl.get(), upper)) { return; } m_model = mdl; - m_c.model_updated(mdl); + m_c.model_updated(mdl.get()); - TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0);); + TRACE("opt", tout << "updated upper: " << upper << "\nmodel\n" << *m_model;); i = 0; for (expr* s : m_soft) { - m_assignment[i++] = is_true(s); + m_assignment[i++] = m_model->is_true(s); } // DEBUG_CODE(verify_assignment();); m_upper = upper; + trace(); add_upper_bound_block(); - } void add_upper_bound_block() { @@ -769,54 +775,28 @@ public: s().assert_expr(fml); } - bool is_true(model* mdl, expr* e) { - expr_ref tmp(m); - return mdl->eval(e, tmp, true) && m.is_true(tmp); - } - - bool is_false(model* mdl, expr* e) { - expr_ref tmp(m); - return mdl->eval(e, tmp, true) && m.is_false(tmp); - } - - bool is_true(expr* e) { - return is_true(m_model.get(), e); - } - - bool is_true(expr_ref_vector const& es) { - unsigned i = 0; - for (; i < es.size() && is_true(es[i]); ++i) { } - CTRACE("opt_bug", i < es.size(), tout << mk_pp(es[i], m) << "\n"; - model_smt2_pp(tout, m, *m_model, 0);); - return i == es.size(); - } - void remove_soft(exprs const& core, expr_ref_vector& asms) { - for (unsigned i = 0; i < asms.size(); ++i) { - if (core.contains(asms[i].get())) { - asms[i] = asms.back(); - asms.pop_back(); - --i; - } - } + TRACE("opt", tout << "before remove: " << asms << "\n";); + unsigned j = 0; + for (expr* a : asms) + if (!core.contains(a)) + asms[j++] = a; + asms.shrink(j); + TRACE("opt", tout << "after remove: " << asms << "\n";); } - void remove_core(exprs const& core) { - remove_soft(core, m_asms); - } - - virtual void updt_params(params_ref& p) { - maxsmt_solver_base::updt_params(p); - opt_params _p(p); - m_hill_climb = _p.maxres_hill_climb(); - m_add_upper_bound_block = _p.maxres_add_upper_bound_block(); - m_max_num_cores = _p.maxres_max_num_cores(); - m_max_core_size = _p.maxres_max_core_size(); - m_maximize_assignment = _p.maxres_maximize_assignment(); - m_max_correction_set_size = _p.maxres_max_correction_set_size(); - m_pivot_on_cs = _p.maxres_pivot_on_correction_set(); - m_wmax = _p.maxres_wmax(); - m_dump_benchmarks = _p.dump_benchmarks(); + virtual void updt_params(params_ref& _p) { + maxsmt_solver_base::updt_params(_p); + opt_params p(_p); + m_hill_climb = p.maxres_hill_climb(); + m_add_upper_bound_block = p.maxres_add_upper_bound_block(); + m_max_num_cores = p.maxres_max_num_cores(); + m_max_core_size = p.maxres_max_core_size(); + m_maximize_assignment = p.maxres_maximize_assignment(); + m_max_correction_set_size = p.maxres_max_correction_set_size(); + m_pivot_on_cs = p.maxres_pivot_on_correction_set(); + m_wmax = p.maxres_wmax(); + m_dump_benchmarks = p.dump_benchmarks(); } lbool init_local() { @@ -828,9 +808,8 @@ public: if (is_sat != l_true) { return is_sat; } - obj_map::iterator it = new_soft.begin(), end = new_soft.end(); - for (; it != end; ++it) { - add_soft(it->m_key, it->m_value); + for (auto const& kv : new_soft) { + add_soft(kv.m_key, kv.m_value); } m_max_upper = m_upper; m_found_feasible_optimum = false; @@ -843,10 +822,7 @@ public: virtual void commit_assignment() { if (m_found_feasible_optimum) { - TRACE("opt", tout << "Committing feasible solution\n"; - tout << m_defs; - tout << m_asms; - ); + TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;); s().assert_expr(m_defs); s().assert_expr(m_asms); } diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index fc5bd6bbb..c97b818cf 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -76,9 +76,7 @@ namespace opt { m_upper.reset(); m_assignment.reset(); for (unsigned i = 0; i < m_weights.size(); ++i) { - expr_ref val(m); - if (!m_model->eval(m_soft[i], val)) return false; - m_assignment.push_back(m.is_true(val)); + m_assignment.push_back(m.is_true(m_soft[i])); if (!m_assignment.back()) { m_upper += m_weights[i]; } @@ -232,9 +230,7 @@ namespace opt { m_msolver = nullptr; symbol const& maxsat_engine = m_c.maxsat_engine(); IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";); - TRACE("opt", tout << "maxsmt\n"; - s().display(tout); tout << "\n"; - ); + TRACE("opt_verbose", s().display(tout << "maxsmt\n") << "\n";); if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) { m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints); } @@ -455,10 +451,9 @@ namespace opt { maxsmt.get_model(m_model, labels); // TBD: is m_fm applied or not? unsigned j = 0; - expr_ref tmp(m); - for (unsigned i = 0; i < soft.size(); ++i) { - if (m_model->eval(soft[i].first, tmp) && m.is_true(tmp)) { - soft[j++] = soft[i]; + for (auto const& p : soft) { + if (m_model->is_true(p.first)) { + soft[j++] = p; } } soft.shrink(j); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 37dbd0817..af28d2254 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -341,6 +341,7 @@ namespace opt { void context::fix_model(model_ref& mdl) { if (mdl && !m_model_fixed.contains(mdl.get())) { + TRACE("opt", tout << "fix-model\n";); (*m_fm)(mdl); apply(m_model_converter, mdl); m_model_fixed.push_back(mdl.get()); @@ -350,7 +351,7 @@ namespace opt { void context::get_model_core(model_ref& mdl) { mdl = m_model; fix_model(mdl); - TRACE("opt", model_smt2_pp(tout, m, *mdl.get(), 0);); + TRACE("opt", tout << *mdl;); } void context::get_box_model(model_ref& mdl, unsigned index) { @@ -502,7 +503,8 @@ namespace opt { case O_MINIMIZE: is_ge = !is_ge; case O_MAXIMIZE: - if (mdl->eval(obj.m_term, val, true) && is_numeral(val, k)) { + val = (*mdl)(obj.m_term); + if (is_numeral(val, k)) { if (is_ge) { result = mk_ge(obj.m_term, val); } @@ -522,7 +524,7 @@ namespace opt { for (unsigned i = 0; i < sz; ++i) { terms.push_back(obj.m_terms[i]); coeffs.push_back(obj.m_weights[i]); - if (mdl->eval(obj.m_terms[i], val, true) && m.is_true(val)) { + if (mdl->is_true(obj.m_terms[i])) { k += obj.m_weights[i]; } else { @@ -1036,7 +1038,7 @@ namespace opt { buffer << prefix << (m_model_counter++) << ".smt2"; std::ofstream out(buffer.str()); if (out) { - model_smt2_pp(out, m, *mdl, 0); + out << *mdl; out.close(); } } @@ -1052,11 +1054,7 @@ namespace opt { expr_ref val(m); model_ref mdl = md->copy(); fix_model(mdl); - - if (!mdl->eval(term, val, true)) { - TRACE("opt", tout << "Term does not evaluate " << term << "\n";); - return false; - } + val = (*mdl)(term); unsigned bvsz; if (!m_arith.is_numeral(val, r) && !m_bv.is_numeral(val, r, bvsz)) { TRACE("opt", tout << "model does not evaluate objective to a value\n";); @@ -1195,9 +1193,9 @@ namespace opt { rational r; switch(obj.m_type) { case O_MINIMIZE: { - bool evaluated = m_model->eval(obj.m_term, val, true); - TRACE("opt", tout << obj.m_term << " " << val << " " << evaluated << " " << is_numeral(val, r) << "\n";); - if (evaluated && is_numeral(val, r)) { + val = (*m_model)(obj.m_term); + TRACE("opt", tout << obj.m_term << " " << val << " " << is_numeral(val, r) << "\n";); + if (is_numeral(val, r)) { inf_eps val = inf_eps(obj.m_adjust_value(r)); TRACE("opt", tout << "adjusted value: " << val << "\n";); if (is_lower) { @@ -1210,9 +1208,9 @@ namespace opt { break; } case O_MAXIMIZE: { - bool evaluated = m_model->eval(obj.m_term, val, true); + val = (*m_model)(obj.m_term); TRACE("opt", tout << obj.m_term << " " << val << "\n";); - if (evaluated && is_numeral(val, r)) { + if (is_numeral(val, r)) { inf_eps val = inf_eps(obj.m_adjust_value(r)); TRACE("opt", tout << "adjusted value: " << val << "\n";); if (is_lower) { @@ -1227,15 +1225,10 @@ namespace opt { case O_MAXSMT: { bool ok = true; for (unsigned j = 0; ok && j < obj.m_terms.size(); ++j) { - bool evaluated = m_model->eval(obj.m_terms[j], val, true); + val = (*m_model)(obj.m_terms[j]); TRACE("opt", tout << mk_pp(obj.m_terms[j], m) << " " << val << "\n";); - if (evaluated) { - if (!m.is_true(val)) { - r += obj.m_weights[j]; - } - } - else { - ok = false; + if (!m.is_true(val)) { + r += obj.m_weights[j]; } } if (ok) { @@ -1485,7 +1478,7 @@ namespace opt { } if (is_internal && mc) { - mc->collect(visitor); + mc->set_env(&visitor); } param_descrs descrs; @@ -1531,7 +1524,9 @@ namespace opt { if (is_internal && mc) { mc->display(out); } - + if (is_internal && mc) { + mc->set_env(nullptr); + } out << "(check-sat)\n"; return out.str(); } @@ -1545,7 +1540,7 @@ namespace opt { model_ref mdl; get_model(mdl); for (expr * f : fmls) { - if (!mdl->eval(f, tmp) || !m.is_true(tmp)) { + if (!mdl->is_true(f)) { //IF_VERBOSE(0, m_fm->display(verbose_stream() << "fm\n")); IF_VERBOSE(0, m_model_converter->display(verbose_stream() << "mc\n")); IF_VERBOSE(0, verbose_stream() << "Failed to validate " << mk_pp(f, m) << "\n" << tmp << "\n"); @@ -1559,18 +1554,14 @@ namespace opt { void context::validate_maxsat(symbol const& id) { maxsmt& ms = *m_maxsmts.find(id); TRACE("opt", tout << "Validate: " << id << "\n";); - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; + for (objective const& obj : m_objectives) { if (obj.m_id == id && obj.m_type == O_MAXSMT) { SASSERT(obj.m_type == O_MAXSMT); rational value(0); expr_ref val(m); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { - bool evaluated = m_model->eval(obj.m_terms[i], val); - SASSERT(evaluated); - CTRACE("opt", evaluated && !m.is_true(val) && !m.is_false(val), tout << mk_pp(obj.m_terms[i], m) << " " << val << "\n";); - CTRACE("opt", !evaluated, tout << mk_pp(obj.m_terms[i], m) << "\n";); - if (evaluated && !m.is_true(val)) { + auto const& t = obj.m_terms[i]; + if (!m_model->is_true(t)) { value += obj.m_weights[i]; } // TBD: check that optimal was not changed. @@ -1595,14 +1586,13 @@ namespace opt { if (m_optsmt.objective_is_model_valid(obj.m_index) && n.get_infinity().is_zero() && n.get_infinitesimal().is_zero() && - m_model->eval(obj.m_term, val) && - is_numeral(val, r1)) { + is_numeral((*m_model)(obj.m_term), r1)) { rational r2 = n.get_rational(); if (obj.m_type == O_MINIMIZE) { r1.neg(); } CTRACE("opt", r1 != r2, tout << obj.m_term << " evaluates to " << r1 << " but has objective " << r2 << "\n";); - CTRACE("opt", r1 != r2, model_smt2_pp(tout, m, *m_model, 0);); + CTRACE("opt", r1 != r2, tout << *m_model;); SASSERT(r1 == r2); } break; @@ -1610,8 +1600,7 @@ namespace opt { case O_MAXSMT: { rational value(0); for (unsigned i = 0; i < obj.m_terms.size(); ++i) { - bool evaluated = m_model->eval(obj.m_terms[i], val); - if (evaluated && !m.is_true(val)) { + if (!m_model->is_true(obj.m_terms[i])) { value += obj.m_weights[i]; } // TBD: check that optimal was not changed. diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 702702ef4..a461d4a22 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -318,7 +318,7 @@ namespace opt { m_s->get_labels(m_labels); for (unsigned i = 0; i < ors.size(); ++i) { expr_ref tmp(m); - if (m_model->eval(ors[i].get(), tmp) && m.is_true(tmp)) { + if (m_model->is_true(ors[i].get())) { m_lower[i] = m_upper[i]; ors[i] = m.mk_false(); disj[i] = m.mk_false(); diff --git a/src/opt/pb_sls.cpp b/src/opt/pb_sls.cpp index e28c3cd3d..9054e2b00 100644 --- a/src/opt/pb_sls.cpp +++ b/src/opt/pb_sls.cpp @@ -179,7 +179,7 @@ namespace smt { m_orig_model = mdl; for (unsigned i = 0; i < m_var2decl.size(); ++i) { expr_ref tmp(m); - m_assignment[i] = mdl->eval(m_var2decl[i], tmp) && m.is_true(tmp); + m_assignment[i] = mdl->is_true(m_var2decl[i]); } } @@ -343,10 +343,7 @@ namespace smt { for (unsigned i = 0; i < m_clauses.size(); ++i) { if (!eval(m_clauses[i])) { m_hard_false.insert(i); - expr_ref tmp(m); - if (!m_orig_model->eval(m_orig_clauses[i].get(), tmp)) { - return; - } + expr_ref tmp = (*m_orig_model)(m_orig_clauses[i].get()); IF_VERBOSE(0, verbose_stream() << "original evaluation: " << tmp << "\n"; verbose_stream() << mk_pp(m_orig_clauses[i].get(), m) << "\n"; @@ -521,14 +518,13 @@ namespace smt { literal mk_aux_literal(expr* f) { unsigned var; - expr_ref tmp(m); if (!m_decl2var.find(f, var)) { var = m_hard_occ.size(); SASSERT(m_var2decl.size() == var); SASSERT(m_soft_occ.size() == var); m_hard_occ.push_back(unsigned_vector()); m_soft_occ.push_back(unsigned_vector()); - m_assignment.push_back(m_orig_model->eval(f, tmp) && m.is_true(tmp)); + m_assignment.push_back(m_orig_model->is_true(f)); m_decl2var.insert(f, var); m_var2decl.push_back(f); } diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 9c45e42a2..6e7e6ec78 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -73,8 +73,7 @@ namespace opt { unsigned first = 0; it = soft.begin(); for (; it != end; ++it) { - expr_ref tmp(m); - if (m_model->eval(it->m_key, tmp) && m.is_true(tmp)) { + if (m_model->is_true(it->m_key)) { unsigned n = it->m_value.get_unsigned(); while (n > 0) { s().assert_expr(out[first]); @@ -121,8 +120,7 @@ namespace opt { } bool is_true(expr* e) { - expr_ref tmp(m); - return m_model->eval(e, tmp) && m.is_true(tmp); + return m_model->is_true(e); } // definitions used for sorting network diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 513c68d6e..97231f69e 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -120,8 +120,7 @@ namespace opt { } bool is_true(expr* e) { - expr_ref tmp(m); - return m_model->eval(e, tmp) && m.is_true(tmp); + return m_model->is_true(e); } void update_assignment() { @@ -307,9 +306,8 @@ namespace opt { } void update_model(expr* def, expr* value) { - expr_ref val(m); - if (m_model && m_model->eval(value, val, true)) { - m_model->register_decl(to_app(def)->get_decl(), val); + if (m_model) { + m_model->register_decl(to_app(def)->get_decl(), (*m_model)(value)); } } diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 9276b60cd..016c6f4e5 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2611,8 +2611,8 @@ namespace smt2 { expr ** expr_it = expr_stack().c_ptr() + spos; expr ** expr_end = expr_it + m_cached_strings.size(); for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) { - expr_ref v(m()); - md->eval(*expr_it, v, true); + model::scoped_model_completion _scm(md, true); + expr_ref v = (*md)(*expr_it); if (i > 0) m_ctx.regular_stream() << "\n "; m_ctx.regular_stream() << "(" << m_cached_strings[i] << " "; diff --git a/src/qe/qe_arrays.cpp b/src/qe/qe_arrays.cpp index a4da829a0..4c81418b6 100644 --- a/src/qe/qe_arrays.cpp +++ b/src/qe/qe_arrays.cpp @@ -1181,9 +1181,8 @@ namespace qe { indices(ast_manager& m, model& model, unsigned n, expr* const* vars): m_values(m), m_vars(vars) { expr_ref val(m); - for (unsigned i = 0; i < n; ++i) { - VERIFY(model.eval(vars[i], val)); - m_values.push_back(val); + for (unsigned i = 0; i < n; ++i) { + m_values.push_back(model(vars[i])); } } }; @@ -1269,7 +1268,7 @@ namespace qe { args.push_back (s); args.append(idxs[i].m_values.size(), idxs[i].m_vars); sel = a.mk_select (args.size (), args.c_ptr ()); - VERIFY (model.eval (sel, val)); + val = model(sel); model.register_decl (var->get_decl (), val); args[0] = result; diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index 87ae97857..5499d638d 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -42,8 +42,7 @@ namespace qe { } bool operator()(model& model, app* var, app_ref_vector& vars, expr_ref_vector& lits) { - expr_ref val(m); - VERIFY(model.eval(var, val)); + expr_ref val = model(var); SASSERT(is_app(val)); TRACE("qe", tout << mk_pp(var, m) << " := " << val << "\n";); m_val = to_app(val); diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp index 438f1c061..78dcbfd16 100644 --- a/src/qe/qe_mbp.cpp +++ b/src/qe/qe_mbp.cpp @@ -66,7 +66,7 @@ expr_ref project_plugin::pick_equality(ast_manager& m, model& model, expr* t) { app* alit = to_app(t); for (expr * e1 : *alit) { expr *e2; - VERIFY(model.eval(e1, val)); + val = model(e1); if (val2expr.find(val, e2)) { return expr_ref(m.mk_eq(e1, e2), m); } @@ -501,7 +501,7 @@ public: expr_ref val(m); model_evaluator eval(model); for (expr * f : fmls) { - VERIFY(model.eval(f, val) && m.is_true(val)); + VERIFY(model.is_true(f)); } return true; } @@ -538,7 +538,7 @@ public: var = new_vars.back(); new_vars.pop_back(); expr_safe_replace sub(m); - VERIFY(model.eval(var, val)); + val = model(var); sub.insert(var, val); for (unsigned i = 0; i < fmls.size(); ++i) { sub(fmls[i].get(), tmp); diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 64cde4b1d..a2e8fd8b1 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -516,8 +516,8 @@ namespace qe { expr_ref val_a(m), val_b(m); expr* a = it->m_key; expr* b = it->m_value; - VERIFY(model.eval(a, val_a)); - VERIFY(model.eval(b, val_b)); + val_a = model(a); + val_b = model(b); if (val_a != val_b) { TRACE("qe", tout << mk_pp(a, m) << " := " << val_a << "\n"; @@ -1060,11 +1060,9 @@ namespace qe { } bool validate_assumptions(model& mdl, expr_ref_vector const& core) { - for (unsigned i = 0; i < core.size(); ++i) { - expr_ref val(m); - VERIFY(mdl.eval(core[i], val)); - if (!m.is_true(val)) { - TRACE("qe", tout << "component of core is not true: " << mk_pp(core[i], m) << "\n";); + for (expr* c : core) { + if (!mdl.is_true(c)) { + TRACE("qe", tout << "component of core is not true: " << mk_pp(c, m) << "\n";); return false; } } @@ -1111,14 +1109,10 @@ namespace qe { bool validate_model(model& mdl, unsigned sz, expr* const* fmls) { expr_ref val(m); for (unsigned i = 0; i < sz; ++i) { - if (!m_model->eval(fmls[i], val) && !m.canceled()) { - TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";); + if (!m_model->is_true(fmls[i]) && !m.canceled()) { + TRACE("qe", tout << "Formula does not evaluate to true in model: " << mk_pp(fmls[i], m) << "\n";); return false; } - if (!m.is_true(val)) { - TRACE("qe", tout << mk_pp(fmls[i], m) << " evaluates to " << val << " in model\n";); - return false; - } } return true; } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 75290946a..5f0fbec16 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -968,9 +968,9 @@ model_converter* sat2goal::mc::translate(ast_translation& translator) { return result; } -void sat2goal::mc::collect(ast_pp_util& visitor) { +void sat2goal::mc::set_env(ast_pp_util* visitor) { flush_gmc(); - if (m_gmc) m_gmc->collect(visitor); + if (m_gmc) m_gmc->set_env(visitor); } void sat2goal::mc::display(std::ostream& out) { diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index 32b89fe5d..d86b2d7e4 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -92,7 +92,7 @@ public: void operator()(model_ref& md) override; void operator()(expr_ref& fml) override; model_converter* translate(ast_translation& translator) override; - void collect(ast_pp_util& visitor) override; + void set_env(ast_pp_util* visitor) override; void display(std::ostream& out) override; void get_units(obj_map& units) override; app* var2expr(sat::bool_var v) const { return m_var2expr.get(v, nullptr); } diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp index 5af5bfdd7..0a2a8f4a1 100644 --- a/src/shell/opt_frontend.cpp +++ b/src/shell/opt_frontend.cpp @@ -121,10 +121,8 @@ static unsigned parse_opt(std::istream& in, opt_format f) { expr_ref_vector hard(m); opt.get_hard_constraints(hard); for (expr* h : hard) { - expr_ref tmp(m); - VERIFY(mdl->eval(h, tmp)); - if (!m.is_true(tmp)) { - std::cout << mk_pp(h, m) << " " << tmp << "\n"; + if (!mdl->is_true(h)) { + std::cout << mk_pp(h, m) << " evaluates to: " << (*mdl)(h) << "\n"; } } } diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index ff62dacec..c35a0b180 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -569,10 +569,9 @@ namespace smt { if (m_context) { ast_manager & m = m_context->get_manager(); out << "patterns:\n"; - ptr_vector::const_iterator it = m_patterns.begin(); - ptr_vector::const_iterator end = m_patterns.end(); - for (; it != end; ++it) - out << mk_pp(*it, m) << "\n"; + for (expr* p : m_patterns) { + out << mk_pp(p, m) << "\n"; + } } #endif out << "function: " << m_root_lbl->get_name(); @@ -831,10 +830,8 @@ namespace smt { void init(code_tree * t, quantifier * qa, app * mp, unsigned first_idx) { SASSERT(m_ast_manager.is_pattern(mp)); #ifdef Z3DEBUG - svector::iterator it = m_mark.begin(); - svector::iterator end = m_mark.end(); - for (; it != end; ++it) { - SASSERT(*it == NOT_CHECKED); + for (auto cm : m_mark) { + SASSERT(cm == NOT_CHECKED); } #endif m_tree = t; @@ -1711,14 +1708,12 @@ namespace smt { set_next(curr, new_child_head1); // set: new_child_head1:CHOOSE(new_child_head2) -> i1 -> i2 -> first_child_head curr = new_child_head1; - ptr_vector::iterator it2 = m_incompatible.begin(); - ptr_vector::iterator end2 = m_incompatible.end(); - for (; it2 != end2; ++it2) { + for (instruction* inc : m_incompatible) { if (curr == new_child_head1) - curr->m_next = *it2; // new_child_head1 is a new node, I don't need to save trail + curr->m_next = inc; // new_child_head1 is a new node, I don't need to save trail else - set_next(curr, *it2); - curr = *it2; + set_next(curr, inc); + curr = inc; } set_next(curr, first_child_head); // build new_child_head2:NOOP -> linearise() @@ -3353,10 +3348,7 @@ namespace smt { void update_vars(unsigned short var_id, path * p, quantifier * qa, app * mp) { paths & var_paths = m_var_paths[var_id]; bool found = false; - paths::iterator it = var_paths.begin(); - paths::iterator end = var_paths.end(); - for (; it != end; ++it) { - path * curr_path = *it; + for (path* curr_path : var_paths) { if (is_equal(p, curr_path)) found = true; func_decl * lbl1 = curr_path->m_label; @@ -3647,18 +3639,12 @@ namespace smt { TRACE("incremental_matcher", tout << "pp: plbls1: " << plbls1 << ", plbls2: " << plbls2 << "\n";); TRACE("mam_info", tout << "pp: " << plbls1.size() * plbls2.size() << "\n";); if (!plbls1.empty() && !plbls2.empty()) { - approx_set::iterator it1 = plbls1.begin(); - approx_set::iterator end1 = plbls1.end(); - for (; it1 != end1; ++it1) { + for (unsigned plbl1 : plbls1) { if (m_context.get_cancel_flag()) { break; } - unsigned plbl1 = *it1; SASSERT(plbls1.may_contain(plbl1)); - approx_set::iterator it2 = plbls2.begin(); - approx_set::iterator end2 = plbls2.end(); - for (; it2 != end2; ++it2) { - unsigned plbl2 = *it2; + for (unsigned plbl2 : plbls2) { SASSERT(plbls2.may_contain(plbl2)); unsigned n_plbl1 = plbl1; unsigned n_plbl2 = plbl2; diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 13fd9e6ea..4cb331661 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -637,15 +637,14 @@ namespace smt { model_ref mdl; for (unsigned i = 0; i < unfixed.size(); ++i) { push(); - for (unsigned j = 0; j < assumptions.size(); ++j) { - assert_expr(assumptions[j]); - } + for (expr* a : assumptions) + assert_expr(a); TRACE("context", tout << "checking unfixed: " << mk_pp(unfixed[i], m) << "\n";); lbool is_sat = check(); SASSERT(is_sat != l_false); if (is_sat == l_true) { get_model(mdl); - mdl->eval(unfixed[i], tmp); + tmp = (*mdl)(unfixed[i]); if (m.is_value(tmp)) { tmp = m.mk_not(m.mk_eq(unfixed[i], tmp)); assert_expr(tmp); diff --git a/src/smt/smt_implied_equalities.cpp b/src/smt/smt_implied_equalities.cpp index 0b944c145..9119119d3 100644 --- a/src/smt/smt_implied_equalities.cpp +++ b/src/smt/smt_implied_equalities.cpp @@ -199,7 +199,7 @@ namespace smt { for (unsigned i = 0; i < terms.size(); ++i) { expr* t = terms[i].term; - model->eval(t, vl); + vl = (*model)(t); TRACE("get_implied_equalities", tout << mk_pp(t, m) << " |-> " << mk_pp(vl, m) << "\n";); reduce_value(model, vl); if (!m.is_value(vl)) { diff --git a/src/solver/mus.cpp b/src/solver/mus.cpp index b3d6c9ad9..094b27ed3 100644 --- a/src/solver/mus.cpp +++ b/src/solver/mus.cpp @@ -332,8 +332,7 @@ struct mus::imp { m_solver.get_model(mdl); rational w; for (unsigned i = 0; i < m_soft.size(); ++i) { - mdl->eval(m_soft[i].get(), tmp); - if (!m.is_true(tmp)) { + if (!mdl->is_true(m_soft.get(i))) { w += m_weights[i]; } } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 84b5eb588..186449545 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -44,7 +44,7 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum ast_pp_util visitor(get_manager()); model_converter_ref mc = get_model_converter(); if (mc.get()) { - mc->collect(visitor); + mc->set_env(&visitor); } visitor.collect(fmls); visitor.collect(n, assumptions); @@ -52,6 +52,7 @@ std::ostream& solver::display(std::ostream & out, unsigned n, expr* const* assum visitor.display_asserts(out, fmls, true); if (mc.get()) { mc->display(out); + mc->set_env(nullptr); } return out; } diff --git a/src/tactic/generic_model_converter.cpp b/src/tactic/generic_model_converter.cpp index 1911edf3b..0790c962a 100644 --- a/src/tactic/generic_model_converter.cpp +++ b/src/tactic/generic_model_converter.cpp @@ -114,11 +114,16 @@ model_converter * generic_model_converter::translate(ast_translation & translato return res; } -void generic_model_converter::collect(ast_pp_util& visitor) { - m_env = &visitor.env(); - for (entry const& e : m_entries) { - visitor.coll.visit_func(e.m_f); - if (e.m_def) visitor.coll.visit(e.m_def); +void generic_model_converter::set_env(ast_pp_util* visitor) { + if (!visitor) { + m_env = nullptr; + } + else { + m_env = &visitor->env(); + for (entry const& e : m_entries) { + visitor->coll.visit_func(e.m_f); + if (e.m_def) visitor->coll.visit(e.m_def); + } } } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index d303fb2e3..a190b8525 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -68,7 +68,7 @@ public: model_converter * translate(ast_translation & translator) override; - void collect(ast_pp_util& visitor) override; + void set_env(ast_pp_util* visitor) override; void operator()(expr_ref& fml) override; diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/tactic/horn_subsume_model_converter.cpp index 0d49a769e..eeb2967f2 100644 --- a/src/tactic/horn_subsume_model_converter.cpp +++ b/src/tactic/horn_subsume_model_converter.cpp @@ -195,8 +195,7 @@ void horn_subsume_model_converter::operator()(model_ref& mr) { SASSERT(m.is_bool(body)); TRACE("mc", tout << "eval: " << h->get_name() << "\n" << body << "\n";); - expr_ref tmp(body); - mr->eval(tmp, body); + body = (*mr)(body); TRACE("mc", tout << "to:\n" << body << "\n";); diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index b39940366..89e2b6602 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -43,6 +43,16 @@ void model_converter::display_del(std::ostream& out, func_decl* f) const { } } +void model_converter::set_env(ast_pp_util* visitor) { + if (visitor) { + m_env = &visitor->env(); + } + else { + m_env = nullptr; + } +} + + void model_converter::display_add(std::ostream& out, ast_manager& m) { // default printer for converter that adds entries model_ref mdl = alloc(model, m); @@ -91,9 +101,9 @@ public: return this->translate_core(translator); } - void collect(ast_pp_util& visitor) override { - this->m_c1->collect(visitor); - this->m_c2->collect(visitor); + void set_env(ast_pp_util* visitor) override { + this->m_c1->set_env(visitor); + this->m_c2->set_env(visitor); } }; @@ -125,9 +135,8 @@ public: } void operator()(expr_ref& fml) override { - expr_ref r(m_model->get_manager()); - m_model->eval(fml, r, false); - fml = r; + model::scoped_model_completion _scm(m_model, false); + fml = (*m_model)(fml); } void get_units(obj_map& fmls) override { diff --git a/src/tactic/model_converter.h b/src/tactic/model_converter.h index cd8fb5ee3..9c5b72830 100644 --- a/src/tactic/model_converter.h +++ b/src/tactic/model_converter.h @@ -80,7 +80,7 @@ public: virtual model_converter * translate(ast_translation & translator) = 0; - virtual void collect(ast_pp_util& visitor) { m_env = &visitor.env(); } + virtual void set_env(ast_pp_util* visitor); /** \brief we are adding a formula to the context of the model converter. diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp index 7836ab70f..f5b5ec1b2 100644 --- a/src/tactic/sls/sls_engine.cpp +++ b/src/tactic/sls/sls_engine.cpp @@ -100,36 +100,27 @@ void sls_engine::checkpoint() { } bool sls_engine::full_eval(model & mdl) { - bool res = true; - - unsigned sz = m_assertions.size(); - for (unsigned i = 0; i < sz && res; i++) { - checkpoint(); - expr_ref o(m_manager); - - if (!mdl.eval(m_assertions[i], o, true)) - exit(ERR_INTERNAL_FATAL); - - res = m_manager.is_true(o.get()); - } - - TRACE("sls", tout << "Evaluation: " << res << std::endl;); - - return res; + model::scoped_model_completion _scm(mdl, true); + for (expr* a : m_assertions) { + checkpoint(); + if (!mdl.is_true(a)) { + TRACE("sls", tout << "Evaluation: false\n";); + return false; + } + } + return true; } double sls_engine::top_score() { double top_sum = 0.0; - unsigned sz = m_assertions.size(); - for (unsigned i = 0; i < sz; i++) { - expr * e = m_assertions[i]; + for (expr* e : m_assertions) { top_sum += m_tracker.get_score(e); } TRACE("sls_top", tout << "Score distribution:"; - for (unsigned i = 0; i < sz; i++) - tout << " " << m_tracker.get_score(m_assertions[i]); - tout << " AVG: " << top_sum / (double)sz << std::endl;); + for (expr* e : m_assertions) + tout << " " << m_tracker.get_score(e); + tout << " AVG: " << top_sum / (double)m_assertions.size() << std::endl;); m_tracker.set_top_sum(top_sum);