From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 27 Jun 2010 10:59:46 +0000 (+0000)
Subject: Speedup. Don't push extracts through ites. Sometimes this may be good to do. But... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1f64484b5513424217b34c2adc88be586df42166;p=francis%2Fstp.git

Speedup. Don't push extracts through ites. Sometimes this may be good to do. But usually not.



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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index ca235c3..8aa26f8 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -2165,9 +2165,15 @@ namespace BEEV
               //        nf->CreateTerm(BVSX,a_len,t,
               //                        _bm->CreateBVConst(32,a_len));
               //        } break; }
+
+              /*
+               * On deeply nested ITES, this can cause an exponential number
+               * of nodes to be produced. Especially if there are different
+               * extracts over the same node.
+               *
             case ITE:
               {
-                const ASTNode& t0 = a0[0];
+            	 const ASTNode& t0 = a0[0];
                 ASTNode t1 = 
                   SimplifyTerm(nf->CreateTerm(BVEXTRACT,
                                                a_len, a0[1], i, j), 
@@ -2179,6 +2185,7 @@ namespace BEEV
                 output = CreateSimplifiedTermITE(t0, t1, t2);
                 break;
               }
+              */
             default:
               {
                 output = nf->CreateTerm(BVEXTRACT, a_len, a0, i, j);