added some extra options to the bit-vector theory

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 8374a3f75f4e29e06abab4cfa80e1c609f354276..1c6920236e27f664b5e214bd06f83a1281d9d505 100644 (file)
--- 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 2308f36a3a76db6a4a92aeb28f8c181f42244701..244d87233f202b85280f8a5b489f5e4ff784f872 100644 (file)
--- 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 819b3d62c8d7687c0f21e5b33836496951895884..315254c8e22fe8ea369c964713aa3074adbe34a8 100644 (file)
--- 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 c0546f892c5d4e13eea7155f41048d8a5b3dc491..f7209d32671ae8bfd4e6bc645fc82d6ebf1ac5f0 100644 (file)
--- 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 7b87baa217bf2a627ca6547c642431b151d16536..077299d1fcaa9b6a64bed4406d58ba51e70ecdab 100644 (file)
--- 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 4803fd62e680955484f6feaeaba0c9995d287f66..224359952aeacd0da62d20f508081980ae640f18 100644 (file)
--- 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);
     }