mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

make roots uniform for theory lemmas

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-29 13:42:11 -08:00
parent 69b4392210
commit a90b66134d
7 changed files with 20 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/array_internalize.cpp
View file

@ -124,7 +124,7 @@ namespace array {
mk_var(n); mk_var(n);
for (auto* arg : euf::enode_args(n)) for (auto* arg : euf::enode_args(n))
ensure_var(arg); ensure_var(arg);
if (ctx.is_relevant(n)) if (ctx.is_relevant(n) || !ctx.relevancy().enabled())
relevant_eh(n); relevant_eh(n);
return true; return true;
} }

5
src/sat/smt/bv_internalize.cpp
View file

@ -427,7 +427,6 @@ namespace bv {
expr_ref sum(m_autil.mk_add(sz, args.data()), m); expr_ref sum(m_autil.mk_add(sz, args.data()), m);
sat::literal lit = eq_internalize(n, sum); sat::literal lit = eq_internalize(n, sum);
add_unit(lit); add_unit(lit);
ctx.add_root(lit);
} }
void solver::internalize_int2bv(app* n) { void solver::internalize_int2bv(app* n) {
@ -457,7 +456,6 @@ namespace bv {
rhs = m_autil.mk_mod(e, m_autil.mk_int(mod)); rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
sat::literal eq_lit = eq_internalize(lhs, rhs); sat::literal eq_lit = eq_internalize(lhs, rhs);
add_unit(eq_lit); add_unit(eq_lit);
ctx.add_root(eq_lit);
expr_ref_vector n_bits(m); expr_ref_vector n_bits(m);
get_bits(n_enode, n_bits); get_bits(n_enode, n_bits);
@ -470,7 +468,6 @@ namespace bv {
lhs = n_bits.get(i); lhs = n_bits.get(i);
eq_lit = eq_internalize(lhs, rhs); eq_lit = eq_internalize(lhs, rhs);
add_unit(eq_lit); add_unit(eq_lit);
ctx.add_root(eq_lit);
} }
} }
@ -536,7 +533,6 @@ namespace bv {
if (p.hi_div0()) { if (p.hi_div0()) {
eq_lit = eq_internalize(n, ibin(arg1, arg2)); eq_lit = eq_internalize(n, ibin(arg1, arg2));
add_unit(eq_lit); add_unit(eq_lit);
ctx.add_root(eq_lit);
} }
else { else {
unsigned sz = bv.get_bv_size(n); unsigned sz = bv.get_bv_size(n);
@ -654,7 +650,6 @@ namespace bv {
mk_bits(get_th_var(e)); mk_bits(get_th_var(e));
sat::literal eq_lit = eq_internalize(e, r); sat::literal eq_lit = eq_internalize(e, r);
add_unit(eq_lit); add_unit(eq_lit);
ctx.add_root(eq_lit);
} }
void solver::internalize_bit2bool(app* n) { void solver::internalize_bit2bool(app* n) {

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

@ -162,10 +162,8 @@ namespace euf {
sat::literal lit2 = literal(v, false); sat::literal lit2 = literal(v, false);
s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(~lit, lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id())); s().mk_clause(lit, ~lit2, sat::status::th(m_is_redundant, m.get_basic_family_id()));
if (relevancy_enabled()) { add_aux(~lit, lit2);
add_aux(~lit, lit2); add_aux(lit, ~lit2);
add_aux(lit, ~lit2);
}
lit = lit2; lit = lit2;
} }
@ -225,8 +223,7 @@ namespace euf {
} }
} }
s().mk_clause(lits, st); s().mk_clause(lits, st);
if (relevancy_enabled()) add_root(lits);
add_root(lits);
} }
else { else {
// g(f(x_i)) = x_i // g(f(x_i)) = x_i
@ -251,8 +248,7 @@ namespace euf {
expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m); expr_ref at_least2(pb.mk_at_least_k(eqs.size(), eqs.data(), 2), m);
sat::literal lit = si.internalize(at_least2, m_is_redundant); sat::literal lit = si.internalize(at_least2, m_is_redundant);
s().mk_clause(1, &lit, st); s().mk_clause(1, &lit, st);
if (relevancy_enabled()) add_root(1, &lit);
add_root(1, &lit);
} }
} }
@ -269,8 +265,7 @@ namespace euf {
expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
sat::literal lit = ~mk_literal(eq); sat::literal lit = ~mk_literal(eq);
s().add_clause(1, &lit, st); s().add_clause(1, &lit, st);
if (relevancy_enabled()) add_root(1, &lit);
add_root(1, &lit);
} }
} }
} }
@ -288,8 +283,7 @@ namespace euf {
expr_ref eq = mk_eq(fapp, fresh); expr_ref eq = mk_eq(fapp, fresh);
sat::literal lit = mk_literal(eq); sat::literal lit = mk_literal(eq);
s().add_clause(1, &lit, st); s().add_clause(1, &lit, st);
if (relevancy_enabled()) add_root(1, &lit);
add_root(1, &lit);
} }
} }
} }

1
src/sat/smt/q_mbi.cpp
View file

@ -71,7 +71,6 @@ namespace q {
euf::solver::scoped_generation sg(ctx, generation + 1); euf::solver::scoped_generation sg(ctx, generation + 1);
sat::literal lit = ctx.mk_literal(fml); sat::literal lit = ctx.mk_literal(fml);
m_qs.add_clause(~qlit, ~lit); m_qs.add_clause(~qlit, ~lit);
ctx.add_root(~qlit, ~lit);
} }
m_instantiations.reset(); m_instantiations.reset();
return result; return result;

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

@ -44,19 +44,16 @@ namespace q {
if (l.sign() == is_forall(e)) { if (l.sign() == is_forall(e)) {
sat::literal lit = skolemize(q); sat::literal lit = skolemize(q);
add_clause(~l, lit); add_clause(~l, lit);
ctx.add_root(~l, lit);
} }
else if (expand(q)) { else if (expand(q)) {
for (expr* e : m_expanded) { for (expr* e : m_expanded) {
sat::literal lit = ctx.internalize(e, l.sign(), false, false); sat::literal lit = ctx.internalize(e, l.sign(), false, false);
add_clause(~l, lit); add_clause(~l, lit);
ctx.add_root(~l, lit);
} }
} }
else if (is_ground(q->get_expr())) { else if (is_ground(q->get_expr())) {
auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false); auto lit = ctx.internalize(q->get_expr(), l.sign(), false, false);
add_clause(~l, lit); add_clause(~l, lit);
ctx.add_root(~l, lit);
} }
else { else {
ctx.push_vec(m_universal, l); ctx.push_vec(m_universal, l);

26
src/sat/smt/sat_th.cpp
View file

@ -132,6 +132,7 @@ namespace euf {
bool th_euf_solver::add_unit(sat::literal lit) { bool th_euf_solver::add_unit(sat::literal lit) {
bool was_true = is_true(lit); bool was_true = is_true(lit);
ctx.s().add_clause(1, &lit, mk_status()); ctx.s().add_clause(1, &lit, mk_status());
ctx.add_root(lit);
return !was_true; return !was_true;
} }
@ -143,32 +144,27 @@ namespace euf {
return is_new; return is_new;
} }
bool th_euf_solver::add_clause(sat::literal a, sat::literal b) { bool th_euf_solver::add_clause(sat::literal a, sat::literal b) {
bool was_true = is_true(a, b);
sat::literal lits[2] = { a, b }; sat::literal lits[2] = { a, b };
ctx.s().add_clause(2, lits, mk_status()); return add_clause(2, lits);
return !was_true;
} }
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) { bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c) {
bool was_true = is_true(a, b, c);
sat::literal lits[3] = { a, b, c }; sat::literal lits[3] = { a, b, c };
ctx.s().add_clause(3, lits, mk_status()); return add_clause(3, lits);
return !was_true;
} }
bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) { bool th_euf_solver::add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d) {
bool was_true = is_true(a, b, c, d);
sat::literal lits[4] = { a, b, c, d }; sat::literal lits[4] = { a, b, c, d };
ctx.s().add_clause(4, lits, mk_status()); return add_clause(4, lits);
return !was_true;
} }
bool th_euf_solver::add_clause(sat::literal_vector const& lits) { bool th_euf_solver::add_clause(unsigned n, sat::literal* lits) {
bool was_true = false; bool was_true = false;
for (auto lit : lits) for (unsigned i = 0; i < n; ++i)
was_true |= is_true(lit); was_true |= is_true(lits[i]);
s().add_clause(lits.size(), lits.data(), mk_status()); ctx.add_root(n, lits);
s().add_clause(n, lits, mk_status());
return !was_true; return !was_true;
} }

3
src/sat/smt/sat_th.h
View file

@ -141,7 +141,8 @@ namespace euf {
bool add_clause(sat::literal a, sat::literal b); bool add_clause(sat::literal a, sat::literal b);
bool add_clause(sat::literal a, sat::literal b, sat::literal c); bool add_clause(sat::literal a, sat::literal b, sat::literal c);
bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d); bool add_clause(sat::literal a, sat::literal b, sat::literal c, sat::literal d);
bool add_clause(sat::literal_vector const& lits); bool add_clause(sat::literal_vector const& lits) { return add_clause(lits.size(), lits.data()); }
bool add_clause(unsigned n, sat::literal* lits);
void add_equiv(sat::literal a, sat::literal b); void add_equiv(sat::literal a, sat::literal b);
void add_equiv_and(sat::literal a, sat::literal_vector const& bs); void add_equiv_and(sat::literal a, sat::literal_vector const& bs);