Separating the subtheory implementations in the bitvector theory.

7 files changed, 264 insertions, 178 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index 8f524c8fc..7748817e3 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -12,7 +12,10 @@ libbv_la_SOURCES = \
 	bitblaster.h \
 	bitblaster.cpp \
 	bv_subtheory.h \
-	bv_subtheory.cpp \
+ 	bv_subtheory_eq.h \
+	bv_subtheory_eq.cpp \
+	bv_subtheory_bitblast.h \
+	bv_subtheory_bitblast.cpp \
 	bitblast_strategies.h \
 	bitblast_strategies.cpp \
 	theory_bv.h \
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index d508976ae..a8813b7aa 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -35,7 +35,6 @@ const bool d_useSatPropagation = true;
 
 // forward declaration 
 class TheoryBV; 
-class Bitblaster;
 
 /**
  * Abstract base class for bit-vector subtheory solvers
@@ -65,78 +64,6 @@ public:
 
 }; 
 
-
-/**
- * BitblastSolver
- */
-class BitblastSolver : public SubtheorySolver {
-
-  /** Bitblaster */
-  Bitblaster* d_bitblaster; 
-
-  /** Nodes that still need to be bit-blasted */
-  context::CDQueue<TNode> d_bitblastQueue; 
-
-public:
-  BitblastSolver(context::Context* c, TheoryBV* bv);
-  ~BitblastSolver(); 
-
-  void  preRegister(TNode node);
-  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions);
-  EqualityStatus getEqualityStatus(TNode a, TNode b);
-};
-
-
-/**
- * EqualitySolver
- */
-class EqualitySolver : public SubtheorySolver {
-
-  // NotifyClass: handles call-back from congruence closure module
-
-  class NotifyClass : public eq::EqualityEngineNotify {
-    TheoryBV* d_bv;
-
-  public:
-    NotifyClass(TheoryBV* bv): d_bv(bv) {}
-    bool eqNotifyTriggerEquality(TNode equality, bool value);
-    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
-    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
-    bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
-};
-
-
-  /** The notify class for d_equalityEngine */
-  NotifyClass d_notify;
-
-  /** Equality engine */
-  eq::EqualityEngine d_equalityEngine;
-  
-public:
-
-  EqualitySolver(context::Context* c, TheoryBV* bv);
-
-  void  preRegister(TNode node);
-  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
-  void  explain(TNode literal, std::vector<TNode>& assumptions);
-  void  addSharedTerm(TNode t) {
-    d_equalityEngine.addTriggerTerm(t, THEORY_BV);
-  }
-  EqualityStatus getEqualityStatus(TNode a, TNode b) {
-    if (d_equalityEngine.areEqual(a, b)) {
-      // The terms are implied to be equal
-      return EQUALITY_TRUE;
-    }
-    if (d_equalityEngine.areDisequal(a, b)) {
-      // The terms are implied to be dis-equal
-      return EQUALITY_FALSE;
-    }
-    return EQUALITY_UNKNOWN; 
-  }
-}; 
-
-
 }
 }
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
new file mode 100644
index 000000000..ff0fc2b1a
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file bv_subtheory_eq_bitblast.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: dejan
+ ** 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 Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#include "theory/bv/bv_subtheory_bitblast.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/bitblaster.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
+  : SubtheorySolver(c, bv),
+    d_bitblaster(new Bitblaster(c, bv)),
+    d_bitblastQueue(c)
+{}
+
+BitblastSolver::~BitblastSolver() {
+  delete d_bitblaster;
+}
+
+void BitblastSolver::preRegister(TNode node) {
+  if ((node.getKind() == kind::EQUAL ||
+       node.getKind() == kind::BITVECTOR_ULT ||
+       node.getKind() == kind::BITVECTOR_ULE ||
+       node.getKind() == kind::BITVECTOR_SLT ||
+       node.getKind() == kind::BITVECTOR_SLE) &&
+      !d_bitblaster->hasBBAtom(node)) {
+    d_bitblastQueue.push_back(node);
+  }
+}
+
+void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  d_bitblaster->explain(literal, assumptions);
+}
+
+bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
+  BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+
+  //// Eager bit-blasting
+  if (Options::current()->bitvectorEagerBitblast) {
+    for (unsigned i = 0; i < assertions.size(); ++i) {
+      TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
+      if (atom.getKind() != kind::BITVECTOR_BITOF) {
+        d_bitblaster->bbAtom(atom);
+      }
+    }
+    return true;
+  }
+
+  //// Lazy bit-blasting
+
+  // bit-blast enqueued nodes
+  while (!d_bitblastQueue.empty()) {
+    TNode atom = d_bitblastQueue.front();
+    d_bitblaster->bbAtom(atom);
+    d_bitblastQueue.pop();
+  }
+
+  // propagation
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    TNode fact = assertions[i];
+    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) {
+      // Some atoms have not been bit-blasted yet
+      d_bitblaster->bbAtom(fact);
+      // Assert to sat
+      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
+      if (!ok) {
+        std::vector<TNode> conflictAtoms;
+        d_bitblaster->getConflict(conflictAtoms);
+        d_bv->setConflict(mkConjunction(conflictAtoms));
+        return false;
+      }
+    }
+  }
+
+  // solving
+  if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
+    Assert(!d_bv->inConflict());
+    BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
+    bool ok = d_bitblaster->solve();
+    if (!ok) {
+      std::vector<TNode> conflictAtoms;
+      d_bitblaster->getConflict(conflictAtoms);
+      Node conflict = mkConjunction(conflictAtoms);
+      d_bv->setConflict(conflict);
+      return false;
+    }
+  }
+
+  return true;
+}
+
+EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
+  return d_bitblaster->getEqualityStatus(a, b);
+}
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
new file mode 100644
index 000000000..0a8f046b7
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file bv_subtheory_eq_bitblast.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: dejan
+ ** 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 Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#pragma once
+
+#include "theory/bv/bv_subtheory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+class Bitblaster;
+
+/**
+ * BitblastSolver
+ */
+class BitblastSolver : public SubtheorySolver {
+
+  /** Bitblaster */
+  Bitblaster* d_bitblaster;
+
+  /** Nodes that still need to be bit-blasted */
+  context::CDQueue<TNode> d_bitblastQueue;
+
+public:
+  BitblastSolver(context::Context* c, TheoryBV* bv);
+  ~BitblastSolver();
+
+  void  preRegister(TNode node);
+  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  void  explain(TNode literal, std::vector<TNode>& assumptions);
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+};
+
+}
+}
+}
diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index fa36236c9..807d90137 100644
--- a/src/theory/bv/bv_subtheory.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file bv_subtheory.cpp
+/*! \file bv_subtheory_eq.cpp
  ** \verbatim
  ** Original author: lianah
- ** Major contributors: 
+ ** Major contributors: dejan
  ** 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)
@@ -11,113 +11,22 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
+ ** \brief Algebraic solver.
  **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** Algebraic solver.
  **/
 
-#include "theory/bv/bv_subtheory.h"
+#include "theory/bv/bv_subtheory_eq.h"
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
-#include "theory/bv/bitblaster.h"
-
 
+using namespace std;
 using namespace CVC4;
+using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
-using namespace CVC4::context;
-
-using namespace std;
 using namespace CVC4::theory::bv::utils;
 
-
-BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
-  : SubtheorySolver(c, bv), 
-    d_bitblaster(new Bitblaster(c, bv)),
-    d_bitblastQueue(c)
-{}
-
-BitblastSolver::~BitblastSolver() {
-  delete d_bitblaster; 
-}
-
-void BitblastSolver::preRegister(TNode node) {
-  if ((node.getKind() == kind::EQUAL ||
-       node.getKind() == kind::BITVECTOR_ULT ||
-       node.getKind() == kind::BITVECTOR_ULE ||
-       node.getKind() == kind::BITVECTOR_SLT ||
-       node.getKind() == kind::BITVECTOR_SLE) &&
-      !d_bitblaster->hasBBAtom(node)) {
-    d_bitblastQueue.push_back(node); 
-  }
-}
-
-void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
-  d_bitblaster->explain(literal, assumptions); 
-}
-
-bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
-  BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
-
-  //// Eager bit-blasting
-  if (Options::current()->bitvectorEagerBitblast) {
-    for (unsigned i = 0; i < assertions.size(); ++i) {
-      TNode atom = assertions[i].getKind() == kind::NOT ? assertions[i][0] : assertions[i];
-      if (atom.getKind() != kind::BITVECTOR_BITOF) {
-        d_bitblaster->bbAtom(atom);
-      }
-    }
-    return true; 
-  }
-
-  //// Lazy bit-blasting
-    
-  // bit-blast enqueued nodes
-  while (!d_bitblastQueue.empty()) {
-    TNode atom = d_bitblastQueue.front();
-    d_bitblaster->bbAtom(atom);
-    d_bitblastQueue.pop(); 
-  }
-
-  // propagation
-  for (unsigned i = 0; i < assertions.size(); ++i) {
-    TNode fact = assertions[i];
-    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) {
-      // Some atoms have not been bit-blasted yet
-      d_bitblaster->bbAtom(fact);
-      // Assert to sat
-      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
-      if (!ok) {
-        std::vector<TNode> conflictAtoms;
-        d_bitblaster->getConflict(conflictAtoms);
-        d_bv->setConflict(mkConjunction(conflictAtoms)); 
-        return false; 
-      }
-    }
-  }
-
-  // solving
-  if (e == Theory::EFFORT_FULL || Options::current()->bitvectorEagerFullcheck) {
-    Assert(!d_bv->inConflict());
-    BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n"; 
-    bool ok = d_bitblaster->solve();
-    if (!ok) {
-      std::vector<TNode> conflictAtoms;
-      d_bitblaster->getConflict(conflictAtoms);
-      Node conflict = mkConjunction(conflictAtoms);
-      d_bv->setConflict(conflict); 
-      return false; 
-    }
-  }
-
-  return true; 
-}
-
-EqualityStatus BitblastSolver::getEqualityStatus(TNode a, TNode b) {
-  return d_bitblaster->getEqualityStatus(a, b);
-}
-
 EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_notify(bv),
@@ -180,12 +89,12 @@ void EqualitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 }
 
 bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
-  BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n"; 
+  BVDebug("bitvector::equality") << "EqualitySolver::addAssertions \n";
   Assert (!d_bv->inConflict());
-  
+
   for (unsigned i = 0; i < assertions.size(); ++i) {
     TNode fact = assertions[i];
-    
+
     // Notify the equality engine
     if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::SUB_EQUALITY) ) {
       bool negated = fact.getKind() == kind::NOT;
@@ -206,13 +115,13 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
       }
     }
 
-    // checking for a conflict 
+    // checking for a conflict
     if (d_bv->inConflict()) {
       return false;
     }
   }
-  
-  return true; 
+
+  return true;
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
diff --git a/src/theory/bv/bv_subtheory_eq.h b/src/theory/bv/bv_subtheory_eq.h
new file mode 100644
index 000000000..241dd5919
--- /dev/null
+++ b/src/theory/bv/bv_subtheory_eq.h
@@ -0,0 +1,78 @@
+/*********************                                                        */
+/*! \file bv_subtheory_eq.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: dejan
+ ** 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 Algebraic solver.
+ **
+ ** Algebraic solver.
+ **/
+
+#pragma once
+
+#include "theory/bv/bv_subtheory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/**
+ * Bitvector equality solver
+ */
+class EqualitySolver : public SubtheorySolver {
+
+  // NotifyClass: handles call-back from congruence closure module
+
+  class NotifyClass : public eq::EqualityEngineNotify {
+    TheoryBV* d_bv;
+
+  public:
+    NotifyClass(TheoryBV* bv): d_bv(bv) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+    bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
+};
+
+
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
+
+  /** Equality engine */
+  eq::EqualityEngine d_equalityEngine;
+
+public:
+
+  EqualitySolver(context::Context* c, TheoryBV* bv);
+
+  void  preRegister(TNode node);
+  bool  addAssertions(const std::vector<TNode>& assertions, Theory::Effort e);
+  void  explain(TNode literal, std::vector<TNode>& assumptions);
+  void  addSharedTerm(TNode t) {
+    d_equalityEngine.addTriggerTerm(t, THEORY_BV);
+  }
+  EqualityStatus getEqualityStatus(TNode a, TNode b) {
+    if (d_equalityEngine.areEqual(a, b)) {
+      // The terms are implied to be equal
+      return EQUALITY_TRUE;
+    }
+    if (d_equalityEngine.areDisequal(a, b)) {
+      // The terms are implied to be dis-equal
+      return EQUALITY_FALSE;
+    }
+    return EQUALITY_UNKNOWN;
+  }
+};
+
+
+}
+}
+}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 214fa3b36..9c27f62c5 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -29,6 +29,8 @@
 #include "util/stats.h"
 #include "context/cdqueue.h"
 #include "theory/bv/bv_subtheory.h"
+#include "theory/bv/bv_subtheory_eq.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
 
 namespace CVC4 {
 namespace theory {