Refactor. Add an extra configuration option to control always_true detection.

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

diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp
index ef6e2e0b1c1f5f9f64ab7c573f248e28192958a5..95ae0054383c5f3dc30dc00210c1fbbe076e4d83 100644 (file)
--- a/src/simplifier/PropagateEqualities.cpp
+++ b/src/simplifier/PropagateEqualities.cpp
@@ -37,14 +37,12 @@ namespace BEEV
             }
         else if (IFF == k || EQ == k)
             {
-                ASTVec c = a.GetChildren();
+                const ASTVec& c = a.GetChildren();
 
                 if (c[0] == c[1])
                     return ASTTrue;
 
-                ASTNode c1 = c[1];
-
-                bool updated = simp->UpdateSubstitutionMap(c[0], c1);
+                bool updated = simp->UpdateSubstitutionMap(c[0], c[1]);
                 output = updated ? ASTTrue : a;
 
                 if (updated)
@@ -52,10 +50,10 @@ namespace BEEV
                         //fill the arrayname readindices vector if e0 is a
                         //READ(Arr,index) and index is a BVCONST
                         int to;
-                        if ((to = TermOrder(c[0], c1)) == 1 && c[0].GetKind() == READ)
-                            at->FillUp_ArrReadIndex_Vec(c[0], c1);
-                        else if (to == -1 && c1.GetKind() == READ)
-                            at->FillUp_ArrReadIndex_Vec(c1, c[0]);
+                        if ((to = TermOrder(c[0], c[1])) == 1 && c[0].GetKind() == READ)
+                            at->FillUp_ArrReadIndex_Vec(c[0], c[1]);
+                        else if (to == -1 && c[1].GetKind() == READ)
+                            at->FillUp_ArrReadIndex_Vec(c[1], c[0]);
                     }
             }
         else if (XOR == k)
@@ -138,7 +136,8 @@ namespace BEEV
 
                 for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
                     {
-                        simp->UpdateAlwaysTrueFormSet(*it);
+                        if (always_true)
+                          simp->UpdateAlwaysTrueFormSet(*it);
                         ASTNode aaa = propagate(*it, at);
 
                         if (ASTTrue != aaa)

diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h
index 2703f4dbb5e207b66682b67b20ce86b5174a6d90..96217a007b12e9701c8c6278ccb2118978b3d096 100644 (file)
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -26,10 +26,12 @@ namespace BEEV
         propagate(const ASTNode& a, ArrayTransformer*at);
         HASHSET<int> alreadyVisited;
 
+        const bool always_true;
     public:
 
         PropagateEqualities(Simplifier *simp_, NodeFactory *nf_, STPMgr *bm_) :
-                ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse)
+                ASTTrue(bm_->ASTTrue), ASTFalse(bm_->ASTFalse),
+                always_true(bm_->UserFlags.isSet("always_true","1"))
         {
             simp = simp_;
             nf = nf_;