Refactor. rename a configuration property.

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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index b92a28353b77a930eca6bd5b7e4de1fd743ae9c9..5040345ba66c948d84a1fa6ed5251e92d33590a7 100644 (file)
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -53,7 +53,7 @@ namespace BEEV
           bm->UserFlags.print_arrayval_declaredorder_flag = true;
           break;
         case 'r':
-          bm->UserFlags.arrayread_refinement_flag = false;
+          bm->UserFlags.ackermannisation = true;
           break;
         case 's' :
           bm->UserFlags.stats_flag = true;

diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index de4bdbc2e80c6261050a30ad59344a83751027ac..42eb09e2e8edb0ad70f204bee2f3be76a1891684 100644 (file)
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -51,7 +51,7 @@ namespace BEEV
 
 
     // This establishes equalities between every indexes, and a fresh variable.
-    if (bm->UserFlags.arrayread_refinement_flag)
+    if (!bm->UserFlags.ackermannisation)
     {
                ASTNodeMap replaced;
 
@@ -586,7 +586,7 @@ namespace BEEV
 
           result = CurrentSymbol;
 
-          if (bm->UserFlags.arrayread_refinement_flag)
+          if (!bm->UserFlags.ackermannisation)
             {
               // result is a variable here; it is an ite in the
               // else-branch

diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp
index 084a1f6c2880151a0ff3a526ebf7ca69947ce5ba..d790488acd08c20c90d6bb79d33e6e0fa02db9b5 100644 (file)
--- a/src/STPManager/STP.cpp
+++ b/src/STPManager/STP.cpp
@@ -214,7 +214,7 @@ namespace BEEV {
     // TODO: Should be enabled irrespective of whether refinement is enabled.
     // TODO: I chose the number of reads we perform this operation at randomly.
     bool removed = false;
-    if (!bm->UserFlags.arrayread_refinement_flag && numberOfReadsLessThan(simplified_solved_InputToSAT,50))
+    if (bm->UserFlags.ackermannisation && numberOfReadsLessThan(simplified_solved_InputToSAT,50))
       {
           // If the number of axioms that would be added it small. Remove them.
               simplified_solved_InputToSAT = arrayTransformer->TransformFormula_TopLevel(simplified_solved_InputToSAT);
@@ -460,7 +460,7 @@ namespace BEEV {
     bm->UserFlags.optimize_flag = optimize_enabled;
 
     SOLVER_RETURN_TYPE res;
-    if (bm->UserFlags.arrayread_refinement_flag)
+    if (!bm->UserFlags.ackermannisation)
       {
         bm->counterexample_checking_during_refinement = true;
       }
@@ -478,7 +478,7 @@ namespace BEEV {
     if (bm->UserFlags.stats_flag)
       simp->printCacheStatus();
 
-    const bool maybeRefinement = arrayops && bm->UserFlags.arrayread_refinement_flag;
+    const bool maybeRefinement = arrayops && !bm->UserFlags.ackermannisation;
 
     simplifier::constantBitP::ConstantBitPropagation* cb = NULL;
     std::auto_ptr<simplifier::constantBitP::ConstantBitPropagation> cleaner;
@@ -518,7 +518,7 @@ namespace BEEV {
       }
 
     assert(arrayops); // should only go to abstraction refinement if there are array ops.
-    assert(bm->UserFlags.arrayread_refinement_flag); // Refinement must be enabled too.
+    assert(!bm->UserFlags.ackermannisation); // Refinement must be enabled too.
     assert (bm->UserFlags.solver_to_use != UserDefinedFlags::MINISAT_PROPAGATORS); // The array solver shouldn't have returned undecided..
 
     res = Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, original_input, satBase);

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 7fdcb313defefa77fc1102268b1821a78f9fac1f..3e83589e27e4fd15cf972a09fed39352d107722f 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -39,11 +39,11 @@ namespace BEEV
     //run STP in optimized mode
     bool optimize_flag;
     
-    //do sat refinement, i.e. underconstraint the problem, and feed to
+    //do sat refinement, i.e. underconstrain the problem, and feed to
     //SAT. if this works, great. else, add a set of suitable constraints
     //to re-constraint the problem correctly, and call SAT again, until
     //all constraints have been added.
-    bool arrayread_refinement_flag;
+    bool ackermannisation; // eagerly write through the array's function congruence axioms.
     
     //switch to control write refinements
     //bool arraywrite_refinement_flag;
@@ -198,7 +198,7 @@ namespace BEEV
       // SAT. if this works, great. else, add a set of suitable
       // constraints to re-constraint the problem correctly, and call SAT again, 
       // until all constraints have been added.
-      arrayread_refinement_flag = true;
+      ackermannisation = false;
   
       //flag to control write refinement
       //arraywrite_refinement_flag = true;

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 4e818b6cf22fe275dace9a97179e9cec056faaf1..9d9c7211d6ba58337a67b46462bef8477ee46d07 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -141,7 +141,7 @@ namespace BEEV
             }
 
         // One modified version of Minisat has an array propagator based solver built in. So this block sends the details of the arrays to it.
-        if ((bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) &&  bm->UserFlags.arrayread_refinement_flag )
+        if ((bm->UserFlags.solver_to_use == UserDefinedFlags::MINISAT_PROPAGATORS) &&  !bm->UserFlags.ackermannisation )
             {
                 int array_id = 0; // Is incremented for each distinct array.
                 bool found = false;