mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-04 13:48:51 -07:00
parent 7cda90c06a
commit ae6aea7a4d
3 changed files with 14 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/euf_internalize.cpp
View file

@ -193,8 +193,8 @@ namespace euf {
}
s().mk_clause(lits, st);
if (relevancy_enabled())
add_root(lits.size(), lits.data());
}
add_root(lits);
}
else {
// g(f(x_i)) = x_i
// f(x_1) = a + .... + f(x_n) = a >= 2

5
src/sat/smt/euf_solver.h
View file

@ -357,8 +357,11 @@ namespace euf {
// relevancy
bool relevancy_enabled() const { return get_config().m_relevancy_lvl > 0; }
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); }
void add_root(sat::literal a, sat::literal b) { sat::literal lits[2] = {a, b}; add_root(2, lits); }
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 lits[2] = {a, b}; add_aux(2, lits); }
void track_relevancy(sat::bool_var v);
bool is_relevant(expr* e) const;
bool is_relevant(enode* n) const;

10
src/sat/smt/q_solver.cpp
View file

@ -42,8 +42,12 @@ namespace q {
auto const& exp = expand(q);
if (exp.size() > 1 && is_forall(q)) {
for (expr* e : exp)
add_clause(~l, ctx.internalize(e, l.sign(), false, false));
for (expr* e : exp) {
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
add_clause(~l, lit);
if (ctx.relevancy_enabled())
ctx.add_root(~l, lit);
}
return;
}
if (exp.size() > 1 && is_exists(q)) {
@ -52,6 +56,8 @@ namespace q {
for (expr* e : exp)
lits.push_back(ctx.internalize(e, l.sign(), false, false));
add_clause(lits);
if (ctx.relevancy_enabled())
ctx.add_root(lits);
return;
}