Refactor.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1506 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 174df3c9148b6d1dd6baaf8f8d9a592d59094a6a..68f13e5111bacb642c1acf0c8a244ffd03ac9969 100644 (file)
--- 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 3494955970a656397d893e8b2ef55bc579230d22..ef6e2e0b1c1f5f9f64ab7c573f248e28192958a5 100644 (file)
--- 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 831c98e20b63b24c292c2060f7de60dddd5fae46..2703f4dbb5e207b66682b67b20ce86b5174a6d90 100644 (file)
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -27,7 +27,6 @@ namespace BEEV
         HASHSET<int> 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);