From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 31 Mar 2011 12:39:46 +0000 (+0000)
Subject: Small improvement. Discard the inner write if the two WRITEs are to the same index.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=88b51082e8536c371890181cacecbc5c7e712e1d;p=francis%2Fstp.git

Small improvement. Discard the inner write if the two WRITEs are to the same index.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index d47bb7a..ebd16ac 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -870,6 +870,16 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
 		}
 		break;
 
+        case BEEV::WRITE:
+          if (children[0].GetKind() == BEEV::WRITE)
+          {
+              // If the indexes of two writes are the same, then discard the inner write.
+              if (children[1] == children[0][1])
+              {
+                  result = NodeFactory::CreateArrayTerm(BEEV::WRITE, children[0].GetIndexWidth(), children[0].GetValueWidth(),  children[0][0], children[1], children[2]);
+              }
+          }
+          break;
 
 	case BEEV::READ:
 	if (children[0].GetKind() == BEEV::WRITE)