From 9c38f4b06fdf86b07d8545575b5f12c8419aa69f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 2 Jan 2011 12:03:38 +0000 Subject: [PATCH] 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 --- .../AbsRefine_CounterExample.h | 29 +- .../AbstractionRefinement.cpp | 412 ------------------ .../CounterExample.cpp | 47 +- 3 files changed, 18 insertions(+), 470 deletions(-) diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index a1a8f8f..efd2e91 100644 --- 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 ce31f60..9fda21d 100644 --- 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 6ca710f..b3d0889 100644 --- 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; } } -- 2.47.3