Measure the difficulty of formula by using a simple function, that amongst other...

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

diff --git a/src/STPManager/DifficultyScore.h b/src/STPManager/DifficultyScore.h
new file mode 100644 (file)
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<ASTNode,int> 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 3fe4c0a149ab9eabf49b059fbfe7574ed4910b21..cc4608d61a5c3d95a6b22ffe127a2abc865967bb 100644 (file)
--- 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 <<endl;
+       cerr << "Final Difficulty Score:" << final_difficulty_score <<endl;
+    }
+
+    bool optimize_enabled = bm->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."<<endl;
+       simplified_solved_InputToSAT = original_input;
+
+       // I do this to clear the substitution/solver map.
+       // Not sure what would happen if it contained simplifications
+       // that haven't been applied.
+       simp->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 540e7e79eee7133f767817193f98a031916ff9d9..f406029f350fadc04bd8e64f233adac90c73e00e 100644 (file)
--- 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 f33074a1d7b1dfbd8aad622340afb8252cec7f69..b6dc3cf8a320b83242343f2cf28b1980a1aadeca 100644 (file)
--- 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);