cleaned up the bv subtheory interface; added check for inequality theory completeness

9 files changed, 185 insertions, 78 deletions

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 00b3526c0..4389dc50d 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -76,7 +76,7 @@ protected:
   /** The bit-vector theory */
   TheoryBV* d_bv;
   AssertionQueue d_assertionQueue;
-  context::CDO<uint32_t>  d_assertionIndex; 
+  context::CDO<uint32_t>  d_assertionIndex;
 public:
   
   SubtheorySolver(context::Context* c, TheoryBV* bv) :
@@ -93,7 +93,7 @@ public:
   virtual void collectModelInfo(TheoryModel* m) = 0;
   virtual bool isComplete() = 0;
   virtual EqualityStatus getEqualityStatus(TNode a, TNode b) = 0;
-  
+  virtual void addSharedTerm(TNode node) {} 
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
     Assert (!done()); 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 20da2511c..c7387daf8 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -30,13 +30,23 @@ 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)
+    d_bitblastQueue(c),
+    d_statistics()
 {}
 
 BitblastSolver::~BitblastSolver() {
   delete d_bitblaster;
 }
 
+BitblastSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::BitblastSolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+BitblastSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
 void BitblastSolver::preRegister(TNode node) {
   if ((node.getKind() == kind::EQUAL ||
        node.getKind() == kind::BITVECTOR_ULT ||
@@ -54,6 +64,7 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& assumptions) {
 
 
 bool BitblastSolver::check(Theory::Effort e) {
+  ++(d_statistics.d_numCallstoCheck); 
   //// Eager bit-blasting
   if (options::bitvectorEagerBitblast()) {
     while (!done()) {
@@ -77,7 +88,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   // Processing assertions  
   while (!done()) {
     TNode fact = get(); 
-    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
+    if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
       // Assert to sat
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 47bed07dd..b05ac74cd 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -30,13 +30,17 @@ class Bitblaster;
  * BitblastSolver
  */
 class BitblastSolver : public SubtheorySolver {
-
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
   /** Bitblaster */
   Bitblaster* d_bitblaster;
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
-
+  Statistics d_statistics; 
 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 6f5fd4119..ad12681f3 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -192,7 +192,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
 bool CoreSolver::check(Theory::Effort e) {
   Trace("bitvector::core") << "CoreSolver::check \n";
   Assert (!d_bv->inConflict());
-
+  ++(d_statistics.d_numCallstoCheck); 
   bool ok = true; 
   std::vector<Node> core_eqs;
   while (! done()) {
@@ -226,7 +226,7 @@ bool CoreSolver::check(Theory::Effort e) {
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine 
-  if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
+  if (d_useEqualityEngine && !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;
@@ -310,3 +310,12 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
   d_bv->computeRelevantTerms(termSet);
   m->assertEqualityEngine(&d_equalityEngine, &termSet);
 }
+
+CoreSolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::CoreSolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+CoreSolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
diff --git a/src/theory/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 5eb37b50a..4a9d84f79 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -31,7 +31,12 @@ class Base;
  * Bitvector equality solver
  */
 class CoreSolver : public SubtheorySolver {
-
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
+  
   // NotifyClass: handles call-back from congruence closure module
   class NotifyClass : public eq::EqualityEngineNotify {
     CoreSolver& d_solver;
@@ -68,6 +73,7 @@ class CoreSolver : public SubtheorySolver {
   bool assertFactToEqualityEngine(TNode fact, TNode reason);  
   bool decomposeFact(TNode fact);
   Node getBaseDecomposition(TNode a, std::vector<TNode>& explanation);
+  Statistics d_statistics; 
 public: 
   CoreSolver(context::Context* c, TheoryBV* bv);
   ~CoreSolver();
diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 338026681..3d7339e88 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -27,7 +27,9 @@ using namespace CVC4::theory::bv;
 using namespace CVC4::theory::bv::utils;
 
 bool InequalitySolver::check(Theory::Effort e) {
-  Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n"; 
+  Debug("bv-subtheory-inequality") << "InequalitySolveR::check("<< e <<")\n";
+  ++(d_statistics.d_numCallstoCheck);
+  
   bool ok = true; 
   while (!done() && ok) {
     TNode fact = get();
@@ -111,7 +113,36 @@ EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
 
 void InequalitySolver::assertFact(TNode fact) {
   d_assertionQueue.push_back(fact);
-  d_assertionSet.insert(fact); 
+  d_assertionSet.insert(fact);
+  if (!isInequalityOnly(fact)) {
+    d_isComplete = false; 
+  }
+}
+
+bool InequalitySolver::isInequalityOnly(TNode node) {
+  if (d_ineqTermCache.find(node) != d_ineqTermCache.end()) {
+    return d_ineqTermCache[node]; 
+  }
+  
+  if (node.getKind() == kind::NOT) {
+    node = node[0]; 
+  }
+  
+  if (node.getKind() != kind::EQUAL &&
+      node.getKind() != kind::BITVECTOR_ULT &&
+      node.getKind() != kind::BITVECTOR_ULE &&
+      node.getKind() != kind::CONST_BITVECTOR &&
+      node.getKind() != kind::SELECT &&
+      node.getKind() != kind::STORE &&
+      node.getMetaKind() != kind::metakind::VARIABLE) {
+    return false; 
+  }
+  bool res = true; 
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    res = res && isInequalityOnly(node[i]);
+  }
+  d_ineqTermCache[node] = res; 
+  return res; 
 }
 
 void InequalitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
@@ -122,3 +153,12 @@ void InequalitySolver::propagate(Theory::Effort e) {
   Assert (false); 
 }
 
+InequalitySolver::Statistics::Statistics()
+  : d_numCallstoCheck("theory::bv::InequalitySolver::NumCallsToCheck", 0)
+{
+  StatisticsRegistry::registerStat(&d_numCallstoCheck);
+}
+InequalitySolver::Statistics::~Statistics() {
+  StatisticsRegistry::unregisterStat(&d_numCallstoCheck);
+}
+
diff --git a/src/theory/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 6d1d77c7e..bcf94dc8b 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -28,20 +28,32 @@ namespace theory {
 namespace bv {
 
 class InequalitySolver: public SubtheorySolver {
+  struct Statistics {
+    IntStat d_numCallstoCheck;
+    Statistics();
+    ~Statistics(); 
+  }; 
+
   context::CDHashSet<Node, NodeHashFunction> d_assertionSet; 
   InequalityGraph d_inequalityGraph;
+  context::CDO<bool> d_isComplete;
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_ineqTermCache; 
+  bool isInequalityOnly(TNode node); 
+  Statistics d_statistics; 
 public:
-  
   InequalitySolver(context::Context* c, TheoryBV* bv)
     : SubtheorySolver(c, bv),
       d_assertionSet(c),
-      d_inequalityGraph(c)
+      d_inequalityGraph(c),
+      d_isComplete(c, true),
+      d_ineqTermCache(),
+      d_statistics()
   {}
   
   bool check(Theory::Effort e);
   void propagate(Theory::Effort e); 
   void explain(TNode literal, std::vector<TNode>& assumptions);
-  bool isComplete() { return true; }
+  bool isComplete() { return d_isComplete; }
   void collectModelInfo(TheoryModel* m) {}
   EqualityStatus getEqualityStatus(TNode a, TNode b);
   void assertFact(TNode fact); 
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index bdf93eadc..a62324946 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -22,6 +22,9 @@
 #include "theory/bv/bitblaster.h"
 #include "theory/bv/options.h"
 #include "theory/bv/theory_bv_rewrite_rules_normalization.h"
+#include "theory/bv/bv_subtheory_core.h"
+#include "theory/bv/bv_subtheory_inequality.h"
+#include "theory/bv/bv_subtheory_bitblast.h"
 #include "theory/model.h"
 
 using namespace CVC4;
@@ -37,37 +40,57 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_context(c),
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
-    d_coreSolver(c, this),
-    d_inequalitySolver(c, this),
-    d_bitblastSolver(c, this),
+    d_subtheories(),
+    d_subtheoryMap(),
     d_statistics(),
     d_conflict(c, false),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c)
-  {}
-
-TheoryBV::~TheoryBV() {}
+  {
+    SubtheorySolver* core_solver = new CoreSolver(c, this); 
+    d_subtheories.push_back(core_solver);
+    d_subtheoryMap[SUB_CORE] = core_solver;
+
+    SubtheorySolver* ineq_solver = new InequalitySolver(c, this); 
+    d_subtheories.push_back(ineq_solver);
+    d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
+
+    SubtheorySolver* bb_solver = new BitblastSolver(c, this); 
+    d_subtheories.push_back(bb_solver);
+    d_subtheoryMap[SUB_BITBLAST] = bb_solver;
+  }
 
+TheoryBV::~TheoryBV() {
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    delete d_subtheories[i]; 
+  }
+}
 
 void TheoryBV::setMasterEqualityEngine(eq::EqualityEngine* eq) {
-  d_coreSolver.setMasterEqualityEngine(eq);
+  dynamic_cast<CoreSolver*>(d_subtheoryMap[SUB_CORE])->setMasterEqualityEngine(eq);
 }
 
 TheoryBV::Statistics::Statistics():
   d_avgConflictSize("theory::bv::AvgBVConflictSize"),
   d_solveSubstitutions("theory::bv::NumberOfSolveSubstitutions", 0),
-  d_solveTimer("theory::bv::solveTimer")
+  d_solveTimer("theory::bv::solveTimer"),
+  d_numCallsToCheckFullEffort("theory::bv::NumberOfFullCheckCalls", 0),
+  d_numCallsToCheckStandardEffort("theory::bv::NumberOfStandardCheckCalls", 0)
 {
   StatisticsRegistry::registerStat(&d_avgConflictSize);
   StatisticsRegistry::registerStat(&d_solveSubstitutions);
   StatisticsRegistry::registerStat(&d_solveTimer);
+  StatisticsRegistry::registerStat(&d_numCallsToCheckFullEffort);
+  StatisticsRegistry::registerStat(&d_numCallsToCheckStandardEffort);
 }
 
 TheoryBV::Statistics::~Statistics() {
   StatisticsRegistry::unregisterStat(&d_avgConflictSize);
   StatisticsRegistry::unregisterStat(&d_solveSubstitutions);
   StatisticsRegistry::unregisterStat(&d_solveTimer);
+  StatisticsRegistry::unregisterStat(&d_numCallsToCheckFullEffort);
+  StatisticsRegistry::unregisterStat(&d_numCallsToCheckStandardEffort);
 }
 
 
@@ -79,9 +102,9 @@ void TheoryBV::preRegisterTerm(TNode node) {
     // don't use the equality engine in the eager bit-blasting
     return;
   }
-  
-  d_bitblastSolver.preRegister(node);
-  d_coreSolver.preRegister(node);
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    d_subtheories[i]->preRegister(node); 
+  }
 }
 
 void TheoryBV::sendConflict() {
@@ -99,7 +122,11 @@ void TheoryBV::sendConflict() {
 void TheoryBV::check(Effort e)
 {
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
+  if (Theory::fullEffort(e)) {
+    ++(d_statistics.d_numCallsToCheckFullEffort); 
+  } else {
+    ++(d_statistics.d_numCallsToCheckStandardEffort); 
+  }
   // if we are already in conflict just return the conflict
   if (inConflict()) {
     sendConflict();
@@ -108,38 +135,37 @@ void TheoryBV::check(Effort e)
 
   while (!done()) {
     TNode fact = get().assertion;
-    d_coreSolver.assertFact(fact);
-    d_inequalitySolver.assertFact(fact); 
-    d_bitblastSolver.assertFact(fact); 
-  }
-
-  bool ok = true; 
-  if (!inConflict()) {
-    ok = d_coreSolver.check(e); 
+    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+      d_subtheories[i]->assertFact(fact); 
+    }
   }
-  Assert (!ok == inConflict()); 
 
-  if (!inConflict() && !d_coreSolver.isComplete()) {
-    ok = d_inequalitySolver.check(e); 
-  }
+  bool ok = true;
+  bool complete = false;
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    Assert (!inConflict()); 
+    ok = d_subtheories[i]->check(e);
+    complete = d_subtheories[i]->isComplete(); 
 
-  // Assert (!ok == inConflict());
-  // if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-  // if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
-  //   ok = d_bitblastSolver.check(e); 
-  // }
-  
-  Assert (!ok == inConflict()); 
-  if (inConflict()) {
-    sendConflict();
+    if (!ok) {
+      // if we are in a conflict no need to check with other theories
+      Assert (inConflict());
+      sendConflict();
+      return; 
+    }
+    if (complete) {
+      // if the last subtheory was complete we stop
+      return; 
+    }
   }
 }
 
 void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   Assert(!inConflict());
   //  Assert (fullModel); // can only query full model
-  d_coreSolver.collectModelInfo(m); 
-  d_bitblastSolver.collectModelInfo(m); 
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    d_subtheories[i]->collectModelInfo(m); 
+  }
 }
 
 void TheoryBV::propagate(Effort e) {
@@ -255,15 +281,9 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
 
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
-  // Ask the appropriate subtheory for the explanation
-  if (propagatedBy(literal, SUB_CORE)) {
-    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << "): CORE" << std::endl;
-    d_coreSolver.explain(literal, assumptions);
-  } else {
-    Assert(propagatedBy(literal, SUB_BITBLAST));
-    Debug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;
-    d_bitblastSolver.explain(literal, assumptions);
-  }
+  Assert (wasPropagatedBySubtheory(literal));
+  SubTheory sub = getPropagatingSubtheory(literal);
+  d_subtheoryMap[sub]->explain(literal, assumptions);
 }
 
 
@@ -288,7 +308,9 @@ void TheoryBV::addSharedTerm(TNode t) {
   Debug("bitvector::sharing") << indent() << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
   d_sharedTermsSet.insert(t);
   if (!options::bitvectorEagerBitblast() && d_useEqualityEngine) {
-    d_coreSolver.addSharedTerm(t);
+    for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+      d_subtheories[i]->addSharedTerm(t);
+    }
   }
 }
 
@@ -298,15 +320,13 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
   if (options::bitvectorEagerBitblast()) {
     return EQUALITY_UNKNOWN;
   }
-
-  EqualityStatus status = d_coreSolver.getEqualityStatus(a, b);
-  if (status == EQUALITY_UNKNOWN) {
-    status = d_inequalitySolver.getEqualityStatus(a, b); 
-  }
-  if (status == EQUALITY_UNKNOWN) {
-    status = d_bitblastSolver.getEqualityStatus(a, b);
+  
+  for (unsigned i = 0; i < d_subtheories.size(); ++i) {
+    EqualityStatus status = d_subtheories[i]->getEqualityStatus(a, b);
+    if (status != EQUALITY_UNKNOWN) {
+      return status; 
+    }
   }
-
-  return status;
+  return EQUALITY_UNKNOWN; ;
 }
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 54260deb9..5d139e11f 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -26,15 +26,15 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "util/statistics_registry.h"
 #include "theory/bv/bv_subtheory.h"
-#include "theory/bv/bv_subtheory_core.h"
-#include "theory/bv/bv_subtheory_bitblast.h"
-#include "theory/bv/bv_subtheory_inequality.h"
-#include "theory/bv/slicer.h"
 
 namespace CVC4 {
 namespace theory {
 namespace bv {
 
+class CoreSolver;
+class InequalitySolver;
+class BitblastSolver; 
+
 class TheoryBV : public Theory {
 
   /** The context we are using */
@@ -44,9 +44,8 @@ class TheoryBV : public Theory {
   context::CDHashSet<Node, NodeHashFunction> d_alreadyPropagatedSet;
   context::CDHashSet<Node, NodeHashFunction> d_sharedTermsSet;
   
-  CoreSolver       d_coreSolver;
-  InequalitySolver d_inequalitySolver; 
-  BitblastSolver   d_bitblastSolver;
+  std::vector<SubtheorySolver*> d_subtheories;
+  __gnu_cxx::hash_map<SubTheory, SubtheorySolver*, std::hash<int> > d_subtheoryMap; 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
@@ -77,6 +76,8 @@ private:
     AverageStat d_avgConflictSize;
     IntStat     d_solveSubstitutions;
     TimerStat   d_solveTimer;
+    IntStat d_numCallsToCheckFullEffort;
+    IntStat d_numCallsToCheckStandardEffort; 
     Statistics();
     ~Statistics();
   };
@@ -102,10 +103,14 @@ private:
   typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
   PropagatedMap d_propagatedBy;
 
-  bool propagatedBy(TNode literal, SubTheory subtheory) const {
+  bool wasPropagatedBySubtheory(TNode literal) const {
+    return d_propagatedBy.find(literal) != d_propagatedBy.end(); 
+  }
+  
+  SubTheory getPropagatingSubtheory(TNode literal) const {
+    Assert(wasPropagatedBySubtheory(literal)); 
     PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
-    if (find == d_propagatedBy.end()) return false;
-    else return (*find).second == subtheory;
+    return (*find).second;
   }
 
   /** Should be called to propagate the literal.  */