add checks for flipping externals / assumptions in model converter, fix scc converter bug

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

src/sat/sat_elim_eqs.cpp

@@ -182,7 +182,7 @@ namespace sat {
             literal  l(v, false);
             literal r  = roots[v];
             SASSERT(v != r.var());
-            if (m_solver.is_external(v) && !m_solver.set_root(l, r)) {
+            if (m_solver.is_external(v) || !m_solver.set_root(l, r)) {
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 m_solver.mk_bin_clause(~l, r, false);
                 m_solver.mk_bin_clause(l, ~r, false);

src/sat/sat_model_converter.cpp

@@ -39,6 +39,22 @@ namespace sat {
         return *this;
     }
 
+    bool model_converter::legal_to_flip(bool_var v) const {
+        // std::cout << "check " << v << " " << m_solver << "\n";
+        if (m_solver && m_solver->is_assumption(v)) {
+            std::cout << "flipping assumption v" << v << "\n";
+            UNREACHABLE();
+            throw solver_exception("flipping assumption");
+        }
+        if (m_solver && m_solver->is_external(v)) {
+            std::cout << "flipping external v" << v << "\n";
+            UNREACHABLE();
+            throw solver_exception("flipping external");
+        }
+        return !m_solver || !m_solver->is_assumption(v);
+    }
+
+
     void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const {
         SASSERT(!stack.empty());
         unsigned sz = stack.size();
@@ -50,6 +66,7 @@ namespace sat {
                 sat = value_at(c[j], m) == l_true;
             }
             if (!sat) {
+                VERIFY(legal_to_flip(lit.var()));
                 m[lit.var()] = lit.sign() ? l_false : l_true;
             }
         }
@@ -59,7 +76,7 @@ namespace sat {
         vector<entry>::const_iterator begin = m_entries.begin();
         vector<entry>::const_iterator it    = m_entries.end();
         bool first = true;
-        //VERIFY(!m_solver || m_solver->check_clauses(m));
+        //SASSERT(!m_solver || m_solver->check_clauses(m));
         while (it != begin) {
             --it;
             SASSERT(it->get_kind() != ELIM_VAR || m[it->var()] == l_undef);
@@ -69,11 +86,13 @@ namespace sat {
             bool var_sign = false;
             unsigned index = 0;
             literal_vector clause;
+            VERIFY(legal_to_flip(it->var()));
             for (literal l : it->m_clauses) {
                 if (l == null_literal) {
                     // end of clause
                     elim_stack* st = it->m_elim_stack[index];
-                    if (!sat) {                        
+                    if (!sat) {     
+                        VERIFY(legal_to_flip(it->var()));                        
                         m[it->var()] = var_sign ? l_false : l_true;
                     }
                     if (st) {
@@ -101,6 +120,7 @@ namespace sat {
                 if (value_at(l, m) == l_true)
                     sat = true;
                 else if (!sat && v != it->var() && m[v] == l_undef) {
+                    VERIFY(legal_to_flip(v));
                     // clause can be satisfied by assigning v.
                     m[v] = sign ? l_false : l_true;
                     // if (first) std::cout << "set: " << l << "\n";
@@ -170,6 +190,7 @@ namespace sat {
         entry & e = m_entries.back();
         SASSERT(e.var() == v);
         SASSERT(e.get_kind() == k);
+        VERIFY(legal_to_flip(v));
         return e;
     }
 
@@ -213,6 +234,7 @@ namespace sat {
         for (literal l : c) e.m_clauses.push_back(l);
         e.m_clauses.push_back(null_literal);
         e.m_elim_stack.push_back(elims.empty() ? nullptr : alloc(elim_stack, elims));
+        for (auto const& s : elims) VERIFY(legal_to_flip(s.second.var()));
         TRACE("sat_mc_bug", tout << "adding: " << c << "\n";);
     }
 

src/sat/sat_model_converter.h

@@ -92,6 +92,8 @@ namespace sat {
 
         std::ostream& display(std::ostream & out, entry const& entry) const;
 
+        bool legal_to_flip(bool_var v) const;
+
     public:
         model_converter();
         ~model_converter();

src/sat/sat_solver.cpp

@@ -61,7 +61,7 @@ namespace sat {
         m_num_checkpoints         = 0;
         m_simplifications         = 0;
         m_cuber                   = nullptr;
-        m_mc.set_solver(nullptr);
+        m_mc.set_solver(this);
     }
 
     solver::~solver() {
@@ -1544,7 +1544,7 @@ namespace sat {
         
         if (m_config.m_drat) m_drat.check_model(m_model);
 
-        m_mc.set_solver(nullptr);
+        // m_mc.set_solver(nullptr);
         m_mc(m_model);
 
         
@@ -1601,7 +1601,7 @@ namespace sat {
         for (literal l : m_assumptions) {
             if (value_at(l, m) != l_true) {
                 VERIFY(is_external(l.var()));
-                IF_VERBOSE(0, verbose_stream() << l << " does not model check " << value_at(l, m) << "\n";);
+                IF_VERBOSE(0, verbose_stream() << "assumption: " << l << " does not model check " << value_at(l, m) << "\n";);
                 TRACE("sat",
                       tout << l << " does not model check\n";
                       tout << "trail: " << m_trail << "\n";

src/sat/sat_solver.h

@@ -353,6 +353,7 @@ namespace sat {
         void set_model(model const& mdl);
         char const* get_reason_unknown() const { return m_reason_unknown.c_str(); }
         bool check_clauses(model const& m) const;
+        bool is_assumption(bool_var v) const;
 
         literal select_lookahead(literal_vector const& assumptions, bool_var_vector const& vars);
         lbool  cube(bool_var_vector const& vars, literal_vector& lits, unsigned backtrack_level);
@@ -389,7 +390,6 @@ namespace sat {
         void reinit_assumptions();
         bool tracking_assumptions() const;
         bool is_assumption(literal l) const;
-        bool is_assumption(bool_var v) const;
         void simplify_problem();
         void mk_model();
         bool check_model(model const & m) const;