testing memory defragmentation, prefetch, delay ate

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

src/ast/seq_decl_plugin.cpp

@@ -253,6 +253,7 @@ bool zstring::contains(zstring const& other) const {
 
 int zstring::indexof(zstring const& other, int offset) const {
     SASSERT(offset >= 0);
+    if (static_cast<unsigned>(offset) <= length() && other.length() == 0) return offset;
     if (static_cast<unsigned>(offset) == length()) return -1;
     if (other.length() + offset > length()) return -1;
     unsigned last = length() - other.length();

src/sat/ba_solver.cpp

@@ -2245,8 +2245,8 @@ namespace sat {
                 IF_VERBOSE(0, 
                            verbose_stream() << "Discrepancy of watched literal: " << l << " id: " << c.id() 
                            << " clause: " << c << (found?" is watched, but shouldn't be":" not watched, but should be") << "\n";
-                           display_watch_list(verbose_stream() << l << ": ", s().m_cls_allocator, get_wlist(l)) << "\n";
+                           s().display_watch_list(verbose_stream() <<  l << ": ", get_wlist(l)) << "\n";
-                           display_watch_list(verbose_stream() << ~l << ": ", s().m_cls_allocator, get_wlist(~l)) << "\n";
+                           s().display_watch_list(verbose_stream() << ~l << ": ", get_wlist(~l)) << "\n";
                            verbose_stream() << "value: " << value(l) << " level: " << lvl(l) << "\n";
                            display(verbose_stream(), c, true);
                            if (c.lit() != null_literal) verbose_stream() << value(c.lit()) << "\n";);

src/sat/sat_allocator.h

@@ -0,0 +1,101 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    sat_allocator.h
+
+Abstract:
+
+    Small object allocator suitable for clauses
+
+Author:
+
+    Nikolaj bjorner (nbjorner) 2018-04-26.
+
+Revision History:
+--*/
+
+#ifndef SAT_ALLOCATOR_H_
+#define SAT_ALLOCATOR_H_
+
+#include "util/vector.h"
+#include "util/machine.h"
+
+class sat_allocator {
+    static const unsigned CHUNK_SIZE     = (1 << 16);
+    static const unsigned SMALL_OBJ_SIZE = 512;
+    static const unsigned MASK = ((1 << PTR_ALIGNMENT) - 1);
+    static const unsigned NUM_FREE = 1 + (SMALL_OBJ_SIZE >> PTR_ALIGNMENT);
+    struct chunk {
+        char  * m_curr;
+        char    m_data[CHUNK_SIZE];
+        chunk():m_curr(m_data) {}
+    };
+    ptr_vector<chunk>         m_chunks;
+    void *                    m_chunk_ptr;
+    ptr_vector<void>          m_free[NUM_FREE];
+    size_t                    m_alloc_size;
+    char const *              m_id;
+
+    unsigned align_size(size_t sz) const {
+        return  free_slot_id(sz) << PTR_ALIGNMENT;
+    }
+    unsigned free_slot_id(size_t size) const {
+        return (static_cast<unsigned>(size >> PTR_ALIGNMENT) + ((0 != (size & MASK)) ? 1u : 0u));
+    }
+public:
+    sat_allocator(char const * id = "unknown"): m_id(id), m_alloc_size(0), m_chunk_ptr(nullptr) {}
+    ~sat_allocator() { reset(); }
+    void reset() {
+        for (chunk * ch : m_chunks) dealloc(ch);
+        m_chunks.reset();
+        for (unsigned i = 0; i < NUM_FREE; ++i) m_free[i].reset();
+        m_alloc_size = 0;
+        m_chunk_ptr = nullptr;
+    }
+    void * allocate(size_t size) {
+        m_alloc_size += size;
+        if (size >= SMALL_OBJ_SIZE) {
+            return memory::allocate(size);
+        }
+        unsigned slot_id = free_slot_id(size);
+        if (!m_free[slot_id].empty()) {
+            void* result = m_free[slot_id].back();
+            m_free[slot_id].pop_back();
+            return result;
+        }
+        if (m_chunks.empty()) {
+            m_chunks.push_back(alloc(chunk));
+            m_chunk_ptr = m_chunks.back();
+        }
+        
+        unsigned sz = align_size(size);
+        if ((char*)m_chunk_ptr + sz > (char*)m_chunks.back() + CHUNK_SIZE) {
+            m_chunks.push_back(alloc(chunk));
+            m_chunk_ptr = m_chunks.back();            
+        }
+        void * result = m_chunk_ptr;
+        m_chunk_ptr = (char*)m_chunk_ptr + sz;
+        return result;
+    }
+
+    void deallocate(size_t size, void * p) {
+        m_alloc_size -= size;
+        if (size >= SMALL_OBJ_SIZE) {
+            memory::deallocate(p);
+        }
+        else {
+            m_free[free_slot_id(size)].push_back(p);
+        }
+    }
+    size_t get_allocation_size() const { return m_alloc_size; }
+};
+
+inline void * operator new(size_t s, sat_allocator & r) { return r.allocate(s); }
+inline void * operator new[](size_t s, sat_allocator & r) { return r.allocate(s); }
+inline void operator delete(void * p, sat_allocator & r) { UNREACHABLE(); }
+inline void operator delete[](void * p, sat_allocator & r) { UNREACHABLE(); }
+
+#endif /* SAT_ALLOCATOR_H_ */
+

src/sat/sat_clause.cpp

@@ -135,12 +135,15 @@ namespace sat {
         m_allocator("clause-allocator") {
     }
 
+    void clause_allocator::finalize() {
+        m_allocator.reset();
+    }
+
     clause * clause_allocator::get_clause(clause_offset cls_off) const {
         SASSERT(cls_off == reinterpret_cast<clause_offset>(reinterpret_cast<clause*>(cls_off)));
         return reinterpret_cast<clause *>(cls_off);
     }
 
-
     clause_offset clause_allocator::get_offset(clause const * cls) const {
         SASSERT(cls == reinterpret_cast<clause *>(reinterpret_cast<size_t>(cls)));
         return reinterpret_cast<size_t>(cls);
@@ -155,6 +158,18 @@ namespace sat {
         return cls;
     }
 
+    clause * clause_allocator::copy_clause(clause const& other) {
+        size_t size = clause::get_obj_size(other.size());
+        void * mem = m_allocator.allocate(size);
+        clause * cls = new (mem) clause(m_id_gen.mk(), other.size(), other.m_lits, other.is_learned());
+        cls->m_reinit_stack = other.on_reinit_stack();
+        cls->m_glue   = other.glue();
+        cls->m_psm    = other.psm();
+        cls->m_frozen = other.frozen();
+        cls->m_approx = other.approx();
+        return cls;
+    }
+
     void clause_allocator::del_clause(clause * cls) {
         TRACE("sat_clause", tout << "delete: " << cls->id() << " " << *cls << "\n";);
         m_id_gen.recycle(cls->id());

src/sat/sat_clause.h

@@ -19,10 +19,11 @@ Revision History:
 #ifndef SAT_CLAUSE_H_
 #define SAT_CLAUSE_H_
 
-#include "sat/sat_types.h"
 #include "util/small_object_allocator.h"
 #include "util/id_gen.h"
 #include "util/map.h"
+#include "sat/sat_types.h"
+#include "sat/sat_allocator.h"
 
 #ifdef _MSC_VER
 #pragma warning(disable : 4200)
@@ -133,13 +134,16 @@ namespace sat {
        \brief Simple clause allocator that allows uint (32bit integers) to be used to reference clauses (even in 64bit machines).
     */
     class clause_allocator {
-        small_object_allocator m_allocator;
+        small_object_allocator    m_allocator;
-        id_gen                 m_id_gen;
+        id_gen           m_id_gen;
     public:
         clause_allocator();
+        void          finalize();
+        size_t        get_allocation_size() const { return m_allocator.get_allocation_size(); }
         clause *      get_clause(clause_offset cls_off) const;
         clause_offset get_offset(clause const * ptr) const;
         clause *      mk_clause(unsigned num_lits, literal const * lits, bool learned);
+        clause *      copy_clause(clause const& other);
         void          del_clause(clause * cls);
     };
 

src/sat/sat_config.cpp

@@ -41,6 +41,7 @@ namespace sat {
         else
             throw sat_param_exception("invalid restart strategy");
 
+        m_restart_fast = p.restart_fast();
         s = p.phase();
         if (s == symbol("always_false")) 
             m_phase = PS_ALWAYS_FALSE;
@@ -60,6 +61,7 @@ namespace sat {
         m_restart_initial = p.restart_initial();
         m_restart_factor  = p.restart_factor();
         m_restart_max     = p.restart_max();
+        m_propagate_prefetch = p.propagate_prefetch();
         m_inprocess_max   = p.inprocess_max();
 
         m_random_freq     = p.random_freq();
@@ -139,6 +141,7 @@ namespace sat {
         m_gc_small_lbd    = p.gc_small_lbd();
         m_gc_k            = std::min(255u, p.gc_k());
         m_gc_burst        = p.gc_burst();
+        m_gc_defrag       = p.gc_defrag();
 
         m_minimize_lemmas = p.minimize_lemmas();
         m_core_minimize   = p.core_minimize();

src/sat/sat_config.h

@@ -85,7 +85,9 @@ namespace sat {
         unsigned           m_phase_caching_on;
         unsigned           m_phase_caching_off;
         bool               m_phase_sticky;
+        bool               m_propagate_prefetch;
         restart_strategy   m_restart;
+        bool               m_restart_fast;
         unsigned           m_restart_initial;
         double             m_restart_factor; // for geometric case
         unsigned           m_restart_max;
@@ -126,6 +128,7 @@ namespace sat {
         unsigned           m_gc_small_lbd;
         unsigned           m_gc_k;
         bool               m_gc_burst;
+        bool               m_gc_defrag;
 
 
         bool               m_minimize_lemmas;

src/sat/sat_drat.cpp

@@ -42,7 +42,7 @@ namespace sat {
         for (unsigned i = 0; i < m_proof.size(); ++i) {
             clause* c = m_proof[i];
             if (c && (c->size() == 2 || m_status[i] == status::deleted || m_status[i] == status::external)) {
-                s.m_cls_allocator.del_clause(c);
+                s.dealloc_clause(c);
             }
         }
     }
@@ -118,7 +118,7 @@ namespace sat {
             if (st == status::learned) {
                 verify(2, lits);
             }
-            clause* c = s.m_cls_allocator.mk_clause(2, lits, st == status::learned);
+            clause* c = s.alloc_clause(2, lits, st == status::learned);
             m_proof.push_back(c);
             m_status.push_back(st);
             unsigned idx = m_watched_clauses.size();
@@ -452,7 +452,7 @@ namespace sat {
             case 0: add(); break;
             case 1: append(lits[0], status::external); break;
             default: {
-                clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), true);
+                clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), true);
                 append(*c, status::external);
                 break;
             }
@@ -468,7 +468,7 @@ namespace sat {
             case 1: append(c[0], status::learned); break;
             default: {
                 verify(c.size(), c.begin());
-                clause* cl = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), true);
+                clause* cl = s.alloc_clause(c.size(), c.c_ptr(), true);
                 append(*cl, status::external);                
                 break;
             }
@@ -490,7 +490,7 @@ namespace sat {
         TRACE("sat", tout << "del: " << c << "\n";);
         if (m_out) dump(c.size(), c.begin(), status::deleted);
         if (m_check) {
-            clause* c1 = s.m_cls_allocator.mk_clause(c.size(), c.begin(), c.is_learned()); 
+            clause* c1 = s.alloc_clause(c.size(), c.begin(), c.is_learned()); 
             append(*c1, status::deleted);
         }
     }

src/sat/sat_elim_vars.cpp

@@ -185,7 +185,7 @@ namespace sat{
                     s.m_stats.m_mk_ter_clause++;
                 else
                     s.m_stats.m_mk_clause++;
-                clause* cp = s.m_cls_allocator.mk_clause(c.size(), c.c_ptr(), false);
+                clause* cp = s.alloc_clause(c.size(), c.c_ptr(), false);
                 s.m_clauses.push_back(cp);
                 simp.m_use_list.insert(*cp);
                 if (simp.m_sub_counter > 0)
@@ -214,7 +214,7 @@ namespace sat{
         }
         if (b.is_false()) {
             if (lits.size() > 1) {
-                clause* c = s.m_cls_allocator.mk_clause(lits.size(), lits.c_ptr(), false);
+                clause* c = s.alloc_clause(lits.size(), lits.c_ptr(), false);
                 clauses.push_back(c);
             }
             else {

src/sat/sat_iff3_finder.cpp

@@ -136,9 +136,9 @@ namespace sat {
             TRACE("iff3_finder", 
                   tout << "visiting: " << x << "\n";
                   tout << "pos:\n";
-                  display_watch_list(tout, s.m_cls_allocator, pos_wlist);
+                  s.display_watch_list(tout,  pos_wlist);
                   tout << "\nneg:\n";
-                  display_watch_list(tout, s.m_cls_allocator, neg_wlist);
+                  s.display_watch_list(tout, neg_wlist);
                   tout << "\n--------------\n";);
             // traverse the ternary clauses x \/ l1 \/ l2
             bool_var curr_v1 = null_bool_var;

src/sat/sat_integrity_checker.cpp

@@ -66,7 +66,7 @@ namespace sat {
         if (c.size() == 3) {
             CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n";
                    tout << "watch_list:\n";
-                   sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
+                   s.display_watch_list(tout, s.get_wlist(~c[0]));
                    tout << "\n";);
             VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
             VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
@@ -164,9 +164,9 @@ namespace sat {
                        tout << "was_eliminated1: " << s.was_eliminated(l.var());
                        tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var());
                        tout << " learned: " << w.is_learned() << "\n";
-                       sat::display_watch_list(tout, s.m_cls_allocator, wlist);
+                       s.display_watch_list(tout, wlist);
                        tout << "\n";
-                       sat::display_watch_list(tout, s.m_cls_allocator, s.get_wlist(~(w.get_literal())));
+                       s.display_watch_list(tout, s.get_wlist(~(w.get_literal())));
                        tout << "\n";);
                 VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l));
                 break;
@@ -176,7 +176,7 @@ namespace sat {
                 VERIFY(w.get_literal1().index() < w.get_literal2().index());
                 break;
             case watched::CLAUSE:
-                VERIFY(!s.m_cls_allocator.get_clause(w.get_clause_offset())->was_removed());
+                VERIFY(!s.get_clause(w.get_clause_offset()).was_removed());
                 break;
             default:
                 break;

src/sat/sat_params.pyg

@@ -6,9 +6,11 @@ def_module_params('sat',
                           ('phase.caching.on', UINT, 400, 'phase caching on period (in number of conflicts)'),
                           ('phase.caching.off', UINT, 100, 'phase caching off period (in number of conflicts)'),
                           ('phase.sticky', BOOL, False, 'use sticky phase caching for local search'),
+                          ('propagate.prefetch', BOOL, True, 'prefetch watch lists for assigned literals'),
                           ('restart', SYMBOL, 'luby', 'restart strategy: luby or geometric'),
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
+                          ('restart.fast', BOOL, False, 'use fast restart strategy.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
                           ('variable_decay', UINT, 120, 'multiplier (divided by 100) for the VSIDS activity increement'), 
                           ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'),
@@ -24,6 +26,7 @@ def_module_params('sat',
                           ('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.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'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),

src/sat/sat_simplifier.cpp

@@ -100,7 +100,7 @@ namespace sat {
             !m_learned_in_use_lists && m_num_calls >= m_bce_delay && single_threaded();
     }
 
-    bool simplifier::ate_enabled()  const { return m_ate; }
+    bool simplifier::ate_enabled()  const { return m_num_calls >= m_bce_delay && m_ate; }
     bool simplifier::bce_enabled()  const { return bce_enabled_base() && (m_bce || m_bce_at == m_num_calls || m_acce || m_abce || m_cce); }
     bool simplifier::acce_enabled() const { return bce_enabled_base() && m_acce; }
     bool simplifier::cce_enabled()  const { return bce_enabled_base() && (m_cce || m_acce); }
@@ -1581,8 +1581,8 @@ namespace sat {
                 IF_VERBOSE(0, verbose_stream() << "blocked: " << l << " @ " << c << " :covered " << m_covered_clause << "\n";
                            s.m_use_list.display(verbose_stream() << "use  " << l << ":", l);
                            s.m_use_list.display(verbose_stream() << "use  " << ~l << ":", ~l);
-                           display_watch_list(verbose_stream() <<  ~l << ": ", s.s.m_cls_allocator, s.get_wlist(l)) << "\n";
+                           s.s.display_watch_list(verbose_stream() <<  ~l << ": ", s.get_wlist(l)) << "\n";
-                           display_watch_list(verbose_stream() <<   l << ": ", s.s.m_cls_allocator, s.get_wlist(~l)) << "\n";
+                           s.s.display_watch_list(verbose_stream() <<   l << ": ", s.get_wlist(~l)) << "\n";
                            );
                 
             }
@@ -1999,8 +1999,8 @@ namespace sat {
             literal l(v, false);
             IF_VERBOSE(0, 
                        verbose_stream() << "elim: " << l << "\n";
-                       display_watch_list(verbose_stream() <<  ~l << ": ", s.m_cls_allocator, get_wlist(l)) << "\n";
+                       s.display_watch_list(verbose_stream() <<  ~l << ": ", get_wlist(l)) << "\n";
-                       display_watch_list(verbose_stream() <<   l << ": ", s.m_cls_allocator, get_wlist(~l)) << "\n";);
+                       s.display_watch_list(verbose_stream() <<   l << ": ", get_wlist(~l)) << "\n";);
         }
         // eliminate variable
         ++s.m_stats.m_elim_var_res;
@@ -2018,8 +2018,6 @@ namespace sat {
 
         m_elim_counter -= num_pos * num_neg + before_lits;
 
-
-
         for (auto & c1 : m_pos_cls) {
             for (auto & c2 : m_neg_cls) {
                 m_new_cls.reset();
@@ -2046,7 +2044,7 @@ namespace sat {
                         s.m_stats.m_mk_ter_clause++;
                     else
                         s.m_stats.m_mk_clause++;
-                    clause * new_c = s.m_cls_allocator.mk_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
+                    clause * new_c = s.alloc_clause(m_new_cls.size(), m_new_cls.c_ptr(), false);
 
                     if (s.m_config.m_drat) s.m_drat.add(*new_c, true);
                     s.m_clauses.push_back(new_c);

src/sat/sat_solver.cpp

@@ -36,7 +36,8 @@ namespace sat {
         m_rlimit(l),
         m_checkpoint_enabled(true),
         m_config(p),
-        m_par(0),
+        m_par(nullptr),
+        m_cls_allocator_idx(false),
         m_par_syncing_clauses(false),
         m_par_id(0),
         m_cleaner(*this),
@@ -78,7 +79,7 @@ namespace sat {
 
     void solver::del_clauses(clause_vector& clauses) {
         for (clause * cp : clauses) 
-            m_cls_allocator.del_clause(cp);
+            dealloc_clause(cp);
         clauses.reset();
         ++m_stats.m_non_learned_generation;
     }
@@ -298,7 +299,7 @@ namespace sat {
         if (m_config.m_drat && !m_drat.is_cleaned(c)) {
             m_drat.del(c);
         }
-        m_cls_allocator.del_clause(&c);        
+        dealloc_clause(&c);        
         m_stats.m_del_clause++;
     }
 
@@ -396,7 +397,7 @@ namespace sat {
 
     clause * solver::mk_ter_clause(literal * lits, bool learned) {
         m_stats.m_mk_ter_clause++;
-        clause * r = m_cls_allocator.mk_clause(3, lits, learned);
+        clause * r = alloc_clause(3, lits, learned);
         bool reinit = attach_ter_clause(*r);
         if (reinit && !learned) push_reinit_stack(*r);
         if (m_config.m_drat) m_drat.add(*r, learned);
@@ -435,7 +436,7 @@ namespace sat {
 
     clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
         m_stats.m_mk_clause++;
-        clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
+        clause * r = alloc_clause(num_lits, lits, learned);
         SASSERT(!learned || r->is_learned());
         bool reinit = attach_nary_clause(*r);
         if (reinit && !learned) push_reinit_stack(*r);
@@ -452,7 +453,7 @@ namespace sat {
 
     bool solver::attach_nary_clause(clause & c) {
         bool reinit = false;
-        clause_offset cls_off = m_cls_allocator.get_offset(&c);
+        clause_offset cls_off = cls_allocator().get_offset(&c);
         if (!at_base_lvl()) {
             if (c.is_learned()) {
                 unsigned w2_idx = select_learned_watch_lit(c);
@@ -511,6 +512,85 @@ namespace sat {
         }
     }
 
+    bool solver::memory_pressure() {
+        return 3*cls_allocator().get_allocation_size()/2 + memory::get_allocation_size() > memory::get_max_memory_size();
+    }
+
+    struct solver::cmp_activity {
+        solver& s;
+        cmp_activity(solver& s):s(s) {}
+        bool operator()(bool_var v1, bool_var v2) const {
+            return s.m_activity[v1] > s.m_activity[v2];
+        }
+    };
+
+    void solver::defrag_clauses() {
+        if (memory_pressure()) return;
+        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;
+        ptr_addr_map<clause, clause_offset> cls2offset;
+        for (clause* c : m_clauses) c->unmark_used();
+        for (clause* c : m_learned) c->unmark_used();
+
+        svector<bool_var> vars;
+        for (unsigned i = 0; i < num_vars(); ++i) vars.push_back(i);
+        std::stable_sort(vars.begin(), vars.end(), cmp_activity(*this));
+        literal_vector lits;
+        for (bool_var v : vars) lits.push_back(to_literal(v)), lits.push_back(~to_literal(v));
+
+        // walk clauses, reallocate them in an order that defragments memory and creates locality.
+        //for (literal lit : lits) {
+        //watch_list& wlist = m_watches[lit.index()];
+        for (watch_list& wlist : m_watches) {            
+            for (watched& w : wlist) {
+                if (w.is_clause()) {
+                    clause& c1 = get_clause(w);
+                    clause_offset offset;
+                    if (c1.was_used()) {
+                        offset = cls2offset[&c1];
+                    }
+                    else {
+                        clause* c2 = alloc.copy_clause(c1); 
+                        c1.mark_used();
+                        if (c1.is_learned()) {
+                            new_learned.push_back(c2);
+                        }
+                        else {
+                            new_clauses.push_back(c2);
+                        }
+                        offset = get_offset(*c2);
+                        cls2offset.insert(&c1, offset);
+                    }
+                    w = watched(w.get_blocked_literal(), offset);
+                }
+            }
+        }
+
+        // reallocate ternary clauses.
+        for (clause* c : m_clauses) {
+            if (!c->was_used()) {
+                SASSERT(c->size() == 3);
+                new_clauses.push_back(alloc.copy_clause(*c));
+            }
+            dealloc_clause(c);
+        }
+
+        for (clause* c : m_learned) {
+            if (!c->was_used()) {
+                SASSERT(c->size() == 3);
+                new_learned.push_back(alloc.copy_clause(*c));
+            }
+            dealloc_clause(c);
+        }
+        m_clauses.swap(new_clauses);
+        m_learned.swap(new_learned);
+
+        cls_allocator().finalize();
+        m_cls_allocator_idx = !m_cls_allocator_idx;
+    }
+
+
     void solver::set_learned(literal l1, literal l2, bool learned) {
         set_learned1(l1, l2, learned);
         set_learned1(l2, l1, learned);
@@ -702,6 +782,7 @@ namespace sat {
             m_reasoned[v] = 0;
             break;
         }
+
         if (m_config.m_anti_exploration) {
             uint64 age = m_stats.m_conflict - m_canceled[v];
             if (age > 0) {
@@ -712,7 +793,10 @@ namespace sat {
                 m_case_split_queue.activity_changed_eh(v, false);
             }
         }
-
+        
+        if (m_config.m_propagate_prefetch) {
+            _mm_prefetch((char const*)(m_watches.c_ptr() + l.index()), 0);
+        }
 
         SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
         SASSERT(l.sign()  || m_phase[v] == POS_PHASE);
@@ -725,9 +809,8 @@ namespace sat {
 
     lbool solver::status(clause const & c) const {
         bool found_undef = false;
-        unsigned sz = c.size();
+        for (literal lit : c) {
-        for (unsigned i = 0; i < sz; i++) {
+            switch (value(lit)) {
-            switch (value(c[i])) {
             case l_true:
                 return l_true;
             case l_undef:
@@ -1006,7 +1089,7 @@ namespace sat {
                     return l_undef;
                 }
 
-                restart();
+                restart(!m_config.m_restart_fast);
                 simplify_problem();
                 if (check_inconsistent()) return l_false;
                 gc();
@@ -1507,6 +1590,7 @@ namespace sat {
         m_min_d_tk                = 1.0;
         m_search_lvl              = 0;
         m_conflicts_since_gc      = 0;
+        m_restart_next_out        = 0;
         m_asymm_branch.init_search();
         m_stopwatch.reset();
         m_stopwatch.start();
@@ -1752,15 +1836,34 @@ namespace sat {
         return ok;
     }
 
-    void solver::restart() {
+    void solver::restart(bool to_base) {
         m_stats.m_restart++;
         m_restarts++;
-        IF_VERBOSE(1,
+        if (m_conflicts_since_init > m_restart_next_out + 500) {
-                   verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
+            m_restart_next_out = m_conflicts_since_init;
-                   << " :restarts " << m_stats.m_restart << mk_stat(*this)
+            IF_VERBOSE(1,
-                   << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
+                       verbose_stream() << "(sat-restart :conflicts " << m_stats.m_conflict << " :decisions " << m_stats.m_decision
+                       << " :restarts " << m_stats.m_restart << mk_stat(*this)
+                       << " :time " << std::fixed << std::setprecision(2) << m_stopwatch.get_current_seconds() << ")\n";);
+        }
         IF_VERBOSE(30, display_status(verbose_stream()););
-        pop_reinit(scope_lvl() - search_lvl());
+        unsigned num_scopes = 0;
+        if (to_base || scope_lvl() == search_lvl()) {
+            num_scopes = scope_lvl() - search_lvl();
+        }
+        else {
+            bool_var next = m_case_split_queue.min_var();
+            do {
+                scope& s = m_scopes[scope_lvl() - num_scopes - 1];
+                bool_var prev = m_trail[s.m_trail_lim].var();
+                //IF_VERBOSE(0, verbose_stream() << "more active: " << m_case_split_queue.more_active(next, prev) << "\n");
+                if (!m_case_split_queue.more_active(next, prev)) break;                
+                ++num_scopes;
+            }
+            while (num_scopes < scope_lvl() - search_lvl());
+            //IF_VERBOSE(0, verbose_stream() << "backtrack " << num_scopes << " " << scope_lvl() - search_lvl() << "\n");
+        }
+        pop_reinit(num_scopes);
         m_conflicts_since_restart = 0;
         switch (m_config.m_restart) {
         case RS_GEOMETRIC:
@@ -1788,6 +1891,7 @@ namespace sat {
             return;
         if (m_config.m_gc_strategy == GC_DYN_PSM && !at_base_lvl())
             return;
+        unsigned gc = m_stats.m_gc_clause;
         IF_VERBOSE(10, verbose_stream() << "(sat.gc)\n";);
         CASSERT("sat_gc_bug", check_invariant());
         switch (m_config.m_gc_strategy) {
@@ -1813,6 +1917,11 @@ namespace sat {
             break;
         }
         if (m_ext) m_ext->gc();
+        if (gc > 0 && m_config.m_gc_defrag && !memory_pressure()) {
+            pop(scope_lvl());
+            defrag_clauses();
+            reinit_assumptions();
+        }
         m_conflicts_since_gc = 0;
         m_gc_threshold += m_config.m_gc_increment;
         CASSERT("sat_gc_bug", check_invariant());
@@ -2320,8 +2429,7 @@ namespace sat {
     void solver::resolve_conflict_for_unsat_core() {
         TRACE("sat", display(tout);
               unsigned level = 0;
-              for (unsigned i = 0; i < m_trail.size(); ++i) {
+              for (literal l : m_trail) {
-                  literal l = m_trail[i];
                   if (level != m_level[l.var()]) {
                       level = m_level[l.var()];
                       tout << level << ": ";
@@ -2341,8 +2449,8 @@ namespace sat {
         }
         SASSERT(m_unmark.empty());
         DEBUG_CODE({
-                for (unsigned i = 0; i < m_trail.size(); ++i) {
+                for (literal lit : m_trail) {
-                    SASSERT(!is_marked(m_trail[i].var()));
+                    SASSERT(!is_marked(lit.var()));
                 }});
 
         unsigned old_size = m_unmark.size();
@@ -2798,8 +2906,7 @@ namespace sat {
             }
         }
         reset_mark(m_lemma[0].var());
-        for (unsigned i = m_lemma.size(); i > sz; ) {
+        for (unsigned i = m_lemma.size(); i-- > sz; ) {
-            --i;
             reset_mark(m_lemma[i].var());
         }
         m_lemma.shrink(sz);
@@ -3431,7 +3538,7 @@ namespace sat {
     }
 
     void solver::display_watches(std::ostream & out, literal lit) const {
-        sat::display_watch_list(out << lit << ": ", m_cls_allocator, get_wlist(lit)) << "\n";
+        display_watch_list(out << lit << ": ", get_wlist(lit)) << "\n";
     }
 
     void solver::display_watches(std::ostream & out) const {
@@ -3439,10 +3546,14 @@ namespace sat {
         for (watch_list const& wlist : m_watches) {
             literal l = to_literal(l_idx++);
             if (!wlist.empty()) 
-                sat::display_watch_list(out << l << ": ", m_cls_allocator, wlist) << "\n";
+                display_watch_list(out << l << ": ", wlist) << "\n";
         }
     }
 
+    std::ostream& solver::display_watch_list(std::ostream& out, watch_list const& wl) const {
+        return sat::display_watch_list(out, cls_allocator(), wl);
+    }
+
     void solver::display_assignment(std::ostream & out) const {
         out << m_trail << "\n";
     }
@@ -3774,7 +3885,7 @@ namespace sat {
                 return l_undef;
             }
 
-            restart();
+            restart(true);
             simplify_problem();
             if (check_inconsistent()) {
                 fixup_consequence_core();
@@ -3867,7 +3978,7 @@ namespace sat {
                 else {
                     is_sat = bounded_search();
                     if (is_sat == l_undef) {
-                        restart();
+                        restart(true);
                     }
                     extract_fixed_consequences(unfixed_lits, assumptions, unfixed_vars, conseq);
                 }

src/sat/sat_solver.h

@@ -86,7 +86,8 @@ namespace sat {
         scoped_ptr<extension>   m_ext;
         parallel*               m_par;
         random_gen              m_rand;
-        clause_allocator        m_cls_allocator;
+        clause_allocator        m_cls_allocator[2];
+        bool                    m_cls_allocator_idx;
         cleaner                 m_cleaner;
         model                   m_model;        
         model_converter         m_mc;
@@ -217,9 +218,16 @@ namespace sat {
         void mk_clause(literal_vector const& lits, bool learned = false) { mk_clause(lits.size(), lits.c_ptr(), learned); }
         void mk_clause(unsigned num_lits, literal * lits, bool learned = false);
         void mk_clause(literal l1, literal l2, bool learned = false);
-        void mk_clause(literal l1, literal l2, literal l3, bool learned = false);
+        void mk_clause(literal l1, literal l2, literal l3, bool learned = false);        
 
     protected:
+        inline clause_allocator& cls_allocator() { return m_cls_allocator[m_cls_allocator_idx]; }
+        inline clause_allocator const& cls_allocator() const { return m_cls_allocator[m_cls_allocator_idx]; }
+        inline clause * alloc_clause(unsigned num_lits, literal const * lits, bool learned) { return cls_allocator().mk_clause(num_lits, lits, learned); }
+        inline void     dealloc_clause(clause* c) { cls_allocator().del_clause(c); }
+        struct cmp_activity;
+        void defrag_clauses();
+        bool memory_pressure();
         void del_clause(clause & c);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
         clause * mk_clause_core(literal_vector const& lits) { return mk_clause_core(lits.size(), lits.c_ptr()); }
@@ -301,7 +309,7 @@ namespace sat {
         void set_conflict(justification c, literal not_l);
         void set_conflict(justification c) { set_conflict(c, null_literal); }
         lbool status(clause const & c) const;        
-        clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
+        clause_offset get_offset(clause const & c) const { return cls_allocator().get_offset(&c); }
         void checkpoint() {
             if (!m_checkpoint_enabled) return;
             if (!m_rlimit.inc()) {
@@ -373,6 +381,7 @@ namespace sat {
 
         unsigned m_conflicts_since_init;
         unsigned m_restarts;
+        unsigned m_restart_next_out;
         unsigned m_conflicts_since_restart;
         unsigned m_simplifications;
         unsigned m_restart_threshold;
@@ -405,7 +414,7 @@ namespace sat {
         void simplify_problem();
         void mk_model();
         bool check_model(model const & m) const;
-        void restart();
+        void restart(bool to_base);
         void sort_watch_lits();
         void exchange_par();
         lbool check_par(unsigned num_lits, literal const* lits);
@@ -437,7 +446,7 @@ namespace sat {
             if (value(l0) != l_true)
                 return true;
             justification const & jst = m_justification[l0.var()];
-            return !jst.is_clause() || m_cls_allocator.get_clause(jst.get_clause_offset()) != &c;
+            return !jst.is_clause() || cls_allocator().get_clause(jst.get_clause_offset()) != &c;
         }
 
         clause& get_clause(watch_list::iterator it) const {
@@ -445,13 +454,18 @@ namespace sat {
             return get_clause(it->get_clause_offset());
         }
 
+        clause& get_clause(watched const& w) const {
+            SASSERT(w.get_kind() == watched::CLAUSE);
+            return get_clause(w.get_clause_offset());
+        }
+
         clause& get_clause(justification const& j) const {
             SASSERT(j.is_clause());
             return get_clause(j.get_clause_offset());
         }
 
         clause& get_clause(clause_offset cls_off) const {
-            return *(m_cls_allocator.get_clause(cls_off));
+            return *(cls_allocator().get_clause(cls_off));
         }
         
         // -----------------------
@@ -634,6 +648,7 @@ namespace sat {
         void display_wcnf(std::ostream & out, unsigned sz, literal const* lits, unsigned const* weights) const;
         void display_assignment(std::ostream & out) const;
         std::ostream& display_justification(std::ostream & out, justification const& j) const;
+        std::ostream& display_watch_list(std::ostream& out, watch_list const& wl) const;
 
     protected:
         void display_binary(std::ostream & out) const;

src/sat/sat_var_queue.h

@@ -72,6 +72,8 @@ namespace sat {
         bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
 
         bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
+
+        bool more_active(bool_var v1, bool_var v2) const { return m_queue.less_than(v1, v2); }
     };
 };
 

src/util/heap.h

@@ -27,10 +27,6 @@ class heap : private LT {
     int_vector    m_values;
     int_vector    m_value2indices;
 
-    bool less_than(int v1, int v2) const { 
-        return LT::operator()(v1, v2); 
-    }
-
     static int left(int i) { 
         return i << 1; 
     }
@@ -126,6 +122,10 @@ public:
         CASSERT("heap", check_invariant());
     }
 
+    bool less_than(int v1, int v2) const { 
+        return LT::operator()(v1, v2); 
+    }
+
     bool empty() const { 
         return m_values.size() == 1; 
     }