fixed getModelValue to only query the value of leaves and evaluate more complex bv...

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index d8a7845445dff5563f537094effed44579865b28..613300f9ee60df72e06b1dda384474092df25d5b 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -31,6 +31,7 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_bitblaster(new Bitblaster(c, bv)),
     d_bitblastQueue(c),
+    d_modelValuesCache(c), 
     d_statistics()
 {}
 
@@ -139,7 +140,61 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node BitblastSolver::getModelValue(TNode node) {
-  Node val = d_bitblaster->getVarValue(node);
+  Debug("bitvector-model") << "BitblastSolver::getModelValue (" << node <<")";
+  std::vector<TNode> stack;
+  __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; 
+  stack.push_back(node);
+
+  while (!stack.empty()) {
+    TNode current = stack.back();
+    stack.pop_back();
+    processed.insert(current);
+    
+    if (d_modelValuesCache.hasSubstitution(current) ||
+        processed.count(current) != 0) {
+      // if it has a subsitution or we have already processed it nothing to do
+      continue; 
+    }
+
+    // see if the node itself has a value in the bit-blaster
+    // this can happen if say select (...) = x has been asserted
+    // to the bit-blaster
+    Node current_val = d_bitblaster->getVarValue(current);
+    if (current_val != Node()) {
+      d_modelValuesCache.addSubstitution(current, current_val); 
+    } else {
+      // if not process all of the children 
+      for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+        TNode child = current[i];
+        if (current[i].getType().isBitVector() &&
+            ( current[i].getKind() == kind::VARIABLE ||
+              current[i].getKind() == kind::STORE ||
+              current[i].getKind() == kind::SKOLEM)) {
+          // we only want the values of variables 
+          Node child_value = d_bitblaster->getVarValue(child);
+          Debug("bitvector-model") << child << " => " << child_value <<"\n"; 
+          if (child_value == Node()) {
+            return Node(); 
+          }
+          d_modelValuesCache.addSubstitution(child, child_value);
+        }
+        stack.push_back(child);
+      }
+    }
+  }
+  
+  Node val = Rewriter::rewrite(d_modelValuesCache.apply(node));
+  Debug("bitvector-model") << " => " << val <<"\n";
   Assert (val != Node() || d_bv->isSharedTerm(node));
+  
+  if (val.getKind() != kind::CONST_BITVECTOR) {
+    // if we could not reduce the value to a constant return Null
+    return Node(); 
+  }
+  
+  if (node != val) {
+    d_modelValuesCache.addSubstitution(node, val);
+  }
+  
   return val; 
 }

diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index 1fab621cded1d592c7a4f3b501569f10dc042aba..d508a83d496aaaa1d2f20b63e61ea82040406c78 100644 (file)
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -19,7 +19,7 @@
 #pragma once
 
 #include "theory/bv/bv_subtheory.h"
-
+#include "theory/substitutions.h"
 namespace CVC4 {
 namespace theory {
 namespace bv {
@@ -40,6 +40,7 @@ class BitblastSolver : public SubtheorySolver {
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
+  SubstitutionMap d_modelValuesCache; 
   Statistics d_statistics; 
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index a1c8f0e9a0d17844e2b7d71cd3edfc9a57261586..c0546f892c5d4e13eea7155f41048d8a5b3dc491 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -387,17 +387,26 @@ void CoreSolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node CoreSolver::getModelValue(TNode var) {
+  // we don't need to evaluate bv expressions and only look at variable values
+  // because this only gets called when the core theory is complete (i.e. no other bv
+  // function symbols are currently asserted)
+  Assert (d_slicer->isCoreTerm(var)); 
+  
+  Debug("bitvector-model") << "CoreSolver::getModelValue (" << var <<")";  
   Assert (isComplete());
   TNode repr = d_equalityEngine.getRepresentative(var);
+  Node result = Node(); 
   if (repr.getKind() == kind::CONST_BITVECTOR) {
-    return repr; 
-  }
-  if (d_modelValues.find(repr) == d_modelValues.end()) {
+    result = repr; 
+  } else if (d_modelValues.find(repr) == d_modelValues.end()) {
     // it may be a shared term that never gets asserted
+    // result is just Null
     Assert(d_bv->isSharedTerm(var));
-    return Node(); 
+  } else {
+    result = d_modelValues[repr]; 
   }
-  return d_modelValues[repr]; 
+  Debug("bitvector-model") << " => " << result <<"\n"; 
+  return result; 
 }
 
 CoreSolver::Statistics::Statistics()

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 40093f0707ef12701830ae44cdec136075fc764f..f45250f5b3c16fa9ff1228df4869214acdb5575c 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -178,13 +178,18 @@ void InequalitySolver::collectModelInfo(TheoryModel* m) {
 }
 
 Node InequalitySolver::getModelValue(TNode var) {
+  Assert (isInequalityOnly(var)); 
+  Debug("bitvector-model") << "InequalitySolver::getModelValue (" << var <<")";  
   Assert (isComplete());
+  Node result = Node(); 
   if (!d_inequalityGraph.hasValueInModel(var)) {
     Assert (d_bv->isSharedTerm(var));
-    return Node(); 
+  } else {
+    BitVector val = d_inequalityGraph.getValueInModel(var);
+    result = utils::mkConst(val);
   }
-  BitVector val = d_inequalityGraph.getValueInModel(var);
-  return utils::mkConst(val); 
+  Debug("bitvector-model") << " => " << result <<"\n";  
+  return result; 
 }
 
 InequalitySolver::Statistics::Statistics()