add model checker to external

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

src/sat/ba_solver.cpp

@@ -1641,7 +1641,6 @@ namespace sat {
         xr* x = new (mem) xr(next_id(), lits);
         x->set_learned(learned);
         add_constraint(x);
-        for (literal l : lits) s().set_external(l.var()); // TBD: determine if goal2sat does this.
         return x;
     }
 
@@ -1715,7 +1714,6 @@ namespace sat {
     }
 
 
-
     void ba_solver::ensure_parity_size(bool_var v) {
         if (m_parity_marks.size() <= static_cast<unsigned>(v)) {
             m_parity_marks.resize(static_cast<unsigned>(v) + 1, 0);
@@ -2087,6 +2085,17 @@ namespace sat {
         return l_undef;        
     }
 
+    lbool ba_solver::eval(model const& m, constraint const& c) const {
+        lbool v1 = c.lit() == null_literal ? l_true : value(c.lit());
+        switch (c.tag()) {
+        case card_t: return eval(v1, eval(m, c.to_card())); 
+        case pb_t:   return eval(v1, eval(m, c.to_pb()));
+        case xr_t:  return eval(v1, eval(m, c.to_xr()));
+        default: UNREACHABLE(); break;
+        }
+        return l_undef;        
+    }
+
     lbool ba_solver::eval(lbool a, lbool b) const {
         if (a == l_undef || b == l_undef) return l_undef;
         return (a == b) ? l_true : l_false;
@@ -2106,6 +2115,34 @@ namespace sat {
         return l_undef;        
     }
 
+    lbool ba_solver::eval(model const& m, card const& c) const {
+        unsigned trues = 0, undefs = 0;
+        for (literal l : c) {
+            switch (l.sign() ? ~m[l.var()] : m[l.var()]) {
+            case l_true: trues++; break;
+            case l_undef: undefs++; break;
+            default: break;
+            }
+        }
+        if (trues + undefs < c.k()) return l_false;
+        if (trues >= c.k()) return l_true;
+        return l_undef;        
+    }
+
+    lbool ba_solver::eval(model const& m, pb const& p) const {
+        unsigned trues = 0, undefs = 0;
+        for (wliteral wl : p) {
+            switch (wl.second.sign() ? ~m[wl.second.var()] : m[wl.second.var()]) {
+            case l_true: trues += wl.first; break;
+            case l_undef: undefs += wl.first; break;
+            default: break;
+            }
+        }
+        if (trues + undefs < p.k()) return l_false;
+        if (trues >= p.k()) return l_true;
+        return l_undef;        
+    }
+
     lbool ba_solver::eval(pb const& p) const {
         unsigned trues = 0, undefs = 0;
         for (wliteral wl : p) {
@@ -2133,6 +2170,19 @@ namespace sat {
         return odd ? l_true : l_false;
     }
 
+    lbool ba_solver::eval(model const& m, xr const& x) const {
+        bool odd = false;
+        
+        for (auto l : x) {
+            switch (l.sign() ? ~m[l.var()] : m[l.var()]) {
+            case l_true: odd = !odd; break;
+            case l_false: break;
+            default: return l_undef;
+            }
+        }
+        return odd ? l_true : l_false;
+    }
+
     bool ba_solver::validate() {
         if (!validate_watch_literals()) {
             return false;
@@ -2903,7 +2953,6 @@ namespace sat {
                     remove_constraint(c, "contains eliminated var");                    
                     break;
                 }
-                s().set_external(v);                
             }
         }
         return ext;
@@ -2984,14 +3033,6 @@ namespace sat {
         m_constraint_removed = false;
     }
 
-    void ba_solver::ensure_external(constraint const& c) {
-        literal_vector lits(c.literals());
-        for (literal l : lits) {
-            s().set_external(l.var());
-        }
-    }
-
-
     void ba_solver::cleanup_constraints(ptr_vector<constraint>& cs, bool learned) {
         ptr_vector<constraint>::iterator it = cs.begin();
         ptr_vector<constraint>::iterator it2 = it;
@@ -3004,7 +3045,6 @@ namespace sat {
                 m_allocator.deallocate(c.obj_size(), &c);
             }
             else if (learned && !c.learned()) {
-                ensure_external(c);
                 m_constraints.push_back(&c);
             }
             else {
@@ -4051,6 +4091,23 @@ namespace sat {
         return value < p.m_k;
     }
 
+    bool ba_solver::check_model(model const& m) const {
+        bool ok = true;
+        for (constraint const* c : m_constraints) {
+            if (!check_model(m, *c)) ok = false;
+        }
+        return ok;
+    }
+
+    bool ba_solver::check_model(model const& m, constraint const& c) const {
+        if (eval(m, c) != l_true) {
+            IF_VERBOSE(0, verbose_stream() << "failed checking " << c.id() << ": " << c << "\n";);
+            return false;
+        }
+        else {
+            return true;
+        }
+    }
 
     
 };

src/sat/ba_solver.h

@@ -302,7 +302,6 @@ namespace sat {
         void cleanup_clauses();
         void cleanup_constraints();
         void cleanup_constraints(ptr_vector<constraint>& cs, bool learned);
-        void ensure_external(constraint const& c);
         void remove_constraint(constraint& c, char const* reason);
 
         // constraints
@@ -328,6 +327,7 @@ namespace sat {
         void attach_constraint(constraint const& c);
         void detach_constraint(constraint const& c);
         lbool eval(constraint const& c) const;
+        lbool eval(model const& m, constraint const& c) const;
         lbool eval(lbool a, lbool b) const;
         void assert_unconstrained(literal lit, literal_vector const& lits);
         void flush_roots(constraint& c);
@@ -348,6 +348,7 @@ namespace sat {
         bool clausify(card& c);
         bool clausify(literal lit, unsigned n, literal const* lits, unsigned k);
         lbool eval(card const& c) const;
+        lbool eval(model const& m, card const& c) const;
         double get_reward(card const& c, literal_occs_fun& occs) const;
 
 
@@ -362,6 +363,7 @@ namespace sat {
         bool clausify(xr& x);
         void flush_roots(xr& x);
         lbool eval(xr const& x) const;
+        lbool eval(model const& m, xr const& x) const;
         
         // pb functionality
         unsigned m_a_max;
@@ -379,6 +381,7 @@ namespace sat {
         bool clausify(pb& p);
         bool is_cardinality(pb const& p, literal_vector& lits);
         lbool eval(pb const& p) const;
+        lbool eval(model const& m, pb const& p) const;
         double get_reward(pb const& p, literal_occs_fun& occs) const;
 
         // access solver
@@ -463,6 +466,8 @@ namespace sat {
 
         void copy_core(ba_solver* result, bool learned);
         void copy_constraints(ba_solver* result, ptr_vector<constraint> const& constraints);
+
+        bool check_model(model const& m, constraint const& c) const;
     public:
         ba_solver();
         virtual ~ba_solver();
@@ -497,6 +502,7 @@ namespace sat {
         virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r);
         virtual void init_use_list(ext_use_list& ul);
         virtual bool is_blocked(literal l, ext_constraint_idx idx);
+        virtual bool check_model(model const& m) const;
 
         ptr_vector<constraint> const & constraints() const { return m_constraints; }
         void display(std::ostream& out, constraint const& c, bool values) const;

src/sat/sat_extension.h

@@ -79,6 +79,7 @@ namespace sat {
         virtual bool validate() = 0;
         virtual void init_use_list(ext_use_list& ul) = 0;
         virtual bool is_blocked(literal l, ext_constraint_idx) = 0;
+        virtual bool check_model(model const& m) const = 0;
     };
 
 };

src/sat/sat_solver.cpp

@@ -244,7 +244,6 @@ namespace sat {
     void solver::set_external(bool_var v) {
         if (m_external[v] != 0) return;
         m_external[v] = 1;
-
         if (!m_ext) return;
         
         lbool val = value(v);
@@ -1707,6 +1706,9 @@ namespace sat {
                 ok = false;
             }
         }
+        if (m_ext && !m_ext->check_model(m)) {
+            ok = false;
+        }
         return ok;
     }