interleave linear solver calls

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

src/math/polysat/linear_solver.cpp

@@ -13,12 +13,13 @@ Author:
 --*/
 
 #include "math/polysat/linear_solver.h"
+#include "math/polysat/solver.h"
 
 namespace polysat {
 
     void linear_solver::push() {}
     void linear_solver::pop(unsigned n) {}
-    void linear_solver::internalize_constraint(constraint& c) {}
+    void linear_solver::new_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) {}

src/math/polysat/linear_solver.h

@@ -32,8 +32,10 @@ Author:
 
 namespace polysat {
 
+    class solver;
+
     class linear_solver {
-        reslimit&                m_lim;
+        solver&                  s;
         ptr_vector<fixplex_base> m_fix;
         unsigned_vector          m_var2ext;
         unsigned_vector          m_ext2var;
@@ -45,13 +47,13 @@ namespace polysat {
         // removing rows from fixplex
         //
     public:
-        linear_solver(reslimit& lim):
-            m_lim(lim)
+        linear_solver(solver& s):
+            s(s) 
         {}
 
         void push();
         void pop(unsigned n); 
-        void internalize_constraint(constraint& c);
+        void new_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);

src/math/polysat/solver.cpp

@@ -68,6 +68,7 @@ namespace polysat {
     
     solver::solver(reslimit& lim): 
         m_lim(lim),
+        m_linear_solver(*this),
         m_bdd(1000),
         m_dm(m_value_manager, m_alloc),
         m_free_vars(m_activity) {
@@ -155,6 +156,7 @@ namespace polysat {
     void solver::new_constraint(constraint* c) {
         SASSERT(c);
         LOG("New constraint: " << *c);
+        m_linear_solver.new_constraint(*c);
         m_constraints.push_back(c);
         SASSERT(!get_bv2c(c->bvar()));
         insert_bv2c(c->bvar(), c);
@@ -243,6 +245,7 @@ namespace polysat {
         m_assign_eh_history.push_back(v);
         m_trail.push_back(trail_instr_t::assign_eh_i);
         c->narrow(*this);
+        m_linear_solver.activate_constraint(*c);
     }
 
 
@@ -254,6 +257,13 @@ namespace polysat {
         push_qhead();
         while (can_propagate()) 
             propagate(m_search[m_qhead++].first);
+        switch (m_linear_solver.check()) {
+        case l_false:
+            // TODO extract conflict
+            break;
+        default:
+            break;
+        }
         SASSERT(wlist_invariant());
     }
 
@@ -282,10 +292,12 @@ namespace polysat {
     void solver::push_level() {
         ++m_level;
         m_trail.push_back(trail_instr_t::inc_level_i);
+        m_linear_solver.push();
     }
 
     void solver::pop_levels(unsigned num_levels) {
         LOG("Pop " << num_levels << " levels; current level is " << m_level);
+        m_linear_solver.pop(num_levels);
         while (num_levels > 0) {
             switch (m_trail.back()) {
             case trail_instr_t::qhead_i: {
@@ -422,6 +434,7 @@ namespace polysat {
         m_search.push_back(std::make_pair(v, val));
         m_trail.push_back(trail_instr_t::assign_i);
         m_justification[v] = j; 
+        m_linear_solver.set_value(v, val);
     }
 
     void solver::set_conflict(constraint& c) { 
@@ -777,9 +790,9 @@ namespace polysat {
         cs.append(m_constraints.size(), m_constraints.data());
         cs.append(m_redundant.size(), m_redundant.data());
         for (auto* c : cs) {
-            unsigned num_watches = 0;
+            int64_t num_watches = 0;
             for (auto const& wlist : m_watch) {
-                unsigned n = std::count(wlist.begin(), wlist.end(), c);
+                auto n = std::count(wlist.begin(), wlist.end(), c);
                 VERIFY(n <= 1);  // no duplicates in the watchlist
                 num_watches += n;
             }

src/math/polysat/solver.h

@@ -24,6 +24,7 @@ Author:
 #include "math/polysat/var_constraint.h"
 #include "math/polysat/ule_constraint.h"
 #include "math/polysat/justification.h"
+#include "math/polysat/linear_solver.h"
 #include "math/polysat/trail.h"
 
 namespace polysat {
@@ -43,10 +44,12 @@ namespace polysat {
         friend class var_constraint;
         friend class ule_constraint;
         friend class forbidden_intervals;
+        friend class linear_solver;
 
         typedef ptr_vector<constraint> constraints;
 
         reslimit&                m_lim;
+        linear_solver            m_linear_solver;
         scoped_ptr_vector<dd::pdd_manager> m_pdd;
         scoped_ptr_vector<dd::fdd> m_bits;
         dd::bdd_manager          m_bdd;