From e3be25dad611df6772b15bcb91039f9b2908f741 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 1 Aug 2021 16:48:25 -0700 Subject: [PATCH] #5445 --- src/sat/smt/euf_internalize.cpp | 5 +- src/sat/smt/euf_solver.cpp | 114 ++++++++++++++++++++++++++++++-- src/sat/smt/euf_solver.h | 8 ++- src/sat/smt/sat_dual_solver.cpp | 4 +- src/sat/tactic/goal2sat.cpp | 2 +- 5 files changed, 120 insertions(+), 13 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index f44967885..020d29baa 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -35,7 +35,10 @@ namespace euf { sat::literal solver::mk_literal(expr* e) { expr_ref _e(e, m); bool is_not = m.is_not(e, e); - return internalize(e, is_not, false, m_is_redundant); + sat::literal lit = internalize(e, false, false, m_is_redundant); + if (is_not) + lit.neg(); + return lit; } sat::literal solver::internalize(expr* e, bool sign, bool root, bool redundant) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 739cbf9b7..d2ae0a0dd 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -561,14 +561,11 @@ namespace euf { scoped_set_replay replay(*this); scoped_suspend_rlimit suspend_rlimit(m.limit()); - for (auto const& t : m_reinit) - replay.m.insert(std::get<0>(t), std::get<2>(t)); - + for (auto const& [e, generation, v] : m_reinit) + replay.m.insert(e, v); + TRACE("euf", for (auto const& kv : replay.m) tout << kv.m_value << "\n";); - for (auto const& t : m_reinit) { - expr_ref e = std::get<0>(t); - unsigned generation = std::get<1>(t); - sat::bool_var v = std::get<2>(t); + for (auto const& [e, generation, v] : m_reinit) { scoped_generation _sg(*this, generation); TRACE("euf", tout << "replay: " << v << " " << mk_bounded_pp(e, m) << "\n";); sat::literal lit; @@ -579,9 +576,112 @@ namespace euf { VERIFY(lit.var() == v); attach_lit(lit, e); } + + if (relevancy_enabled()) + for (auto const& [e, generation, v] : m_reinit) + if (si.is_bool_op(e)) + relevancy_reinit(e); TRACE("euf", display(tout << "replay done\n");); } + /** + * Boolean structure needs to be replayed for relevancy tracking. + * Main cases for replaying Boolean functions are included. When a replay + * is not supported, we just disable relevancy. + */ + void solver::relevancy_reinit(expr* e) { + TRACE("euf", tout << "internalize again " << mk_pp(e, m) << "\n";); + if (to_app(e)->get_family_id() != m.get_basic_family_id()) { + disable_relevancy(e); + return; + } + auto lit = si.internalize(e, true); + switch (to_app(e)->get_decl_kind()) { + case OP_NOT: { + auto lit2 = si.internalize(to_app(e)->get_arg(0), true); + add_aux(lit, lit2); + add_aux(~lit, ~lit2); + break; + } + case OP_EQ: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + return; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(~lit, ~lit1, lit2); + add_aux(~lit, lit1, ~lit2); + add_aux(lit, lit1, lit2); + add_aux(lit, ~lit1, ~lit2); + break; + } + case OP_OR: { + sat::literal_vector lits; + for (expr* arg : *to_app(e)) + lits.push_back(si.internalize(arg, true)); + for (auto lit2 : lits) + add_aux(~lit2, lit); + lits.push_back(~lit); + add_aux(lits); + break; + } + case OP_AND: { + sat::literal_vector lits; + for (expr* arg : *to_app(e)) + lits.push_back(~si.internalize(arg, true)); + for (auto nlit2 : lits) + add_aux(~lit, ~nlit2); + lits.push_back(lit); + add_aux(lits); + break; + } + case OP_TRUE: + add_root(lit); + break; + case OP_FALSE: + add_root(~lit); + break; + case OP_ITE: { + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + auto lit3 = si.internalize(to_app(e)->get_arg(2), true); + add_aux(~lit, ~lit1, lit2); + add_aux(~lit, lit1, lit3); + add_aux(lit, ~lit1, ~lit2); + add_aux(lit, lit1, ~lit3); + break; + } + case OP_XOR: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + break; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(lit, ~lit1, lit2); + add_aux(lit, lit1, ~lit2); + add_aux(~lit, lit1, lit2); + add_aux(~lit, ~lit1, ~lit2); + break; + } + case OP_IMPLIES: { + if (to_app(e)->get_num_args() != 2) { + disable_relevancy(e); + break; + } + auto lit1 = si.internalize(to_app(e)->get_arg(0), true); + auto lit2 = si.internalize(to_app(e)->get_arg(1), true); + add_aux(~lit, ~lit1, lit2); + add_aux(lit, lit1); + add_aux(lit, ~lit2); + break; + } + default: + UNREACHABLE(); + } + } + void solver::pre_simplify() { for (auto* e : m_solvers) e->pre_simplify(); diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index cf8b9766e..5f3b62781 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -134,8 +134,9 @@ namespace euf { typedef std::tuple reinit_t; vector m_reinit; - void start_reinit(unsigned num_scopes); + void start_reinit(unsigned num_scopes); void finish_reinit(); + void relevancy_reinit(expr* e); // extensions th_solver* get_solver(family_id fid, func_decl* f); @@ -356,7 +357,9 @@ namespace euf { bool is_shared(euf::enode* n) const; // relevancy - bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; } + bool m_relevancy = true; + bool relevancy_enabled() const { return m_relevancy && get_config().m_relevancy_lvl > 0; } + void disable_relevancy(expr* e) { IF_VERBOSE(0, verbose_stream() << "disabling relevancy " << mk_pp(e, m) << "\n"); m_relevancy = false; } void add_root(unsigned n, sat::literal const* lits); void add_root(sat::literal_vector const& lits) { add_root(lits.size(), lits.data()); } void add_root(sat::literal lit) { add_root(1, &lit); } @@ -364,6 +367,7 @@ namespace euf { void add_aux(sat::literal_vector const& lits) { add_aux(lits.size(), lits.data()); } void add_aux(unsigned n, sat::literal const* lits); void add_aux(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_aux(2, lits); } + void add_aux(sat::literal a, sat::literal b, sat::literal c) { sat::literal lits[3] = { a, b, c }; add_aux(3, lits); } void track_relevancy(sat::bool_var v); bool is_relevant(expr* e) const; bool is_relevant(enode* n) const; diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp index e16b09ed1..00d01b1b7 100644 --- a/src/sat/smt/sat_dual_solver.cpp +++ b/src/sat/smt/sat_dual_solver.cpp @@ -106,11 +106,11 @@ namespace sat { } void dual_solver::add_aux(unsigned sz, literal const* clause) { - flush(); - TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";); + flush(); m_lits.reset(); for (unsigned i = 0; i < sz; ++i) m_lits.push_back(ext2lit(clause[i])); + TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << " -> " << m_lits << "\n";); m_solver.mk_clause(sz, m_lits.data(), status::input()); } diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index a5c60d3db..4d0cc7880 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -796,7 +796,7 @@ struct goal2sat::imp : public sat::sat_internalizer { m_frame_stack.pop_back(); continue; } - if (m.is_not(t) && !m.is_not(t->get_arg(0))) { + if (m.is_not(t) && !m.is_not(t->get_arg(0)) && fsz != sz + 1) { m_frame_stack.pop_back(); visit(t->get_arg(0), root, !sign); continue;