From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 24 Jun 2010 14:28:31 +0000 (+0000)
Subject: Add a new function to replace using the substitution/solver map. It's not currently... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=25087498a39d9763d880f527d7b334f7764a1c9a;p=francis%2Fstp.git

Add a new function to replace using the substitution/solver map. It's not currently used by anything. So this checkin does nothing.



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 88b3b0b..2e368d3 100644
--- 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 dc46d77..df03da0 100644
--- 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);
 };
 
 }