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

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 ca235c3e6f5cb4517e8f357356ec6e90d96d2080..8aa26f8d07c53accfac127a13b1c1762e4def1d8 100644 (file)
--- 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);