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 d47bb7a7b71c9658ffc6f10b8173172fa8b4aa65..ebd16acc6f6214c80d72bbfc2e42655b3c806676 100644 (file)
--- 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)