expose extension conflict resolution as plugin to sat solver

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

src/sat/card_extension.cpp

@@ -94,7 +94,7 @@ namespace sat {
                     alit = c[j];
                 }
             }
-            set_conflict(c);
+            set_conflict(c, alit);
         }
         else if (j == bound) {
             for (unsigned i = 0; i < bound && !s().inconsistent(); ++i) {
@@ -140,12 +140,24 @@ namespace sat {
         case l_true: 
             break;
         case l_false: 
-            set_conflict(c); 
+            set_conflict(c, lit); 
             break;
         default:
             m_stats.m_num_propagations++;
+            m_num_propagations_since_pop++;
             //TRACE("sat", tout << "#prop: " << m_stats.m_num_propagations << " - " << c.lit() << " => " << lit << "\n";);
             SASSERT(validate_unit_propagation(c));
+            if (s().m_config.m_drat) {
+                svector<drat::premise> ps;
+                literal_vector lits;
+                lits.push_back(~c.lit());
+                for (unsigned i = c.k(); i < c.size(); ++i) {
+                    lits.push_back(c[i]);
+                }
+                lits.push_back(lit);
+                ps.push_back(drat::premise(drat::s_ext(), c.lit()));
+                s().m_drat.add(lits, ps);
+            }
             s().assign(lit, justification::mk_ext_justification(c.index()));
             break;
         }
@@ -163,23 +175,10 @@ namespace sat {
         cards->push_back(&c);
     }
 
-    void card_extension::set_conflict(card& c) {
+    void card_extension::set_conflict(card& c, literal lit) {
         TRACE("sat", display(tout, c, true); );
         SASSERT(validate_conflict(c));
-        m_stats.m_num_conflicts++;
+        s().set_conflict(justification::mk_ext_justification(c.index()), ~lit);
-        literal lit = last_false_literal(c);
-        if (!resolve_conflict(c, lit)) {   
-            TRACE("sat", tout << "bail out conflict resolution\n";);
-            m_conflict.reset();
-            m_conflict.push_back(~c.lit()); 
-            unsigned sz = c.size();
-            for (unsigned i = c.k(); i < sz; ++i) {
-                m_conflict.push_back(c[i]);
-            }
-            m_conflict.push_back(lit);
-            // SASSERT(validate_conflict(m_conflict));
-            s().assign(lit, justification::mk_ext_justification(0));
-        }
         SASSERT(s().inconsistent());
     }
 
@@ -251,6 +250,15 @@ namespace sat {
         else if (coeff0 < 0 && inc > 0) {
             m_bound -= std::min(0, coeff1) - coeff0;
         }
+        // reduce coefficient to be no larger than bound.
+        if (coeff1 > m_bound) {
+            //if (m_bound > 1) std::cout << m_bound << " " << coeff1 << "\n";
+            m_coeffs[v] = m_bound;
+        }
+        else if (coeff1 < 0 && -coeff1 > m_bound) {
+            //if (m_bound > 1) std::cout << m_bound << " " << coeff1 << "\n";
+            m_coeffs[v] = -m_bound;
+        }
     }
 
     int card_extension::get_coeff(bool_var v) const {
@@ -270,100 +278,105 @@ namespace sat {
         m_active_vars.reset();
     }
 
-    bool card_extension::resolve_conflict(card& c, literal alit) {
+    bool card_extension::resolve_conflict() {        
-        bool_var v;
+        if (0 == m_num_propagations_since_pop) 
-        m_conflict_lvl = lvl(~alit);       
-        for (unsigned i = c.k(); i < c.size(); ++i) {
-            literal lit = c[i];
-            SASSERT(value(lit) == l_false);
-            m_conflict_lvl = std::max(m_conflict_lvl, lvl(lit));
-        }
-        if (m_conflict_lvl < lvl(c.lit()) || m_conflict_lvl == 0) {
             return false;
-        }
-        // std::cout << "conflict level: " << m_conflict_lvl << " " << lvl(~alit) << "\n";
-
         reset_coeffs();
         m_num_marks = 0;
-        m_bound = c.k();
+        m_bound = 0;
-        m_conflict.reset();
+        m_lemma.reset();        
+        m_lemma.push_back(null_literal);
+        literal consequent = s().m_not_l;
+        justification js = s().m_conflict;
+        m_conflict_lvl = s().get_max_lvl(consequent, js);
+        if (consequent != null_literal) {
+            consequent.neg();
+            process_antecedent(consequent, 1);
+        }
         literal_vector const& lits = s().m_trail;
         unsigned idx = lits.size()-1;
-        justification js;
+        int offset = 1;
-        literal consequent = ~alit;
-        process_card(c, 1);
 
+        unsigned num_card = 0;
+        unsigned num_steps = 0;
         DEBUG_CODE(active2pb(m_A););
 
-        while (m_num_marks > 0) {
+        do {
-            SASSERT(value(consequent) == l_true);
-            v = consequent.var();
-            int offset = get_abs_coeff(v);
-
             // TRACE("sat", display(tout, m_A););
 
             if (offset == 0) {
                 goto process_next_resolvent;            
             }
-            if (offset > 1000) {
+            // TBD: need proper check for overflow.
+            if (offset > (1 << 12)) {
+                // std::cout << "offset: " << offset << "\n";
                 goto bail_out;
             }
 
-            SASSERT(validate_lemma());
+            ++num_steps;
 
             SASSERT(offset > 0);
+            SASSERT(m_bound >= 0);
 
-            js = s().m_justification[v];
             DEBUG_CODE(justification2pb(js, consequent, offset, m_B););
             
-            int bound = 1;            
             switch(js.get_kind()) {
             case justification::NONE:
-                //std::cout << "NONE\n";
+                SASSERT (consequent != null_literal);
+                m_lemma.push_back(~consequent);
+                m_bound += offset;
                 inc_coeff(consequent, offset);
                 break;
             case justification::BINARY:
-                //std::cout << "BINARY\n";
+                m_bound += offset;
+                SASSERT (consequent != null_literal);
                 inc_coeff(consequent, offset);
-                process_antecedent((js.get_literal()), offset);
+                process_antecedent(js.get_literal(), offset);
                 break;
             case justification::TERNARY:
-                //std::cout << "TERNARY\n";
+                m_bound += offset;
+                SASSERT (consequent != null_literal);
                 inc_coeff(consequent, offset);
-                process_antecedent((js.get_literal1()), offset);
+                process_antecedent(js.get_literal1(), offset);
-                process_antecedent((js.get_literal2()), offset);
+                process_antecedent(js.get_literal2(), offset);
                 break;
             case justification::CLAUSE: {
-                //std::cout << "CLAUSE\n";
+                m_bound += offset;
-                inc_coeff(consequent, offset);
                 clause & c = *(s().m_cls_allocator.get_clause(js.get_clause_offset()));
                 unsigned i = 0;
-                SASSERT(c[0] == consequent || c[1] == consequent);
+                if (consequent != null_literal) {
+                    inc_coeff(consequent, offset);
                     if (c[0] == consequent) {
                         i = 1;
                     }
                     else {
+                        SASSERT(c[1] == consequent);
                         process_antecedent(c[0], offset);
                         i = 2;
                     }
+                }
                 unsigned sz = c.size();
                 for (; i < sz; i++)
                     process_antecedent(c[i], offset);
                 break;
             }
             case justification::EXT_JUSTIFICATION: {
-                //std::cout << "CARDINALITY\n";
+                ++num_card;
                 unsigned index = js.get_ext_justification_idx();
-                card& c2 = *m_constraints[index];
+                card& c = *m_constraints[index];
-                process_card(c2, offset);
+                m_bound += offset * c.k();
-                bound = c2.k();
+                if (!process_card(c, offset)) {
+                    std::cout << "failed to process card\n";
+                    goto bail_out;
+                }
                 break;
             }
             default:
                 UNREACHABLE();
                 break;
             }
-            m_bound += offset * bound;
+            
+            SASSERT(validate_lemma());            
 
             DEBUG_CODE(
                 active2pb(m_C);
@@ -376,6 +389,7 @@ namespace sat {
             
             // find the next marked variable in the assignment stack
             //
+            bool_var v;
             while (true) {
                 consequent = lits[idx];
                 v = consequent.var();
@@ -388,17 +402,20 @@ namespace sat {
             s().reset_mark(v);
             --idx;
             --m_num_marks;
+            js = s().m_justification[v];
+            offset = get_abs_coeff(v);
+            SASSERT(value(consequent) == l_true);
         }        
+        while (m_num_marks > 0);
+
+        std::cout << m_num_propagations_since_pop << " " << num_steps << " " << num_card << "\n";
+        // std::cout << consequent << "\n";
         
         DEBUG_CODE(for (bool_var i = 0; i < static_cast<bool_var>(s().num_vars()); ++i) SASSERT(!s().is_marked(i)););
         SASSERT(validate_lemma());
 
         normalize_active_coeffs();
         
-        if (m_bound > 0 && m_active_vars.empty()) {
-            return false;
-        }
-
         int slack = -m_bound;
         for (unsigned i = 0; i < m_active_vars.size(); ++i) { 
             bool_var v = m_active_vars[i];
@@ -408,10 +425,11 @@ namespace sat {
         TRACE("sat", display(tout, m_A););
         
         ++idx;
-        alit = null_literal;
+        consequent = null_literal;
-#if 1
+
         // std::cout << c.size() << " >= " << c.k() << "\n";
         // std::cout << m_active_vars.size() << ": " << slack + m_bound << " >= " << m_bound << "\n";
+
         while (0 <= slack) {            
             literal lit = lits[idx];
             bool_var v = lit.var();
@@ -427,62 +445,48 @@ namespace sat {
                     append = true;
                 }
                 if (append) {
-                    if (alit == null_literal) {
+                    if (consequent == null_literal) {
-                        alit = ~lit;
+                        consequent = ~lit;
                     }
                     else {
-                        m_conflict.push_back(~lit);
+                        m_lemma.push_back(~lit);
                     }
                 }
             }
             SASSERT(idx > 0 || slack < 0);
             --idx;
         }
-        if (alit == null_literal) {
-            return false;
-        }
-        if (alit != null_literal) {
-            m_conflict.push_back(alit);
-        }
-#else
-        for (unsigned i = 0; 0 <= slack; ++i) {
-            SASSERT(i <= idx);
-            literal lit = lits[i];
-            bool_var v = lit.var();
-            if (m_active_var_set.contains(v)) {
-                int coeff = get_coeff(v);
 
-                if (coeff < 0 && !lit.sign()) {
-                    slack += coeff;
-                    m_conflict.push_back(~lit);
-                }
-                else if (coeff > 0 && lit.sign()) {
-                    slack -= coeff;
-                    m_conflict.push_back(~lit);
-                }
-            }
-        }
-        
-        if (!m_conflict.empty()) {
-            alit = m_conflict.back();
-        }
-#endif
-
-        if (m_conflict.empty()) {
-            IF_VERBOSE(0, verbose_stream() << "(empty conflict)\n";);
-            return false;
-        }
         SASSERT(slack < 0);
-        SASSERT(validate_conflict(m_conflict, m_A));
 
-        TRACE("sat", tout << m_conflict << "\n";);
+        if (consequent == null_literal) {
+            std::cout << "null literal: " << m_lemma.empty() << "\n";
+            if (!m_lemma.empty()) return false;
+        }
+        else {
+            m_lemma[0] = consequent;        
+            SASSERT(validate_conflict(m_lemma, m_A));
+        }
+        TRACE("sat", tout << m_lemma << "\n";);
+
+        if (s().m_config.m_drat) {
+            svector<drat::premise> ps; // TBD fill in
+            s().m_drat.add(m_lemma, ps);
+        }
+
+        // std::cout << m_lemma << "\n";
+        s().m_lemma.reset();
+        s().m_lemma.append(m_lemma);
+        for (unsigned i = 1; i < m_lemma.size(); ++i) {
+            s().mark(m_lemma[i].var());
+        }
+        m_stats.m_num_conflicts++;
 
-        s().assign(alit, justification::mk_ext_justification(0));
         return true;
 
     bail_out:
         while (m_num_marks > 0 && idx > 0) {
-            v = lits[idx].var();
+            bool_var v = lits[idx].var();
             if (s().is_marked(v)) {
                 s().reset_mark(v);
                 --m_num_marks;
@@ -492,7 +496,7 @@ namespace sat {
         return false;
     }
 
-    void card_extension::process_card(card& c, int offset) {
+    bool card_extension::process_card(card& c, int offset) {
         SASSERT(c.k() <= c.size());
         SASSERT(value(c.lit()) == l_true);
         for (unsigned i = c.k(); i < c.size(); ++i) {
@@ -502,8 +506,9 @@ namespace sat {
             inc_coeff(c[i], offset);                        
         }
         if (lvl(c.lit()) > 0) {
-            m_conflict.push_back(~c.lit());
+            m_lemma.push_back(~c.lit());
         }
+        return (lvl(c.lit()) <= m_conflict_lvl);
     }
 
     void card_extension::process_antecedent(literal l, int offset) {
@@ -536,7 +541,6 @@ namespace sat {
 
     card_extension::card_extension(): m_solver(0) {        
         TRACE("sat", tout << this << "\n";);
-        m_constraints.push_back(0); // dummy constraint for conflicts
     }
 
     card_extension::~card_extension() {
@@ -562,15 +566,6 @@ namespace sat {
     }
 
     void card_extension::get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) {
-        if (idx == 0) {
-            // std::cout << "antecedents0: " << l << " " << m_conflict.size() << "\n";
-            SASSERT(m_conflict.back() == l);
-            for (unsigned i = 0; i + 1 < m_conflict.size(); ++i) {
-                SASSERT(value(m_conflict[i]) == l_false);
-                r.push_back(~m_conflict[i]);
-            }
-        }
-        else {
         card& c = *m_constraints[idx];
         
         DEBUG_CODE(
@@ -588,7 +583,6 @@ namespace sat {
             r.push_back(~c[i]);
         }
     }
-    }
 
 
     lbool card_extension::add_assign(card& c, literal alit) {
@@ -626,7 +620,7 @@ namespace sat {
         // conflict
         if (bound != index && value(c[bound]) == l_false) {
             TRACE("sat", tout << "conflict " << c[bound] << " " << alit << "\n";);
-            set_conflict(c);
+            set_conflict(c, alit);
             return l_false;
         }
 
@@ -709,6 +703,7 @@ namespace sat {
             }
         }
         m_var_lim.resize(new_lim);
+        m_num_propagations_since_pop = 0;
     }
 
     void card_extension::simplify() {}
@@ -718,7 +713,6 @@ namespace sat {
     extension* card_extension::copy(solver* s) {
         card_extension* result = alloc(card_extension);
         result->set_solver(s);
-        result->m_constraints.push_back(0);
         for (unsigned i = 1; i < m_constraints.size(); ++i) {
             literal_vector lits;
             card& c = *m_constraints[i];
@@ -795,7 +789,7 @@ namespace sat {
 
     std::ostream& card_extension::display_justification(std::ostream& out, ext_justification_idx idx) const {
         if (idx == 0) {
-            out << "conflict: " << m_conflict;
+            out << "conflict: " << m_lemma;
         }
         else {
             card& c = *m_constraints[idx];
@@ -938,7 +932,7 @@ namespace sat {
             literal lit = m_C.m_lits[i];
             unsigned coeff;
             if (coeffs.find(lit.index(), coeff)) {
-                SASSERT(coeff <= m_C.m_coeffs[i]);
+                SASSERT(coeff <= m_C.m_coeffs[i] || m_C.m_coeffs[i] == m_C.m_k);
                 coeffs.remove(lit.index());
             }
         }

src/sat/card_extension.h

@@ -94,8 +94,9 @@ namespace sat {
         svector<bool_var> m_active_vars;
         int               m_bound;
         tracked_uint_set  m_active_var_set;
-        literal_vector    m_conflict;
+        literal_vector    m_lemma;
         literal_vector    m_literals;
+        unsigned          m_num_propagations_since_pop;
 
         solver& s() const { return *m_solver; }
         void init_watch(card& c, bool is_true);
@@ -103,7 +104,7 @@ namespace sat {
         void assign(card& c, literal lit);
         lbool add_assign(card& c, literal lit);
         void watch_literal(card& c, literal lit);
-        void set_conflict(card& c);
+        void set_conflict(card& c, literal lit);
         literal last_false_literal(card& c);
         void clear_watch(card& c);
         void reset_coeffs();
@@ -122,9 +123,8 @@ namespace sat {
 
         literal_vector& get_literals() { m_literals.reset(); return m_literals; }
         literal get_asserting_literal(literal conseq);
-        bool resolve_conflict(card& c, literal alit);
         void process_antecedent(literal l, int offset);
-        void process_card(card& c, int offset);
+        bool process_card(card& c, int offset);
         void cut();
 
         // validation utilities
@@ -148,6 +148,7 @@ namespace sat {
         virtual void set_solver(solver* s) { m_solver = s; }
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
+        virtual bool resolve_conflict();
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
         virtual void asserted(literal l);
         virtual check_result check();

src/sat/sat_drat.cpp

@@ -52,6 +52,7 @@ namespace sat {
         case drat::status::learned:  return out << "l";
         case drat::status::asserted: return out << "a";
         case drat::status::deleted:  return out << "d";
+        case drat::status::external: return out << "e";
         default: return out;
         }
     }
@@ -60,16 +61,11 @@ namespace sat {
         if (is_cleaned(n, c)) return;
         switch (st) {
         case status::asserted: return;
+        case status::external: return; // requires extension to drat format.
         case status::learned: break;
         case status::deleted: (*m_out) << "d "; break;
         }
-        literal last = null_literal;
+        for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
-        for (unsigned i = 0; i < n; ++i) {
-            if (c[i] != last) {
-                (*m_out) << c[i] << " ";
-                last = c[i];
-            }
-        }
         (*m_out) << "0\n";
     }
 
@@ -186,7 +182,6 @@ namespace sat {
         }
     }
 
-
     void drat::declare(literal l) {
         unsigned n = static_cast<unsigned>(l.var());
         while (m_assignment.size() <= n) {
@@ -196,11 +191,8 @@ namespace sat {
         }
     }
 
-    void drat::verify(unsigned n, literal const* c) {
+    bool drat::is_drup(unsigned n, literal const* c) {
-        if (m_inconsistent) {
+        if (m_inconsistent || n == 0) return true;
-            std::cout << "inconsistent\n";
-            return;
-        }
         unsigned num_units = m_units.size();
         for (unsigned i = 0; !m_inconsistent && i < n; ++i) {            
             assign_propagate(~c[i]);
@@ -211,12 +203,38 @@ namespace sat {
         m_units.resize(num_units);
         bool ok = m_inconsistent;
         m_inconsistent = false;
-        if (ok) {
+        return ok;
+    }
+
+    bool drat::is_drat(unsigned n, literal const* c) {
+        if (m_inconsistent || n == 0) return true;
+        literal l = c[0];
+        literal_vector lits(n - 1, c + 1);
+        for (unsigned i = 0; m_proof.size(); ++i) {
+            status st = m_status[i];
+            if (m_proof[i] && (st == status::asserted || st == status::external)) {
+                clause& c = *m_proof[i];
+                unsigned j = 0;
+                for (; j < c.size() && c[j] != ~l; ++j) {}
+                if (j != c.size()) {
+                    lits.append(j, c.begin());
+                    lits.append(c.size() - j - 1, c.begin() + j + 1);
+                    if (!is_drup(lits.size(), lits.c_ptr())) return false;
+                    lits.resize(n - 1);
+                }
+            }
+        }
+        return true;
+    }
+
+    void drat::verify(unsigned n, literal const* c) {
+        if (is_drup(n, c) || is_drat(n, c)) {
             std::cout << "Verified\n";            
         }
         else {
             std::cout << "Verification failed\n";
             display(std::cout);
+            exit(0);
         }
     }
 
@@ -356,10 +374,17 @@ namespace sat {
         if (m_out) dump(c.size(), c.begin(), st);
         if (s.m_config.m_drat_check) append(c, get_status(learned));
     }
-    void drat::add(unsigned n, literal const* lits, unsigned m, premise * const* premises) {
+    void drat::add(literal_vector const& lits, svector<premise> const& premises) {
         if (s.m_config.m_drat_check) {
-            clause* c = s.m_cls_allocator.mk_clause(n, lits, true);
+            switch (lits.size()) {
+            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);
                 append(*c, status::external);
+                break;
+            }
+            }
         }                        
     }
     void drat::del(literal l) {

src/sat/sat_drat.h

@@ -21,15 +21,22 @@ Notes:
 
 namespace sat {
     class drat {
-        enum status { asserted, learned, deleted, external };
+    public:
-        typedef ptr_vector<clause> watch;
+        struct s_ext {};
+        struct s_unit {};
         struct premise {
             enum { t_clause, t_unit, t_ext } m_type;
-            union evidence {
+            union {
                 clause* m_clause;
                 literal m_literal;                
-            } m_evidence;
             };
+            premise(s_ext, literal l): m_type(t_ext), m_literal(l) {}
+            premise(s_unit, literal l): m_type(t_unit), m_literal(l) {}
+            premise(clause* c): m_type(t_clause), m_clause(c) {}
+        };
+    private:
+        enum status { asserted, learned, deleted, external };
+        typedef ptr_vector<clause> watch;
         solver& s;
         std::ostream*           m_out;
         ptr_vector<clause>      m_proof;
@@ -53,6 +60,8 @@ namespace sat {
         void assign_propagate(literal l);
         void del_watch(clause& c, literal l);
         void verify(unsigned n, literal const* c);
+        bool is_drup(unsigned n, literal const* c);
+        bool is_drat(unsigned n, literal const* c);
         lbool value(literal l) const; 
         void trace(std::ostream& out, unsigned n, literal const* c, status st);
         void display(std::ostream& out) const;
@@ -64,7 +73,7 @@ namespace sat {
         void add(literal l, bool learned);
         void add(literal l1, literal l2, bool learned);
         void add(clause& c, bool learned);
-        void add(unsigned n, literal const* c, unsigned m, premise* const* premises);
+        void add(literal_vector const& c, svector<premise> const& premises);
         
         void del(literal l);
         void del(literal l1, literal l2);

src/sat/sat_extension.h

@@ -37,6 +37,7 @@ namespace sat {
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) = 0;
         virtual void asserted(literal l) = 0;
         virtual check_result check() = 0;
+        virtual bool resolve_conflict() { return false; } // stores result in sat::solver::m_lemma
         virtual void push() = 0;
         virtual void pop(unsigned n) = 0;
         virtual void simplify() = 0;

src/sat/sat_solver.cpp

@@ -1739,11 +1739,17 @@ namespace sat {
             return false;
         }
 
-        m_lemma.reset();
-
         forget_phase_of_vars(m_conflict_lvl);
 
+        if (m_ext && m_ext->resolve_conflict()) {
+            learn_lemma_and_backjump();
+            return true;
+        }
+
+        m_lemma.reset();
+
         unsigned idx = skip_literals_above_conflict_level();
+
         // save space for first uip
         m_lemma.push_back(null_literal);
 
@@ -1820,6 +1826,11 @@ namespace sat {
         while (num_marks > 0);
 
         m_lemma[0] = ~consequent;
+        learn_lemma_and_backjump();
+        return true;
+    }
+
+    void solver::learn_lemma_and_backjump() {
         TRACE("sat_lemma", tout << "new lemma size: " << m_lemma.size() << "\n" << m_lemma << "\n";);
 
         if (m_config.m_minimize_lemmas) {
@@ -1851,7 +1862,6 @@ namespace sat {
         }
         decay_activity();
         updt_phase_counters();
-        return true;
     }
 
     void solver::process_antecedent_for_unsat_core(literal antecedent) {
@@ -1917,122 +1927,6 @@ namespace sat {
         }
     }
 
-    bool solver::resolve_conflict_for_init() {
-        if (m_conflict_lvl == 0) {
-            return false;
-        }
-        m_lemma.reset();
-        m_lemma.push_back(null_literal); // asserted literal
-        literal consequent = null_literal;
-        if (m_not_l != null_literal) {
-            TRACE("sat", tout << "not_l: " << m_not_l << "\n";);
-            process_antecedent_for_init(m_not_l);
-            consequent = ~m_not_l;
-        }
-        justification js   = m_conflict;
-
-        SASSERT(m_trail.size() > 0);
-        unsigned idx = m_trail.size();
-        while (process_consequent_for_init(consequent, js)) {
-            while (true) {
-                --idx;
-                literal l = m_trail[idx];
-                if (is_marked(l.var()))
-                    break;
-                SASSERT(idx > 0);
-            }
-            consequent     = m_trail[idx];
-            bool_var c_var = consequent.var();
-            if (lvl(consequent) == 0) {
-                return false;
-            }
-            SASSERT(m_conflict_lvl == 1);
-            js = m_justification[c_var];
-            reset_mark(c_var);
-        }
-
-        unsigned new_scope_lvl = 0;
-        m_lemma[0] = ~consequent;
-        for (unsigned i = 1; i < m_lemma.size(); ++i) {
-            bool_var var = m_lemma[i].var();
-            if (is_marked(var)) {
-                reset_mark(var);
-                new_scope_lvl = std::max(new_scope_lvl, lvl(var));
-            }
-            else {
-                m_lemma[i] = m_lemma.back();
-                m_lemma.pop_back();
-                --i;
-            }
-        }
-        TRACE("sat", tout << "lemma: " << m_lemma << "\n"; display(tout); tout << "assignment:\n"; display_assignment(tout););
-        if (new_scope_lvl == 0) {
-            pop_reinit(m_scope_lvl);
-        }
-        else {
-            unassign_vars(idx);
-        }
-        mk_clause_core(m_lemma.size(), m_lemma.c_ptr(), true);
-        TRACE("sat", tout << "Trail: " << m_trail << "\n";);
-        m_inconsistent = false;
-        return true;
-    }
-
-    bool solver::process_consequent_for_init(literal consequent, justification const& js) {
-        switch (js.get_kind()) {
-        case justification::NONE:
-            return false;
-        case justification::BINARY:
-            process_antecedent_for_init(~(js.get_literal()));
-            break;
-        case justification::TERNARY:
-            process_antecedent_for_init(~(js.get_literal1()));
-            process_antecedent_for_init(~(js.get_literal2()));
-            break;
-        case justification::CLAUSE: {
-            clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
-            unsigned i   = 0;
-            if (consequent != null_literal) {
-                SASSERT(c[0] == consequent || c[1] == consequent);
-                if (c[0] == consequent) {
-                    i = 1;
-                }
-                else {
-                    process_antecedent_for_init(~c[0]);
-                    i = 2;
-                }
-            }
-            unsigned sz  = c.size();
-            for (; i < sz; i++)
-                process_antecedent_for_init(~c[i]);
-            break;
-        }
-        case justification::EXT_JUSTIFICATION: {
-            fill_ext_antecedents(consequent, js);
-            literal_vector::iterator it  = m_ext_antecedents.begin();
-            literal_vector::iterator end = m_ext_antecedents.end();
-            for (; it != end; ++it)
-                process_antecedent_for_init(*it);
-            break;
-        }
-        default:
-            UNREACHABLE();
-            break;
-        }
-        return true;
-    }
-
-    void solver::process_antecedent_for_init(literal antecedent) {
-        bool_var var     = antecedent.var();
-        SASSERT(var < num_vars());
-        if (!is_marked(var) && lvl(var) > 0) {
-            mark(var);
-            m_lemma.push_back(~antecedent);
-        }
-    }
-
-
-    static int count = 0;
     void solver::resolve_conflict_for_unsat_core() {
         TRACE("sat", display(tout);
               unsigned level = 0;
@@ -2080,10 +1974,6 @@ namespace sat {
             }
             consequent = ~m_not_l;
         }
-        std::cout << "CONFLICT: " << m_core << "\n";
-        display_status(std::cout);
-        ++count;
-        exit(0);
 
         justification js = m_conflict;
 
@@ -2140,16 +2030,13 @@ namespace sat {
         }
         case justification::EXT_JUSTIFICATION: {
             unsigned r = 0;
-            if (not_l != null_literal)
+            SASSERT(not_l != null_literal);
-                r = lvl(~not_l);
+            r = lvl(not_l);
             fill_ext_antecedents(~not_l, js);
             literal_vector::iterator it  = m_ext_antecedents.begin();
             literal_vector::iterator end = m_ext_antecedents.end();
             for (; it != end; ++it)
                 r = std::max(r, lvl(*it));
-            if (true || r != scope_lvl() || r != lvl(not_l)) {
-                // std::cout << "get max level " << r << " scope level " << scope_lvl() << " lvl(l): " << lvl(not_l) << "\n";
-            }
             return r;
         }
         default:

src/sat/sat_solver.h

@@ -378,14 +378,12 @@ namespace sat {
         literal_vector m_ext_antecedents;
         bool resolve_conflict();
         bool resolve_conflict_core();
+        void learn_lemma_and_backjump();
         unsigned get_max_lvl(literal consequent, justification js);
         void process_antecedent(literal antecedent, unsigned & num_marks);
         void resolve_conflict_for_unsat_core();
         void process_antecedent_for_unsat_core(literal antecedent);
         void process_consequent_for_unsat_core(literal consequent, justification const& js);
-        bool resolve_conflict_for_init();
-        void process_antecedent_for_init(literal antecedent);
-        bool process_consequent_for_init(literal consequent, justification const& js);
         void fill_ext_antecedents(literal consequent, justification js);
         unsigned skip_literals_above_conflict_level();
         void forget_phase_of_vars(unsigned from_lvl);

src/sat/sat_types.h

@@ -138,6 +138,7 @@ namespace sat {
 
     typedef svector<lbool> model;
 
+    inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
     inline lbool value_at(bool_var v, model const & m) { return m[v]; }
     inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; }
 

src/smt/theory_pb.cpp

@@ -811,7 +811,7 @@ namespace smt {
         }
 
         if (bound == c->size() || bound == 1) {
-            std::cout << "is-clause\n";
+            //
         }
         
         if (bound == c->size()) {
@@ -1827,11 +1827,11 @@ namespace smt {
         lbool is_sat = k.check();
         validating = false;
         std::cout << is_sat << "\n";
-        if (is_sat != l_false) {
+        if (is_sat == l_true) {
             std::cout << A << "\n";
             std::cout << B << "\n";
         }
-        SASSERT(is_sat == l_false);
+        SASSERT(is_sat != l_true);
         return true;
     }