refactored TheoryBV bitblaster and equality engine into subtheories (similar to TheoryEngine

1 files changed, 247 insertions, 0 deletions

diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp
new file mode 100644
index 000000000..f55d231b2
--- /dev/null
+++ b/src/theory/bv/bv_subtheory.cpp
@@ -0,0 +1,247 @@
+/*********************                                                        */
+/*! \file bv_subtheory.cpp
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: 
+ ** 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 "theory/bv/bv_subtheory.h"
+#include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/bitblaster.h"
+
+
+using namespace CVC4;
+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; 
+}
+
+EqualitySolver::EqualitySolver(context::Context* c, TheoryBV* bv)
+  : SubtheorySolver(c, bv),
+    d_notify(bv),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV")
+{
+  if (d_useEqualityEngine) {
+
+    // The kinds we are treating as function application in congruence
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+    //    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);
+    d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+    //    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);
+  }
+}
+
+void EqualitySolver::preRegister(TNode node) {
+  if (!d_useEqualityEngine)
+    return;
+
+  if (node.getKind() == kind::EQUAL) {
+      d_equalityEngine.addTriggerEquality(node);
+  } else {
+    d_equalityEngine.addTerm(node);
+  }
+}
+
+void EqualitySolver::explain(TNode literal, std::vector<TNode>& assumptions) {
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  if (atom.getKind() == kind::EQUAL) {
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  } else {
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+  }
+}
+
+bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory::Effort e) {
+  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;
+      TNode predicate = negated ? fact[0] : fact;
+      if (predicate.getKind() == kind::EQUAL) {
+        if (negated) {
+          // dis-equality
+          d_equalityEngine.assertEquality(predicate, false, fact);
+        } else {
+          // equality
+          d_equalityEngine.assertEquality(predicate, true, fact);
+        }
+      } else {
+        // Adding predicate if the congruence over it is turned on
+        if (d_equalityEngine.isFunctionKind(predicate.getKind())) {
+          d_equalityEngine.assertPredicate(predicate, !negated, fact);
+        }
+      }
+    }
+
+    // checking for a conflict 
+    if (d_bv->inConflict()) {
+      return false;
+    }
+  }
+  
+  return true; 
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value) {
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  if (value) {
+    return d_bv->storePropagation(equality, TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(equality.notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  if (value) {
+    return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(predicate.notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+  if (value) {
+    return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+  } else {
+    return d_bv->storePropagation(t1.eqNode(t2).notNode(), TheoryBV::SUB_EQUALITY);
+  }
+}
+
+bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+  if (Theory::theoryOf(t1) == THEORY_BOOL) {
+    return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
+  }
+  return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
+}