na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/polysat/CMakeLists.txt

@@ -2,12 +2,13 @@ z3_add_component(polysat
   SOURCES
     constraint.cpp
     eq_constraint.cpp
-    ule_constraint.cpp
-    var_constraint.cpp
     forbidden_intervals.cpp
     justification.cpp
+    linear_solver.cpp
     log.cpp
     solver.cpp
+    ule_constraint.cpp
+    var_constraint.cpp
   COMPONENT_DEPENDENCIES
     util
     dd

src/math/polysat/fixplex.h

@@ -30,9 +30,11 @@ namespace polysat {
 
     typedef unsigned var_t;
 
+    struct fixplex_base {};
+
 
     template<typename Ext>
-    class fixplex {
+    class fixplex : public fixplex_base {
     public:
         typedef typename Ext::numeral numeral;
         typedef typename Ext::scoped_numeral scoped_numeral;
@@ -137,7 +139,6 @@ namespace polysat {
         void set_bounds(var_t v, numeral const& lo, numeral const& hi);
         void unset_bounds(var_t v) { m_vars[v].set_free(); }
 
-        var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
         numeral const& lo(var_t var) const { return m_vars[var].lo; }
         numeral const& hi(var_t var) const { return m_vars[var].hi; }
         numeral const& value(var_t var) const { return m_vars[var].m_value; }
@@ -149,15 +150,17 @@ namespace polysat {
         vector<var_eq> const& var_eqs() const { return m_var_eqs; }
         void reset_eqs() { m_var_eqs.reset(); }
         lbool make_feasible();
-        row add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
+        void add_row(var_t base, unsigned num_vars, var_t const* vars, numeral const* coeffs);
         std::ostream& display(std::ostream& out) const;
-        std::ostream& display_row(std::ostream& out, row const& r, bool values = true);
         void collect_statistics(::statistics & st) const;
         row get_infeasible_row();
         void del_row(var_t base_var);
 
     private:
 
+        std::ostream& display_row(std::ostream& out, row const& r, bool values = true);
+        var_t get_base_var(row const& r) const { return m_rows[r.id()].m_base; }
+
         void update_value_core(var_t v, numeral const& delta);
         void ensure_var(var_t v);
 

src/math/polysat/fixplex_def.h

@@ -84,8 +84,7 @@ namespace polysat {
     }
 
     template<typename Ext>
-    typename fixplex<Ext>::row 
-    fixplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
+    void fixplex<Ext>::add_row(var_t base_var, unsigned num_vars, var_t const* vars, numeral const* coeffs) {
         for (unsigned i = 0; i < num_vars; ++i) 
             ensure_var(vars[i]);
 
@@ -122,7 +121,6 @@ namespace polysat {
             ++m_stats.m_num_approx;
         SASSERT(well_formed_row(r));
         SASSERT(well_formed());
-        return r;
     }
 
     template<typename Ext>

src/math/polysat/linear_solver.cpp

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2014 Microsoft Corporation
+
+Module Name:
+
+    linear_solver.cpp
+    
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2021-05-14
+    Jakob Rath 2021-05-14
+
+--*/
+
+#include "math/polysat/linear_solver.h"
+
+namespace polysat {
+
+    void linear_solver::push() {}
+    void linear_solver::pop(unsigned n) {}
+    void linear_solver::internalize_constraint(constraint& c) {}
+    void linear_solver::set_value(pvar v, rational const& value) {}
+    void linear_solver::set_bound(pvar v, rational const& lo, rational const& hi) {}
+    void linear_solver::activate_constraint(constraint& c) {}
+    
+    // check integer modular feasibility under current bounds.
+    lbool linear_solver::check() { return l_undef; }
+    void linear_solver::unsat_core(unsigned_vector& deps) {}
+
+    // current value assigned to (linear) variable according to tableau.
+    rational linear_solver::value(pvar v) { return rational(0); }
+    
+};
+

src/math/polysat/linear_solver.h

@@ -13,11 +13,13 @@ Abstract:
     into linear form.
     Equalities, Inequalities are converted into rows and slack variables.
     Slack variables are bounded when constraints are activated.
+    It also handles backtracking state: bounds that are activated inside one 
+    scope are de-activated when exiting the scope.
     
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2021-03-19
-    Jakob Rath 2021-04-6
+    Nikolaj Bjorner (nbjorner) 2021-05-14
+    Jakob Rath 2021-05-14
 
 --*/
 
@@ -47,19 +49,23 @@ namespace polysat {
             m_lim(lim)
         {}
 
-        void push() {}
-        void pop(unsigned n) {}
-        void internalize_constraint(constraint& c) {}
-        void set_value(pvar v, rational const& value) {}
-        void set_bound(pvar v, rational const& lo, rational const& hi) {}
-        void activate_constraint(constraint& c) {}
+        void push();
+        void pop(unsigned n); 
+        void internalize_constraint(constraint& c);
+        void set_value(pvar v, rational const& value);
+        void set_bound(pvar v, rational const& lo, rational const& hi);
+        void activate_constraint(constraint& c);
 
         // check integer modular feasibility under current bounds.
-        lbool check() { return l_undef; }
-        void unsat_core(unsigned_vector& deps) {}
+        lbool check();
+        void unsat_core(unsigned_vector& deps);
 
         // current value assigned to (linear) variable according to tableau.
-        rational value(pvar v) { return rational(0); }
+        rational value(pvar v);
+
+        std::ostream& display(std::ostream& out) const { return out; }
+        void collect_statistics(::statistics & st) const {}
+
     };