Fixing regression failure. The only unfixed ones seem model related which would require some graph coloring algorithm.

8 files changed, 47 insertions, 24 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 91482526a..cc589c5c3 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -92,7 +92,7 @@ void Bitblaster::bbAtom(TNode node) {
   // make sure it is marked as an atom
   addAtom(node); 
 
-  BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
   Node atom_bb = Rewriter::rewrite(d_atomBBStrategies[node.getKind()](node, this));
@@ -115,7 +115,7 @@ void Bitblaster::bbTerm(TNode node, Bits& bits) {
     return;
   }
 
-  BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
+  Debug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numTerms;
 
   d_termBBStrategies[node.getKind()] (node, bits,this);
@@ -195,8 +195,8 @@ bool Bitblaster::assertToSat(TNode lit, bool propagate) {
     markerLit = ~markerLit;
   }
   
-  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
-  BVDebug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat asserting node: " << atom <<"\n";
+  Debug("bitvector-bb") << "TheoryBV::Bitblaster::assertToSat with literal:   " << markerLit << "\n";  
 
   SatValue ret = d_satSolver->assertAssumption(markerLit, propagate);
 
@@ -221,7 +221,7 @@ bool Bitblaster::solve(bool quick_solve) {
       Trace("bitvector") << "     " << d_cnfStream->getNode(*it) << "\n";
     }
   }
-  BVDebug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
+  Debug("bitvector") << "Bitblaster::solve() asserted atoms " << d_assertedAtoms.size() <<"\n"; 
   return SAT_VALUE_TRUE == d_satSolver->solve(); 
 }
 
@@ -412,6 +412,23 @@ bool Bitblaster::isSharedTerm(TNode node) {
   return d_bv->d_sharedTermsSet.find(node) != d_bv->d_sharedTermsSet.end(); 
 }
 
+bool Bitblaster::hasValue(TNode a) {
+  Assert (d_termCache.find(a) != d_termCache.end()); 
+  Bits bits = d_termCache[a];
+  for (int i = bits.size() -1; i >= 0; --i) {
+    SatValue bit_value; 
+    if (d_cnfStream->hasLiteral(bits[i])) { 
+      SatLiteral bit = d_cnfStream->getLiteral(bits[i]);
+      bit_value = d_satSolver->value(bit);
+      if (bit_value == SAT_VALUE_UNKNOWN)
+        return false; 
+    } else {
+      return false; 
+    }
+  }
+  return true; 
+}
+
 Node Bitblaster::getVarValue(TNode a) {
   Assert (d_termCache.find(a) != d_termCache.end()); 
   Bits bits = d_termCache[a];
@@ -436,7 +453,7 @@ void Bitblaster::collectModelInfo(TheoryModel* m) {
   __gnu_cxx::hash_set<TNode, TNodeHashFunction>::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) {
+    if ((Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)) && hasValue(var))  {
       Node const_value = getVarValue(var);
       Debug("bitvector-model") << "Bitblaster::collectModelInfo (assert (= "
                                 << var << " "
diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index fb4394673..84a67e884 100644
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -124,7 +124,8 @@ class Bitblaster {
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
-  void bbUrem(TNode node, Bits& bits); 
+  void bbUrem(TNode node, Bits& bits);
+  bool hasValue(TNode a); 
 public:
   void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
   void bbTerm(TNode node, Bits&  bits);
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index e113048b8..985a9b500 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -53,18 +53,8 @@ void BitblastSolver::explain(TNode literal, std::vector<TNode>& 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::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;
-  }
+  Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions (" << e << ")" << std::endl;
+  Debug("bitvector::bitblaster") << "number of assertions:  " << assertions.size() << std::endl;
 
   //// Lazy bit-blasting
 
@@ -106,7 +96,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   // solving
   if (e == Theory::EFFORT_FULL || options::bitvectorEagerFullcheck()) {
     Assert(!d_bv->inConflict());
-    BVDebug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
+    Debug("bitvector::bitblaster") << "BitblastSolver::addAssertions solving. \n";
     bool ok = d_bitblaster->solve();
     if (!ok) {
       std::vector<TNode> conflictAtoms;
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 1e74f86f2..a3290ff7c 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -157,7 +157,14 @@ bool CoreSolver::addAssertions(const std::vector<TNode>& assertions, Theory::Eff
     if (d_isCoreTheory && !d_slicer->isCoreTerm(fact)) {
       d_isCoreTheory = false; 
     }
-    ok = decomposeFact(fact);
+    
+    // only reason about equalities
+    // FIXME: should we slice when we have the terms in inequalities?
+    if (fact.getKind() == kind::EQUAL || (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL)) {
+      ok = decomposeFact(fact);
+    } else {
+      ok = assertFact(fact, fact); 
+    }
     if (!ok)
       return false; 
   }
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 55402251d..87295e8f6 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -481,6 +481,7 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp) {
     current_low += current_size;
     decomp.push_back(current); 
   }
+  // cache the result
 
   Debug("bv-slicer") << "as [";
   for (unsigned i = 0; i < decomp.size(); ++i) {
diff --git a/src/theory/bv/slicer.h b/src/theory/bv/slicer.h
index f3b16e3d7..b0929d617 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -229,7 +229,8 @@ public:
 class Slicer {
   __gnu_cxx::hash_map<TermId, TNode> d_idToNode;
   __gnu_cxx::hash_map<TNode, TermId, TNodeHashFunction> d_nodeToId;
-  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache; 
+  __gnu_cxx::hash_map<TNode, bool, TNodeHashFunction> d_coreTermCache;
+  __gnu_cxx::hash_map<TNode, std::vector<Node>, TNodeHashFunction> d_decompositionCache; 
   UnionFind d_unionFind;
   ExtractTerm registerTerm(TNode node); 
 public:
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 848063b76..bb4b480d6 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -41,6 +41,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_alreadyPropagatedSet(c),
     d_sharedTermsSet(c),
     d_slicer(),
+    d_bitblastAssertionsQueue(c),
     d_bitblastSolver(c, this),
     d_coreSolver(c, this, &d_slicer),
     d_statistics(),
@@ -117,6 +118,7 @@ void TheoryBV::check(Effort e)
     Assertion assertion = get();
     TNode fact = assertion.assertion;
     new_assertions.push_back(fact);
+    d_bitblastAssertionsQueue.push_back(fact); 
     Debug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n";
   }
 
@@ -128,6 +130,9 @@ void TheoryBV::check(Effort e)
   if (!inConflict() && !d_coreSolver.isCoreTheory()) {
     // sending assertions to the bitblast solver if it's not just core theory 
     d_bitblastSolver.addAssertions(new_assertions, e);
+  } else {
+  // sending assertions to the bitblast solver if it's not just core theory 
+    d_bitblastSolver.addAssertions(new_assertions, EFFORT_STANDARD);
   }
   
   if (inConflict()) {
@@ -140,7 +145,6 @@ void TheoryBV::collectModelInfo( TheoryModel* m, bool fullModel ){
   //  Assert (fullModel); // can only query full model
   d_coreSolver.collectModelInfo(m); 
   d_bitblastSolver.collectModelInfo(m); 
-  
 }
 
 void TheoryBV::propagate(Effort e) {
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index c16e854cc..ec72f40e1 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -47,9 +47,11 @@ class TheoryBV : public Theory {
 
   Slicer         d_slicer;
   
+  context::CDQueue<TNode> d_bitblastAssertionsQueue;
+
   BitblastSolver d_bitblastSolver;
   CoreSolver d_coreSolver;
-
+  
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);