fix cnf check

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

src/opt/opt_context.cpp

@@ -361,7 +361,7 @@ namespace opt {
         mdl = m_model;
         fix_model(mdl);
         if (mdl) mdl->set_model_completion(true);
-        TRACE("opt", tout << *mdl;);
+        CTRACE("opt", mdl, tout << *mdl;);
     }
 
     void context::get_box_model(model_ref& mdl, unsigned index) {

src/sat/sat_drat.cpp

@@ -143,7 +143,7 @@ namespace sat {
         IF_VERBOSE(20, trace(verbose_stream(), n, c.begin(), st););
 
         if (st == status::learned) {
-            verify(n, c.begin());
+            verify(c);
         }
 
         m_status.push_back(st);
@@ -225,6 +225,55 @@ namespace sat {
         m_units.resize(num_units);
         bool ok = m_inconsistent;
         m_inconsistent = false;
+
+        if (!ok) {
+            literal_vector lits(n, c);
+            IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
+            for (unsigned v = 0; v < m_assignment.size(); ++v) {
+                lbool val = m_assignment[v];
+                if (val != l_undef) {
+                    IF_VERBOSE(0, verbose_stream() << literal(v, false) << " |-> " << val << "\n");
+                }
+            }
+            for (clause* cp : s.m_clauses) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            for (clause* cp : s.m_learned) {
+                clause& cl = *cp;
+                bool found = false;
+                for (literal l : cl) {
+                    if (m_assignment[l.var()] != (l.sign() ? l_true : l_false)) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Clause is false under assignment: " << cl << "\n");
+                }
+            }
+            svector<sat::solver::bin_clause> bin;
+            s.collect_bin_clauses(bin, true);
+            for (auto & b : bin) {
+                bool found = false;
+                if (m_assignment[b.first.var()] != (b.first.sign() ? l_true : l_false)) found = true;
+                if (m_assignment[b.second.var()] != (b.second.sign() ? l_true : l_false)) found = true;
+                if (!found) {
+                    IF_VERBOSE(0, verbose_stream() << "Bin clause is false under assignment: " << b.first << " " << b.second << "\n");
+                }
+            }
+            IF_VERBOSE(0, s.display(verbose_stream()));
+            exit(0);
+        }
         return ok;
     }
 
@@ -280,7 +329,10 @@ namespace sat {
 
     void drat::verify(unsigned n, literal const* c) {
         if (m_check_unsat && !is_drup(n, c) && !is_drat(n, c)) {
-            std::cout << "Verification failed\n";
+            literal_vector lits(n, c);
+            std::cout << "Verification of " << lits << " failed\n";
+            s.display(std::cout);
+            exit(0);
             UNREACHABLE();
             //display(std::cout);
             TRACE("sat", 
@@ -291,6 +343,35 @@ namespace sat {
         }
     }
 
+    bool drat::contains(unsigned n, literal const* lits) {
+        for (unsigned i = m_proof.size(); i-- > 0; ) {
+            clause& c = *m_proof[i];
+            status st = m_status[i];
+            if (match(n, lits, c)) {
+                return st != status::deleted;
+            }
+        }
+        return false;
+    }
+
+    bool drat::match(unsigned n, literal const* lits, clause const& c) const {
+        if (n == c.size()) {
+            for (unsigned i = 0; i < n; ++i) {
+                literal lit1 = lits[i];
+                bool found = false;
+                for (literal lit2 : c) {
+                    if (lit1 == lit2) {
+                        found = true;
+                        break;
+                    }
+                }
+                if (!found) return false;
+            }
+            return true;
+        }
+        return false;
+    }
+
     void drat::display(std::ostream& out) const {
         out << "units: " << m_units << "\n";
         for (unsigned i = 0; i < m_assignment.size(); ++i) {

src/sat/sat_drat.h

@@ -67,7 +67,6 @@ namespace sat {
         void propagate(literal l);
         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);
         bool is_drat(unsigned n, literal const* c, unsigned pos);
@@ -75,6 +74,7 @@ namespace sat {
         void trace(std::ostream& out, unsigned n, literal const* c, status st);
         void display(std::ostream& out) const;
         void validate_propagation() const;
+        bool match(unsigned n, literal const* lits, clause const& c) const;
 
     public:
         drat(solver& s);
@@ -93,6 +93,16 @@ namespace sat {
         void del(literal l1, literal l2);
         void del(clause& c);
 
+        void verify(clause const& c) { verify(c.size(), c.begin()); }
+        void verify(unsigned n, literal const* c);
+        void verify(literal l1, literal l2) { literal lits[2] = {l1, l2}; verify(2, lits); }
+        void verify(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; verify(3, lits); }
+
+        bool contains(clause const& c) { return contains(c.size(), c.begin()); }
+        bool contains(unsigned n, literal const* c);
+        bool contains(literal l1, literal l2) { literal lits[2] = {l1, l2}; return contains(2, lits); }
+        bool contains(literal l1, literal l2, literal l3) { literal lits[3] = {l1, l2, l3}; return contains(3, lits); }
+
         void check_model(model const& m);
     };
 

src/sat/sat_solver/inc_sat_solver.cpp

@@ -279,7 +279,6 @@ public:
             }
         }
         else {
-            m_is_cnf &= is_clause(t);
             assert_expr_core(t);
         }
     }
@@ -287,6 +286,7 @@ public:
     ast_manager& get_manager() const override { return m; }
     void assert_expr_core(expr * t) override {
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
+        m_is_cnf &= is_clause(t);
         m_fmls.push_back(t);
     }
     void set_produce_models(bool f) override {}