model conversion and acce tracking

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

src/ackermannization/ackermannize_bv_tactic.cpp

@@ -52,7 +52,7 @@ public:
         result.push_back(resg.get());
         // report model
         if (g->models_enabled()) {
-            g->add(mk_ackermannize_bv_model_converter(m, lackr.get_info()));
+            resg->add(mk_ackermannize_bv_model_converter(m, lackr.get_info()));
         }
         
         resg->inc_depth();

src/sat/sat_asymm_branch.cpp

@@ -333,13 +333,18 @@ namespace sat {
         if (!m_to_delete.empty()) {
             unsigned j = 0;
             for (unsigned i = 0; i < c.size(); ++i) {
-                if (!m_to_delete.contains(c[i])) {
+                literal lit = c[i];
-                    c[j] = c[i];
+                switch (s.value(lit)) {
-                    ++j;
+                case l_true:
+                    scoped_d.del_clause();
+                    return false;
+                case l_false:    
+                    break;
+                default:
+                    if (!m_to_delete.contains(lit)) {
+                        c[j++] = lit;
                     }
-                else {
+                    break;
-                    m_pos.erase(c[i]);
-                    m_neg.erase(~c[i]);
                 }
             }
             return re_attach(scoped_d, c, j);
@@ -359,6 +364,7 @@ namespace sat {
     }
 
     bool asymm_branch::flip_literal_at(clause const& c, unsigned flip_index, unsigned& new_sz) {
+        VERIFY(s.m_trail.size() == s.m_qhead);
         bool found_conflict = false;
         unsigned i = 0, sz = c.size();        
         s.push();
@@ -399,6 +405,7 @@ namespace sat {
     }
 
     bool asymm_branch::re_attach(scoped_detach& scoped_d, clause& c, unsigned new_sz) {
+        VERIFY(s.m_trail.size() == s.m_qhead);
         m_elim_literals += c.size() - new_sz;
         if (c.is_learned()) {
             m_elim_learned_literals += c.size() - new_sz; 
@@ -415,6 +422,7 @@ namespace sat {
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
+            VERIFY(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
             s.mk_bin_clause(c[0], c[1], c.is_learned());
             if (s.m_trail.size() > s.m_qhead) s.propagate_core(false);
             scoped_d.del_clause();

src/sat/sat_model_converter.cpp

@@ -75,7 +75,7 @@ namespace sat {
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
         vector<entry>::const_iterator it    = m_entries.end();
-        bool first = true;
+        bool first = false; // true;
         //SASSERT(!m_solver || m_solver->check_clauses(m));
         while (it != begin) {
             --it;
@@ -99,8 +99,8 @@ namespace sat {
                         process_stack(m, clause, st->stack());
                     }
                     sat = false;
-                    if (false && first && m_solver && !m_solver->check_clauses(m)) {
+                    if (first && m_solver && !m_solver->check_clauses(m)) {
-                        display(std::cout, *it) << "\n";
+                        IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n");
                         first = false;
                     }
                     ++index;
@@ -125,8 +125,8 @@ namespace sat {
                     m[v] = sign ? l_false : l_true;
                     // if (first) std::cout << "set: " << l << "\n";
                     sat = true;
-                    if (false && first && m_solver && !m_solver->check_clauses(m)) {
+                    if (first && m_solver && !m_solver->check_clauses(m)) {
-                        display(std::cout, *it)  << "\n";;
+                        IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it)  << "\n");
                         first = false;
                     }
                 }

src/sat/sat_simplifier.cpp

@@ -939,6 +939,19 @@ namespace sat {
             bool operator==(clause_ante const& a) const {
                 return a.m_lit1 == m_lit1 && a.m_lit2 == m_lit2 && a.m_clause == m_clause;
             }
+            std::ostream& display(std::ostream& out) const {
+                if (cls()) {
+                    out << *cls() << " ";
+                }
+                if (lit1() != null_literal) {
+                    out << lit1() << " ";
+                }
+                if (lit2() != null_literal) {
+                    out << lit2() << " ";
+                }
+                out << "\n";
+                return out;
+            }
         };
 
         class queue {
@@ -1154,10 +1167,14 @@ namespace sat {
            \brief idx is the index of the blocked literal.
            m_tautology contains literals that were used to establish that the current members of m_covered_clause is blocked.
            This routine removes literals that were not relevant to establishing it was blocked.
+
+           It has a bug: literals that are used to prune tautologies during resolution intersection should be included
+           in the dependencies.
          */
         void minimize_covered_clause(unsigned idx) {
             // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause 
             // << " @ " << idx << "\n" << "tautology: " << m_tautology << "\n";);
+            literal _blocked = m_covered_clause[idx];
             for (literal l : m_tautology) VERIFY(s.is_marked(l));
             for (literal l : m_covered_clause) s.unmark_visited(l);
             for (literal l : m_tautology) s.mark_visited(l);
@@ -1167,8 +1184,18 @@ namespace sat {
                 if (m_covered_antecedent[i] == clause_ante()) s.mark_visited(lit);
                 if (s.is_marked(lit)) idx = i; 
             }
+            if (_blocked.var() == 16774 && false) {
+                IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n";
+                           verbose_stream() << "tautology: " << m_tautology << "\n";
+                           verbose_stream() << "index: " << idx << "\n";
+                           for (unsigned i = idx; i > 0; --i) {
+                               m_covered_antecedent[i].display(verbose_stream() << "ante " << m_covered_clause[i] << ":");
+                           });
+            }
             for (unsigned i = idx; i > 0; --i) {
                 literal lit = m_covered_clause[i];
+                s.mark_visited(lit);
+                continue;
                 if (!s.is_marked(lit)) continue;
                 clause_ante const& ante = m_covered_antecedent[i];
                 if (ante.cls()) {
@@ -1205,6 +1232,9 @@ namespace sat {
             // unsigned sz0 = m_covered_clause.size();
             m_covered_clause.resize(j);
             VERIFY(j >= m_clause.size());
+            if (_blocked.var() == 16774 && false) {
+                IF_VERBOSE(0, verbose_stream() << "covered: " << m_covered_clause << "\n");
+            }
             // IF_VERBOSE(0, verbose_stream() << "reduced from size " << sz0 << " to " << m_covered_clause << "\n" << m_clause << "\n";);
         }
 
@@ -1531,13 +1561,10 @@ namespace sat {
                 return;
             }
             for (literal l2 : m_intersection) {
-                l2.neg();
+                watched* w = find_binary_watch(s.get_wlist(~l), ~l2);
-                watched* w = find_binary_watch(s.get_wlist(~l), l2);
                 if (!w) {
-                    IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
+                    IF_VERBOSE(10, verbose_stream() << "bca " << l << " " << ~l2 << "\n";);
-                    s.get_wlist(~l).push_back(watched(l2, true));
+                    s.s.mk_bin_clause(l, ~l2, true);
-                    VERIFY(!find_binary_watch(s.get_wlist(~l2), l));
-                    s.get_wlist(~l2).push_back(watched(l, true));
                     ++s.m_num_bca;
                 }
             }
@@ -1997,7 +2024,7 @@ namespace sat {
         sat_simplifier_params p(_p);
         m_cce                     = p.cce();
         m_acce                    = p.acce();
-        m_bca                     = p.bca();
+        m_bca                     = false && p.bca(); // disabled
         m_abce                    = p.abce();
         m_ate                     = p.ate();
         m_bce_delay               = p.bce_delay();

src/sat/sat_solver.cpp

@@ -333,6 +333,13 @@ namespace sat {
     }
 
     void solver::mk_bin_clause(literal l1, literal l2, bool learned) {
+#if 0
+        if ((l1 == literal(5981, false) && l2 == literal(16764, false)) ||
+            (l2 == literal(5981, false) && l1 == literal(16764, false))) {
+            IF_VERBOSE(0, display(verbose_stream()));
+            //VERIFY(false);
+        }
+#endif
         if (find_binary_watch(get_wlist(~l1), ~l2)) {
             assign(l1, justification());
             return;
@@ -1656,6 +1663,7 @@ namespace sat {
         
         if (!check_clauses(m_model)) {
             IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
+            IF_VERBOSE(10, m_mc.display(verbose_stream()));
             throw solver_exception("check model failed");
         }
 

src/tactic/goal.cpp

@@ -85,6 +85,9 @@ goal::goal(goal const & src, bool):
     m_core_enabled(src.unsat_core_enabled()),
     m_inconsistent(false),
     m_precision(src.m_precision) {
+    m_mc = src.m_mc.get();
+    m_pc = src.m_pc.get();
+    m_dc = src.m_dc.get();
 }
 
 goal::~goal() {