From b10fab3e1e5b55e0da6a6fb9ed6158224807ce04 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 4 Sep 2009 18:11:36 +0000 Subject: [PATCH] Basic finite-FOR loop coded up. Testing/Debugging under way git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@185 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 32 +++-- src/AST/AbstractionRefinement.cpp | 215 ++++++++++++++++++++---------- src/AST/ToCNF.cpp | 3 +- src/AST/ToSAT.cpp | 8 +- src/sat/simp/depend.mk | 12 -- 5 files changed, 165 insertions(+), 105 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 2b2a586..8c51e89 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1232,20 +1232,24 @@ namespace BEEV SOLVER_RETURN_TYPE CallSAT_ResultCheck(MINISAT::Solver& newS, const ASTNode& modified_input, const ASTNode& original_input); - SOLVER_RETURN_TYPE SATBased_ArrayReadRefinement(MINISAT::Solver& newS, - const ASTNode& modified_input, - const ASTNode& original_input); - SOLVER_RETURN_TYPE SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, - const ASTNode& orig_input); - - SOLVER_RETURN_TYPE SATBased_FiniteLoop_Refinement(MINISAT::Solver& newS, - const ASTNode& orig_input); - void Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input, - const ASTNode& finiteloop,ASTNodeMap* ParamToCurrentValMap, - bool AbstractionRefinement=true); - ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, - ASTNodeMap* VarConstMap); - + SOLVER_RETURN_TYPE SATBased_ArrayReadRefinement(MINISAT::Solver& newS, + const ASTNode& modified_input, + const ASTNode& original_input); + SOLVER_RETURN_TYPE SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, + const ASTNode& orig_input); + SOLVER_RETURN_TYPE SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input, + const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap); + SOLVER_RETURN_TYPE SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, + const ASTNode& orig_input); + + ASTNode Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap, + bool CheckUsingModel_Or_Expand); + + ASTNode Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop); + //creates array write axiom only for the input term or formula, if //necessary. If there are no axioms to produce then it simply //generates TRUE diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index 51ae361..6622c76 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -17,6 +17,7 @@ namespace BEEV * Abstraction Refinement related functions ******************************************************************/ + //FIXME: Write a detailed comment on how this actually works SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, const ASTNode& inputAlreadyInSAT, const ASTNode& original_input) { @@ -137,6 +138,7 @@ namespace BEEV return CallSAT_ResultCheck(SatSolver, RemainingAxioms, original_input); } //end of SATBased_ArrayReadRefinement + //Creates Array Write Axioms ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, const ASTNode& newvar) { if (READ != term.GetKind() && WRITE != term[0].GetKind()) @@ -150,6 +152,7 @@ namespace BEEV return arraywrite_axiom; }//end of Create_ArrayWriteAxioms() + //FIXME: Write a detailed comment on how this actually works SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { @@ -207,11 +210,11 @@ namespace BEEV return SOLVER_UNDECIDED; } //end of SATBased_ArrayWriteRefinement - + //Expands all finite-for-loops using counterexample-guided //abstraction-refinement. - SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + SOLVER_RETURN_TYPE BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input) { /* * For each 'finiteloop' in the global list 'List_Of_FiniteLoops' @@ -230,24 +233,115 @@ namespace BEEV * if the 'done' flag is true, then we terminate this refinement * loop. */ - } - - void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input, - const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap, - bool AbstractionRefinement) { + } //end of SATBased_AllFiniteLoops_Refinement() + + //SATBased_FiniteLoop_Refinement + // + //Expand the finite loop, check against model, and add false + //formulas to the SAT solver + SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input, + const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap) + { /* * '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 formulabody = finiteloop[4]; + int paramCurrentValue = paramInit; + + //Update ParamToCurrentValMap with parameter and its current + //value. Here paramCurrentValue is the initial value + unsigned width = 32; + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + + //Go recursively thru' all the FOR-constructs. + if(FOR == formulabody.GetKind()) + { + while(paramCurrentValue < paramLimit) + { + SATBased_FiniteLoop_Refinement(SatSolver, original_input, + formulabody, ParamToCurrentValMap); + paramCurrentValue = paramCurrentValue + paramIncrement; + + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } //end of While + } + + ASTVec forloopFormulaVector; + //Expand the leaf level FOR-construct completely + for(; + paramCurrentValue < paramLimit; + paramCurrentValue = paramCurrentValue + paramIncrement) + { + ASTNode currentFormula; + currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); + + //Check the currentformula against the model, and add it to the + //SAT solver if it is false against the model + if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) { + forloopFormulaVector.push_back(currentFormula); + ASTNode forloopFormulas = + (forloopFormulaVector.size() != 1) ? + CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + + SOLVER_RETURN_TYPE result = + CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); + if(result != SOLVER_UNDECIDED) + { + return result; + } + } + + //Update ParamToCurrentValMap with parameter and its current + //value + // + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } + return SOLVER_UNDECIDED; + } //end of the SATBased_FiniteLoop_Refinement() + + //SATBased_FiniteLoop_Refinement_UsingModel + // + //Expand the finite loop, check against model, and add false + //formulas to the SAT solver + ASTNode BeevMgr::Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap, + bool CheckUsingModel_Or_Expand = 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 @@ -255,34 +349,6 @@ namespace BEEV * * Nested FORs are allowed, but only the innermost loop can have a * formula in it - * - * STEPS: - * - * 0. Populate the top of the parameter stack with 'finiteloop' - * parameter initial, limit and increment values - * - * 1. If formulabody in 'finiteloop' is another for loop, then - * recurse - * - * 2. Else if current parameter value is less than limit value then - * - * Instantiate a singleformula - * - * Check if the formula is true in the current model - * - * If true, discard it - * - * If false, add it to the SAT solver to get a new model. Make - * sure to update array index tables to facilitate array - * read refinement later. - * - * 3. If control reaches here, it means one of the following - * possibilities (We have instantiated all relevant formulas by - * now): - * - * 3.1: We have UNSAT. Return UNSAT - * - * 3.2: We have SAT, and it is indeed a satisfying model */ //BVTypeCheck should have already checked the sanity of the input @@ -304,8 +370,8 @@ namespace BEEV { while(paramCurrentValue < paramLimit) { - Expand_FiniteLoop(SatSolver, original_input, - formulabody, ParamToCurrentValMap); + Check_FiniteLoop_UsingModel(formulabody, + ParamToCurrentValMap, CheckUsingModel_Or_Expand); paramCurrentValue = paramCurrentValue + paramIncrement; //Update ParamToCurrentValMap with parameter and its current @@ -323,46 +389,47 @@ namespace BEEV paramCurrentValue < paramLimit; paramCurrentValue = paramCurrentValue + paramIncrement) { - ASTNode currentFormula = - FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap); + ASTNode currentFormula; + currentFormula = SimplifyFormula(formulabody, ParamToCurrentValMap); - if(AbstractionRefinement) + if(CheckUsingModel_Or_Expand) { - int result = 0; //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) { - forloopFormulaVector.push_back(currentFormula); - } - - //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' - (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); - } //end of if + if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) + return ASTFalse; + } else { forloopFormulaVector.push_back(currentFormula); } - } //end of for - - ASTNode forloopFormulas = - (forloopFormulaVector.size() != 1) ? - CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; - - //result = CallSAT_ResultCheck(SatSolver, forloopFormulas, original_input); - } //end of the Expand_FiniteLoop() + + //Update ParamToCurrentValMap with parameter and its current + //value + //FIXME: Possible leak since I am not freeing the previous + //'value' for the same 'key' + (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); + } - ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody, - ASTNodeMap* VarToConstantMap) + + if(CheckUsingModel_Or_Expand) + { + ASTNode retFormula = + (forloopFormulaVector.size() != 1) ? CreateNode(AND, forloopFormulaVector) : forloopFormulaVector[0]; + return retFormula; + } + else + { + return ASTTrue; + } + } //end of the Check_FiniteLoop_UsingModel() + + + //Expand_FiniteLoop_For_ModelCheck + ASTNode BeevMgr::Expand_FiniteLoop_TopLevel(const ASTNode& finiteloop) { - /* - * Takes a formula 'formulabody', and simplifies it against - * variable-to-constant map 'VarToConstantMap' - */ - return SimplifyFormula(formulabody, VarToConstantMap); - } //end of FiniteLoop_Extract_SingleFormula() + ASTNodeMap ParamToCurrentValMap; + return Check_FiniteLoop_UsingModel(finiteloop, &ParamToCurrentValMap, false); + } //end of Expand_FiniteLoop_TopLevel() };// end of namespace BEEV diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index 816ff0a..28d3440 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1846,5 +1846,4 @@ namespace BEEV } } //end of CALLSAT_ResultCheck - -} // end namespace +} // end namespace BEEV diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index 2931bb0..03fbeef 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -18,7 +18,7 @@ namespace BEEV * lookup or create new MINISAT Vars from the global MAP * _ASTNode_to_SATVar. */ - /**const**/ MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) + MINISAT::Var BeevMgr::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) { ASTtoSATMap::iterator it; MINISAT::Var v; @@ -46,8 +46,10 @@ namespace BEEV * calls solve(). If solve returns unsat, then stop and return * unsat. else continue. */ - // FIXME: Still need to deal with TRUE/FALSE in clauses! - //bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll, ASTNodeToIntMap& heuristic) + // FIXME: Still need to deal with TRUE/FALSE in clauses! + // + //bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, + //BeevMgr::ClauseList& cll, ASTNodeToIntMap& heuristic) bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) { CountersAndStats("SAT Solver"); diff --git a/src/sat/simp/depend.mk b/src/sat/simp/depend.mk index cd452e0..1323fd9 100644 --- a/src/sat/simp/depend.mk +++ b/src/sat/simp/depend.mk @@ -1,24 +1,12 @@ -Main.o: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ - ../core/SolverTypes.h SimpSolver.o: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ ../mtl/Alg.h ../core/SolverTypes.h -Main.op: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ - ../core/SolverTypes.h SimpSolver.op: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ ../mtl/Alg.h ../core/SolverTypes.h -Main.od: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ - ../core/SolverTypes.h SimpSolver.od: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ ../mtl/Alg.h ../core/SolverTypes.h -Main.or: Main.C SimpSolver.h ../mtl/Queue.h ../mtl/Vec.h ../core/Solver.h \ - ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h ../mtl/Alg.h \ - ../core/SolverTypes.h SimpSolver.or: SimpSolver.C ../mtl/Sort.h ../mtl/Vec.h SimpSolver.h \ ../mtl/Queue.h ../core/Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \ ../mtl/Alg.h ../core/SolverTypes.h -- 2.47.3