adding elim sequences

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

src/sat/sat_model_converter.cpp

@@ -49,16 +49,35 @@ namespace sat {
             // and the following procedure flips its value.
             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;
                     }
                     sat = false;
+                    ++index;
                     continue;
                 }
+                prev = l;
 
                 if (sat)
                     continue;
@@ -136,15 +155,17 @@ namespace sat {
         return e;
     }
 
-    void model_converter::insert(entry & e, clause const & c) {
+    void model_converter::insert(entry & e, clause const & c, elim_sequence* s) {
         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);
         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);
@@ -152,6 +173,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);
         TRACE("sat_mc_bug", tout << "adding (binary): " << l1 << " " << l2 << "\n";);
     }
 
@@ -163,6 +185,7 @@ 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);
         // TRACE("sat_mc_bug", tout << "adding (wrapper): "; for (literal l : c) tout << l << " "; tout << "\n";);
     }
 

src/sat/sat_model_converter.h

@@ -20,6 +20,7 @@ Revision History:
 #define SAT_MODEL_CONVERTER_H_
 
 #include "sat/sat_types.h"
+#include "util/ref_vector.h"
 
 namespace sat {
     /**
@@ -36,19 +37,40 @@ namespace sat {
        it can be converted into a general Z3 model_converter
     */
     class model_converter {
+        
     public:
+        class elim_sequence {
+            unsigned       m_refcount;
+            elim_sequence* m_next;
+            literal        m_literal;
+            literal_vector m_clause;
+        public:
+            elim_sequence(literal l, literal_vector const& clause, elim_sequence* next): 
+                m_refcount(0), 
+                m_next(next),
+                m_literal(l),
+                m_clause(clause) {
+                if (m_next) m_next->inc_ref();
+            }
+            ~elim_sequence() { if (m_next) m_next->dec_ref(); }
+            void inc_ref() { ++m_refcount; }
+            void dec_ref() { if (0 == --m_refcount) dealloc(this); }
+        };
+
         enum kind { ELIM_VAR = 0, BLOCK_LIT };
         class entry {
             friend class model_converter;
             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;
             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_clauses(src.m_clauses),
+                m_elim_sequence(src.m_elim_sequence) {
             }
             bool_var var() const { return m_var; }
             kind get_kind() const { return static_cast<kind>(m_kind); }
@@ -62,7 +84,7 @@ namespace sat {
         model_converter& operator=(model_converter const& other);
 
         entry & mk(kind k, bool_var v);
-        void insert(entry & e, clause const & c);
+        void insert(entry & e, clause const & c, elim_sequence* s = nullptr);
         void insert(entry & e, literal l1, literal l2);
         void insert(entry & e, clause_wrapper const & c);