Try to produce an op_constraint lemma before invoking the fallback solver

src/math/polysat/solver.cpp

@@ -633,15 +633,32 @@ namespace polysat {
     /// Verify the value we're trying to assign against the univariate solver
     void solver::assign_verify(pvar v, rational val, justification j) {
         SASSERT(j.is_decision() || j.is_propagation());
-        // First, check evaluation of the currently-univariate constraints
+        signed_constraint c;
-        // TODO: we should add a better way to test constraints under assignments, without modifying the solver state.
+        {
-        m_value[v] = val;
+            // Fake the assignment v := val so we can check the constraints using the new value.
-        m_search.push_assignment(v, val);
+            m_value[v] = val;
-        m_justification[v] = j;
+            m_search.push_assignment(v, val);
-        bool is_valid = m_viable_fallback.check_constraints(v);
+            m_justification[v] = j;
-        m_search.pop();
+            on_scope_exit _undo([&](){
-        m_justification[v] = justification::unassigned();
+                m_search.pop();
-        if (!is_valid) {
+                m_justification[v] = justification::unassigned();
+            });
+
+            // Check evaluation of the currently-univariate constraints.
+            c = m_viable_fallback.find_violated_constraint(v);
+
+            if (c) {
+                LOG("Violated constraint: " << c);
+                // op_constraints produce lemmas rather than forbidden intervals, so give it an opportunity to
+                // produce a lemma before invoking the fallback solver.
+                if (c->is_op()) {
+                    c.narrow(*this, false);
+                    if (is_conflict())
+                        return;
+                }
+            }
+        }
+        if (c) {
             LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
             ++m_stats.m_num_viable_fallback;
             // Try to find a valid replacement value

src/math/polysat/viable.cpp

@@ -837,17 +837,17 @@ namespace polysat {
         m_constraints[v].pop_back();
     }
 
-    bool viable_fallback::check_constraints(pvar v) {
+    signed_constraint viable_fallback::find_violated_constraint(pvar v) {
-        for (auto const& c : m_constraints[v]) {
+        for (signed_constraint const c : m_constraints[v]) {
             // for this check, all variables need to be assigned
             DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
             if (c.is_currently_false(s)) {
                 LOG(assignment_pp(s, v, s.get_value(v)) << " violates constraint " << lit_pp(s, c));
-                return false;
+                return c;
             }
             SASSERT(c.is_currently_true(s));
         }
-        return true;
+        return {};
     }
 
     dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) {
@@ -869,6 +869,7 @@ namespace polysat {
 
         auto const& cs = m_constraints[v];
         for (unsigned i = cs.size(); i-- > 0; ) {
+            LOG("Univariate constraint: " << cs[i]);
             cs[i].add_to_univariate_solver(s, *us, i);
         }
 

src/math/polysat/viable.h

@@ -102,10 +102,9 @@ namespace polysat {
         bool is_viable(pvar v, rational const& val);
 
         /*
-        * Extract min and max viable values for v
+         * Extract min and max viable values for v
-        */
+         */
         rational min_viable(pvar v);
-
         rational max_viable(pvar v);
 
         /**
@@ -249,8 +248,10 @@ namespace polysat {
         void push_constraint(pvar v, signed_constraint const& c);
         void pop_constraint();
 
-        // Check whether all constraints for 'v' are satisfied.
+        // Check whether all constraints for 'v' are satisfied;
-        bool check_constraints(pvar v);
+        // or find an arbitrary violated constraint.
+        bool check_constraints(pvar v) { return !find_violated_constraint(v); }
+        signed_constraint find_violated_constraint(pvar v);
 
         dd::find_t find_viable(pvar v, rational& out_val);
         signed_constraints unsat_core(pvar v);