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 1946d67b7ee528f6c6ed48892bba1abc76555406..409735f832130668362441deb580bb9b01a2b208 100644 (file)
--- 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 55b6131b386218589b8ccdfd53350b903057f79e..d998c76abee0792b1c1564747a2c99cc1cccaae7 100644 (file)
--- 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;
+
                 }
             }
         }