Speedup. Remove some unnecessary tests.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index b70a15b716859433082fdfd7d05d2d340f37f749..de0ae21ee306dd76c46a8cbaf99dc9229d848d97 100644 (file)
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -86,49 +86,25 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
       return output;
     }
 
-  if (IFF == k)
+  if (IFF == k || EQ == k)
     {
       ASTVec c = a.GetChildren();
       SortByArith(c);
-      if (SYMBOL != c[0].GetKind() ||
-          bm->VarSeenInTerm(c[0],
-                            simp->SimplifyFormula_NoRemoveWrites(c[1], false)))
-        {
-          return a;
-        }
-      bool updated =
-        UpdateSubstitutionMap(c[0],
-                                    simp->SimplifyFormula(c[1], false));
-      output = updated ? ASTTrue : a;
-      return output;
-    }
 
-  if (EQ == k)
-    {
+      ASTNode c1;
+      if (EQ == k)
+         c1 = simp->SimplifyTerm(c[1]);
+      else// (IFF == k )
+         c1= simp->SimplifyFormula_NoRemoveWrites(c[1], false);
+
       //fill the arrayname readindices vector if e0 is a
       //READ(Arr,index) and index is a BVCONST
-      ASTVec c = a.GetChildren();
-      SortByArith(c);
-      ASTNode c1 = simp->SimplifyTerm(c[1]);
-
       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 (SYMBOL == c[0].GetKind()
-          && bm->VarSeenInTerm(c[0], c1))
-        {
-          return a;
-        }
-
-      if (1 == TermOrder(c[0], c1)
-          && READ == c[0].GetKind()
-          && bm->VarSeenInTerm(c[0][1], c1))
-        {
-          return a;
-        }
       bool updated = UpdateSubstitutionMap(c[0], c1);
       output = updated ? ASTTrue : a;
       return output;