From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 15 Oct 2011 13:43:22 +0000 (+0000)
Subject: Experimental change. Do an expensive check if the index of the read equals the index... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=46fb837c6c98da2aa3bcc82813aa5655fd4ab1ae;p=francis%2Fstp.git

Experimental change. Do an expensive check if the index of the read equals the index of the write.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index e41ac84..c6bfdee 100644
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -728,6 +728,7 @@ ASTNode SimplifyingNodeFactory::chaseRead(const ASTVec& children, unsigned int w
 	ASTNode write = children[0];
 
 	const bool read_is_const = (BEEV::BVCONST == readIndex.GetKind());
+        ASTVec c(2);
 
 	while (write.GetKind() == BEEV::WRITE)
 	{
@@ -745,9 +746,28 @@ ASTNode SimplifyingNodeFactory::chaseRead(const ASTVec& children, unsigned int w
 			//cerr << "+";
 		}else
 		{
-			// They may be the same. Exit.
+		        // They may be the same. Exit.
+		        // We've finished the cheap tests, now do the expensive one.
+		        // I don't know if the cost of this justifies the benefit.
 			//cerr << "#";
-			break;
+		        c[0] =write_index;
+		        c[1] = readIndex;
+		        ASTNode n = CreateSimpleEQ(c);
+		        if (n == ASTTrue)
+		            {
+		                //cerr << "#";
+		                return write[2];
+		            }
+		        else if (n == ASTFalse)
+		            {
+		                cerr << "!";
+		            }
+		        else
+		            {
+		                //cerr << "."
+		                //Perhaps they are the same, perhaps not.
+		                break;
+		            }
 		}
 		write = write[0];
 	}