From: vijay_ganesh Date: Wed, 18 Nov 2009 20:20:19 +0000 (+0000) Subject: userguided abstraction-refinement is now at the toplevel X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=30d5844172260df323d01129bd170f66f6bfb3a8;p=francis%2Fstp.git userguided abstraction-refinement is now at the toplevel git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@412 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 9f3c730..a6a4265 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -11,13 +11,51 @@ namespace BEEV { + // The absolute TopLevel function that invokes STP on the input + // formula + SOLVER_RETURN_TYPE STP::TopLevelSTP(const ASTNode& inputasserts, + const ASTNode& query) + { + ASTNode original_input = bm->CreateNode(AND, + inputasserts, + bm->CreateNode(NOT, query)); + ASTNode modified_input = original_input; + + //solver instantiated here +#ifdef CORE + MINISAT::Solver NewSolver; +#endif +#ifdef CRYPTOMINISAT + MINISAT::Solver NewSolver; +#endif +#ifdef SIMP + MINISAT::SimpSolver NewSolver; +#endif +#ifdef UNSOUND + MINISAT::UnsoundSimpSolver NewSolver; +#endif + + if(bm->UserFlags.num_absrefine_flag) + { + return UserGuided_AbsRefine(NewSolver, + original_input); + } + else + { + return TopLevelSTPAux(NewSolver, + modified_input, original_input); + } + } //End of TopLevelSTP() + //Acceps a query, calls the SAT solver and generates Valid/InValid. //if returned 0 then input is INVALID if returned 1 then input is //VALID if returned 2 then UNDECIDED - SOLVER_RETURN_TYPE STP::TopLevelSTPAux(const ASTNode& inputasserts_and_query) + SOLVER_RETURN_TYPE STP::TopLevelSTPAux(MINISAT::Solver& NewSolver, + const ASTNode& modified_input, + const ASTNode& original_input) { - ASTNode inputToSAT = inputasserts_and_query; - ASTNode orig_input = inputToSAT; + ASTNode inputToSAT = modified_input; + ASTNode orig_input = original_input; bm->ASTNodeStats("input asserts and query: ", inputToSAT); ASTNode simplified_solved_InputToSAT = inputToSAT; @@ -127,37 +165,13 @@ namespace BEEV { bm->TermsAlreadySeenMap_Clear(); SOLVER_RETURN_TYPE res; - - //solver instantiated here -#ifdef CORE - MINISAT::Solver newS; -#endif -#ifdef CRYPTOMINISAT - MINISAT::Solver newS; -#endif -#ifdef SIMP - MINISAT::SimpSolver newS; -#endif -#ifdef UNSOUND - MINISAT::UnsoundSimpSolver newS; -#endif - - if(bm->UserFlags.num_absrefine_flag - && !bm->UserFlags.arrayread_refinement_flag) - { - res = - Ctr_Example->UserGuided_AbsRefine(newS, - orig_input); - return res; - } - if (bm->UserFlags.arrayread_refinement_flag) { bm->counterexample_checking_during_refinement = true; } res = - Ctr_Example->CallSAT_ResultCheck(newS, + Ctr_Example->CallSAT_ResultCheck(NewSolver, simplified_solved_InputToSAT, orig_input); if (SOLVER_UNDECIDED != res) @@ -166,7 +180,7 @@ namespace BEEV { return res; } - // res = SATBased_AllFiniteLoops_Refinement(newS, orig_input); + // res = SATBased_AllFiniteLoops_Refinement(NewSolver, orig_input); // if (SOLVER_UNDECIDED != res) // { // CountersAndStats("print_func_stats"); @@ -174,7 +188,7 @@ namespace BEEV { // } res = - Ctr_Example->SATBased_ArrayReadRefinement(newS, + Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, orig_input); if (SOLVER_UNDECIDED != res) @@ -184,7 +198,7 @@ namespace BEEV { } res = - Ctr_Example->SATBased_ArrayWriteRefinement(newS, orig_input); + Ctr_Example->SATBased_ArrayWriteRefinement(NewSolver, orig_input); if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats", bm); @@ -192,7 +206,7 @@ namespace BEEV { } res = - Ctr_Example->SATBased_ArrayReadRefinement(newS, + Ctr_Example->SATBased_ArrayReadRefinement(NewSolver, simplified_solved_InputToSAT, orig_input); if (SOLVER_UNDECIDED != res) @@ -206,4 +220,73 @@ namespace BEEV { //bogus return to make the compiler shut up return SOLVER_ERROR; } //End of TopLevelSTPAux + + //UserGuided abstraction refinement + SOLVER_RETURN_TYPE + STP:: + UserGuided_AbsRefine(MINISAT::Solver& NewSolver, + const ASTNode& original_input) + { + ASTVec v = bm->GetAsserts_WithKey(0); + if(v.empty()) + { + FatalError("UserGuided_AbsRefine: Something is seriously wrong."\ + "The input set is empty"); + } + ASTNode sureAddInput = + (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); + + SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; + res = TopLevelSTPAux(NewSolver, sureAddInput, original_input); + if(SOLVER_UNDECIDED != res) + { + return res; + } + + //Do refinement here + if(AND != original_input.GetKind()) + { + FatalError("UserGuided_AbsRefine: The input must be an AND"); + } + + ASTVec RefineFormulasVec; + ASTVec RemainingFormulasVec; + ASTNode asttrue = bm->CreateNode(TRUE); + ASTNode astfalse = bm->CreateNode(FALSE); + for(int count=0; count < bm->UserFlags.num_absrefine; count++) + { + RemainingFormulasVec.clear(); + RemainingFormulasVec.push_back(asttrue); + RefineFormulasVec.clear(); + RefineFormulasVec.push_back(asttrue); + ASTVec InputKids = original_input.GetChildren(); + for(ASTVec::iterator it = InputKids.begin(), itend = InputKids.end(); + it!=itend;it++) + { + Ctr_Example->ClearComputeFormulaMap(); + if(astfalse == Ctr_Example->ComputeFormulaUsingModel(*it)) + { + RefineFormulasVec.push_back(*it); + } + else + { + RemainingFormulasVec.push_back(*it); + } + } + ASTNode RefineFormulas = + (RefineFormulasVec.size() == 1) ? + RefineFormulasVec[0] : bm->CreateNode(AND, RefineFormulasVec); + res = TopLevelSTPAux(NewSolver, RefineFormulas, original_input); + if(SOLVER_UNDECIDED != res) + { + return res; + } + } + + ASTNode RemainingFormulas = + (RemainingFormulasVec.size() == 1) ? + RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec); + res = TopLevelSTPAux(NewSolver, RemainingFormulas, original_input); + return res; + } //End of UserGuided_AbsRefine() }; //end of namespace diff --git a/src/STPManager/STP.h b/src/STPManager/STP.h index ee051b3..8e1f519 100644 --- a/src/STPManager/STP.h +++ b/src/STPManager/STP.h @@ -77,22 +77,20 @@ namespace BEEV // The absolute TopLevel function that invokes STP on the input // formula SOLVER_RETURN_TYPE TopLevelSTP(const ASTNode& inputasserts, - const ASTNode& query) - { - ASTNode q = bm->CreateNode(AND, - inputasserts, - bm->CreateNode(NOT, query)); - return TopLevelSTPAux(q); - } //End of TopLevelSTP() + const ASTNode& query); // Accepts query and returns the answer. if query is valid, // returns VALID, else returns INVALID. Automatically constructs // counterexample for invalid queries, and prints them upon - // request. - SOLVER_RETURN_TYPE TopLevelSTPAux(const ASTNode& inputasserts_and_query); + // request. + SOLVER_RETURN_TYPE TopLevelSTPAux(MINISAT::Solver& NewSolver, + const ASTNode& modified_input, + const ASTNode& original_input); - //void ClearAllCaches(void); - + SOLVER_RETURN_TYPE + UserGuided_AbsRefine(MINISAT::Solver& SatSolver, + const ASTNode& original_input); + void ClearAllTables(void) { simp->ClearAllTables(); diff --git a/src/absrefine_counterexample/AbsRefine_CounterExample.h b/src/absrefine_counterexample/AbsRefine_CounterExample.h index 53ab852..a858a28 100644 --- a/src/absrefine_counterexample/AbsRefine_CounterExample.h +++ b/src/absrefine_counterexample/AbsRefine_CounterExample.h @@ -154,11 +154,6 @@ namespace BEEV SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); - SOLVER_RETURN_TYPE - UserGuided_AbsRefine(MINISAT::Solver& SatSolver, - const ASTNode& original_input); - - // SOLVER_RETURN_TYPE // SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& newS, // const ASTNode& orig_input); diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp index bea6ec6..f922a9b 100644 --- a/src/absrefine_counterexample/AbstractionRefinement.cpp +++ b/src/absrefine_counterexample/AbstractionRefinement.cpp @@ -259,74 +259,6 @@ namespace BEEV return arraywrite_axiom; }//end of Create_ArrayWriteAxioms() - //UserGuided abstraction refinement - SOLVER_RETURN_TYPE - AbsRefine_CounterExample:: - UserGuided_AbsRefine(MINISAT::Solver& SatSolver, - //const ASTNode& modified_input, - const ASTNode& original_input) - { - ASTVec v = bm->GetAsserts_WithKey(0); - if(v.empty()) - { - FatalError("UserGuided_AbsRefine: Something is seriously wrong."\ - "The input set is empty"); - } - ASTNode sureAddInput = - (v.size() == 1) ? v[0] : bm->CreateNode(AND, v); - - SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; - res = CallSAT_ResultCheck(SatSolver, sureAddInput, original_input); - if(SOLVER_UNDECIDED != res) - { - return res; - } - - //Do refinement here - if(AND != original_input.GetKind()) - { - FatalError("UserGuided_AbsRefine: The input must be an AND"); - } - - ASTVec RefineFormulasVec; - ASTVec RemainingFormulasVec; - for(int count=0; count < bm->UserFlags.num_absrefine; count++) - { - RemainingFormulasVec.clear(); - RemainingFormulasVec.push_back(ASTTrue); - RefineFormulasVec.clear(); - RefineFormulasVec.push_back(ASTTrue); - ASTVec InputKids = original_input.GetChildren(); - for(ASTVec::iterator it = InputKids.begin(), itend = InputKids.end(); - it!=itend;it++) - { - ClearComputeFormulaMap(); - if(ASTFalse == ComputeFormulaUsingModel(*it)) - { - RefineFormulasVec.push_back(*it); - } - else - { - RemainingFormulasVec.push_back(*it); - } - } - ASTNode RefineFormulas = - (RefineFormulasVec.size() == 1) ? - RefineFormulasVec[0] : bm->CreateNode(AND, RefineFormulasVec); - res = CallSAT_ResultCheck(SatSolver, RefineFormulas, original_input); - if(SOLVER_UNDECIDED != res) - { - return res; - } - } - - ASTNode RemainingFormulas = - (RemainingFormulasVec.size() == 1) ? - RemainingFormulasVec[0] : bm->CreateNode(AND, RemainingFormulasVec); - res = CallSAT_ResultCheck(SatSolver, RemainingFormulas, original_input); - return res; - } //End of UserGuided_AbsRefine() - // static void ReplaceOrAddToMap(ASTNodeMap * VarToConstMap, // const ASTNode& key, const ASTNode& value) // {