mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

don't have bv-ackerman influence simplification

Browse source 
previous scheme has Ackmerman module instrument main solver to backjump and simplify when reaching a threshold.
This destroys overall performance: simplification does many more things than invoking Ackerman axioms.
Having a dependency between simplification (in-processing) and depleting a priority queue of auxiliary axioms therefore hurts overall performance. It has to be decoupled. The current approach is now to empty the axiom queue on occasion.
It is still not ideal - it should be coupled with the search level - axioms don't survive higher levels where redundant clauses get garbage collected as they don't have a chance of being used.
This commit is contained in:
Nikolaj Bjorner 2022-08-21 15:24:30 -07:00
parent be0cd74c71
commit 17fc438476
3 changed files with 13 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/sat/smt/bv_ackerman.cpp
View file

@ -57,8 +57,8 @@ namespace bv {
remove(other);
add_cc(v1, v2);
}
else if (other->m_count > m_propagate_high_watermark)
s.s().set_should_simplify();
else if (other->m_count > 2*m_propagate_high_watermark)
propagate();
}
void ackerman::used_diseq_eh(euf::theory_var v1, euf::theory_var v2) {
@ -76,8 +76,8 @@ namespace bv {
new_tmp();
gc();
}
if (other->m_count > m_propagate_high_watermark)
s.s().set_should_simplify();
if (other->m_count > 2*m_propagate_high_watermark)
propagate();
}
void ackerman::update_glue(vv& v) {
@ -137,6 +137,9 @@ namespace bv {
if (m_num_propagations_since_last_gc <= s.get_config().m_dack_gc)
return;
m_num_propagations_since_last_gc = 0;
if (m_table.size() > m_gc_threshold)
propagate();
while (m_table.size() > m_gc_threshold)
remove(m_queue->prev());
@ -147,7 +150,6 @@ namespace bv {
}
void ackerman::propagate() {
SASSERT(s.s().at_base_lvl());
auto* n = m_queue;
vv* k = nullptr;
unsigned num_prop = static_cast<unsigned>(s.s().get_stats().m_conflict * s.get_config().m_dack_factor);