From bd9e8c41d621ecff6d0cf3b34c894dd9cc1fcd8d Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Thu, 3 Sep 2009 23:47:32 +0000 Subject: [PATCH] added enum for Solver returntype git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@179 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 25 +++++--- src/AST/AbstractionRefinement.cpp | 90 +++++++++++++++------------- src/AST/ToCNF.cpp | 36 ++++++----- src/AST/ToSAT.cpp | 23 +++---- src/AST/printer/AssortedPrinters.cpp | 6 +- 5 files changed, 102 insertions(+), 78 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 0bbcb77..e7d84f9 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -64,6 +64,12 @@ namespace BEEV BOOLEAN_TYPE = 0, BITVECTOR_TYPE, ARRAY_TYPE, UNKNOWN_TYPE }; + enum SOLVER_RETURN_TYPE + { + SOLVER_INVALID=0, SOLVER_VALID=1, SOLVER_UNDECIDED=2, SOLVER_ERROR=-100 + }; + + class BeevMgr; class ASTNode; class ASTInternal; @@ -1218,15 +1224,20 @@ 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 SATBased_ArrayWriteRefinement(MINISAT::Solver& newS, const ASTNode& orig_input); + 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); - int SATBased_FiniteLoop_Refinement(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); + const ASTNode& finiteloop,ASTNodeMap* ParamToCurrentValMap, + bool AbstractionRefinement=true); ASTNode FiniteLoop_Extract_SingleFormula(const ASTNode& finiteloop_formulabody, ASTNodeMap* VarConstMap); diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp index 9b860fa..51ae361 100644 --- a/src/AST/AbstractionRefinement.cpp +++ b/src/AST/AbstractionRefinement.cpp @@ -17,9 +17,9 @@ namespace BEEV * Abstraction Refinement related functions ******************************************************************/ - int BeevMgr::SATBased_ArrayReadRefinement(MINISAT::Solver& SatSolver, - const ASTNode& inputAlreadyInSAT, - const ASTNode& original_input) { + 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 @@ -116,7 +116,7 @@ namespace BEEV CreateNode(AND, FalseAxiomsVec) : FalseAxiomsVec[0]; ASTNodeStats("adding false readaxioms to SAT: ", FalseAxioms); //printf("spot 01\n"); - int res2 = 2; + SOLVER_RETURN_TYPE res2 = SOLVER_UNDECIDED; //if (FalseAxiomsVec.size() > 0) if (FalseAxiomsVec.size() > oldFalseAxiomsSize) { @@ -124,7 +124,7 @@ namespace BEEV oldFalseAxiomsSize = FalseAxiomsVec.size(); } //printf("spot 02, res2 = %d\n", res2); - if (2 != res2) + if (SOLVER_UNDECIDED != res2) { return res2; } @@ -150,7 +150,8 @@ namespace BEEV return arraywrite_axiom; }//end of Create_ArrayWriteAxioms() - int BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) + SOLVER_RETURN_TYPE BeevMgr::SATBased_ArrayWriteRefinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input) { ASTNode writeAxiom; ASTNodeMap::iterator it = ReadOverWrite_NewName_Map.begin(); @@ -183,13 +184,13 @@ namespace BEEV (FalseAxioms.size() != 1) ? CreateNode(AND, FalseAxioms) : FalseAxioms[0]; ASTNodeStats("adding false writeaxiom to SAT: ", writeAxiom); - int res2 = 2; + SOLVER_RETURN_TYPE res2 = SOLVER_UNDECIDED; if (FalseAxioms.size() > oldFalseAxiomsSize) { res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input); oldFalseAxiomsSize = FalseAxioms.size(); } - if (2 != res2) + if (SOLVER_UNDECIDED != res2) { return res2; } @@ -199,18 +200,18 @@ namespace BEEV CreateNode(AND, RemainingAxioms) : RemainingAxioms[0]; ASTNodeStats("adding remaining writeaxiom to SAT: ", writeAxiom); res2 = CallSAT_ResultCheck(SatSolver, writeAxiom, original_input); - if (2 != res2) + if (SOLVER_UNDECIDED != res2) { return res2; } - return 2; + return SOLVER_UNDECIDED; } //end of SATBased_ArrayWriteRefinement //Expands all finite-for-loops using counterexample-guided //abstraction-refinement. - int BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, - const ASTNode& original_input) + SOLVER_RETURN_TYPE BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input) { /* * For each 'finiteloop' in the global list 'List_Of_FiniteLoops' @@ -231,10 +232,9 @@ namespace BEEV */ } - void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver, - const ASTNode& original_input, - const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap) { + void BeevMgr::Expand_FiniteLoop(MINISAT::Solver& SatSolver, const ASTNode& original_input, + const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap, + bool AbstractionRefinement) { /* * 'finiteloop' is the finite loop to be expanded * @@ -316,33 +316,43 @@ namespace BEEV (*ParamToCurrentValMap)[parameter] = CreateBVConst(32,paramCurrentValue); } //end of While } - else + + ASTVec forloopFormulaVector; + //Expand the leaf level FOR-construct completely + for(; + paramCurrentValue < paramLimit; + paramCurrentValue = paramCurrentValue + paramIncrement) { - //Expand the leaf level FOR-construct completely - for(; - paramCurrentValue < paramLimit; - paramCurrentValue = paramCurrentValue + paramIncrement) - { ASTNode currentFormula = FiniteLoop_Extract_SingleFormula(formulabody, ParamToCurrentValMap); - - //Check the currentformula against the model, and add it to the - //SAT solver if it is false against the model - ASTNode formulaInModel = ComputeFormulaUsingModel(currentFormula); - - int result = 0; - if(ASTFalse == formulaInModel) { - result = CallSAT_ResultCheck(SatSolver, currentFormula, original_input); - } - - //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 else + + if(AbstractionRefinement) + { + 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 + 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() ASTNode BeevMgr::FiniteLoop_Extract_SingleFormula(const ASTNode& formulabody, diff --git a/src/AST/ToCNF.cpp b/src/AST/ToCNF.cpp index 3ceb73c..dc90b51 100644 --- a/src/AST/ToCNF.cpp +++ b/src/AST/ToCNF.cpp @@ -1777,37 +1777,42 @@ namespace BEEV delete cllp; } - int BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& newS, - const ASTNode& q, const ASTNode& orig_input) + //Call the SAT solver, and check the result before returning. This + //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED + SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, + const ASTNode& modified_input, + const ASTNode& original_input) { - ASTNode BBFormula = BBForm(q); + ASTNode BBFormula = BBForm(modified_input); CNFMgr* cm = new CNFMgr(this); ClauseList* cl = cm->convertToCNF(BBFormula); if (stats_flag) + { cerr << "Number of clauses:" << cl->size() << endl; + } //PrintClauseList(cout, *cl); - bool sat = toSATandSolve(newS, *cl); + bool sat = toSATandSolve(SatSolver, *cl); cm->DELETE(cl); delete cm; if (!sat) { PrintOutput(true); - return 1; + return SOLVER_VALID; } - else if (newS.okay()) + else if (SatSolver.okay()) { CounterExampleMap.clear(); - ConstructCounterExample(newS); + ConstructCounterExample(SatSolver); if (stats_flag && print_nodes_flag) { - PrintSATModel(newS); + PrintSATModel(SatSolver); } //check if the counterexample is good or not ComputeFormulaMap.clear(); if (counterexample_checking_during_refinement) bvdiv_exception_occured = false; - ASTNode orig_result = ComputeFormulaUsingModel(orig_input); + ASTNode orig_result = ComputeFormulaUsingModel(original_input); if (!(ASTTrue == orig_result || ASTFalse == orig_result)) FatalError("TopLevelSat: Original input must compute to "\ "true or false against model"); @@ -1816,11 +1821,11 @@ namespace BEEV // invalid if (ASTTrue == orig_result) { - //CheckCounterExample(newS.okay()); + //CheckCounterExample(SatSolver.okay()); PrintOutput(false); - PrintCounterExample(newS.okay()); - PrintCounterExample_InOrder(newS.okay()); - return 0; + PrintCounterExample(SatSolver.okay()); + PrintCounterExample_InOrder(SatSolver.okay()); + return SOLVER_INVALID; } // counterexample is bogus: flag it else @@ -1834,13 +1839,14 @@ namespace BEEV print_counterexample_flag = tmp; } - return 2; + return SOLVER_UNDECIDED; } } else { + //Control should never reach here PrintOutput(true); - return -100; + return SOLVER_ERROR; } } //end of CALLSAT_ResultCheck diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index f716c6a..bf4bc26 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -909,11 +909,9 @@ namespace BEEV //################################################## //################################################## - // FIXME: Don't use numeric codes. Use an enum type! //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 ERROR + //if returned 0 then input is INVALID if returned 1 then input is + //VALID if returned 2 then UNDECIDED int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) { ASTNode inputToSAT = inputasserts; @@ -998,10 +996,7 @@ namespace BEEV ASTNodeStats("after transformation: ", simplified_solved_InputToSAT); TermsAlreadySeenMap.clear(); - //if(stats_flag) - // printCacheStatus(); - - int res; + SOLVER_RETURN_TYPE res; //solver instantiated here MINISAT::Solver newS; //MINISAT::SimpSolver newS; @@ -1012,28 +1007,28 @@ namespace BEEV } res = CallSAT_ResultCheck(newS, simplified_solved_InputToSAT, orig_input); - if (2 != res) + if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); return res; } res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input); - if (2 != res) + if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); return res; } res = SATBased_ArrayWriteRefinement(newS, orig_input); - if (2 != res) + if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); return res; } res = SATBased_ArrayReadRefinement(newS, simplified_solved_InputToSAT, orig_input); - if (2 != res) + if (SOLVER_UNDECIDED != res) { CountersAndStats("print_func_stats"); return res; @@ -1042,8 +1037,8 @@ namespace BEEV FatalError("TopLevelSATAux: reached the end without proper conclusion:" "either a divide by zero in the input or a bug in STP"); //bogus return to make the compiler shut up - return 2; - } //End of TopLevelSAT + return SOLVER_ERROR; + } //End of TopLevelSATAux /******************************************************************* * Helper Functions diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index 42aa67a..2a56271 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -279,11 +279,13 @@ namespace BEEV { if (smtlib_parser_flag) { - if (true_iff_valid && (BEEV::input_status == TO_BE_SATISFIABLE)) + if (true_iff_valid && + (BEEV::input_status == TO_BE_SATISFIABLE)) { cerr << "Warning. Expected satisfiable, FOUND unsatisfiable" << endl; } - else if (!true_iff_valid && (BEEV::input_status == TO_BE_UNSATISFIABLE)) + else if (!true_iff_valid && + (BEEV::input_status == TO_BE_UNSATISFIABLE)) { cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; } -- 2.47.3