Refactor. A new function to check if there are unapplied variable substitutions.

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 7c4cf1ff32ac2271f1a94ff114e04911c8f11df4..ed2106b7a683abfe0cba19686920eedcd3df7c60 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -115,14 +115,13 @@ namespace BEEV {
                          simplified_solved_InputToSAT);
                }
 
-               int initialSize = simp->Return_SolverMap()->size();
-        simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
-               if (initialSize != simp->Return_SolverMap()->size())
+               simplified_solved_InputToSAT = simp->CreateSubstitutionMap(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);
-               }
+                  simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
+                  simp->haveAppliedSubstitutionMap();
+                  bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT);
+                }
 
            // Find pure literals.
                if (bm->UserFlags.isSet("pure-literals","1"))
@@ -165,9 +164,8 @@ namespace BEEV {
     const bool arrayops = containsArrayOps(original_input);
 
     DifficultyScore difficulty;
-    long initial_difficulty_score = difficulty.score(original_input);
     if (bm->UserFlags.stats_flag)
-       cerr << "Difficulty Initially:" << initial_difficulty_score << endl;
+       cerr << "Difficulty Initially:" << difficulty.score(original_input) << endl;
 
     // A heap object so I can easily control its lifetime.
     BVSolver* bvSolver = new BVSolver(bm,simp);
@@ -175,7 +173,7 @@ namespace BEEV {
     simplified_solved_InputToSAT = sizeReducing(inputToSAT,bvSolver);
     //simplified_solved_InputToSAT = sizeReducing(simplified_solved_InputToSAT,bvSolver);
 
-    initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
+    unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
     if (bm->UserFlags.stats_flag)
        cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl;
 
@@ -200,8 +198,6 @@ namespace BEEV {
 
         if(bm->UserFlags.optimize_flag) 
           {
-            int initialSize = simp->Return_SolverMap()->size();
-
             simplified_solved_InputToSAT = 
                simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
 
@@ -213,7 +209,7 @@ namespace BEEV {
                        // But it shouldn't be T, it should be a constant.
                        // Applying the substitution map fixes this case.
             //
-                       if (initialSize != simp->Return_SolverMap()->size())
+                       if (simp->hasUnappliedSubstitutions())
                        {
                                simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
                                simp->haveAppliedSubstitutionMap();
@@ -308,12 +304,10 @@ namespace BEEV {
 
         if(bm->UserFlags.optimize_flag) 
           {
-               int initialSize = simp->Return_SolverMap()->size();
-
                simplified_solved_InputToSAT =
                simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer);
 
-                       if (initialSize != simp->Return_SolverMap()->size())
+                       if (simp->hasUnappliedSubstitutions())
                        {
                                simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT);
                                simp->haveAppliedSubstitutionMap();

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index 325e0ad9bfe45a543accf5dc088b3d637047d498..5c4ca60f532f5ef122cf1b3946b58d44ac060790 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -39,8 +39,14 @@ class SubstitutionMap {
        void loops_helper(const set<ASTNode>& varsToCheck, set<ASTNode>& visited);
        bool loops(const ASTNode& n0, const ASTNode& n1);
 
+       int substitutionsLastApplied;
 public:
 
+       bool hasUnappliedSubstitutions()
+       {
+         return (substitutionsLastApplied != SolverMap->size());
+       }
+
        // When the substitutionMap has been applied globally, then,
        // these are no longer needed.
        void haveAppliedSubstitutionMap()
@@ -49,6 +55,7 @@ public:
                rhs.clear();
                rhs_visited.clear();
                rhsAlreadyAdded.clear();
+               substitutionsLastApplied = SolverMap->size();
        }
 
        VariablesInExpression vars;
@@ -63,6 +70,7 @@ public:
 
                SolverMap = new ASTNodeMap(INITIAL_TABLE_SIZE);
                loopCount = 0;
+               substitutionsLastApplied =0;
        }
 
        void clear()

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 49d306aa2b00ded5d2fd696508b55392dba086a3..ae92333395d78ed4faab4fa73194dfb83e631a88 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -814,8 +814,11 @@ namespace BEEV
 
     // Imagine in the last conjunct A is replaced by B. But there could
     // be variable A's in the first conjunct. This gets rid of 'em.
-       output = _simp->applySubstitutionMap(output);
-       _simp->haveAppliedSubstitutionMap();
+    if (_simp->hasUnappliedSubstitutions())
+      {
+          output = _simp->applySubstitutionMap(output);
+          _simp->haveAppliedSubstitutionMap();
+      }
 
     UpdateAlreadySolvedMap(_input, output);
     _bm->GetRunTimes()->stop(RunTimes::BVSolver);

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 1f5611a602bb4e1b5b9ba973aa3918c3a6f0728e..3aa9eb4896abe39c0bc6e54901e568d401785ff4 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -239,6 +239,11 @@ namespace BEEV
       return ReadOverWrite_NewName_Map;
     } // End of ReadOverWriteMap()
       
+    bool hasUnappliedSubstitutions()
+    {
+      return substitutionMap.hasUnappliedSubstitutions();
+    }
+
     ASTNodeMap * Return_SolverMap()
     {
        return substitutionMap.Return_SolverMap();