From a2f1e5041ddbc0db823741897b8ed7c6a5914cbf Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 13 Mar 2011 23:24:15 +0000
Subject: [PATCH] Improvement. Add a simple read over write simplification to
 the simplifying node factory.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1208 e59a4935-1847-0410-ae03-e826735625c1
---
 .../NodeFactory/SimplifyingNodeFactory.cpp    | 46 +++++++++++++++++++
 src/AST/NodeFactory/SimplifyingNodeFactory.h  |  1 +
 2 files changed, 47 insertions(+)

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index cea9846..c3bf3bd 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -433,6 +433,44 @@ ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children)
 	return retval;
 }
 
+// Move reads down through writes until, either we hit a write to an identical (syntactically) index,
+// or we hit a write to an index that might be the same. This is intended to simplify things like:
+// read(write(write(A,1,2),2,3),4) cheaply.
+// The "children" that are passed should be the children of a READ.
+ASTNode SimplifyingNodeFactory::chaseRead(const ASTVec& children, unsigned int width)
+{
+	assert(children[0].GetKind() == BEEV::WRITE);
+	const ASTNode& readIndex = children[1];
+	ASTNode write = children[0];
+
+	const bool read_is_const = (BEEV::BVCONST == readIndex.GetKind());
+
+	while (write.GetKind() == BEEV::WRITE)
+	{
+		const ASTNode& write_index = write[1];
+
+		if (readIndex == write_index)
+		{
+			// The are definately the same.
+			//cerr << "-";
+			return write[2];
+		}
+		else if (read_is_const && BEEV::BVCONST == write_index.GetKind())
+		{
+			// They are definately different. Ignore this.
+			//cerr << "+";
+		}else
+		{
+			// They may be the same. Exit.
+			//cerr << "#";
+			break;
+		}
+		write = write[0];
+	}
+	return hashing.CreateTerm(BEEV::READ, width, write,readIndex);
+}
+
+
 ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		const ASTVec &children)
 {
@@ -490,6 +528,14 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		}
 	}
 	break;
+
+	case BEEV::READ:
+	if (children[0].GetKind() == BEEV::WRITE)
+	{
+		result = chaseRead(children,width);
+	}
+	break;
+
 	default: // quieten compiler.
 		break;
 	}
diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.h b/src/AST/NodeFactory/SimplifyingNodeFactory.h
index 75ddeab..e96cd3d 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.h
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.h
@@ -48,6 +48,7 @@ private:
 	SimplifyingNodeFactory(const SimplifyingNodeFactory& );
 	SimplifyingNodeFactory& operator=(const SimplifyingNodeFactory&);
 
+	ASTNode chaseRead(const ASTVec& children, unsigned int width );
 
 public:
 
-- 
2.47.3