mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
This commit is contained in:
parent
123c446395
commit
e3be25dad6
|
@ -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) {
|
||||
|
|
|
@ -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();
|
||||
|
|
|
@ -134,8 +134,9 @@ namespace euf {
|
|||
typedef std::tuple<expr_ref, unsigned, sat::bool_var> reinit_t;
|
||||
vector<reinit_t> 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;
|
||||
|
|
|
@ -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());
|
||||
}
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue