From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 3 Jan 2011 05:11:54 +0000 (+0000)
Subject: * Remove the arraywrite_refinement_flag boolean flag. It didn't seem to do anything.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=31367111ca26b15299b319581cddd346ffc8ee62;p=francis%2Fstp.git

* 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 28036f0..e5bdf7e 100644
--- 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 fd73c53..db38a4a 100644
--- 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 d0569b8..d9139b9 100644
--- 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 ab3f89b..e3c2e03 100644
--- 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;