From 8022a9f782ea95f366ac1009d26b106f83913bfb Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 25 Jun 2010 05:25:17 +0000 Subject: [PATCH] Measure the difficulty of formula by using a simple function, that amongst other things counts the number of multiplications in the input. If after simplifications the difficulty has increased. Then the original formula is used instead of the not-simplified one. This is a very rough way of performing DAG aware simplifications. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@885 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/DifficultyScore.h | 58 ++++++++++++++++++++++++++++++++ src/STPManager/STP.cpp | 35 +++++++++++++++++++ src/simplifier/simplifier.cpp | 12 +++++-- src/simplifier/simplifier.h | 1 + 4 files changed, 103 insertions(+), 3 deletions(-) create mode 100644 src/STPManager/DifficultyScore.h diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h new file mode 100644 index 0000000..4e78b55 --- /dev/null +++ b/src/STPManager/DifficultyScore.h @@ -0,0 +1,58 @@ +#ifndef DIFFICULTYSCORE_H_ +#define DIFFICULTYSCORE_H_ + +#include "../AST/AST.h" +#include "../AST/AST.h" +#include "../AST/ASTKind.h" + +// estimate how difficult that input is to solve based on some simple rules. + +namespace BEEV +{ +struct DifficultyScore +{ + typedef map Cache; + + static bool isLikeMultiplication(const Kind& k) + { + return k == BVMULT || k == BVDIV || k == BVMOD || k == SBVDIV || k == SBVREM || k == SBVMOD; + } + + static int visit(const ASTNode& b, Cache& cache) + { + Cache::iterator it; + + if ((it = cache.find(b)) != cache.end()) + return 0; // already included. + + int score= 0; + if (isLikeMultiplication(b.GetKind())) + score += (b.GetValueWidth() * b.GetValueWidth() ); + else + score += b.GetValueWidth(); + + const ASTVec& c = b.GetChildren(); + ASTVec::const_iterator itC = c.begin(); + ASTVec::const_iterator itendC = c.end(); + for (; itC != itendC; itC++) + { + score += visit(*itC, cache); + } + + cache[b] = score; + return score; + } + + static int score(const ASTNode& top) + { + Cache cache; + int result = visit(top,cache); + return result; + } +}; +}; + +#endif /* DIFFICULTYSCORE_H_ */ + + + diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 3fe4c0a..cc4608d 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -8,6 +8,7 @@ ********************************************************************/ #include "STP.h" +#include "DifficultyScore.h" namespace BEEV { @@ -81,6 +82,9 @@ namespace BEEV { bm->ASTNodeStats("input asserts and query: ", inputToSAT); ASTNode simplified_solved_InputToSAT = inputToSAT; + + long initial_difficulty_score = DifficultyScore::score(original_input); + //round of substitution, solving, and simplification. ensures that //DAG is minimized as much as possibly, and ideally should //garuntee that all liketerms in BVPLUSes have been combined. @@ -177,11 +181,42 @@ namespace BEEV { bm->SimplifyWrites_InPlace_Flag = false; bm->Begin_RemoveWrites = false; + + long final_difficulty_score = DifficultyScore::score(simplified_solved_InputToSAT); + if (bm->UserFlags.stats_flag) + { + cerr << "Initial Difficulty Score:" << initial_difficulty_score <UserFlags.optimize_flag; + if (final_difficulty_score > 2 *initial_difficulty_score && !containsArrayOps(orig_input)) + { + // If the simplified problem is harder, than the + // initial problem we revert back to the initial + // problem. + + if (bm->UserFlags.stats_flag) + cerr << "simplification made the problem harder, reverting."<ClearAllTables(); + + // The arrayTransformer calls simplify. We don't want + // it to put back in all the bad simplifications. + bm->UserFlags.optimize_flag = false; + } + simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT); bm->ASTNodeStats("after transformation: ", simplified_solved_InputToSAT); bm->TermsAlreadySeenMap_Clear(); + bm->UserFlags.optimize_flag = optimize_enabled; + SOLVER_RETURN_TYPE res; if (bm->UserFlags.arrayread_refinement_flag) { diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 540e7e7..f406029 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -150,6 +150,11 @@ namespace BEEV return substitutionMap.CheckSubstitutionMap(key,output); } + ASTNode Simplifier::applySubstitutionMap(const ASTNode& n) + { + return substitutionMap.applySubstitutionMap(n); + } + bool Simplifier::CheckSubstitutionMap(const ASTNode& key) { return substitutionMap.CheckSubstitutionMap(key); @@ -263,8 +268,7 @@ namespace BEEV Simplifier::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - // if (!optimize_flag) - // return b; + assert(_bm->UserFlags.optimize_flag); Kind kind = b.GetKind(); if (BOOLEAN_TYPE != b.GetType()) @@ -1592,7 +1596,9 @@ namespace BEEV Simplifier::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) { - if (actualInputterm.isConstant()) + assert(_bm->UserFlags.optimize_flag); + + if (actualInputterm.isConstant()) return actualInputterm; ASTNode inputterm(actualInputterm); // mutable local copy. diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h index f33074a..b6dc3cf 100644 --- a/src/simplifier/simplifier.h +++ b/src/simplifier/simplifier.h @@ -112,6 +112,7 @@ namespace BEEV bool CheckSubstitutionMap(const ASTNode& a); bool UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1); + ASTNode applySubstitutionMap(const ASTNode& n); void ResetSimplifyMaps(void); -- 2.47.3