Improvement. Add a simple read over write simplification to the simplifying node...

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index cea9846afbed84fcf5a2a17088340bddd091541b..c3bf3bda4ba9f22ed1eb23a184c04a29b425754c 100644 (file)
--- 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 75ddeabd20fa1934bd6c966109c0659bb3aa1791..e96cd3dc6e187b96aba878d4f651b06357d3eb61 100644 (file)
--- 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: