Speedup. Flatten multiplications, sort, then re-assable into 2-arity functions. This...

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 4e42875941a34615fe3f4eb2f67e4cfbb1abef5d..dab3a50a24040117062ef50968486c36f48058c3 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1554,7 +1554,7 @@ namespace BEEV
   ASTNode Simplifier::FlattenOneLevel(const ASTNode& a)
   {
     const Kind k = a.GetKind();
-    if (!(BVPLUS == k || AND == k || OR == k
+    if (!(BVPLUS == k || AND == k || OR == k || BVMULT == k
           //|| BVAND == k
           //|| BVOR == k
           ))
@@ -1591,6 +1591,40 @@ namespace BEEV
     return output;
   } //end of flattenonelevel()
 
+
+  ASTNode
+  Simplifier::makeTower(const Kind k, const BEEV::ASTVec &children)
+  {
+    deque<ASTNode> names;
+
+    for (unsigned i = 0; i < children.size(); i++)
+      names.push_back(children[i]);
+
+    while (names.size() > 2)
+      {
+        ASTNode a = names.front();
+        names.pop_front();
+
+        ASTNode b = names.front();
+        names.pop_front();
+
+        ASTNode n = nf->CreateTerm(k, a.GetValueWidth(), a, b);
+        names.push_back(n);
+      }
+
+    // last two now.
+    assert(names.size() == 2);
+
+    ASTNode a = names.front();
+    names.pop_front();
+
+    ASTNode b = names.front();
+    names.pop_front();
+
+    return nf->CreateTerm(k, a.GetValueWidth(), a, b);
+  }
+
+
   //This function simplifies terms based on their kind
   ASTNode 
   Simplifier::SimplifyTerm(const ASTNode& actualInputterm, 
@@ -1711,9 +1745,7 @@ namespace BEEV
         output = inputterm;
         break;
       case BVMULT:
-
-                       assert(2 == inputterm.Degree());
-                       // follow on.
+        // follow on.
       case BVPLUS:
             {
                const ASTNode &n = Flatten(inputterm);
@@ -1852,9 +1884,11 @@ namespace BEEV
                 }
             }
 
-
-
-          if (BVMULT == output.GetKind() || BVPLUS == output.GetKind())
+          if (BVMULT == output.GetKind())
+            {
+              output = makeTower(BVMULT,output.GetChildren());
+            }
+          else  if ( BVPLUS == output.GetKind())
             {
               ASTVec d = output.GetChildren();
               SortByArith(d);

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index b6dc3cf8a320b83242343f2cf28b1980a1aadeca..fb65b69b4dc03b78793cd8cb155dd20d8ff43518 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -54,6 +54,9 @@ namespace BEEV
     SubstitutionMap substitutionMap;
 
     void checkIfInSimplifyMap(const ASTNode& n, ASTNodeSet visited);
+
+    ASTNode makeTower(const Kind k , const ASTVec& children);
+
   public:
       
     /****************************************************************