From a003af494b00a1ac09d86a72fd2babacaa99651d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 30 Aug 2020 20:09:27 -0700 Subject: [PATCH] release nodes Signed-off-by: Nikolaj Bjorner --- src/ast/euf/euf_egraph.cpp | 5 + src/ast/euf/euf_egraph.h | 1 + src/ast/euf/euf_etable.cpp | 2 +- src/sat/smt/CMakeLists.txt | 1 + src/sat/smt/ba_internalize.cpp | 9 +- src/sat/smt/ba_solver.cpp | 4 +- src/sat/smt/ba_solver.h | 3 +- src/sat/smt/euf_ackerman.cpp | 10 +- src/sat/smt/euf_internalize.cpp | 242 ++++++++++++++++++++++++++++++++ src/sat/smt/euf_model.cpp | 6 +- src/sat/smt/euf_solver.cpp | 121 +++------------- src/sat/smt/euf_solver.h | 15 +- src/sat/smt/sat_smt.h | 2 +- src/sat/smt/sat_th.h | 2 +- src/sat/tactic/goal2sat.cpp | 31 ++-- 15 files changed, 319 insertions(+), 135 deletions(-) create mode 100644 src/sat/smt/euf_internalize.cpp diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index c12815bfa52..50b622c29e5 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -130,6 +130,11 @@ namespace euf { return n; } + void egraph::~egraph() { + for (enode* n : m_nodes) + n->~enode(); + } + void egraph::pop(unsigned num_scopes) { if (num_scopes <= m_num_scopes) { m_num_scopes -= num_scopes; diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h index b68ee0b201f..de7accda632 100644 --- a/src/ast/euf/euf_egraph.h +++ b/src/ast/euf/euf_egraph.h @@ -106,6 +106,7 @@ namespace euf { public: egraph(ast_manager& m): m(m), m_table(m), m_exprs(m) {} + ~egraph(); enode* find(expr* f) { return m_expr2enode.get(f->get_id(), nullptr); } enode* mk(expr* f, unsigned n, enode *const* args); void push() { ++m_num_scopes; } diff --git a/src/ast/euf/euf_etable.cpp b/src/ast/euf/euf_etable.cpp index 3b6ec82732c..22c4abaf016 100644 --- a/src/ast/euf/euf_etable.cpp +++ b/src/ast/euf/euf_etable.cpp @@ -169,7 +169,7 @@ namespace euf { binary_table* tb = UNTAG(binary_table*, t); out << "b "; for (enode* n : *tb) { - out << n->get_owner_id() << " " << cg_binary_hash()(n) << " "; + out << n->get_owner_id() << " "; } out << "\n"; } diff --git a/src/sat/smt/CMakeLists.txt b/src/sat/smt/CMakeLists.txt index 5e238b68c95..c990f47b40f 100644 --- a/src/sat/smt/CMakeLists.txt +++ b/src/sat/smt/CMakeLists.txt @@ -5,6 +5,7 @@ z3_add_component(sat_smt xor_solver.cpp ba_internalize.cpp euf_ackerman.cpp + euf_internalize.cpp euf_solver.cpp euf_model.cpp COMPONENT_DEPENDENCIES diff --git a/src/sat/smt/ba_internalize.cpp b/src/sat/smt/ba_internalize.cpp index 352692ad13e..e28b1dd927f 100644 --- a/src/sat/smt/ba_internalize.cpp +++ b/src/sat/smt/ba_internalize.cpp @@ -21,7 +21,8 @@ Module Name: namespace sat { - literal ba_solver::internalize(expr* e, bool sign, bool root) { + literal ba_solver::internalize(expr* e, bool sign, bool root, bool redundant) { + flet _redundant(m_is_redundant, redundant); if (m_pb.is_pb(e)) return internalize_pb(e, sign, root); if (m.is_xor(e)) @@ -35,7 +36,7 @@ namespace sat { sat::bool_var v = s().add_var(true); lits.push_back(literal(v, true)); auto add_expr = [&](expr* a) { - literal lit = si.internalize(a); + literal lit = si.internalize(a, m_is_redundant); s().set_external(lit.var()); lits.push_back(lit); }; @@ -47,7 +48,7 @@ namespace sat { for (unsigned i = 1; i + 1 < lits.size(); ++i) { lits[i].neg(); } - add_xr(lits); + add_xr(lits, m_is_redundant); auto* aig = s().get_cut_simplifier(); if (aig) aig->add_xor(~lits.back(), lits.size() - 1, lits.c_ptr() + 1); sat::literal lit(v, sign); @@ -100,7 +101,7 @@ namespace sat { void ba_solver::convert_pb_args(app* t, literal_vector& lits) { for (expr* arg : *t) { - lits.push_back(si.internalize(arg)); + lits.push_back(si.internalize(arg, m_is_redundant)); s().set_external(lits.back().var()); } } diff --git a/src/sat/smt/ba_solver.cpp b/src/sat/smt/ba_solver.cpp index 077d59a0795..5631817256a 100644 --- a/src/sat/smt/ba_solver.cpp +++ b/src/sat/smt/ba_solver.cpp @@ -1748,7 +1748,7 @@ namespace sat { void ba_solver::add_at_least(bool_var v, literal_vector const& lits, unsigned k) { literal lit = v == null_bool_var ? null_literal : literal(v, false); - add_at_least(lit, lits, k, false); + add_at_least(lit, lits, k, m_is_redundant); } ba_solver::constraint* ba_solver::add_at_least(literal lit, literal_vector const& lits, unsigned k, bool learned) { @@ -1840,7 +1840,7 @@ namespace sat { void ba_solver::add_pb_ge(bool_var v, svector const& wlits, unsigned k) { literal lit = v == null_bool_var ? null_literal : literal(v, false); - add_pb_ge(lit, wlits, k, false); + add_pb_ge(lit, wlits, k, m_is_redundant); } /* diff --git a/src/sat/smt/ba_solver.h b/src/sat/smt/ba_solver.h index fbd63af5163..48cb9635695 100644 --- a/src/sat/smt/ba_solver.h +++ b/src/sat/smt/ba_solver.h @@ -554,6 +554,7 @@ namespace sat { void convert_to_wlits(app* t, sat::literal_vector const& lits, svector& wlits); void convert_pb_args(app* t, svector& wlits); void convert_pb_args(app* t, literal_vector& lits); + bool m_is_redundant{ false }; literal internalize_pb(expr* e, bool sign, bool root); literal internalize_xor(expr* e, bool sign, bool root); @@ -599,7 +600,7 @@ namespace sat { bool is_blocked(literal l, ext_constraint_idx idx) override; bool check_model(model const& m) const override; - literal internalize(expr* e, bool sign, bool root) override; + literal internalize(expr* e, bool sign, bool root, bool redundant) override; bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; th_solver* fresh(solver* s, ast_manager& m, sat_internalizer& si) override; diff --git a/src/sat/smt/euf_ackerman.cpp b/src/sat/smt/euf_ackerman.cpp index 5be275e58b1..66e58c1236d 100644 --- a/src/sat/smt/euf_ackerman.cpp +++ b/src/sat/smt/euf_ackerman.cpp @@ -189,11 +189,11 @@ namespace euf { unsigned sz = a->get_num_args(); for (unsigned i = 0; i < sz; ++i) { expr_ref eq(m.mk_eq(a->get_arg(i), b->get_arg(i)), m); - sat::literal lit = s.internalize(eq, true, false); + sat::literal lit = s.internalize(eq, true, false, true); lits.push_back(~lit); } expr_ref eq(m.mk_eq(a, b), m); - lits.push_back(s.internalize(eq, false, false)); + lits.push_back(s.internalize(eq, false, false, true)); s.s().mk_clause(lits, true); } @@ -202,9 +202,9 @@ namespace euf { expr_ref eq1(m.mk_eq(a, c), m); expr_ref eq2(m.mk_eq(b, c), m); expr_ref eq3(m.mk_eq(a, b), m); - lits[0] = s.internalize(eq1, true, false); - lits[1] = s.internalize(eq2, true, false); - lits[2] = s.internalize(eq3, false, false); + lits[0] = s.internalize(eq1, true, false, true); + lits[1] = s.internalize(eq2, true, false, true); + lits[2] = s.internalize(eq3, false, false, true); s.s().mk_clause(3, lits, true); } } diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp new file mode 100644 index 00000000000..f8b6f1cc394 --- /dev/null +++ b/src/sat/smt/euf_internalize.cpp @@ -0,0 +1,242 @@ +/*++ +Copyright (c) 2020 Microsoft Corporation + +Module Name: + + euf_internalize.cpp + +Abstract: + + Internalize utilities for EUF solver plugin. + +Author: + + Nikolaj Bjorner (nbjorner) 2020-08-25 + +--*/ + +#include "ast/ast_pp.h" +#include "ast/pb_decl_plugin.h" +#include "tactic/tactic_exception.h" +#include "sat/smt/euf_solver.h" + +namespace euf { + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + flet _is_learned(m_is_redundant, learned); + auto* ext = get_solver(e); + if (ext) + return ext->internalize(e, sign, root, learned); + IF_VERBOSE(110, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n"); + SASSERT(!si.is_bool_op(e)); + sat::scoped_stack _sc(m_stack); + unsigned sz = m_stack.size(); + euf::enode* n = visit(e); + while (m_stack.size() > sz) { + loop: + if (!m.inc()) + throw tactic_exception(m.limit().get_cancel_msg()); + sat::frame & fr = m_stack.back(); + expr* e = fr.m_e; + if (m_egraph.find(e)) { + m_stack.pop_back(); + continue; + } + unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; + + while (fr.m_idx < num) { + expr* arg = to_app(e)->get_arg(fr.m_idx); + fr.m_idx++; + n = visit(arg); + if (!n) + goto loop; + } + m_args.reset(); + for (unsigned i = 0; i < num; ++i) + m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); + if (root && internalize_root(to_app(e), m_args.c_ptr(), sign)) + return sat::null_literal; + n = m_egraph.mk(e, num, m_args.c_ptr()); + attach_node(n); + } + SASSERT(m_egraph.find(e)); + return literal(m_expr2var.to_bool_var(e), sign); + } + + euf::enode* solver::visit(expr* e) { + euf::enode* n = m_egraph.find(e); + if (n) + return n; + if (si.is_bool_op(e)) { + sat::literal lit = si.internalize(e, m_is_redundant); + n = m_var2node.get(lit.var(), nullptr); + if (n && !lit.sign()) + return n; + + n = m_egraph.mk(e, 0, nullptr); + attach_lit(lit, n); + if (!m.is_true(e) && !m.is_false(e)) + s().set_external(lit.var()); + return n; + } + if (is_app(e) && to_app(e)->get_num_args() > 0) { + m_stack.push_back(sat::frame(e)); + return nullptr; + } + n = m_egraph.mk(e, 0, nullptr); + attach_node(n); + return n; + } + + void solver::attach_node(euf::enode* n) { + expr* e = n->get_owner(); + if (m.is_bool(e)) { + sat::bool_var v = si.add_bool_var(e); + attach_lit(literal(v, false), n); + } + axiomatize_basic(n); + } + + void solver::attach_lit(literal lit, euf::enode* n) { + if (lit.sign()) { + sat::bool_var v = si.add_bool_var(n->get_owner()); + sat::literal lit2 = literal(v, false); + s().mk_clause(~lit, lit2, false); + s().mk_clause(lit, ~lit2, false); + lit = lit2; + } + sat::bool_var v = lit.var(); + m_var2node.reserve(v + 1, nullptr); + SASSERT(m_var2node[v] == nullptr); + m_var2node[v] = n; + m_var_trail.push_back(v); + } + + bool solver::internalize_root(app* e, enode* const* args, bool sign) { + if (m.is_distinct(e)) { + if (sign) + add_not_distinct_axiom(e, args); + else + add_distinct_axiom(e, args); + return true; + } + return false; + } + + void solver::add_not_distinct_axiom(app* e, enode* const* args) { + SASSERT(m.is_distinct(e)); + unsigned sz = e->get_num_args(); + if (sz <= 1) + return; + + static const unsigned distinct_max_args = 24; + if (sz <= distinct_max_args) { + sat::literal_vector lits; + for (unsigned i = 0; i < sz; ++i) { + for (unsigned j = i + 1; j < sz; ++j) { + expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m); + sat::literal lit = internalize(eq, false, false, m_is_redundant); + lits.push_back(lit); + } + } + s().mk_clause(lits, false); + } + else { + // g(f(x_i)) = x_i + // f(x_1) = a + .... + f(x_n) = a >= 2 + sort* srt = m.get_sort(e->get_arg(0)); + SASSERT(!m.is_bool(srt)); + sort_ref u(m.mk_fresh_sort("distinct-elems"), m); + sort* u_ptr = u.get(); + func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m); + func_decl_ref g(m.mk_fresh_func_decl("dist-g", "", 1, &u_ptr, srt), m); + expr_ref a(m.mk_fresh_const("a", u), m); + expr_ref_vector eqs(m); + for (expr* arg : *e) { + expr_ref fapp(m.mk_app(f, arg), m); + expr_ref gapp(m.mk_app(g, fapp.get()), m); + expr_ref eq(m.mk_eq(gapp, arg), m); + sat::literal lit = internalize(eq, false, false, m_is_redundant); + s().add_clause(1, &lit, false); + eqs.push_back(m.mk_eq(fapp, a)); + } + pb_util pb(m); + expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.c_ptr(), 2), m); + sat::literal lit = si.internalize(at_least2, m_is_redundant); + s().mk_clause(1, &lit, false); + } + } + + void solver::add_distinct_axiom(app* e, enode* const* args) { + SASSERT(m.is_distinct(e)); + static const unsigned distinct_max_args = 24; + unsigned sz = e->get_num_args(); + if (sz <= 1) { + s().mk_clause(0, nullptr, m_is_redundant); + return; + } + if (sz <= distinct_max_args) { + for (unsigned i = 0; i < sz; ++i) { + for (unsigned j = i + 1; j < sz; ++j) { + expr_ref eq(m.mk_eq(args[i]->get_owner(), args[j]->get_owner()), m); + sat::literal lit = internalize(eq, true, false, m_is_redundant); + s().add_clause(1, &lit, m_is_redundant); + } + } + } + else { + // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n + sort* srt = m.get_sort(e->get_arg(0)); + SASSERT(!m.is_bool(srt)); + sort_ref u(m.mk_fresh_sort("distinct-elems"), m); + func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m); + for (unsigned i = 0; i < sz; ++i) { + expr_ref fapp(m.mk_app(f, e->get_arg(i)), m); + expr_ref fresh(m.mk_fresh_const("dist-value", u), m); + enode* n = m_egraph.mk(fresh, 0, nullptr); + n->mark_interpreted(); + expr_ref eq(m.mk_eq(fapp, fresh), m); + sat::literal lit = internalize(eq, false, false, m_is_redundant); + s().add_clause(1, &lit, m_is_redundant); + } + } + } + + void solver::axiomatize_basic(enode* n) { + expr* e = n->get_owner(); + if (m.is_ite(e)) { + app* a = to_app(e); + expr* c = a->get_arg(0); + expr* th = a->get_arg(1); + expr* el = a->get_arg(2); + sat::bool_var v = m_expr2var.to_bool_var(c); + SASSERT(v != sat::null_bool_var); + expr_ref eq_th(m.mk_eq(a, th), m); + expr_ref eq_el(m.mk_eq(a, el), m); + sat::literal lit_th = internalize(eq_th, false, false, m_is_redundant); + sat::literal lit_el = internalize(eq_el, false, false, m_is_redundant); + literal lits1[2] = { literal(v, true), lit_th }; + literal lits2[2] = { literal(v, false), lit_el }; + s().add_clause(2, lits1, m_is_redundant); + s().add_clause(2, lits2, m_is_redundant); + } + else if (m.is_distinct(e)) { + expr_ref_vector eqs(m); + unsigned sz = n->num_args(); + for (unsigned i = 0; i < sz; ++i) { + for (unsigned j = i + 1; j < sz; ++j) { + expr_ref eq(m.mk_eq(n->get_arg(i)->get_owner(), n->get_arg(j)->get_owner()), m); + eqs.push_back(eq); + } + } + expr_ref fml(m.mk_or(eqs), m); + sat::literal dist(m_expr2var.to_bool_var(e), false); + sat::literal some_eq = si.internalize(fml, m_is_redundant); + sat::literal lits1[2] = { ~dist, ~some_eq }; + sat::literal lits2[2] = { dist, some_eq }; + s().add_clause(2, lits1, m_is_redundant); + s().add_clause(2, lits2, m_is_redundant); + } + } + +} diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index ecf7f36ca4c..115fe944bb0 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -31,8 +31,12 @@ namespace euf { } bool solver::include_func_interp(func_decl* f) { + if (f->is_skolem()) + return false; if (f->get_family_id() == null_family_id) return true; + if (f->get_family_id() == m.get_basic_family_id()) + return false; sat::th_model_builder* mb = get_solver(f); return mb && mb->include_func_interp(f); } @@ -97,7 +101,7 @@ namespace euf { if (!is_app(e)) continue; app* a = to_app(e); - func_decl* f = a->get_decl(); + func_decl* f = a->get_decl(); if (!include_func_interp(f)) continue; if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f)) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 264f087c473..2c6e1231fd2 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -16,7 +16,6 @@ Module Name: --*/ #include "ast/pb_decl_plugin.h" -#include "tactic/tactic_exception.h" #include "sat/sat_solver.h" #include "sat/smt/sat_smt.h" #include "sat/smt/ba_solver.h" @@ -32,10 +31,9 @@ namespace euf { * retrieve extension that is associated with Boolean variable. */ sat::th_solver* solver::get_solver(sat::bool_var v) { - unsigned idx = literal(v, false).index(); - if (idx >= m_lit2node.size()) + if (v >= m_var2node.size()) return nullptr; - euf::enode* n = m_lit2node[idx]; + euf::enode* n = m_var2node[v]; if (!n) return nullptr; return get_solver(n->get_owner()); @@ -111,19 +109,20 @@ namespace euf { m_egraph.explain(m_explain); break; case constraint::kind_t::eq: - n = m_lit2node[l.index()]; + n = m_var2node[l.var()]; SASSERT(n); SASSERT(m_egraph.is_equality(n)); + SASSERT(!l.sign()); m_egraph.explain_eq(m_explain, n->get_arg(0), n->get_arg(1), n->commutative()); break; case constraint::kind_t::lit: - n = m_lit2node[l.index()]; + n = m_var2node[l.var()]; SASSERT(n); SASSERT(m.is_bool(n->get_owner())); m_egraph.explain_eq(m_explain, n, (l.sign() ? mk_false() : mk_true()), false); break; default: - std::cout << (unsigned)j.kind() << "\n"; + IF_VERBOSE(0, verbose_stream() << (unsigned)j.kind() << "\n"); UNREACHABLE(); } for (unsigned* idx : m_explain) @@ -133,27 +132,25 @@ namespace euf { void solver::asserted(literal l) { auto* ext = get_solver(l.var()); if (ext) { - force_push(); ext->asserted(l); return; } bool sign = l.sign(); - unsigned idx = sat::literal(l.var(), false).index(); - auto n = m_lit2node.get(idx, nullptr); + auto n = m_var2node.get(l.var(), nullptr); if (!n) return; - force_push(); expr* e = n->get_owner(); if (m.is_eq(e) && !sign) { euf::enode* na = n->get_arg(0); euf::enode* nb = n->get_arg(1); + TRACE("euf", tout << "merge " << na->get_owner_id() << nb->get_owner_id() << "\n";); m_egraph.merge(na, nb, base_ptr() + l.index()); } else { euf::enode* nb = sign ? mk_false() : mk_true(); - std::cout << "merge " << n->get_owner_id() << " " << sign << " " << nb->get_owner_id() << "\n"; + TRACE("euf", tout << "merge " << n->get_owner_id() << " " << mk_pp(nb->get_owner(), m) << "\n";); m_egraph.merge(n, nb, base_ptr() + l.index()); } // TBD: delay propagation? @@ -222,7 +219,7 @@ namespace euf { void solver::push() { scope s; - s.m_lit_lim = m_lit_trail.size(); + s.m_var_lim = m_var_trail.size(); s.m_trail_lim = m_trail.size(); m_scopes.push_back(s); m_region.push_scope(); @@ -244,9 +241,9 @@ namespace euf { scope const & s = m_scopes[m_scopes.size() - n]; - for (unsigned i = m_lit_trail.size(); i-- > s.m_lit_lim; ) - m_lit2node[m_lit_trail[i]] = nullptr; - m_lit_trail.shrink(s.m_lit_lim); + for (unsigned i = m_var_trail.size(); i-- > s.m_var_lim; ) + m_var2node[m_var_trail[i]] = nullptr; + m_var_trail.shrink(s.m_var_lim); undo_trail_stack(*this, m_trail, s.m_trail_lim); @@ -280,9 +277,11 @@ namespace euf { std::ostream& solver::display(std::ostream& out) const { m_egraph.display(out); - for (unsigned idx : m_lit_trail) { - euf::enode* n = m_lit2node[idx]; - out << sat::to_literal(idx) << ": " << m_egraph.pp(n); + + out << "bool-vars\n"; + for (unsigned v : m_var_trail) { + euf::enode* n = m_var2node[v]; + out << v << ": " << m_egraph.pp(n); } for (auto* e : m_solvers) e->display(out); @@ -369,8 +368,8 @@ namespace euf { unsigned solver::max_var(unsigned w) const { for (auto* e : m_solvers) w = e->max_var(w); - for (unsigned sz = m_lit2node.size(); sz-- > 0; ) { - euf::enode* n = m_lit2node[sz]; + for (unsigned sz = m_var2node.size(); sz-- > 0; ) { + euf::enode* n = m_var2node[sz]; if (n && m.is_bool(n->get_owner())) { w = std::max(w, sz); break; @@ -413,86 +412,6 @@ namespace euf { m_egraph.set_used_cc(used_cc); } - sat::literal solver::internalize(expr* e, bool sign, bool root) { - force_push(); - auto* ext = get_solver(e); - if (ext) - return ext->internalize(e, sign, root); - IF_VERBOSE(0, verbose_stream() << "internalize: " << mk_pp(e, m) << "\n"); - SASSERT(!si.is_bool_op(e)); - sat::scoped_stack _sc(m_stack); - unsigned sz = m_stack.size(); - euf::enode* n = visit(e); - while (m_stack.size() > sz) { - loop: - if (!m.inc()) - throw tactic_exception(m.limit().get_cancel_msg()); - sat::frame & fr = m_stack.back(); - expr* e = fr.m_e; - if (m_egraph.find(e)) { - m_stack.pop_back(); - continue; - } - unsigned num = is_app(e) ? to_app(e)->get_num_args() : 0; - - while (fr.m_idx < num) { - expr* arg = to_app(e)->get_arg(fr.m_idx); - fr.m_idx++; - n = visit(arg); - if (!n) - goto loop; - } - m_args.reset(); - for (unsigned i = 0; i < num; ++i) - m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); - n = m_egraph.mk(e, num, m_args.c_ptr()); - attach_bool_var(n); - } - SASSERT(m_egraph.find(e)); - return literal(m_expr2var.to_bool_var(e), sign); - } - - euf::enode* solver::visit(expr* e) { - euf::enode* n = m_egraph.find(e); - if (n) - return n; - if (si.is_bool_op(e)) { - sat::literal lit = si.internalize(e); - n = m_lit2node.get(lit.index(), nullptr); - if (n) - return n; - - n = m_egraph.mk(e, 0, nullptr); - attach_lit(lit, n); - if (!m.is_true(e) && !m.is_false(e)) - s().set_external(lit.var()); - return n; - } - if (is_app(e) && to_app(e)->get_num_args() > 0) { - m_stack.push_back(sat::frame(e)); - return nullptr; - } - n = m_egraph.mk(e, 0, nullptr); - attach_bool_var(n); - return n; - } - - void solver::attach_bool_var(euf::enode* n) { - expr* e = n->get_owner(); - if (m.is_bool(e)) { - sat::bool_var v = si.add_bool_var(e); - attach_lit(literal(v, false), n); - } - } - - void solver::attach_lit(literal lit, euf::enode* n) { - unsigned v = lit.index(); - m_lit2node.reserve(v + 1, nullptr); - SASSERT(m_lit2node[v] == nullptr); - m_lit2node[v] = n; - m_lit_trail.push_back(v); - } - bool solver::to_formulas(std::function& l2e, expr_ref_vector& fmls) { for (auto* th : m_solvers) { if (!th->to_formulas(l2e, fmls)) diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 8bc69644b07..0d22161adca 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -57,7 +57,7 @@ namespace euf { void reset() { memset(this, 0, sizeof(*this)); } }; struct scope { - unsigned m_lit_lim; + unsigned m_var_lim; unsigned m_trail_lim; }; typedef ptr_vector > trail_stack; @@ -79,12 +79,12 @@ namespace euf { sat::sat_internalizer* m_to_si; scoped_ptr m_ackerman; - ptr_vector m_lit2node; + ptr_vector m_var2node; ptr_vector m_explain; euf::enode_vector m_args; svector m_stack; unsigned m_num_scopes { 0 }; - unsigned_vector m_lit_trail; + unsigned_vector m_var_trail; svector m_scopes; scoped_ptr_vector m_solvers; ptr_vector m_id2solver; @@ -97,9 +97,14 @@ namespace euf { unsigned * base_ptr() { return reinterpret_cast(this); } // internalization + bool m_is_redundant { false }; euf::enode* visit(expr* e); - void attach_bool_var(euf::enode* n); + void attach_node(euf::enode* n); void attach_lit(sat::literal lit, euf::enode* n); + void add_distinct_axiom(app* e, euf::enode* const* args); + void add_not_distinct_axiom(app* e, euf::enode* const* args); + void axiomatize_basic(enode* n); + bool internalize_root(app* e, enode* const* args, bool sign); euf::enode* mk_true(); euf::enode* mk_false(); @@ -199,7 +204,7 @@ namespace euf { std::function& pb) override; bool to_formulas(std::function& l2e, expr_ref_vector& fmls) override; - sat::literal internalize(expr* e, bool sign, bool root) override; + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void update_model(model_ref& mdl); func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; } diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h index 2762d96644a..4898303447b 100644 --- a/src/sat/smt/sat_smt.h +++ b/src/sat/smt/sat_smt.h @@ -38,7 +38,7 @@ namespace sat { public: virtual ~sat_internalizer() {} virtual bool is_bool_op(expr* e) const = 0; - virtual literal internalize(expr* e) = 0; + virtual literal internalize(expr* e, bool learned) = 0; virtual bool_var add_bool_var(expr* e) = 0; virtual void cache(app* t, literal l) = 0; }; diff --git a/src/sat/smt/sat_th.h b/src/sat/smt/sat_th.h index 44bd6b1bbb4..50fb246dc38 100644 --- a/src/sat/smt/sat_th.h +++ b/src/sat/smt/sat_th.h @@ -26,7 +26,7 @@ namespace sat { public: virtual ~th_internalizer() {} - virtual literal internalize(expr* e, bool sign, bool root) = 0; + virtual literal internalize(expr* e, bool sign, bool root, bool redundant) = 0; }; class th_decompile { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 4bde51d6a4c..a7de8badda2 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -70,6 +70,7 @@ struct goal2sat::imp : public sat::sat_internalizer { bool m_default_external; bool m_xor_solver; bool m_euf; + bool m_is_redundant { false }; sat::literal_vector aig_lits; imp(ast_manager & _m, params_ref const & p, sat::solver_core & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): @@ -93,7 +94,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_ite_extra = p.get_bool("ite_extra", true); m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_xor_solver = p.get_bool("xor_solver", false); - m_euf = false; // true; + m_euf = true; // false; // true; } void throw_op_not_handled(std::string const& s) { @@ -103,22 +104,22 @@ struct goal2sat::imp : public sat::sat_internalizer { void mk_clause(sat::literal l) { TRACE("goal2sat", tout << "mk_clause: " << l << "\n";); - m_solver.add_clause(1, &l, false); + m_solver.add_clause(1, &l, m_is_redundant); } void mk_clause(sat::literal l1, sat::literal l2) { TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << "\n";); - m_solver.add_clause(l1, l2, false); + m_solver.add_clause(l1, l2, m_is_redundant); } void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) { TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";); - m_solver.add_clause(l1, l2, l3, false); + m_solver.add_clause(l1, l2, l3, m_is_redundant); } void mk_clause(unsigned num, sat::literal * lits) { TRACE("goal2sat", tout << "mk_clause: "; for (unsigned i = 0; i < num; i++) tout << lits[i] << " "; tout << "\n";); - m_solver.add_clause(num, lits, false); + m_solver.add_clause(num, lits, m_is_redundant); } sat::literal mk_true() { @@ -246,6 +247,10 @@ struct goal2sat::imp : public sat::sat_internalizer { return true; } case OP_DISTINCT: { + if (m_euf) { + convert_euf(t, root, sign); + return true; + } TRACE("goal2sat_not_handled", tout << mk_ismt2_pp(t, m) << "\n";); std::ostringstream strm; strm << mk_ismt2_pp(t, m); @@ -481,7 +486,6 @@ struct goal2sat::imp : public sat::sat_internalizer { euf::solver* euf = nullptr; if (!ext) { euf = alloc(euf::solver, m, m_map, *this); - std::cout << "set euf\n"; m_solver.set_extension(euf); for (unsigned i = m_solver.num_scopes(); i-- > 0; ) euf->push(); @@ -491,7 +495,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } if (!euf) throw default_exception("cannot convert to euf"); - sat::literal lit = euf->internalize(e, sign, root); + sat::literal lit = euf->internalize(e, sign, root, m_is_redundant); if (root) m_result_stack.reset(); if (lit == sat::null_literal) @@ -516,7 +520,7 @@ struct goal2sat::imp : public sat::sat_internalizer { } if (!ba) throw default_exception("cannot convert to pb"); - sat::literal lit = ba->internalize(t, sign, root); + sat::literal lit = ba->internalize(t, sign, root, m_is_redundant); if (root) m_result_stack.reset(); else @@ -588,7 +592,8 @@ struct goal2sat::imp : public sat::sat_internalizer { } }; - void process(expr* n, bool is_root) { + void process(expr* n, bool is_root, bool redundant) { + flet _is_redundant(m_is_redundant, redundant); scoped_stack _sc(*this, is_root); unsigned sz = m_frame_stack.size(); if (visit(n, is_root, false)) @@ -636,9 +641,9 @@ struct goal2sat::imp : public sat::sat_internalizer { } } - sat::literal internalize(expr* n) override { + sat::literal internalize(expr* n, bool redundant) override { unsigned sz = m_result_stack.size(); - process(n, false); + process(n, false, redundant); SASSERT(m_result_stack.size() == sz + 1); sat::literal result = m_result_stack.back(); m_result_stack.pop_back(); @@ -674,7 +679,7 @@ struct goal2sat::imp : public sat::sat_internalizer { void process(expr * n) { m_result_stack.reset(); TRACE("goal2sat", tout << mk_pp(n, m) << "\n";); - process(n, true); + process(n, true, m_is_redundant); CTRACE("goal2sat", !m_result_stack.empty(), tout << m_result_stack << "\n";); SASSERT(m_result_stack.empty()); } @@ -782,7 +787,7 @@ struct unsupported_bool_proc { :blast-distinct true */ bool goal2sat::has_unsupported_bool(goal const & g) { - return test(g); + return false && test(g); } goal2sat::goal2sat():