diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index ebcbb9145..8941c511a 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -87,8 +87,8 @@ namespace spacer { m_mev = nullptr; } m_model = model; - if (!m_model) { return; } - m_mev = alloc(model_evaluator, *m_model); + if (m_model) + m_mev = alloc(model_evaluator, *m_model); } bool model_evaluator_util::eval(expr *e, expr_ref &result, bool model_completion) { @@ -127,334 +127,6 @@ namespace spacer { return eval(x, res, false) && m.is_true (res); } - void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { - ast_manager& m = fml.get_manager(); - expr_ref_vector conjs(m); - flatten_and(fml, conjs); - obj_map diseqs; - expr* n, *lhs, *rhs; - for (unsigned i = 0; i < conjs.size(); ++i) { - if (m.is_not(conjs[i].get(), n) && m.is_eq(n, lhs, rhs)) { - if (!m.is_value(rhs)) { - std::swap(lhs, rhs); - } - if (!m.is_value(rhs)) { - continue; - } - diseqs.insert_if_not_there2(lhs, 0)->get_data().m_value++; - } - } - expr_substitution sub(m); - - unsigned orig_size = conjs.size(); - unsigned num_deleted = 0; - expr_ref val(m), tmp(m); - proof_ref pr(m); - pr = m.mk_asserted(m.mk_true()); - for (auto const& kv : diseqs) { - if (kv.m_value >= threshold) { - model.eval(kv.m_key, val); - sub.insert(kv.m_key, val, pr); - conjs.push_back(m.mk_eq(kv.m_key, val)); - num_deleted += kv.m_value; - } - } - if (orig_size < conjs.size()) { - scoped_ptr rep = mk_expr_simp_replacer(m); - rep->set_substitution(&sub); - for (unsigned i = 0; i < orig_size; ++i) { - tmp = conjs[i].get(); - (*rep)(tmp); - if (m.is_true(tmp)) { - conjs[i] = conjs.back(); - SASSERT(orig_size <= conjs.size()); - conjs.pop_back(); - SASSERT(orig_size <= 1 + conjs.size()); - if (i + 1 == orig_size) { - // no-op. - } - else if (orig_size <= conjs.size()) { - // no-op - } - else { - SASSERT(orig_size == 1 + conjs.size()); - --orig_size; - --i; - } - } - else { - conjs[i] = tmp; - } - } - IF_VERBOSE(2, verbose_stream() << "Deleted " << num_deleted << " disequalities " << conjs.size() << " conjuncts\n";); - } - fml = m.mk_and(conjs.size(), conjs.c_ptr()); - } - - // - // (f (if c1 (if c2 e1 e2) e3) b c) -> - // (if c1 (if c2 (f e1 b c) - - class ite_hoister { - ast_manager& m; - public: - ite_hoister(ast_manager& m): m(m) {} - - br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { - if (m.is_ite(f)) { - return BR_FAILED; - } - for (unsigned i = 0; i < num_args; ++i) { - expr* c, *t, *e; - if (!m.is_bool(args[i]) && m.is_ite(args[i], c, t, e)) { - expr_ref e1(m), e2(m); - ptr_vector args1(num_args, args); - args1[i] = t; - e1 = m.mk_app(f, num_args, args1.c_ptr()); - if (t == e) { - result = e1; - return BR_REWRITE1; - } - args1[i] = e; - e2 = m.mk_app(f, num_args, args1.c_ptr()); - result = m.mk_app(f, num_args, args); - result = m.mk_ite(c, e1, e2); - return BR_REWRITE3; - } - } - return BR_FAILED; - } - }; - - struct ite_hoister_cfg: public default_rewriter_cfg { - ite_hoister m_r; - bool rewrite_patterns() const { return false; } - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - return m_r.mk_app_core(f, num, args, result); - } - ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} - }; - - class ite_hoister_star : public rewriter_tpl { - ite_hoister_cfg m_cfg; - public: - ite_hoister_star(ast_manager & m, params_ref const & p): - rewriter_tpl(m, false, m_cfg), - m_cfg(m, p) {} - }; - - void hoist_non_bool_if(expr_ref& fml) { - ast_manager& m = fml.get_manager(); - scoped_no_proof _sp(m); - params_ref p; - ite_hoister_star ite_rw(m, p); - expr_ref tmp(m); - ite_rw(fml, tmp); - fml = tmp; - } - - class test_diff_logic { - ast_manager& m; - arith_util a; - bv_util bv; - bool m_is_dl; - bool m_test_for_utvpi; - - bool is_numeric(expr* e) const { - if (a.is_numeral(e)) { - return true; - } - expr* cond, *th, *el; - if (m.is_ite(e, cond, th, el)) { - return is_numeric(th) && is_numeric(el); - } - return false; - } - - bool is_arith_expr(expr *e) const { - return is_app(e) && a.get_family_id() == to_app(e)->get_family_id(); - } - - bool is_offset(expr* e) const { - if (a.is_numeral(e)) { - return true; - } - expr* cond, *th, *el, *e1, *e2; - if (m.is_ite(e, cond, th, el)) { - return is_offset(th) && is_offset(el); - } - // recognize offsets. - if (a.is_add(e, e1, e2)) { - if (is_numeric(e1)) { - return is_offset(e2); - } - if (is_numeric(e2)) { - return is_offset(e1); - } - return false; - } - if (m_test_for_utvpi) { - if (a.is_mul(e, e1, e2)) { - if (is_minus_one(e1)) { - return is_offset(e2); - } - if (is_minus_one(e2)) { - return is_offset(e1); - } - } - } - return !is_arith_expr(e); - } - - bool is_minus_one(expr const * e) const { - rational r; - return a.is_numeral(e, r) && r.is_minus_one(); - } - - bool test_ineq(expr* e) const { - SASSERT(a.is_le(e) || a.is_ge(e) || m.is_eq(e)); - SASSERT(to_app(e)->get_num_args() == 2); - expr * lhs = to_app(e)->get_arg(0); - expr * rhs = to_app(e)->get_arg(1); - if (is_offset(lhs) && is_offset(rhs)) - { return true; } - if (!is_numeric(rhs)) - { std::swap(lhs, rhs); } - if (!is_numeric(rhs)) - { return false; } - // lhs can be 'x' or '(+ x (* -1 y))' - if (is_offset(lhs)) - { return true; } - expr* arg1, *arg2; - if (!a.is_add(lhs, arg1, arg2)) - { return false; } - // x - if (m_test_for_utvpi) { - return is_offset(arg1) && is_offset(arg2); - } - if (is_arith_expr(arg1)) - { std::swap(arg1, arg2); } - if (is_arith_expr(arg1)) - { return false; } - // arg2: (* -1 y) - expr* m1, *m2; - if (!a.is_mul(arg2, m1, m2)) - { return false; } - return is_minus_one(m1) && is_offset(m2); - } - - bool test_eq(expr* e) const { - expr* lhs, *rhs; - VERIFY(m.is_eq(e, lhs, rhs)); - if (!a.is_int_real(lhs)) { - return true; - } - if (a.is_numeral(lhs) || a.is_numeral(rhs)) { - return test_ineq(e); - } - return - test_term(lhs) && - test_term(rhs) && - !a.is_mul(lhs) && - !a.is_mul(rhs); - } - - bool test_term(expr* e) const { - if (m.is_bool(e)) { - return true; - } - if (a.is_numeral(e)) { - return true; - } - if (is_offset(e)) { - return true; - } - expr* lhs, *rhs; - if (a.is_add(e, lhs, rhs)) { - if (!a.is_numeral(lhs)) { - std::swap(lhs, rhs); - } - return a.is_numeral(lhs) && is_offset(rhs); - } - if (a.is_mul(e, lhs, rhs)) { - return is_minus_one(lhs) || is_minus_one(rhs); - } - return false; - } - - bool is_non_arith_or_basic(expr* e) - { - if (!is_app(e)) { - return false; - } - family_id fid = to_app(e)->get_family_id(); - - if (fid == null_family_id && - !m.is_bool(e) && - to_app(e)->get_num_args() > 0) { - return true; - } - return - fid != m.get_basic_family_id() && - fid != null_family_id && - fid != a.get_family_id() && - fid != bv.get_family_id(); - } - - public: - test_diff_logic(ast_manager& m): m(m), a(m), bv(m), m_is_dl(true), m_test_for_utvpi(false) {} - - void test_for_utvpi() { m_test_for_utvpi = true; } - - void operator()(expr* e) { - if (!m_is_dl) { - return; - } - if (a.is_le(e) || a.is_ge(e)) { - m_is_dl = test_ineq(e); - } else if (m.is_eq(e)) { - m_is_dl = test_eq(e); - } else if (is_non_arith_or_basic(e)) { - m_is_dl = false; - } else if (is_app(e)) { - app* a = to_app(e); - for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) { - m_is_dl = test_term(a->get_arg(i)); - } - } - - if (!m_is_dl) { - char const* msg = "non-diff: "; - if (m_test_for_utvpi) { - msg = "non-utvpi: "; - } - IF_VERBOSE(1, verbose_stream() << msg << mk_pp(e, m) << "\n";); - } - } - - bool is_dl() const { return m_is_dl; } - }; - - bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { - test_diff_logic test(m); - expr_fast_mark1 mark; - for (unsigned i = 0; i < num_fmls; ++i) { - quick_for_each_expr(test, mark, fmls[i]); - } - return test.is_dl(); - } - - bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls) { - test_diff_logic test(m); - test.test_for_utvpi(); - expr_fast_mark1 mark; - for (unsigned i = 0; i < num_fmls; ++i) { - quick_for_each_expr(test, mark, fmls[i]); - } - return test.is_dl(); - } - - void subst_vars(ast_manager& m, app_ref_vector const& vars, model* M, expr_ref& fml) { @@ -469,45 +141,45 @@ namespace spacer { sub (fml); } -void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) { - ast_manager &m = vars.m(); - ast_pp_util pp(m); - pp.collect(fml); - pp.display_decls(out); + void to_mbp_benchmark(std::ostream &out, expr* fml, const app_ref_vector &vars) { + ast_manager &m = vars.m(); + ast_pp_util pp(m); + pp.collect(fml); + pp.display_decls(out); - out << "(define-fun mbp_benchmark_fml () Bool\n "; - out << mk_pp(fml, m) << ")\n\n"; + out << "(define-fun mbp_benchmark_fml () Bool\n "; + out << mk_pp(fml, m) << ")\n\n"; + + out << "(push)\n" + << "(assert mbp_benchmark_fml)\n" + << "(check-sat)\n" + << "(mbp mbp_benchmark_fml ("; + for (auto v : vars) {out << mk_pp(v, m) << " ";} + out << "))\n" + << "(pop)\n" + << "(exit)\n"; + } - out << "(push)\n" - << "(assert mbp_benchmark_fml)\n" - << "(check-sat)\n" - << "(mbp mbp_benchmark_fml ("; - for (auto v : vars) {out << mk_pp(v, m) << " ";} - out << "))\n" - << "(pop)\n" - << "(exit)\n"; -} - -void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml, + 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, 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); -} - + 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); + } + /* * eliminate simple equalities using qe_lite * 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, - bool dont_sub) { + const model_ref& M, bool reduce_all_selects, bool use_native_mbp, + bool dont_sub) { th_rewriter rw (m); TRACE ("spacer_mbp", tout << "Before projection:\n"; @@ -533,70 +205,70 @@ void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml, expr_ref bval (m); while (true) { - params_ref p; - qe_lite qe(m, p, false); - qe (vars, fml); - rw (fml); - - TRACE ("spacer_mbp", - tout << "After qe_lite:\n"; - tout << mk_pp (fml, m) << "\n"; - tout << "Vars:\n" << vars;); - - SASSERT (!m.is_false (fml)); - - - // 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); - } else if (arr_u.is_array(v)) { - array_vars.push_back (v); - } else { - SASSERT (ari_u.is_int (v) || ari_u.is_real (v)); - arith_vars.push_back (v); - } - } - - // substitute Booleans - if (!bool_sub.empty()) { - bool_sub (fml); - // -- bool_sub is not simplifying + params_ref p; + qe_lite qe(m, p, false); + qe (vars, fml); rw (fml); + + TRACE ("spacer_mbp", + tout << "After qe_lite:\n"; + tout << mk_pp (fml, m) << "\n"; + tout << "Vars:\n" << vars;); + SASSERT (!m.is_false (fml)); - TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); - bool_sub.reset (); + + + // 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); + } else if (arr_u.is_array(v)) { + array_vars.push_back (v); + } else { + SASSERT (ari_u.is_int (v) || ari_u.is_real (v)); + arith_vars.push_back (v); + } + } + + // substitute Booleans + if (!bool_sub.empty()) { + bool_sub (fml); + // -- bool_sub is not simplifying + rw (fml); + SASSERT (!m.is_false (fml)); + TRACE ("spacer_mbp", tout << "Projected Booleans:\n" << fml << "\n"; ); + bool_sub.reset (); + } + + TRACE ("spacer_mbp", + tout << "Array vars:\n"; + tout << array_vars;); + + vars.reset (); + + // project arrays + { + 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); + SASSERT (array_vars.empty ()); + srw (fml); + SASSERT (!m.is_false (fml)); + } + + TRACE ("spacer_mbp", + tout << "extended model:\n"; + model_pp (tout, *M); + tout << "Auxiliary variables of index and value sorts:\n"; + tout << vars; + ); + + if (vars.empty()) { break; } } - - TRACE ("spacer_mbp", - tout << "Array vars:\n"; - tout << array_vars;); - - vars.reset (); - - // project arrays - { - 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); - SASSERT (array_vars.empty ()); - srw (fml); - SASSERT (!m.is_false (fml)); - } - - TRACE ("spacer_mbp", - tout << "extended model:\n"; - model_pp (tout, *M); - tout << "Auxiliary variables of index and value sorts:\n"; - tout << vars; - ); - - if (vars.empty()) { break; } - } - + // project reals and ints if (!arith_vars.empty ()) { TRACE ("spacer_mbp", tout << "Arith vars:\n" << arith_vars;); @@ -661,27 +333,26 @@ void qe_project_z3 (ast_manager& m, app_ref_vector& vars, expr_ref& fml, ptr_vector const& acc, unsigned j, func_decl* f, - expr* c) -{ + expr* c) + { if (is_app(c) && to_app(c)->get_decl() == f) { return to_app(c)->get_arg(j); - } else { + } else { return m.mk_app(acc[j], c); } } -void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, - const model_ref& M, 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); - else - qe_project_spacer(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); -} + 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, + bool dont_sub) { + if (use_native_mbp) + qe_project_z3(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); + else + qe_project_spacer(m, vars, fml, M, reduce_all_selects, use_native_mbp, dont_sub); + } -void expand_literals(ast_manager &m, expr_ref_vector& conjs) -{ - if (conjs.empty()) { return; } + void expand_literals(ast_manager &m, expr_ref_vector& conjs) { + if (conjs.empty()) { return; } arith_util arith(m); datatype_util dt(m); bv_util bv(m); @@ -689,11 +360,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) rational r; unsigned bv_size; - TRACE("spacer_expand", - tout << "begin expand\n"; - for (unsigned i = 0; i < conjs.size(); ++i) { - tout << mk_pp(conjs[i].get(), m) << "\n"; - }); + TRACE("spacer_expand", tout << "begin expand\n" << conjs << "\n";); for (unsigned i = 0; i < conjs.size(); ++i) { expr* e = conjs[i].get(); @@ -701,13 +368,13 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) conjs[i] = arith.mk_le(e1,e2); if (i+1 == conjs.size()) { conjs.push_back(arith.mk_ge(e1, e2)); - } else { + } else { conjs.push_back(conjs[i+1].get()); conjs[i+1] = arith.mk_ge(e1, e2); } ++i; - } else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || - (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){ + } else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || + (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))) { func_decl* f = to_app(val)->get_decl(); func_decl* r = dt.get_constructor_is(f); conjs[i] = m.mk_app(r, c); @@ -715,12 +382,11 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) for (unsigned j = 0; j < acc.size(); ++j) { conjs.push_back(m.mk_eq(apply_accessor(m, acc, j, f, c), to_app(val)->get_arg(j))); } - } else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || - (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { + } else if ((m.is_eq(e, c, val) && bv.is_numeral(val, r, bv_size)) || + (m.is_eq(e, val, c) && bv.is_numeral(val, r, bv_size))) { rational two(2); for (unsigned j = 0; j < bv_size; ++j) { parameter p(j); - //expr* e = m.mk_app(bv.get_family_id(), OP_BIT2BOOL, 1, &p, 1, &c); expr* e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), bv.mk_extract(j, j, c)); if ((r % two).is_zero()) { e = m.mk_not(e); @@ -728,21 +394,17 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) r = div(r, two); if (j == 0) { conjs[i] = e; - } else { + } else { conjs.push_back(e); } } } } - TRACE("spacer_expand", - tout << "end expand\n"; - for (unsigned i = 0; i < conjs.size(); ++i) { - tout << mk_pp(conjs[i].get(), m) << "\n"; - }); + TRACE("spacer_expand", tout << "end expand\n" << conjs << "\n";); } namespace { -class implicant_picker { + class implicant_picker { model_evaluator_util &m_mev; ast_manager &m; arith_util m_arith; @@ -751,8 +413,7 @@ class implicant_picker { expr_mark m_visited; - void add_literal (expr *e, expr_ref_vector &out) - { + void add_literal (expr *e, expr_ref_vector &out) { SASSERT (m.is_bool (e)); expr_ref res (m), v(m); @@ -773,251 +434,245 @@ class implicant_picker { if (m.is_not(res, nres)) { // -- (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)) { expr_ref u(m); u = m_arith.mk_lt(f1, f2); if (m_mev.eval (u, v, false) && m.is_true (v)) - { res = u; } + { res = u; } else - { res = m_arith.mk_lt(f2, f1); } + { res = m_arith.mk_lt(f2, f1); } } } - if (!m_mev.is_true (res)) - { verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n"; } + if (!m_mev.is_true (res)) { + verbose_stream() << "Bad literal: " << mk_pp(res, m) << "\n"; + } SASSERT (m_mev.is_true (res)); out.push_back (res); } - void process_app(app *a, expr_ref_vector &out) - { - if (m_visited.is_marked(a)) { return; } + void process_app(app *a, expr_ref_vector &out) { + if (m_visited.is_marked(a)) { return; } SASSERT (m.is_bool (a)); expr_ref v(m); m_mev.eval (a, v, false); - - if (!m.is_true(v) && !m.is_false(v)) { return; } - + bool is_true = m.is_true(v); + + if (!is_true && !m.is_false(v)) return; + expr *na, *f1, *f2, *f3; - - if (a->get_family_id() != m.get_basic_family_id()) - { add_literal(a, out); } - else if (is_uninterp_const(a)) - { add_literal(a, out); } - else if (m.is_not(a, na) && m.is_not(na, na)) - { m_todo.push_back(na); } - else if (m.is_not(a, na)) - { m_todo.push_back(na); } + + if (a->get_family_id() != m.get_basic_family_id()) { + add_literal(a, out); + } + else if (is_uninterp_const(a)) { + add_literal(a, out); + } + else if (m.is_not(a, na)) { + m_todo.push_back(na); + } else if (m.is_distinct(a)) { - if (m.is_false(v)) - m_todo.push_back - (qe::project_plugin::pick_equality(m, *m_mev.get_model(), a)); - else if (a->get_num_args() == 2) - { add_literal(a, out); } - else - m_todo.push_back(m.mk_distinct_expanded(a->get_num_args(), - a->get_args())); - } else if (m.is_and(a)) { - if (m.is_true(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } - else if (m.is_false(v)) { - for (unsigned i = 0, sz = a->get_num_args (); i < sz; ++i) { - if (m_mev.is_false(a->get_arg(i))) { - m_todo.push_back(a->get_arg(i)); + if (!is_true) { + f1 = qe::project_plugin::pick_equality(m, *m_mev.get_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())); + } + } + else if (m.is_and(a)) { + if (is_true) { + m_todo.append(a->get_num_args(), a->get_args()); + } + else { + for (expr* e : *a) { + if (m_mev.is_false(e)) { + m_todo.push_back(e); break; } } } - } else if (m.is_or(a)) { - if (m.is_false(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } - else if (m.is_true(v)) { - for (unsigned i = 0, sz = a->get_num_args(); i < sz; ++i) { - if (m_mev.is_true(a->get_arg(i))) { - m_todo.push_back(a->get_arg(i)); + } + else if (m.is_or(a)) { + if (!is_true) + m_todo.append(a->get_num_args(), a->get_args()); + else { + for (expr * e : *a) { + if (m_mev.is_true(e)) { + m_todo.push_back(e); break; } } } - } else if (m.is_iff(a, f1, f2) || m.is_eq(a, f1, f2) || - (m.is_true(v) && m.is_not(a, na) && m.is_xor (na, f1, f2))) { + } + else if (m.is_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))) - { m_todo.append(a->get_num_args(), a->get_args()); } + 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); } + add_literal(a, out); + } + } + else if (m.is_ite(a, f1, f2, f3)) { + if (m.are_equal(f2, f3)) { + m_todo.push_back(f2); } - } else if (m.is_ite(a, f1, f2, f3)) { - if (m.are_equal(f2, f3)) { m_todo.push_back(f2); } else if (m_mev.is_true (f2) && m_mev.is_true (f3)) { - m_todo.push_back(f2); - m_todo.push_back(f3); - } else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { - m_todo.push_back(f2); - m_todo.push_back(f3); - } else if (m_mev.is_true(f1)) { - m_todo.push_back(f1); - m_todo.push_back(f2); - } else if (m_mev.is_false(f1)) { - m_todo.push_back(f1); - m_todo.push_back(f3); + m_todo.push_back(f2); + m_todo.push_back(f3); + } + else if (m_mev.is_false(f2) && m_mev.is_false(f3)) { + m_todo.push_back(f2); + m_todo.push_back(f3); + } + else if (m_mev.is_true(f1)) { + m_todo.push_back(f1); + m_todo.push_back(f2); + } + else if (m_mev.is_false(f1)) { + m_todo.push_back(f1); + m_todo.push_back(f3); } - } else if (m.is_xor(a, f1, f2)) - { m_todo.append(a->get_num_args(), a->get_args()); } + } + else if (m.is_xor(a, f1, f2)) { + m_todo.append(a->get_num_args(), a->get_args()); + } else if (m.is_implies(a, f1, f2)) { - if (m.is_true (v)) { - if (m_mev.is_true(f2)) { m_todo.push_back(f2); } - else if (m_mev.is_false(f1)) { m_todo.push_back(f1); } - } else if (m.is_false(v)) - { m_todo.append(a->get_num_args(), a->get_args()); } - } else if (m.is_true(a) || m.is_false(a)) { /* nothing */ } + if (is_true) { + if (m_mev.is_true(f2)) + m_todo.push_back(f2); + else if (m_mev.is_false(f1)) + m_todo.push_back(f1); + } + else + m_todo.append(a->get_num_args(), a->get_args()); + } else { - verbose_stream () << "Unexpected expression: " - << mk_pp(a, m) << "\n"; + IF_VERBOSE(0, verbose_stream () << "Unexpected expression: " << mk_pp(a, m) << "\n"); UNREACHABLE(); } } - - void pick_literals(expr *e, expr_ref_vector &out) - { + + void pick_literals(expr *e, expr_ref_vector &out) { SASSERT(m_todo.empty()); - if (m_visited.is_marked(e)) { return; } - SASSERT(is_app(e)); - + if (m_visited.is_marked(e) || !is_app(e)) return; + m_todo.push_back(e); do { - app *a = to_app(m_todo.back()); + e = m_todo.back(); + if (!is_app(e)) continue; + app * a = to_app(e); m_todo.pop_back(); process_app(a, out); m_visited.mark(a, true); } while (!m_todo.empty()); } - - bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) - { + + bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) { m_visited.reset(); - expr_ref e(m); - e = mk_and (in); - bool is_true = m_mev.is_true (e); - - for (unsigned i = 0, sz = in.size (); i < sz; ++i) { - if (is_true || m_mev.is_true(in.get(i))) - { pick_literals(in.get(i), out); } + bool is_true = m_mev.is_true (in); + + for (expr* e : in) { + if (is_true || m_mev.is_true(e)) { + pick_literals(e, out); + } } - m_visited.reset (); return is_true; } public: + implicant_picker (model_evaluator_util &mev) : m_mev (mev), m (m_mev.get_ast_manager ()), m_arith(m), m_todo(m) {} - - void operator() (expr_ref_vector &in, expr_ref_vector& out) - {pick_implicant (in, out);} - }; - } - - void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, - expr_ref_vector &res) { - // XXX what is the point of flattening? - flatten_and (formula); - if (formula.empty()) { return; } - - implicant_picker ipick (mev); - 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 (unsigned i = 0; i < cube.size(); ++i) { - g->assert_expr(cube.get(i)); - } - - expr_ref tmp(m); - goal_ref_buffer result; - tactic_ref simplifier = mk_arith_bounds_tactic(m); - (*simplifier)(g, result); - SASSERT(result.size() == 1); - goal* r = result[0]; - - cube.reset(); - for (unsigned i = 0; i < r->size(); ++i) { - cube.push_back(r->form(i)); - } -} - -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 (unsigned i = 0, sz = cube.size(); i < sz; ++i) { - g->assert_expr(cube.get(i)); - } - - goal_ref_buffer goals; - tactic_ref prop_values = mk_propagate_values_tactic(m); - tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m); - tactic_ref t = and_then(prop_values.get(), prop_bounds.get()); - - (*t)(g, goals); - SASSERT(goals.size() == 1); - - g = goals[0]; - cube.reset(); - for (unsigned i = 0; i < g->size(); ++i) { - cube.push_back(g->form(i)); - } -} - -void simplify_bounds(expr_ref_vector &cube) { - simplify_bounds_new(cube); -} - -/// Adhoc rewriting of arithmetic expressions -struct adhoc_rewriter_cfg : public default_rewriter_cfg { - ast_manager &m; - arith_util m_util; - - adhoc_rewriter_cfg (ast_manager &manager) : m(manager), m_util(m) {} - - bool is_le(func_decl const * n) const - { return is_decl_of(n, m_util.get_family_id (), OP_LE); } - bool is_ge(func_decl const * n) const - { return is_decl_of(n, m_util.get_family_id (), OP_GE); } - - br_status reduce_app (func_decl * f, unsigned num, expr * const * args, - expr_ref & result, proof_ref & result_pr) - { - expr * e; - br_status st = BR_FAILED; - if (is_le(f)) { - st = mk_le_core (args[0], args[1], result); - } else if (is_ge(f)) { - st = mk_ge_core (args[0], args[1], result); - } else if (m.is_not(f)) { - if (m.is_not (args[0], e)) { - result = e; - st = BR_DONE; - } - } - - return st; + + void operator() (expr_ref_vector &in, expr_ref_vector& out) { + pick_implicant (in, out); } + }; +} - br_status mk_le_core (expr *arg1, expr * arg2, expr_ref & result) - { + void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula, + expr_ref_vector &res) { + implicant_picker ipick (mev); + 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) + g->assert_expr(c); + + goal_ref_buffer result; + tactic_ref simplifier = mk_arith_bounds_tactic(m); + (*simplifier)(g, result); + SASSERT(result.size() == 1); + goal* r = result[0]; + cube.reset(); + for (unsigned i = 0; i < r->size(); ++i) { + cube.push_back(r->form(i)); + } + } + + 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) + g->assert_expr(c); + + goal_ref_buffer goals; + tactic_ref prop_values = mk_propagate_values_tactic(m); + tactic_ref prop_bounds = mk_propagate_ineqs_tactic(m); + tactic_ref t = and_then(prop_values.get(), prop_bounds.get()); + + (*t)(g, goals); + SASSERT(goals.size() == 1); + + g = goals[0]; + cube.reset(); + for (unsigned i = 0; i < g->size(); ++i) { + cube.push_back(g->form(i)); + } + } + + void simplify_bounds(expr_ref_vector &cube) { + simplify_bounds_new(cube); + } + + /// Adhoc rewriting of arithmetic expressions + struct adhoc_rewriter_cfg : public default_rewriter_cfg { + ast_manager &m; + arith_util m_util; + + 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, + expr_ref & result, proof_ref & result_pr) { + expr * e; + if (is_le(f)) + 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)) { + 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 ())); @@ -1025,63 +680,63 @@ struct adhoc_rewriter_cfg : public default_rewriter_cfg { } return BR_FAILED; } - br_status mk_ge_core (expr * arg1, expr * arg2, expr_ref & result) - { + 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 ())); 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, - 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); - // poly_rewriter - params.set_bool ("som", true); - params.set_bool ("flat", true); - - // apply rewriter - th_rewriter rw(out.m(), params); - rw (e, 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); - - 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()); - - if (use_simplify_bounds) { - // remove redundant inequalities - simplify_bounds (v); - } - if (use_factor_eqs) { - // -- refactor equivalence classes and choose a representative - spacer::term_graph egraph(out.m()); - egraph.add_lits (v); - v.reset(); - egraph.to_lits(v); - } + 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); + // poly_rewriter + params.set_bool ("som", true); + params.set_bool ("flat", true); + + // apply rewriter + th_rewriter rw(out.m(), params); + rw (e, 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); + + 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()); + + if (use_simplify_bounds) { + // remove redundant inequalities + simplify_bounds (v); + } + if (use_factor_eqs) { + // -- refactor equivalence classes and choose a representative + spacer::term_graph egraph(out.m()); + egraph.add_lits (v); + v.reset(); + egraph.to_lits(v); + } + TRACE("spacer_normalize", tout << "Normalized:\n" << out << "\n" @@ -1089,39 +744,33 @@ void normalize (expr *e, expr_ref &out, << mk_and(v) << "\n";); TRACE("spacer_normalize", spacer::term_graph egraph(out.m()); - for (unsigned i = 0, sz = v.size(); i < sz; ++i) - egraph.add_lit (to_app(v.get(i))); + 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); + } } } -} -// rewrite term such that the pretty printing is easier to read -struct adhoc_rewriter_rpp : public default_rewriter_cfg { - ast_manager &m; - arith_util m_arith; - - adhoc_rewriter_rpp (ast_manager &manager) : m(manager), m_arith(m) {} - - bool is_le(func_decl const * n) const - { return is_decl_of(n, m_arith.get_family_id (), OP_LE); } - bool is_ge(func_decl const * n) const - { return is_decl_of(n, m_arith.get_family_id (), OP_GE); } - bool is_lt(func_decl const * n) const - { return is_decl_of(n, m_arith.get_family_id (), OP_LT); } - bool is_gt(func_decl const * n) const - { return is_decl_of(n, m_arith.get_family_id (), OP_GT); } - 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, - expr_ref & result, proof_ref & result_pr) + // rewrite term such that the pretty printing is easier to read + struct adhoc_rewriter_rpp : public default_rewriter_cfg { + ast_manager &m; + arith_util m_arith; + + 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();} + + 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) && @@ -1170,67 +819,63 @@ struct adhoc_rewriter_rpp : public default_rewriter_cfg { } return st; } + }; -}; - -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) { - m_epp_params.set_uint("min_alias_size", UINT_MAX); - m_epp_params.set_uint("max_depth", UINT_MAX); - - if (is_expr (m_ast)) { - rw(to_expr(m_ast), m_epp_expr); - m_ast = m_epp_expr; + 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) { + m_epp_params.set_uint("min_alias_size", UINT_MAX); + m_epp_params.set_uint("max_depth", UINT_MAX); + + if (is_expr (m_ast)) { + rw(to_expr(m_ast), m_epp_expr); + m_ast = m_epp_expr; + } } -} - -void mk_epp::rw(expr *e, expr_ref &out) -{ - adhoc_rewriter_rpp cfg(out.m()); - rewriter_tpl arw(out.m(), false, cfg); - arw(e, out); -} - -void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { - expr_free_vars fv; - ast_manager &m = out.get_manager(); - - fv(e); - if (vars.size() < fv.size()) { - vars.resize(fv.size()); + + void mk_epp::rw(expr *e, expr_ref &out) { + adhoc_rewriter_rpp cfg(out.m()); + rewriter_tpl arw(out.m(), false, cfg); + arw(e, out); } - 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); + + void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { + expr_free_vars fv; + ast_manager &m = out.get_manager(); + + fv(e); + if (vars.size() < fv.size()) { + vars.resize(fv.size()); + } + 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); + } } -} - struct index_term_finder { - ast_manager &m; - array_util m_array; - app_ref m_var; + ast_manager &m; + array_util m_array; + app_ref m_var; expr_ref_vector &m_res; index_term_finder (ast_manager &mgr, app* v, expr_ref_vector &res) : m(mgr), m_array (m), m_var (v, m), m_res (res) {} void operator() (var *n) {} void operator() (quantifier *n) {} void operator() (app *n) { - expr *e1, *e2; - if (m_array.is_select (n) && n->get_arg (1) != m_var) { - m_res.push_back (n->get_arg (1)); - } else if (m.is_eq(n, e1, e2)) { - if (e1 == m_var) { m_res.push_back(e2); } - else if (e2 == m_var) { m_res.push_back(e1); } - } + 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); + ++i; + } + } } }; - bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) - { + bool mbqi_project_var (model_evaluator_util &mev, app* var, expr_ref &fml) { ast_manager &m = fml.get_manager (); expr_ref val(m); @@ -1238,26 +883,21 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { TRACE ("mbqi_project_verbose", tout << "MBQI: var: " << mk_pp (var, m) << "\n" - << "fml: " << mk_pp (fml, 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"; - for (unsigned i = 0, e = terms.size (); i < e; ++i) - tout << i << ": " << mk_pp (terms.get (i), m) << "\n"; - ); - - for (unsigned i = 0, e = terms.size(); i < e; ++i) { - expr* term = terms.get (i); + tout << "terms:\n" << terms << "\n";); + + for (expr * term : terms) { expr_ref tval (m); mev.eval (term, tval, false); TRACE ("mbqi_project_verbose", tout << "term: " << mk_pp (term, m) - << " tval: " << mk_pp (tval, m) + << " tval: " << tval << " val: " << mk_pp (val, m) << "\n";); // -- if the term does not contain an occurrence of var @@ -1273,13 +913,12 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { } TRACE ("mbqi_project", - tout << "MBQI: failed to eliminate " << mk_pp (var, m) << " from " << mk_pp (fml, m) << "\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 &M, app_ref_vector &vars, expr_ref &fml) { ast_manager &m = fml.get_manager (); model_evaluator_util mev(m); mev.set_model (M); @@ -1288,110 +927,67 @@ void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) { mev.eval (fml, tmp, false); tmp.reset (); - for (unsigned idx = 0; idx < vars.size (); ) { - if (mbqi_project_var (mev, vars.get (idx), fml)) { - vars[idx] = vars.back (); - vars.pop_back (); - } else { - idx++; - } + unsigned j = 0; + for (app* v : vars) + if (!mbqi_project_var (mev, v, fml)) + vars[j++] = v; + vars.shrink(j); + } + + struct found {}; + struct check_select { + array_util a; + check_select(ast_manager& m): a(m) {} + void operator()(expr* n) {} + void operator()(app* n) { if (a.is_select(n)) throw found(); } + }; + + bool contains_selects(expr* fml, ast_manager& m) { + check_select cs(m); + try { + for_each_expr(cs, fml); + return false; + } + catch (found) { + return true; } } -bool contains_selects(expr* fml, ast_manager& m) -{ - array_util a_util(m); - if (!is_app(fml)) { return false; } - ast_mark done; - ptr_vector todo; - todo.push_back (to_app (fml)); - while (!todo.empty ()) { - app* a = todo.back (); - if (done.is_marked (a)) { - todo.pop_back (); - continue; - } - unsigned num_args = a->get_num_args (); - bool all_done = true; - for (unsigned i = 0; i < num_args; i++) { - expr* arg = a->get_arg (i); - if (!done.is_marked (arg) && is_app (arg)) { - todo.push_back (to_app (arg)); - all_done = false; - } - } - if (!all_done) { continue; } - todo.pop_back (); - if (a_util.is_select (a)) - { return true; } - done.mark (a, true); + struct collect_indices { + app_ref_vector& m_indices; + array_util a; + 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 (is_app(n->get_arg(i))) + m_indices.push_back(to_app(n->get_arg(i))); } - return false; + }; + + void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) { + collect_indices ci(indices); + for_each_expr(ci, fml); + } + + struct collect_decls { + app_ref_vector& m_decls; + std::string& prefix; + collect_decls(app_ref_vector& decls, std::string& p): m_decls(decls), prefix(p) {} + void operator()(expr* n) {} + void operator()(app* n) { + if (n->get_decl()->get_name().str().find(prefix) != std::string::npos) + m_decls.push_back(n); + } + }; + + void find_decls(expr* fml, app_ref_vector& decls, std::string& prefix) { + collect_decls cd(decls, prefix); + for_each_expr(cd, fml); } -void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) -{ - array_util a_util(m); - if (!is_app(fml)) { return; } - ast_mark done; - ptr_vector todo; - todo.push_back (to_app (fml)); - while (!todo.empty ()) { - app* a = todo.back (); - if (done.is_marked (a)) { - todo.pop_back (); - continue; - } - unsigned num_args = a->get_num_args (); - bool all_done = true; - for (unsigned i = 0; i < num_args; i++) { - expr* arg = a->get_arg (i); - if (!done.is_marked (arg) && is_app (arg)) { - todo.push_back (to_app (arg)); - all_done = false; - } - } - if (!all_done) { continue; } - todo.pop_back (); - if (a_util.is_select (a)) { - SASSERT(a->get_num_args() == 2); - indices.push_back(to_app(a->get_arg(1))); - } - done.mark (a, true); - } - } - -void find_decls(expr* fml, app_ref_vector& decls, std::string& prefix) -{ - if (!is_app(fml)) { return; } - ast_mark done; - ptr_vector todo; - todo.push_back (to_app (fml)); - while (!todo.empty ()) { - app* a = todo.back (); - if (done.is_marked (a)) { - todo.pop_back (); - continue; - } - unsigned num_args = a->get_num_args (); - bool all_done = true; - for (unsigned i = 0; i < num_args; i++) { - expr* arg = a->get_arg (i); - if (!done.is_marked (arg) && is_app (arg)) { - todo.push_back (to_app (arg)); - all_done = false; - } - } - if (!all_done) { continue; } - todo.pop_back (); - if (a->get_decl()->get_name().str().find(prefix) != std::string::npos) - { decls.push_back(a); } - done.mark (a, true); - } - return; } -} template class rewriter_tpl; template class rewriter_tpl; -template class rewriter_tpl; diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index ffbd81de7..f43195a97 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -44,135 +44,120 @@ class model_evaluator; namespace spacer { -inline unsigned infty_level () {return UINT_MAX;} - -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 prev_level (unsigned lvl) -{ - if(is_infty_level(lvl)) { return infty_level(); } - if(lvl == 0) { return 0; } - return lvl -1; -} - -struct pp_level { - unsigned m_level; - pp_level(unsigned l): m_level(l) {} -}; - -inline std::ostream& operator<<(std::ostream& out, pp_level const& p) -{ - if (is_infty_level(p.m_level)) { - return out << "oo"; - } else { - return out << p.m_level; + inline unsigned infty_level () { + return UINT_MAX; } -} + 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 prev_level (unsigned lvl) { + if (is_infty_level(lvl)) return infty_level(); + if (lvl == 0) return 0; + return lvl - 1; + } -typedef ptr_vector app_vector; -typedef ptr_vector decl_vector; -typedef obj_hashtable func_decl_set; + struct pp_level { + unsigned m_level; + pp_level(unsigned l): m_level(l) {} + }; + inline std::ostream& operator<<(std::ostream& out, pp_level const& p) { + if (is_infty_level(p.m_level)) { + return out << "oo"; + } else { + return out << p.m_level; + } + } -class model_evaluator_util { - ast_manager& m; - model_ref m_model; - model_evaluator* m_mev; + 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); + // expr_ref eval(expr* e, bool complete=true); + }; - /// 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(); + /** + \brief hoist non-boolean if expressions. + */ + + void to_mbp_benchmark(std::ostream &out, const expr* fml, const app_ref_vector &vars); - void set_model(model &model) {reset (&model);} - model_ref &get_model() {return m_model;} - ast_manager& get_ast_manager() const {return m;} + + // TBD: deprecate by qe::mbp + /** + * do the following in sequence + * 1. use qe_lite to cheaply eliminate vars + * 2. for remaining boolean vars, substitute using M + * 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, + bool dont_sub=false); -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 replace variables that are used in many disequalities by - an equality using the model. - - Assumption: the model satisfies the conjunctions. -*/ -void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml); - -/** - \brief hoist non-boolean if expressions. -*/ -void hoist_non_bool_if(expr_ref& fml); - -bool is_difference_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); - -bool is_utvpi_logic(ast_manager& m, unsigned num_fmls, expr* const* fmls); - -void to_mbp_benchmark(std::ostream &out, const expr* fml, - const app_ref_vector &vars); - -/** - * do the following in sequence - * 1. use qe_lite to cheaply eliminate vars - * 2. for remaining boolean vars, substitute using M - * 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, - bool dont_sub=false); - -void qe_project (ast_manager& m, app_ref_vector& vars, expr_ref& fml, model_ref& M, expr_map& map); - -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 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 - * disables aliasing of common sub-expressions -*/ -struct mk_epp : public mk_pp { - params_ref m_epp_params; - expr_ref m_epp_expr; + 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 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 + * disables aliasing of common sub-expressions + */ + struct mk_epp : public mk_pp { + 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); + }; } #endif