Add a public function that calls sizeReducing until fixed point (under some conditions.)

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 7cfd1705cc3943b8bd2c85a61b74e2d34df51cdf..bf8a30bdade982f66635f684611856943ba67a7b 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -86,6 +86,35 @@ namespace BEEV {
 
   } //End of TopLevelSTP()
   
+  ASTNode
+  STP::callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score)
+  {
+    while (true)
+      {
+        ASTNode last = simplified_solved_InputToSAT;
+        simplified_solved_InputToSAT = sizeReducing(last, bvSolver);
+        if (last == simplified_solved_InputToSAT)
+          break;
+      }
+
+    // Expensive, so only want to do it once.
+    if (bm->UserFlags.isSet("bitblast-simplification", "1") && initial_difficulty_score < 250000)
+      {
+        BBNodeManagerAIG bbnm;
+        SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
+        BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
+        ASTNodeMap fromTo;
+        bb.getConsts(simplified_solved_InputToSAT, fromTo);
+        if (fromTo.size() > 0)
+          {
+            ASTNodeMap cache;
+            simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
+            bm->ASTNodeStats("After bitblast simplification: ", simplified_solved_InputToSAT);
+          }
+      }
+    return simplified_solved_InputToSAT;
+  }
+
 
   // These transformations should never increase the size of the DAG.
    ASTNode
@@ -195,29 +224,7 @@ namespace BEEV {
     // so it's expensive to call.
     if (!arrayops && initial_difficulty_score < 1000000)
       {
-        while (true)
-          {
-            ASTNode last = simplified_solved_InputToSAT;
-            simplified_solved_InputToSAT = sizeReducing(last, bvSolver);
-            if (last == simplified_solved_InputToSAT)
-              break;
-          }
-
-        // Expensive, so only want to do it once.
-        if (bm->UserFlags.isSet("bitblast-simplification", "1") && initial_difficulty_score < 250000)
-          {
-            BBNodeManagerAIG bbnm;
-            SimplifyingNodeFactory nf(*(bm->hashingNodeFactory), *bm);
-            BitBlaster<BBNodeAIG, BBNodeManagerAIG> bb(&bbnm, simp, &nf , &(bm->UserFlags));
-            ASTNodeMap fromTo;
-            bb.getConsts(simplified_solved_InputToSAT, fromTo);
-            if (fromTo.size() > 0)
-              {
-                ASTNodeMap cache;
-                simplified_solved_InputToSAT = SubstitutionMap::replace(simplified_solved_InputToSAT, fromTo, cache,&nf);
-                bm->ASTNodeStats("After bitblast simplification: ", simplified_solved_InputToSAT);
-              }
-          }
+        simplified_solved_InputToSAT = callSizeReducing(simplified_solved_InputToSAT, bvSolver, initial_difficulty_score);
         initial_difficulty_score = difficulty.score(simplified_solved_InputToSAT);
       }
 

diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h
index 2973d1763397042edf311f67f559c17e1c94296a..9de176e31d445c375ac149c1778366e7796a2d04 100644 (file)
--- a/src/STPManager/STP.h
+++ b/src/STPManager/STP.h
@@ -26,10 +26,14 @@
 namespace BEEV
 {
   class STP {
-public:
-         ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver);
+  private:
+          ASTNode sizeReducing(ASTNode input, BVSolver* bvSolver);
 
   public:
+          // calls sizeReducing and the bitblasting simplification.
+          ASTNode callSizeReducing(ASTNode simplified_solved_InputToSAT, BVSolver* bvSolver, const int initial_difficulty_score);
+
+
     /****************************************************************
      * Public Data:
      *