From 00278b728cb2fc9e90861570e0db4632c147f79e Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Nov 2011 05:28:57 +0000 Subject: [PATCH] Revert to r1423. I checked in the wrong file. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1426 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index f23529e..de7950c 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -23,7 +23,6 @@ #include "../simplifier/UseITEContext.h" #include "../simplifier/AlwaysTrue.h" #include "../simplifier/AIGSimplifyPropositionalCore.h" -#include "../simplifier/BigRewriter.h" #include namespace BEEV { @@ -109,7 +108,6 @@ namespace BEEV { bm->ASTNodeStats("After bitblast simplification: ", simplified_solved_InputToSAT); } } - return simplified_solved_InputToSAT; } @@ -222,23 +220,10 @@ namespace BEEV { // so it's expensive to call. if (!arrayops && initial_difficulty_score < 1000000) { - // Remove the sdiv/smod/srem - simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT); - simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score); initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT); } - { - bm->GetRunTimes()->start(RunTimes::BigRewrite); - BEEV::BigRewriter b ; - ASTNodeMap fromTo; - SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm); - simplified_solved_InputToSAT = b.rewrite(simplified_solved_InputToSAT, fromTo, &nf,bm); - bm->GetRunTimes()->stop(RunTimes::BigRewrite); - } - - if (bm->UserFlags.stats_flag) cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl; @@ -295,7 +280,6 @@ namespace BEEV { } while (inputToSAT != simplified_solved_InputToSAT); - if (bm->UserFlags.bitConstantProp_flag) { bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); -- 2.47.3