From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 13 Aug 2010 06:05:05 +0000 (+0000)
Subject: Speedup. Reduce the number of times that SortByArith is called. Previously:
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=655304903a7899571a888808752002fabb520b86;p=francis%2Fstp.git

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 68a4946..f8848ab 100644
--- 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 fbf237f..7b8bdd3 100644
--- 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 d82c82c..8362cdd 100644
--- 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 67283bb..20efa8e 100644
--- 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 0970375..8a57d28 100644
--- 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);