From 072b6ca710ebc4d9c7df959752c5b680b3a51fd8 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 10 Jul 2010 09:46:47 +0000
Subject: [PATCH] Speedup. Flatten multiplications, sort, then re-assable into
 2-arity functions. This detects some associativity.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@947 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/simplifier.cpp | 48 ++++++++++++++++++++++++++++++-----
 src/simplifier/simplifier.h   |  3 +++
 2 files changed, 44 insertions(+), 7 deletions(-)

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 4e42875..dab3a50 100644
--- 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 b6dc3cf..fb65b69 100644
--- 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:
       
     /****************************************************************
-- 
2.47.3