Speedup. Reduce the number of times that SortByArith is called. Previously:

* If was explicitly called
* Then it was implicitly called when CreateTerm ran.
* Then it was implicitly called again when CombineLikeTerms called CreateTerm.

Remove an unecessary flatten.

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

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 68a494685e1840a4e43a2f5447da89d8a2bf56dd..f8848abd4ac0dce6d8496f546b5f25dd50c54a1f 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -164,8 +164,7 @@ namespace simplifier
       fixedMap = new NodeToFixedBitsMap(1000); // better to use the function that returns the number of nodes.. whatever that is.
       workList = new WorkList(top);
       dependents = new Dependencies(top); // List of the parents of a node.
-      msm = NULL;
-      //msm = new MultiplicationStatsMap();
+      msm = new MultiplicationStatsMap();
 
 
       // not fixing the topnode.
@@ -689,11 +688,10 @@ namespace simplifier
       // safe approximation to no overflow multiplication.
       if (k == BVMULT)
         {
-          //MultiplicationStats ms;
-          //result = bvMultiplyBothWays(children, output, n.GetSTPMgr(),&ms);
-          result = bvMultiplyBothWays(children, output, n.GetSTPMgr());
-          //           if (CONFLICT != result)
-          //                   msm->map[n] = ms;
+          MultiplicationStats ms;
+          result = bvMultiplyBothWays(children, output, n.GetSTPMgr(),&ms);
+                       if (CONFLICT != result)
+                               msm->map[n] = ms;
           mult_like=true;
         }
       else if (k == BVDIV)

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.h b/src/simplifier/constantBitP/ConstantBitPropagation.h
index fbf237f1b230f8d367bcfaacaf3ae3fc6cb9e876..7b8bdd3e8f62feee591b41c297f6914057f1d9cc 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.h
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.h
@@ -38,7 +38,6 @@ namespace simplifier
       Result status;
       WorkList *workList;
       Dependencies * dependents;
-      MultiplicationStatsMap* msm;
 
       bool topFixed;
 
@@ -56,6 +55,7 @@ namespace simplifier
 
 public:
       NodeToFixedBitsMap* fixedMap;
+      MultiplicationStatsMap* msm;
 
       bool isUnsatisfiable()
       {

diff --git a/src/simplifier/constantBitP/MultiplicationStats.h b/src/simplifier/constantBitP/MultiplicationStats.h
index d82c82cebbdfa604a69854415fab0dc2ebc78aa8..8362cddc1c9c5b82992f98c4de6fae1ab7ad51ed 100644 (file)
--- a/src/simplifier/constantBitP/MultiplicationStats.h
+++ b/src/simplifier/constantBitP/MultiplicationStats.h
@@ -112,7 +112,7 @@ namespace simplifier
       void
       print()
       {
-        ostream& log = std::cout;
+        ostream& log = std::cerr;
 
         log << x << " * " << y << "=" << r << endl;
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 67283bb8ff8a3a8bbb6f0f8c340e1c4a7c87c65a..20efa8e88944cfc0dccdfe5dd8bf7f27a78c86a2 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1884,10 +1884,11 @@ namespace BEEV
                   else // pluss.
                     {
                       assert(BVPLUS == k);
-                      SortByArith(nonconstkids);
-                      output = nf->CreateTerm(k, inputValueWidth, nonconstkids);
-                      output = Flatten(output);
-                      output = CombineLikeTerms(output);
+                      //SortByArith(nonconstkids);
+                      //output = nf->CreateTerm(k, inputValueWidth, nonconstkids);
+                      //output = Flatten(output);
+                      //output = CombineLikeTerms(output);
+                      output = CombineLikeTerms(nonconstkids);
                   }
                 }
               else
@@ -2926,8 +2927,13 @@ namespace BEEV
         return output;
       }
 
-    const ASTVec& c = a.GetChildren();
-    //map from variables to vector of constants
+    return CombineLikeTerms(a.GetChildren());
+  }
+
+    ASTNode Simplifier::CombineLikeTerms(const ASTVec& c)
+    {
+      ASTNode output;
+      //map from variables to vector of constants
     ASTNodeToVecMap vars_to_consts;
     //vector to hold constants
     ASTVec constkids;

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 09703753b50672e01c3c9a85f09f734d8220dffb..8a57d287942d34e7ae084e223bbe5c4865c9a9c2 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -210,6 +210,7 @@ namespace BEEV
     ASTNode FlattenAndOr(const ASTNode& a);
 
     ASTNode CombineLikeTerms(const ASTNode& a);
+    ASTNode CombineLikeTerms(const ASTVec& a);
 
     ASTNode LhsMinusRhs(const ASTNode& eq);