Refactor. Retry splitting out propagating equalities.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 4734e7f8c2b3b4280c5a89509a0f87ac782e0c40..8ff1b21bcb1aca41ae010d52d2b571a31099b44c 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -65,7 +65,7 @@ int TermOrder(const ASTNode& a, const ASTNode& b)
 // formula by true.
 // The bvsolver puts expressions of the form (= SYMBOL TERM) into the solverMap.
 
-ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransformer*at)
+ASTNode SubstitutionMap::propagate(const ASTNode& a,  ArrayTransformer*at)
 {
   if (!bm->UserFlags.wordlevel_solve_flag)
     return a;
@@ -86,12 +86,12 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
   const Kind k = a.GetKind();
   if (SYMBOL == k && BOOLEAN_TYPE == a.GetType())
     {
-      bool updated = UpdateSubstitutionMap(a, ASTTrue);
+      bool updated = simp->UpdateSubstitutionMap(a, ASTTrue);
       output = updated ? ASTTrue : a;
     }
   else if (NOT == k && SYMBOL == a[0].GetKind())
     {
-      bool updated = UpdateSubstitutionMap(a[0], ASTFalse);
+      bool updated = simp->UpdateSubstitutionMap(a[0], ASTFalse);
       output = updated ? ASTTrue : a;
     }
   else if (IFF == k || EQ == k)
@@ -110,7 +110,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
       else// (IFF == k )
          c1= simplify_during_create_subM ?  simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1];
 
-      bool updated = UpdateSubstitutionMap(c[0], c1);
+      bool updated = simp->UpdateSubstitutionMap(c[0], c1);
       output = updated ? ASTTrue : a;
 
       if (updated)
@@ -138,7 +138,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                  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 (UpdateSolverMap(symbol, newN))
+                  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)
@@ -146,7 +146,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                   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 (UpdateSolverMap(symbol, newN))
+                  if (simp->UpdateSolverMap(symbol, newN))
                       output =  ASTTrue;
                 }
              else if (a[0].GetKind() == EQ && a[0][0].GetValueWidth() ==1 && a[0][1].GetKind() == SYMBOL)
@@ -156,7 +156,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                  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 (UpdateSolverMap(symbol, newN))
+                  if (simp->UpdateSolverMap(symbol, newN))
                       output =  ASTTrue;
                }
              else if (a[1].GetKind() == EQ && a[1][0].GetValueWidth() ==1 && a[1][1].GetKind() == SYMBOL)
@@ -164,7 +164,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
                   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 (UpdateSolverMap(symbol, newN))
+                  if (simp->UpdateSolverMap(symbol, newN))
                       output =  ASTTrue;
                 }
              else
@@ -186,7 +186,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
 
                 assert(symbol.GetKind() == SYMBOL);
 
-                if (UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
+                if (simp->UpdateSolverMap(symbol, nf->CreateNode(NOT, rhs)))
                    output =  ASTTrue;
            }
   }
@@ -201,7 +201,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
            it != itend; it++)
         {
           simp->UpdateAlwaysTrueFormSet(*it);
-          ASTNode aaa = CreateSubstitutionMap(*it,at);
+          ASTNode aaa = propagate(*it,at);
 
           if (ASTTrue != aaa)
             {

diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index bc4bff865af957468d7088d31b47a201ff7e9ec9..d3f4e35b91f3f27ea008a3f3499304e6e5d37fac 100644 (file)
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -187,7 +187,7 @@ public:
                return false;
        }
 
-       ASTNode CreateSubstitutionMap(const ASTNode& a,   ArrayTransformer*at);
+       ASTNode propagate(const ASTNode& a,   ArrayTransformer*at);
 
        ASTNode applySubstitutionMap(const ASTNode& n);
 

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 796757dea9f9c626507db29a19027c0047da23e8..13d6d23cdbf8fda78c86f4c6c5aae98b6ad6f090 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -125,7 +125,7 @@ namespace BEEV
   Simplifier::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer* at)
   {
     _bm->GetRunTimes()->start(RunTimes::PropagateEqualities);
-    ASTNode result = substitutionMap.CreateSubstitutionMap(a, at);
+    ASTNode result = substitutionMap.propagate(a, at);
     _bm->GetRunTimes()->stop(RunTimes::PropagateEqualities);
     return result;
   }