Refactor. Now finised. doing what I broke in r1445/r1446.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 819a1bd5b91b7328a845297ac0d450f025b88dd7..9eec1520b9474637a4e86b09c64917cf1cd90e50 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -83,12 +83,12 @@ namespace BEEV {
   } //End of TopLevelSTP()
   
   ASTNode
-  STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score)
+  STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score)
   {
     while (true)
       {
         ASTNode last = simplified_solved_InputToSAT;
-        simplified_solved_InputToSAT = sizeReducing(last, bvSolver);
+        simplified_solved_InputToSAT = sizeReducing(last, bvSolver,pe);
         if (last == simplified_solved_InputToSAT)
           break;
       }
@@ -114,14 +114,14 @@ namespace BEEV {
 
   // These transformations should never increase the size of the DAG.
    ASTNode
-  STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver)
+  STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe)
   {
-    simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer);
+    simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer);
     if (simp->hasUnappliedSubstitutions())
       {
         simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
         simp->haveAppliedSubstitutionMap();
-        bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
+        bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT);
       }
 
     if (bm->UserFlags.isSet("enable-unconstrained", "1"))
@@ -204,6 +204,7 @@ namespace BEEV {
 
     // A heap object so I can easily control its lifetime.
     BVSolver* bvSolver = new BVSolver(bm, simp);
+    PropagateEqualities * pe = new PropagateEqualities(simp,bm->defaultNodeFactory,bm);
 
     ASTNode simplified_solved_InputToSAT = original_input;
 
@@ -228,7 +229,7 @@ namespace BEEV {
       assert(!arrayops);
 
     // Run size reducing just once.
-    simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver);
+    simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT, bvSolver,pe);
 
     unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
 
@@ -236,7 +237,7 @@ namespace BEEV {
     // Currently we discards all the state each time sizeReducing is called,
     // so it's expensive to call.
     if (!arrayops && initial_difficulty_score < 1000000)
-           simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score);
+           simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver,pe, initial_difficulty_score);
 
     if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
       {
@@ -271,7 +272,7 @@ namespace BEEV {
 
         if (bm->UserFlags.optimize_flag)
           {
-            simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer);
+            simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer);
 
             // Imagine:
             // The simplifier simplifies (0 + T) to T
@@ -287,7 +288,7 @@ namespace BEEV {
                 simp->haveAppliedSubstitutionMap();
               }
 
-            bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+            bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT);
 
             simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
 
@@ -364,7 +365,7 @@ namespace BEEV {
 
         if (bm->UserFlags.optimize_flag)
           {
-            simplified_solved_InputToSAT = simp->topLevel(simplified_solved_InputToSAT, arrayTransformer);
+            simplified_solved_InputToSAT = pe->topLevel(simplified_solved_InputToSAT, arrayTransformer);
 
             if (simp->hasUnappliedSubstitutions())
               {
@@ -372,7 +373,7 @@ namespace BEEV {
                 simp->haveAppliedSubstitutionMap();
               }
 
-            bm->ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+            bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT);
 
             simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
             bm->ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
@@ -474,6 +475,8 @@ namespace BEEV {
     // Deleting it clears out all the buckets associated with hashmaps etc. too.
     delete bvSolver;
     bvSolver = NULL;
+    delete pe;
+    pe = NULL;
 
     if (bm->UserFlags.stats_flag)
       simp->printCacheStatus();

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index ca2d372ffcd2e75200468d07b978173be9e92e74..7c9b7f6662150034fc88925fb589728870e465ad 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -18,6 +18,7 @@
 #include "../to-sat/ASTNode/ToSAT.h"
 #include "../parser/LetMgr.h"
 #include "../absrefine_counterexample/AbsRefine_CounterExample.h"
+#include "../simplifier/PropagateEqualities.h"
 
 namespace BEEV
 {
@@ -25,7 +26,7 @@ namespace BEEV
 
     ArrayTransformer * arrayTransformer;
 
-          ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver);
+          ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver, PropagateEqualities *pe);
 
           // A copy of all the state we need to restore to a prior expression.
           struct Revert_to
@@ -46,7 +47,7 @@ namespace BEEV
 
   public:
           // calls sizeReducing and the bitblasting simplification.
-          ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score);
+          ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score);
 
 
     /****************************************************************

diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h
index 102190809de239d9a63592ad9c9ab651d15a3fb5..831c98e20b63b24c292c2060f7de60dddd5fae46 100644 (file)
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -22,8 +22,11 @@ namespace BEEV
         STPMgr *bm;
         const ASTNode ASTTrue, ASTFalse;
 
-    public:
+        ASTNode
+        propagate(const ASTNode& a, ArrayTransformer*at);
         HASHSET<int> alreadyVisited;
+
+    public:
         const static string message;
 
         PropagateEqualities(Simplifier *simp_, NodeFactory *nf_, STPMgr *bm_) :
@@ -35,7 +38,14 @@ namespace BEEV
         }
 
         ASTNode
-        propagate(const ASTNode& a, ArrayTransformer*at);
+        topLevel(const ASTNode& a, ArrayTransformer* at)
+        {
+          bm->GetRunTimes()->start(RunTimes::PropagateEqualities);
+          ASTNode result = propagate(a, at);
+          bm->GetRunTimes()->stop(RunTimes::PropagateEqualities);
+          return result;
+        }
+
     };
 }
 

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index cd7d9c960392079d0f2e3a4030da6ce1472a2fb2..a726ca2ded155754c9ee39fb2fc37121f11035e1 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -14,7 +14,6 @@ SubstitutionMap::~SubstitutionMap()
 {
        delete SolverMap;
        delete nf;
-       delete pe;
 }
 
 // if false. Don't simplify while creating the substitution map.
@@ -76,12 +75,6 @@ ASTNode SubstitutionMap::applySubstitutionMap(const ASTNode& n)
        return result;
 }
 
-
-ASTNode SubstitutionMap::propagate(const ASTNode& a, ArrayTransformer*at)
-{
-    return pe->propagate(a,at);
-}
-
 // not always idempotent.
 ASTNode SubstitutionMap::applySubstitutionMapUntilArrays(const ASTNode& n)
 {

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 71155618b5316a37258454b6eb58216c32b29063..5ed390a0f8741651e0c5c46a2ecbb62955d1eb64 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -10,7 +10,6 @@
 #include "../STPManager/STPManager.h"
 #include "../AST/NodeFactory/SimplifyingNodeFactory.h"
 #include "VariablesInExpression.h"
-#include "PropagateEqualities.h"
 
 namespace BEEV {
 
@@ -26,7 +25,6 @@ class SubstitutionMap {
        STPMgr* bm;
        ASTNode ASTTrue, ASTFalse, ASTUndefined;
        NodeFactory *nf;
-       PropagateEqualities *pe;
 
        // These are used to avoid substituting {x = f(y,z), z = f(x)}
        typedef hash_map<ASTNode, Symbols*,ASTNode::ASTNodeHasher> DependsType;
@@ -76,14 +74,12 @@ public:
                loopCount = 0;
                substitutionsLastApplied =0;
                nf = new SimplifyingNodeFactory (*bm->hashingNodeFactory, *bm);
-               pe = new PropagateEqualities(_simp, nf, bm);
        }
 
        void clear()
        {
                SolverMap->clear();
                haveAppliedSubstitutionMap();
-               pe->alreadyVisited.clear();
        }
 
        virtual ~SubstitutionMap();
@@ -190,8 +186,6 @@ public:
                return false;
        }
 
-       ASTNode propagate(const ASTNode& a,   ArrayTransformer*at);
-
        ASTNode applySubstitutionMap(const ASTNode& n);
 
        ASTNode applySubstitutionMapUntilArrays(const ASTNode& n);

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 2abba2231b38fd0e3e6283345cbbf9d78b8c644a..5a883689dfdd24c46acfb836c672099c9fed1f74 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -121,15 +121,6 @@ namespace BEEV
 
   // Substitution Map methods....
 
-  ASTNode
-  Simplifier::topLevel(const ASTNode& a, ArrayTransformer* at)
-  {
-    _bm->GetRunTimes()->start(RunTimes::PropagateEqualities);
-    ASTNode result = substitutionMap.propagate(a, at);
-    _bm->GetRunTimes()->stop(RunTimes::PropagateEqualities);
-    return result;
-  }
-
   bool
   Simplifier::UpdateSolverMap(const ASTNode& key, const ASTNode& value)
   {