From: vijay_ganesh Date: Mon, 7 Sep 2009 01:33:04 +0000 (+0000) Subject: coded up abstraction-refinement X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9f5003368127eb1e1f627b4c538b96af006b5b53;p=francis%2Fstp.git coded up abstraction-refinement git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@201 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.h b/src/AST/AST.h index cfad329..110bdcc 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1234,7 +1234,6 @@ namespace BEEV 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 @@ -1251,6 +1250,11 @@ namespace BEEV bool Begin_RemoveWrites; bool SimplifyWrites_InPlace_Flag; + //For finiteloop construct + // + //A list of all finiteloop constructs in the input formula + ASTVec GlobalList_Of_FiniteLoops; + void CopySolverMap_To_CounterExample(void); //int LinearSearch(const ASTNode& orig_input); //Datastructures and functions needed for counterexample @@ -1354,8 +1358,6 @@ namespace BEEV // but it accesses private elements. Move it later. ASTNode TransformFormula_TopLevel(const ASTNode& form); ASTNode TransformArray(const ASTNode& term); - ASTNode TransformFiniteFor(const ASTNode& form); - //LET Management private: @@ -1434,10 +1436,6 @@ namespace BEEV //terms ASTNodeMap NewName_ReadOverWrite_Map; - //For finiteloop construct - // - //A list of all finiteloop constructs in the input formula - ASTVec List_Of_FiniteLoops; public: //print the STP solver output void PrintOutput(bool true_iff_valid); @@ -1604,7 +1602,7 @@ namespace BEEV //destructor ~BeevMgr(); - }; //End of Class BeevMgr + };//End of Class BeevMgr class CompleteCounterExample diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index df86ac4..dae4a17 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -13,31 +13,31 @@ namespace BEEV { + /****************************************************************** * Abstraction Refinement related functions ******************************************************************/ - //FIXME: Write a detailed comment on how this actually works + /****************************************************************** + * ARRAY READ ABSTRACTION REFINEMENT + * + * What it really does is, for each array, loop over each index i. + * inside that loop, it finds all the true and false axioms with i + * as first index. When it's got them all, it adds the false axioms + * to the formula and re-solves, and returns if the result is + * correct. Otherwise, it goes on to the next index. + * + * If it gets through all the indices without a correct result + * (which I think is impossible), it then solves with all the true + * axioms, too. + * + * This is not the most obvious way to do it, and I don't know how + * it compares with other approaches (e.g., one false axiom at a + * time or all the false axioms each time). + *****************************************************************/ SOLVER_RETURN_TYPE 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 - //go away. if yes, return the correct answer. if no, continue adding - //Leibnitz axioms systematically. - // FIXME: What it really does is, for each array, loop over each index i. - // inside that loop, it finds all the true and false axioms with i as first - // index. When it's got them all, it adds the false axioms to the formula - // and re-solves, and returns if the result is correct. Otherwise, it - // goes on to the next index. - // If it gets through all the indices without a correct result (which I think - // is impossible, but this is pretty confusing), it then solves with all - // the true axioms, too. - // This is not the most obvious way to do it, and I don't know how it - // compares with other approaches (e.g., one false axiom at a time or - // all the false axioms each time). - //printf("doing array read refinement\n"); if (!arrayread_refinement_flag) FatalError("SATBased_ArrayReadRefinement: Control should not reach here"); @@ -138,21 +138,12 @@ 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()) - { - FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE", term); - } - - ASTNode lhs = newvar; - ASTNode rhs = term; - ASTNode arraywrite_axiom = CreateSimplifiedEQ(lhs, rhs); - return arraywrite_axiom; - }//end of Create_ArrayWriteAxioms() - //FIXME: Write a detailed comment on how this actually works + /****************************************************************** + * ARRAY WRITE ABSTRACTION REFINEMENT + * + * FIXME: Write Detailed Comment + *****************************************************************/ SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { @@ -211,30 +202,78 @@ namespace BEEV return SOLVER_UNDECIDED; } //end of SATBased_ArrayWriteRefinement - //Expands all finite-for-loops using counterexample-guided - //abstraction-refinement. + //Creates Array Write Axioms + ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, + const ASTNode& newvar) + { + if (READ != term.GetKind() && WRITE != term[0].GetKind()) + { + FatalError("Create_ArrayWriteAxioms: Input must be a READ over a WRITE", term); + } + + ASTNode lhs = newvar; + ASTNode rhs = term; + ASTNode arraywrite_axiom = CreateSimplifiedEQ(lhs, rhs); + return arraywrite_axiom; + }//end of Create_ArrayWriteAxioms() + + + /****************************************************************** + * 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 BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { - /* - * For each 'finiteloop' in the global list 'List_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. - */ + for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),iend=GlobalList_Of_FiniteLoops.end(); + i!=iend;i++) + { + ASTNodeMap ParamToCurrentValMap; + SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + *i,&ParamToCurrentValMap); + if(SOLVER_UNDECIDED != ret) + { + return ret; + } + } + return SOLVER_UNDECIDED; } //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 @@ -243,23 +282,7 @@ namespace BEEV 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]; diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp index 89646e1..0939781 100644 --- a/src/AST/Transform.cpp +++ b/src/AST/Transform.cpp @@ -15,7 +15,6 @@ * formula. Arrays are replaced by equivalent bit-vector variables */ - #include "AST.h" #include #include @@ -174,8 +173,13 @@ namespace BEEV { assertTransformPostConditions(*it); } - } + }//End of assertTransformPostConditions() + /******************************************************** + * TransformFormula() + * + * Get rid of DIV/MODs, ARRAY read/writes, FOR constructs + ********************************************************/ ASTNode TransformFormula(const ASTNode& form) { BeevMgr& bm = form.GetBeevMgr(); @@ -254,6 +258,10 @@ namespace BEEV break; } case FOR: + //Insert in a global list of FOR constructs. Return TRUE now + bm.GlobalList_Of_FiniteLoops.push_back(simpleForm); + return bm.CreateNode(TRUE); + break; default: if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType()) result = simpleForm; @@ -618,10 +626,4 @@ namespace BEEV (*TransformMap)[term] = result; return result; } //end of TransformArray() - - ASTNode BeevMgr::TransformFiniteFor(const ASTNode& form) - { - return form; - } - } //end of namespace BEEV diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp index 8bb7598..2044c16 100644 --- a/src/AST/printer/PLPrinter.cpp +++ b/src/AST/printer/PLPrinter.cpp @@ -180,8 +180,10 @@ namespace printer PL_Print1(os, c[1], indentation, letize); os << ";"; PL_Print1(os, c[2], indentation, letize); - os << "){ \n"; + os << ";"; PL_Print1(os, c[3], indentation, letize); + os << "){ \n"; + PL_Print1(os, c[4], indentation, letize); os << "} \n"; break; case BVLT: