From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Mar 2011 02:21:13 +0000 (+0000)
Subject: Refactor. A new function to check if there are unapplied variable substitutions.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=db943dab65d7c339d010a9e71b3143c41198cf2f;p=francis%2Fstp.git

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 7c4cf1f..ed2106b 100644
--- 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 325e0ad..5c4ca60 100644
--- 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 49d306a..ae92333 100644
--- 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 1f5611a..3aa9eb4 100644
--- 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();