From d235c5e13f12156f6aa760a561c5f14f051a2195 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 5 Apr 2012 03:55:50 +0000 Subject: [PATCH] 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 --- src/simplifier/simplifier.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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& found, int maxCount = 45) + getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector& 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) -- 2.47.3