From af2376e9e4c4e98d9c493c49c73ac97167516359 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 16 Apr 2021 10:00:44 -0700
Subject: [PATCH] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polysat/CMakeLists.txt     |  1 +
 src/math/polysat/bit_constraint.cpp | 20 ++++++--------------
 src/math/polysat/solver.cpp         |  3 ++-
 src/math/polysat/solver.h           |  1 +
 4 files changed, 10 insertions(+), 15 deletions(-)

diff --git a/src/math/polysat/CMakeLists.txt b/src/math/polysat/CMakeLists.txt
index 0a2dd8bca..502f6d5b8 100644
--- a/src/math/polysat/CMakeLists.txt
+++ b/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
diff --git a/src/math/polysat/bit_constraint.cpp b/src/math/polysat/bit_constraint.cpp
index e43c9ccdc..be87b71ea 100644
--- a/src/math/polysat/bit_constraint.cpp
+++ b/src/math/polysat/bit_constraint.cpp
@@ -13,14 +13,14 @@ Author:
 --*/
 
 #include "math/polysat/bit_constraint.h"
+#include "math/polysat/solver.h"
 
 namespace polysat {
 
     std::ostream& bit_constraint::display(std::ostream& out) const {
-            if (!m_value)
-                out << "~";
-            out << "v" << m_var << "[" << m_index << "] ";
-        }
+        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();
-        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);
+        s.intersect_viable(m_var, m_value ? s.m_bdd.mk_var(m_index) : s.m_bdd.mk_nvar(m_index));
     }
 
 }
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 87a94fa62..17236a3a4 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -43,12 +43,13 @@ 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),
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 4414986ac..e85c44f13 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -37,6 +37,7 @@ namespace polysat {
         };
 
         friend class eq_constraint;
+        friend class bit_constraint;
 
         typedef ptr_vector<constraint> constraints;