Refactor. Remove some commented out code. No idea what it did.

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

diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h
index a1a8f8fb4b4d57ce3eb1e1da87655373e6694373..efd2e91f598a1caaa1438ecb041d819667f91fa6 100644 (file)
--- a/src/absrefine_counterexample/AbsRefine_CounterExample.h
+++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h
@@ -40,9 +40,6 @@ namespace BEEV
     // Ptr to ArrayTransformer
     ArrayTransformer * ArrayTransform;
       
-    // Ptr to ToSAT
-    //ToSATBase * tosat;
-
     // Checks if the counterexample is good. In order for the
     // counterexample to be ok, every assert must evaluate to true
     // w.r.t couner_example, and the query must evaluate to
@@ -83,20 +80,19 @@ namespace BEEV
       ASTUndefined = bm->CreateNode(UNDEFINED);
     }
 
+    //Prints the counterexample to stdout
+    void PrintCounterExample(bool t, std::ostream& os = cout);
+      
     void ClearCounterExampleMap(void)
     {
       CounterExampleMap.clear();
     }
 
-    void ClearComputeFormulaMap(void) 
+    void ClearComputeFormulaMap(void)
     {
       ComputeFormulaMap.clear();
     }
 
-      
-    //Prints the counterexample to stdout
-    void PrintCounterExample(bool t, std::ostream& os = cout);
-      
     //Prints the counterexample to stdout
     void PrintCounterExample_InOrder(bool t);
       
@@ -147,23 +143,6 @@ namespace BEEV
     SATBased_ArrayWriteRefinement(SATSolver& newS,
                                   const ASTNode& orig_input,
                                   ToSATBase *tosat);
-    
-    //     SOLVER_RETURN_TYPE
-    // SATBased_AllFiniteLoops_Refinement(SATSolver& newS,
-    // const ASTNode& orig_input);
-      
-    //     ASTVec SATBased_FiniteLoop_Refinement(SATSolver&
-    // SatSolver, const ASTNode& original_input, const ASTNode&
-    // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
-    // absrefine_flag=false);
-      
-    //     ASTNode Check_FiniteLoop_UsingModel(const ASTNode&
-    // finiteloop, ASTNodeMap* ParamToCurrentValMap, bool
-    // CheckUsingModel_Or_Expand);
-    //
-    //     ASTNode Expand_FiniteLoop_TopLevel(const ASTNode&
-    //     finiteloop); ASTNode Check_FiniteLoop_UsingModel(const
-    //     ASTNode& finiteloop);
 
     void ClearAllTables(void)
     {

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index ce31f605fcc6f931c2387c3932c182bfe6a21574..9fda21d1aef53b90f26353c86237dbceafb94db4 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -266,416 +266,4 @@ namespace BEEV
     return arraywrite_axiom;
   }//end of Create_ArrayWriteAxioms()
 
-  //   static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, 
-  //                            const ASTNode& key, const ASTNode& value)
-  //   {
-  //     ASTNodeMap::iterator it = VarToConstMap->find(key);
-  //     if(it != VarToConstMap->end())
-  //       {
-  //    VarToConstMap->erase(it);       
-  //       }
-
-  //     (*VarToConstMap)[key] = value;
-  //     return;   
-  //   }
-
-
-  //   /******************************************************************
-  //    * FINITE FORLOOP ABSTRACTION REFINEMENT
-  //    *
-  //    * For each 'finiteloop' in the list 'GlobalList_Of_FiniteLoops'
-  //    *
-  //    * Expand_FiniteLoop(finiteloop);
-  //    *
-  //    * The 'Expand_FiniteLoop' function expands the 'finiteloop' in a
-  //    * counterexample-guided refinement fashion
-  //    *
-  //    * Once all the finiteloops have been expanded, we need to go back
-  //    * and recheck that every discarded constraint is true with the
-  //    * final model. A flag 'done' is set to false if atleast one
-  //    * constraint is false during model-check, and is set to true if all
-  //    * constraints are true during model-check.
-  //    *
-  //    * if the 'done' flag is true, then we terminate this refinement
-  //    * loop.  
-  //    *****************************************************************/
-  //   SOLVER_RETURN_TYPE 
-  //   AbsRefine_CounterExample::
-  //   SATBased_AllFiniteLoops_Refinement(SATSolver& SatSolver,
-  //                                          const ASTNode& original_input)
-  //   {
-  //     cout << "The number of abs-refinement limit is " 
-  //          << num_absrefine << endl;
-  //     for(int absrefine_count=0;
-  //         absrefine_count < num_absrefine; absrefine_count++) 
-  //       {
-  //    ASTVec Allretvec0;
-  //    Allretvec0.push_back(ASTTrue);
-  //    SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;      
-  //    for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
-  //          iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-  //      {
-  //        ASTVec retvec;
-  //        ASTNodeMap ParamToCurrentValMap;
-  //        retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
-  //                                                 original_input,
-  //                                                 *i,
-  //                                                 &ParamToCurrentValMap,
-  //                                                 true); //absrefine flag
-
-  //        for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();
-  //            j!=jend;j++) 
-  //          {
-  //            Allretvec0.push_back(*j);
-  //          }
-  //        //Allretvec0.(Allretvec0.end(),retvec.begin(),retvec.end());
-  //      } //End of For
-          
-  //    ASTNode retformula = 
-  //      (Allretvec0.size() == 1) ?
-  //      Allretvec0[0] : bm->CreateNode(AND,Allretvec0);
-  //    retformula = TransformFormula_TopLevel(retformula);
-        
-  //    //Add the return value of all loops to the SAT Solver
-  //    res = 
-  //      CallSAT_ResultCheck(SatSolver, retformula, original_input);
-  //    if(SOLVER_UNDECIDED != res) 
-  //      {
-  //        return res;
-  //      }     
-  //       } //end of absrefine count
-    
-  //     ASTVec Allretvec1;
-  //     Allretvec1.push_back(ASTTrue);
-  //     SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED;     
-  //     for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),
-  //      iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++)
-  //     {
-  //       //cout << "The abs-refine didn't finish the job. "\
-  //                 "Add the remaining formulas\n";
-  //       ASTNodeMap ParamToCurrentValMap;
-  //       ASTVec retvec;
-  //       retvec =  SATBased_FiniteLoop_Refinement(SatSolver,
-  //                                           original_input,
-  //                                           *i,
-  //                                           &ParamToCurrentValMap,
-  //                                           false); //absrefine flag
-  //       for(ASTVec::iterator j=retvec.begin(),jend=retvec.end();j!=jend;j++) 
-  //    {
-  //      Allretvec1.push_back(*j);
-  //    }
-  //     } //End of For    
-        
-  //     ASTNode retformula = 
-  //       (Allretvec1.size() == 1) ?
-  //       Allretvec1[0] : bm->CreateNode(AND,Allretvec1);
-  //     retformula = TransformFormula_TopLevel(retformula);
-  //     //Add the return value of all loops to the SAT Solver
-  //     res = CallSAT_ResultCheck(SatSolver, retformula, original_input);
-  //     return res;
-  //   } //end of SATBased_AllFiniteLoops_Refinement()
-  
-  
-  //   /*****************************************************************
-  //    * SATBased_FiniteLoop_Refinement
-  //    *
-  //    * 'finiteloop' is the finite loop to be expanded
-  //    * Every finiteloop has three parts:
-  //    * 0) Parameter Name
-  //    * 1) Parameter initialization
-  //    * 2) Parameter limit value
-  //    * 3) Increment formula
-  //    * 4) Formula Body
-  //    *
-  //    * ParamToCurrentValMap contains a map from parameters to their
-  //    * current values in the recursion
-  //    *   
-  //    * Nested FORs are allowed, but only the innermost loop can have a
-  //    * formula in it
-  //    *****************************************************************/
-  //   //SATBased_FiniteLoop_Refinement
-  //   //
-  //   //Expand the finite loop, check against model, and add false
-  //   //formulas to the SAT solver
-  //   ASTVec
-  //   AbsRefine_CounterExample::
-  //   SATBased_FiniteLoop_Refinement(SATSolver& SatSolver,
-  //                                      const ASTNode& original_input,
-  //                                      const ASTNode& finiteloop,
-  //                                      ASTNodeMap* ParamToCurrentValMap,
-  //                                      bool absrefine_flag)
-  //   {     
-  //     //BVTypeCheck should have already checked the sanity of the input
-  //     //FOR-formula
-  //     ASTNode parameter     = finiteloop[0];
-  //     int paramInit         = GetUnsignedConst(finiteloop[1]);
-  //     int paramLimit        = GetUnsignedConst(finiteloop[2]);
-  //     int paramIncrement    = GetUnsignedConst(finiteloop[3]);
-  //     ASTNode exceptFormula = finiteloop[4];
-  //     ASTNode formulabody   = finiteloop[5];
-  //     int paramCurrentValue = paramInit;
-  //     int width             = finiteloop[1].GetValueWidth();
-
-  //     //Update ParamToCurrentValMap with parameter and its current
-  //     //value. Here paramCurrentValue is the initial value    
-  //     ASTNode value =       
-  //       bm->CreateBVConst(width,paramCurrentValue);
-  //     ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-    
-  //     //Go recursively thru' all the FOR-constructs.
-  //     if(FOR == formulabody.GetKind()) 
-  //       { 
-  //    ASTVec retvec;
-  //    ASTVec retvec_innerfor;
-  //    retvec.push_back(ASTTrue);
-  //         while(paramCurrentValue < paramLimit) 
-  //           {
-  //             retvec_innerfor = 
-  //          SATBased_FiniteLoop_Refinement(SatSolver, 
-  //                                         original_input,
-  //                                         formulabody, 
-  //                                         ParamToCurrentValMap,
-  //                                         absrefine_flag);
-
-  //        for(ASTVec::iterator i=retvec_innerfor.begin(),
-  //              iend=retvec_innerfor.end();i!=iend;i++)
-  //          {
-  //            retvec.push_back(*i);
-  //          }
-
-  //             //Update ParamToCurrentValMap with parameter and its
-  //             //current value.
-  //             paramCurrentValue = paramCurrentValue + paramIncrement;
-  //        value = bm->CreateTerm(BVPLUS, 
-  //                           width, 
-  //                           (*ParamToCurrentValMap)[parameter],
-  //                           bm->CreateOneConst(width));      
-  //        ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-  //           } //end of While
-
-  //    return retvec;
-  //       } //end of recursion FORs
-
-  //     //Expand the leaf level FOR-construct completely
-  //     //increment of paramCurrentValue done inside loop
-  //     int ThisForLoopAllTrue = 0;
-  //     ASTVec ForloopVec;
-  //     ForloopVec.push_back(ASTTrue);
-  //     for(;paramCurrentValue < paramLimit;) 
-  //       {
-  //         ASTNode currentFormula;
-  //    ASTNode currentExceptFormula = exceptFormula;
-  //    currentExceptFormula = 
-  //      SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
-  //    if(ASTTrue ==  currentExceptFormula)
-  //      {         
-  //        currentFormula = ASTTrue;
-  //      }
-  //    else 
-  //      {
-  //        currentFormula =
-  //          SimplifyFormula(formulabody, false, ParamToCurrentValMap);
-  //      }
-
-  //         //Check the currentformula against the model, and add it to the
-  //         //SAT solver if it is false against the model
-  //         if(absrefine_flag 
-  //       && 
-  //       ASTFalse == ComputeFormulaUsingModel(currentFormula)
-  //       ) 
-  //      {
-  //        ForloopVec.push_back(currentFormula);
-  //           }
-  //    else 
-  //      {
-  //        if(ASTTrue != currentFormula)
-  //          {
-  //            ForloopVec.push_back(currentFormula);
-  //          }
-  //        if(ASTFalse == currentFormula)
-  //          {
-  //            ForloopVec.push_back(ASTFalse);
-  //            return ForloopVec;
-  //          }
-  //      }
-        
-  //         //Update ParamToCurrentValMap with parameter and its current
-  //         //value.
-  //    paramCurrentValue = paramCurrentValue + paramIncrement;
-  //    value = bm->CreateTerm(BVPLUS, 
-  //                       width, 
-  //                       (*ParamToCurrentValMap)[parameter],
-  //                       bm->CreateOneConst(width));  
-  //    ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-  //       } //end of expanding the FOR loop
-    
-  //     return ForloopVec;
-  //   } //end of the SATBased_FiniteLoop_Refinement()
-
-  //   //SATBased_FiniteLoop_Refinement_UsingModel().  Expand the finite
-  //   //loop, check against model
-  //   ASTNode 
-  //   AbsRefine_CounterExample::
-  //   Check_FiniteLoop_UsingModel(const ASTNode& finiteloop,
-  //                                   ASTNodeMap* ParamToCurrentValMap,
-  //                                   bool checkusingmodel_flag = true)
-  //   {
-  //     /*
-  //      * 'finiteloop' is the finite loop to be expanded
-  //      * Every finiteloop has three parts:    
-  //      * 0) Parameter Name     
-  //      * 1) Parameter initialization     
-  //      * 2) Parameter limit value     
-  //      * 3) Increment formula     
-  //      * 4) Formula Body
-  //      *    
-  //      * ParamToCurrentValMap contains a map from parameters to their
-  //      * current values in the recursion
-  //      *   
-  //      * Nested FORs are allowed, but only the innermost loop can have a
-  //      * formula in it
-  //      */
-
-  //     //BVTypeCheck should have already checked the sanity of the input
-  //     //FOR-formula
-  //     ASTNode parameter     = finiteloop[0];
-  //     int paramInit         = GetUnsignedConst(finiteloop[1]);
-  //     int paramLimit        = GetUnsignedConst(finiteloop[2]);
-  //     int paramIncrement    = GetUnsignedConst(finiteloop[3]);
-  //     ASTNode exceptFormula = finiteloop[4];
-  //     ASTNode formulabody   = finiteloop[5];
-  //     int paramCurrentValue = paramInit;
-  //     int width             = finiteloop[1].GetValueWidth();
-
-  //     //Update ParamToCurrentValMap with parameter and its current
-  //     //value. Here paramCurrentValue is the initial value
-  //     ASTNode value =       
-  //       bm->CreateBVConst(width,paramCurrentValue);
-  //     ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-
-  //     ASTNode ret = ASTTrue;
-  //     ASTVec returnVec;
-  //     //Go recursively thru' all the FOR-constructs.
-  //     if(FOR == formulabody.GetKind()) 
-  //       { 
-  //         while(paramCurrentValue < paramLimit) 
-  //           {
-  //             ret = Check_FiniteLoop_UsingModel(formulabody,
-  //                                          ParamToCurrentValMap, 
-  //                                          checkusingmodel_flag);
-  //        if(ASTFalse == ret) 
-  //          {
-  //            //no more expansion needed. Return immediately
-  //            return ret;
-  //          }
-  //        else 
-  //          {
-  //            returnVec.push_back(ret);
-  //          }
-
-  //             //Update ParamToCurrentValMap with parameter and its
-  //             //current value.
-  //             paramCurrentValue = paramCurrentValue + paramIncrement;
-  //        value = bm->CreateTerm(BVPLUS, 
-  //                           width, 
-  //                           (*ParamToCurrentValMap)[parameter],
-  //                           bm->CreateOneConst(width));
-  //        ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-  //           } //end of While
-
-  //    ASTNode retFormula = 
-  //      (returnVec.size() > 1) ? 
-  //      bm->CreateNode(AND, returnVec) : 
-  //      (returnVec.size() == 1) ?
-  //      returnVec[0] :
-  //      ASTTrue;
-  //         return retFormula;      
-  //       }
-
-  //     ASTVec forloopFormulaVector;
-  //     //Expand the leaf level FOR-construct completely
-  //     //incrementing of paramCurrentValue is done inside loop
-  //     for(;paramCurrentValue < paramLimit;)
-  //       {
-  //    ASTNode currentFormula;
-
-  //    ASTNode currentExceptFormula = exceptFormula;
-  //    currentExceptFormula = 
-  //      SimplifyFormula(exceptFormula, false, ParamToCurrentValMap);
-  //    if(ASTTrue ==  currentExceptFormula)
-  //      {
-  //        currentFormula = ASTTrue;
-  //        //continue;
-  //      }
-  //    else 
-  //      {
-  //        currentFormula = 
-  //          SimplifyFormula(formulabody, false, ParamToCurrentValMap);
-  //      }
-
-  //         if(checkusingmodel_flag) 
-  //           {
-  //             //Check the currentformula against the model, and return
-  //             //immediately
-  //        //cout << "Printing current Formula: " << currentFormula << "\n"; 
-  //        ASTNode computedForm = ComputeFormulaUsingModel(currentFormula);
-  //        //cout << "Printing computed Formula: " << computedForm << "\n"; 
-  //             if(ASTFalse == computedForm)
-  //          {
-  //            return ASTFalse;
-  //          }
-  //           }
-  //         else 
-  //           {
-  //        if(ASTTrue != currentFormula)
-  //          {
-  //            forloopFormulaVector.push_back(currentFormula);
-  //          }
-  //           }
-        
-  //         //Update ParamToCurrentValMap with parameter and its current
-  //         //value         
-  //    paramCurrentValue = paramCurrentValue + paramIncrement;
-  //    value = bm->CreateTerm(BVPLUS, 
-  //                       width, 
-  //                       (*ParamToCurrentValMap)[parameter],
-  //                       bm->CreateOneConst(width));  
-  //    ReplaceOrAddToMap(ParamToCurrentValMap, parameter, value);
-  //       } //end of For
-
-  //     if(checkusingmodel_flag) 
-  //       {
-  //    return ASTTrue;
-  //       }
-  //     else 
-  //       {
-  //         ASTNode retFormula = 
-  //           (forloopFormulaVector.size() > 1) ? 
-  //      bm->CreateNode(AND, forloopFormulaVector) :
-  //      (forloopFormulaVector.size() == 1) ? 
-  //      forloopFormulaVector[0] :
-  //      ASTTrue;
-  //         return retFormula;
-  //       }
-  //   } //end of the Check_FiniteLoop_UsingModel()
-  
-
-  //   //Expand_FiniteLoop_For_ModelCheck
-  //   ASTNode 
-  //   AbsRefine_CounterExample::
-  //   Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) 
-  //   {
-  //     ASTNodeMap ParamToCurrentValMap;
-  //     return Check_FiniteLoop_UsingModel(finiteloop, 
-  //                                   &ParamToCurrentValMap, false);
-  //   } //end of Expand_FiniteLoop_TopLevel()  
-
-  //   ASTNode
-  //   AbsRefine_CounterExample::
-  //   Check_FiniteLoop_UsingModel(const ASTNode& finiteloop)
-  //   {
-  //     ASTNodeMap ParamToCurrentValMap;
-  //     return Check_FiniteLoop_UsingModel(finiteloop, 
-  //                                   &ParamToCurrentValMap, true);
-  //   } //end of Check_FiniteLoop_UsingModel  
 };// end of namespace BEEV

diff --git a/src/absrefine_counterexample/CounterExample.cpp b/src/absrefine_counterexample/CounterExample.cpp
index 6ca710fc23b7857b0ea8907baf8b38f04afb0650..b3d0889170eeb669f488619a9af3eaa490c7e778 100644 (file)
--- a/src/absrefine_counterexample/CounterExample.cpp
+++ b/src/absrefine_counterexample/CounterExample.cpp
@@ -15,9 +15,6 @@ const bool debug_counterexample =  false;
 
 namespace BEEV
 {
-
-
-
   /*FUNCTION: constructs counterexample from MINISAT counterexample
    * step1 : iterate through MINISAT counterexample and assemble the
    * bits for each AST term. Store it in a map from ASTNode to vector
@@ -141,36 +138,22 @@ namespace BEEV
   //4. doesn't have a value in the counterexample then return 0 as the
   //4. value of the arrayread.
   ASTNode
-  AbsRefine_CounterExample::TermToConstTermUsingModel(const ASTNode& t,
+  AbsRefine_CounterExample::TermToConstTermUsingModel(const ASTNode& term,
       bool ArrayReadFlag)
   {
-    bm->Begin_RemoveWrites = false;
-    bm->SimplifyWrites_InPlace_Flag = false;
-    //ASTNode term = SimplifyTerm(t);
-    ASTNode term = t;
-    Kind k = term.GetKind();
-
-    //cerr << "Input to TermToConstTermUsingModel: " << term << endl;
-    if (!is_Term_kind(k))
-      {
-        FatalError("TermToConstTermUsingModel: "
-          "The input is not a term: ", term);
-      }
-    if (k == WRITE)
-      {
-        FatalError("TermToConstTermUsingModel: "
-          "The input has wrong kind: WRITE : ", term);
-      }
-    if (k == SYMBOL && BOOLEAN_TYPE == term.GetType())
-      {
-        FatalError("TermToConstTermUsingModel: "
-          "The input has wrong kind: Propositional variable : ", term);
-      }
+    if (term.GetKind() == BVCONST)
+       return term;
 
-    ASTNodeMap::iterator it1;
+    const Kind k = term.GetKind();
+
+    assert (is_Term_kind(k));
+    assert (k != WRITE);
+    assert (BOOLEAN_TYPE != term.GetType());
+
+    ASTNodeMap::const_iterator it1;
     if ((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end())
       {
-        ASTNode val = it1->second;
+        const ASTNode& val = it1->second;
         if (BVCONST != val.GetKind())
           {
             //CounterExampleMap has two maps rolled into
@@ -336,19 +319,17 @@ namespace BEEV
         {
           const ASTVec& c = term.GetChildren();
           ASTVec o;
-                   o.reserve(c.size());
+          o.reserve(c.size());
         for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it
             != itend; it++)
             {
               ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag);
               o.push_back(ff);
             }
-          output = bm->CreateTerm(k, term.GetValueWidth(), o);
+          output = bm->hashingNodeFactory->CreateTerm(k, term.GetValueWidth(), o);
           //output is a CONST expression. compute its value and store it
           //in the CounterExampleMap
-          ASTNode oo = simp->BVConstEvaluator(output);
-          //the return value
-          output = oo;
+          output = simp->BVConstEvaluator(output);
           break;
         }
       }