From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 25 Jun 2010 05:16:40 +0000 (+0000)
Subject: The array transformer now respects optimisations being disabled.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=cf79060532aa80e0ace9042c73ed215fba98572e;p=francis%2Fstp.git

The array transformer now respects optimisations being disabled.



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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index 1946d67..409735f 100644
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -26,6 +26,7 @@ namespace BEEV
   bool arithless(const ASTNode n1, const ASTNode n2);
   bool isAtomic(Kind k);
   bool isCommutative(const Kind k);
+  bool containsArrayOps(const ASTNode&n);
 
   // If (a > b) in the termorder, then return 1 elseif (a < b) in the
   // termorder, then return -1 else return 0
diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 55b6131..d998c76 100644
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -101,7 +101,10 @@ namespace BEEV
                          modnode);
 
         //put everything together, simplify, and return
-        return simp->SimplifyTerm_TopLevel(n);
+        if (bm->UserFlags.optimize_flag)
+            return simp->SimplifyTerm_TopLevel(n);
+        else
+        	return n;
       }
 
     // This is the modulus of dividing rounding to -infinity.
@@ -151,7 +154,10 @@ namespace BEEV
                          nf->CreateTerm(BVPLUS, len, rev_node, divisor),
                          rev_node);
 
-        return simp->SimplifyTerm_TopLevel(n);
+        if (bm->UserFlags.optimize_flag)
+            return simp->SimplifyTerm_TopLevel(n);
+        else
+        	return n;
       }
     else if (SBVDIV == in.GetKind())
       {
@@ -194,7 +200,10 @@ namespace BEEV
                          nf->CreateTerm(BVUMINUS, len, divnode),
                          divnode);
 
-        return simp->SimplifyTerm_TopLevel(n);
+        if (bm->UserFlags.optimize_flag)
+            return simp->SimplifyTerm_TopLevel(n);
+        else
+        	return n;
       }
 
     FatalError("TranslateSignedDivModRem:"\
@@ -461,7 +470,11 @@ namespace BEEV
                                    one, result);
 
                   //return result;
-                  return simp->SimplifyTerm_TopLevel(result);
+                  if (bm->UserFlags.optimize_flag)
+                      return simp->SimplifyTerm_TopLevel(result);
+                  else
+                  	return result;
+
                 }
             }
         }