Making getEqualityStatus more powerful for bit-vector theory.

8 files changed, 180 insertions, 121 deletions

diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index ecd7013c7..ea31e3821 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -74,19 +74,22 @@ protected:
   typedef std::vector<T> Bits;
   typedef __gnu_cxx::hash_map <Node, Bits, NodeHashFunction>  TermDefMap;
   typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction>       TNodeSet;
+  typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction>   ModelCache;
 
   typedef void  (*TermBBStrategy) (TNode, Bits&, TBitblaster<T>*);
   typedef T     (*AtomBBStrategy) (TNode, TBitblaster<T>*);
 
   // caches and mappings
-  TermDefMap                   d_termCache;
-
+  TermDefMap d_termCache;
+  ModelCache d_modelCache;
+  
   void initAtomBBStrategies();
   void initTermBBStrategies();
 protected:
   /// function tables for the various bitblasting strategies indexed by node kind
   TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
   AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND]; 
+  virtual Node getModelFromSatSolver(TNode node, bool fullModel) = 0; 
 public:
   TBitblaster(); 
   virtual ~TBitblaster() {}
@@ -97,9 +100,18 @@ public:
   virtual bool hasBBAtom(TNode atom) const = 0;
   virtual void storeBBAtom(TNode atom, T atom_bb) = 0;
   
+  
   bool hasBBTerm(TNode node) const;
   void getBBTerm(TNode node, Bits& bits) const;
-  void storeBBTerm(TNode term, const Bits& bits); 
+  void storeBBTerm(TNode term, const Bits& bits);
+  /**
+   * Return a constant representing the value of a in the  model.
+   * If fullModel is true set unconstrained bits to 0. If not return
+   * NullNode() for a fully or partially unconstrained.
+   *
+   */
+  Node getTermModel(TNode node, bool fullModel);
+  void invalidateModelCache();
 }; 
 
 
@@ -109,7 +121,6 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   typedef std::vector<Node> Bits;
   typedef context::CDList<prop::SatLiteral> AssertionList;
   typedef context::CDHashMap<prop::SatLiteral, std::vector<prop::SatLiteral> , prop::SatLiteralHashFunction> ExplanationMap;
-  
   /** This class gets callbacks from minisat on propagations */
   class MinisatNotify : public prop::BVSatSolverInterface::Notify {
     prop::CnfStream* d_cnf;
@@ -143,9 +154,12 @@ class TLazyBitblaster :  public TBitblaster<Node> {
   TNodeSet d_bbAtoms; 
   AbstractionModule* d_abstraction;
   bool d_emptyNotify;
+
+  context::CDO<bool> d_satSolverFullModel;
   
   void addAtom(TNode atom);
   bool hasValue(TNode a);
+  Node getModelFromSatSolver(TNode a, bool fullModel);  
 public:
   void bbTerm(TNode node, Bits&  bits);
   void bbAtom(TNode node);
@@ -172,14 +186,7 @@ public:
   void setAbstraction(AbstractionModule* abs);
   
   theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
-  /**
-   * Return a constant Node representing the value of a variable
-   * in the current model.
-   * @param a
-   *
-   * @return
-   */
-  Node getVarValue(TNode a, bool fullModel=true);
+
   /**
    * Adds a constant value for each bit-blasted variable in the model.
    *
@@ -245,7 +252,7 @@ class EagerBitblaster : public TBitblaster<Node> {
   TNodeSet d_bbAtoms;
   TNodeSet d_variables;
 
-  Node getVarValue(TNode a, bool fullModel);
+  Node getModelFromSatSolver(TNode a, bool fullModel);
   bool isSharedTerm(TNode node); 
 
 public:
@@ -299,7 +306,7 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> {
   bool hasInput(TNode input);
   void convertToCnfAndAssert();
   void assertToSatSolver(Cnf_Dat_t* pCnf);
-
+  Node getModelFromSatSolver(TNode a, bool fullModel) { Unreachable(); }
 public:
   AigBitblaster();
   ~AigBitblaster();
@@ -387,6 +394,7 @@ template <class T> void TBitblaster<T>::initTermBBStrategies() {
 template <class T>
 TBitblaster<T>::TBitblaster()
   : d_termCache()
+  , d_modelCache()
 {
   initAtomBBStrategies();
   initTermBBStrategies(); 
@@ -407,6 +415,53 @@ void TBitblaster<T>::storeBBTerm(TNode node, const Bits& bits) {
   d_termCache.insert(std::make_pair(node, bits));
 }
 
+template <class T>
+void TBitblaster<T>::invalidateModelCache() {
+  d_modelCache.clear();
+}
+
+template <class T>
+Node TBitblaster<T>::getTermModel(TNode node, bool fullModel) {
+  if (d_modelCache.find(node) != d_modelCache.end())
+    return d_modelCache[node]; 
+
+  if (node.isConst())
+    return node; 
+
+  Node value = getModelFromSatSolver(node, false);
+  if (!value.isNull()) {
+    Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from SatSolver" << node <<" => " << value <<"\n";
+    d_modelCache[node] = value;
+    Assert (value.isConst()); 
+    return value;
+  }
+
+  if (Theory::isLeafOf(node, theory::THEORY_BV)) {
+    // if it is a leaf may ask for fullModel
+    value = getModelFromSatSolver(node, fullModel); 
+    Debug("bv-equality-status")<< "TLazyBitblaster::getTermModel from VarValue" << node <<" => " << value <<"\n";
+    Assert (!value.isNull()); 
+    d_modelCache[node] = value;
+    return value;
+  }
+  Assert (node.getType().isBitVector());
+  
+  NodeBuilder<> nb(node.getKind());
+  if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+    nb << node.getOperator(); 
+  }
+
+  for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+    nb << getTermModel(node[i], fullModel); 
+  }
+  value = nb; 
+  value = Rewriter::rewrite(value);
+  Assert (value.isConst()); 
+  d_modelCache[node] = value;
+  Debug("bv-term-model")<< "TLazyBitblaster::getTermModel Building Value" << node <<" => " << value <<"\n";
+  return value; 
+}
+
 
 } /* bv namespace */
 
diff --git a/src/theory/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 5f35f95e3..b2b4eebdf 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -115,7 +115,7 @@ BVQuickCheck::vars_iterator BVQuickCheck::endVars() {
 }
 
 Node BVQuickCheck::getVarValue(TNode var) {
-  return d_bitblaster->getVarValue(var); 
+  return d_bitblaster->getTermModel(var, true); 
 }
 
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index a2a6e19ac..35542fc68 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -103,6 +103,7 @@ void BitblastSolver::bitblastQueue() {
       // don't bit-blast lemma atoms
       continue;
     }
+    Debug("bitblast-queue") << "Bitblasting atom " << atom <<"\n"; 
     d_bitblaster->bbAtom(atom);
   }
 }
@@ -218,48 +219,45 @@ void BitblastSolver::collectModelInfo(TheoryModel* m, bool fullModel) {
 
 Node BitblastSolver::getModelValue(TNode node)
 {
-  if (!d_validModelCache) {
-    d_modelCache.clear();
-    d_validModelCache = true;
-  }
-  return getModelValueRec(node);
-}
-
-Node BitblastSolver::getModelValueRec(TNode node)
-{
-  Node val;
-  if (node.isConst()) {
-    return node;
-  }
-  NodeMap::iterator it = d_modelCache.find(node);
-  if (it != d_modelCache.end()) {
-    val = (*it).second;
-    Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
-    return val;
-  }
-  if (d_bv->isLeaf(node)) {
-    val = d_bitblaster->getVarValue(node);
-    if (val == Node()) {
-      // If no value in model, just set to 0
-      val = utils::mkConst(utils::getSize(node), (unsigned)0);
-    }
-  } else {
-    NodeBuilder<> valBuilder(node.getKind());
-    if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      valBuilder << node.getOperator();
-    }
-    for (unsigned i = 0; i < node.getNumChildren(); ++i) {
-      valBuilder << getModelValueRec(node[i]);
-    }
-    val = valBuilder;
-    val = Rewriter::rewrite(val);
-  }
-  Assert(val.isConst());
-  d_modelCache[node] = val;
-  Debug("bitvector-model") << node << " => " << val <<"\n";
+  Node val = d_bitblaster->getTermModel(node, false);
   return val;
 }
 
+// Node BitblastSolver::getModelValueRec(TNode node)
+// {
+//   Node val;
+//   if (node.isConst()) {
+//     return node;
+//   }
+//   NodeMap::iterator it = d_modelCache.find(node);
+//   if (it != d_modelCache.end()) {
+//     val = (*it).second;
+//     Debug("bitvector-model") << node << " => (cached) " << val <<"\n";
+//     return val;
+//   }
+//   if (d_bv->isLeaf(node)) {
+//     val = d_bitblaster->getVarValue(node);
+//     if (val == Node()) {
+//       // If no value in model, just set to 0
+//       val = utils::mkConst(utils::getSize(node), (unsigned)0);
+//     }
+//   } else {
+//     NodeBuilder<> valBuilder(node.getKind());
+//     if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+//       valBuilder << node.getOperator();
+//     }
+//     for (unsigned i = 0; i < node.getNumChildren(); ++i) {
+//       valBuilder << getModelValueRec(node[i]);
+//     }
+//     val = valBuilder;
+//     val = Rewriter::rewrite(val);
+//   }
+//   Assert(val.isConst());
+//   d_modelCache[node] = val;
+//   Debug("bitvector-model") << node << " => " << val <<"\n";
+//   return val;
+// }
+
 
 void BitblastSolver::setConflict(TNode conflict) {
   Node final_conflict = conflict;
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 414abdcce..77461163c 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -57,7 +57,7 @@ class BitblastSolver : public SubtheorySolver {
   AbstractionModule* d_abstractionModule;
   BVQuickCheck* d_quickCheck;
   QuickXPlain* d_quickXplain;
-  Node getModelValueRec(TNode node);
+  //  Node getModelValueRec(TNode node);
   void setConflict(TNode conflict); 
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index e8fee00f5..38b9a1a0a 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -156,11 +156,11 @@ bool EagerBitblaster::solve() {
  *
  * @return
  */
-Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
+Node EagerBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   if (!hasBBTerm(a)) {
-    Assert(isSharedTerm(a));
-    return Node();
+    return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
   }
+  
   Bits bits;
   getBBTerm(a, bits);
   Integer value(0);
@@ -171,7 +171,8 @@ Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
       bit_value = d_satSolver->value(bit);
       Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
     } else {
-      // the bit is unconstrainted so we can give it an arbitrary value
+      if (!fullModel) return Node();
+      // unconstrained bits default to false
       bit_value = prop::SAT_VALUE_FALSE;
     }
     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
@@ -182,19 +183,17 @@ Node EagerBitblaster::getVarValue(TNode a, bool fullModel) {
 
 
 void EagerBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
-  TNodeSet::const_iterator it = d_variables.begin();
+  TNodeSet::iterator it = d_variables.begin();
   for (; it!= d_variables.end(); ++it) {
     TNode var = *it;
-    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
-      Node const_value = getVarValue(var, fullModel);
-      if(const_value == Node()) {
-        if( fullModel ){
-          // if the value is unassigned just set it to zero
-          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
-        }
-      }
+    if (d_bv->isLeaf(var) || isSharedTerm(var))  {
+      // only shared terms could not have been bit-blasted
+      Assert (hasBBTerm(var) || isSharedTerm(var));
+      
+      Node const_value = getModelFromSatSolver(var, fullModel);
+      
       if(const_value != Node()) {
-        Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+        Debug("bitvector-model") << "EagerBitblaster::collectModelInfo (assert (= "
                                  << var << " "
                                  << const_value << "))\n";
         m->assertEquality(var, const_value, true);
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index f721a22f0..101d8b082 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -41,6 +41,7 @@ TLazyBitblaster::TLazyBitblaster(context::Context* c, bv::TheoryBV* bv, const st
   , d_bbAtoms()
   , d_abstraction(NULL)
   , d_emptyNotify(emptyNotify)
+  , d_satSolverFullModel(c, false)
   , d_name(name)
   , d_statistics(name) {
   d_satSolver = prop::SatSolverFactory::createMinisat(c, name);
@@ -258,6 +259,7 @@ bool TLazyBitblaster::solve() {
     }
   }
   Debug("bitvector") << "TLazyBitblaster::solve() asserted atoms " << d_assertedAtoms->size() <<"\n";
+  d_satSolverFullModel.set(true); 
   return prop::SAT_VALUE_TRUE == d_satSolver->solve();
 }
 
@@ -354,42 +356,38 @@ void TLazyBitblaster::MinisatNotify::safePoint() {
   d_bv->d_out->safePoint();
 }
 
+
 EqualityStatus TLazyBitblaster::getEqualityStatus(TNode a, TNode b) {
+  Debug("bv-equality-status")<< "TLazyBitblaster::getEqualityStatus " << a <<" = " << b <<"\n";
+  Debug("bv-equality-status")<< "BVSatSolver has full model? " << d_satSolverFullModel.get() <<"\n";
 
-  // 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);
-    theory::EqualityStatus status = theory::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])) {
-        prop::SatLiteral a_lit = d_cnfStream->getLiteral(a_bits[i]);
-        prop::SatValue a_lit_value = d_satSolver->value(a_lit);
-        if (a_lit_value != prop::SAT_VALUE_UNKNOWN) {
-          prop::SatLiteral b_lit = d_cnfStream->getLiteral(b_bits[i]);
-          prop::SatValue b_lit_value = d_satSolver->value(b_lit);
-          if (b_lit_value != prop::SAT_VALUE_UNKNOWN) {
-            if (a_lit_value != b_lit_value) {
-              return theory::EQUALITY_FALSE_IN_MODEL;
-            }
-          } else {
-            status = theory::EQUALITY_UNKNOWN;
-          }
-        } {
-          status = theory::EQUALITY_UNKNOWN;
-        }
-      } else {
-        status = theory::EQUALITY_UNKNOWN;
-      }
-    }
+  // First check if it trivially rewrites to false/true
+  Node a_eq_b = Rewriter::rewrite(utils::mkNode(kind::EQUAL, a, b));
 
-    return status;
+  if (a_eq_b == utils::mkFalse()) return theory::EQUALITY_FALSE;
+  if (a_eq_b == utils::mkTrue()) return theory::EQUALITY_TRUE;
 
-  } else {
-    return theory::EQUALITY_UNKNOWN;
+  if (!d_satSolverFullModel.get())
+    return theory::EQUALITY_UNKNOWN; 
+  
+  // Check if cache is valid (invalidated in check and pops)
+  if (d_bv->d_invalidateModelCache.get()) {
+    invalidateModelCache(); 
   }
+  d_bv->d_invalidateModelCache.set(false); 
+
+  Node a_value = getTermModel(a, true);
+  Node b_value = getTermModel(b, true);
+
+  Assert (a_value.isConst() &&
+          b_value.isConst());
+
+  if (a_value == b_value) {
+    Debug("bv-equality-status")<< "theory::EQUALITY_TRUE_IN_MODEL\n";
+    return theory::EQUALITY_TRUE_IN_MODEL; 
+  }
+  Debug("bv-equality-status")<< "theory::EQUALITY_FALSE_IN_MODEL\n";
+  return theory::EQUALITY_FALSE_IN_MODEL; 
 }
 
 
@@ -424,11 +422,11 @@ bool TLazyBitblaster::hasValue(TNode a) {
  *
  * @return
  */
-Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
+Node TLazyBitblaster::getModelFromSatSolver(TNode a, bool fullModel) {
   if (!hasBBTerm(a)) {
-    Assert(isSharedTerm(a));
-    return Node();
+    return fullModel? utils::mkConst(utils::getSize(a), 0u) : Node();
   }
+  
   Bits bits;
   getBBTerm(a, bits);
   Integer value(0);
@@ -439,7 +437,8 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
       bit_value = d_satSolver->value(bit);
       Assert (bit_value != prop::SAT_VALUE_UNKNOWN);
     } else {
-      // the bit is unconstrainted so we can give it an arbitrary value
+      if (!fullModel) return Node();
+      // unconstrained bits default to false
       bit_value = prop::SAT_VALUE_FALSE;
     }
     Integer bit_int = bit_value == prop::SAT_VALUE_TRUE ? Integer(1) : Integer(0);
@@ -449,23 +448,26 @@ Node TLazyBitblaster::getVarValue(TNode a, bool fullModel) {
 }
 
 void TLazyBitblaster::collectModelInfo(TheoryModel* m, bool fullModel) {
-  TNodeSet::iterator it = d_variables.begin();
-  for (; it!= d_variables.end(); ++it) {
+  std::set<Node> termSet;
+  d_bv->computeRelevantTerms(termSet);
+
+  for (std::set<Node>::const_iterator it = termSet.begin(); it != termSet.end(); ++it) {
     TNode var = *it;
-    if (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var))  {
-      Node const_value = getVarValue(var, fullModel);
-      if(const_value == Node()) {
-        if( fullModel ){
-          // if the value is unassigned just set it to zero
-          const_value = utils::mkConst(BitVector(utils::getSize(var), 0u));
-        }
-      }
-      if(const_value != Node()) {
-        Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
-                                 << var << " "
-                                 << const_value << "))\n";
+    // not actually a leaf of the bit-vector theory
+    if (d_variables.find(var) == d_variables.end())
+      continue;
+    
+    Assert (Theory::theoryOf(var) == theory::THEORY_BV || isSharedTerm(var)); 
+    // only shared terms could not have been bit-blasted
+    Assert (hasBBTerm(var) || isSharedTerm(var));
+    
+    Node const_value = getModelFromSatSolver(var, fullModel);
+    Assert (const_value.isNull() || const_value.isConst()); 
+    if(const_value != Node()) {
+      Debug("bitvector-model") << "TLazyBitblaster::collectModelInfo (assert (= "
+                               << var << " "
+                               << const_value << "))\n";
         m->assertEquality(var, const_value, true);
-      }
     }
   }
 }
@@ -481,7 +483,7 @@ void TLazyBitblaster::clearSolver() {
   d_bbAtoms.clear();
   d_variables.clear();
   d_termCache.clear(); 
-
+  
   // recreate sat solver
   d_satSolver = prop::SatSolverFactory::createMinisat(d_ctx);
   d_cnfStream = new prop::TseitinCnfStream(d_satSolver,
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 4abf25bb1..40bc2417b 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -49,6 +49,7 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel&
     d_staticLearnCache(),
     d_lemmasAdded(c, false),
     d_conflict(c, false),
+    d_invalidateModelCache(c, true),
     d_literalsToPropagate(c),
     d_literalsToPropagateIndex(c, 0),
     d_propagatedBy(c),
@@ -357,7 +358,8 @@ void TheoryBV::checkForLemma(TNode fact) {
 void TheoryBV::check(Effort e)
 {
   Debug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
-
+  // we may be getting new assertions so the model cache may not be sound
+  d_invalidateModelCache.set(true); 
   // if we are using the eager solver
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     // this can only happen on an empty benchmark
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 22d9f6775..a37a4019e 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -141,6 +141,9 @@ private:
   // Are we in conflict?
   context::CDO<bool> d_conflict;
 
+  // Invalidate the model cache if check was called
+  context::CDO<bool> d_invalidateModelCache;
+
   /** The conflict node */
   Node d_conflictNode;