From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Jun 2010 14:06:31 +0000 (+0000)
Subject: Don't perform simplifications when creating the substitution map. I'm not sure if... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=54a8f962f8e50ed5a7bf9225c79cd2bf3301d830;p=francis%2Fstp.git

Don't perform simplifications when creating the substitution map. I'm not sure if this is justified, but it makes STP easier to understand. I'll check if it's useful.




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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index de0ae21..88b3b0b 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -15,6 +15,9 @@ SubstitutionMap::~SubstitutionMap()
 	delete SolverMap;
 }
 
+// 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;
 
 //if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1
 //if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1
@@ -93,9 +96,9 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
 
       ASTNode c1;
       if (EQ == k)
-    	  c1 = simp->SimplifyTerm(c[1]);
+    	  c1 = simplify_during_create_subM ? simp->SimplifyTerm(c[1]) : c[1];
       else// (IFF == k )
-    	  c1= simp->SimplifyFormula_NoRemoveWrites(c[1], false);
+    	  c1= simplify_during_create_subM ?  simp->SimplifyFormula_NoRemoveWrites(c[1], false) : c[1];
 
       //fill the arrayname readindices vector if e0 is a
       //READ(Arr,index) and index is a BVCONST