From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 7 Apr 2011 14:36:10 +0000 (+0000)
Subject: Improvement. When a node is simplified set a value so that we can avoid simplifying... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=18db9fa6368eec716140fd946d294b6f43edbce5;p=francis%2Fstp.git

Improvement. When a node is simplified set a value so that we can avoid simplifying it later.


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

diff --git a/src/AST/ASTInternal.h b/src/AST/ASTInternal.h
index 31910b4..e4bfb63 100644
--- a/src/AST/ASTInternal.h
+++ b/src/AST/ASTInternal.h
@@ -175,6 +175,18 @@ namespace BEEV
       return _node_num;
     } //End of GetNodeNum()
 
+
+    virtual bool isSimplified() const
+    {
+      return false;
+    }
+
+    virtual void hasBeenSimplified() const
+    {
+      cerr << "astinternal has been";
+    }
+
+
     void SetNodeNum(int nn)
     {
       _node_num = nn;
diff --git a/src/AST/ASTInternalWithChildren.h b/src/AST/ASTInternalWithChildren.h
index c744dcb..d1e9339 100644
--- a/src/AST/ASTInternalWithChildren.h
+++ b/src/AST/ASTInternalWithChildren.h
@@ -16,6 +16,9 @@ namespace BEEV
     // The vector of children
     ASTVec _children;
 
+    /// todo. This should be a bitfield in a superclass if it can fit without increasing the sizeof..
+    mutable bool is_simplified;
+
   public:
 
     virtual ASTVec const &GetChildren() const
@@ -23,16 +26,28 @@ namespace BEEV
       return _children;
     }
 
+    bool isSimplified() const
+    {
+      return is_simplified;
+    }
+
+    void hasBeenSimplified() const
+    {
+      is_simplified =true;
+    }
+
     // Constructor (kind and children).
     ASTInternalWithChildren(Kind kind, const ASTVec &children, int nodenum = 0) :
       ASTInternal(kind,nodenum), _children(children)
     {
+      is_simplified = false;
     }
 
     // Constructor (kind only, empty children, int nodenum)
     ASTInternalWithChildren(Kind kind, int nodenum = 0) :
       ASTInternal(kind,nodenum)
     {
+      is_simplified = false;
     }
   }; //End of Class ASTInternalBase
 }; //end of namespace
diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp
index 26bad1d..c5bc09c 100644
--- a/src/AST/ASTNode.cpp
+++ b/src/AST/ASTNode.cpp
@@ -217,6 +217,19 @@ namespace BEEV
       }
   } //End of NFASTPrint()
 
+  bool
+  ASTNode::isSimplfied() const
+  {
+    return _int_node_ptr->isSimplified();
+  }
+
+  void
+  ASTNode::hasBeenSimplfied() const
+  {
+    _int_node_ptr->hasBeenSimplified();
+  }
+
+
   //traverse "*this", and construct "let variables" for terms that
   //occur more than once in "*this".
   void ASTNode::LetizeNode(void) const
diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h
index e83ce2d..b050a51 100644
--- a/src/AST/ASTNode.h
+++ b/src/AST/ASTNode.h
@@ -147,6 +147,10 @@ namespace BEEV
     	return (k == BVCONST || k == TRUE || k == FALSE);
     }
 
+    bool isSimplfied() const;
+
+    void hasBeenSimplfied() const;
+
 
     bool isITE() const
 	{
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index ecc4c22..3b02959 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -67,6 +67,14 @@ namespace BEEV
       {
         return false;
       }
+
+    if (!pushNeg && key.isSimplfied())
+      {
+        output = key;
+        return true;
+      }
+
+
     ASTNodeMap::iterator it, itend;
     it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
     itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end();
@@ -106,11 +114,16 @@ namespace BEEV
     // to cache.
     if (0 == key.Degree())
       return;
-    
+
     if (pushNeg)
       (*SimplifyNegMap)[key] = value;
     else
       (*SimplifyMap)[key] = value;
+
+    if (!pushNeg && key == value)
+      {
+        key.hasBeenSimplfied();
+      }
   }
 
   // Substitution Map methods....
@@ -1661,6 +1674,9 @@ namespace BEEV
     if (n.isConstant())
       return true;
 
+    if (n.isSimplfied())
+      return true;
+
     //If it's a symbol that's not in the substitition Map.
     if (n.GetKind() == SYMBOL && CheckSubstitutionMap(n))
       return false;