From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Fri, 9 Jul 2010 14:06:23 +0000 (+0000)
Subject: Decision. This optimisation helps our cvc regressions but hurts our smtlib ones.... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e5c6620767423d81db449bed452015dfbdd89389;p=francis%2Fstp.git

Decision. This optimisation helps our cvc regressions but hurts our smtlib ones. So I'm taking it out..




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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 93cee1e..4e42875 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2120,12 +2120,19 @@ namespace BEEV
                   }
                 break;
               }
+
+          // This can increase the number of nodes exponentially.
+          // If turned on bitrev2048 will blow out main memory, with
+          // this disabled it takes 12MB.
+              #if 0
+
             case BVAND:
             case BVOR:
             case BVXOR:
               {
             	assert(a0.Degree() == 2);
-                //assumes these operators are binary
+
+            	//assumes these operators are binary
                 //
                 // (t op u)[i:j] <==> t[i:j] op u[i:j]
                 ASTNode t = a0[0];
@@ -2140,9 +2147,12 @@ namespace BEEV
                                VarConstMap);
                 BVTypeCheck(t);
                 BVTypeCheck(u);
-                output = nf->CreateTerm(k1, a_len, t, u);
+                //output = nf->CreateTerm(k1, a_len, t, u);
+
+                output = inputterm;
                 break;
               }
+          #endif
             case BVNEG:
               {
                 // (~t)[i:j] <==> ~(t[i:j])