Extract viable_fallback into separate file

src/math/polysat/CMakeLists.txt

@@ -30,6 +30,7 @@ z3_add_component(polysat
     umul_ovfl_constraint.cpp
     variable_elimination.cpp
     viable.cpp
+    viable_fallback.cpp
   COMPONENT_DEPENDENCIES
     bigfix
     dd

src/math/polysat/solver.h

@@ -36,6 +36,7 @@ Author:
 #include "math/polysat/trail.h"
 #include "math/polysat/pvar_queue.h"
 #include "math/polysat/viable.h"
+#include "math/polysat/viable_fallback.h"
 #include "math/polysat/log.h"
 #include <limits>
 #include <optional>

src/math/polysat/viable.cpp

@@ -8,7 +8,7 @@ Module Name:
 Author:
 
     Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Jakob Rath 2021-04-06
 
 Notes:
 
@@ -18,11 +18,6 @@ In other cases, the phase of a variable assignment across branches
 might be used in a call to is_viable. With phase caching on, it may
 just check if the cached phase is viable without detecting that it is a propagation.
 
-TODO: improve management of the fallback univariate solvers:
-      - use a solver pool and recycle the least recently used solver
-      - incrementally add/remove constraints
-      - set resource limit of univariate solver
-
 TODO: plan to fix the FI "pumping":
     1. simple looping detection and bitblasting fallback.  -- done
     2. intervals at multiple bit widths
@@ -37,7 +32,6 @@ TODO: plan to fix the FI "pumping":
 #include "math/polysat/viable.h"
 #include "math/polysat/solver.h"
 #include "math/polysat/number.h"
-#include "math/polysat/univariate/univariate_solver.h"
 
 namespace polysat {
 
@@ -2312,110 +2306,4 @@ namespace {
         return true;
     }
 
-    //************************************************************************
-    // viable_fallback
-    //************************************************************************
-
-    viable_fallback::viable_fallback(solver& s):
-        s(s) {
-        m_usolver_factory = mk_univariate_bitblast_factory();
-    }
-
-    void viable_fallback::push_var(unsigned bit_width) {
-        m_constraints.push_back({});
-    }
-
-    void viable_fallback::pop_var() {
-        m_constraints.pop_back();
-    }
-
-    void viable_fallback::push_constraint(pvar v, signed_constraint const& c) {
-        // v is the only unassigned variable in c.
-        SASSERT(c->vars().size() == 1 || !s.is_assigned(v));
-        DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); });
-        m_constraints[v].push_back(c);
-        m_constraints_trail.push_back(v);
-        s.m_trail.push_back(trail_instr_t::viable_constraint_i);
-    }
-
-    void viable_fallback::pop_constraint() {
-        pvar v = m_constraints_trail.back();
-        m_constraints_trail.pop_back();
-        m_constraints[v].pop_back();
-    }
-
-    signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar 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(a.contains(w)); });
-            if (c.is_currently_false(a)) {
-                LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c));
-                return c;
-            }
-            SASSERT(c.is_currently_true(a));
-        }
-        return {};
-    }
-
-    univariate_solver* viable_fallback::usolver(unsigned bit_width) {
-        univariate_solver* us;
-
-        auto it = m_usolver.find_iterator(bit_width);
-        if (it != m_usolver.end()) {
-            us = it->m_value.get();
-            us->pop(1);
-        }
-        else {
-            auto& mk_solver = *m_usolver_factory;
-            m_usolver.insert(bit_width, mk_solver(bit_width));
-            us = m_usolver[bit_width].get();
-        }
-        SASSERT_EQ(us->scope_level(), 0);
-
-        // push once on the empty solver so we can reset it before the next use
-        us->push();
-
-        return us;
-    }
-
-    find_t viable_fallback::find_viable(pvar v, rational& out_val) {
-        unsigned const bit_width = s.m_size[v];
-        univariate_solver* us = usolver(bit_width);
-
-        auto const& cs = m_constraints[v];
-        for (unsigned i = cs.size(); i-- > 0; ) {
-            signed_constraint const c = cs[i];
-            LOG("Univariate constraint: " << c);
-            c.add_to_univariate_solver(v, s, *us, c.blit().to_uint());
-        }
-
-        switch (us->check()) {
-        case l_true:
-            out_val = us->model();
-            // we don't know whether the SMT instance has a unique solution
-            return find_t::multiple;
-        case l_false:
-            s.set_conflict_by_viable_fallback(v, *us);
-            return find_t::empty;
-        default:
-            return find_t::resource_out;
-        }
-    }
-
-    std::ostream& operator<<(std::ostream& out, find_t x) {
-        switch (x) {
-        case find_t::empty:
-            return out << "empty";
-        case find_t::singleton:
-            return out << "singleton";
-        case find_t::multiple:
-            return out << "multiple";
-        case find_t::resource_out:
-            return out << "resource_out";
-        }
-        UNREACHABLE();
-        return out;
-    }
-
 }
-

src/math/polysat/viable.h

@@ -452,37 +452,4 @@ namespace polysat {
         return v.v.display(out, v.var);
     }
 
-    class viable_fallback {
-        friend class viable;
-
-        solver& s;
-
-        scoped_ptr<univariate_solver_factory>   m_usolver_factory;
-        u_map<scoped_ptr<univariate_solver>>    m_usolver;  // univariate solver for each bit width
-        vector<signed_constraints>              m_constraints;
-        svector<unsigned>                       m_constraints_trail;
-
-        univariate_solver* usolver(unsigned bit_width);
-
-    public:
-        viable_fallback(solver& s);
-
-        // declare and remove var
-        void push_var(unsigned bit_width);
-        void pop_var();
-
-        // add/remove constraints stored in the fallback solver
-        void push_constraint(pvar v, signed_constraint const& c);
-        void pop_constraint();
-
-        // Check whether all constraints for 'v' are satisfied;
-        // or find an arbitrary violated constraint.
-        bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
-        signed_constraint find_violated_constraint(assignment const& a, pvar v);
-
-        find_t find_viable(pvar v, rational& out_val);
-    };
-
 }
-
-

src/math/polysat/viable_fallback.cpp

@@ -0,0 +1,132 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    viable fallback to univariate solvers
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+Notes:
+
+TODO: improve management of the fallback univariate solvers:
+      - use a solver pool and recycle the least recently used solver
+      - incrementally add/remove constraints
+      - set resource limit of univariate solver
+
+--*/
+
+
+#include "util/debug.h"
+#include "math/polysat/viable_fallback.h"
+#include "math/polysat/solver.h"
+#include "math/polysat/univariate/univariate_solver.h"
+
+namespace polysat {
+
+    viable_fallback::viable_fallback(solver& s):
+        s(s) {
+        m_usolver_factory = mk_univariate_bitblast_factory();
+    }
+
+    void viable_fallback::push_var(unsigned bit_width) {
+        m_constraints.push_back({});
+    }
+
+    void viable_fallback::pop_var() {
+        m_constraints.pop_back();
+    }
+
+    void viable_fallback::push_constraint(pvar v, signed_constraint const& c) {
+        // v is the only unassigned variable in c.
+        SASSERT(c->vars().size() == 1 || !s.is_assigned(v));
+        DEBUG_CODE(for (pvar w : c->vars()) { if (v != w) SASSERT(s.is_assigned(w)); });
+        m_constraints[v].push_back(c);
+        m_constraints_trail.push_back(v);
+        s.m_trail.push_back(trail_instr_t::viable_constraint_i);
+    }
+
+    void viable_fallback::pop_constraint() {
+        pvar v = m_constraints_trail.back();
+        m_constraints_trail.pop_back();
+        m_constraints[v].pop_back();
+    }
+
+    signed_constraint viable_fallback::find_violated_constraint(assignment const& a, pvar 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(a.contains(w)); });
+            if (c.is_currently_false(a)) {
+                LOG(assignment_pp(s, v, a.value(v)) << " violates constraint " << lit_pp(s, c));
+                return c;
+            }
+            SASSERT(c.is_currently_true(a));
+        }
+        return {};
+    }
+
+    univariate_solver* viable_fallback::usolver(unsigned bit_width) {
+        univariate_solver* us;
+
+        auto it = m_usolver.find_iterator(bit_width);
+        if (it != m_usolver.end()) {
+            us = it->m_value.get();
+            us->pop(1);
+        }
+        else {
+            auto& mk_solver = *m_usolver_factory;
+            m_usolver.insert(bit_width, mk_solver(bit_width));
+            us = m_usolver[bit_width].get();
+        }
+        SASSERT_EQ(us->scope_level(), 0);
+
+        // push once on the empty solver so we can reset it before the next use
+        us->push();
+
+        return us;
+    }
+
+    find_t viable_fallback::find_viable(pvar v, rational& out_val) {
+        unsigned const bit_width = s.m_size[v];
+        univariate_solver* us = usolver(bit_width);
+
+        auto const& cs = m_constraints[v];
+        for (unsigned i = cs.size(); i-- > 0; ) {
+            signed_constraint const c = cs[i];
+            LOG("Univariate constraint: " << c);
+            c.add_to_univariate_solver(v, s, *us, c.blit().to_uint());
+        }
+
+        switch (us->check()) {
+        case l_true:
+            out_val = us->model();
+            // we don't know whether the SMT instance has a unique solution
+            return find_t::multiple;
+        case l_false:
+            s.set_conflict_by_viable_fallback(v, *us);
+            return find_t::empty;
+        default:
+            return find_t::resource_out;
+        }
+    }
+
+    std::ostream& operator<<(std::ostream& out, find_t x) {
+        switch (x) {
+        case find_t::empty:
+            return out << "empty";
+        case find_t::singleton:
+            return out << "singleton";
+        case find_t::multiple:
+            return out << "multiple";
+        case find_t::resource_out:
+            return out << "resource_out";
+        }
+        UNREACHABLE();
+        return out;
+    }
+
+}
+

src/math/polysat/viable_fallback.h

@@ -0,0 +1,52 @@
+/*++
+Copyright (c) 2021 Microsoft Corporation
+
+Module Name:
+
+    viable_fallback to univariate solvers
+    (bit-blasting or int-blasting over a single variable)
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-03-19
+    Jakob Rath 2021-04-06
+
+--*/
+#pragma once
+
+#include "math/polysat/viable.h"
+
+namespace polysat {
+
+    class viable_fallback {
+        friend class viable;
+
+        solver& s;
+
+        scoped_ptr<univariate_solver_factory>   m_usolver_factory;
+        u_map<scoped_ptr<univariate_solver>>    m_usolver;  // univariate solver for each bit width
+        vector<signed_constraints>              m_constraints;
+        svector<unsigned>                       m_constraints_trail;
+
+        univariate_solver* usolver(unsigned bit_width);
+
+    public:
+        viable_fallback(solver& s);
+
+        // declare and remove var
+        void push_var(unsigned bit_width);
+        void pop_var();
+
+        // add/remove constraints stored in the fallback solver
+        void push_constraint(pvar v, signed_constraint const& c);
+        void pop_constraint();
+
+        // Check whether all constraints for 'v' are satisfied;
+        // or find an arbitrary violated constraint.
+        bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
+        signed_constraint find_violated_constraint(assignment const& a, pvar v);
+
+        find_t find_viable(pvar v, rational& out_val);
+    };
+
+}