fix removal bug, tune all-interval usage

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

examples/python/all_interval_series.py

@@ -8,6 +8,8 @@ from __future__ import print_function
 from z3 import *
 import time
 
+set_option("sat.gc.burst", False)      # disable GC at every search. It is wasteful for these small queries.
+
 def diff_at_j_is_i(xs, j, i):
     assert(0 <= j and j + 1 < len(xs))
     assert(1 <= i and i < len(xs))

src/sat/sat_params.pyg

@@ -28,7 +28,7 @@ def_module_params('sat',
                           ('gc.increment', UINT, 500, 'increment to the garbage collection threshold'),
                           ('gc.small_lbd', UINT, 3, 'learned clauses with small LBD are never deleted (only used in dyn_psm)'),
                           ('gc.k', UINT, 7, 'learned clauses that are inactive for k gc rounds are permanently deleted (only used in dyn_psm)'),
-                          ('gc.burst', BOOL, True, 'perform eager garbage collection during initialization'),
+                          ('gc.burst', BOOL, False, 'perform eager garbage collection during initialization'),
                           ('gc.defrag', BOOL, True, 'defragment clauses when garbage collecting'),
                           ('simplify.delay', UINT, 0, 'set initial delay of simplification by a conflict count'),
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),

src/sat/sat_simplifier.cpp

@@ -664,8 +664,9 @@ namespace sat {
                 m_sub_todo.insert(it.curr());
             }
             clause_use_list& cs = m_use_list.get(l);
-            for (auto it = cs.mk_iterator(); !it.at_end(); it.next()) {
+            for (auto it = cs.mk_iterator(); !it.at_end(); ) {
                 clause & c = it.curr();
+                it.next();
                 remove_clause(c, l);
             }
             cs.reset();            
@@ -2023,7 +2024,7 @@ namespace sat {
                 m_new_cls.reset();
                 if (!resolve(c1, c2, pos_l, m_new_cls))
                     continue;
-                if (false && v == 27041) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " +  " << c2 << " -> " << m_new_cls << "\n");
+                if (false && v == 767) IF_VERBOSE(0, verbose_stream() << "elim: " << c1 << " +  " << c2 << " -> " << m_new_cls << "\n");
                 TRACE("resolution_new_cls", tout << c1 << "\n" << c2 << "\n-->\n" << m_new_cls << "\n";);
                 if (cleanup_clause(m_new_cls))
                     continue; // clause is already satisfied.

src/sat/sat_simplifier.h

@@ -219,6 +219,8 @@ namespace sat {
         simplifier(solver & s, params_ref const & p);
         ~simplifier();
 
+        void init_search() { m_num_calls = 0; }
+
         void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); }
 
         void reset_todos() {

src/sat/sat_solver.cpp

@@ -524,8 +524,15 @@ namespace sat {
         }
     };
 
+    bool solver::should_defrag() {
+        if (m_defrag_threshold > 0) --m_defrag_threshold;
+        return m_defrag_threshold == 0 && m_config.m_gc_defrag;
+    }
+
     void solver::defrag_clauses() {
+        return;
         if (memory_pressure()) return;
+        pop(scope_lvl());
         IF_VERBOSE(1, verbose_stream() << "(sat-defrag)\n");
         clause_allocator& alloc = m_cls_allocator[!m_cls_allocator_idx];
         ptr_vector<clause> new_clauses, new_learned;
@@ -585,6 +592,8 @@ namespace sat {
 
         cls_allocator().finalize();
         m_cls_allocator_idx = !m_cls_allocator_idx;
+
+        reinit_assumptions();
     }
 
 
@@ -1576,6 +1585,7 @@ namespace sat {
         m_restart_threshold       = m_config.m_restart_initial;
         m_luby_idx                = 1;
         m_gc_threshold            = m_config.m_gc_initial;
+        m_defrag_threshold        = 2;
         m_restarts                = 0;
         m_simplifications         = 0;
         m_conflicts_since_init    = 0;
@@ -1590,6 +1600,7 @@ namespace sat {
         m_core.reset();
         m_min_core_valid = false;
         m_min_core.reset();
+        m_simplifier.init_search();
         TRACE("sat", display(tout););
     }
 
@@ -1939,10 +1950,8 @@ namespace sat {
             break;
         }
         if (m_ext) m_ext->gc();
-        if (gc > 0 && m_config.m_gc_defrag && !memory_pressure()) {
+        if (gc > 0 && should_defrag()) {
-            pop(scope_lvl());
             defrag_clauses();
-            reinit_assumptions();
         }
         m_conflicts_since_gc = 0;
         m_gc_threshold += m_config.m_gc_increment;

src/sat/sat_solver.h

@@ -230,6 +230,7 @@ namespace sat {
         inline void     dealloc_clause(clause* c) { cls_allocator().del_clause(c); }
         struct cmp_activity;
         void defrag_clauses();
+        bool should_defrag();
         bool memory_pressure();
         void del_clause(clause & c);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
@@ -392,6 +393,7 @@ namespace sat {
         unsigned m_luby_idx;
         unsigned m_conflicts_since_gc;
         unsigned m_gc_threshold;
+        unsigned m_defrag_threshold;
         unsigned m_num_checkpoints;
         double   m_min_d_tk;
         unsigned m_next_simplify;