From 3fbe8810c610c8fea6ed656a6c0de387b5a32a38 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 16 Jan 2012 01:41:14 +0000 Subject: [PATCH] Refactor. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1506 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 6 ++++-- src/simplifier/PropagateEqualities.cpp | 6 ++---- src/simplifier/PropagateEqualities.h | 4 +++- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 174df3c..68f13e5 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -34,6 +34,8 @@ namespace BEEV { const static string pl_message = "After Pure Literals. "; const static string bitvec_message = "After Bit-vector Solving. "; const static string size_inc_message= "After Speculative Simplifications. "; + const static string pe_message= "After Propagating Equalities. "; + // The absolute TopLevel function that invokes STP on the input @@ -124,7 +126,7 @@ namespace BEEV { { simplified_solved_InputToSAT = simp->applySubstitutionMap(simplified_solved_InputToSAT); simp->haveAppliedSubstitutionMap(); - bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); + bm->ASTNodeStats(pe_message.c_str(), simplified_solved_InputToSAT); } if (bm->UserFlags.isSet("enable-unconstrained", "1")) @@ -291,7 +293,7 @@ namespace BEEV { simp->haveAppliedSubstitutionMap(); } - bm->ASTNodeStats(pe->message.c_str(), simplified_solved_InputToSAT); + bm->ASTNodeStats(pe_message.c_str(), simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp index 3494955..ef6e2e0 100644 --- a/src/simplifier/PropagateEqualities.cpp +++ b/src/simplifier/PropagateEqualities.cpp @@ -5,14 +5,12 @@ namespace BEEV { - const string PropagateEqualities::message = "After Propagating Equalities: "; + + // This doesn't rewrite changes through properly so needs to have a substitution applied to its output. ASTNode PropagateEqualities::propagate(const ASTNode& a, ArrayTransformer*at) { - if (!bm->UserFlags.propagate_equalities) - return a; - ASTNode output; //if the variable has been solved for, then simply return it if (simp->CheckSubstitutionMap(a, output)) diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h index 831c98e..2703f4d 100644 --- a/src/simplifier/PropagateEqualities.h +++ b/src/simplifier/PropagateEqualities.h @@ -27,7 +27,6 @@ namespace BEEV HASHSET alreadyVisited; public: - const static string message; PropagateEqualities(Simplifier *simp_, NodeFactory *nf_, STPMgr *bm_) : ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse) @@ -40,6 +39,9 @@ namespace BEEV ASTNode topLevel(const ASTNode& a, ArrayTransformer* at) { + if (!bm->UserFlags.propagate_equalities) + return a; + bm->GetRunTimes()->start(RunTimes::PropagateEqualities); ASTNode result = propagate(a, at); bm->GetRunTimes()->stop(RunTimes::PropagateEqualities); -- 2.47.3