equality status for bitvectors can now look into the sat solver to check for IN_MODEL...

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index 6b59b9b0066b5b526426505c1c41ccec94fda79f..d512847d59daab82fe83067b2c2c8a9c4944aea1 100644 (file)
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -110,31 +110,19 @@ void Bitblaster::bbAtom(TNode node) {
 
 
 void Bitblaster::bbTerm(TNode node, Bits& bits) {
+
   if (hasBBTerm(node)) {
     getBBTerm(node, bits);
     return;
   }
+
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numTerms;
 
-  Node optimized = bbOptimize(node); 
-
-  // if we already bitblasted the optimized version 
-  if(hasBBTerm(optimized)) {
-    getBBTerm(optimized, bits);
-    // cache it as the same for this node
-    cacheTermDef(node, bits);
-    return; 
-  }
-  
-  d_termBBStrategies[optimized.getKind()] (optimized, bits,this);
+  d_termBBStrategies[node.getKind()] (node, bits,this);
   
-  Assert (bits.size() == utils::getSize(node) &&
-          bits.size() == utils::getSize(optimized));
+  Assert (bits.size() == utils::getSize(node));
 
-  if(optimized != node) {
-    cacheTermDef(optimized, bits);
-  }
   cacheTermDef(node, bits); 
 }
 
@@ -306,7 +294,7 @@ void Bitblaster::initTermBBStrategies() {
 
 }
  
-bool Bitblaster::hasBBAtom(TNode atom) {
+bool Bitblaster::hasBBAtom(TNode atom) const {
   return d_bitblastedAtoms.find(atom) != d_bitblastedAtoms.end();
 }
 
@@ -315,15 +303,14 @@ void Bitblaster::cacheTermDef(TNode term, Bits def) {
   d_termCache[term] = def; 
 }
 
-bool Bitblaster::hasBBTerm(TNode node) {
+bool Bitblaster::hasBBTerm(TNode node) const {
   return d_termCache.find(node) != d_termCache.end(); 
 }
 
-void Bitblaster::getBBTerm(TNode node, Bits& bits) {
-  
+void Bitblaster::getBBTerm(TNode node, Bits& bits) const {
   Assert (hasBBTerm(node)); 
   // copy?
-  bits = d_termCache[node]; 
+  bits = d_termCache.find(node)->second;
 }
 
 Bitblaster::Statistics::Statistics() :
@@ -366,6 +353,43 @@ void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
   }
 };
 
+EqualityStatus Bitblaster::getEqualityStatus(TNode a, TNode b) {
+
+  // We don't want to bit-blast every possibly expensive term for the sake of equality checking
+  if (hasBBTerm(a) && hasBBTerm(b)) {
+
+  Bits a_bits, b_bits;
+  getBBTerm(a, a_bits);
+  getBBTerm(b, b_bits);
+  EqualityStatus status = EQUALITY_TRUE_IN_MODEL;
+  for (unsigned i = 0; i < a_bits.size(); ++ i) {
+    if (d_cnfStream->hasLiteral(a_bits[i]) && d_cnfStream->hasLiteral(b_bits[i])) {
+      SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]);
+      SatValue a_lit_value = d_satSolver->value(a_lit);
+      if (a_lit_value != SAT_VALUE_UNKNOWN) {
+        SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]);
+        SatValue b_lit_value = d_satSolver->value(b_lit);
+        if (b_lit_value != SAT_VALUE_UNKNOWN) {
+          if (a_lit_value != b_lit_value) {
+            return EQUALITY_FALSE_IN_MODEL;
+          }
+        } else {
+          status = EQUALITY_UNKNOWN;
+        }
+      } {
+        status = EQUALITY_UNKNOWN;
+      }
+    } else {
+      status = EQUALITY_UNKNOWN;
+    }
+  }
+
+  return status;
+
+  } else {
+    return EQUALITY_UNKNOWN;
+  }
+}
 
 } /*bv namespace */
 } /* theory namespace */

diff --git a/src/theory/bv/bitblaster.h b/src/theory/bv/bitblaster.h
index 6de84fc01203de2f1106c1b282c62b39f9ba6eab..b27415e0b489485289048bdccc37d78ff077d81d 100644 (file)
--- a/src/theory/bv/bitblaster.h
+++ b/src/theory/bv/bitblaster.h
@@ -33,6 +33,7 @@
 #include "context/cdhashset.h"
 #include "context/cdlist.h"
 
+#include "theory/theory.h"
 #include "theory_bv_utils.h"
 #include "util/stats.h"
 #include "bitblast_strategies.h"
@@ -99,10 +100,10 @@ class Bitblaster {
 
   /// helper methods
   public:
-  bool          hasBBAtom(TNode node);    
+  bool          hasBBAtom(TNode node) const;
   private:
-  bool          hasBBTerm(TNode node); 
-  void          getBBTerm(TNode node, Bits& bits);
+  bool          hasBBTerm(TNode node) const;
+  void          getBBTerm(TNode node, Bits& bits) const;
 
   /// function tables for the various bitblasting strategies indexed by node kind
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
@@ -132,6 +133,8 @@ public:
   void getConflict(std::vector<TNode>& conflict); 
   void explain(TNode atom, std::vector<TNode>& explanation);
 
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+
 private:
 
   

diff --git a/src/theory/bv/bv_subtheory.cpp b/src/theory/bv/bv_subtheory.cpp
index f55d231b21d2e9ca1e06eb34210590bf557fdc97..502d59f8dd0acd25551c463de128562aee8fbef6 100644 (file)
--- a/src/theory/bv/bv_subtheory.cpp
+++ b/src/theory/bv/bv_subtheory.cpp
@@ -114,6 +114,10 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   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),

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index cc62013fd647c0788e4e40ef02f7da82c4d9deaa..db7bad30cb515e449517f313cceba0d0fd2a3094 100644 (file)
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -68,9 +68,7 @@ public:
 
 /**
  * BitblastSolver
- *
  */
-
 class BitblastSolver : public SubtheorySolver {
 
   /** Bitblaster */
@@ -86,14 +84,13 @@ public:
   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
@@ -107,7 +104,7 @@ class EqualitySolver : public SubtheorySolver {
     bool eqNotifyTriggerPredicate(TNode predicate, bool value);
     bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value); 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2);
-  };
+};
 
 
   /** The notify class for d_equalityEngine */
@@ -140,11 +137,6 @@ public:
 }; 
 
 
-// class CoreSolver : public SubtheorySolver {
-  
-// }; 
-
-
 }
 }
 }

diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 26452e5e824534c98d59daef15b18431c15f53b2..79ab955aaf9fc718b34ba4a4735d2d18b43a335c 100644 (file)
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -296,6 +296,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
     return EQUALITY_UNKNOWN;
   }
 
-  return d_equalitySolver.getEqualityStatus(a, b); 
+  EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b);
+  if (status == EQUALITY_UNKNOWN) {
+    status = d_bitblastSolver.getEqualityStatus(a, b);
+  }
+
+  return status;
 }