From 46fb837c6c98da2aa3bcc82813aa5655fd4ab1ae Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 15 Oct 2011 13:43:22 +0000 Subject: [PATCH] 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 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 24 +++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) 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]; } -- 2.47.3