more cleanup

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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index cec92f9367cf01499ce3c389e97d1ca8fa7b086a..0bbcb7749010f342a5b88fc479f2e0a43249d315 100644 (file)
--- a/src/AST/AST.h
+++ b/src/AST/AST.h
@@ -1218,12 +1218,15 @@ namespace BEEV
     void ClearAllTables(void);
     void ClearAllCaches(void);
     int  BeforeSAT_ResultCheck(const ASTNode& q);
-    int  CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
-    int  SATBased_ArrayReadRefinement(MINISAT::Solver& newS, const ASTNode& q, const ASTNode& orig_input);
+    int  CallSAT_ResultCheck(MINISAT::Solver& newS, 
+                            const ASTNode& q, const ASTNode& orig_input);
+    int  SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
+                                     const ASTNode& q, const ASTNode& orig_input);
     int  SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input);
         
     int  SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, const ASTNode& orig_input);
-    void Expand_FiniteLoop(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap);
+    void Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input,
+                          const ASTNode& finiteloop,ASTNodeMap* ParamToCurrentValMap);
     ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, 
                                              ASTNodeMap* VarConstMap);
 

diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp
index 63f2dff90e59887b2f5365af092d40f2665329e0..9b860fa75fa20a96fc2bb318ccf563a884609f72 100644 (file)
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/AST/AbstractionRefinement.cpp
@@ -17,8 +17,9 @@ namespace BEEV
    * Abstraction Refinement related functions
    ******************************************************************/  
   
-  int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& newS, 
-                                            const ASTNode& q, const ASTNode& orig_input) {
+  int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, 
+                                            const ASTNode& inputAlreadyInSAT, 
+                                           const ASTNode& original_input) {
     //go over the list of indices for each array, and generate Leibnitz
     //axioms. Then assert these axioms into the SAT solver. Check if the
     //addition of the new constraints has made the bogus counterexample
@@ -55,7 +56,8 @@ namespace BEEV
            iset_end = _arrayname_readindices.end(); iset != iset_end; iset++)
       {
         ASTVec listOfIndices = iset->second;
-        //loop over the list of indices for the array and create LA, and add to q
+        //loop over the list of indices for the array and create LA,
+        //and add to inputAlreadyInSAT
         for (ASTVec::iterator it = listOfIndices.begin(),
                itend = listOfIndices.end(); it != itend; it++)
           {
@@ -118,7 +120,7 @@ namespace BEEV
             //if (FalseAxiomsVec.size() > 0)
             if (FalseAxiomsVec.size() > oldFalseAxiomsSize)
               {
-                res2 = CallSAT_ResultCheck(newS, FalseAxioms, orig_input);
+                res2 = CallSAT_ResultCheck(SatSolver, FalseAxioms, original_input);
                 oldFalseAxiomsSize = FalseAxiomsVec.size();
               }
             //printf("spot 02, res2 = %d\n", res2);
@@ -132,7 +134,7 @@ namespace BEEV
       (RemainingAxiomsVec.size() > 1) ? 
       CreateNode(AND, RemainingAxiomsVec) : RemainingAxiomsVec[0];
     ASTNodeStats("adding remaining readaxioms to SAT: ", RemainingAxioms);
-    return CallSAT_ResultCheck(newS, RemainingAxioms, orig_input);
+    return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input);
   } //end of SATBased_ArrayReadRefinement
 
   ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, const ASTNode& newvar)
@@ -148,7 +150,7 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
-  int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input)
+  int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, const ASTNode& original_input)
   {
     ASTNode writeAxiom;
     ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin();
@@ -184,7 +186,7 @@ namespace BEEV
     int res2 = 2;
     if (FalseAxioms.size() > oldFalseAxiomsSize)
       {
-        res2 = CallSAT_ResultCheck(newS, writeAxiom, orig_input);
+        res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input);
         oldFalseAxiomsSize = FalseAxioms.size();
       }
     if (2 != res2)
@@ -196,7 +198,7 @@ namespace BEEV
       (RemainingAxioms.size() != 1) ? 
       CreateNode(AND, RemainingAxioms) : RemainingAxioms[0];
     ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom);
-    res2 = CallSAT_ResultCheck(newS, writeAxiom, orig_input);
+    res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input);
     if (2 != res2)
       {
         return res2;
@@ -207,8 +209,8 @@ namespace BEEV
 
   //Expands all finite-for-loops using counterexample-guided
   //abstraction-refinement.
-  int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, 
-                                              const ASTNode& orig_input)
+  int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, 
+                                              const ASTNode& original_input)
   {
     /*
      * For each 'finiteloop' in the global list 'List_Of_FiniteLoops'
@@ -229,8 +231,10 @@ namespace BEEV
      */
   }
 
-  void BeevMgr::Expand_FiniteLoop(const ASTNode& finiteloop,
-                                 ASTNodeMap* ParamToCurrentValMap) {
+  void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver,
+                                 const ASTNode& original_input,
+                                 const ASTNode& finiteloop,
+                                 ASTNodeMap* ParamToCurrentValMap) {
     /*
      * 'finiteloop' is the finite loop to be expanded
      * 
@@ -300,7 +304,8 @@ namespace BEEV
       { 
       while(paramCurrentValue < paramLimit) 
        {
-         Expand_FiniteLoop(formulabody, ParamToCurrentValMap);
+         Expand_FiniteLoop(SatSolver, original_input,
+                           formulabody, ParamToCurrentValMap);
          paramCurrentValue = paramCurrentValue + paramIncrement;
 
          //Update ParamToCurrentValMap with parameter and its current
@@ -327,7 +332,7 @@ namespace BEEV
 
        int result = 0;
        if(ASTFalse == formulaInModel) {
-         //result = CallSAT_ResultCheck(newS, currentFormula, orig_input);
+         result = CallSAT_ResultCheck(SatSolver, currentFormula, original_input);
        }
 
         //Update ParamToCurrentValMap with parameter and its current

diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp
index 1055068a90a00eeef817cf8e1c523f03f9ce4331..3ceb73c45bd95b124355a5bf4188547f5114c837 100644 (file)
--- a/src/AST/ToCNF.cpp
+++ b/src/AST/ToCNF.cpp
@@ -1,3 +1,12 @@
+/********************************************************************
+ * AUTHORS: Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
 #include "AST.h"
 #include "../simplifier/bvsolver.h"
 

diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp
index cd9dbda0d8cbed0beded416614292eefd18a3048..f716c6a199ffa9c3721fe3cd0a9e7f55b0445e14 100644 (file)
--- a/src/AST/ToSAT.cpp
+++ b/src/AST/ToSAT.cpp
@@ -916,11 +916,11 @@ namespace BEEV
   //if returned 2 then ERROR
   int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts)
   {
-    ASTNode q = inputasserts;
-    ASTNode orig_input = q;
-    ASTNodeStats("input asserts and query: ", q);
+    ASTNode inputToSAT = inputasserts;
+    ASTNode orig_input = inputToSAT;
+    ASTNodeStats("input asserts and query: ", inputToSAT);
 
-    ASTNode newq = q;
+    ASTNode simplified_solved_InputToSAT = inputToSAT;
     //round of substitution, solving, and simplification. ensures that
     //DAG is minimized as much as possibly, and ideally should
     //garuntee that all liketerms in BVPLUSes have been combined.
@@ -931,64 +931,71 @@ namespace BEEV
     TermsAlreadySeenMap.clear();
     do
       {
-        q = newq;
-        newq = CreateSubstitutionMap(newq);
+        inputToSAT = simplified_solved_InputToSAT;
+        simplified_solved_InputToSAT = 
+         CreateSubstitutionMap(simplified_solved_InputToSAT);
         //printf("##################################################\n");
-        ASTNodeStats("after pure substitution: ", newq);
-        newq = SimplifyFormula_TopLevel(newq, false);
-        ASTNodeStats("after simplification: ", newq);
-        newq = bvsolver.TopLevelBVSolve(newq);
-        ASTNodeStats("after solving: ", newq);
-      } while (q != newq);
-
-    ASTNodeStats("Before SimplifyWrites_Inplace begins: ", newq);
+        ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+        simplified_solved_InputToSAT = 
+         SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+        ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+        simplified_solved_InputToSAT = 
+         bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+        ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+      } while (inputToSAT != simplified_solved_InputToSAT);
+
+    ASTNodeStats("Before SimplifyWrites_Inplace begins: ", simplified_solved_InputToSAT);
     SimplifyWrites_InPlace_Flag = true;
     Begin_RemoveWrites = false;
     start_abstracting = false;
     TermsAlreadySeenMap.clear();
     do
       {
-        q = newq;
-        newq = CreateSubstitutionMap(newq);
-        ASTNodeStats("after pure substitution: ", newq);
-        newq = SimplifyFormula_TopLevel(newq, false);
-        ASTNodeStats("after simplification: ", newq);
-        newq = bvsolver.TopLevelBVSolve(newq);
-        ASTNodeStats("after solving: ", newq);
-      } while (q != newq);
-    ASTNodeStats("After SimplifyWrites_Inplace: ", newq);
+        inputToSAT = simplified_solved_InputToSAT;
+        simplified_solved_InputToSAT = 
+         CreateSubstitutionMap(simplified_solved_InputToSAT);
+        ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+        simplified_solved_InputToSAT = 
+         SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+        ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+        simplified_solved_InputToSAT = 
+         bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+        ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+      } while (inputToSAT != simplified_solved_InputToSAT);
+    ASTNodeStats("After SimplifyWrites_Inplace: ", simplified_solved_InputToSAT);
 
     start_abstracting = (arraywrite_refinement_flag) ? true : false;
     SimplifyWrites_InPlace_Flag = false;
     Begin_RemoveWrites = (start_abstracting) ? false : true;
     if (start_abstracting)
       {
-        ASTNodeStats("before abstraction round begins: ", newq);
+        ASTNodeStats("before abstraction round begins: ", simplified_solved_InputToSAT);
       }
 
     TermsAlreadySeenMap.clear();
     do
       {
-        q = newq;
-        //newq = CreateSubstitutionMap(newq);
+        inputToSAT = simplified_solved_InputToSAT;
+        //simplified_solved_InputToSAT = CreateSubstitutionMap(simplified_solved_InputToSAT);
         //Begin_RemoveWrites = true;
-        //ASTNodeStats("after pure substitution: ", newq);
-        newq = SimplifyFormula_TopLevel(newq, false);
-        //ASTNodeStats("after simplification: ", newq);
-        //newq = bvsolver.TopLevelBVSolve(newq);
-        //ASTNodeStats("after solving: ", newq);
-      } while (q != newq);
+        //ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT);
+        simplified_solved_InputToSAT = 
+         SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false);
+        //ASTNodeStats("after simplification: ", simplified_solved_InputToSAT);
+        //simplified_solved_InputToSAT = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT);
+        //ASTNodeStats("after solving: ", simplified_solved_InputToSAT);
+      } while (inputToSAT != simplified_solved_InputToSAT);
 
     if (start_abstracting)
       {
-        ASTNodeStats("After abstraction: ", newq);
+        ASTNodeStats("After abstraction: ", simplified_solved_InputToSAT);
       }
     start_abstracting = false;
     SimplifyWrites_InPlace_Flag = false;
     Begin_RemoveWrites = false;
 
-    newq = TransformFormula_TopLevel(newq);
-    ASTNodeStats("after transformation: ", newq);
+    simplified_solved_InputToSAT = TransformFormula_TopLevel(simplified_solved_InputToSAT);
+    ASTNodeStats("after transformation: ", simplified_solved_InputToSAT);
     TermsAlreadySeenMap.clear();
 
     //if(stats_flag)
@@ -1004,14 +1011,14 @@ namespace BEEV
         counterexample_checking_during_refinement = true;
       }
 
-    res = CallSAT_ResultCheck(newS, newq, orig_input);
+    res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input);
     if (2 != res)
       {
         CountersAndStats("print_func_stats");
         return res;
       }
 
-    res = SATBased_ArrayReadRefinement(newS, newq, orig_input);
+    res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
     if (2 != res)
       {
         CountersAndStats("print_func_stats");
@@ -1025,7 +1032,7 @@ namespace BEEV
         return res;
       }
 
-    res = SATBased_ArrayReadRefinement(newS, newq, orig_input);
+    res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input);
     if (2 != res)
       {
         CountersAndStats("print_func_stats");