mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
regression fix to ackerman gc and memory smash, perf fix for handling bv2int axioms, perf fix for filtering ackerman
this update addresses some perf regressions introduced when handling axioms for bv2int and a memory smash regression when decoupling bv-ackerman from in-processing. It adds a filter based on bv_eq_axioms for disabling ackerman reductions on disequalities.
This commit is contained in:
parent
ca0a82952f
commit
159026b5e8
|
@ -49,16 +49,19 @@ namespace bv {
|
|||
update_glue(*other);
|
||||
|
||||
vv::push_to_front(m_queue, other);
|
||||
if (other == n) {
|
||||
bool do_gc = other == n;
|
||||
if (other == n)
|
||||
new_tmp();
|
||||
gc();
|
||||
}
|
||||
|
||||
if (other->m_glue == 0) {
|
||||
do_gc = false;
|
||||
remove(other);
|
||||
add_cc(v1, v2);
|
||||
}
|
||||
else if (other->m_count > 2*m_propagate_high_watermark)
|
||||
propagate();
|
||||
if (do_gc)
|
||||
gc();
|
||||
}
|
||||
|
||||
void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
|
||||
|
|
|
@ -429,6 +429,8 @@ namespace bv {
|
|||
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);
|
||||
sat::literal lit = eq_internalize(n, sum);
|
||||
m_bv2ints.push_back(expr2enode(n));
|
||||
ctx.push(push_back_vector<euf::enode_vector>(m_bv2ints));
|
||||
add_unit(lit);
|
||||
}
|
||||
|
||||
|
|
|
@ -211,9 +211,8 @@ namespace bv {
|
|||
return;
|
||||
}
|
||||
euf::enode* n1 = var2enode(eq.v1());
|
||||
for (euf::enode* bv2int : euf::enode_class(n1)) {
|
||||
if (!bv.is_bv2int(bv2int->get_expr()))
|
||||
continue;
|
||||
|
||||
auto propagate_bv2int = [&](euf::enode* bv2int) {
|
||||
euf::enode* bv2int_arg = bv2int->get_arg(0);
|
||||
for (euf::enode* p : euf::enode_parents(n1->get_root())) {
|
||||
if (bv.is_int2bv(p->get_expr()) && p->get_sort() == bv2int_arg->get_sort() && p->get_root() != bv2int_arg->get_root()) {
|
||||
|
@ -224,6 +223,19 @@ namespace bv {
|
|||
break;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
if (m_bv2ints.size() < n1->class_size()) {
|
||||
for (auto* bv2int : m_bv2ints) {
|
||||
if (bv2int->get_root() == n1->get_root())
|
||||
propagate_bv2int(bv2int);
|
||||
}
|
||||
}
|
||||
else {
|
||||
for (euf::enode* bv2int : euf::enode_class(n1)) {
|
||||
if (bv.is_bv2int(bv2int->get_expr()))
|
||||
propagate_bv2int(bv2int);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -279,6 +291,8 @@ namespace bv {
|
|||
++m_stats.m_num_ne2bit;
|
||||
s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent));
|
||||
}
|
||||
else if (!get_config().m_bv_eq_axioms)
|
||||
;
|
||||
else if (s().at_search_lvl()) {
|
||||
force_push();
|
||||
assert_ackerman(v1, v2);
|
||||
|
|
|
@ -207,8 +207,9 @@ namespace bv {
|
|||
literal_vector m_tmp_literals;
|
||||
svector<propagation_item> m_prop_queue;
|
||||
unsigned_vector m_prop_queue_lim;
|
||||
unsigned m_prop_queue_head { 0 };
|
||||
sat::literal m_true { sat::null_literal };
|
||||
unsigned m_prop_queue_head = 0;
|
||||
sat::literal m_true = sat::null_literal;
|
||||
euf::enode_vector m_bv2ints;
|
||||
|
||||
// internalize
|
||||
void insert_bv2a(bool_var bv, atom * a) { m_bool_var2atom.setx(bv, a, 0); }
|
||||
|
|
|
@ -527,7 +527,7 @@ namespace euf {
|
|||
bool merged = false;
|
||||
for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) {
|
||||
euf::enode* n = m_egraph.nodes()[i];
|
||||
if (!is_shared(n) || !m.is_bool(n->get_expr()))
|
||||
if (!m.is_bool(n->get_expr()) || !is_shared(n))
|
||||
continue;
|
||||
if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) {
|
||||
m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
|
||||
|
|
|
@ -599,6 +599,8 @@ namespace smt {
|
|||
TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
|
||||
process_args(n);
|
||||
mk_enode(n);
|
||||
m_bv2int.push_back(ctx.get_enode(n));
|
||||
ctx.push_trail(push_back_vector<enode_vector>(m_bv2int));
|
||||
if (!ctx.relevancy())
|
||||
assert_bv2int_axiom(n);
|
||||
}
|
||||
|
@ -1496,12 +1498,10 @@ namespace smt {
|
|||
unsigned sz = m_bits[v1].size();
|
||||
bool changed = true;
|
||||
TRACE("bv", tout << "bits size: " << sz << "\n";);
|
||||
if (sz == 0) {
|
||||
if (sz == 0 && !m_bv2int.empty()) {
|
||||
// int2bv(bv2int(x)) = x when int2bv(bv2int(x)) has same sort as x
|
||||
enode* n1 = get_enode(r1);
|
||||
for (enode* bv2int : *n1) {
|
||||
if (!m_util.is_bv2int(bv2int->get_expr()))
|
||||
continue;
|
||||
auto propagate_bv2int = [&](enode* bv2int) {
|
||||
enode* bv2int_arg = bv2int->get_arg(0);
|
||||
for (enode* p : enode::parents(n1->get_root())) {
|
||||
if (m_util.is_int2bv(p->get_expr()) && p->get_root() != bv2int_arg->get_root() && p->get_sort() == bv2int_arg->get_sort()) {
|
||||
|
@ -1514,6 +1514,18 @@ namespace smt {
|
|||
break;
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
if (m_bv2int.size() < n1->get_class_size()) {
|
||||
for (enode* bv2int : m_bv2int)
|
||||
if (bv2int->get_root() == n1->get_root())
|
||||
propagate_bv2int(bv2int);
|
||||
}
|
||||
else {
|
||||
for (enode* bv2int : *n1) {
|
||||
if (m_util.is_bv2int(bv2int->get_expr()))
|
||||
propagate_bv2int(bv2int);
|
||||
}
|
||||
}
|
||||
}
|
||||
do {
|
||||
|
|
|
@ -112,6 +112,7 @@ namespace smt {
|
|||
svector<unsigned> m_wpos; // per var, watch position for fixed variable detection.
|
||||
vector<zero_one_bits> m_zero_one_bits; // per var, see comment in the struct zero_one_bit
|
||||
bool_var2atom m_bool_var2atom;
|
||||
enode_vector m_bv2int;
|
||||
typedef svector<theory_var> vars;
|
||||
|
||||
typedef std::pair<numeral, unsigned> value_sort_pair;
|
||||
|
|
Loading…
Reference in a new issue