debugging card

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

src/sat/card_extension.cpp

@@ -234,9 +234,8 @@ namespace sat {
     }
 
     bool card_extension::resolve_conflict(card& c, literal alit) {
-
         bool_var v;
-        m_conflict_lvl = 0;
+        m_conflict_lvl = lvl(~alit);       
         for (unsigned i = c.k(); i < c.size(); ++i) {
             literal lit = c[i];
             SASSERT(value(lit) == l_false);
@@ -245,6 +244,7 @@ namespace sat {
         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;
@@ -351,6 +351,7 @@ namespace sat {
             --m_num_marks;
         }        
         
+        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();
@@ -367,11 +368,13 @@ namespace sat {
         
         ++idx;
         alit = null_literal;
-#if 0
+#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();
-            if (m_active_vars.contains(v)) {
+            if (m_active_var_set.contains(v)) {
                 int coeff = get_coeff(v);
                 bool append = false;
                 if (coeff < 0 && !lit.sign()) {
@@ -394,6 +397,9 @@ namespace sat {
             SASSERT(idx > 0 || slack < 0);
             --idx;
         }
+        if (alit == null_literal) {
+            return false;
+        }
         if (alit != null_literal) {
             m_conflict.push_back(alit);
         }
@@ -402,7 +408,7 @@ namespace sat {
             SASSERT(i <= idx);
             literal lit = lits[i];
             bool_var v = lit.var();
-            if (m_active_vars.contains(v)) {
+            if (m_active_var_set.contains(v)) {
                 int coeff = get_coeff(v);
                 
                 if (coeff < 0 && !lit.sign()) {
@@ -514,6 +520,7 @@ 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);
@@ -530,6 +537,7 @@ namespace sat {
                 }
                 SASSERT(found););
 
+            std::cout << "antecedents: " << idx << ": " << l << " " << c.size() - c.k() + 1 << "\n";            
             r.push_back(c.lit());
             SASSERT(value(c.lit()) == l_true);
             for (unsigned i = c.k(); i < c.size(); ++i) {
@@ -834,6 +842,7 @@ namespace sat {
     // validate that m_A & m_B implies m_C
 
     bool card_extension::validate_resolvent() {
+        std::cout << "validate resolvent\n";
         u_map<unsigned> coeffs;
         unsigned k = m_A.m_k + m_B.m_k;
         for (unsigned i = 0; i < m_A.m_lits.size(); ++i) {

src/sat/sat_solver.cpp

@@ -1726,12 +1726,13 @@ namespace sat {
         m_lemma.push_back(null_literal);
 
         unsigned num_marks = 0;
+        literal consequent = null_literal;
         if (m_not_l != null_literal) {
             TRACE("sat_conflict", tout << "not_l: " << m_not_l << "\n";);
             process_antecedent(m_not_l, num_marks);
+            consequent = ~m_not_l;
         }
 
-        literal consequent = m_not_l; 
         justification js   = m_conflict;
 
         do {
@@ -1900,11 +1901,12 @@ namespace sat {
         }
         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;
         }
-        literal consequent = m_not_l;
         justification js   = m_conflict;
 
         SASSERT(m_trail.size() > 0);
@@ -2008,6 +2010,7 @@ namespace sat {
     }
 
 
+    static int count = 0;
     void solver::resolve_conflict_for_unsat_core() {
         TRACE("sat", display(tout);
               unsigned level = 0;
@@ -2039,6 +2042,7 @@ namespace sat {
         unsigned old_size = m_unmark.size();
         int idx = skip_literals_above_conflict_level();
 
+        literal consequent = m_not_l;
         if (m_not_l != null_literal) {
             justification js = m_justification[m_not_l.var()];
             TRACE("sat", tout << "not_l: " << m_not_l << "\n";
@@ -2052,9 +2056,9 @@ namespace sat {
             else {
                 process_consequent_for_unsat_core(m_not_l, js);
             }
+            consequent = ~m_not_l;
         }
 
-        literal consequent = m_not_l;
         justification js   = m_conflict;
 
         while (true) {
@@ -2093,6 +2097,9 @@ namespace sat {
             set_model(m_mus.get_model());
             IF_VERBOSE(2, verbose_stream() << "(sat.core: " << m_core << ")\n";);
         }
+
+        ++count;
+        SASSERT(count == 1);
     }
 
 
@@ -2116,6 +2123,9 @@ namespace sat {
             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: