From 65acda8d2de92761e0ae9636442f64ef623341ec Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Nov 2011 05:22:26 +0000 Subject: [PATCH] Improvement. If simplifications make the problem containing arrays harder, then revert it. Prevsiously it only did this for bit-vector only problems. This uses extra memory. It seems justified. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1425 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/STP.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index de7950c..f23529e 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -23,6 +23,7 @@ #include "../simplifier/UseITEContext.h" #include "../simplifier/AlwaysTrue.h" #include "../simplifier/AIGSimplifyPropositionalCore.h" +#include "../simplifier/BigRewriter.h" #include namespace BEEV { @@ -108,6 +109,7 @@ namespace BEEV { bm->ASTNodeStats("After bitblast simplification: ", simplified_solved_InputToSAT); } } + return simplified_solved_InputToSAT; } @@ -220,10 +222,23 @@ 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; @@ -280,6 +295,7 @@ namespace BEEV { } while (inputToSAT != simplified_solved_InputToSAT); + if (bm->UserFlags.bitConstantProp_flag) { bm->GetRunTimes()->start(RunTimes::ConstantBitPropagation); -- 2.47.3