Fix dependency tracking for viable_fallback

now takes into account explanations for overlapping variables

src/math/polysat/conflict.cpp

@@ -288,13 +288,15 @@ namespace polysat {
         SASSERT(!empty());
     }
 
-    void conflict::init_by_viable_fallback(pvar v, univariate_solver& us) {
+    void conflict::init_viable_fallback_begin(pvar v) {
         LOG("Conflict: viable_fallback v" << v);
         SASSERT(empty());
         SASSERT(!s.is_assigned(v));
         m_level = s.m_level;
         logger().begin_conflict(header_with_var("viable_fallback v", v));
-        VERIFY(s.m_viable.resolve_fallback(v, us, *this));
+    }
+
+    void conflict::init_viable_fallback_end(pvar v) {
         SASSERT(!empty());
         revert_pvar(v);  // at this point, v is not assigned
     }

src/math/polysat/conflict.h

@@ -137,7 +137,8 @@ namespace polysat {
         /** conflict because there is no viable value for the variable v, by interval reasoning */
         void init_by_viable_interval(pvar v);
         /** conflict because there is no viable value for the variable v, by fallback solver */
-        void init_by_viable_fallback(pvar v, univariate_solver& us);
+        void init_viable_fallback_begin(pvar v);
+        void init_viable_fallback_end(pvar v);
 
         /** conflict depends on dep and free variables in c **/
         /** c evaluates to false but is assigned to true by dep **/

src/math/polysat/solver.h

@@ -302,7 +302,6 @@ namespace polysat {
         void set_conflict(signed_constraint c) { m_conflict.init(c); }
         void set_conflict(clause& cl) { m_conflict.init(cl); }
         void set_conflict_by_viable_interval(pvar v) { m_conflict.init_by_viable_interval(v); }
-        void set_conflict_by_viable_fallback(pvar v, univariate_solver& us) { m_conflict.init_by_viable_fallback(v, us); }
 
         bool can_decide() const;
         bool can_bdecide() const;

src/math/polysat/viable.cpp

@@ -1780,8 +1780,7 @@ namespace polysat {
         unsigned const bit_width = s.size(v);
         univariate_solver* us = s.m_viable_fallback.usolver(bit_width);
         sat::literal_set added;
-
+        svector<std::pair<pvar, sat::literal>> deps;
-        // TODO: justifications need to include equalities from slicing egraph
 
         // First step: only query the looping constraints and see if they alone are already UNSAT.
         // The constraints which caused the refinement loop can always be reached from m_units.
@@ -1801,7 +1800,9 @@ namespace polysat {
                                 added.insert(lit);
                                 LOG("Adding " << lit_pp(s, lit));
                                 IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
-                                src.add_to_univariate_solver(x, s, *us, lit.to_uint());
+                                unsigned d = deps.size();
+                                deps.push_back({x, lit});
+                                src.add_to_univariate_solver(x, s, *us, d);
                             }
                         }
                     }
@@ -1813,7 +1814,7 @@ namespace polysat {
 
         switch (us->check()) {
         case l_false:
-            s.set_conflict_by_viable_fallback(v, *us);
+            set_conflict_by_fallback(v, *us, deps);
             return l_false;
         case l_true:
             // At this point we don't know much because we did not add all relevant constraints
@@ -1834,13 +1835,15 @@ namespace polysat {
                 LOG("Adding " << lit_pp(s, lit));
                 IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
                 added.insert(lit);
-                cs[i].add_to_univariate_solver(x, s, *us, lit.to_uint());
+                unsigned d = deps.size();
+                deps.push_back({x, lit});
+                cs[i].add_to_univariate_solver(x, s, *us, d);
             }
         }
 
         switch (us->check()) {
         case l_false:
-            s.set_conflict_by_viable_fallback(v, *us);
+            set_conflict_by_fallback(v, *us, deps);
             return l_false;
         case l_true:
             lo = us->model();
@@ -1876,7 +1879,9 @@ namespace polysat {
         IF_VERBOSE(10, verbose_stream() << "Fallback\n";);
         LOG("Refinement budget exhausted! Fall back to univariate solver.");
 
-        return find_viable_fallback(v, lo, hi);
+        pvar_vector overlaps;
+        overlaps.push_back(v);
+        return find_viable_fallback(v, overlaps, lo, hi);
     }
 
     lbool viable::query_find(pvar v, rational& lo, rational& hi, fixed_bits_info const& fbi) {
@@ -1958,75 +1963,9 @@ namespace polysat {
         return l_true;
     }
 
-    lbool viable::find_viable_fallback(pvar v, rational& lo, rational& hi) {
+    bool viable::set_conflict_by_fallback(pvar v, univariate_solver& us, svector<std::pair<pvar, sat::literal>> const& deps) {
-        unsigned const bit_width = s.size(v);
+        auto& core = s.m_conflict;
-        univariate_solver* us = s.m_viable_fallback.usolver(bit_width);
+        core.init_viable_fallback_begin(v);
-        sat::literal_set added;
-
-        // First step: only query the looping constraints and see if they alone are already UNSAT.
-        // The constraints which caused the refinement loop can always be reached from m_units.
-        LOG_H3("Checking looping univariate constraints for v" << v << "...");
-        LOG("Assignment: " << assignments_pp(s));
-        entry const* first = m_units[v].get_entries(s.size(v));  // TODO: take other sizes into account
-        entry const* e = first;
-        do {
-            // in the first step we're only interested in entries from refinement
-            if (e->refined) {
-                for (signed_constraint const src : e->src) {
-                    sat::literal const lit = src.blit();
-                    if (!added.contains(lit)) {
-                        added.insert(lit);
-                        LOG("Adding " << lit_pp(s, lit));
-                        IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
-                        src.add_to_univariate_solver(v, s, *us, lit.to_uint());
-                    }
-                }
-            }
-            e = e->next();
-        }
-        while (e != first);
-
-        switch (us->check()) {
-        case l_false:
-            s.set_conflict_by_viable_fallback(v, *us);
-            return l_false;
-        case l_true:
-            // At this point we don't know much because we did not add all relevant constraints
-            break;
-        default:
-            // resource limit
-            return l_undef;
-        }
-
-        // Second step: looping constraints aren't UNSAT, so add the remaining relevant constraints
-        LOG_H3("Checking all univariate constraints for v" << v << "...");
-        auto const& cs = s.m_viable_fallback.m_constraints[v];
-        for (unsigned i = cs.size(); i-- > 0; ) {
-            sat::literal const lit = cs[i].blit();
-            if (added.contains(lit))
-                continue;
-            LOG("Adding " << lit_pp(s, lit));
-            IF_VERBOSE(10, verbose_stream() << ";; " << lit_pp(s, lit) << "\n");
-            added.insert(lit);
-            cs[i].add_to_univariate_solver(v, s, *us, lit.to_uint());
-        }
-
-        switch (us->check()) {
-        case l_false:
-            s.set_conflict_by_viable_fallback(v, *us);
-            return l_false;
-        case l_true:
-            lo = us->model();
-            hi = -1;
-            return l_true;
-            // TODO: return us.find_two(lo, hi) ? l_true : l_undef;  ???
-        default:
-            // resource limit
-            return l_undef;
-        }
-    }
-
-    bool viable::resolve_fallback(pvar v, univariate_solver& us, conflict& core) {
         // The conflict is the unsat core of the univariate solver,
         // and the current assignment (under which the constraints are univariate in v)
         // TODO:
@@ -2034,8 +1973,11 @@ namespace polysat {
         //      e.g.:   v^2 + w^2 == 0;   w := 1
         // - but we could use side constraints on the coefficients instead (coefficients when viewed as polynomial over v):
         //      e.g.:   v^2 + w^2 == 0;   w^2 == 1
-        for (unsigned dep : us.unsat_core()) {
+        for (unsigned d : us.unsat_core()) {
-            sat::literal lit = sat::to_literal(dep);
+            auto [x, lit] = deps[d];
+            s.m_slicing.explain_simple_overlap(v, x, [this, &core](sat::literal l) {
+                core.insert(s.lit2cnstr(l));
+            });
             signed_constraint c = s.lit2cnstr(lit);
             core.insert(c);
             core.insert_vars(c);
@@ -2043,6 +1985,7 @@ namespace polysat {
         SASSERT(!core.vars().contains(v));
         core.add_lemma("viable unsat core", core.build_lemma());
         IF_VERBOSE(10, verbose_stream() << "unsat core " << core << "\n";);
+        core.init_viable_fallback_end(v);
         return true;
     }
 

src/math/polysat/viable.h

@@ -202,10 +202,14 @@ namespace polysat {
          * Bitblasting-based query.
          * @return l_true on success, l_false on conflict, l_undef on resource limit
          */
-        lbool find_viable_fallback(pvar v, rational& out_lo, rational& out_hi);
-
         lbool find_viable_fallback(pvar v, pvar_vector const& overlaps, rational& out_lo, rational& out_hi);
 
+        /**
+         * Enter conflict state after querying the univariate solver.
+         * \pre there are no viable values for v (determined by fallback solver)
+         */
+        bool set_conflict_by_fallback(pvar v, univariate_solver& us, svector<std::pair<pvar, sat::literal>> const& deps);
+
 
 public:
         lbool find_viable2_new(pvar v, rational& out_lo, rational& out_hi);
@@ -299,12 +303,6 @@ public:
          */
         bool resolve_interval(pvar v, conflict& core);
 
-        /**
-         * Retrieve the unsat core for v.
-         * \pre there are no viable values for v (determined by fallback solver)
-         */
-        bool resolve_fallback(pvar v, univariate_solver& us, conflict& core);
-
         /** Log all viable values for the given variable.
          * (Inefficient, but useful for debugging small instances.)
          */