3 files changed, 138 insertions, 4 deletions

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index b2369e2d7..bb0b5ea08 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -4,6 +4,7 @@ UNIT_TESTS = \
 	theory/theory_black \
 	theory/theory_arith_white \
 	theory/union_find_black \
+	theory/theory_bv_white \
 	expr/expr_public \
 	expr/expr_manager_public \
 	expr/node_white \
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 8520dacd8..99e8b087c 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -30,10 +30,10 @@
 #include "prop/prop_engine.h"
 #include "prop/sat.h"
 #include "smt/smt_engine.h"
-#include "theory/registrar.h"
 
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
+#include "theory/theory_registrar.h"
 
 #include "theory/builtin/theory_builtin.h"
 #include "theory/booleans/theory_bool.h"
@@ -45,7 +45,7 @@ using namespace CVC4::prop;
 using namespace std;
 
 /* This fake class relies on the face that a MiniSat variable is just an int. */
-class FakeSatSolver : public SatInputInterface {
+class FakeSatSolver : public SatSolverInterface {
   SatVariable d_nextVar;
   bool d_addClauseCalled;
 
@@ -83,6 +83,23 @@ public:
 
   void interrupt() {
   }
+  
+  SatLiteralValue solve() {
+    return SatValUnknown;
+  }
+
+  SatLiteralValue solve(long unsigned int& resource) {
+    return SatValUnknown;
+  }
+
+  SatLiteralValue value(SatLiteral l) {
+    return SatValUnknown;
+  }
+
+  SatLiteralValue modelValue(SatLiteral l) {
+    return SatValUnknown;
+  }
+
 };
 
 class CnfStreamBlack : public CxxTest::TestSuite {
@@ -117,8 +134,7 @@ class CnfStreamBlack : public CxxTest::TestSuite {
     d_theoryEngine->addTheory<theory::builtin::TheoryBuiltin>(theory::THEORY_BUILTIN);
     d_theoryEngine->addTheory<theory::booleans::TheoryBool>(theory::THEORY_BOOL);
     d_theoryEngine->addTheory<theory::arith::TheoryArith>(theory::THEORY_ARITH);
-    theory::Registrar registrar(d_theoryEngine);
-    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, registrar);
+    d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, new theory::TheoryRegistrar(d_theoryEngine));
   }
 
   void tearDown() {
diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h
new file mode 100644
index 000000000..a158b167f
--- /dev/null
+++ b/test/unit/theory/theory_bv_white.h
@@ -0,0 +1,117 @@
+/*********************                                                        */
+/*! \file theory_bv_white.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+
+#include <cxxtest/TestSuite.h>
+
+#include "theory/theory.h"
+#include "theory/bv/bv_sat.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+
+#include "theory/theory_test_utils.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils; 
+using namespace CVC4::expr;
+using namespace CVC4::context;
+
+using namespace std;
+
+class TheoryBVWhite : public CxxTest::TestSuite {
+
+  Context* d_ctxt;
+  NodeManager* d_nm;
+  NodeManagerScope* d_scope;
+
+  bool debug;
+
+public:
+
+  TheoryBVWhite() : debug(false) {}
+
+
+  void setUp() {
+    d_ctxt = new Context();
+    d_nm = new NodeManager(d_ctxt, NULL);
+    d_scope = new NodeManagerScope(d_nm);
+
+  }
+
+  void tearDown() {
+    delete d_scope;
+    delete d_nm;
+    delete d_ctxt;
+  }
+
+ 
+  void testBitblasterCore() {
+    // ClauseManager tests 
+    Context* ctx = new Context();
+    Bitblaster* bb = new Bitblaster(ctx); 
+    
+    NodeManager* nm = NodeManager::currentNM();
+    // TODO: update this
+    // Node a = nm->mkVar("a", nm->mkBitVectorType(4));
+    // Node b = nm->mkVar("b", nm->mkBitVectorType(4));
+    // Node a1 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(2,1)), a);
+    // Node b1 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(2,1)), b);
+    
+    // Node abeq = nm->mkNode(kind::EQUAL, a, b);
+    // Node neq = nm->mkNode(kind::NOT, abeq);
+    // Node a1b1eq = nm->mkNode(kind::EQUAL, a1, b1);
+    
+    // bb->bitblast(neq);
+    // bb->bitblast(a1b1eq); 
+
+    // /// constructing the rest of the problem 
+    // Node a2 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)), a);
+    // Node b2 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(0,0)), b);
+    // Node eq2 = nm->mkNode(kind::EQUAL, a2, b2); 
+    
+    // Node a3 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(3,3)), a);
+    // Node b3 = nm->mkNode(nm->mkConst<BitVectorExtract>(BitVectorExtract(3,3)), b);
+    // Node eq3 = nm->mkNode(kind::EQUAL, a3, b3);
+
+    // bb->bitblast(eq2);
+    // bb->bitblast(eq3); 
+
+    // ctx->push();
+    // bb->assertToSat(neq);
+    // bb->assertToSat(a1b1eq);
+    // bool res = bb->solve();
+    // TS_ASSERT (res == true);
+
+    // ctx->push();
+    // bb->assertToSat(eq2);
+    // bb->assertToSat(eq3); 
+
+    // res = bb->solve();
+    // TS_ASSERT(res == false); 
+    
+    delete bb;    
+    
+  }
+
+};