Refactor. automatically layout code.

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

diff --git a/src/simplifier/PropagateEqualities.cpp b/src/simplifier/PropagateEqualities.cpp
index 46c21f518e5c0749f15cb2244b827cd125803b20..3494955970a656397d893e8b2ef55bc579230d22 100644 (file)
--- a/src/simplifier/PropagateEqualities.cpp
+++ b/src/simplifier/PropagateEqualities.cpp
@@ -7,176 +7,162 @@ namespace BEEV
 {
     const string PropagateEqualities::message = "After Propagating Equalities: ";
 
-    // if false. Don't simplify while creating the substitution map.
-    // This makes it easier to spot how long is spent in the simplifier.
-    const bool simplify_during_create_subM = false;
-
+    ASTNode
+    PropagateEqualities::propagate(const ASTNode& a, ArrayTransformer*at)
+    {
+        if (!bm->UserFlags.propagate_equalities)
+            return a;
 
-    //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
-    // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
-    // or (=SYMBOL BVCONST).
-    // It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the
-    // formula by true.
-    // The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap.
+        ASTNode output;
+        //if the variable has been solved for, then simply return it
+        if (simp->CheckSubstitutionMap(a, output))
+            return output;
 
-    ASTNode PropagateEqualities::propagate(const ASTNode& a,  ArrayTransformer*at)
-    {
-      if (!bm->UserFlags.propagate_equalities)
-        return a;
+        if (!alreadyVisited.insert(a.GetNodeNum()).second)
+            {
+                return a;
+            }
 
-      ASTNode output;
-      //if the variable has been solved for, then simply return it
-      if (simp->CheckSubstitutionMap(a, output))
-        return output;
+        output = a;
 
-      if (!alreadyVisited.insert(a.GetNodeNum()).second)
-      {
-        return a;
-      }
-
-      output = a;
-
-      //traverse a and populate the SubstitutionMap
-      const Kind k = a.GetKind();
-      if (SYMBOL == k && BOOLEAN_TYPE == a.GetType())
-        {
-          bool updated = simp->UpdateSubstitutionMap(a, ASTTrue);
-          output = updated ? ASTTrue : a;
-        }
-      else if (NOT == k && SYMBOL == a[0].GetKind())
-        {
-          bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse);
-          output = updated ? ASTTrue : a;
-        }
-      else if (IFF == k || EQ == k)
-        {
-              ASTVec c = a.GetChildren();
-
-              if (simplify_during_create_subM)
-                      SortByArith(c);
-
-              if (c[0] == c[1])
-                      return ASTTrue;
-
-          ASTNode c1;
-          if (EQ == k)
-              c1 = simplify_during_create_subM ? simp->SimplifyTerm(c[1]) : c[1];
-          else// (IFF == k )
-              c1= simplify_during_create_subM ?  simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1];
-
-          bool updated = simp->UpdateSubstitutionMap(c[0], c1);
-          output = updated ? ASTTrue : a;
-
-          if (updated)
+        //traverse a and populate the SubstitutionMap
+        const Kind k = a.GetKind();
+        if (SYMBOL == k && BOOLEAN_TYPE == a.GetType())
             {
-              //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]);
+                bool updated = simp->UpdateSubstitutionMap(a, ASTTrue);
+                output = updated ? ASTTrue : a;
             }
-        }
-      else if (XOR == k)
-      {
-              if (a.Degree() !=2)
-                return output;
-
-              int to = TermOrder(a[0],a[1]);
-              if (0 == to)
-                {
-                  if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ && a[0][0][0].GetValueWidth() ==1 && a[0][0][1].GetKind() == SYMBOL)
-                    {
-                      // (XOR (NOT(= (1 v)))  ... )
-                      const ASTNode& symbol = a[0][0][1];
-                      const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], a[0][0][0], nf->CreateTerm(BVNEG, 1,a[0][0][0]));
+        else if (NOT == k && SYMBOL == a[0].GetKind())
+            {
+                bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse);
+                output = updated ? ASTTrue : a;
+            }
+        else if (IFF == k || EQ == k)
+            {
+                ASTVec c = a.GetChildren();
 
-                      if (simp->UpdateSolverMap(symbol, newN))
-                          output =  ASTTrue;
-                    }
-                  else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ && a[1][0][0].GetValueWidth() ==1 && a[1][0][1].GetKind() == SYMBOL)
-                    {
-                      const ASTNode& symbol = a[1][0][1];
-                      const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], a[1][0][0], nf->CreateTerm(BVNEG, 1,a[1][0][0]));
+                if (c[0] == c[1])
+                    return ASTTrue;
 
-                      if (simp->UpdateSolverMap(symbol, newN))
-                          output =  ASTTrue;
-                    }
-                  else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL)
-                    {
-                      // XOR ((= 1 v) ... )
+                ASTNode c1 = c[1];
 
-                      const ASTNode& symbol = a[0][1];
-                      const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], nf->CreateTerm(BVNEG, 1,a[0][0]), a[0][0]);
+                bool updated = simp->UpdateSubstitutionMap(c[0], c1);
+                output = updated ? ASTTrue : a;
 
-                      if (simp->UpdateSolverMap(symbol, newN))
-                          output =  ASTTrue;
-                    }
-                  else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() ==1 && a[1][1].GetKind() == SYMBOL)
+                if (updated)
                     {
-                      const ASTNode& symbol = a[1][1];
-                      const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], nf->CreateTerm(BVNEG, 1,a[1][0]), a[1][0]);
-
-                      if (simp->UpdateSolverMap(symbol, newN))
-                          output =  ASTTrue;
+                        //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]);
                     }
-                  else
-                  return output;
-                }
-              else
-                {
-                    ASTNode symbol,rhs;
-                    if (to==1)
+            }
+        else if (XOR == k)
+            {
+                if (a.Degree() != 2)
+                    return output;
+
+                int to = TermOrder(a[0], a[1]);
+                if (0 == to)
                     {
-                        symbol = a[0];
-                        rhs = a[1];
+                        if (a[0].GetKind() == NOT && a[0][0].GetKind() == EQ && a[0][0][0].GetValueWidth() == 1
+                                && a[0][0][1].GetKind() == SYMBOL)
+                            {
+                                // (XOR (NOT(= (1 v)))  ... )
+                                const ASTNode& symbol = a[0][0][1];
+                                const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], a[0][0][0],
+                                        nf->CreateTerm(BVNEG, 1, a[0][0][0]));
+
+                                if (simp->UpdateSolverMap(symbol, newN))
+                                    output = ASTTrue;
+                            }
+                        else if (a[1].GetKind() == NOT && a[1][0].GetKind() == EQ && a[1][0][0].GetValueWidth() == 1
+                                && a[1][0][1].GetKind() == SYMBOL)
+                            {
+                                const ASTNode& symbol = a[1][0][1];
+                                const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], a[1][0][0],
+                                        nf->CreateTerm(BVNEG, 1, a[1][0][0]));
+
+                                if (simp->UpdateSolverMap(symbol, newN))
+                                    output = ASTTrue;
+                            }
+                        else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() == 1 && a[0][1].GetKind() == SYMBOL)
+                            {
+                                // XOR ((= 1 v) ... )
+
+                                const ASTNode& symbol = a[0][1];
+                                const ASTNode newN = nf->CreateTerm(ITE, 1, a[1], nf->CreateTerm(BVNEG, 1, a[0][0]),
+                                        a[0][0]);
+
+                                if (simp->UpdateSolverMap(symbol, newN))
+                                    output = ASTTrue;
+                            }
+                        else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() == 1 && a[1][1].GetKind() == SYMBOL)
+                            {
+                                const ASTNode& symbol = a[1][1];
+                                const ASTNode newN = nf->CreateTerm(ITE, 1, a[0], nf->CreateTerm(BVNEG, 1, a[1][0]),
+                                        a[1][0]);
+
+                                if (simp->UpdateSolverMap(symbol, newN))
+                                    output = ASTTrue;
+                            }
+                        else
+                            return output;
                     }
-                    else
+                else
                     {
-                        symbol = a[1];
-                        rhs = a[0];
+                        ASTNode symbol, rhs;
+                        if (to == 1)
+                            {
+                                symbol = a[0];
+                                rhs = a[1];
+                            }
+                        else
+                            {
+                                symbol = a[1];
+                                rhs = a[0];
+                            }
+
+                        assert(symbol.GetKind() == SYMBOL);
+
+                        if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
+                            output = ASTTrue;
                     }
-
-                    assert(symbol.GetKind() == SYMBOL);
-
-                    if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
-                       output =  ASTTrue;
-                }
-      }
-      else if (AND == k)
-        {
-              const ASTVec& c = a.GetChildren();
-              ASTVec o;
-          o.reserve(c.size());
-
-          for (ASTVec::const_iterator
-                 it = c.begin(), itend = c.end();
-               it != itend; it++)
+            }
+        else if (AND == k)
             {
-              simp->UpdateAlwaysTrueFormSet(*it);
-              ASTNode aaa = propagate(*it,at);
-
-              if (ASTTrue != aaa)
-                {
-                  if (ASTFalse == aaa)
-                    return ASTFalse;
-                  else
-                    o.push_back(aaa);
-                }
+                const ASTVec& c = a.GetChildren();
+                ASTVec o;
+                o.reserve(c.size());
+
+                for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++)
+                    {
+                        simp->UpdateAlwaysTrueFormSet(*it);
+                        ASTNode aaa = propagate(*it, at);
+
+                        if (ASTTrue != aaa)
+                            {
+                                if (ASTFalse == aaa)
+                                    return ASTFalse;
+                                else
+                                    o.push_back(aaa);
+                            }
+                    }
+                if (o.size() == 0)
+                    output = ASTTrue;
+                else if (o.size() == 1)
+                    output = o[0];
+                else if (o != c)
+                    output = nf->CreateNode(AND, o);
+                else
+                    output = a;
             }
-          if (o.size() == 0)
-            output =  ASTTrue;
-          else if (o.size() == 1)
-            output = o[0];
-          else if (o != c)
-            output = nf->CreateNode(AND, o);
-          else
-            output = a;
-        }
-
-      return output;
-    } //end of CreateSubstitutionMap()
 
+        return output;
+    } //end of CreateSubstitutionMap()
 
-};
+}
+;

diff --git a/src/simplifier/PropagateEqualities.h b/src/simplifier/PropagateEqualities.h
index a1fb618274cd690d9a824772d77d99047653b016..102190809de239d9a63592ad9c9ab651d15a3fb5 100644 (file)
--- a/src/simplifier/PropagateEqualities.h
+++ b/src/simplifier/PropagateEqualities.h
@@ -4,12 +4,11 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 
-    //This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
-    // (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
-    // or (=SYMBOL BVCONST).
-    // It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the
-    // formula by true.
-
+//This finds conjuncts which are one of: (= SYMBOL BVCONST), (= BVCONST (READ SYMBOL BVCONST)),
+// (IFF SYMBOL TRUE), (IFF SYMBOL FALSE), (IFF SYMBOL SYMBOL), (=SYMBOL SYMBOL)
+// or (=SYMBOL BVCONST).
+// It tries to remove the conjunct, storing it in the substitutionmap. It replaces it in the
+// formula by true.
 
 namespace BEEV
 {