From 86deec6c7dba09b9af149a46839cadf907cee03e Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 3 Mar 2011 06:12:23 +0000
Subject: [PATCH] Refactor. Neaten up the CreateSubstitutionMap function.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1185 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/SubstitutionMap.cpp | 54 +++++++++++++-----------------
 1 file changed, 24 insertions(+), 30 deletions(-)

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index 932811d..0cf4c65 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -69,7 +69,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
   if (!bm->UserFlags.wordlevel_solve_flag)
     return a;
 
-  ASTNode output = a;
+  ASTNode output;
   //if the variable has been solved for, then simply return it
   if (CheckSubstitutionMap(a, output))
     return output;
@@ -79,6 +79,7 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
     return a;
   }
 
+  output = a;
 
   //traverse a and populate the SubstitutionMap
   const Kind k = a.GetKind();
@@ -86,19 +87,18 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
     {
       bool updated = UpdateSubstitutionMap(a, ASTTrue);
       output = updated ? ASTTrue : a;
-      return output;
     }
-  if (NOT == k && SYMBOL == a[0].GetKind())
+  else if (NOT == k && SYMBOL == a[0].GetKind())
     {
       bool updated = UpdateSubstitutionMap(a[0], ASTFalse);
       output = updated ? ASTTrue : a;
-      return output;
     }
-
-  if (IFF == k || EQ == k)
+  else if (IFF == k || EQ == k)
     {
 	  ASTVec c = a.GetChildren();
-	  SortByArith(c);
+
+	  if (simplify_during_create_subM)
+		  SortByArith(c);
 
 	  if (c[0] == c[1])
 		  return ASTTrue;
@@ -122,11 +122,8 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
           else if (to ==-1 && c1.GetKind() == READ)
                     at->FillUp_ArrReadIndex_Vec(c1,c[0]);
         }
-
-      return output;
     }
-
-  if (XOR == k)
+  else if (XOR == k)
   {
 	  if (a.Degree() !=2)
 		  return output;
@@ -151,20 +148,17 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
 
 	  // If either side is already solved for.
 	  if (CheckSubstitutionMap(symbol) || CheckSubstitutionMap(rhs))
-		  return output;
-
-	  if (UpdateSolverMap(symbol, bm->CreateNode(NOT, rhs)))
-			return ASTTrue;
-		else
-			return output;
+	  {}
+	  else if (UpdateSolverMap(symbol, bm->CreateNode(NOT, rhs)))
+			output =  ASTTrue;
   }
-
-
-  if (AND == k)
+  else if (AND == k)
     {
-      ASTVec o;
-      ASTVec c = a.GetChildren();
-      for (ASTVec::iterator
+	  const ASTVec& c = a.GetChildren();
+	  ASTVec o;
+      o.reserve(c.size());
+
+      for (ASTVec::const_iterator
              it = c.begin(), itend = c.end();
            it != itend; it++)
         {
@@ -180,15 +174,15 @@ ASTNode SubstitutionMap::CreateSubstitutionMap(const ASTNode& a,  ArrayTransform
             }
         }
       if (o.size() == 0)
-        return ASTTrue;
-
-      if (o.size() == 1)
-        return o[0];
-
-      return bm->CreateNode(AND, o);
+        output =  ASTTrue;
+      else if (o.size() == 1)
+        output = o[0];
+      else if (o != c)
+    	output = bm->CreateNode(AND, o);
+      else
+    	output = a;
     }
 
-  //printf("I gave up on kind: %d node: %d\n", k, a.GetNodeNum());
   return output;
 } //end of CreateSubstitutionMap()
 
-- 
2.47.3