move tbv

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

src/math/polysat/viable.h

@@ -16,12 +16,18 @@ Author:
 
 #include <limits>
 #include "math/dd/dd_bdd.h"
+#include "math/interval/mod_interval.h"
 #include "math/polysat/types.h"
 
 namespace polysat {
 
     class solver;
 
+    class viable_values : public mod_interval<rational> {
+
+
+    };
+
     class viable {
         typedef dd::bdd bdd;
         solver& s;

src/muz/rel/CMakeLists.txt

@@ -23,7 +23,6 @@ z3_add_component(rel
     doc.cpp
     karr_relation.cpp
     rel_context.cpp
-    tbv.cpp
     udoc_relation.cpp
   COMPONENT_DEPENDENCIES
     muz

src/muz/rel/doc.cpp

@@ -695,12 +695,36 @@ void doc_manager::check_equiv(ast_manager& m, expr* fml1, expr* fml2) {
     SASSERT(res == l_false);
 }
 
+
+expr_ref doc_manager::to_formula(ast_manager & m, tbv const& src) {
+    expr_ref result(m);
+    expr_ref_vector conj(m);
+    for (unsigned i = 0; i < num_tbits(); ++i) {
+        switch (src[i]) {
+        case BIT_0:
+            conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort())));
+            break;
+        case BIT_1:
+            conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort()));
+            break;
+        default:
+            break;            
+        }        
+    }
+    result = mk_and(m, conj.size(), conj.data());
+    return result;    
+}
+
+expr_ref doc_manager::mk_var(ast_manager & m, unsigned i) {
+    return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m);    
+}
+
 expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
     expr_ref result(m);
     expr_ref_vector conj(m);
-    conj.push_back(tbvm().to_formula(m, src.pos()));
+    conj.push_back(to_formula(m, src.pos()));
     for (unsigned i = 0; i < src.neg().size(); ++i) {
-        conj.push_back(m.mk_not(tbvm().to_formula(m, src.neg()[i])));
+        conj.push_back(m.mk_not(to_formula(m, src.neg()[i])));
     }
     result = mk_and(m, conj.size(), conj.data());
     return result;
@@ -712,9 +736,9 @@ void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
     for (unsigned i = 0; i < num_tbits(); ++i) {
         if (to_delete.get(i)) {
             expr_safe_replace rep1(m), rep2(m);
-            rep1.insert(tbvm().mk_var(m, i), m.mk_true());
+            rep1.insert(mk_var(m, i), m.mk_true());
             rep1(fml, tmp1);
-            rep2.insert(tbvm().mk_var(m, i), m.mk_false());
+            rep2.insert(mk_var(m, i), m.mk_false());
             rep2(fml, tmp2);
             if (tmp1 == tmp2) {
                 fml = tmp1;
@@ -731,7 +755,7 @@ void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
     expr_safe_replace rep(m);
     for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
         if (!to_delete.get(i)) {
-            rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
+            rep.insert(mk_var(m, j), mk_var(m, i));
             ++j;
         }
     }

src/muz/rel/doc.h

@@ -22,7 +22,7 @@ Revision History:
 
 #pragma once
 
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 #include "util/union_find.h"
 #include "util/buffer.h"
 
@@ -101,6 +101,8 @@ private:
     void project_rename(expr_ref& fml, bit_vector const& to_delete);
     void project_expand(expr_ref& fml, bit_vector const& to_delete);
     expr_ref to_formula(ast_manager& m, doc const& src);
+    expr_ref to_formula(ast_manager& m, tbv const& src);
+    expr_ref mk_var(ast_manager& m, unsigned i);
     void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
 };
 

src/util/CMakeLists.txt

@@ -54,6 +54,7 @@ z3_add_component(util
     state_graph.cpp
     statistics.cpp
     symbol.cpp
+    tbv.cpp
     timeit.cpp
     timeout.cpp
     trace.cpp

src/util/tbv.cpp

@@ -18,7 +18,7 @@ Revision History:
 
 --*/
 
-#include "muz/rel/tbv.h"
+#include "util/tbv.h"
 #include "util/hashtable.h"
 #include "ast/ast_util.h"
 
@@ -301,26 +301,3 @@ std::ostream& tbv_manager::display(std::ostream& out, tbv const& b) const {
     if (num_tbits() == 0) return out << "[]";
     return display(out, b, num_tbits()-1, 0);
 }
-
-expr_ref tbv_manager::to_formula(ast_manager& m, tbv const& src) {
-    expr_ref result(m);
-    expr_ref_vector conj(m);
-    for (unsigned i = 0; i < num_tbits(); ++i) {
-        switch (src[i]) {
-        case BIT_0:
-            conj.push_back(m.mk_not(m.mk_const(symbol(i), m.mk_bool_sort())));
-            break;
-        case BIT_1:
-            conj.push_back(m.mk_const(symbol(i), m.mk_bool_sort()));
-            break;
-        default:
-            break;
-        }
-    }
-    result = mk_and(m, conj.size(), conj.data());
-    return result;
-}
-
-expr_ref tbv_manager::mk_var(ast_manager& m, unsigned i) {
-    return expr_ref(m.mk_const(symbol(i), m.mk_bool_sort()), m);
-}

src/util/tbv.h

@@ -21,6 +21,7 @@ Revision History:
 #pragma once
 
 #include "util/fixed_bit_vector.h"
+#include "util/bit_vector.h"
 #include "util/rational.h"
 #include "ast/ast.h"
 
@@ -84,10 +85,7 @@ public:
     void set(tbv& dst, tbv const& other, unsigned hi, unsigned lo);
     void set(tbv& dst, unsigned index, tbit value);
 
-
     static void debug_alloc();
-    expr_ref to_formula(ast_manager& m, tbv const& src);
-    expr_ref mk_var(ast_manager& m, unsigned i);
 };
 
 class tbv: private fixed_bit_vector {