added some extra options to the bit-vector theory

6 files changed, 47 insertions, 46 deletions

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 8374a3f75..1c6920236 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -55,9 +55,6 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
 }
 
 
-const bool d_useEqualityEngine = true;
-const bool d_useSatPropagation = true;
-
 // forward declaration 
 class TheoryBV; 
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 2308f36a3..244d87233 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -34,7 +34,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
     d_bitblaster(new Bitblaster(c, bv)),
     d_bitblastQueue(c),
     d_statistics(),
-    d_validModelCache(c, true)
+    d_validModelCache(c, true),
+    d_useSatPropagation(options::bvPropagate())
 {}
 
 BitblastSolver::~BitblastSolver() {
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 819b3d62c..315254c8e 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -47,6 +47,7 @@ class BitblastSolver : public SubtheorySolver {
   context::CDO<bool> d_validModelCache;
   Node getModelValueRec(TNode node);
 
+  bool  d_useSatPropagation; 
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c0546f892..f7209d326 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -37,40 +37,38 @@ CoreSolver::CoreSolver(context::Context* c, TheoryBV* bv)
     d_isCoreTheory(c, true),
     d_reasons(c)
 {
-  if (d_useEqualityEngine) {
 
-    // The kinds we are treating as function application in congruence
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
-    d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
-    //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
-  }
+  // The kinds we are treating as function application in congruence
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT, true);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT, true);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS, true);
+  d_equalityEngine.addFunctionKind(kind::BITVECTOR_EXTRACT, true);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+  //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
 }
 
 CoreSolver::~CoreSolver() {
@@ -81,9 +79,6 @@ void CoreSolver::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 }
 
 void CoreSolver::preRegister(TNode node) {
-  if (!d_useEqualityEngine)
-    return;
-
   if (node.getKind() == kind::EQUAL) {
       d_equalityEngine.addTriggerEquality(node);
       if (options::bitvectorCoreSolver()) {
@@ -291,7 +286,7 @@ void CoreSolver::buildModel() {
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine 
-  if (d_useEqualityEngine && !d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+  if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
     bool negated = fact.getKind() == kind::NOT;
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 7b87baa21..077299d1f 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -22,5 +22,11 @@ option bitvectorCoreSolver --bv-core-solver bool
 
 option bvToBool --bv-to-bool bool
  lift bit-vectors of size 1 to booleans when possible
+
+option bvPropagate --bv-propagate bool :default true
+ use bit-vector propagation in the bit-blaster
+
+option bvEquality --bv-eq bool :default true
+ use the equality engine for the bit-vector theory
  
 endmodule
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4803fd62e..224359952 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -49,10 +49,11 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
   {
-    SubtheorySolver* core_solver = new CoreSolver(c, this); 
-    d_subtheories.push_back(core_solver);
-    d_subtheoryMap[SUB_CORE] = core_solver;
-
+    if (options::bvEquality()) {
+      SubtheorySolver* core_solver = new CoreSolver(c, this); 
+      d_subtheories.push_back(core_solver);
+      d_subtheoryMap[SUB_CORE] = core_solver;
+    }
     if (options::bitvectorInequalitySolver()) {
       SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
       d_subtheories.push_back(ineq_solver);
@@ -366,7 +367,7 @@ Node TheoryBV::explain(TNode node) {
 void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
-  if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
+  if (!options::bitvectorEagerBitblast() && options::bvEquality()) {
     for (unsigned i = 0; i < d_subtheories.size(); ++i) {
       d_subtheories[i]->addSharedTerm(t);
     }