mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

#5482 other relevancy tracking

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-25 05:59:27 -07:00
parent e75b5e9513
commit 17663acf75
1 changed files with 14 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -423,9 +423,9 @@ namespace bv {
for (expr* b : k_bits) for (expr* b : k_bits)
args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero)); args.push_back(m.mk_ite(b, m_autil.mk_int(power2(i++)), zero));
expr_ref sum(m_autil.mk_add(sz, args.data()), m); expr_ref sum(m_autil.mk_add(sz, args.data()), m);
expr_ref eq = mk_eq(n, sum); sat::literal lit = eq_internalize(n, sum);
sat::literal lit = ctx.internalize(eq, false, false, m_is_redundant); add_unit(lit);
add_unit(lit); ctx.add_root(lit);
} }
void solver::internalize_int2bv(app* n) { void solver::internalize_int2bv(app* n) {
@ -453,9 +453,9 @@ namespace bv {
unsigned sz = bv.get_bv_size(n); unsigned sz = bv.get_bv_size(n);
numeral mod = power(numeral(2), sz); numeral mod = power(numeral(2), sz);
rhs = m_autil.mk_mod(e, m_autil.mk_int(mod)); rhs = m_autil.mk_mod(e, m_autil.mk_int(mod));
expr_ref eq = mk_eq(lhs, rhs); sat::literal eq_lit = eq_internalize(lhs, rhs);
TRACE("bv", tout << eq << "\n";); add_unit(eq_lit);
add_unit(ctx.internalize(eq, false, false, m_is_redundant)); 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);
@ -466,9 +466,9 @@ namespace bv {
rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2)); rhs = m_autil.mk_mod(rhs, m_autil.mk_int(2));
rhs = mk_eq(rhs, m_autil.mk_int(1)); rhs = mk_eq(rhs, m_autil.mk_int(1));
lhs = n_bits.get(i); lhs = n_bits.get(i);
expr_ref eq = mk_eq(lhs, rhs); eq_lit = eq_internalize(lhs, rhs);
TRACE("bv", tout << eq << "\n";); add_unit(eq_lit);
add_unit(ctx.internalize(eq, false, false, m_is_redundant)); ctx.add_root(eq_lit);
} }
} }
@ -650,7 +650,9 @@ namespace bv {
conc.push_back(arg); conc.push_back(arg);
expr_ref r(bv.mk_concat(conc), m); expr_ref r(bv.mk_concat(conc), m);
mk_bits(get_th_var(e)); mk_bits(get_th_var(e));
add_unit(eq_internalize(e, r)); sat::literal eq_lit = eq_internalize(e, r);
add_unit(eq_lit);
ctx.add_root(eq_lit);
} }
void solver::internalize_bit2bool(app* n) { void solver::internalize_bit2bool(app* n) {
@ -760,9 +762,8 @@ namespace bv {
expr_ref e1(m), e2(m); expr_ref e1(m), e2(m);
e1 = bv.mk_bit2bool(o1, i); e1 = bv.mk_bit2bool(o1, i);
e2 = bv.mk_bit2bool(o2, i); e2 = bv.mk_bit2bool(o2, i);
expr_ref e = mk_eq(e1, e2); literal eq = eq_internalize(e1, e2);
literal eq = ctx.internalize(e, false, false, m_is_redundant); add_clause(eq, ~oeq);
add_clause(eq, ~oeq);
eqs.push_back(~eq); eqs.push_back(~eq);
} }
TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";); TRACE("bv", for (auto l : eqs) tout << mk_bounded_pp(literal2expr(l), m) << " "; tout << "\n";);