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

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 31910b488dc9b790aaf5206e3f89865f6d2a7253..e4bfb637a82c8b8d904e421c6f041aa6a5e1eb8a 100644 (file)
--- 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 c744dcbc234ab81fab28108f780bc25a3520d317..d1e93391c1b174a52e8286e89f8485162ece03f5 100644 (file)
--- 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 26bad1da015bbe16e77ccc08d33e2d746293a2d8..c5bc09c02a46b633ec5a08a66c89ea77715de0a5 100644 (file)
--- 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 e83ce2d19578831aec17f874e757d4c4c7ccb641..b050a51e072826fa4989e96bd36628e7401cd714 100644 (file)
--- 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 ecc4c2230d9e355b612bdff20b541c580ddefba5..3b02959b271e5be351f09003362d4d35440a95bf 100644 (file)
--- 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;