From 2d263b111df2e47f3e37947f9c694083263aca89 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 11 Sep 2009 02:38:17 +0000 Subject: [PATCH] fixed some issues with FOR-construct git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@218 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 13 +- .../AbstractionRefinement.cpp | 153 ++++++++++-------- src/main/Globals.cpp | 8 +- src/main/Globals.h | 5 + src/main/main.cpp | 22 +-- src/sat/sat.h | 12 +- src/sat/unsound/UnsoundSimpSolver.C | 42 ++--- src/simplifier/bvsolver.cpp | 20 +-- src/simplifier/simplifier.cpp | 22 +-- src/to-sat/ToSAT.cpp | 108 ++++++++----- 10 files changed, 227 insertions(+), 178 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 26ece48..85ad53d 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1231,13 +1231,16 @@ namespace BEEV 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); - + + ASTVec SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, + const ASTNode& original_input, + const ASTNode& finiteloop, + ASTNodeMap* ParamToCurrentValMap, + bool absrefine_flag=false); + ASTNode Check_FiniteLoop_UsingModel(const ASTNode& finiteloop, ASTNodeMap* ParamToCurrentValMap, bool CheckUsingModel_Or_Expand); diff --git a/src/abstraction-refinement/AbstractionRefinement.cpp b/src/abstraction-refinement/AbstractionRefinement.cpp index 852a076..d441d43 100644 --- a/src/abstraction-refinement/AbstractionRefinement.cpp +++ b/src/abstraction-refinement/AbstractionRefinement.cpp @@ -251,45 +251,64 @@ namespace BEEV BeevMgr::SATBased_AllFiniteLoops_Refinement(MINISAT::Solver& SatSolver, const ASTNode& original_input) { - SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED; - std::vector retvec; + ASTVec retvec; + ASTVec Allretvec; + Allretvec.push_back(ASTTrue); + SOLVER_RETURN_TYPE res = SOLVER_UNDECIDED; for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(), iend=GlobalList_Of_FiniteLoops.end(); i!=iend; i++) - { - //ASTNodeMap * ParamToCurrentValMap = new ASTNodeMap; - ASTNodeMap ParamToCurrentValMap; - ret = SATBased_FiniteLoop_Refinement(SatSolver, - original_input, - *i, - &ParamToCurrentValMap); - if(SOLVER_VALID == ret) - { - return ret; - } - retvec.push_back(ret); + { + //cout << "The number of abs-refinement limit is " << num_absrefine << endl; + for(int absrefine_count=0;absrefine_count < num_absrefine; absrefine_count++) + { + ASTNodeMap ParamToCurrentValMap; + retvec = SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + *i, + &ParamToCurrentValMap, + true); //absrefine flag + ASTNode retformula = + (retvec.size() == 1) ? + retvec[0] : CreateNode(AND,retvec); + //SimplifyFormula(CreateNode(AND,Allretvec),false,NULL); + retformula = TransformFormula_TopLevel(retformula); + + //Add the return value of all loops to the SAT Solver + res = + CallSAT_ResultCheck(SatSolver, retformula, original_input); + if(SOLVER_UNDECIDED != res) + { + return res; + } + } //end of absrefine count + + ASTNodeMap ParamToCurrentValMap; + retvec = SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + *i, + &ParamToCurrentValMap, + false); //absrefine flag + + ASTNode retformula = + (retvec.size() == 1) ? + retvec[0] : CreateNode(AND,retvec); + retformula = TransformFormula_TopLevel(retformula); + //Add the return value of all loops to the SAT Solver + SOLVER_RETURN_TYPE res = + CallSAT_ResultCheck(SatSolver, retformula, original_input); + if(SOLVER_UNDECIDED != res) + { + return res; + } } //End of For() - //Even if one of the for loops results in SOLVER_UNDECIDED, then - //it means that the constructed model is bogus. Return this fact. - for(vector::iterator i=retvec.begin(), - iend=retvec.end();i!=iend;i++) - { - if(SOLVER_UNDECIDED == *i) - { - return SOLVER_UNDECIDED; - } - } - - //All for loops are true in the model - //return CallSAT_ResultCheck(SatSolver, ASTTrue, original_input); - return ret; + return res; } //end of SATBased_AllFiniteLoops_Refinement() /***************************************************************** * SATBased_FiniteLoop_Refinement * - * * 'finiteloop' is the finite loop to be expanded * Every finiteloop has three parts: * 0) Parameter Name @@ -308,11 +327,12 @@ namespace BEEV // //Expand the finite loop, check against model, and add false //formulas to the SAT solver - SOLVER_RETURN_TYPE + ASTVec BeevMgr::SATBased_FiniteLoop_Refinement(MINISAT::Solver& SatSolver, const ASTNode& original_input, const ASTNode& finiteloop, - ASTNodeMap* ParamToCurrentValMap) + ASTNodeMap* ParamToCurrentValMap, + bool absrefine_flag) { //BVTypeCheck should have already checked the sanity of the input //FOR-formula @@ -329,23 +349,27 @@ namespace BEEV (*ParamToCurrentValMap)[parameter] = CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - SOLVER_RETURN_TYPE ret = SOLVER_UNDECIDED; //Go recursively thru' all the FOR-constructs. if(FOR == formulabody.GetKind()) { + ASTVec retvec; + ASTVec retvec_innerfor; + retvec.push_back(ASTTrue); while(paramCurrentValue < paramLimit) { - ret = SATBased_FiniteLoop_Refinement(SatSolver, - original_input, - formulabody, - ParamToCurrentValMap); - if(SOLVER_VALID == ret) + retvec_innerfor = + SATBased_FiniteLoop_Refinement(SatSolver, + original_input, + formulabody, + ParamToCurrentValMap, + absrefine_flag); + + for(ASTVec::iterator i=retvec_innerfor.begin(), + iend=retvec_innerfor.end();i!=iend;i++) { - //If formula is valid, return immediately - return ret; + retvec.push_back(*i); } - //Update ParamToCurrentValMap with parameter and its //current value. FIXME: Possible leak since I am not //freeing the previous 'value' for the same 'key' @@ -354,16 +378,14 @@ namespace BEEV CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); } //end of While - //The last 'ret' value is the truthvalue of the formula. If it - //is SOLVER_INVALID then the formula is indeed INVALID, else - //ret can only be SOLVER_UNDECIDED at this point. Hence return - //UNDECIDED. - return ret; + return retvec; } //end of recursion FORs //Expand the leaf level FOR-construct completely //increment of paramCurrentValue done inside loop int ThisForLoopAllTrue = 0; + ASTVec ForloopVec; + ForloopVec.push_back(ASTTrue); for(;paramCurrentValue < paramLimit;) { ASTNode currentFormula; @@ -381,40 +403,33 @@ namespace BEEV //Check the currentformula against the model, and add it to the //SAT solver if it is false against the model - if(ASTFalse == ComputeFormulaUsingModel(currentFormula)) - { - currentFormula = TransformFormula_TopLevel(currentFormula); - SOLVER_RETURN_TYPE result = - CallSAT_ResultCheck(SatSolver, currentFormula, original_input); - if(result != SOLVER_UNDECIDED) - { - return result; - } + if(absrefine_flag && + ASTFalse == ComputeFormulaUsingModel(currentFormula)) + { + ForloopVec.push_back(currentFormula); } else { - //ComputeFormulaUsingModel can either return ASTFalse or - //ASTTrue - ThisForLoopAllTrue++; + if(ASTTrue != currentFormula) + { + ForloopVec.push_back(currentFormula); + } + if(ASTFalse == currentFormula) + { + ForloopVec.push_back(ASTFalse); + return ForloopVec; + } } //Update ParamToCurrentValMap with parameter and its current - //value - // - //FIXME: Possible leak since I am not freeing the previous - //'value' for the same 'key' + //value. FIXME: Possible leak since I am not freeing the + //previous 'value' for the same 'key' paramCurrentValue = paramCurrentValue + paramIncrement; (*ParamToCurrentValMap)[parameter] = - CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); - //cout << (*ParamToCurrentValMap)[parameter]; + CreateBVConst(finiteloop[1].GetValueWidth(),paramCurrentValue); } //end of expanding the FOR loop - if(ThisForLoopAllTrue == paramLimit) - { - return SOLVER_INVALID; - } - - return SOLVER_UNDECIDED; + return ForloopVec; } //end of the SATBased_FiniteLoop_Refinement() //SATBased_FiniteLoop_Refinement_UsingModel diff --git a/src/main/Globals.cpp b/src/main/Globals.cpp index dd35947..cc6e725 100644 --- a/src/main/Globals.cpp +++ b/src/main/Globals.cpp @@ -42,7 +42,13 @@ namespace BEEV bool print_binary_flag = false; //Expands out the finite for-construct completely - bool expand_finitefor_flag; + bool expand_finitefor_flag = false; + + //Determines the number of abstraction-refinement loop count for the + //for-construct + bool num_absrefine_flag = false; + int num_absrefine = 0; + //if this option is true then print the way dawson wants using a //different printer. do not use this printer. diff --git a/src/main/Globals.h b/src/main/Globals.h index 6d1b4ae..fca9d40 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -70,6 +70,11 @@ namespace BEEV //Expands out the finite for-construct completely extern bool expand_finitefor_flag; + //Determines the number of abstraction-refinement loop count for the + //for-construct + extern bool num_absrefine_flag; + extern int num_absrefine; + //if this option is true then print the way dawson wants using a //different printer. do not use this printer. extern bool print_arrayval_declaredorder_flag; diff --git a/src/main/main.cpp b/src/main/main.cpp index 16cc0eb..76c1c29 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -51,6 +51,7 @@ int main(int argc, char ** argv) { helpstring += "-c : construct counterexample\n"; helpstring += "-d : check counterexample\n"; helpstring += "-e : expand finite-for construct\n"; + helpstring += "-f : number of abstraction-refinement loops\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; helpstring += "-p : print counterexample\n"; @@ -65,6 +66,13 @@ int main(int argc, char ** argv) { { if(argv[i][0] == '-') { + if(argv[i][2]) { + fprintf(stderr, "Multiple character options are not allowed.\n"); + fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n"); + fprintf(stderr,usage,prog); + cout << helpstring; + return -1; + } switch(argv[i][1]) { case 'a' : @@ -83,6 +91,10 @@ int main(int argc, char ** argv) { case 'e': expand_finitefor_flag = true; break; + case 'f': + num_absrefine_flag = true; + num_absrefine = atoi(argv[++i]); + break; case 'h': fprintf(stderr,usage,prog); cout << helpstring; @@ -133,16 +145,8 @@ int main(int argc, char ** argv) { return -1; break; } - if(argv[i][2]) { - fprintf(stderr, "Multiple character options are not allowed.\n"); - fprintf(stderr, "(for example: -ab is not an abbreviation for -a -b)\n"); - fprintf(stderr,usage,prog); - cout << helpstring; - return -1; - } - } else { + } else { infile = argv[i]; - if (smtlib_parser_flag) { smtin = fopen(infile,"r"); diff --git a/src/sat/sat.h b/src/sat/sat.h index f17456c..c6e9224 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -3,17 +3,7 @@ #include "core/Solver.h" #include "core/SolverTypes.h" -//#include "../sat/simp/SimpSolver.h" -//#include "../sat/unsound/UnsoundSimpSolver.h" - - -#endif /* SAT_H_ */ -#ifndef SAT_H_ -#define SAT_H_ - -#include "core/Solver.h" -#include "core/SolverTypes.h" -//#include "../sat/simp/SimpSolver.h" +#include "../sat/simp/SimpSolver.h" //#include "../sat/unsound/UnsoundSimpSolver.h" diff --git a/src/sat/unsound/UnsoundSimpSolver.C b/src/sat/unsound/UnsoundSimpSolver.C index 72f40cc..1901ccc 100644 --- a/src/sat/unsound/UnsoundSimpSolver.C +++ b/src/sat/unsound/UnsoundSimpSolver.C @@ -491,30 +491,32 @@ bool UnsoundSimpSolver::eliminateVar(Var v, bool fail, bool stop_unsoundness) return false; - if(!stop_unsoundness) { - //abductive logic - vec resolvedClauses; - for (int i = 0; i < pos.size(); i++) { - for (int j = 0; j < pos.size(); j++) { + if(!stop_unsoundness) + { + //abductive logic + vec resolvedClauses; + for (int i = 0; i < pos.size(); i++) { + for (int j = 0; j < pos.size(); j++) { + if(i == j) + continue; + abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true); + if(!addClause(resolvedClauses)) + return false; + } + } + //} + + resolvedClauses.clear(); + for (int i = 0; i < neg.size(); i++) { + for (int j = 0; j < neg.size(); j++) { if(i == j) continue; - abductive_merge(*pos[i], *pos[j], v, resolvedClauses, true); + abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true); if(!addClause(resolvedClauses)) - return false; + return false; } - } - } -// resolvedClauses.clear(); -// for (int i = 0; i < neg.size(); i++) { -// for (int j = 0; j < neg.size(); j++) { -// if(i == j) -// continue; -// abductive_neg_merge(*neg[i], *neg[j], v, resolvedClauses,true); -// if(!addClause(resolvedClauses)) -// return false; -// } -// } -// } + } + } // DEBUG: For checking that a clause set is saturated with respect // to variable elimination. If the clause set is expected diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index 4d68ab6..a51549d 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -310,7 +310,7 @@ namespace BEEV { ASTNode eq = input; //cerr << "Input to BVSolve_Odd()" << eq << endl; - if (!(wordlevel_solve_flag && EQ == eq.GetKind())) + if (!(EQ == eq.GetKind())) { return input; } @@ -524,10 +524,10 @@ namespace BEEV //the formula ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input) { - if (!wordlevel_solve_flag) - { - return input; - } + // if (!wordlevel_solve_flag) + // { + // return input; + // } Kind k = input.GetKind(); if (!(EQ == k || AND == k)) @@ -596,7 +596,7 @@ namespace BEEV { ASTNode eq = input; //cerr << "Input to BVSolve_Odd()" << eq << endl; - if (!(wordlevel_solve_flag && EQ == eq.GetKind())) + if (!(EQ == eq.GetKind())) { evenflag = false; return eq; @@ -652,10 +652,10 @@ namespace BEEV //solve an eqn whose monomials have only even coefficients ASTNode BVSolver::BVSolve_Even(const ASTNode& input) { - if (!wordlevel_solve_flag) - { - return input; - } + // if (!wordlevel_solve_flag) + // { + // return input; + // } if (!(EQ == input.GetKind() || AND == input.GetKind())) { diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 5e8f864..187e40a 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -324,8 +324,8 @@ ASTNode Flatten(const ASTNode& a) BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - if (!optimize_flag) - return b; +// if (!optimize_flag) +// return b; Kind kind = b.GetKind(); if (BOOLEAN_TYPE != b.GetType()) @@ -404,8 +404,8 @@ ASTNode Flatten(const ASTNode& a) BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { - if (!optimize_flag) - return a; +// if (!optimize_flag) +// return a; ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -686,7 +686,7 @@ ASTNode Flatten(const ASTNode& a) { CountersAndStats("ITEOpts_InEqs"); - if (!(EQ == in.GetKind() && optimize_flag)) + if (!(EQ == in.GetKind())) { return in; } @@ -1258,8 +1258,8 @@ ASTNode Flatten(const ASTNode& a) ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - if (!optimize_flag) - return b; + // if (!optimize_flag) +// return b; ASTNode output; if (CheckSimplifyMap(b, output, pushNeg, VarConstMap)) @@ -1395,10 +1395,10 @@ ASTNode Flatten(const ASTNode& a) ASTNode inputterm(actualInputterm); // mutable local copy. //cout << "SimplifyTerm: input: " << a << endl; - if (!optimize_flag) - { - return inputterm; - } + // if (!optimize_flag) + // { + // return inputterm; + // } ASTNode output; assert(BVTypeCheck(inputterm)); diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 76232f0..d7b96c5 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -938,23 +938,32 @@ namespace BEEV { inputToSAT = simplified_solved_InputToSAT; - simplified_solved_InputToSAT = - CreateSubstitutionMap(simplified_solved_InputToSAT); - //printf("##################################################\n"); - 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); + if(optimize_flag) + { + + simplified_solved_InputToSAT = + CreateSubstitutionMap(simplified_solved_InputToSAT); + //printf("##################################################\n"); + ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + + simplified_solved_InputToSAT = + SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); + ASTNodeStats("after simplification: ", simplified_solved_InputToSAT); + } + + if(wordlevel_solve_flag) + { + 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); + ASTNodeStats("Before SimplifyWrites_Inplace begins: ", + simplified_solved_InputToSAT); + SimplifyWrites_InPlace_Flag = true; Begin_RemoveWrites = false; start_abstracting = false; @@ -962,22 +971,27 @@ namespace BEEV do { inputToSAT = simplified_solved_InputToSAT; - simplified_solved_InputToSAT = - CreateSubstitutionMap(simplified_solved_InputToSAT); - ASTNodeStats("after pure substitution: ", simplified_solved_InputToSAT); + + if(optimize_flag) + { + 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); + } + + if(wordlevel_solve_flag) + { + simplified_solved_InputToSAT = + bvsolver->TopLevelBVSolve(simplified_solved_InputToSAT); + ASTNodeStats("after solving: ", simplified_solved_InputToSAT); + } + } while (inputToSAT != 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); - delete bvsolver; bvsolver = NULL; @@ -990,21 +1004,31 @@ namespace BEEV } TermsAlreadySeenMap.clear(); - do - { - inputToSAT = simplified_solved_InputToSAT; - //simplified_solved_InputToSAT = - //CreateSubstitutionMap(simplified_solved_InputToSAT); - //Begin_RemoveWrites = true; 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); + // do +// { +// inputToSAT = simplified_solved_InputToSAT; + +// if(optimize_flag) +// { +// //simplified_solved_InputToSAT = +// //CreateSubstitutionMap(simplified_solved_InputToSAT); +// //Begin_RemoveWrites = true; ASTNodeStats("after pure +// //substitution: ", simplified_solved_InputToSAT); +// simplified_solved_InputToSAT = +// SimplifyFormula_TopLevel(simplified_solved_InputToSAT, false); +// //ASTNodeStats("after simplification: ", +// //simplified_solved_InputToSAT); +// // +// } + +// if(wordlevel_solve_flag) +// { +// simplified_solved_InputToSAT +// = bvsolver.TopLevelBVSolve(simplified_solved_InputToSAT); +// ASTNodeStats("after solving: ", +// simplified_solved_InputToSAT); +// } +// } while (inputToSAT != simplified_solved_InputToSAT); if (start_abstracting) { -- 2.47.3