* Remove the arraywrite_refinement_flag boolean flag. It didn't seem to do anything.

* If refinement is turned off, then use the AIG CNF conversion code (which is much much better).

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

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 28036f08c5f57bbbe7be5c6e6f3109bfe11fdcaa..e5bdf7e6d460a4b9128fbc0e9082fe5374b87953 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -1,6 +1,6 @@
 // -*- c++ -*-
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -187,21 +187,8 @@ namespace BEEV {
     bm->ASTNodeStats("After SimplifyWrites_Inplace: ", 
                      simplified_solved_InputToSAT);
 
-    bm->start_abstracting = 
-      (bm->UserFlags.arraywrite_refinement_flag) ? true : false;
-    bm->SimplifyWrites_InPlace_Flag = false;
-    bm->Begin_RemoveWrites = (bm->start_abstracting) ? false : true;
-    if (bm->start_abstracting)
-      {
-        bm->ASTNodeStats("before abstraction round begins: ", 
-                         simplified_solved_InputToSAT);
-      }
-
     bm->TermsAlreadySeenMap_Clear();
-    if (bm->start_abstracting)
-      {
-        bm->ASTNodeStats("After abstraction: ", simplified_solved_InputToSAT);
-      }
+
     bm->start_abstracting = false;
     bm->SimplifyWrites_InPlace_Flag = false;
     bm->Begin_RemoveWrites = false;
@@ -259,7 +246,7 @@ namespace BEEV {
     bvsolver = new BVSolver(bm,simp);
 
     // If it doesn't contain array operations, use ABC's CNF generation.
-    if (!arrayops)
+    if (!arrayops || !bm->UserFlags.arrayread_refinement_flag)
     {
       simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
 
@@ -306,13 +293,7 @@ namespace BEEV {
       }
 
     assert(arrayops); // should only go to abstraction refinement if there are array ops.
-
-    // res = SATBased_AllFiniteLoops_Refinement(NewSolver, orig_input);
-    //     if (SOLVER_UNDECIDED != res)
-    //       {
-    //  CountersAndStats("print_func_stats");
-    //         return res;      
-    //       }
+    assert(bm->UserFlags.arrayread_refinement_flag); // Refinement must be enabled too.
 
     res = 
       Ctr_Example->SATBased_ArrayReadRefinement(NewSolver,

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index fd73c53c8b568bfc7feaa1bc6b600730421f27c5..db38a4a68b22f6f5e6f41373fa1e654fe3e46b9a 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -42,7 +42,7 @@ namespace BEEV
     bool arrayread_refinement_flag;
     
     //switch to control write refinements
-    bool arraywrite_refinement_flag;
+    //bool arraywrite_refinement_flag;
     
     //check the counterexample against the original input to STP
     bool check_counterexample_flag;
@@ -191,7 +191,7 @@ namespace BEEV
       arrayread_refinement_flag = true;
   
       //flag to control write refinement
-      arraywrite_refinement_flag = true;
+      //arraywrite_refinement_flag = true;
       
       //check the counterexample against the original input to STP
       check_counterexample_flag = true;

diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp
index d0569b82873b257110a0aa0131629b06c1a1e650..d9139b95c899e4f035d9b8b2a48c0041a5c918bb 100644 (file)
--- a/src/c_interface/c_interface.cpp
+++ b/src/c_interface/c_interface.cpp
@@ -121,7 +121,7 @@ void vc_setFlags(VC vc, char c, int param_value) {
     b->UserFlags.stats_flag = true;
     break;
   case 'u':
-    b->UserFlags.arraywrite_refinement_flag = false;
+    //b->UserFlags.arraywrite_refinement_flag = false;
     break;
   case 'v' :
     b->UserFlags.print_nodes_flag = true;

diff --git a/src/main/main.cpp b/src/main/main.cpp
index ab3f89b8e6462a3477b3a55226e1b6f27ef18685..e3c2e03b256dd467fc9831ae23069550b87c5945 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -388,7 +388,7 @@ int main(int argc, char ** argv) {
               bm->UserFlags.quick_statistics_flag = true;
               break;
             case 'u':
-              bm->UserFlags.arraywrite_refinement_flag = false;
+              //bm->UserFlags.arraywrite_refinement_flag = false;
               break;
             case 'v' :
               bm->UserFlags.print_nodes_flag = true;