Add a new function to replace using the substitution/solver map. It's not currently...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@878 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 88b3b0bbc4e1a355f47a67a2beeec6368a6f0fce..2e368d3758eaecad00ce343471aefb786fcb75f6 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -145,4 +145,99 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
   return output;
 } //end of CreateSubstitutionMap()
 
+
+ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
+{
+       ASTNodeMap cache;
+       return replace(n,SolverMap,cache);
+}
+
+// NOTE the fromTo map is changed as we traverse downwards.
+// We call replace on each of the things in the fromTo map aswell.
+// This is in case we have a fromTo map: (x maps to y), (y maps to 5),
+// and pass the replace() function the node "x" to replace, then it
+// will return 5, rather than y.
+
+ASTNode SubstitutionMap::replace(const ASTNode& n, ASTNodeMap& fromTo,
+               ASTNodeMap& cache)
+{
+       ASTNodeMap::const_iterator it;
+       if ((it = cache.find(n)) != cache.end())
+               return it->second;
+
+       if ((it = fromTo.find(n)) != fromTo.end())
+       {
+               if (n.GetIndexWidth() != 0)
+               {
+                       const ASTNode& r = it->second;
+                       r.SetIndexWidth(n.GetIndexWidth());
+                       assert(BVTypeCheck(r));
+                       ASTNode replaced = replace(r, fromTo, cache);
+                       if (replaced != r)
+                               fromTo[n] = replaced;
+
+                       return replaced;
+               }
+               ASTNode replaced = replace(it->second, fromTo, cache);
+               if (replaced != it->second)
+                       fromTo[n] = replaced;
+
+               return replaced;
+       }
+
+       // These can't be created like regular nodes are. Skip 'em for now.
+       if (n.isConstant() || n.GetKind() == SYMBOL /*|| n.GetKind() == WRITE*/)
+               return n;
+
+       ASTVec children;
+       children.reserve(n.GetChildren().size());
+       for (unsigned i = 0; i < n.GetChildren().size(); i++)
+       {
+               children.push_back(replace(n[i], fromTo, cache));
+       }
+
+       // This code short-cuts if the children are the same. Nodes with the same children,
+       // won't have necessarily given the same node if the simplifyingNodeFactory is enabled
+       // now, but wasn't enabled when the node was created. Shortcutting saves lots of time.
+
+       ASTNode result;
+       if (n.GetType() == BOOLEAN_TYPE)
+       {
+               assert(children.size() > 0);
+               if (children != n.GetChildren()) // short-cut.
+               {
+                       result = bm->CreateNode(n.GetKind(), children);
+               }
+               else
+                       result = n;
+       }
+       else
+       {
+               assert(children.size() > 0);
+               if (children != n.GetChildren()) // short-cut.
+               {
+                       // If the index and value width aren't saved, they are reset sometimes (??)
+                       const unsigned int indexWidth = n.GetIndexWidth();
+                       const unsigned int valueWidth = n.GetValueWidth();
+                       result = bm->CreateTerm(n.GetKind(), n.GetValueWidth(),
+                                       children);
+                       result.SetValueWidth(valueWidth);
+                       result.SetIndexWidth(indexWidth);
+               }
+               else
+                       result = n;
+       }
+
+       if (n != result)
+       {
+               assert(BVTypeCheck(result));
+               assert(result.GetValueWidth() == n.GetValueWidth());
+               assert(result.GetIndexWidth() == n.GetIndexWidth());
+       }
+
+       cache[n] = result;
+       return result;
+}
+
+
 };

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index dc46d77bff70fa1e56775bb3e0e78ff9b394f75e..df03da09949acc21581768184252312015f5f5df 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -81,6 +81,8 @@ public:
                        return false;
 
                assert(e0 != e1); // One side should be a variable, the other a constant.
+               assert(e0.GetValueWidth() == e1.GetValueWidth());
+               assert(e0.GetIndexWidth() == e1.GetIndexWidth());
 
                //e0 is of the form READ(Arr,const), and e1 is const, or
                //e0 is of the form var, and e1 is const
@@ -107,6 +109,11 @@ public:
 
        ASTNode CreateSubstitutionMap(const ASTNode& a,   ArrayTransformer*at);
 
+       ASTNode applySubstitutionMap(const ASTNode& n);
+
+       // Replace any nodes in "n" that exist in the fromTo map.
+       // NB the fromTo map is changed.
+       ASTNode replace(const ASTNode& n, ASTNodeMap& fromTo, ASTNodeMap& cache);
 };
 
 }