From: vijay_ganesh Date: Thu, 3 Sep 2009 22:17:47 +0000 (+0000) Subject: more cleanup X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3d419b9e71219bdf04f202aa39f768d488d11387;p=francis%2Fstp.git 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 cec92f9..0bbcb77 100644 --- 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 63f2dff..9b860fa 100644 --- 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 1055068..3ceb73c 100644 --- 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 cd9dbda..f716c6a 100644 --- 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");