Check invariant on pvars

src/math/polysat/assignment.h

@@ -77,7 +77,7 @@ namespace polysat {
     /** Full variable assignment, may include variables of varying bit widths. */
     class assignment {
         solver*                                 m_solver;
-        vector<assignment_item_t>               m_pairs;  // TODO: do we still need this?
+        vector<assignment_item_t>               m_pairs;
         mutable scoped_ptr_vector<substitution> m_subst;
         vector<substitution>                    m_subst_trail;
 

src/math/polysat/solver.cpp

@@ -74,6 +74,7 @@ namespace polysat {
             LOG("Assignment:     " << assignments_pp(*this));
             if (is_conflict()) LOG("Conflict:       " << m_conflict);
             IF_LOGGING(m_viable.log());
+            SASSERT(var_queue_invariant());
             if (is_conflict() && at_base_level()) { LOG_H2("UNSAT"); return l_false; }
             else if (is_conflict()) resolve_conflict();
             else if (should_add_pwatch()) add_pwatch();
@@ -1445,7 +1446,7 @@ namespace polysat {
     }
 
     /** Check that boolean assignment and constraint evaluation are consistent */
-    bool solver::assignment_invariant() {
+    bool solver::assignment_invariant() const {
         if (is_conflict())
             return true;
         bool ok = true;
@@ -1464,6 +1465,25 @@ namespace polysat {
         return ok;
     }
 
+    /** Check that each variable is either assigned or queued for decisions */
+    bool solver::var_queue_invariant() const {
+        if (is_conflict())
+            return true;
+        uint_set active;
+        for (pvar v : m_free_pvars)
+            active.insert(v);
+        for (auto const& [v, val] : assignment())
+            active.insert(v);
+        bool ok = true;
+        for (pvar v = 0; v < num_vars(); ++v) {
+            if (!active.contains(v)) {
+                ok = false;
+                LOG("Lost variable v" << v << " (it is neither assigned nor free)");
+            }
+        }
+        return ok;
+    }
+
     /// Check that all constraints on the stack are satisfied by the current model.
     bool solver::verify_sat() {
         LOG_H1("Checking current model...");

src/math/polysat/solver.h

@@ -211,6 +211,8 @@ namespace polysat {
         dd::pdd_manager& sz2pdd(unsigned sz) const;
         dd::pdd_manager& var2pdd(pvar v) const;
 
+        pvar num_vars() const { return m_value.size(); }
+
         assignment_t const& assignment() const { return m_search.assignment(); }
 
         void push_level();
@@ -306,7 +308,8 @@ namespace polysat {
         static bool invariant(signed_constraints const& cs);
         bool wlist_invariant() const;
         bool bool_watch_invariant() const;
-        bool assignment_invariant();
+        bool assignment_invariant() const;
+        bool var_queue_invariant() const;
         bool verify_sat();
 
         bool can_propagate();

src/util/var_queue.h

@@ -89,6 +89,10 @@ public:
         }
         return out;
     }
+
+    using const_iterator = decltype(m_queue)::const_iterator;
+    const_iterator begin() const { return m_queue.begin(); }
+    const_iterator end() const { return m_queue.end(); }
 };
 
 inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) {