From e4371b2385e3906a4f8687fff11858a9d23607e1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 1 May 2011 03:38:53 +0000 Subject: [PATCH] Enable bitblast simplifications by default git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1296 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 97d0dc2..e87ea4c 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -194,7 +194,7 @@ namespace BEEV { } // Expensive, so only want to do it once. - if (bm->UserFlags.isSet("bitblast-simplification", "0") && initial_difficulty_score < 250000) + if (bm->UserFlags.isSet("bitblast-simplification", "1") && initial_difficulty_score < 250000) { BBNodeManagerAIG bbnm; SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); @@ -203,14 +203,11 @@ namespace BEEV { bb.getConsts(simplified_solved_InputToSAT, fromTo); if (fromTo.size() > 0) { - cerr << "#" << fromTo.size() << endl; ASTNodeMap cache; simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf); bm->ASTNodeStats("After bitblast simplification: ", simplified_solved_InputToSAT); } } - - initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); } -- 2.47.3