Propagation must be justified by a prefix of Gamma

src/math/polysat/solver.cpp

@@ -981,6 +981,16 @@ namespace polysat {
         m_search.push_boolean(lit);
     }
 
+    /** Push c onto \Gamma, unless it is already true. */
+    void solver::try_assign_eval(signed_constraint c) {
+        sat::literal const lit = c.blit();
+        if (m_bvars.is_assigned(lit))
+            return;
+        if (c.is_always_true())
+            return;
+        assign_eval(lit);
+    }
+
     /**
     * Activate constraint immediately
     * Activation and de-activation of constraints follows the scope controlled by push/pop.

src/math/polysat/solver.h

@@ -167,6 +167,8 @@ namespace polysat {
         void push_level();
         void pop_levels(unsigned num_levels);
 
+        void try_assign_eval(signed_constraint c);
+
         void assign_propagate(sat::literal lit, clause& reason);
         void assign_decision(sat::literal lit);
         void assign_eval(sat::literal lit);

src/math/polysat/viable.cpp

@@ -132,7 +132,7 @@ namespace polysat {
             rational val;
             switch (find_viable(v, val)) {
             case dd::find_t::singleton:
-                s.assign_propagate(v, val);
+                propagate(v, val);
                 prop = true;
                 break;
             case dd::find_t::empty:
@@ -150,6 +150,24 @@ namespace polysat {
         return prop;
     }
 
+    void viable::propagate(pvar v, rational const& val) {
+        // NOTE: all propagations must be justified by a prefix of \Gamma,
+        //       otherwise dependencies may be missed during conflict resolution.
+        //       The propagation reason for v := val consists of the following constraints:
+        //       - source constraint (already on \Gamma)
+        //       - side conditions
+        //       - i.lo() == i.lo_val() for each unit interval i
+        //       - i.hi() == i.hi_val() for each unit interval i
+        for (auto const& c : get_constraints(v)) {
+            s.try_assign_eval(c);
+        }
+        for (auto const& i : units(v)) {
+            s.try_assign_eval(s.eq(i.lo(), i.lo_val()));
+            s.try_assign_eval(s.eq(i.hi(), i.hi_val()));
+        }
+        s.assign_propagate(v, val);
+    }
+
     bool viable::intersect(pvar v, signed_constraint const& c) {
         entry* ne = alloc_entry();
         if (!m_forbidden_intervals.get_interval(c, v, *ne)) {
@@ -187,6 +205,7 @@ namespace polysat {
     }
 
     bool viable::intersect(pvar v, entry* ne) {
+        SASSERT(!s.is_assigned(v));
         entry* e = m_units[v];
         if (e && e->interval.is_full()) {
             m_alloc.push_back(ne);

src/math/polysat/viable.h

@@ -63,6 +63,8 @@ namespace polysat {
 
         void insert(entry* e, pvar v, ptr_vector<entry>& entries, entry_kind k);
 
+        void propagate(pvar v, rational const& val);
+
     public:
         viable(solver& s);