From 60888a93eb24d4f5ce0b3defaaeccfba2c977af7 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 13:42:26 -0700 Subject: [PATCH 1/7] Minor fixes to model --- src/model/model.h | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/src/model/model.h b/src/model/model.h index 3fda2832f..429e7b51a 100644 --- a/src/model/model.h +++ b/src/model/model.h @@ -24,10 +24,13 @@ Revision History: #include "util/ref.h" #include "ast/ast_translation.h" +class model; +typedef ref model_ref; + class model : public model_core { protected: typedef obj_map*> sort2universe; - + ptr_vector m_usorts; sort2universe m_usort2universe; model_evaluator m_mev; @@ -42,10 +45,10 @@ public: void copy_usort_interps(model const & source); 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); - + expr * get_some_value(sort * s) override; ptr_vector const & get_universe(sort * s) const override; unsigned get_num_uninterpreted_sorts() const override; @@ -78,25 +81,21 @@ public: bool m_old_completion; model& m_model; public: - scoped_model_completion(model& m, bool c): + scoped_model_completion(model& m, bool c): m_old_completion(m.m_mev.get_model_completion()), m_model(m) { m.set_model_completion(c); } -#if 0 - scoped_model_completion(model_ref& m, bool c): + scoped_model_completion(model_ref& m, bool c): m_old_completion(m->m_mev.get_model_completion()), m_model(*m.get()) { m->set_model_completion(c); } -#endif ~scoped_model_completion() { m_model.set_model_completion(m_old_completion); } }; - + }; -typedef ref model_ref; #endif /* MODEL_H_ */ - From fffc8489bff01631591aea95be1e5b18e4c938dd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 13:43:30 -0700 Subject: [PATCH 2/7] Switched compute_implicant_literals to use new model API --- src/api/api_qe.cpp | 7 +- src/muz/spacer/spacer_context.cpp | 8 +- src/muz/spacer/spacer_util.cpp | 309 +++++++++++++++--------------- src/muz/spacer/spacer_util.h | 46 ++--- 4 files changed, 188 insertions(+), 182 deletions(-) diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 2516aacfb..0073ef274 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -52,7 +52,7 @@ extern "C" Z3_TRY; LOG_Z3_qe_model_project (c, m, num_bounds, bound, body); RESET_ERROR_CODE(); - + app_ref_vector vars(mk_c(c)->m ()); if (!to_apps(num_bounds, bound, vars)) { SET_ERROR_CODE (Z3_INVALID_ARG); @@ -119,11 +119,8 @@ extern "C" facts.push_back (to_expr (fml)); flatten_and (facts); - spacer::model_evaluator_util mev (mk_c(c)->m()); - mev.set_model (*model); - expr_ref_vector lits (mk_c(c)->m()); - spacer::compute_implicant_literals (mev, facts, lits); + spacer::compute_implicant_literals (*model, facts, lits); expr_ref result (mk_c(c)->m ()); result = mk_and (lits); diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 03093ab63..db1153de3 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -366,7 +366,7 @@ pob *derivation::create_next_child () // get an implicant of the summary expr_ref_vector u(m), lits (m); u.push_back (rf->get ()); - compute_implicant_literals (mev, u, lits); + compute_implicant_literals (*model, u, lits); expr_ref v(m); v = mk_and (lits); @@ -1172,7 +1172,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, // -- pick an implicant expr_ref_vector lits(m); - compute_implicant_literals (mev, summary, lits); + compute_implicant_literals (*mev.get_model(), summary, lits); return mk_and(lits); } @@ -3599,7 +3599,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, if (ctx.reach_dnf()) { expr_ref_vector u(m), lits(m); u.push_back (res); - compute_implicant_literals (mev, u, lits); + compute_implicant_literals (*mev.get_model(), u, lits); res = mk_and (lits); } @@ -3670,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r, forms.push_back(pt.get_transition(r)); forms.push_back(n.post()); - compute_implicant_literals (mev, forms, lits); + compute_implicant_literals (*mev.get_model(), forms, lits); expr_ref phi = mk_and (lits); // primed variables of the head diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index f53577b5b..3eb18b0e5 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -405,67 +405,67 @@ namespace spacer { namespace { class implicant_picker { - model_evaluator_util &m_mev; + model &m_model; ast_manager &m; arith_util m_arith; expr_ref_vector m_todo; expr_mark m_visited; + // add literal to the implicant + // applies lightweight normalization + void add_literal(expr *e, expr_ref_vector &out) { + SASSERT(m.is_bool(e)); - void add_literal (expr *e, expr_ref_vector &out) { - SASSERT (m.is_bool (e)); + expr_ref res(m), v(m); + v = m_model(e); + // the literal must have a value + SASSERT(m.is_true(v) || m.is_false(v)); - expr_ref res (m), v(m); - m_mev.eval (e, v, false); - SASSERT (m.is_true (v) || m.is_false (v)); + res = m.is_false(v) ? m.mk_not(e) : e; - res = m.is_false (v) ? m.mk_not (e) : e; - - if (m.is_distinct (res)) { - // -- (distinct a b) == (not (= a b)) + if (m.is_distinct(res)) { + // --(distinct a b) == (not (= a b)) if (to_app(res)->get_num_args() == 2) { - res = m.mk_eq (to_app(res)->get_arg(0), to_app(res)->get_arg(1)); - res = m.mk_not (res); + res = m.mk_eq(to_app(res)->get_arg(0), + to_app(res)->get_arg(1)); + res = m.mk_not(res); } } expr *nres, *f1, *f2; if (m.is_not(res, nres)) { - // -- (not (xor a b)) == (= a b) + // --(not (xor a b)) == (= a b) if (m.is_xor(nres, f1, f2)) - { res = m.mk_eq(f1, f2); } - + res = m.mk_eq(f1, f2); // -- split arithmetic inequality - else if (m.is_eq (nres, f1, f2) && m_arith.is_int_real (f1)) { + else if (m.is_eq(nres, f1, f2) && m_arith.is_int_real(f1)) { expr_ref u(m); u = m_arith.mk_lt(f1, f2); - if (m_mev.eval (u, v, false) && m.is_true (v)) - { res = u; } - else - { res = m_arith.mk_lt(f2, f1); } + res = m_model.is_true(u) ? u : m_arith.mk_lt(f2, f1); } } - if (!m_mev.is_true (res)) { - verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n"; + if (!m_model.is_true(res)) { + verbose_stream() << "Bad literal: " << res << "\n"; } - SASSERT (m_mev.is_true (res)); - out.push_back (res); + SASSERT(m_model.is_true(res)); + out.push_back(res); } void process_app(app *a, expr_ref_vector &out) { - if (m_visited.is_marked(a)) { return; } - SASSERT (m.is_bool (a)); + if (m_visited.is_marked(a)) return; + SASSERT(m.is_bool(a)); expr_ref v(m); - m_mev.eval (a, v, false); + v = m_model(a); bool is_true = m.is_true(v); if (!is_true && !m.is_false(v)) return; expr *na, *f1, *f2, *f3; - if (m.is_true(a) || m.is_false(a)) { + SASSERT(!m.is_false(a)); + if (m.is_true(a)) { // noop } else if (a->get_family_id() != m.get_basic_family_id()) { @@ -479,14 +479,15 @@ namespace { } else if (m.is_distinct(a)) { if (!is_true) { - f1 = qe::project_plugin::pick_equality(m, *m_mev.get_model(), a); + f1 = qe::project_plugin::pick_equality(m, m_model, a); m_todo.push_back(f1); } else if (a->get_num_args() == 2) { add_literal(a, out); } else { - m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), a->get_args())); + m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), + a->get_args())); } } else if (m.is_and(a)) { @@ -494,8 +495,8 @@ namespace { m_todo.append(a->get_num_args(), a->get_args()); } else { - for (expr* e : *a) { - if (m_mev.is_false(e)) { + for(expr* e : *a) { + if (m_model.is_false(e)) { m_todo.push_back(e); break; } @@ -506,17 +507,19 @@ namespace { if (!is_true) m_todo.append(a->get_num_args(), a->get_args()); else { - for (expr * e : *a) { - if (m_mev.is_true(e)) { + for(expr * e : *a) { + if (m_model.is_true(e)) { m_todo.push_back(e); break; } } } } - else if (m.is_eq(a, f1, f2) || (is_true && m.is_not(a, na) && m.is_xor (na, f1, f2))) { + else if (m.is_eq(a, f1, f2) || + (is_true && 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))) + if (m.is_bool(f1) && + (!is_uninterp_const(f1) || !is_uninterp_const(f2))) m_todo.append(a->get_num_args(), a->get_args()); else add_literal(a, out); @@ -526,19 +529,19 @@ namespace { if (m.are_equal(f2, f3)) { m_todo.push_back(f2); } - else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { + else if (m_model.is_true(f2) && m_model.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)) { + else if (m_model.is_false(f2) && m_model.is_false(f3)) { m_todo.push_back(f2); m_todo.push_back(f3); } - else if (m_mev.is_true(f1)) { + else if (m_model.is_true(f1)) { m_todo.push_back(f1); m_todo.push_back(f2); } - else if (m_mev.is_false(f1)) { + else if (m_model.is_false(f1)) { m_todo.push_back(f1); m_todo.push_back(f3); } @@ -548,16 +551,18 @@ namespace { } else if (m.is_implies(a, f1, f2)) { if (is_true) { - if (m_mev.is_true(f2)) + if (m_model.is_true(f2)) m_todo.push_back(f2); - else if (m_mev.is_false(f1)) + else if (m_model.is_false(f1)) m_todo.push_back(f1); } else m_todo.append(a->get_num_args(), a->get_args()); } else { - IF_VERBOSE(0, verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n"); + IF_VERBOSE(0, + verbose_stream() << "Unexpected expression: " + << mk_pp(a, m) << "\n"); UNREACHABLE(); } } @@ -574,70 +579,72 @@ namespace { m_todo.pop_back(); process_app(a, out); m_visited.mark(a, true); - } while (!m_todo.empty()); + } while(!m_todo.empty()); } bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) { m_visited.reset(); - bool is_true = m_mev.is_true (in); + bool is_true = m_model.is_true(in); - for (expr* e : in) { - if (is_true || m_mev.is_true(e)) { + for(expr* e : in) { + if (is_true || m_model.is_true(e)) { pick_literals(e, out); } } - m_visited.reset (); + 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) {} + implicant_picker(model &mdl) : + m_model(mdl), m(m_model.get_manager()), m_arith(m), m_todo(m) {} - void operator() (expr_ref_vector &in, expr_ref_vector& out) { - pick_implicant (in, out); + void operator()(expr_ref_vector &in, expr_ref_vector& out) { + model::scoped_model_completion _sc_(m_model, false); + pick_implicant(in, out); } }; } - void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, + void compute_implicant_literals(model &mdl, + expr_ref_vector &formula, expr_ref_vector &res) { // flatten the formula and remove all trivial literals - // TBD: not clear why there is a dependence on it (other than + // TBD: not clear why there is a dependence on it(other than // not handling of Boolean constants by implicant_picker), however, // it was a source of a problem on a benchmark flatten_and(formula); if (formula.empty()) {return;} - implicant_picker ipick (mev); - ipick (formula, res); + implicant_picker ipick(mdl); + ipick(formula, res); } void simplify_bounds_old(expr_ref_vector& cube) { ast_manager& m = cube.m(); scoped_no_proof _no_pf_(m); goal_ref g(alloc(goal, m, false, false, false)); - for (expr* c : cube) + for(expr* c : cube) g->assert_expr(c); goal_ref_buffer result; tactic_ref simplifier = mk_arith_bounds_tactic(m); - (*simplifier)(g, result); + (*simplifier)(g, result); SASSERT(result.size() == 1); goal* r = result[0]; cube.reset(); - for (unsigned i = 0; i < r->size(); ++i) { + for(unsigned i = 0; i < r->size(); ++i) { cube.push_back(r->form(i)); } } - void simplify_bounds_new (expr_ref_vector &cube) { + void simplify_bounds_new(expr_ref_vector &cube) { ast_manager &m = cube.m(); scoped_no_proof _no_pf_(m); goal_ref g(alloc(goal, m, false, false, false)); - for (expr* c : cube) + for(expr* c : cube) g->assert_expr(c); goal_ref_buffer goals; @@ -645,12 +652,12 @@ namespace { tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m); tactic_ref t = and_then(prop_values.get(), prop_bounds.get()); - (*t)(g, goals); + (*t)(g, goals); SASSERT(goals.size() == 1); g = goals[0]; cube.reset(); - for (unsigned i = 0; i < g->size(); ++i) { + for(unsigned i = 0; i < g->size(); ++i) { cube.push_back(g->form(i)); } } @@ -664,86 +671,86 @@ namespace { ast_manager &m; arith_util m_util; - adhoc_rewriter_cfg (ast_manager &manager) : m(manager), m_util(m) {} + adhoc_rewriter_cfg(ast_manager &manager) : m(manager), m_util(m) {} bool is_le(func_decl const * n) const { return m_util.is_le(n); } bool is_ge(func_decl const * n) const { return m_util.is_ge(n); } - br_status reduce_app (func_decl * f, unsigned num, expr * const * args, + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { expr * e; if (is_le(f)) - return mk_le_core (args[0], args[1], result); + return mk_le_core(args[0], args[1], result); if (is_ge(f)) - return mk_ge_core (args[0], args[1], result); - if (m.is_not(f) && m.is_not (args[0], e)) { + return mk_ge_core(args[0], args[1], result); + if (m.is_not(f) && m.is_not(args[0], e)) { result = e; return BR_DONE; } return BR_FAILED; } - br_status mk_le_core (expr *arg1, expr * arg2, expr_ref & result) { - // t <= -1 ==> t < 0 ==> ! (t >= 0) - if (m_util.is_int (arg1) && m_util.is_minus_one (arg2)) { - result = m.mk_not (m_util.mk_ge (arg1, mk_zero ())); + br_status mk_le_core(expr *arg1, expr * arg2, expr_ref & result) { + // t <= -1 ==> t < 0 ==> !(t >= 0) + if (m_util.is_int(arg1) && m_util.is_minus_one(arg2)) { + result = m.mk_not(m_util.mk_ge(arg1, mk_zero())); return BR_DONE; } return BR_FAILED; } - br_status mk_ge_core (expr * arg1, expr * arg2, expr_ref & result) { - // t >= 1 ==> t > 0 ==> ! (t <= 0) - if (m_util.is_int (arg1) && is_one (arg2)) { + br_status mk_ge_core(expr * arg1, expr * arg2, expr_ref & result) { + // t >= 1 ==> t > 0 ==> !(t <= 0) + if (m_util.is_int(arg1) && is_one(arg2)) { - result = m.mk_not (m_util.mk_le (arg1, mk_zero ())); + result = m.mk_not(m_util.mk_le(arg1, mk_zero())); return BR_DONE; } return BR_FAILED; } - expr * mk_zero () {return m_util.mk_numeral (rational (0), true);} - bool is_one (expr const * n) const { - rational val; return m_util.is_numeral (n, val) && val.is_one (); + expr * mk_zero() {return m_util.mk_numeral(rational(0), true);} + bool is_one(expr const * n) const { + rational val; return m_util.is_numeral(n, val) && val.is_one(); } }; - void normalize (expr *e, expr_ref &out, + void normalize(expr *e, expr_ref &out, bool use_simplify_bounds, bool use_factor_eqs) { params_ref params; // arith_rewriter - params.set_bool ("sort_sums", true); - params.set_bool ("gcd_rounding", true); - params.set_bool ("arith_lhs", true); + params.set_bool("sort_sums", true); + params.set_bool("gcd_rounding", true); + params.set_bool("arith_lhs", true); // poly_rewriter - params.set_bool ("som", true); - params.set_bool ("flat", true); + params.set_bool("som", true); + params.set_bool("flat", true); // apply rewriter th_rewriter rw(out.m(), params); - rw (e, out); + rw(e, out); - adhoc_rewriter_cfg adhoc_cfg(out.m ()); - rewriter_tpl adhoc_rw (out.m (), false, adhoc_cfg); - adhoc_rw (out.get (), out); + adhoc_rewriter_cfg adhoc_cfg(out.m()); + rewriter_tpl adhoc_rw(out.m(), false, adhoc_cfg); + adhoc_rw(out.get(), out); if (out.m().is_and(out)) { expr_ref_vector v(out.m()); - flatten_and (out, v); + flatten_and(out, v); if (v.size() > 1) { // sort arguments of the top-level and - std::stable_sort (v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); + std::stable_sort(v.c_ptr(), v.c_ptr() + v.size(), ast_lt_proc()); if (use_simplify_bounds) { // remove redundant inequalities - simplify_bounds (v); + simplify_bounds(v); } if (use_factor_eqs) { // -- refactor equivalence classes and choose a representative qe::term_graph egraph(out.m()); - egraph.add_lits (v); + egraph.add_lits(v); v.reset(); egraph.to_lits(v); } @@ -755,10 +762,10 @@ namespace { << mk_and(v) << "\n";); TRACE("spacer_normalize", qe::term_graph egraph(out.m()); - for (expr* e : v) egraph.add_lit (to_app(e)); + for(expr* e : v) egraph.add_lit(to_app(e)); tout << "Reduced app:\n" << mk_pp(egraph.to_app(), out.m()) << "\n";); - out = mk_and (v); + out = mk_and(v); } } } @@ -768,34 +775,34 @@ namespace { ast_manager &m; arith_util m_arith; - adhoc_rewriter_rpp (ast_manager &manager) : m(manager), m_arith(m) {} + adhoc_rewriter_rpp(ast_manager &manager) : m(manager), m_arith(m) {} bool is_le(func_decl const * n) const { return m_arith.is_le(n); } bool is_ge(func_decl const * n) const { return m_arith.is_ge(n); } bool is_lt(func_decl const * n) const { return m_arith.is_lt(n); } bool is_gt(func_decl const * n) const { return m_arith.is_gt(n); } - bool is_zero (expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();} + bool is_zero(expr const * n) const {rational val; return m_arith.is_numeral(n, val) && val.is_zero();} - br_status reduce_app (func_decl * f, unsigned num, expr * const * args, + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { br_status st = BR_FAILED; expr *e1, *e2, *e3, *e4; - // rewrites (= (+ A (* -1 B)) 0) into (= A B) - if (m.is_eq (f) && is_zero (args [1]) && - m_arith.is_add (args[0], e1, e2) && - m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) { - result = m.mk_eq (e1, e4); + // rewrites(=(+ A(* -1 B)) 0) into(= A B) + if (m.is_eq(f) && is_zero(args [1]) && + m_arith.is_add(args[0], e1, e2) && + m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) { + result = m.mk_eq(e1, e4); return BR_DONE; } // simplify normalized leq, where right side is different from 0 - // rewrites (<= (+ A (* -1 B)) C) into (<= A B+C) + // rewrites(<=(+ A(* -1 B)) C) into(<= A B+C) else if ((is_le(f) || is_lt(f) || is_ge(f) || is_gt(f)) && - m_arith.is_add (args[0], e1, e2) && - m_arith.is_mul (e2, e3, e4) && m_arith.is_minus_one (e3)) { + m_arith.is_add(args[0], e1, e2) && + m_arith.is_mul(e2, e3, e4) && m_arith.is_minus_one(e3)) { expr_ref rhs(m); - rhs = is_zero (args[1]) ? e4 : m_arith.mk_add(e4, args[1]); + rhs = is_zero(args[1]) ? e4 : m_arith.mk_add(e4, args[1]); if (is_le(f)) { result = m_arith.mk_le(e1, rhs); @@ -813,7 +820,7 @@ namespace { { UNREACHABLE(); } } // simplify negation of ordering predicate - else if (m.is_not (f)) { + else if (m.is_not(f)) { if (m_arith.is_lt(args[0], e1, e2)) { result = m_arith.mk_ge(e1, e2); st = BR_DONE; @@ -834,11 +841,11 @@ namespace { 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) { + mk_pp(t, m, m_epp_params, indent, num_vars, var_prefix), m_epp_expr(m) { m_epp_params.set_uint("min_alias_size", UINT_MAX); m_epp_params.set_uint("max_depth", UINT_MAX); - if (is_expr (m_ast)) { + if (is_expr(m_ast)) { rw(to_expr(m_ast), m_epp_expr); m_ast = m_epp_expr; } @@ -858,11 +865,11 @@ namespace { if (vars.size() < fv.size()) { vars.resize(fv.size()); } - for (unsigned i = 0, sz = fv.size(); i < sz; ++i) { + for(unsigned i = 0, sz = fv.size(); i < sz; ++i) { sort *s = fv[i] ? fv[i] : m.mk_bool_sort(); vars[i] = mk_zk_const(m, i, s); var_subst vs(m, false); - vs(e, vars.size(), (expr * *) vars.c_ptr(), out); + vs(e, vars.size(),(expr * *) vars.c_ptr(), out); } } @@ -872,75 +879,75 @@ namespace { 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) { - if (m_array.is_select (n) || m.is_eq(n)) { + 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) { + if (m_array.is_select(n) || m.is_eq(n)) { unsigned i = 0; - for (expr * arg : *n) { - if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back (arg); + for(expr * arg : *n) { + if ((m.is_eq(n) || i > 0) && m_var != arg) m_res.push_back(arg); ++i; } } } }; - bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) { - ast_manager &m = fml.get_manager (); + 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); + mev.eval(var, val, false); - TRACE ("mbqi_project_verbose", - tout << "MBQI: var: " << mk_pp (var, m) << "\n" + 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); + expr_ref_vector terms(m); + index_term_finder finder(m, var, terms); + for_each_expr(finder, fml); - TRACE ("mbqi_project_verbose", + TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";); - for (expr * term : terms) { - expr_ref tval (m); - mev.eval (term, tval, false); + for(expr * term : terms) { + expr_ref tval(m); + mev.eval(term, tval, false); - TRACE ("mbqi_project_verbose", - tout << "term: " << mk_pp (term, m) + TRACE("mbqi_project_verbose", + tout << "term: " << mk_pp(term, m) << " tval: " << tval - << " val: " << mk_pp (val, m) << "\n";); + << " val: " << mk_pp(val, m) << "\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";); + 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); + sub.insert(var, term); + sub(fml); return true; } } - TRACE ("mbqi_project", - tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << fml << "\n";); + TRACE("mbqi_project", + tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";); return false; } - void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml) { - ast_manager &m = fml.get_manager (); + void mbqi_project(model &M, app_ref_vector &vars, expr_ref &fml) { + ast_manager &m = fml.get_manager(); model_evaluator_util mev(m); - mev.set_model (M); + mev.set_model(M); expr_ref tmp(m); // -- evaluate to initialize mev cache - mev.eval (fml, tmp, false); - tmp.reset (); + mev.eval(fml, tmp, false); + tmp.reset(); unsigned j = 0; - for (app* v : vars) - if (!mbqi_project_var (mev, v, fml)) + for(app* v : vars) + if (!mbqi_project_var(mev, v, fml)) vars[j++] = v; vars.shrink(j); } @@ -959,7 +966,7 @@ namespace { for_each_expr(cs, fml); return false; } - catch (found) { + catch(found) { return true; } } @@ -970,8 +977,8 @@ namespace { collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {} void operator()(expr* n) {} void operator()(app* n) { - if (a.is_select (n)) - for (unsigned i = 1; i < n->get_num_args(); ++i) + if (a.is_select(n)) + for(unsigned i = 1; i < n->get_num_args(); ++i) if (is_app(n->get_arg(i))) m_indices.push_back(to_app(n->get_arg(i))); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index f43195a97..a66d2dd5a 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -48,17 +48,17 @@ namespace spacer { return UINT_MAX; } - inline bool is_infty_level(unsigned lvl) { - return lvl == infty_level (); + inline bool is_infty_level(unsigned lvl) { + return lvl == infty_level (); } - inline unsigned next_level(unsigned lvl) { - return is_infty_level(lvl)?lvl:(lvl+1); + inline unsigned next_level(unsigned lvl) { + return is_infty_level(lvl)?lvl:(lvl+1); } inline unsigned prev_level (unsigned lvl) { - if (is_infty_level(lvl)) return infty_level(); - if (lvl == 0) return 0; + if (is_infty_level(lvl)) return infty_level(); + if (lvl == 0) return 0; return lvl - 1; } @@ -78,28 +78,28 @@ namespace spacer { typedef ptr_vector app_vector; typedef ptr_vector decl_vector; typedef obj_hashtable func_decl_set; - + // TBD: deprecate class model_evaluator_util { ast_manager& m; model_ref m_model; model_evaluator* m_mev; - + /// initialize with a given model. All previous state is lost. model can be NULL void reset (model *model); public: model_evaluator_util(ast_manager& m); ~model_evaluator_util(); - + void set_model(model &model) {reset (&model);} model_ref &get_model() {return m_model;} ast_manager& get_ast_manager() const {return m;} - + public: bool is_true (const expr_ref_vector &v); bool is_false(expr* x); bool is_true(expr* x); - + bool eval (const expr_ref_vector &v, expr_ref &result, bool model_completion); /// evaluates an expression bool eval (expr *e, expr_ref &result, bool model_completion); @@ -109,10 +109,10 @@ namespace spacer { /** \brief hoist non-boolean if expressions. */ - + void to_mbp_benchmark(std::ostream &out, const expr* fml, const app_ref_vector &vars); - + // TBD: deprecate by qe::mbp /** * do the following in sequence @@ -126,27 +126,29 @@ namespace spacer { bool dont_sub=false); void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map); - + // TBD: sort out void expand_literals(ast_manager &m, expr_ref_vector& conjs); - void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, expr_ref_vector &res); + void compute_implicant_literals(model &mdl, + expr_ref_vector &formula, + expr_ref_vector &res); void simplify_bounds (expr_ref_vector &lemmas); void normalize(expr *e, expr_ref &out, bool use_simplify_bounds = true, bool factor_eqs = false); - - /** + + /** * Ground expression by replacing all free variables by skolem * constants. On return, out is the resulting expression, and vars is * a map from variable ids to corresponding skolem constants. */ void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars); - + void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml); - + bool contains_selects (expr* fml, ast_manager& m); void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); - + void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix); - + /** * extended pretty-printer * used for debugging @@ -156,7 +158,7 @@ namespace spacer { params_ref m_epp_params; expr_ref m_epp_expr; mk_epp(ast *t, ast_manager &m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr); - void rw(expr *e, expr_ref &out); + void rw(expr *e, expr_ref &out); }; } From 5e65b37f25d4a536adc99ec25a561d9100d1c68b Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 13:58:58 -0700 Subject: [PATCH 3/7] Switch spacer::qe_project to new model API --- src/api/api_qe.cpp | 2 +- src/muz/spacer/spacer_context.cpp | 12 ++-- src/muz/spacer/spacer_context.h | 2 +- src/muz/spacer/spacer_util.cpp | 95 +++++++++++++------------------ src/muz/spacer/spacer_util.h | 10 +++- 5 files changed, 54 insertions(+), 67 deletions(-) diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp index 0073ef274..92517b02b 100644 --- a/src/api/api_qe.cpp +++ b/src/api/api_qe.cpp @@ -62,7 +62,7 @@ extern "C" expr_ref result (mk_c(c)->m ()); result = to_expr (body); model_ref model (to_model_ref (m)); - spacer::qe_project (mk_c(c)->m (), vars, result, model); + spacer::qe_project (mk_c(c)->m (), vars, result, *model); mk_c(c)->save_ast_trail (result.get ()); return of_expr (result.get ()); diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index db1153de3..8853a2e45 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -265,7 +265,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev) verbose_stream ()); vars.append(m_evars); m_evars.reset(); - pt().mbp(vars, m_trans, mev.get_model(), + pt().mbp(vars, m_trans, *mev.get_model(), true, pt().get_context().use_ground_pob()); m_evars.append (vars); vars.reset(); @@ -294,7 +294,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev) verbose_stream ()); // include m_evars in case they can eliminated now as well vars.append(m_evars); - pt().mbp(vars, post, mev.get_model(), + pt().mbp(vars, post, *mev.get_model(), true, pt().get_context().use_ground_pob()); //qe::reduce_array_selects (*mev.get_model (), post); } @@ -398,7 +398,7 @@ pob *derivation::create_next_child () if (!vars.empty ()) { vars.append(m_evars); m_evars.reset(); - this->pt().mbp(vars, m_trans, mev.get_model(), + this->pt().mbp(vars, m_trans, *mev.get_model(), true, this->pt().get_context().use_ground_pob()); // keep track of implicitly quantified variables m_evars.append (vars); @@ -1267,7 +1267,7 @@ bool pred_transformer::is_qblocked (pob &n) { } -void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, +void pred_transformer::mbp(app_ref_vector &vars, expr_ref &fml, model &mdl, bool reduce_all_selects, bool force) { scoped_watch _t_(m_mbp_watch); qe_project(m, vars, fml, mdl, reduce_all_selects, use_native_mbp(), !force); @@ -3617,7 +3617,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, timeit _timer1 (is_trace_enabled("spacer_timeit"), "mk_rf::qe_project", verbose_stream ()); - mbp(vars, res, mev.get_model(), false, true /* force or skolemize */); + mbp(vars, res, *mev.get_model(), false, true /* force or skolemize */); } @@ -3685,7 +3685,7 @@ bool context::create_children(pob& n, datalog::rule const& r, // skolems of the pob n.get_skolems(vars); - n.pt().mbp(vars, phi, mev.get_model (), true, use_ground_pob()); + n.pt().mbp(vars, phi, *mev.get_model (), true, use_ground_pob()); //qe::reduce_array_selects (*mev.get_model (), phi1); SASSERT (!m_ground_pob || vars.empty ()); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 760f38f69..c502baa63 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -530,7 +530,7 @@ public: bool is_qblocked (pob &n); /// \brief interface to Model Based Projection - void mbp(app_ref_vector &vars, expr_ref &fml, const model_ref &mdl, + void mbp(app_ref_vector &vars, expr_ref &fml, model &mdl, bool reduce_all_selects, bool force = false); void updt_solver(prop_solver *solver); diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 3eb18b0e5..b9768f4be 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -128,17 +128,11 @@ namespace spacer { } void subst_vars(ast_manager& m, - app_ref_vector const& vars, - model* M, expr_ref& fml) { - expr_safe_replace sub (m); - model_evaluator_util mev (m); - mev.set_model(*M); - for (app * v : vars) { - expr_ref val (m); - VERIFY(mev.eval (v, val, true)); - sub.insert (v, val); - } - sub (fml); + app_ref_vector const& vars, model& mdl, expr_ref& fml) { + model::scoped_model_completion _sc_(mdl, true); + expr_safe_replace sub(m); + for (app * v : vars) sub.insert (v, mdl(v)); + sub(fml); } void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) { @@ -161,16 +155,14 @@ namespace spacer { } void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml, - const model_ref& M, bool reduce_all_selects, bool use_native_mbp, + model & mdl, bool reduce_all_selects, bool use_native_mbp, bool dont_sub) { params_ref p; p.set_bool("reduce_all_selects", reduce_all_selects); p.set_bool("dont_sub", dont_sub); qe::mbp mbp(m, p); - // TODO: deal with const - model *mdl = const_cast(M.get()); - mbp.spacer(vars, *mdl, fml); + mbp.spacer(vars, mdl, fml); } /* @@ -178,7 +170,7 @@ namespace spacer { * then, MBP for Booleans (substitute), reals (based on LW), ints (based on Cooper), and arrays */ void qe_project_spacer (ast_manager& m, app_ref_vector& vars, expr_ref& fml, - const model_ref& M, bool reduce_all_selects, bool use_native_mbp, + model& mdl, bool reduce_all_selects, bool use_native_mbp, bool dont_sub) { th_rewriter rw (m); TRACE ("spacer_mbp", @@ -221,30 +213,29 @@ namespace spacer { // sort out vars into bools, arith (int/real), and arrays for (app* v : vars) { if (m.is_bool (v)) { - // obtain the interpretation of the ith var using model completion - VERIFY (M->eval (v, bval, true)); - bool_sub.insert (v, bval); + // obtain the interpretation of the ith var + // 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); + array_vars.push_back(v); } else { - SASSERT (ari_u.is_int (v) || ari_u.is_real (v)); - arith_vars.push_back (v); + SASSERT (ari_u.is_int(v) || ari_u.is_real(v)); + arith_vars.push_back(v); } } // substitute Booleans if (!bool_sub.empty()) { - bool_sub (fml); + bool_sub(fml); // -- bool_sub is not simplifying rw (fml); - SASSERT (!m.is_false (fml)); - TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); - bool_sub.reset (); + SASSERT(!m.is_false (fml)); + TRACE("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); + bool_sub.reset(); } - TRACE ("spacer_mbp", - tout << "Array vars:\n"; - tout << array_vars;); + TRACE ("spacer_mbp", tout << "Array vars:\n"; tout << array_vars;); vars.reset (); @@ -253,7 +244,7 @@ namespace spacer { scoped_no_proof _sp (m); // -- local rewriter that is aware of current proof mode th_rewriter srw(m); - spacer_qe::array_project (*M.get (), array_vars, fml, vars, reduce_all_selects); + spacer_qe::array_project (mdl, array_vars, fml, vars, reduce_all_selects); SASSERT (array_vars.empty ()); srw (fml); SASSERT (!m.is_false (fml)); @@ -261,10 +252,9 @@ namespace spacer { TRACE ("spacer_mbp", tout << "extended model:\n"; - model_pp (tout, *M); + model_pp (tout, mdl); tout << "Auxiliary variables of index and value sorts:\n"; - tout << vars; - ); + tout << vars;); if (vars.empty()) { break; } } @@ -273,39 +263,32 @@ namespace spacer { if (!arith_vars.empty ()) { 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 ()); + mbp (true, arith_vars, mdl, fmls); + fml = mk_and(fmls); + SASSERT(arith_vars.empty ()); } else { scoped_no_proof _sp (m); - spacer_qe::arith_project (*M.get (), arith_vars, fml); - } + spacer_qe::arith_project (mdl, arith_vars, fml); + } TRACE ("spacer_mbp", - tout << "Projected arith vars:\n" << mk_pp (fml, m) << "\n"; + tout << "Projected arith vars:\n" << fml << "\n"; tout << "Remaining arith vars:\n" << arith_vars << "\n";); SASSERT (!m.is_false (fml)); } if (!arith_vars.empty ()) { - mbqi_project (*M.get(), arith_vars, fml); + mbqi_project (mdl, arith_vars, fml); } // substitute any remaining arith vars if (!dont_sub && !arith_vars.empty ()) { - subst_vars (m, arith_vars, M.get(), fml); + subst_vars (m, arith_vars, mdl, fml); TRACE ("spacer_mbp", tout << "After substituting remaining arith vars:\n"; tout << mk_pp (fml, m) << "\n"; @@ -315,11 +298,9 @@ namespace spacer { } DEBUG_CODE ( - model_evaluator_util mev (m); - expr_ref v(m); - mev.set_model(*M.get()); - SASSERT (mev.eval (fml, v, false)); - SASSERT (m.is_true (v)); + model_evaluator mev(mdl); + mev.set_model_completion(false); + SASSERT(mev.is_true(fml)); ); vars.reset (); @@ -343,12 +324,14 @@ namespace spacer { } void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, - const model_ref& M, bool reduce_all_selects, bool use_native_mbp, + model &mdl, bool reduce_all_selects, bool use_native_mbp, bool dont_sub) { if (use_native_mbp) - qe_project_z3(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); + qe_project_z3(m, vars, fml, mdl, + reduce_all_selects, use_native_mbp, dont_sub); else - qe_project_spacer(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); + qe_project_spacer(m, vars, fml, mdl, + reduce_all_selects, use_native_mbp, dont_sub); } void expand_literals(ast_manager &m, expr_ref_vector& conjs) { diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index a66d2dd5a..c3dbbd042 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -121,11 +121,15 @@ namespace spacer { * 3. use MBP for remaining array and arith variables * 4. for any remaining arith variables, substitute using M */ - void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, - const model_ref& M, bool reduce_all_selects=false, bool native_mbp=false, + void qe_project (ast_manager& m, app_ref_vector& vars, + expr_ref& fml, model &mdl, + bool reduce_all_selects=false, + bool native_mbp=false, bool dont_sub=false); - void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map); + // deprecate + void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, + model_ref& M, expr_map& map); // TBD: sort out void expand_literals(ast_manager &m, expr_ref_vector& conjs); From f226c6682bbf1545cc666177f7696af937d3971d Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 14:09:24 -0700 Subject: [PATCH 4/7] Switched derivation to new model API --- src/muz/spacer/spacer_context.cpp | 28 ++++++++++++++-------------- src/muz/spacer/spacer_context.h | 4 ++-- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 8853a2e45..496672b96 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -195,10 +195,10 @@ void derivation::add_premise (pred_transformer &pt, -pob *derivation::create_first_child (model_evaluator_util &mev) { +pob *derivation::create_first_child (model &mdl) { if (m_premises.empty()) { return nullptr; } m_active = 0; - return create_next_child(mev); + return create_next_child(mdl); } void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) { @@ -236,7 +236,7 @@ void derivation::exist_skolemize(expr* fml, app_ref_vector &vars, expr_ref &res) sub(fml, res); } -pob *derivation::create_next_child (model_evaluator_util &mev) +pob *derivation::create_next_child(model &mdl) { timeit _timer (is_trace_enabled("spacer_timeit"), "spacer::derivation::create_next_child", @@ -265,13 +265,13 @@ pob *derivation::create_next_child (model_evaluator_util &mev) verbose_stream ()); vars.append(m_evars); m_evars.reset(); - pt().mbp(vars, m_trans, *mev.get_model(), + pt().mbp(vars, m_trans, mdl, true, pt().get_context().use_ground_pob()); m_evars.append (vars); vars.reset(); } - if (!mev.is_true (m_premises[m_active].get_summary())) { + if (!mdl.is_true(m_premises[m_active].get_summary())) { IF_VERBOSE(1, verbose_stream() << "Summary unexpectendly not true\n";); return nullptr; } @@ -294,7 +294,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev) verbose_stream ()); // include m_evars in case they can eliminated now as well vars.append(m_evars); - pt().mbp(vars, post, *mev.get_model(), + pt().mbp(vars, post, mdl, true, pt().get_context().use_ground_pob()); //qe::reduce_array_selects (*mev.get_model (), post); } @@ -337,7 +337,6 @@ pob *derivation::create_next_child () // construct a new model consistent with the must summary of m_active premise pred_transformer &pt = m_premises[m_active].pt (); - model_ref model; ast_manager &m = get_ast_manager (); manager &pm = get_manager (); @@ -355,18 +354,19 @@ pob *derivation::create_next_child () // if not true, bail out, the must summary of m_active is not strong enough // this is possible if m_post was weakened for some reason - if (!pt.is_must_reachable(mk_and(summaries), &model)) { return nullptr; } + model_ref mdl; + if (!pt.is_must_reachable(mk_and(summaries), &mdl)) { return nullptr; } model_evaluator_util mev (m); - mev.set_model (*model); + mev.set_model (*mdl); // find must summary used reach_fact *rf = pt.get_used_rf (mev, true); // get an implicant of the summary - expr_ref_vector u(m), lits (m); + expr_ref_vector u(m), lits(m); u.push_back (rf->get ()); - compute_implicant_literals (*model, u, lits); + compute_implicant_literals (*mdl, u, lits); expr_ref v(m); v = mk_and (lits); @@ -398,7 +398,7 @@ pob *derivation::create_next_child () if (!vars.empty ()) { vars.append(m_evars); m_evars.reset(); - this->pt().mbp(vars, m_trans, *mev.get_model(), + this->pt().mbp(vars, m_trans, *mdl, true, this->pt().get_context().use_ground_pob()); // keep track of implicitly quantified variables m_evars.append (vars); @@ -408,7 +408,7 @@ pob *derivation::create_next_child () m_active++; - return create_next_child (mev); + return create_next_child (*mdl); } /// derivation::premise @@ -3732,7 +3732,7 @@ bool context::create_children(pob& n, datalog::rule const& r, } // create post for the first child and add to queue - pob* kid = deriv->create_first_child (mev); + pob* kid = deriv->create_first_child (*mev.get_model()); // -- failed to create derivation, cleanup and bail out if (!kid) { diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index c502baa63..93704aefc 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -740,7 +740,7 @@ class derivation { app_ref_vector m_evars; /// -- create next child using given model as the guide /// -- returns NULL if there is no next child - pob* create_next_child (model_evaluator_util &mev); + pob* create_next_child (model &mdl); /// existentially quantify vars and skolemize the result void exist_skolemize(expr *fml, app_ref_vector &vars, expr_ref &res); public: @@ -752,7 +752,7 @@ public: /// creates the first child. Must be called after all the premises /// are added. The model must be valid for the premises /// Returns NULL if no child exits - pob *create_first_child (model_evaluator_util &mev); + pob *create_first_child (model &mdl); /// Create the next child. Must summary of the currently active /// premise must be consistent with the transition relation From a222b6d41f1a8e5573eae52d8fb984ec47640821 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 14:17:33 -0700 Subject: [PATCH 5/7] Switch reach_fact to new model API --- src/muz/spacer/spacer_context.cpp | 43 ++++++++++++++----------------- src/muz/spacer/spacer_context.h | 9 +++---- 2 files changed, 23 insertions(+), 29 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 496672b96..89d438b73 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -361,7 +361,7 @@ pob *derivation::create_next_child () mev.set_model (*mdl); // find must summary used - reach_fact *rf = pt.get_used_rf (mev, true); + reach_fact *rf = pt.get_used_rf (*mev.get_model(), true); // get an implicant of the summary expr_ref_vector u(m), lits(m); @@ -795,27 +795,24 @@ bool pred_transformer::is_must_reachable(expr* state, model_ref* model) -reach_fact* pred_transformer::get_used_rf (model_evaluator_util& mev, - bool all) { +reach_fact* pred_transformer::get_used_rf (model& mdl, bool all) { expr_ref v (m); + model::scoped_model_completion _sc_(mdl, false); for (auto *rf : m_reach_facts) { if (!all && rf->is_init()) continue; - VERIFY(mev.eval (rf->tag(), v, false)); - if (m.is_false(v)) return rf; + if (mdl.is_false(rf->tag())) return rf; } UNREACHABLE(); return nullptr; } -reach_fact *pred_transformer::get_used_origin_rf (model_evaluator_util& mev, - unsigned oidx) { +reach_fact *pred_transformer::get_used_origin_rf(model& mdl, unsigned oidx) { expr_ref b(m), v(m); - + model::scoped_model_completion _sc_(mdl, false); for (auto *rf : m_reach_facts) { pm.formula_n2o (rf->tag(), v, oidx); - VERIFY(mev.eval (v, b, false)); - if (m.is_false (b)) return rf; + if (mdl.is_false(v)) return rf; } UNREACHABLE(); return nullptr; @@ -1139,12 +1136,13 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) * * returns an implicant of the summary */ -expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, +expr_ref pred_transformer::get_origin_summary (model &mdl, unsigned level, unsigned oidx, bool must, const ptr_vector **aux) { + model::scoped_model_completion _sc_(mdl, false); expr_ref_vector summary (m); expr_ref v(m); @@ -1153,7 +1151,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, // -- no auxiliary variables in lemmas *aux = nullptr; } else { // find must summary to use - reach_fact *f = get_used_origin_rf (mev, oidx); + reach_fact *f = get_used_origin_rf(mdl, oidx); summary.push_back (f->get ()); *aux = &f->aux_vars (); } @@ -1167,13 +1165,11 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev, } // bail out of if the model is insufficient - if (!mev.is_true(summary)) - return expr_ref(m); + if (!mdl.is_true(summary)) return expr_ref(m); // -- pick an implicant expr_ref_vector lits(m); - compute_implicant_literals (*mev.get_model(), summary, lits); - + compute_implicant_literals (mdl, summary, lits); return mk_and(lits); } @@ -3199,7 +3195,7 @@ bool context::is_reachable(pob &n) mev.set_model(*model); // -- update must summary if (r && r->get_uninterpreted_tail_size () > 0) { - reach_fact_ref rf = n.pt().mk_rf (n, mev, *r); + reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r); n.pt ().add_rf (rf.get ()); } @@ -3340,7 +3336,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) if (is_concrete) { // -- update must summary if (r && r->get_uninterpreted_tail_size() > 0) { - reach_fact_ref rf = n.pt().mk_rf (n, mev, *r); + reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r); checkpoint (); n.pt ().add_rf (rf.get ()); checkpoint (); @@ -3554,8 +3550,7 @@ bool context::propagate(unsigned min_prop_lvl, return false; } -reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, - const datalog::rule& r) +reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r) { SASSERT(&n.pt() == this); timeit _timer1 (is_trace_enabled("spacer_timeit"), @@ -3576,7 +3571,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, pred_transformer& ch_pt = ctx.get_pred_transformer (pred); // get a reach fact of body preds used in the model expr_ref o_ch_reach (m); - reach_fact *kid = ch_pt.get_used_origin_rf (mev, i); + reach_fact *kid = ch_pt.get_used_origin_rf(mdl, i); child_reach_facts.push_back (kid); pm.formula_n2o (kid->get (), o_ch_reach, i); path_cons.push_back (o_ch_reach); @@ -3599,7 +3594,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, if (ctx.reach_dnf()) { expr_ref_vector u(m), lits(m); u.push_back (res); - compute_implicant_literals (*mev.get_model(), u, lits); + compute_implicant_literals (mdl, u, lits); res = mk_and (lits); } @@ -3617,7 +3612,7 @@ reach_fact *pred_transformer::mk_rf (pob& n, model_evaluator_util &mev, timeit _timer1 (is_trace_enabled("spacer_timeit"), "mk_rf::qe_project", verbose_stream ()); - mbp(vars, res, *mev.get_model(), false, true /* force or skolemize */); + mbp(vars, res, mdl, false, true /* force or skolemize */); } @@ -3722,7 +3717,7 @@ bool context::create_children(pob& n, datalog::rule const& r, const ptr_vector *aux = nullptr; expr_ref sum(m); - sum = pt.get_origin_summary (mev, prev_level(n.level()), + sum = pt.get_origin_summary (*mev.get_model(), prev_level(n.level()), j, reach_pred_used[j], &aux); if (!sum) { dealloc(deriv); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 93704aefc..394dbf7e2 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -440,10 +440,10 @@ public: bool is_must_reachable(expr* state, model_ref* model = nullptr); /// \brief Returns reachability fact active in the given model /// all determines whether initial reachability facts are included as well - reach_fact *get_used_rf(model_evaluator_util& mev, bool all = true); + reach_fact *get_used_rf(model& mdl, bool all = true); /// \brief Returns reachability fact active in the origin of the given model - reach_fact* get_used_origin_rf(model_evaluator_util &mev, unsigned oidx); - expr_ref get_origin_summary(model_evaluator_util &mev, + reach_fact* get_used_origin_rf(model &mdl, unsigned oidx); + expr_ref get_origin_summary(model &mdl, unsigned level, unsigned oidx, bool must, const ptr_vector **aux); @@ -472,8 +472,7 @@ public: /// initialize reachability facts using initial rules void init_rfs (); - reach_fact *mk_rf(pob &n, model_evaluator_util &mev, - const datalog::rule &r); + reach_fact *mk_rf(pob &n, model &mdl, const datalog::rule &r); void add_rf (reach_fact *fact); // add reachability fact reach_fact* get_last_rf () const { return m_reach_facts.back (); } expr* get_last_rf_tag () const; From 4204b6ede25e227574e431131e9fbdf2008fefbd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Sat, 16 Jun 2018 14:40:17 -0700 Subject: [PATCH 6/7] Switch rest of spacer to new model API and remove mev_util --- src/muz/spacer/spacer_context.cpp | 50 +++++++---------- src/muz/spacer/spacer_context.h | 4 +- src/muz/spacer/spacer_pdr.cpp | 4 +- src/muz/spacer/spacer_util.cpp | 90 ++++++------------------------- src/muz/spacer/spacer_util.h | 30 +---------- 5 files changed, 41 insertions(+), 137 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 89d438b73..5d3ecb3fe 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -36,7 +36,6 @@ Notes: #include "muz/base/dl_rule_set.h" #include "smt/tactic/unit_subsumption_tactic.h" #include "model/model_smt2_pp.h" -#include "model/model_evaluator.h" #include "muz/transforms/dl_mk_rule_inliner.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" @@ -356,12 +355,10 @@ pob *derivation::create_next_child () // this is possible if m_post was weakened for some reason model_ref mdl; if (!pt.is_must_reachable(mk_and(summaries), &mdl)) { return nullptr; } + mdl->set_model_completion(false); - model_evaluator_util mev (m); - mev.set_model (*mdl); // find must summary used - - reach_fact *rf = pt.get_used_rf (*mev.get_model(), true); + reach_fact *rf = pt.get_used_rf (*mdl, true); // get an implicant of the summary expr_ref_vector u(m), lits(m); @@ -2883,7 +2880,6 @@ expr_ref context::get_ground_sat_answer() // smt context to obtain local cexes ref cex_ctx = mk_smt_solver(m, params_ref::get_empty(), symbol::null); - model_evaluator_util mev (m); // preorder traversal of the query derivation tree for (unsigned curr = 0; curr < pts.size (); curr++) { @@ -2936,8 +2932,7 @@ expr_ref context::get_ground_sat_answer() model_ref local_mdl; cex_ctx->get_model (local_mdl); cex_ctx->pop (1); - - model_evaluator mev(*local_mdl); + local_mdl->set_model_completion(true); for (unsigned i = 0; i < child_pts.size(); i++) { pred_transformer& ch_pt = *(child_pts.get(i)); unsigned sig_size = ch_pt.sig_size(); @@ -2946,7 +2941,7 @@ expr_ref context::get_ground_sat_answer() for (unsigned j = 0; j < sig_size; j++) { expr_ref sig_arg(m), sig_val(m); sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i)); - VERIFY(mev.eval (sig_arg, sig_val, true)); + sig_val = (*local_mdl)(sig_arg); ground_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val)); ground_arg_vals.push_back(sig_val); } @@ -3166,7 +3161,7 @@ bool context::is_reachable(pob &n) // used in case n is unreachable unsigned uses_level = infty_level (); - model_ref model; + model_ref mdl; // used in case n is reachable bool is_concrete; @@ -3177,7 +3172,7 @@ bool context::is_reachable(pob &n) unsigned saved = n.level (); n.m_level = infty_level (); - lbool res = n.pt().is_reachable(n, nullptr, &model, + lbool res = n.pt().is_reachable(n, nullptr, &mdl, uses_level, is_concrete, r, reach_pred_used, num_reuse_reach); n.m_level = saved; @@ -3191,11 +3186,9 @@ bool context::is_reachable(pob &n) SASSERT(res == l_true); SASSERT(is_concrete); - model_evaluator_util mev (m); - mev.set_model(*model); // -- update must summary if (r && r->get_uninterpreted_tail_size () > 0) { - reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r); + reach_fact_ref rf = n.pt().mk_rf (n, *mdl, *r); n.pt ().add_rf (rf.get ()); } @@ -3322,6 +3315,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) lbool res = n.pt ().is_reachable (n, &cube, &model, uses_level, is_concrete, r, reach_pred_used, num_reuse_reach); + if (model) model->set_model_completion(false); checkpoint (); IF_VERBOSE (1, verbose_stream () << "." << std::flush;); switch (res) { @@ -3330,13 +3324,11 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) // update stats m_stats.m_num_reuse_reach += num_reuse_reach; - model_evaluator_util mev (m); - mev.set_model (*model); // must-reachable if (is_concrete) { // -- update must summary if (r && r->get_uninterpreted_tail_size() > 0) { - reach_fact_ref rf = n.pt().mk_rf (n, *mev.get_model(), *r); + reach_fact_ref rf = n.pt().mk_rf (n, *model, *r); checkpoint (); n.pt ().add_rf (rf.get ()); checkpoint (); @@ -3374,7 +3366,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) // create a child of n out.push_back(&n); - VERIFY(create_children (n, *r, mev, reach_pred_used, out)); + VERIFY(create_children (n, *r, *model, reach_pred_used, out)); IF_VERBOSE(1, verbose_stream () << " U " << std::fixed << std::setprecision(2) << watch.get_seconds () << "\n";); @@ -3449,12 +3441,10 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out) SASSERT(m_weak_abs); m_stats.m_expand_pob_undef++; if (r && r->get_uninterpreted_tail_size() > 0) { - model_evaluator_util mev(m); - mev.set_model(*model); // do not trust reach_pred_used for (unsigned i = 0, sz = reach_pred_used.size(); i < sz; ++i) { reach_pred_used[i] = false; } - has_new_child = create_children(n,*r,mev,reach_pred_used, out); + has_new_child = create_children(n, *r, *model, reach_pred_used, out); } IF_VERBOSE(1, verbose_stream() << " UNDEF " << std::fixed << std::setprecision(2) @@ -3640,7 +3630,7 @@ reach_fact *pred_transformer::mk_rf(pob& n, model &mdl, const datalog::rule& r) \brief create children states from model cube. */ bool context::create_children(pob& n, datalog::rule const& r, - model_evaluator_util &mev, + model &mdl, const vector &reach_pred_used, pob_ref_buffer &out) { @@ -3649,7 +3639,7 @@ bool context::create_children(pob& n, datalog::rule const& r, TRACE("spacer", tout << "Model:\n"; - model_smt2_pp(tout, m, *mev.get_model (), 0); + model_smt2_pp(tout, m, mdl, 0); tout << "\n"; tout << "Transition:\n" << mk_pp(pt.get_transition(r), m) << "\n"; tout << "Pob:\n" << mk_pp(n.post(), m) << "\n";); @@ -3665,7 +3655,7 @@ bool context::create_children(pob& n, datalog::rule const& r, forms.push_back(pt.get_transition(r)); forms.push_back(n.post()); - compute_implicant_literals (*mev.get_model(), forms, lits); + compute_implicant_literals (mdl, forms, lits); expr_ref phi = mk_and (lits); // primed variables of the head @@ -3680,7 +3670,7 @@ bool context::create_children(pob& n, datalog::rule const& r, // skolems of the pob n.get_skolems(vars); - n.pt().mbp(vars, phi, *mev.get_model (), true, use_ground_pob()); + n.pt().mbp(vars, phi, mdl, true, use_ground_pob()); //qe::reduce_array_selects (*mev.get_model (), phi1); SASSERT (!m_ground_pob || vars.empty ()); @@ -3694,7 +3684,7 @@ bool context::create_children(pob& n, datalog::rule const& r, if (m_use_gpdr && preds.size() > 1) { SASSERT(vars.empty()); - return gpdr_create_split_children(n, r, phi, mev.get_model(), out); + return gpdr_create_split_children(n, r, phi, mdl, out); } derivation *deriv = alloc(derivation, n, r, phi, vars); @@ -3717,7 +3707,7 @@ bool context::create_children(pob& n, datalog::rule const& r, const ptr_vector *aux = nullptr; expr_ref sum(m); - sum = pt.get_origin_summary (*mev.get_model(), prev_level(n.level()), + sum = pt.get_origin_summary (mdl, prev_level(n.level()), j, reach_pred_used[j], &aux); if (!sum) { dealloc(deriv); @@ -3727,7 +3717,7 @@ bool context::create_children(pob& n, datalog::rule const& r, } // create post for the first child and add to queue - pob* kid = deriv->create_first_child (*mev.get_model()); + pob* kid = deriv->create_first_child (mdl); // -- failed to create derivation, cleanup and bail out if (!kid) { @@ -3744,8 +3734,8 @@ bool context::create_children(pob& n, datalog::rule const& r, // -- not satisfy 'T && phi'. It is possible to recover from // -- that more gracefully. For now, we just remove the // -- derivation completely forcing it to be recomputed - if (m_weak_abs && (!mev.is_true(pt.get_transition(r)) || - !mev.is_true(n.post()))) + if (m_weak_abs && (!mdl.is_true(pt.get_transition(r)) || + !mdl.is_true(n.post()))) { kid->reset_derivation(); } out.push_back(kid); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 394dbf7e2..37b035b98 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -940,7 +940,7 @@ class context { bool gpdr_check_reachability(unsigned lvl, model_search &ms); bool gpdr_create_split_children(pob &n, const datalog::rule &r, expr *trans, - model_ref &mdl, + model &mdl, pob_ref_buffer &out); // Functions used by search. @@ -952,7 +952,7 @@ class context { bool is_reachable(pob &n); lbool expand_pob(pob &n, pob_ref_buffer &out); bool create_children(pob& n, const datalog::rule &r, - model_evaluator_util &mdl, + model &mdl, const vector& reach_pred_used, pob_ref_buffer &out); diff --git a/src/muz/spacer/spacer_pdr.cpp b/src/muz/spacer/spacer_pdr.cpp index ad2b6200d..4e6b37a0a 100644 --- a/src/muz/spacer/spacer_pdr.cpp +++ b/src/muz/spacer/spacer_pdr.cpp @@ -306,7 +306,7 @@ bool context::gpdr_check_reachability(unsigned lvl, model_search &ms) { bool context::gpdr_create_split_children(pob &n, const datalog::rule &r, expr *trans, - model_ref &mdl, + model &mdl, pob_ref_buffer &out) { pred_transformer &pt = n.pt(); ptr_vector preds; @@ -330,7 +330,7 @@ bool context::gpdr_create_split_children(pob &n, const datalog::rule &r, expr_ref_vector lits(m); flatten_and(trans, lits); vector res(preds.size(), expr_ref_vector(m)); - _mbc(pmap, lits, *mdl.get(), res); + _mbc(pmap, lits, mdl, res); // pick an order to process children unsigned_vector kid_order; diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index b9768f4be..f63fc02d0 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -69,64 +69,6 @@ Notes: namespace spacer { - ///////////////////////// - // model_evaluator_util - // - - model_evaluator_util::model_evaluator_util(ast_manager& m) : - m(m), m_mev(nullptr) { - reset (nullptr); - } - - model_evaluator_util::~model_evaluator_util() {reset (nullptr);} - - - void model_evaluator_util::reset(model* model) { - if (m_mev) { - dealloc(m_mev); - m_mev = nullptr; - } - m_model = model; - if (m_model) - m_mev = alloc(model_evaluator, *m_model); - } - - bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) { - m_mev->set_model_completion (model_completion); - try { - m_mev->operator() (e, result); - return true; - } - catch (model_evaluator_exception &ex) { - (void)ex; - TRACE("spacer_model_evaluator", tout << ex.msg () << "\n";); - return false; - } - } - - bool model_evaluator_util::eval(const expr_ref_vector &v, - expr_ref& res, bool model_completion) { - expr_ref e(m); - e = mk_and (v); - return eval(e, res, model_completion); - } - - - bool model_evaluator_util::is_true(const expr_ref_vector &v) { - expr_ref res(m); - return eval (v, res, false) && m.is_true (res); - } - - bool model_evaluator_util::is_false(expr *x) { - expr_ref res(m); - return eval(x, res, false) && m.is_false (res); - } - - bool model_evaluator_util::is_true(expr *x) { - expr_ref res(m); - return eval(x, res, false) && m.is_true (res); - } - void subst_vars(ast_manager& m, app_ref_vector const& vars, model& mdl, expr_ref& fml) { model::scoped_model_completion _sc_(mdl, true); @@ -876,36 +818,36 @@ namespace { } }; - bool mbqi_project_var(model_evaluator_util &mev, app* var, expr_ref &fml) { + bool mbqi_project_var(model &mdl, app* var, expr_ref &fml) { ast_manager &m = fml.get_manager(); + model::scoped_model_completion _sc_(mdl, false); expr_ref val(m); - mev.eval(var, val, false); + val = mdl(var); TRACE("mbqi_project_verbose", - tout << "MBQI: var: " << mk_pp(var, m) << "\n" - << "fml: " << fml << "\n";); + 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 << "\n";); + TRACE("mbqi_project_verbose", tout << "terms:\n" << terms << "\n";); for(expr * term : terms) { expr_ref tval(m); - mev.eval(term, tval, false); + tval = mdl(term); TRACE("mbqi_project_verbose", tout << "term: " << mk_pp(term, m) - << " tval: " << tval - << " val: " << mk_pp(val, m) << "\n";); + << " 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";); + tout << "MBQI: replacing " << mk_pp(var, m) + << " with " << mk_pp(term, m) << "\n";); expr_safe_replace sub(m); sub.insert(var, term); sub(fml); @@ -914,23 +856,23 @@ namespace { } TRACE("mbqi_project", - tout << "MBQI: failed to eliminate " << mk_pp(var, m) << " from " << fml << "\n";); + tout << "MBQI: failed to eliminate " << mk_pp(var, m) + << " from " << fml << "\n";); return false; } - void mbqi_project(model &M, app_ref_vector &vars, expr_ref &fml) { + void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml) { ast_manager &m = fml.get_manager(); - model_evaluator_util mev(m); - mev.set_model(M); expr_ref tmp(m); + model::scoped_model_completion _sc_(mdl, false); // -- evaluate to initialize mev cache - mev.eval(fml, tmp, false); + tmp = mdl(fml); tmp.reset(); unsigned j = 0; for(app* v : vars) - if (!mbqi_project_var(mev, v, fml)) + if (!mbqi_project_var(mdl, v, fml)) vars[j++] = v; vars.shrink(j); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index c3dbbd042..9912769c5 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -40,7 +40,6 @@ Revision History: class model; class model_core; -class model_evaluator; namespace spacer { @@ -79,33 +78,6 @@ namespace spacer { typedef ptr_vector decl_vector; typedef obj_hashtable func_decl_set; - // TBD: deprecate - class model_evaluator_util { - ast_manager& m; - model_ref m_model; - model_evaluator* m_mev; - - /// initialize with a given model. All previous state is lost. model can be NULL - void reset (model *model); - public: - model_evaluator_util(ast_manager& m); - ~model_evaluator_util(); - - void set_model(model &model) {reset (&model);} - model_ref &get_model() {return m_model;} - ast_manager& get_ast_manager() const {return m;} - - public: - bool is_true (const expr_ref_vector &v); - bool is_false(expr* x); - bool is_true(expr* x); - - bool eval (const expr_ref_vector &v, expr_ref &result, bool model_completion); - /// evaluates an expression - bool eval (expr *e, expr_ref &result, bool model_completion); - // expr_ref eval(expr* e, bool complete=true); - }; - /** \brief hoist non-boolean if expressions. */ @@ -146,7 +118,7 @@ namespace spacer { */ void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars); - void mbqi_project (model &M, app_ref_vector &vars, expr_ref &fml); + void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml); bool contains_selects (expr* fml, ast_manager& m); void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); From 0adf66dc0acda02437b3d25608a1fc660ebd02bc Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 17 Jun 2018 13:16:36 +0200 Subject: [PATCH 7/7] python: fix usage of fpa_get_numeral_significand_uint64 --- src/api/python/z3/z3.py | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index bd954d8ff..5e83a4181 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -8858,7 +8858,10 @@ class FPNumRef(FPRef): 1.25 """ def significand_as_long(self): - return Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast()) + ptr = (ctypes.c_ulonglong * 1)() + if not Z3_fpa_get_numeral_significand_uint64(self.ctx.ref(), self.as_ast(), ptr): + raise Z3Exception("error retrieving the significand of a numeral.") + return ptr[0] """The significand of the numeral as a bit-vector expression.