From 17fc43847623bff8a0a3e2fb1ebfbd6719e6d23a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 21 Aug 2022 15:24:30 -0700 Subject: [PATCH] don't have bv-ackerman influence simplification 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. --- src/sat/sat_solver.h | 1 - src/sat/smt/bv_ackerman.cpp | 12 +++++++----- src/sat/smt/bv_ackerman.h | 12 ++++++------ 3 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 60aadf8a1..dc63c2943 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -714,7 +714,6 @@ namespace sat { // // ----------------------- public: - void set_should_simplify() { m_next_simplify = m_conflicts_since_init; } bool_var_vector const& get_vars_to_reinit() const { return m_vars_to_reinit; } bool is_probing() const { return m_is_probing; } bool is_free(bool_var v) const { return m_free_vars.contains(v); } diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp index 18f0bd951..88cca5257 100644 --- a/src/sat/smt/bv_ackerman.cpp +++ b/src/sat/smt/bv_ackerman.cpp @@ -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(s.s().get_stats().m_conflict * s.get_config().m_dack_factor); diff --git a/src/sat/smt/bv_ackerman.h b/src/sat/smt/bv_ackerman.h index f6465abc7..aab4053a2 100644 --- a/src/sat/smt/bv_ackerman.h +++ b/src/sat/smt/bv_ackerman.h @@ -51,13 +51,13 @@ namespace bv { solver& s; table_t m_table; - vv* m_queue { nullptr }; - vv* m_tmp_vv { nullptr }; + vv* m_queue = nullptr; + vv* m_tmp_vv = nullptr; - unsigned m_gc_threshold { 100 }; - unsigned m_propagate_high_watermark { 10000 }; - unsigned m_propagate_low_watermark { 10 }; - unsigned m_num_propagations_since_last_gc { 0 }; + unsigned m_gc_threshold = 100; + unsigned m_propagate_high_watermark = 10000; + unsigned m_propagate_low_watermark = 10; + unsigned m_num_propagations_since_last_gc = 0; bool_vector m_diff_levels; void update_glue(vv& v);