fix build

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

src/math/polysat/CMakeLists.txt

@@ -2,6 +2,7 @@ z3_add_component(polysat
   SOURCES
     constraint.cpp
     eq_constraint.cpp
+    bit_constraint.cpp
     justification.cpp
     log.cpp
     solver.cpp

src/math/polysat/bit_constraint.cpp

@@ -13,6 +13,7 @@ Author:
 --*/
 
 #include "math/polysat/bit_constraint.h"
+#include "math/polysat/solver.h"
 
 namespace polysat {
 
@@ -20,7 +21,6 @@ namespace polysat {
         if (!m_value)
             out << "~";
         out << "v" << m_var << "[" << m_index << "] ";
-        }
         return out;
     }
 
@@ -39,19 +39,11 @@ namespace polysat {
     }
 
     bool bit_constraint::is_currently_false(solver& s) {
-        return false;
+        return m_viable[m_var].is_false();
     }
 
     void bit_constraint::narrow(solver& s) {
-        bdd viable = s.m_bdd.mk_true();
+        s.intersect_viable(m_var, m_value ? s.m_bdd.mk_var(m_index) : s.m_bdd.mk_nvar(m_index));
-        if (m_value)
-            viable &= s.m_bdd.mk_var(m_index);
-        else 
-            viable &= s.m_bdd.mk_nvar(m_index);
-        s.push_viable(v);
-        s.m_viable[v] &= viable;
-        if (s.m_viable[v].is_false()) 
-            s.set_conflict(v);
     }
 
 }

src/math/polysat/solver.cpp

@@ -43,13 +43,14 @@ namespace polysat {
     void solver::intersect_viable(pvar v, bdd vals) {
         push_viable(v);
         m_viable[v] &= vals;
+        if (m_viable[v].is_false())
+            set_conflict(v);
     }
 
     dd::find_int_t solver::find_viable(pvar v, rational & val) {
         return m_viable[v].find_int(size(v), val);
     }
     
-    
     solver::solver(reslimit& lim): 
         m_lim(lim),
         m_bdd(1000),

src/math/polysat/solver.h

@@ -37,6 +37,7 @@ namespace polysat {
         };
 
         friend class eq_constraint;
+        friend class bit_constraint;
 
         typedef ptr_vector<constraint> constraints;