Speedup. The old Flatten was too slow. On an instance of binary AND nodes 2 million...

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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 9520cfddf7de1387fc2740df710945a1ecad39f2..15079099c7a16d1aa1c7326728e3740d99ecc1a2 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -161,30 +161,28 @@ bool containsArrayOps(const ASTNode&n)
                }
 }
 
-
-  // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)
-  ASTVec FlattenKind(Kind k, const ASTVec &children)
+  void FlattenKind(const Kind k, const ASTVec &children, ASTVec & flat_children)
   {
-    ASTVec flat_children;
-
     ASTVec::const_iterator ch_end = children.end();
     for (ASTVec::const_iterator it = children.begin(); it != ch_end; it++)
       {
         Kind ck = it->GetKind();
         if (k == ck)
           {
-            const ASTVec gchildren = FlattenKind(k,it->GetChildren());
-            //const ASTVec gchildren =  it->GetChildren();
-            // append grandchildren to children
-            flat_children.insert(flat_children.end(),
-                                 gchildren.begin(), gchildren.end());
+            FlattenKind(k,it->GetChildren(), flat_children);
           }
         else
           {
             flat_children.push_back(*it);
           }
       }
+  }
 
+  // Flatten (k ... (k ci cj) ...) to (k ... ci cj ...)
+  ASTVec FlattenKind(Kind k, const ASTVec &children)
+  {
+    ASTVec flat_children;
+    FlattenKind(k,children,flat_children);
     return flat_children;
   }
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 67fe0a3ce20de886efbee6143ba483859a77a5d1..64e829f75b56d53e61ea3e34473fadab5c2699b8 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -27,20 +27,6 @@ namespace BEEV
 // so that's disabled.
   const bool simplify_upfront = true;
 
-  ASTNode Simplifier::Flatten(const ASTNode& a)
-  {
-    ASTNode n = a;
-    while (true)
-      {
-        ASTNode nold = n;
-        n = FlattenOneLevel(n);
-        if ((n == nold))
-          break;
-      }
-        
-    return n;
-  }
-
   // is it ITE(p,bv0[1], bv1[1])  OR  ITE(p,bv0[0], bv1[0])
   bool isPropositionToTerm(const ASTNode& n)
   {
@@ -1071,16 +1057,9 @@ namespace BEEV
     if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
       return output;
 
-    ASTNode flat = Flatten(a);
-    ASTVec c, outvec;
-    c = flat.GetChildren();
+    ASTVec c = FlattenKind(a.GetKind(),a.GetChildren());
     SortByArith(c);
-    Kind k = flat.GetKind();
-
-    // If the simplifying node factory is enabled, a
-    // constant may be returned by Flatten.
-    if (AND !=k && OR !=k)
-       return SimplifyFormula(flat,pushNeg, VarConstMap);
+    Kind k = a.GetKind();
 
     bool isAnd = (k == AND) ? true : false;
 
@@ -1094,6 +1073,8 @@ namespace BEEV
       (pushNeg ? ASTFalse : ASTTrue) : 
       (pushNeg ? ASTTrue : ASTFalse);
 
+    ASTVec outvec;
+
     //do the work
     ASTVec::const_iterator next_it;
     for (ASTVec::const_iterator i = c.begin(), iend = c.end(); i != iend; i++)
@@ -1168,7 +1149,6 @@ namespace BEEV
             (pushNeg ? 
              nf->CreateNode(AND, outvec) :
              nf->CreateNode(OR,outvec));
-          //output = FlattenOneLevel(output);
           break;
         }
       }
@@ -1565,47 +1545,6 @@ namespace BEEV
     return output;
   }
 
-  //one level deep flattening
-  ASTNode Simplifier::FlattenOneLevel(const ASTNode& a)
-  {
-    const Kind k = a.GetKind();
-    if (!(BVPLUS == k || AND == k || OR == k
-          //|| BVAND == k
-          //|| BVOR == k
-          ))
-      {
-        return a;
-      }
-
-    ASTNode output;
-    // if(CheckSimplifyMap(a,output,false)) {
-    //       //check memo table
-    //       //cerr << "output of SimplifyTerm Cache: " << output << endl;
-    //       return output;
-    //     }
-
-    const ASTVec& c = a.GetChildren();
-    ASTVec o;
-    for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
-      {
-        const ASTNode& aaa = *it;
-        if (k == aaa.GetKind())
-          {
-            const ASTVec& ac = aaa.GetChildren();
-            o.insert(o.end(), ac.begin(), ac.end());
-          }
-        else
-          o.push_back(aaa);
-      }
-
-    if (is_Form_kind(k))
-      output = nf->CreateNode(k, o);
-    else
-      output = nf->CreateTerm(k, a.GetValueWidth(), o);
-
-    return output;
-  } //end of flattenonelevel()
-
 
   ASTNode
   Simplifier::makeTower(const Kind k, const BEEV::ASTVec &children)
@@ -2465,10 +2404,10 @@ namespace BEEV
 
           ASTNode identity = (BVAND == k) ? max : zero;
           ASTNode annihilator = (BVAND == k) ? zero : max;
-          ASTVec c = Flatten(inputterm).GetChildren();
+          ASTVec c = FlattenKind(inputterm.GetKind(), inputterm.GetChildren());
           SortByArith(c);
+          ASTVec constants;
           ASTVec o;
-          bool constant = true;
           for (ASTVec::iterator
                  it = c.begin(), itend = c.end(); it != itend; it++)
             {
@@ -2477,12 +2416,6 @@ namespace BEEV
               aaa = SimplifyTerm(aaa);
             assert(hasBeenSimplified(aaa));
 
-
-              if (BVCONST != aaa.GetKind())
-                {
-                  constant = false;
-                }
-
               if (aaa == annihilator)
                 {
                   output = annihilator;
@@ -2508,14 +2441,31 @@ namespace BEEV
                   return output;
               }
 
-
-              if (aaa != identity)
+              if (BVCONST == aaa.GetKind())
+                {
+                  constants.push_back(aaa);
+                }
+              else
                 {
                   o.push_back(aaa);
                 }
-
             }
 
+          while(constants.size() >=2)
+          {
+                 ASTNode a = constants.back();
+                 constants.pop_back();
+                 ASTNode b = constants.back();
+                 constants.pop_back();
+
+                 ASTNode c = BVConstEvaluator(nf->CreateTerm(inputterm.GetKind(),inputterm.GetValueWidth(), a,b));
+
+                 constants.push_back(c);
+
+          }
+          if (constants.size() != 0 && constants.back() != identity)
+                 o.push_back(constants.back());
+
           switch (o.size())
             {
             case 0:
@@ -2526,11 +2476,7 @@ namespace BEEV
               break;
             default:
               SortByArith(o);
-              output = nf->CreateTerm(k, inputValueWidth, o);
-              if (constant)
-                {
-                  output = BVConstEvaluator(output);
-                }
+              output = makeTower(inputterm.GetKind(),o );
               break;
             }
 
@@ -2597,7 +2543,7 @@ namespace BEEV
                                                assert(BVTypeCheck(output));
                                }
                        }
-          break;
+                       break;
         }
       case BVCONCAT:
         {

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 8a57d287942d34e7ae084e223bbe5c4865c9a9c2..0798e2be90c455764dd94ea93106e9b07c298f7b 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -203,11 +203,6 @@ namespace BEEV
     ASTNode SimplifyForFormula(const ASTNode& a,
                                bool pushNeg, ASTNodeMap* VarConstMap=NULL);
 
-    ASTNode Flatten(const ASTNode& a);
-
-    ASTNode FlattenOneLevel(const ASTNode& a);
-
-    ASTNode FlattenAndOr(const ASTNode& a);
 
     ASTNode CombineLikeTerms(const ASTNode& a);
     ASTNode CombineLikeTerms(const ASTVec& a);