Improvement. For some bechmarks anyway. Completely bit-blast small problems when...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1539 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 088e4eace407d9a42fd4419bae0358e073391c14..b05ddd8faf9faabfbf80f36e0c826240f834e209 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -88,7 +88,7 @@ namespace BEEV {
   } //End of TopLevelSTP()
   
   ASTNode
-  STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score)
+  STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score, int & actualBBSize)
   {
     while (true)
       {
@@ -98,6 +98,8 @@ namespace BEEV {
           break;
       }
 
+    actualBBSize=-1;
+
     // Expensive, so only want to do it once.
     if (bm->UserFlags.isSet("bitblast-simplification", "1") && initial_difficulty_score < 250000)
       {
@@ -112,6 +114,7 @@ namespace BEEV {
             simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
             bm->ASTNodeStats(bb_message.c_str(), simplified_solved_InputToSAT);
           }
+        actualBBSize =  bbnm.totalNumberOfNodes();
       }
     return simplified_solved_InputToSAT;
   }
@@ -238,17 +241,23 @@ namespace BEEV {
 
     unsigned initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
 
+    int bitblasted_difficulty = -1;
+
     // Fixed point it if it's not too difficult.
     // Currently we discards all the state each time sizeReducing is called,
     // so it's expensive to call.
     if ((!arrayops && initial_difficulty_score < 1000000) || bm->UserFlags.isSet("preserving-fixedpoint", "0"))
-           simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get(), initial_difficulty_score);
+           simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver.get(),pe.get(), initial_difficulty_score, bitblasted_difficulty);
 
     if ((!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")))
       {
         initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
       }
 
+    if (bitblasted_difficulty != -1 && bm->UserFlags.stats_flag)
+      cout << "Initial Bitblasted size:" << bitblasted_difficulty << endl;
+
+
     if (bm->UserFlags.stats_flag)
       cout << "Difficulty After Size reducing:" << initial_difficulty_score << endl;
 
@@ -430,6 +439,31 @@ namespace BEEV {
     //bm->Begin_RemoveWrites = false;
 
     long final_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
+
+    bool worse= false;
+    if (final_difficulty_score > 1.1 * initial_difficulty_score)
+        worse = true;
+
+    // It's of course very wasteful to do this! Later I'll make it reuse the work..
+    // We bit-blast again, in order to throw it away, so that we can measure whether
+    // the number of AIG nodes is smaller. The difficulty score is sometimes completely
+    // wrong, the sage-app7 are the motivating examples. The other way to improve it would
+    // be to fix the difficulty scorer!
+    if (!worse && (bitblasted_difficulty != -1))
+     {
+        BBNodeManagerAIG bbnm;
+        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
+        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
+        bb.BBForm(simplified_solved_InputToSAT);
+        int newBB=  bbnm.totalNumberOfNodes();
+        if (bm->UserFlags.stats_flag)
+          cerr << "Final BB Size:" << newBB << endl;
+
+        if (bitblasted_difficulty < newBB)
+          worse = true;
+    }
+
+
     if (bm->UserFlags.stats_flag)
       {
         cerr << "Initial Difficulty Score:" << initial_difficulty_score << endl;
@@ -437,7 +471,7 @@ namespace BEEV {
       }
 
     bool optimize_enabled = bm->UserFlags.optimize_flag;
-    if (final_difficulty_score > 1.1 * initial_difficulty_score &&
+    if (worse &&
        (!arrayops || bm->UserFlags.isSet("array-difficulty-reversion", "1")) &&
        bm->UserFlags.isSet("difficulty-reversion", "1"))
       {

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index b5bade0f4e6f4f044fca9129e3df775664fc0f16..4ff85f42b8552848bdc437cb494e184d88017bda 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -51,7 +51,7 @@ namespace BEEV
 ArrayTransformer * arrayTransformer;
     
           // calls sizeReducing and the bitblasting simplification.
-          ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score);
+          ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, PropagateEqualities *pe, const int initial_difficulty_score, int & actualBBSize);
 
 
     /****************************************************************

diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h
index d176f88a3fb80c85c8e88c8e7b0ab728cdda8f91..a712c41ac9fb59a380b0eec714bcd2c6e035db4b 100644 (file)
--- a/src/to-sat/AIG/BBNodeManagerAIG.h
+++ b/src/to-sat/AIG/BBNodeManagerAIG.h
@@ -38,6 +38,12 @@ public:
         typedef map<ASTNode, vector<BBNodeAIG> > SymbolToBBNode;
 
         SymbolToBBNode symbolToBBNode;
+
+        int totalNumberOfNodes()
+        {
+          return aigMgr->nObjs[AIG_OBJ_AND]; // without having removed non-reachable.
+        }
+
 private:
         // AIGs can only take two parameters. This makes a log_2 height
         // tower of varadic inputs.