From a714e9d5964f63fc3da81e15850c27d797b2e0ff Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 07:48:44 +0000
Subject: [PATCH] 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
---
 src/simplifier/SubstitutionMap.cpp | 38 ++++++------------------------
 1 file changed, 7 insertions(+), 31 deletions(-)

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index b70a15b..de0ae21 100644
--- 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;
-- 
2.47.3