Support watching inactive constraints

This allows us to handle non-redundant clauses (like we get from quot_rem)

src/math/polysat/constraint.cpp

@@ -339,4 +339,11 @@ namespace polysat {
     lbool signed_constraint::bvalue(solver& s) const {
         return get()->has_bvar() ? s.m_bvars.value(blit()) : l_undef;
     }
+
+    std::ostream& constraint_pp::display(std::ostream& out) const {
+        if (c)
+            return c->display(out, status);
+        else
+            return out << "<null>";
+    }
 }

src/math/polysat/constraint.h

@@ -149,6 +149,7 @@ namespace polysat {
         unsigned_vector     m_vars;
         lbool               m_external_sign = l_undef;
         bool                m_is_active = false;
+        bool                m_is_pwatched = false;
         /** The boolean variable associated to this constraint, if any.
          *  If this is not null_bool_var, then the constraint corresponds to a literal on the assignment stack.
          *  Convention: the plain constraint corresponds the positive sat::literal.
@@ -207,6 +208,9 @@ namespace polysat {
         bool is_active() const { return m_is_active; }
         void set_active(bool f) { m_is_active = f; }
 
+        bool is_pwatched() const { return m_is_pwatched; }
+        void set_pwatched(bool f) { m_is_pwatched = f; }
+
         /// Assuming the constraint is univariate under the current assignment of 's',
         /// adds the constraint to the univariate solver 'us'.
         virtual void add_to_univariate_solver(solver& s, univariate_solver& us, unsigned dep, bool is_positive) const = 0;
@@ -297,4 +301,15 @@ namespace polysat {
             }
         };
     };
+
+    class constraint_pp {
+        constraint const* c;
+        lbool status;
+    public:
+        constraint_pp(constraint const* c, lbool status): c(c), status(status) {}
+        std::ostream& display(std::ostream& out) const;
+    };
+
+    inline std::ostream& operator<<(std::ostream& out, constraint_pp const& p) { return p.display(out); }
+
 }

src/math/polysat/solver.cpp

@@ -226,15 +226,14 @@ namespace polysat {
 #endif
         push_qhead();
         while (can_propagate()) {
-            if (is_conflict())
-                return;
             auto const& item = m_search[m_qhead++];
             if (item.is_assignment())
                 propagate(item.var());
             else
                 propagate(item.lit());
         }
-        linear_propagate();
+        if (!is_conflict())
+            linear_propagate();
         SASSERT(wlist_invariant());
         SASSERT(assignment_invariant());
     }
@@ -277,8 +276,9 @@ namespace polysat {
         DEBUG_CODE(m_locked_wlist = std::nullopt;);
     }
 
-    bool solver::propagate(pvar v, signed_constraint c) {
+    /** Return true if a new watch was found; or false to keep the existing one. */
-        LOG_H3("Propagate " << m_vars[v] << " in " << c);
+    bool solver::propagate(pvar v, constraint* c) {
+        LOG_H3("Propagate " << m_vars[v] << " in " << constraint_pp(c, m_bvars.value(c->bvar())));
         SASSERT(is_assigned(v));
         SASSERT(!c->vars().empty());
         unsigned idx = 0;
@@ -289,19 +289,48 @@ namespace polysat {
         for (unsigned i = c->vars().size(); i-- > 2; ) {
             unsigned other_v = c->vars()[i];
             if (!is_assigned(other_v)) {
-                add_watch(c, other_v);
+                add_pwatch(c, other_v);
                 std::swap(c->vars()[idx], c->vars()[i]);
-                if (!is_assigned(c->var(1 - idx)))
+                // if (!is_assigned(c->var(1 - idx)))  // TODO: why this check? if the other watch is already assigned (because e.g. all other variables have been propagated from other constraints first), then we end up with 3 watches on c
                     return true;
             }
         }
-        // at most one variable remains unassigned.
+
-        if (c->vars().size() >= 2) {
+        // TODO: aren't we visiting many constraints twice here?
-            unsigned other_v = c->var(1 - idx);
+        //  first, when one variable is unassigned -> intersect viable with constraint
-            if (!is_assigned(other_v))
+        //  second, when all variables are assigned -> check if there's a conflict.
-                m_viable_fallback.push_constraint(other_v, c);
+        // maybe not really a problem.
+
+        // at most one poly variable remains unassigned.
+        if (m_bvars.is_assigned(c->bvar())) {
+            // constraint is active, propagate it
+            SASSERT(c->is_active());
+            signed_constraint sc(c, m_bvars.value(c->bvar()) == l_true);
+            if (c->vars().size() >= 2) {
+                unsigned other_v = c->var(1 - idx);
+                if (!is_assigned(other_v))
+                    m_viable_fallback.push_constraint(other_v, sc);
+            }
+            sc.narrow(*this, false);
+        } else {
+            // constraint is not yet active, try to evaluate it
+            SASSERT(!c->is_active());
+            if (c->vars().size() >= 2) {
+                unsigned other_v = c->var(1 - idx);
+                if (!is_assigned(other_v)) {
+                    // wait for the remaining variable to be assigned (might not be necessary in all cases)
+                    return false;
+                }
+            }
+            // Evaluate constraint
+            signed_constraint sc(c, true);
+            if (sc.is_currently_true(*this))
+                assign_eval(sc.blit());
+            else {
+                SASSERT(sc.is_currently_false(*this));
+                assign_eval(~sc.blit());
+            }
         }
-        c.narrow(*this, false);
         return false;
     }
 
@@ -338,6 +367,7 @@ namespace polysat {
     }
 
     void solver::propagate(pvar v, rational const& val, signed_constraint c) {
+        // this looks weird... mixing propagation and conflict with c? also, the conflict should not be c but the whole of viable+c.
         LOG("Propagation: " << assignment_pp(*this, v, val) << ", due to " << c);
         if (m_viable.is_viable(v, val)) {
             m_free_pvars.del_var_eh(v);
@@ -374,6 +404,12 @@ namespace polysat {
                 pop_qhead();
                 break;
             }
+            case trail_instr_t::pwatch_i: {
+                constraint* c = m_pwatch_trail.back();
+                erase_pwatch(c);
+                m_pwatch_trail.pop_back();
+                break;
+            }
             case trail_instr_t::add_var_i: {
                 del_var();
                 break;
@@ -433,38 +469,46 @@ namespace polysat {
         }
     }
 
-    void solver::add_watch(signed_constraint c) {
+    void solver::add_pwatch(constraint* c) {
         SASSERT(c);
+        if (c->is_pwatched())
+            return;
         auto& vars = c->vars();
         unsigned i = 0, j = 0, sz = vars.size();
         for (; i < sz && j < 2; ++i)
             if (!is_assigned(vars[i]))
                 std::swap(vars[i], vars[j++]);
         if (vars.size() > 0)
-            add_watch(c, vars[0]);
+            add_pwatch(c, vars[0]);
         if (vars.size() > 1)
-            add_watch(c, vars[1]);
+            add_pwatch(c, vars[1]);
+        c->set_pwatched(true);
+        m_pwatch_trail.push_back(c);
+        m_trail.push_back(trail_instr_t::pwatch_i);
     }
 
-    void solver::add_watch(signed_constraint c, pvar v) {
+    void solver::add_pwatch(constraint* c, pvar v) {
-        SASSERT(c);
         // SASSERT(m_locked_wlist != v);  // appending doesn't interfere with propagation, so it should be fine
-        LOG("Watching v" << v << " in constraint " << c);
+        LOG("Watching v" << v << " in constraint " << show_deref(c));
         m_pwatch[v].push_back(c);
     }
 
-    void solver::erase_watch(signed_constraint c) {
+    void solver::erase_pwatch(constraint* c) {
+        if (!c->is_pwatched())
+            return;
         auto const& vars = c->vars();
         if (vars.size() > 0)
-            erase_watch(vars[0], c);
+            erase_pwatch(vars[0], c);
         if (vars.size() > 1)
-            erase_watch(vars[1], c);
+            erase_pwatch(vars[1], c);
+        c->set_pwatched(false);
     }
 
-    void solver::erase_watch(pvar v, signed_constraint c) {
+    void solver::erase_pwatch(pvar v, constraint* c) {
         if (v == null_var)
             return;
         SASSERT(m_locked_wlist != v);
+        LOG("Unwatching v" << v << " in constraint " << show_deref(c));
         auto& wlist = m_pwatch[v];
         unsigned sz = wlist.size();
         for (unsigned i = 0; i < sz; ++i) {
@@ -941,7 +985,7 @@ namespace polysat {
         SASSERT(m_bvars.value(c.blit()) == l_true);
         SASSERT(!c->is_active());
         c->set_active(true);
-        add_watch(c);
+        add_pwatch(c.get());
         if (c->vars().size() == 1)
             m_viable_fallback.push_constraint(c->var(0), c);
         c.narrow(*this, true);
@@ -954,7 +998,6 @@ namespace polysat {
     void solver::deactivate_constraint(signed_constraint c) {
         LOG("Deactivating constraint: " << c.blit());
         c->set_active(false);
-        erase_watch(c);
     }
 
     void solver::backjump(unsigned new_level) {
@@ -977,9 +1020,22 @@ namespace polysat {
         for (sat::literal lit : clause) {
             LOG("   Literal " << lit << " is: " << lit2cnstr(lit));
             // SASSERT(m_bvars.value(lit) != l_true);
+            // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
+            if (m_bvars.value(lit) == l_true) {
+                // in this case the clause is useless
+                LOG("   Clause is already true, skippping...");
+                return;
+            }
         }
         SASSERT(!clause.empty());
         m_constraints.store(&clause, *this, true);
+
+        if (!clause.is_redundant()) {
+            // for (at least) non-redundant clauses, we also need to watch the constraints
+            // so we can discover when the clause should propagate
+            for (sat::literal lit : clause)
+                add_pwatch(m_constraints.lookup(lit.var()));
+        }
     }
 
     void solver::add_clause(unsigned n, signed_constraint* cs, bool is_redundant) {
@@ -1125,6 +1181,12 @@ namespace polysat {
      * Check that two variables of each constraint are watched.
      */
     bool solver::wlist_invariant() {
+        for (pvar v = 0; v < m_value.size(); ++v) {
+            std::stringstream s;
+            for (constraint* c : m_pwatch[v])
+                s << " " << c->bvar();
+            LOG("Watch for v" << v << ": " << s.str());
+        }
         // Skip boolean variables that aren't active yet
         uint_set skip;
         for (unsigned i = m_qhead; i < m_search.size(); ++i)
@@ -1143,7 +1205,7 @@ namespace polysat {
             int64_t num_watches = 0;
             signed_constraint sc(c, is_positive);
             for (auto const& wlist : m_pwatch) {
-                auto n = std::count(wlist.begin(), wlist.end(), sc);
+                auto n = std::count(wlist.begin(), wlist.end(), c);
                 if (n > 1)
                     std::cout << sc << "\n" << * this << "\n";
                 VERIFY(n <= 1);  // no duplicates in the watchlist
@@ -1151,7 +1213,7 @@ namespace polysat {
             }
             unsigned expected_watches = std::min(2u, c->vars().size());
             if (num_watches != expected_watches)
-                LOG("wrong number of watches: " << sc << "   vars: " << sc->vars());
+                LOG("wrong number of watches: " << sc.blit() << ": " << sc << " (vars: " << sc->vars() << ")");
             SASSERT_EQ(num_watches, expected_watches);
         }
         return true;

src/math/polysat/solver.h

@@ -108,7 +108,7 @@ namespace polysat {
         // Per variable information
         vector<rational>         m_value;         // assigned value
         vector<justification>    m_justification; // justification for variable assignment
-        vector<signed_constraints> m_pwatch;      // watch list datastructure into constraints.
+        vector<constraints>      m_pwatch;        // watch list datastructure into constraints.
 #ifndef NDEBUG
         std::optional<pvar>      m_locked_wlist;  // restrict watch list modification while it is being propagated
         bool                     m_propagating = false;  // set to true during propagation
@@ -128,7 +128,7 @@ namespace polysat {
 
         svector<trail_instr_t>   m_trail;
         unsigned_vector          m_qhead_trail;
-        unsigned_vector          m_cjust_trail;
+        constraints              m_pwatch_trail;
 
         unsigned_vector          m_base_levels;  // External clients can push/pop scope. 
 
@@ -179,13 +179,13 @@ namespace polysat {
 
         void propagate(sat::literal lit);
         void propagate(pvar v);
-        bool propagate(pvar v, signed_constraint c);
+        bool propagate(pvar v, constraint* c);
         void propagate(pvar v, rational const& val, signed_constraint c);
         bool propagate(sat::literal lit, clause& cl);
-        void erase_watch(pvar v, signed_constraint c);
+        void add_pwatch(constraint* c);
-        void erase_watch(signed_constraint c);
+        void add_pwatch(constraint* c, pvar v);
-        void add_watch(signed_constraint c);
+        void erase_pwatch(pvar v, constraint* c);
-        void add_watch(signed_constraint c, pvar v);
+        void erase_pwatch(constraint* c);
 
         void set_conflict(signed_constraint c) { m_conflict.set(c); }
         void set_conflict(clause& cl) { m_conflict.set(cl); }

src/math/polysat/trail.h

@@ -18,6 +18,7 @@ namespace polysat {
 
     enum class trail_instr_t { 
         qhead_i,
+        pwatch_i,
         add_var_i,
         inc_level_i,
         viable_add_i,