From: Clark Barrett <barrett@cs.nyu.edu>
Date: Thu, 11 Apr 2013 15:50:41 +0000 (-0400)
Subject: Fixes for getModelVal in bv theory
X-Git-Tag: cvc5-1.0.0~7324
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f9ab7f28104831a05f485c346bf8c997d88975dd;p=cvc5.git

Fixes for getModelVal in bv theory
---

diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 613300f9e..997244c40 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -31,8 +31,8 @@ BitblastSolver::BitblastSolver(context::Context* c, TheoryBV* bv)
   : SubtheorySolver(c, bv),
     d_bitblaster(new Bitblaster(c, bv)),
     d_bitblastQueue(c),
-    d_modelValuesCache(c), 
-    d_statistics()
+    d_statistics(),
+    d_validModelCache(c, true)
 {}
 
 BitblastSolver::~BitblastSolver() {
@@ -88,6 +88,7 @@ bool BitblastSolver::check(Theory::Effort e) {
   // Processing assertions  
   while (!done()) {
     TNode fact = get();
+    d_validModelCache = false;
     Debug("bv-bitblast") << "  fact " << fact << ")\n"; 
     if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
@@ -139,62 +140,46 @@ void BitblastSolver::collectModelInfo(TheoryModel* m) {
   return d_bitblaster->collectModelInfo(m); 
 }
 
-Node BitblastSolver::getModelValue(TNode 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; 
-    }
+Node BitblastSolver::getModelValue(TNode node)
+{
+  if (!d_validModelCache) {
+    d_modelCache.clear();
+    d_validModelCache = true;
+  }
+  return getModelValueRec(node);
+}
 
-    // 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 BitblastSolver::getModelValueRec(TNode node)
+{
+  Node val;
+  if (node.isConst()) {
+    return node;
   }
-  
-  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(); 
+  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 (node != val) {
-    d_modelValuesCache.addSubstitution(node, 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; 
 }
diff --git a/src/theory/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index d508a83d4..819b3d62c 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -40,8 +40,13 @@ class BitblastSolver : public SubtheorySolver {
 
   /** Nodes that still need to be bit-blasted */
   context::CDQueue<TNode> d_bitblastQueue;
-  SubstitutionMap d_modelValuesCache; 
   Statistics d_statistics; 
+
+  typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+  NodeMap d_modelCache;
+  context::CDO<bool> d_validModelCache;
+  Node getModelValueRec(TNode node);
+
 public:
   BitblastSolver(context::Context* c, TheoryBV* bv);
   ~BitblastSolver();