From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 5 Apr 2012 03:55:50 +0000 (+0000)
Subject: Improvement. Add a configuration option to remove a simplification, reduce its limit... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d235c5e13f12156f6aa760a561c5f14f051a2195;p=francis%2Fstp.git

Improvement. Add a configuration option to remove a simplification, reduce its limit too.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 21fd657..25a6a9f 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -542,7 +542,7 @@ namespace BEEV
   }
 
   bool
-  getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 45)
+  getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector<ASTNode>& found, int maxCount = 5)
   {
     if (maxCount <= 0)
       return false;
@@ -1005,7 +1005,7 @@ namespace BEEV
         return r;
       }
 
-    if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST))
+    if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST) && _bm->UserFlags.isSet("ite-const","1"))
       {
         // If it can only evaluate to constants on the LHS and the RHS, and those constants are never equal,
         // then it must be false. e.g.   ite( f, 10 , 20 ) = ite (g, 30 ,12)