From: vijay_ganesh Date: Fri, 13 Nov 2009 19:10:14 +0000 (+0000) Subject: fixed the flex-related bug X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=a8e1d30759b6c7857b1355d2b6f2366e464e9c89;p=francis%2Fstp.git fixed the flex-related bug git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@402 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.h b/src/AST/AST.h index ed0887a..a57a521 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -94,7 +94,12 @@ namespace BEEV int, ClauseList *, ltint> ClauseBuckets; - + + typedef MAP< + int, + ASTVec, + ltint> UserGuided_AbsRefine_Asserts; + // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); }; // end namespace BEEV diff --git a/src/STPManager/STP.cpp b/src/STPManager/STP.cpp index 3bafce1..ee69d10 100644 --- a/src/STPManager/STP.cpp +++ b/src/STPManager/STP.cpp @@ -37,20 +37,20 @@ namespace BEEV { bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = arrayTransformer-> - CreateSubstitutionMap(simplified_solved_InputToSAT); + CreateSubstitutionMap(simplified_solved_InputToSAT); bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); //printf("##################################################\n"); bm->ASTNodeStats("after pure substitution: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, - false); + false); bm->ASTNodeStats("after simplification: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); } if(bm->UserFlags.wordlevel_solve_flag) @@ -79,16 +79,16 @@ namespace BEEV { bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); simplified_solved_InputToSAT = arrayTransformer-> - CreateSubstitutionMap(simplified_solved_InputToSAT); + CreateSubstitutionMap(simplified_solved_InputToSAT); bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); bm->ASTNodeStats("after pure substitution: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); simplified_solved_InputToSAT = simp->SimplifyFormula_TopLevel(simplified_solved_InputToSAT, - false); + false); bm->ASTNodeStats("after simplification: ", - simplified_solved_InputToSAT); + simplified_solved_InputToSAT); } if(bm->UserFlags.wordlevel_solve_flag) diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 9389bfa..c2c8708 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -382,7 +382,7 @@ namespace BEEV ~STPMgr() { - ClearAllTables(); + ClearAllTables(); vector::iterator it = _asserts.begin(); vector::iterator itend = _asserts.end(); @@ -396,7 +396,7 @@ namespace BEEV delete letmgr; delete runTimes; - + _interior_unique_table.clear(); _bvconst_unique_table.clear(); _symbol_unique_table.clear(); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 3b7c77d..46c657f 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -393,8 +393,8 @@ void vc_printQuery(VC vc){ nodestar persistNode(node n) { - persist.push_back(new node(n)); - return persist.back(); + persist.push_back(new node(n)); + return persist.back(); } @@ -421,7 +421,7 @@ Type vc_arrayType(VC vc, Type typeIndex, Type typeData) { } node output = b->CreateNode(BEEV::ARRAY,(*ti)[0],(*td)[0]); - return persistNode(output); + return persistNode(output); } //! Create an expression for the value of array at the given index @@ -1856,8 +1856,8 @@ void vc_Destroy(VC vc) { // } for (vector::iterator it = persist.begin(); it!= persist.end();it++) - delete *it; - persist.clear(); + delete *it; + persist.clear(); delete decls; delete (stpstar)vc; diff --git a/src/parser/Makefile b/src/parser/Makefile index 1c088dc..18e8724 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -15,15 +15,17 @@ libparser.a: $(OBJS) lexCVC.cpp: CVC.lex parseCVC_defs.h ../AST/AST.h $(LEX) -olexCVC.cpp -Pcvc CVC.lex -#For rules with multiple targets. Make runs the rule once for each target. -#These rules are "pattern rules" which only run once (rather than twice). +#For rules with multiple targets. Make runs the rule once for each +#target. These rules are "pattern rules" which only run once (rather +#than twice). + parseCV%_defs.h parseCV%.cpp: CVC.y $(YACC) -o cvc.tab.c -p cvc CVC.y @cp cvc.tab.c parseCVC.cpp @cp cvc.tab.h parseCVC_defs.h lexSMT.cpp: parseSMT_defs.h smtlib.lex ../AST/AST.h - $(LEX) -o lexSMT.cpp --prefix smt smtlib.lex + $(LEX) -olexSMT.cpp -Psmt smtlib.lex parseSM%_defs.h parseSM%.cpp:smtlib.y $(YACC) -o smt.tab.c -p smt smtlib.y diff --git a/src/parser/let-funcs.h b/src/parser/let-funcs.h index 9b33e21..b7ac39d 100644 --- a/src/parser/let-funcs.h +++ b/src/parser/let-funcs.h @@ -33,9 +33,9 @@ namespace BEEV } ~LETMgr() - { - delete _letid_expr_map; - } + { + delete _letid_expr_map; + } ASTNode ResolveID(const ASTNode& var); diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index 674409f..7d32058 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -23,10 +23,10 @@ namespace printer static string tolower(const char * name) { - string s(name); - for (size_t i = 0; i < s.size(); ++i) - s[i] = ::tolower(s[i]); - return s; + string s(name); + for (size_t i = 0; i < s.size(); ++i) + s[i] = ::tolower(s[i]); + return s; } string functionToSMTLIBName(const BEEV::Kind k); diff --git a/src/sat/sat.h b/src/sat/sat.h index 1c40435..4d3bdd9 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -2,23 +2,23 @@ #define SAT_H_ #ifdef CRYPTOMINISAT - #include "cryptominisat/Solver.h" - #include "cryptominisat/SolverTypes.h" +#include "cryptominisat/Solver.h" +#include "cryptominisat/SolverTypes.h" #endif #ifdef CORE - #include "core/Solver.h" - #include "core/SolverTypes.h" +#include "core/Solver.h" +#include "core/SolverTypes.h" #endif #ifdef SIMP - #include "simp/SimpSolver.h" - #include "core/SolverTypes.h" +#include "simp/SimpSolver.h" +#include "core/SolverTypes.h" #endif #ifdef UNSOUND - #include "unsound/UnsoundSimpSolver.h" - #include "core/SolverTypes.h" +#include "unsound/UnsoundSimpSolver.h" +#include "core/SolverTypes.h" #endif #endif diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index 8ecf2a0..c93cf89 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -19,35 +19,35 @@ namespace BEEV //Sort the clauses, and bucketize by the size of the clauses for(ClauseList::iterator it = cl->begin(), itend = cl->end(); - it!=itend; it++) + it!=itend; it++) { - ClausePtr cptr = *it; - int cl_size = cptr->size(); - if(cl_size >= MAX_BUCKET_LIMIT) - { - cl_size = MAX_BUCKET_LIMIT; - } - - //If no clauses of size cl_size have been seen, then create a - //bucket for that size - if(cb->find(cl_size) == cb->end()) - { - ClauseList * cllist = new ClauseList(); - cllist->push_back(cptr); - (*cb)[cl_size] = cllist; - } - else - { - ClauseList * cllist = (*cb)[cl_size]; - cllist->push_back(cptr); - } + ClausePtr cptr = *it; + int cl_size = cptr->size(); + if(cl_size >= MAX_BUCKET_LIMIT) + { + cl_size = MAX_BUCKET_LIMIT; + } + + //If no clauses of size cl_size have been seen, then create a + //bucket for that size + if(cb->find(cl_size) == cb->end()) + { + ClauseList * cllist = new ClauseList(); + cllist->push_back(cptr); + (*cb)[cl_size] = cllist; + } + else + { + ClauseList * cllist = (*cb)[cl_size]; + cllist->push_back(cptr); + } } return cb; } //End of SortClauseList_IntoBuckets() bool ToSAT::CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, - ClauseBuckets * cb) + ClauseBuckets * cb) { ClauseBuckets::iterator it = cb->begin(); ClauseBuckets::iterator itend = cb->end(); @@ -55,12 +55,12 @@ namespace BEEV bool sat = false; for(;it!=itend;it++) { - ClauseList *cl = (*it).second; - sat = toSATandSolve(SatSolver,*cl); - if(!sat) - { - return sat; - } + ClauseList *cl = (*it).second; + sat = toSATandSolve(SatSolver,*cl); + if(!sat) + { + return sat; + } } return sat; } @@ -94,13 +94,13 @@ namespace BEEV if(!sat) { - return sat; + return sat; } #ifdef CRYPTOMINISAT if(!xorcl->empty()) - { - sat = toSATandSolve(SatSolver, *xorcl, true); + { + sat = toSATandSolve(SatSolver, *xorcl, true); } cm->DELETE(xorcl); #endif diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 48ce34e..f9f70ae 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -638,12 +638,12 @@ namespace BEEV #ifdef CRYPTOMINISAT if ((x->clausespos != NULL - && x->clausespos->size() > 1) - || (doRenamePos(*x) && !wasVisited(*x))) + && x->clausespos->size() > 1) + || (doRenamePos(*x) && !wasVisited(*x))) { if (doSibRenamingPos(*x) - || sharesPos(*x) > 1 - || doRenamePos(*x)) + || sharesPos(*x) > 1 + || doRenamePos(*x)) { doRenamingPos(varphi, defs); } @@ -654,7 +654,7 @@ namespace BEEV if (x->clausespos != NULL && x->clausespos->size() > 1) { if (doSibRenamingPos(*x) - || sharesPos(*x) > 1) + || sharesPos(*x) > 1) { doRenamingPos(varphi, defs); } @@ -1293,13 +1293,13 @@ namespace BEEV { convertFormulaToCNF(*it, defs); // make pos and neg clause set - //Creating a new variable name for each of the children of the - //XOR node - //doRenamingPos(*it, defs); - doRenamingNeg(*it, defs); - xor_clause->insert(xor_clause->end(), - ((*(info[*it]->clausespos))[0])->begin(), - ((*(info[*it]->clausespos))[0])->end()); + //Creating a new variable name for each of the children of the + //XOR node + //doRenamingPos(*it, defs); + doRenamingNeg(*it, defs); + xor_clause->insert(xor_clause->end(), + ((*(info[*it]->clausespos))[0])->begin(), + ((*(info[*it]->clausespos))[0])->end()); } doRenamingPosXor(varphi); //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); @@ -1655,7 +1655,7 @@ namespace BEEV // && sharesPos(*xx) > 0 // && sharesNeg(*xx) > 0) // { - // return; + // return; // } ASTVec::const_iterator it = varphi.GetChildren().begin(); @@ -1665,12 +1665,12 @@ namespace BEEV { convertFormulaToCNF(*it, defs); // make pos and neg clause set - //Creating a new variable name for each of the children of the - //XOR node doRenamingPos(*it, defs); - doRenamingNeg(*it, defs); - xor_clause->insert(xor_clause->end(), - ((*(info[*it]->clausespos))[0])->begin(), - ((*(info[*it]->clausespos))[0])->end()); + //Creating a new variable name for each of the children of the + //XOR node doRenamingPos(*it, defs); + doRenamingNeg(*it, defs); + xor_clause->insert(xor_clause->end(), + ((*(info[*it]->clausespos))[0])->begin(), + ((*(info[*it]->clausespos))[0])->end()); } doRenamingPosXor(varphi); //ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); @@ -1909,8 +1909,8 @@ namespace BEEV { cerr << "Number of clauses:" << defs->size() << endl; PrintClauseList(cout, *defs); - cerr << "Number of xor-clauses:" << clausesxor->size() << endl; - PrintClauseList(cout, *clausesxor); + cerr << "Number of xor-clauses:" << clausesxor->size() << endl; + PrintClauseList(cout, *clausesxor); } return defs; diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 8f62a51..aa0d65f 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -11,23 +11,23 @@ namespace BEEV { -bool isTseitinVariable(const ASTNode& n) { - if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) { - const char * zz = n.GetName(); - //if the variables ARE cnf variables then dont make them - // decision variables. - if (0 == strncmp("cnf", zz, 3)) - { - return true; - } - } - return false; -} + bool isTseitinVariable(const ASTNode& n) { + if (n.GetKind() == SYMBOL && n.GetType() == BOOLEAN_TYPE) { + const char * zz = n.GetName(); + //if the variables ARE cnf variables then dont make them + // decision variables. + if (0 == strncmp("cnf", zz, 3)) + { + return true; + } + } + return false; + } - /* FUNCTION: lookup or create a new MINISAT literal - * lookup or create new MINISAT Vars from the global MAP - * _ASTNode_to_SATVar. - */ + /* FUNCTION: lookup or create a new MINISAT literal + * lookup or create new MINISAT Vars from the global MAP + * _ASTNode_to_SATVar. + */ MINISAT::Var ToSAT::LookupOrCreateSATVar(MINISAT::Solver& newS, const ASTNode& n) @@ -49,11 +49,11 @@ bool isTseitinVariable(const ASTNode& n) { // experimental. Don't add Tseitin variables as decision variables. if (!bm->UserFlags.tseitin_are_decision_variables_flag && isTseitinVariable(n)) - { - newS.setDecisionVar(v,false); - } + { + newS.setDecisionVar(v,false); + } - } + } else v = it->second; return v; @@ -66,7 +66,7 @@ bool isTseitinVariable(const ASTNode& n) { * unsat. else continue. */ bool ToSAT::toSATandSolve(MINISAT::Solver& newS, - ClauseList& cll, bool add_xor_clauses) + ClauseList& cll, bool add_xor_clauses) { CountersAndStats("SAT Solver", bm); bm->GetRunTimes()->start(RunTimes::SendingToSAT); @@ -110,31 +110,31 @@ bool isTseitinVariable(const ASTNode& n) { // continue; // } #ifdef CRYPTOMINISAT - if(add_xor_clauses) - { - //cout << "addXorClause:\n"; - newS.addXorClause(satSolverClause, false, 0, "z"); - } - else - { - newS.addClause(satSolverClause,0,"z"); - } + if(add_xor_clauses) + { + //cout << "addXorClause:\n"; + newS.addXorClause(satSolverClause, false, 0, "z"); + } + else + { + newS.addClause(satSolverClause,0,"z"); + } #else newS.addClause(satSolverClause); #endif float percentage=CLAUSAL_ABSTRACTION_CUTOFF; if(count++ >= input_clauselist_size*percentage) { - //Arbitrary adding only 60% of the clauses in the hopes of + //Arbitrary adding only 60% of the clauses in the hopes of //terminating early // cout << "Percentage clauses added: " // << percentage << endl; bm->GetRunTimes()->stop(RunTimes::SendingToSAT); bm->GetRunTimes()->start(RunTimes::Solving); #ifdef CRYPTOMINISAT - if (newS.simplify() == MINISAT::l_Undef) + if (newS.simplify() == MINISAT::l_Undef) #endif - newS.solve(); + newS.solve(); bm->GetRunTimes()->stop(RunTimes::Solving); if(!newS.okay()) { diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index 4654ae6..25ccbe0 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -23,7 +23,7 @@ namespace BEEV { - #define CLAUSAL_ABSTRACTION_CUTOFF 0.5 +#define CLAUSAL_ABSTRACTION_CUTOFF 0.5 class ToSAT { private: @@ -108,11 +108,11 @@ namespace BEEV //Iteratively goes through the Clause Buckets, and calls //toSATandSolve() bool CallSAT_On_ClauseBuckets(MINISAT::Solver& SatSolver, - ClauseBuckets * cb); + ClauseBuckets * cb); // Converts the clause to SAT and calls SAT solver bool toSATandSolve(MINISAT::Solver& S, - ClauseList& cll, bool add_xor_clauses=false); + ClauseList& cll, bool add_xor_clauses=false); //print the STP solver output void PrintOutput(SOLVER_RETURN_TYPE ret);