From 95565ce590b569639c99317b546950f587f603b1 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 27 Jun 2011 02:12:57 +0000 Subject: [PATCH] Adds the push(n) and pop(n) instructions to the SMTLIB2 command language. Previously hitting the EOF would trigger a check for satisfiability. Now, you need to explicitly call (check-sat). git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1357 e59a4935-1847-0410-ae03-e826735625c1 --- src/main/Globals.h | 4 +- src/main/main.cpp | 137 ++++++++++++++++------------- src/parser/ParserInterface.h | 165 +++++++++++++++++++++++++++++++++++ src/parser/smt2.lex | 5 +- src/parser/smt2.y | 51 ++++++----- 5 files changed, 280 insertions(+), 82 deletions(-) diff --git a/src/main/Globals.h b/src/main/Globals.h index f5171f6..da81672 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -59,7 +59,9 @@ namespace BEEV SOLVER_INVALID=0, SOLVER_VALID=1, SOLVER_UNDECIDED=2, - SOLVER_ERROR=-100 + SOLVER_ERROR=-100, + SOLVER_UNSATISFIABLE = 1, + SOLVER_SATISFIABLE = 0 }; //Empty vector. Useful commonly used ASTNodes diff --git a/src/main/main.cpp b/src/main/main.cpp index 49f2c63..1568f1c 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -30,6 +30,7 @@ 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){ @@ -503,12 +504,25 @@ int main(int argc, char ** argv) { else parserInterface = &piTypeCheckSimp; + if (onePrintBack) + { + if (bm->UserFlags.smtlib2_parser_flag) + { + cerr << "Printback from SMTLIB2 inputs isn't currently working." << endl; + cerr << "Please try again later" << endl; + cerr << "It works prior to revision 1354" << endl; + exit(1); + } + } + if (bm->UserFlags.smtlib1_parser_flag) { smtparse((void*) AssertsQuery); smtlex_destroy(); } else if (bm->UserFlags.smtlib2_parser_flag) { - smt2parse((void*) AssertsQuery); + assertionsSMT2.push_back(ASTVec()); + smt2parse((void*) AssertsQuery); + //parserInterface->letMgr.cleanupParserSymbolTable(); smt2lex_destroy(); } else { cvcparse((void*) AssertsQuery); @@ -520,80 +534,87 @@ int main(int argc, char ** argv) { } bm->GetRunTimes()->stop(RunTimes::Parsing); - if(((ASTVec*)AssertsQuery)->empty()) + /* The SMTLIB2 has a command language. The parser calls all the functions, + * so when we get to here the parser has already called "exit". i.e. if the + * language is smt2 then all the work has already been done, and all we need + * to do is cleanup... + * */ + if (!bm->UserFlags.smtlib2_parser_flag) { - FatalError("Input is Empty. Please enter some asserts and query\n"); - } - if(((ASTVec*)AssertsQuery)->size() != 2) - { - FatalError("Input must contain a query\n"); - } + if (((ASTVec*) AssertsQuery)->empty()) + { + FatalError("Input is Empty. Please enter some asserts and query\n"); + } - ASTNode asserts = (*(ASTVec*)AssertsQuery)[0]; - ASTNode query = (*(ASTVec*)AssertsQuery)[1]; + if (((ASTVec*) AssertsQuery)->size() != 2) + { + FatalError("Input must contain a query\n"); + } - if (onePrintBack) - { + ASTNode asserts = (*(ASTVec*) AssertsQuery)[0]; + ASTNode query = (*(ASTVec*) AssertsQuery)[1]; - ASTNode original_input = bm->CreateNode(AND, - bm->CreateNode(NOT, query), - asserts); + if (onePrintBack) + { + ASTNode original_input = bm->CreateNode(AND, bm->CreateNode(NOT, query), asserts); - if(bm->UserFlags.print_STPinput_back_flag) - { - if(bm->UserFlags.smtlib1_parser_flag) - bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true; - else - bm->UserFlags.print_STPinput_back_CVC_flag = true; - } + if (bm->UserFlags.print_STPinput_back_flag) + { + if (bm->UserFlags.smtlib1_parser_flag) + bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true; + else + bm->UserFlags.print_STPinput_back_CVC_flag = true; + } - if (bm->UserFlags.print_STPinput_back_CVC_flag) - { - //needs just the query. Reads the asserts out of the data structure. - print_STPInput_Back(query); - } + if (bm->UserFlags.print_STPinput_back_CVC_flag) + { + //needs just the query. Reads the asserts out of the data structure. + print_STPInput_Back(query); + } - if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag) - { - printer::SMTLIB1_PrintBack(cout, original_input); - } + if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag) + { + printer::SMTLIB1_PrintBack(cout, original_input); + } - if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag) - { - printer::SMTLIB2_PrintBack(cout, original_input); - } + if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag) + { + printer::SMTLIB2_PrintBack(cout, original_input); + } - if (bm->UserFlags.print_STPinput_back_C_flag) - { - printer::C_Print(cout, original_input); - } + if (bm->UserFlags.print_STPinput_back_C_flag) + { + printer::C_Print(cout, original_input); + } - if (bm->UserFlags.print_STPinput_back_GDL_flag) - { - printer::GDL_Print(cout, original_input); - } + if (bm->UserFlags.print_STPinput_back_GDL_flag) + { + printer::GDL_Print(cout, original_input); + } - if (bm->UserFlags.print_STPinput_back_dot_flag) - { - printer::Dot_Print(cout, original_input); - } + if (bm->UserFlags.print_STPinput_back_dot_flag) + { + printer::Dot_Print(cout, original_input); + } - return 0; - } + return 0; + } - SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query); - if (bm->UserFlags.quick_statistics_flag) - { - bm->GetRunTimes()->print(); - } - (GlobalSTP->tosat)->PrintOutput(ret); + SOLVER_RETURN_TYPE ret = GlobalSTP->TopLevelSTP(asserts, query); + if (bm->UserFlags.quick_statistics_flag) + { + bm->GetRunTimes()->print(); + } + (GlobalSTP->tosat)->PrintOutput(ret); + asserts = ASTNode(); + query = ASTNode(); + } AssertsQuery->clear(); delete AssertsQuery; - asserts = ASTNode(); - query = ASTNode(); + _empty_ASTVec.clear(); simpCleaner.release(); @@ -605,7 +626,5 @@ int main(int argc, char ** argv) { delete ParserBM; - - return 0; }//end of Main diff --git a/src/parser/ParserInterface.h b/src/parser/ParserInterface.h index d3c9405..b6ab66a 100644 --- a/src/parser/ParserInterface.h +++ b/src/parser/ParserInterface.h @@ -9,6 +9,7 @@ #include #include "LetMgr.h" #include "../STPManager/STPManager.h" +#include "../STPManager/STP.h" //#include "../boost/pool/object_pool.hpp" namespace BEEV @@ -35,6 +36,9 @@ public: { assert(nf != NULL); alreadyWarned = false; + cache.push_back(Entry(SOLVER_UNDECIDED)); + symbols.push_back(ASTVec()); + } const ASTVec GetAsserts(void) @@ -153,6 +157,167 @@ public: delete n; //node_pool.destroy(n); } + + struct Entry + { + explicit Entry( SOLVER_RETURN_TYPE result_) + { + result = result_; + } + + SOLVER_RETURN_TYPE result; + ASTNode node; + + void print() + { + if (result == SOLVER_UNSATISFIABLE) + cerr << "u"; + else if (result == SOLVER_SATISFIABLE) + cerr << "s"; + else if (result == SOLVER_UNDECIDED) + cerr << "?"; + } + }; + vector cache; + vector > symbols; + + void + addSymbol(ASTNode &s) + { + symbols.back().push_back(s); + letMgr._parser_symbol_table.insert(s); + } + + void + pop() + { + if (symbols.size() ==0) + FatalError("Popping from an empty stack."); + if (symbols.size() ==1) + FatalError("Can't pop away the default base element."); + + 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); + } + + void + push() + { + // If the prior one is unsatisiable then the new one will be too. + if (cache.size() > 1 && cache.back().result == SOLVER_UNSATISFIABLE) + cache.push_back(Entry(SOLVER_UNSATISFIABLE)); + else + cache.push_back(Entry(SOLVER_UNDECIDED)); + + symbols.push_back(ASTVec()); + assert(symbols.size() == cache.size()); + } + + void printStatus() + { + for (int i=0; i < cache.size();i++) + { + cache[i].print(); + } + cerr<< endl; + } + + // Does some simple caching of prior results. + void + checkSat(vector & 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)) + { // If we already know the answer then return. + if (bm.UserFlags.quick_statistics_flag) + { + bm.GetRunTimes()->print(); + } + + (GlobalSTP->tosat)->PrintOutput(cache.back().result); + bm.GetRunTimes()->start(RunTimes::Parsing); + return; + } + + 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]; + else + query = bm.ASTTrue; + + SOLVER_RETURN_TYPE last_result = GlobalSTP->TopLevelSTP(query, bm.ASTFalse); + + // Write in the answer to the current slot. + if (last_result ==SOLVER_SATISFIABLE || last_result ==SOLVER_UNSATISFIABLE) + { + Entry e(last_result); + e.node = assertionsSMT2.back()[0]; + cacheEntry = e; + assert (!cacheEntry.node.IsNull()); + } + + // It's satisfiable, so everything beneath it is satisfiable too. + if (last_result ==SOLVER_SATISFIABLE) + { + for (int i=0; i < cache.size(); i++) + { + assert(cache[i].result != SOLVER_UNSATISFIABLE); + cache[i].result = SOLVER_SATISFIABLE; + } + } + + if (bm.UserFlags.quick_statistics_flag) + { + bm.GetRunTimes()->print(); + } + + (GlobalSTP->tosat)->PrintOutput(last_result); + //printStatus(); + bm.GetRunTimes()->start(RunTimes::Parsing); + } + + void cleanUp() + { + letMgr.cleanupParserSymbolTable(); + cache.clear(); + symbols.clear(); + } }; } diff --git a/src/parser/smt2.lex b/src/parser/smt2.lex index e9cffb6..5765d2b 100644 --- a/src/parser/smt2.lex +++ b/src/parser/smt2.lex @@ -163,11 +163,14 @@ bv{DIGIT}+ { smt2lval.str = new std::string(smt2text+2); return BVCONST_DECIMAL_ "set-logic" { return LOGIC_TOK; } "set-info" { return NOTES_TOK; } "declare-fun" { return DECLARE_FUNCTION_TOK; } +"push" { return PUSH_TOK;} +"pop" { return POP_TOK;} + /* "set-option" "declare-sort" "define-sort" - "push" + "pop" */ "assert" { return FORMULA_TOK; } diff --git a/src/parser/smt2.y b/src/parser/smt2.y index 429b51a..cabc1f2 100644 --- a/src/parser/smt2.y +++ b/src/parser/smt2.y @@ -66,8 +66,8 @@ } ASTNode querysmt2; - ASTVec assertionsSMT2; - vector commands; + vector assertionsSMT2; + #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 104857600 #define YYERROR_VERBOSE 1 @@ -181,6 +181,8 @@ %token NOTES_TOK %token DECLARE_FUNCTION_TOK %token FORMULA_TOK +%token PUSH_TOK +%token POP_TOK /* Functions for QF_AUFBV. */ %token SELECT_TOK; @@ -191,21 +193,9 @@ %% cmd: commands END { - if(querysmt2.IsNull()) - { - querysmt2 = parserInterface->CreateNode(FALSE); - } - - if (assertionsSMT2.size() > 1) - ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(AND,assertionsSMT2)); - else if (assertionsSMT2.size() > 0) - ((ASTVec*)AssertsQuery)->push_back((assertionsSMT2[0])); - else - ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE)); - ((ASTVec*)AssertsQuery)->push_back(querysmt2); - parserInterface->letMgr.cleanupParserSymbolTable(); querysmt2 = ASTNode(); assertionsSMT2.clear(); + parserInterface->cleanUp(); YYACCEPT; } ; @@ -219,11 +209,14 @@ commands: cmdi commands cmdi: LPAREN_TOK EXIT_TOK RPAREN_TOK { - commands.push_back("exit"); + querysmt2 = ASTNode(); + assertionsSMT2.clear(); + parserInterface->cleanUp(); + YYACCEPT; } | LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK { - commands.push_back("check-sat"); + parserInterface->checkSat(assertionsSMT2); } | LPAREN_TOK LOGIC_TOK STRING_TOK RPAREN_TOK @@ -243,11 +236,27 @@ cmdi: {} | LPAREN_TOK NOTES_TOK attribute RPAREN_TOK {} +| LPAREN_TOK PUSH_TOK NUMERAL_TOK RPAREN_TOK + { + for (int i=0; i < $3;i++) + { + parserInterface->push(); + assertionsSMT2.push_back(ASTVec()); + } + } +| LPAREN_TOK POP_TOK NUMERAL_TOK RPAREN_TOK + { + for (int i=0; i < $3;i++) + { + parserInterface->pop(); + assertionsSMT2.erase(assertionsSMT2.end()-1); + } + } | LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK {} | LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK { - assertionsSMT2.push_back(*$3); + assertionsSMT2.back().push_back(*$3); parserInterface->deleteNode($3); } ; @@ -287,7 +296,7 @@ var_decl: STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK { ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); - parserInterface->letMgr._parser_symbol_table.insert(s); + parserInterface->addSymbol(s); //Sort_symbs has the indexwidth/valuewidth. Set those fields in //var s.SetIndexWidth(0); @@ -299,13 +308,13 @@ STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TO ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); s.SetIndexWidth(0); s.SetValueWidth(0); - parserInterface->letMgr._parser_symbol_table.insert(s); + parserInterface->addSymbol(s); delete $1; } | STRING_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK ARRAY_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK RPAREN_TOK { ASTNode s = BEEV::parserInterface->LookupOrCreateSymbol($1->c_str()); - parserInterface->letMgr._parser_symbol_table.insert(s); + parserInterface->addSymbol(s); unsigned int index_len = $9; unsigned int value_len = $14; if(index_len > 0) { -- 2.47.3