From: trevor_hansen Date: Thu, 26 Jan 2012 05:04:55 +0000 (+0000) Subject: Improvement. The SMT-LIB2 parser no longer stores a copy of the asserts/query locally... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=8f9621c02a0d8a701fd1bf2b3cf51042204f4027;p=francis%2Fstp.git Improvement. The SMT-LIB2 parser no longer stores a copy of the asserts/query locally. It uses the stored one. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1525 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 4592366..11df009 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -485,6 +485,32 @@ namespace BEEV return _current_query; } + // return a vector of the levels. + // before returning any vector with >1 nodes is turned into a conjunct. + const ASTVec STPMgr::getVectorOfAsserts() + { + vector::iterator it = _asserts.begin(); + vector::iterator itend = _asserts.end(); + + ASTVec result; + for(; it != itend; it++) + { + ASTVec& a = (**it); + if (a.size() ==0) + a.push_back(ASTTrue); + else if (a.size() > 1) + { + ASTNode conjunct = defaultNodeFactory->CreateNode(AND,a); + a.resize(0); + a.push_back(conjunct); + } + + result.push_back(a[0]); + } + + return result; + } + const ASTVec STPMgr::GetAsserts(void) { diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index 937e2cb..bf47282 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -113,6 +113,11 @@ namespace BEEV {(*it)->iteration = 0;} } + int getAssertLevel() + { + return _asserts.size(); + } + private: // Stack of Logical Context. each entry in the stack is a logical @@ -388,7 +393,9 @@ namespace BEEV void Push(void); const ASTNode PopQuery(); const ASTNode GetQuery(); - const ASTVec GetAsserts(void); + const ASTVec GetAsserts(); + const ASTVec getVectorOfAsserts(); + //add a query/assertion to the current logical context void AddQuery(const ASTNode& q); diff --git a/src/cpp_interface/cpp_interface.cpp b/src/cpp_interface/cpp_interface.cpp index f1ebb50..cca62c6 100644 --- a/src/cpp_interface/cpp_interface.cpp +++ b/src/cpp_interface/cpp_interface.cpp @@ -2,22 +2,19 @@ namespace BEEV { - - -// Does some simple caching of prior results. + // Does some simple caching of prior results. + // Assumes that there is one node for each level!!! void - Cpp_interface::checkSat(vector & assertionsSMT2) + Cpp_interface::checkSat(const ASTVec & assertionsSMT2) { bm.GetRunTimes()->stop(RunTimes::Parsing); + assert(assertionsSMT2.size() == cache.size()); Entry& cacheEntry = cache.back(); - //cerr << "------------" << endl; - //printStatus(); - if ((cacheEntry.result == SOLVER_SATISFIABLE || cacheEntry.result == SOLVER_UNSATISFIABLE) - && (assertionsSMT2.back().size() ==1 && assertionsSMT2.back()[0] == cacheEntry.node)) + && (assertionsSMT2.back() == cacheEntry.node)) { // If we already know the answer then return. if (bm.UserFlags.quick_statistics_flag) { @@ -32,30 +29,12 @@ namespace BEEV bm.ClearAllTables(); GlobalSTP->ClearAllTables(); - // Loop through the set of assertions converting them to single nodes.. - ASTVec v; - for (int i = 0; i < assertionsSMT2.size(); i++) - { - if (assertionsSMT2[i].size() == 1) - {} - else if (assertionsSMT2[i].size() == 0) - assertionsSMT2[i].push_back(bm.ASTTrue); - else - { - ASTNode v = parserInterface->CreateNode(AND, assertionsSMT2[i]); - assertionsSMT2[i].clear(); - assertionsSMT2[i].push_back(v); - } - assert(assertionsSMT2[i].size() ==1); - v.push_back(assertionsSMT2[i][0]); - } - ASTNode query; - if (v.size() > 1) - query = parserInterface->CreateNode(AND, v); - else if (v.size() > 0) - query = v[0]; + if (assertionsSMT2.size() >= 1) + query = parserInterface->CreateNode(AND, assertionsSMT2); + else if (assertionsSMT2.size() == 1) + query = assertionsSMT2[0]; else query = bm.ASTTrue; @@ -65,7 +44,7 @@ namespace BEEV if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE) { Entry e(last_result); - e.node = assertionsSMT2.back()[0]; + e.node = assertionsSMT2.back(); cacheEntry = e; assert (!cacheEntry.node.IsNull()); } diff --git a/src/cpp_interface/cpp_interface.h b/src/cpp_interface/cpp_interface.h index 5b7e4a9..3e2b39f 100644 --- a/src/cpp_interface/cpp_interface.h +++ b/src/cpp_interface/cpp_interface.h @@ -48,6 +48,11 @@ namespace BEEV vector cache; vector > symbols; + void checkInvariant() + { + assert(bm.getAssertLevel() == cache.size()); + assert(bm.getAssertLevel() == symbols.size()); + } public: LETMgr letMgr; @@ -58,8 +63,13 @@ namespace BEEV { assert(nf != NULL); alreadyWarned = false; + cache.push_back(Entry(SOLVER_UNDECIDED)); symbols.push_back(ASTVec()); + + if (bm.getVectorOfAsserts().size() ==0) + bm.Push(); + print_success = false; } @@ -79,6 +89,12 @@ namespace BEEV return bm.GetAsserts(); } + const ASTVec + getAssertVector(void) + { + return bm.getVectorOfAsserts(); + } + UserDefinedFlags& getUserFlags() { @@ -239,12 +255,15 @@ namespace BEEV if (symbols.size() == 1) FatalError("Can't pop away the default base element."); + bm.Pop(); + assert(symbols.size() == cache.size()); cache.erase(cache.end() - 1); ASTVec & current = symbols.back(); for (int i = 0; i < current.size(); i++) letMgr._parser_symbol_table.erase(current[i]); symbols.erase(symbols.end() - 1); + checkInvariant(); } void @@ -256,8 +275,10 @@ namespace BEEV else cache.push_back(Entry(SOLVER_UNDECIDED)); + bm.Push(); symbols.push_back(ASTVec()); assert(symbols.size() == cache.size()); + checkInvariant(); } void @@ -271,7 +292,7 @@ namespace BEEV } void - checkSat(vector & assertionsSMT2); + checkSat(const ASTVec & assertionsSMT2); void cleanUp() diff --git a/src/main/main.cpp b/src/main/main.cpp index d40acb4..d5e127d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -25,12 +25,11 @@ using namespace __gnu_cxx; using namespace BEEV; extern int smtparse(void*); -extern int smt2parse(void*); +extern int smt2parse(); extern int cvcparse(void*); extern int cvclex_destroy(void); extern int smtlex_destroy(void); extern int smt2lex_destroy(void); -extern vector assertionsSMT2; // callback for SIGALRM. void handle_time_out(int parameter){ @@ -446,9 +445,7 @@ int main(int argc, char ** argv) { smtparse((void*) AssertsQuery); smtlex_destroy(); } else if (bm->UserFlags.smtlib2_parser_flag) { - assertionsSMT2.push_back(ASTVec()); - smt2parse((void*) AssertsQuery); - //parserInterface->letMgr.cleanupParserSymbolTable(); + smt2parse(); smt2lex_destroy(); } else { cvcparse((void*) AssertsQuery); diff --git a/src/parser/smt2.y b/src/parser/smt2.y index 332fbb6..aa79897 100644 --- a/src/parser/smt2.y +++ b/src/parser/smt2.y @@ -65,14 +65,12 @@ return 1; } - ASTNode querysmt2; - vector assertionsSMT2; - + #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 104857600 #define YYERROR_VERBOSE 1 #define YY_EXIT_FAILURE -1 -#define YYPARSE_PARAM AssertsQuery + %} %union { @@ -195,8 +193,6 @@ %% cmd: commands END { - querysmt2 = ASTNode(); - assertionsSMT2.clear(); parserInterface->cleanUp(); YYACCEPT; } @@ -211,14 +207,12 @@ commands: commands cmdi cmdi: LPAREN_TOK EXIT_TOK RPAREN_TOK { - querysmt2 = ASTNode(); - assertionsSMT2.clear(); parserInterface->cleanUp(); YYACCEPT; } | LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK { - parserInterface->checkSat(assertionsSMT2); + parserInterface->checkSat(parserInterface->getAssertVector()); } | LPAREN_TOK LOGIC_TOK STRING_TOK RPAREN_TOK @@ -247,17 +241,13 @@ cmdi: for (int i=0; i < $3;i++) { parserInterface->push(); - assertionsSMT2.push_back(ASTVec()); } parserInterface->success(); } | LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK { for (int i=0; i < $3;i++) - { parserInterface->pop(); - assertionsSMT2.erase(assertionsSMT2.end()-1); - } parserInterface->success(); } | LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK @@ -266,7 +256,7 @@ cmdi: } | LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK { - assertionsSMT2.back().push_back(*$3); + parserInterface->AddAssert(*$3); parserInterface->deleteNode($3); parserInterface->success(); }