From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 11 Sep 2011 13:41:14 +0000 (+0000)
Subject: Improvement. run unconstrained elimination after propagating equalities. Unconstraine... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=47c72a5063559f369a834afe9182c99e3c18b77f;p=francis%2Fstp.git

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
---

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);