From 47c72a5063559f369a834afe9182c99e3c18b77f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 11 Sep 2011 13:41:14 +0000 Subject: [PATCH] Improvement. run unconstrained elimination after propagating equalities. Unconstrained is the more expensive, so running the other one first can shrink the size of the problem down before it runs. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1396 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 69b01d6..1fc735d 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -112,14 +112,6 @@ namespace BEEV { ASTNode STP::sizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver) { - if (bm->UserFlags.isSet("enable-unconstrained", "1")) - { - // Remove unconstrained. - RemoveUnconstrained r1(*bm); - simplified_solved_InputToSAT = r1.topLevel(simplified_solved_InputToSAT, simp); - bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT); - } - simplified_solved_InputToSAT = simp->CreateSubstitutionMap(simplified_solved_InputToSAT, arrayTransformer); if (simp->hasUnappliedSubstitutions()) { @@ -128,6 +120,14 @@ namespace BEEV { bm->ASTNodeStats("After Propagating Equalities: ", simplified_solved_InputToSAT); } + if (bm->UserFlags.isSet("enable-unconstrained", "1")) + { + // Remove unconstrained. + RemoveUnconstrained r1(*bm); + simplified_solved_InputToSAT = r1.topLevel(simplified_solved_InputToSAT, simp); + bm->ASTNodeStats("After Removing Unconstrained: ", simplified_solved_InputToSAT); + } + if (bm->UserFlags.isSet("use-intervals", "1")) { EstablishIntervals intervals(*bm); -- 2.47.3