add elimination stack for model reconstruction

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

src/sat/sat_bdd.cpp

@@ -239,9 +239,53 @@ namespace sat {
         // TBD
     }
 
-    void bdd_manager::sift_up(unsigned level) {
+    void bdd_manager::sift_up(unsigned lvl) {
         // exchange level and level + 1.
+#if 0
+        m_relevel.reset(); // nodes to be re-leveled.
 
+        for (unsigned n : m_level2nodes[lvl + 1]) {
+            BDD l = lo(n);
+            BDD h = hi(n);
+            if (l == 0 && h == 0) continue;
+            BDD a, b, c, d;
+            if (level(l) == lvl) {
+                a = lo(l);
+                b = hi(l);
+            }
+            else {
+                a = b = l;
+            }
+            if (level(h) == lvl) {
+                c = lo(h);
+                d = hi(h);
+            }
+            else {
+                c = d = h;
+            }
+
+            push(make_node(lvl, a, c));
+            push(make_node(lvl, b, d));
+            m_node_table.remove(m_nodes[n]);
+            m_nodes[n].m_lo = read(2);
+            m_nodes[n].m_hi = read(1);
+            m_relevel.push_back(l);
+            m_relevel.push_back(r);
+            // TBD: read(2); read(1); should be inserted into m_level2nodes[lvl];
+            pop(2);
+            m_node_table.insert(m_nodes[n]);
+        }
+        unsigned v = m_level2var[lvl];
+        unsigned w = m_level2var[lvl+1];
+        std::swap(m_level2var[lvl], m_level2var[lvl+1]);
+        std::swap(m_var2level[v], m_var2level[w]);
+        for (unsigned n : m_relevel) {
+            if (level(n) == lvl) {
+                // whoever points to n uses it as if it is level lvl + 1.
+                m_level2nodes[m_node2levelpos[n]];
+            }
+        }
+#endif
     }
 
     bdd bdd_manager::mk_var(unsigned i) {
@@ -454,9 +498,14 @@ namespace sat {
         }
         for (unsigned i = m_nodes.size(); i-- > 2; ) {
             if (!reachable[i]) {
+                m_nodes[i].m_lo = m_nodes[i].m_hi = 0;
                 m_free_nodes.push_back(i);                
             }
         }
+        // sort free nodes so that adjacent nodes are picked in order of use
+        std::sort(m_free_nodes.begin(), m_free_nodes.end());
+        m_free_nodes.reverse();
+
         for (auto* e : m_op_cache) {
             m_alloc.deallocate(sizeof(*e), e);
         }

src/sat/sat_model_converter.cpp

@@ -38,6 +38,22 @@ namespace sat {
         return *this;
     }
 
+    void model_converter::process_stack(model & m, literal_vector const& stack) const {
+        SASSERT(!stack.empty());
+        unsigned sz = stack.size();
+        SASSERT(stack[sz - 1] == null_literal);
+        for (unsigned i = sz - 1; i-- > 0; ) {
+            literal lit = stack[i]; // this is the literal that is pivoted on. It is repeated
+            bool sat = false;
+            for (; i > 0 && stack[--i] != null_literal;) {
+                if (sat) continue;
+                sat = value_at(stack[i], m) == l_true;
+            }
+            if (!sat) {
+                m[lit.var()] = lit.sign() ? l_false : l_true;
+            }
+        }
+    }
     
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
@@ -50,34 +66,20 @@ namespace sat {
             bool sat = false;
             bool var_sign = false;
             unsigned index = 0;
-            literal prev = null_literal;
             for (literal l : it->m_clauses) {
                 if (l == null_literal) {
                     // end of clause
-                    if (!sat && it->m_elim_sequence[index]) {
-                        SASSERT(prev != null_literal);
-                        m[prev.var()] = prev.sign() ? l_false : l_true;
-                        elim_sequence* s = it->m_elim_sequence[index];
-#if 0
-                        while (!sat) {
-                            SASSERT(s);
-                            for (literal l2 : s->clause()) {
-                                sat = value_at(l2, m) == l_true;
-                            }
-                            s->clause();
-                        }
-#endif
-                        NOT_IMPLEMENTED_YET();
-                    }
                     if (!sat) {
                         m[it->var()] = var_sign ? l_false : l_true;
-                        break;
+                    }
+                    elim_stack* s = it->m_elim_stack[index];
+                    if (s) {
+                        process_stack(m, s->stack());
                     }
                     sat = false;
                     ++index;
                     continue;                    
                 }
-                prev = l;
 
                 if (sat)
                     continue;
@@ -155,17 +157,16 @@ namespace sat {
         return e;
     }
 
-    void model_converter::insert(entry & e, clause const & c, elim_sequence* s) {
+    void model_converter::insert(entry & e, clause const & c) {
         SASSERT(c.contains(e.var()));
         SASSERT(m_entries.begin() <= &e);
         SASSERT(&e < m_entries.end());
         for (literal l : c) e.m_clauses.push_back(l);
         e.m_clauses.push_back(null_literal);
-        e.m_elim_sequence.push_back(s);
+        e.m_elim_stack.push_back(nullptr);
         TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
     }
 
-
     void model_converter::insert(entry & e, literal l1, literal l2) {
         SASSERT(l1.var() == e.var() || l2.var() == e.var());
         SASSERT(m_entries.begin() <= &e);
@@ -173,7 +174,7 @@ namespace sat {
         e.m_clauses.push_back(l1);
         e.m_clauses.push_back(l2);
         e.m_clauses.push_back(null_literal);
-        e.m_elim_sequence.push_back(nullptr);
+        e.m_elim_stack.push_back(nullptr);
         TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";);
     }
 
@@ -185,10 +186,21 @@ namespace sat {
         for (unsigned i = 0; i < sz; ++i) 
             e.m_clauses.push_back(c[i]);
         e.m_clauses.push_back(null_literal);
-        e.m_elim_sequence.push_back(nullptr);
+        e.m_elim_stack.push_back(nullptr);
         // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
     }
 
+    void model_converter::insert(entry & e, literal_vector const& c, literal_vector const& elims) {
+        SASSERT(c.contains(literal(e.var(), false)) || c.contains(literal(e.var(), true)));
+        SASSERT(m_entries.begin() <= &e);
+        SASSERT(&e < m_entries.end());
+        for (literal l : c) e.m_clauses.push_back(l);
+        e.m_clauses.push_back(null_literal);
+        e.m_elim_stack.push_back(alloc(elim_stack, elims));
+        TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
+    }
+
+
     bool model_converter::check_invariant(unsigned num_vars) const {
         // After a variable v occurs in an entry n and the entry has kind ELIM_VAR,
         // then the variable must not occur in any other entry occurring after it.

src/sat/sat_model_converter.h

@@ -39,22 +39,18 @@ namespace sat {
     class model_converter {
         
     public:
-        class elim_sequence {
+        class elim_stack {
             unsigned       m_refcount;
-            elim_sequence* m_next;
+            literal_vector m_stack;
-            literal        m_literal;
-            literal_vector m_clause;
         public:
-            elim_sequence(literal l, literal_vector const& clause, elim_sequence* next): 
+            elim_stack(literal_vector const& stack): 
                 m_refcount(0), 
-                m_next(next),
+                m_stack(stack) {
-                m_literal(l),
-                m_clause(clause) {
-                if (m_next) m_next->inc_ref();
             }
-            ~elim_sequence() { if (m_next) m_next->dec_ref(); }
+            ~elim_stack() { }
             void inc_ref() { ++m_refcount; }
             void dec_ref() { if (0 == --m_refcount) dealloc(this); }
+            literal_vector const& stack() const { return m_stack; }
         };
 
         enum kind { ELIM_VAR = 0, BLOCK_LIT };
@@ -63,20 +59,23 @@ namespace sat {
             unsigned           m_var:31;
             unsigned           m_kind:1;
             literal_vector     m_clauses; // the different clauses are separated by null_literal
-            sref_vector<elim_sequence>  m_elim_sequence;
+            sref_vector<elim_stack>  m_elim_stack;
             entry(kind k, bool_var v):m_var(v), m_kind(k) {}
         public:
             entry(entry const & src):
                 m_var(src.m_var),
                 m_kind(src.m_kind),
                 m_clauses(src.m_clauses),
-                m_elim_sequence(src.m_elim_sequence) {
+                m_elim_stack(src.m_elim_stack) {
             }
             bool_var var() const { return m_var; }
             kind get_kind() const { return static_cast<kind>(m_kind); }
         };
     private:
         vector<entry>          m_entries;
+
+        void process_stack(model & m, literal_vector const& stack) const;
+
     public:
         model_converter();
         ~model_converter();
@@ -84,9 +83,10 @@ namespace sat {
         model_converter& operator=(model_converter const& other);
 
         entry & mk(kind k, bool_var v);
-        void insert(entry & e, clause const & c, elim_sequence* s = nullptr);
+        void insert(entry & e, clause const & c);
         void insert(entry & e, literal l1, literal l2);
         void insert(entry & e, clause_wrapper const & c);
+        void insert(entry & c, literal_vector const& covered_clause, literal_vector const& elim_stack);
 
         bool empty() const { return m_entries.empty(); }
 

src/sat/sat_simplifier.cpp

@@ -1025,34 +1025,39 @@ namespace sat {
             return first;
         }
 
-        literal_vector m_added;
+        literal_vector m_covered_clause;
         literal_vector m_intersection;
+        literal_vector m_elim_stack;
 
         bool cla(literal lit) {
             bool is_tautology = false;
-            for (literal l : m_added) s.mark_visited(l);
+            for (literal l : m_covered_clause) s.mark_visited(l);
             unsigned num_iterations = 0, sz;
+            m_elim_stack.reset();
             do {
                 ++num_iterations;
-                sz = m_added.size();
+                sz = m_covered_clause.size();
-                for (unsigned i = 0; i < m_added.size(); ++i) {
+                for (unsigned i = 0; i < m_covered_clause.size(); ++i) {
-                    if (ri(m_added[i], m_intersection) && m_added[i] == lit) {
+                    m_intersection.reset();
+                    if (ri(m_covered_clause[i], m_intersection) && m_covered_clause[i] == lit) {
                         is_tautology = true;
                         break;
                     }
                     for (literal l : m_intersection) {
                         if (!s.is_marked(l)) {
                             s.mark_visited(l);
-                            m_added.push_back(l);
+                            m_covered_clause.push_back(l);
                         }
                     }
-                    m_intersection.reset();
+                    if (!m_intersection.empty()) {
+                        m_elim_stack.append(m_covered_clause);           // the current clause
+                        m_elim_stack.push_back(m_covered_clause[i]);     // the pivot literal
+                        m_elim_stack.push_back(null_literal);   // null demarcation
                     }
                 }
-            while (m_added.size() > sz && !is_tautology);
+            }
-            for (literal l : m_added) s.unmark_visited(l);
+            while (m_covered_clause.size() > sz && !is_tautology);
-            m_intersection.reset();
+            for (literal l : m_covered_clause) s.unmark_visited(l);
-            m_added.reset();
             if (is_tautology) std::cout << "taut: " << num_iterations << "\n";
             return is_tautology;
         }
@@ -1061,13 +1066,15 @@ namespace sat {
         // first extract the covered literal addition (CLA).
         // then check whether the CLA is blocked.
         bool cce(clause& c, literal lit) {
-            for (literal l : c) m_added.push_back(l);
+            m_covered_clause.reset();
+            for (literal l : c) m_covered_clause.push_back(l);
             return cla(lit);
         }
 
         bool cce(literal lit, literal l2) {
-            m_added.push_back(lit);
+            m_covered_clause.reset();
-            m_added.push_back(l2);
+            m_covered_clause.push_back(lit);
+            m_covered_clause.push_back(l2);
             return cla(lit);            
         }
 
@@ -1093,7 +1100,7 @@ namespace sat {
                         s.m_num_blocked_clauses++;
                     }
                     else if (cce(c, l)) {
-                        block_clause(c, l, new_entry);
+                        block_covered_clause(c, l, new_entry);
                         s.m_num_covered_clauses++;                        
                     }
                     it.next();
@@ -1121,7 +1128,7 @@ namespace sat {
                         s.m_num_blocked_clauses++;
                     }
                     else if (cce(l, l2)) {
-                        block_binary(it, l, new_entry);
+                        block_covered_binary(it, l, new_entry);
                         s.m_num_covered_clauses++;
                     }
                     else {
@@ -1134,12 +1141,11 @@ namespace sat {
             }
         }
 
-        void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+        void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry) {
             TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
             if (new_entry == 0)
                 new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
             m_to_remove.push_back(&c);
-            mc.insert(*new_entry, c);
             for (literal lit : c) {
                 if (lit != l && process_var(lit.var())) {
                     m_queue.decreased(~lit);
@@ -1147,14 +1153,33 @@ namespace sat {
             }
         }
 
-        void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+        void block_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            prepare_block_clause(c, l, new_entry);
+            mc.insert(*new_entry, c);
+        }
+
+        void block_covered_clause(clause& c, literal l, model_converter::entry *& new_entry) {
+            prepare_block_clause(c, l, new_entry);
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
+        }
+        
+        void prepare_block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
             if (new_entry == 0)
                 new_entry = &(mc.mk(model_converter::BLOCK_LIT, l.var()));
             literal l2 = it->get_literal();
             TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l << "\n";);
             s.remove_bin_clause_half(l2, l, it->is_learned());
             m_queue.decreased(~l2);
-            mc.insert(*new_entry, l, l2);
+        }
+
+        void block_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+            prepare_block_binary(it, l, new_entry);
+            mc.insert(*new_entry, l, it->get_literal());
+        }
+
+        void block_covered_binary(watch_list::iterator it, literal l, model_converter::entry *& new_entry) {
+            prepare_block_binary(it, l, new_entry);
+            mc.insert(*new_entry, m_covered_clause, m_elim_stack);
         }
 
         bool all_tautology(literal l) {