Speedup for AND/OR with lots of sharing to fix the testcase of 1667. Thanks to Carste...

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 45288527dfdd7fa04f96870bed77276bc79028d7..fe26ad8390704b54454e2ba4bc325f70eb6ef480 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -44,7 +44,7 @@ namespace BEEV
   // NB: The boolean value is always true!
   bool BVTypeCheck(const ASTNode& n);
   
- long getCurrentTime();
+  long getCurrentTime();
 
   ASTVec FlattenKind(Kind k, const ASTVec &children);
 
@@ -82,6 +82,8 @@ namespace BEEV
     ASTNode::ASTNodeHasher, 
     ASTNode::ASTNodeEqual> ASTNodeToVecMap;
 
+  void FlattenKindNoDuplicates(const Kind k, const ASTVec &children, ASTVec & flat_children, ASTNodeSet& alreadyFlattened);
+
   //Needed for defining the MAP below
   struct ltint
   {

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index aecb98c4cfb4768b6dd4a28ceb48e384d21f3e2d..d33be74a00df51b624c84dcf9981046cfa8e2a63 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -13,7 +13,7 @@
 
 namespace BEEV
 {
-  
+
   /****************************************************************
    * Universal Helper Functions                                   *
    ****************************************************************/
@@ -235,7 +235,7 @@ namespace BEEV
     exit(-1);
 
   }
-  
+
   void SortByExprNum(ASTVec& v)
   {
     sort(v.begin(), v.end(), exprless);
@@ -248,12 +248,12 @@ namespace BEEV
 
   bool isAtomic(Kind kind)
   {
-    if (TRUE == kind  || FALSE == kind || 
+    if (TRUE == kind  || FALSE == kind ||
         EQ == kind    ||
-        BVLT == kind  || BVLE == kind  || 
-        BVGT == kind  || BVGE == kind  || 
-        BVSLT == kind || BVSLE == kind || 
-        BVSGT == kind || BVSGE == kind || 
+        BVLT == kind  || BVLE == kind  ||
+        BVGT == kind  || BVGE == kind  ||
+        BVSLT == kind || BVSLE == kind ||
+        BVSGT == kind || BVSGE == kind ||
         SYMBOL == kind || BVGETBIT == kind)
       return true;
     return false;
@@ -303,7 +303,33 @@ namespace BEEV
                }
 }
 
-  void FlattenKind(const Kind k, const ASTVec &children, ASTVec & flat_children)
+  /* Maintains a set of nodes that have already been seen. So that deeply shared AND,OR operations are not
+   * flattened multiple times.
+   */
+  void
+  FlattenKindNoDuplicates(const Kind k, const ASTVec &children, ASTVec & flat_children, ASTNodeSet& alreadyFlattened)
+  {
+    const ASTVec::const_iterator ch_end = children.end();
+    for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
+      {
+        const Kind ck = it->GetKind();
+        if (k == ck)
+          {
+            if (alreadyFlattened.find(*it) == alreadyFlattened.end())
+              {
+                alreadyFlattened.insert(*it);
+                FlattenKindNoDuplicates(k, it->GetChildren(), flat_children,alreadyFlattened);
+              }
+          }
+        else
+          {
+            flat_children.push_back(*it);
+          }
+      }
+  }
+
+  void
+  FlattenKind(const Kind k, const ASTVec &children, ASTVec & flat_children)
   {
     ASTVec::const_iterator ch_end = children.end();
     for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
@@ -311,7 +337,7 @@ namespace BEEV
         Kind ck = it->GetKind();
         if (k == ck)
           {
-            FlattenKind(k,it->GetChildren(), flat_children);
+            FlattenKind(k, it->GetChildren(), flat_children);
           }
         else
           {
@@ -324,7 +350,13 @@ namespace BEEV
   ASTVec FlattenKind(Kind k, const ASTVec &children)
   {
     ASTVec flat_children;
-    FlattenKind(k,children,flat_children);
+    if (k == OR || k == BVOR || k == BVAND || k == AND)
+      {
+        ASTNodeSet alreadyFlattened;
+        FlattenKindNoDuplicates(k,children,flat_children,alreadyFlattened);
+      }
+    else
+      FlattenKind(k,children,flat_children);
     return flat_children;
   }