tune cardinality solver for cache misses

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

src/sat/card_extension.cpp

@@ -119,20 +119,37 @@ namespace sat {
         if (m_var_infos.size() <= static_cast<unsigned>(lit.var())) {
             return;
         }
-        ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
+        ptr_vector<card>*& cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
         if (cards) {
-            remove(*cards, c);        
+            if (remove(*cards, c)) {
+                std::cout << "Empty: " << cards->empty() << "\n";
+                cards = set_tag_empty(cards);
+            }        
         }
     }
 
-    void card_extension::remove(ptr_vector<card>& cards, card* c) {
-        for (unsigned j = 0; j < cards.size(); ++j) {
+    ptr_vector<card_extension::card>* card_extension::set_tag_empty(ptr_vector<card>* c) {
+        return TAG(ptr_vector<card>*, c, 1);
+    }
+
+    bool card_extension::is_tag_empty(ptr_vector<card>* c) {
+        return !c || GET_TAG(c) == 1;
+    }
+
+    ptr_vector<card_extension::card>* card_extension::set_tag_non_empty(ptr_vector<card>* c) {
+        return UNTAG(ptr_vector<card>*, c);
+    }
+
+    bool card_extension::remove(ptr_vector<card>& cards, card* c) {
+        unsigned sz = cards.size();
+        for (unsigned j = 0; j < sz; ++j) {
             if (cards[j] == c) {                        
-                std::swap(cards[j], cards[cards.size()-1]);
+                std::swap(cards[j], cards[sz-1]);
                 cards.pop_back();
-                break;
+                return sz == 1;
             }
         }
+        return false;
     }
 
     void card_extension::assign(card& c, literal lit) {
@@ -171,6 +188,10 @@ namespace sat {
             cards = alloc(ptr_vector<card>);
             m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;
         }
+        else if (is_tag_empty(cards)) {
+            cards = set_tag_non_empty(cards);
+            m_var_infos[lit.var()].m_lit_watch[lit.sign()] = cards;            
+        }
         TRACE("sat_verbose", tout << "insert: " << lit.var() << " " << lit.sign() << "\n";);
         cards->push_back(&c);
     }
@@ -617,13 +638,16 @@ namespace sat {
 
     void card_extension::asserted(literal l) {
         bool_var v = l.var();
+        if (s().inconsistent()) return;
         if (v >= m_var_infos.size()) return;
         var_info& vinfo = m_var_infos[v];
         ptr_vector<card>* cards = vinfo.m_lit_watch[!l.sign()];
         //TRACE("sat", tout << "retrieve: " << v << " " << !l.sign() << "\n";);
         //TRACE("sat", tout << "asserted: " << l << " " << (cards ? "non-empty" : "empty") << "\n";);
-        if (cards != 0  && !cards->empty() && !s().inconsistent())  {
-            ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
+        static unsigned is_empty = 0, non_empty = 0;
+        if (!is_tag_empty(cards)) {
+            ptr_vector<card>::iterator begin = cards->begin();
+            ptr_vector<card>::iterator it = begin, it2 = it, end = cards->end();
             for (; it != end; ++it) {
                 card& c = *(*it);
                 if (value(c.lit()) != l_true) {
@@ -648,6 +672,9 @@ namespace sat {
                 }
             }
             cards->set_end(it2);
+            if (cards->empty()) {
+                m_var_infos[v].m_lit_watch[!l.sign()] = set_tag_empty(cards);
+            }
         }
 
         card* crd = vinfo.m_card;

src/sat/card_extension.h

@@ -71,11 +71,14 @@ namespace sat {
             }
             void reset() {
                 dealloc(m_card);
-                dealloc(m_lit_watch[0]);
-                dealloc(m_lit_watch[1]);
+                dealloc(card_extension::set_tag_non_empty(m_lit_watch[0]));
+                dealloc(card_extension::set_tag_non_empty(m_lit_watch[1]));
             }
         };
 
+        ptr_vector<card>* set_tag_empty(ptr_vector<card>* c);        
+        bool is_tag_empty(ptr_vector<card>* c);
+        static ptr_vector<card>* set_tag_non_empty(ptr_vector<card>* c);
 
         solver*             m_solver;
         stats               m_stats;        
@@ -113,7 +116,7 @@ namespace sat {
         inline unsigned lvl(bool_var v) const { return m_solver->lvl(v); }
 
         void unwatch_literal(literal w, card* c);
-        void remove(ptr_vector<card>& cards, card* c);
+        bool remove(ptr_vector<card>& cards, card* c);
 
         void normalize_active_coeffs();
         void inc_coeff(literal l, int offset);

src/sat/sat_cleaner.cpp

@@ -142,12 +142,17 @@ namespace sat {
                         c.shrink(new_sz);
                         *it2 = *it;
                         it2++;
-                        if (!c.frozen()) {
-                            if (new_sz == 3)
+                        if (!c.frozen()) {                            
+                            if (new_sz == 3) 
                                 s.attach_ter_clause(c);
                             else
                                 s.attach_nary_clause(c);
                         }
+                        if (s.m_config.m_drat) {
+                            // for optimization, could also report deletion 
+                            // of previous version of clause.
+                            s.m_drat.add(c, true);
+                        }
                     }
                 }
             }

src/sat/sat_par.cpp

@@ -117,7 +117,7 @@ namespace sat {
             if (i == 1 + num_threads/2) {
                 s.m_params.set_sym("phase", symbol("random"));
             }                        
-            m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i], 0);
+            m_solvers[i] = alloc(sat::solver, s.m_params, m_limits[i]);
             m_solvers[i]->copy(s);
             m_solvers[i]->set_par(this, i);
             m_scoped_rlimit.push_child(&m_solvers[i]->rlimit());            

src/sat/sat_simplifier.cpp

@@ -304,6 +304,9 @@ namespace sat {
                     s.attach_ter_clause(c);
                 else
                     s.attach_nary_clause(c);
+                if (s.m_config.m_drat) {
+                    s.m_drat.add(c, true);
+                }
             }
         }
         cs.set_end(it2);

src/sat/sat_solver.cpp

@@ -31,10 +31,9 @@ Revision History:
 
 namespace sat {
 
-    solver::solver(params_ref const & p, reslimit& l, extension * ext):
+    solver::solver(params_ref const & p, reslimit& l):
         m_rlimit(l),
         m_config(p),
-        m_ext(ext),
         m_par(0),
         m_par_syncing_clauses(false),
         m_par_id(0),
@@ -59,7 +58,6 @@ namespace sat {
         m_conflicts               = 0;
         m_next_simplify           = 0;
         m_num_checkpoints         = 0;
-        if (m_ext) m_ext->set_solver(this);
     }
 
     solver::~solver() {
@@ -77,6 +75,11 @@ namespace sat {
         ++m_stats.m_non_learned_generation;
     }
 
+    void solver::set_extension(extension* ext) {
+        m_ext = ext;
+        if (ext) ext->set_solver(this);
+    }
+
     void solver::copy(solver const & src) {
         pop_to_base_level();
         SASSERT(m_mc.empty() && src.m_mc.empty());
@@ -771,7 +774,7 @@ namespace sat {
         flet<bool> _searching(m_searching, true);
 #ifdef CLONE_BEFORE_SOLVING
         if (m_mc.empty()) {
-            m_clone = alloc(solver, m_params, 0 /* do not clone extension */);
+            m_clone = alloc(solver, m_params);
             SASSERT(m_clone);
         }
 #endif

src/sat/sat_solver.h

@@ -156,7 +156,7 @@ namespace sat {
         friend class par;
         friend struct mk_stat;
     public:
-        solver(params_ref const & p, reslimit& l, extension * ext);
+        solver(params_ref const & p, reslimit& l);
         ~solver();
 
         // -----------------------
@@ -264,6 +264,7 @@ namespace sat {
         bool canceled() { return !m_rlimit.inc(); }
         config const& get_config() { return m_config; }
         extension* get_extension() const { return m_ext.get(); }
+        void       set_extension(extension* e);
         typedef std::pair<literal, literal> bin_clause;
     protected:
         watch_list & get_wlist(literal l) { return m_watches[l.index()]; }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -72,7 +72,7 @@ class inc_sat_solver : public solver {
 public:
     inc_sat_solver(ast_manager& m, params_ref const& p):
         m(m), 
-        m_solver(p, m.limit(), alloc(sat::card_extension)),
+        m_solver(p, m.limit()),
         m_params(p), m_optimize_model(false),
         m_fmls(m),
         m_asmsf(m),

src/sat/tactic/goal2sat.cpp

@@ -78,11 +78,6 @@ struct goal2sat::imp {
         m_default_external(default_external) {
         updt_params(p);
         m_true = sat::null_bool_var;
-        sat::extension* e = m_solver.get_extension();
-        if (e) {
-            sat::card_extension* ce = dynamic_cast<sat::card_extension*>(e);
-            m_ext = ce;
-        }
     }
         
     void updt_params(params_ref const & p) {
@@ -158,7 +153,8 @@ struct goal2sat::imp {
     }
 
     bool convert_app(app* t, bool root, bool sign) {
-        if (m_ext && t->get_family_id() == pb.get_family_id()) {
+        if (t->get_family_id() == pb.get_family_id()) {
+            ensure_extension();
             m_frame_stack.push_back(frame(to_app(t), root, sign, 0));
             return false;
         }
@@ -465,6 +461,20 @@ struct goal2sat::imp {
         }
     }
 
+    void ensure_extension() {
+        if (!m_ext) {
+            sat::extension* ext = m_solver.get_extension();
+            if (ext) {
+                m_ext = dynamic_cast<sat::card_extension*>(ext);
+                SASSERT(m_ext);
+            }
+            if (!m_ext) {
+                m_ext = alloc(sat::card_extension);
+                m_solver.set_extension(m_ext);
+            }
+        }
+    }
+
     void convert(app * t, bool root, bool sign) {
         if (t->get_family_id() == m.get_basic_family_id()) {
             switch (to_app(t)->get_decl_kind()) {
@@ -485,7 +495,8 @@ struct goal2sat::imp {
                 UNREACHABLE();
             }
         }
-        else if (m_ext && t->get_family_id() == pb.get_family_id()) {
+        else if (t->get_family_id() == pb.get_family_id()) {
+            ensure_extension();
             switch (t->get_decl_kind()) {
             case OP_AT_MOST_K:
                 convert_at_most_k(t, pb.get_k(t), root, sign);

src/sat/tactic/sat_tactic.cpp

@@ -34,7 +34,7 @@ class sat_tactic : public tactic {
         
         imp(ast_manager & _m, params_ref const & p):
             m(_m),
-            m_solver(p, m.limit(), 0),
+            m_solver(p, m.limit()),
             m_params(p) {
             SASSERT(!m.proofs_enabled());
         }

src/shell/dimacs_frontend.cpp

@@ -126,7 +126,6 @@ static void track_clauses(sat::solver const& src,
     }
 }
 
-
 unsigned read_dimacs(char const * file_name) {
     g_start_time = clock();
     register_on_timeout_proc(on_timeout);
@@ -134,7 +133,7 @@ unsigned read_dimacs(char const * file_name) {
     params_ref p = gparams::get_module("sat");
     p.set_bool("produce_models", true);
     reslimit limit;
-    sat::solver solver(p, limit, 0);
+    sat::solver solver(p, limit);
     g_solver = &solver;
 
     if (file_name) {
@@ -152,7 +151,7 @@ unsigned read_dimacs(char const * file_name) {
     
     lbool r;
     vector<sat::literal_vector> tracking_clauses;
-    sat::solver solver2(p, limit, 0);
+    sat::solver solver2(p, limit);
     if (p.get_bool("dimacs.core", false)) {
         g_solver = &solver2;        
         sat::literal_vector assumptions;

src/test/sat_user_scope.cpp

@@ -59,7 +59,7 @@ static void init_vars(sat::solver& s) {
 static void check_coherence(sat::solver& s1, trail_t& t) {
     params_ref p;
     reslimit rlim;
-    sat::solver s2(p, rlim, 0);
+    sat::solver s2(p, rlim);
     init_vars(s2);
     sat::literal_vector cls;
     for (unsigned i = 0; i < t.size(); ++i) {
@@ -85,7 +85,7 @@ void tst_sat_user_scope() {
     trail_t trail;
     params_ref p;
     reslimit rlim;
-    sat::solver s(p, rlim, 0);  // incremental solver
+    sat::solver s(p, rlim);  // incremental solver
     init_vars(s);
     while (true) {
         for (unsigned i = 0; i < s_num_frames; ++i) {