From 876768db2810291b735bc2c77951ce7f9e7adcc6 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 29 Dec 2011 03:17:45 +0000 Subject: [PATCH] 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 --- src/STPManager/STP.cpp | 25 ++++++++++++++----------- src/STPManager/STP.h | 5 +++-- src/simplifier/PropagateEqualities.h | 14 ++++++++++++-- src/simplifier/SubstitutionMap.cpp | 7 ------- src/simplifier/SubstitutionMap.h | 6 ------ src/simplifier/simplifier.cpp | 9 --------- 6 files changed, 29 insertions(+), 37 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 819a1bd..9eec152 100644 --- 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 ca2d372..7c9b7f6 100644 --- 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 1021908..831c98e 100644 --- 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 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 cd7d9c9..a726ca2 100644 --- 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 7115561..5ed390a 100644 --- 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 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 2abba22..5a88368 100644 --- 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) { -- 2.47.3