Merge pull request #789 from wintersteiger/gh570-att-2

Gh570 att 2

src/sat/sat_clause.h

@@ -102,10 +102,14 @@ namespace sat {
         unsigned m_val1;
         unsigned m_val2;
     public:
-        bin_clause(literal l1, literal l2, bool learned):m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
+        bin_clause(literal l1, literal l2, bool learned) :m_val1(l1.to_uint()), m_val2((l2.to_uint() << 1) + static_cast<unsigned>(learned)) {}
         literal get_literal1() const { return to_literal(m_val1); }
         literal get_literal2() const { return to_literal(m_val2 >> 1); }
         bool is_learned() const { return (m_val2 & 1) == 1; }
+        bool operator==(const bin_clause & other) const {
+            return (m_val1 == other.m_val1 && m_val2 == other.m_val2) ||
+                   (m_val1 == other.m_val2 && m_val2 == other.m_val1);
+        }
     };
 
     class tmp_clause {

src/sat/sat_probing.cpp

@@ -239,7 +239,7 @@ namespace sat {
             m_counter *= 2;
         }
         CASSERT("probing", s.check_invariant());
-        free_memory();
+        finalize();
         return r;
     }
 
@@ -255,9 +255,10 @@ namespace sat {
         // TODO
     }
 
-    void probing::free_memory() {
+    void probing::finalize() {
-        m_assigned.cleanup();
+        m_assigned.finalize();
         m_to_assert.finalize();
+        m_cached_bins.finalize();
     }
 
     void probing::collect_statistics(statistics & st) const {

src/sat/sat_probing.h

@@ -69,7 +69,7 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void free_memory();
+        void finalize();
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();

src/sat/sat_simplifier.cpp

@@ -63,6 +63,7 @@ namespace sat {
     }
 
     simplifier::~simplifier() {
+        finalize();
     }
 
     inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
@@ -96,7 +97,7 @@ namespace sat {
     inline void simplifier::remove_clause_core(clause & c) {
         unsigned sz = c.size();
         for (unsigned i = 0; i < sz; i++)
-            insert_todo(c[i].var());
+            insert_elim_todo(c[i].var());
         m_sub_todo.erase(c);
         c.set_removed(true);
         TRACE("resolution_bug", tout << "del_clause: " << c << "\n";);
@@ -116,6 +117,7 @@ namespace sat {
     inline void simplifier::remove_bin_clause_half(literal l1, literal l2, bool learned) {
         SASSERT(s.get_wlist(~l1).contains(watched(l2, learned)));
         s.get_wlist(~l1).erase(watched(l2, learned));
+        m_sub_bin_todo.erase(bin_clause(l1, l2, learned));
     }
 
     void simplifier::init_visited() {
@@ -123,21 +125,38 @@ namespace sat {
         m_visited.resize(2*s.num_vars(), false);
     }
 
-    void simplifier::free_memory() {
+    void simplifier::finalize() {
         m_use_list.finalize();
         m_sub_todo.finalize();
         m_sub_bin_todo.finalize();
+        m_elim_todo.finalize();
         m_visited.finalize();
         m_bs_cs.finalize();
         m_bs_ls.finalize();
     }
 
+    void simplifier::initialize() {
+        m_need_cleanup = false;
+        s.m_cleaner(true);
+        m_last_sub_trail_sz = s.m_trail.size();
+        m_use_list.init(s.num_vars());
+        m_sub_todo.reset();
+        m_sub_bin_todo.reset();
+        m_elim_todo.reset();
+        init_visited();
+        TRACE("after_cleanup", s.display(tout););
+        CASSERT("sat_solver", s.check_invariant());
+    }
+
     void simplifier::operator()(bool learned) {
         if (s.inconsistent())
             return;
         if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution)
             return;
 
+
+        initialize();
+
         CASSERT("sat_solver", s.check_invariant());
         TRACE("before_simplifier", s.display(tout););
 
@@ -157,10 +176,10 @@ namespace sat {
         }
         register_clauses(s.m_clauses);
 
+
         if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
             elim_blocked_clauses();
 
-
         if (!learned)
             m_num_calls++;
 
@@ -199,7 +218,7 @@ namespace sat {
         }
         CASSERT("sat_solver", s.check_invariant());
         TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout););
-        free_memory();
+        finalize();
     }
 
     /**
@@ -619,7 +638,7 @@ namespace sat {
         TRACE("elim_lit", tout << "processing: " << c << "\n";);
         m_need_cleanup = true;
         m_num_elim_lits++;
-        insert_todo(l.var());
+        insert_elim_todo(l.var());
         c.elim(l);
         clause_use_list & occurs = m_use_list.get(l);
         occurs.erase_not_removed(c);
@@ -924,8 +943,8 @@ namespace sat {
             model_converter::entry * new_entry = 0;
             if (s.is_external(l.var()) || s.was_eliminated(l.var()))
                 return;
-            {
 
+            {
                 m_to_remove.reset();
                 {
                     clause_use_list & occs = s.m_use_list.get(l);
@@ -1237,12 +1256,14 @@ namespace sat {
                 for (; it2 != end2; ++it2) {
                     if (it2->is_binary_clause() && it2->get_literal() == l) {
                         TRACE("bin_clause_bug", tout << "removing: " << l << " " << it2->get_literal() << "\n";);
+                        m_sub_bin_todo.erase(bin_clause(l2, l, it2->is_learned()));
                         continue;
                     }
                     *itprev = *it2;
                     itprev++;
                 }
                 wlist2.set_end(itprev);
+                m_sub_bin_todo.erase(bin_clause(l, l2, it->is_learned()));
             }
         }
         TRACE("bin_clause_bug", tout << "collapsing watch_list of: " << l << "\n";);

src/sat/sat_simplifier.h

@@ -97,6 +97,8 @@ namespace sat {
 
         void checkpoint();
 
+        void initialize();
+
         void init_visited();
         void mark_visited(literal l) { m_visited[l.index()] = true; }
         void unmark_visited(literal l) { m_visited[l.index()] = false; }
@@ -172,15 +174,20 @@ namespace sat {
         simplifier(solver & s, params_ref const & p);
         ~simplifier();
 
-        void insert_todo(bool_var v) { m_elim_todo.insert(v); }
+        void insert_elim_todo(bool_var v) { m_elim_todo.insert(v); }
-        void reset_todo() { m_elim_todo.reset(); }
+
+        void reset_todos() {
+            m_elim_todo.reset();
+            m_sub_todo.reset();
+            m_sub_bin_todo.reset();
+        }
 
         void operator()(bool learned);
 
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void free_memory();
+        void finalize();
 
         void collect_statistics(statistics & st) const;
         void reset_statistics();

src/sat/sat_solver.cpp

@@ -141,7 +141,7 @@ namespace sat {
         m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
         m_assigned_since_gc.push_back(false);
         m_case_split_queue.mk_var_eh(v);
-        m_simplifier.insert_todo(v);
+        m_simplifier.insert_elim_todo(v);
         SASSERT(!was_eliminated(v));
         return v;
     }
@@ -2674,7 +2674,7 @@ namespace sat {
             m_phase.shrink(v);
             m_prev_phase.shrink(v);
             m_assigned_since_gc.shrink(v);
-            m_simplifier.reset_todo();
+            m_simplifier.reset_todos();
         }
     }
 
@@ -3042,7 +3042,7 @@ namespace sat {
         if (scope_lvl() > 0 || inconsistent())
             return;
         m_simplifier(learned);
-        m_simplifier.free_memory();
+        m_simplifier.finalize();
         if (m_ext)
             m_ext->clauses_modifed();
     }

src/sat/sat_solver.h

@@ -237,7 +237,11 @@ namespace sat {
         lbool status(clause const & c) const;        
         clause_offset get_offset(clause const & c) const { return m_cls_allocator.get_offset(&c); }
         void checkpoint() {
-            if (!m_rlimit.inc()) { throw solver_exception(Z3_CANCELED_MSG); }
+            if (!m_rlimit.inc()) {
+                m_mc.reset();
+                m_model_is_current = false;
+                throw solver_exception(Z3_CANCELED_MSG);
+            }
             ++m_num_checkpoints;
             if (m_num_checkpoints < 10) return;
             m_num_checkpoints = 0;

src/sat/sat_types.h

@@ -200,7 +200,7 @@ namespace sat {
         iterator begin() const { return m_set.begin(); }
         iterator end() const { return m_set.end(); }
         void reset() { m_set.reset(); m_in_set.reset(); }
-        void cleanup() { m_set.finalize(); m_in_set.finalize(); }
+        void finalize() { m_set.finalize(); m_in_set.finalize(); }
         uint_set& operator&=(uint_set const& other) {
             unsigned j = 0;
             for (unsigned i = 0; i < m_set.size(); ++i) {
@@ -259,7 +259,7 @@ namespace sat {
         bool empty() const { return m_set.empty(); }
         unsigned size() const { return m_set.size(); }
         void reset() { m_set.reset(); }
-        void cleanup() { m_set.cleanup(); }
+        void finalize() { m_set.finalize(); }
         class iterator {
             uint_set::iterator m_it;
         public: