From 3340b6be7a24bbce13c36b4b953202a3495a24ec Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 21 Jul 2009 05:20:44 +0000 Subject: [PATCH] * In SMTLIB parsing mode, warn if the expected and actual satisfiability differ. * Fixed a memory leak in ClearTables(), ClearCaches(). * Added back the "if_then_else" token which some SMTLIB benchmarks rely on * Removed unnecessary tokens from the lexer. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@83 e59a4935-1847-0410-ae03-e826735625c1 --- AST/AST.cpp | 8 ++++++++ AST/ASTUtil.h | 10 ++++++++++ AST/ToSAT.cpp | 15 +++++++++++++++ parser/main.cpp | 16 ++++++++++------ parser/smtlib.lex | 13 ++++++------- parser/smtlib.y | 18 ++++++++++++++---- 6 files changed, 63 insertions(+), 17 deletions(-) diff --git a/AST/AST.cpp b/AST/AST.cpp index 1b7b705..6f7c6e5 100644 --- a/AST/AST.cpp +++ b/AST/AST.cpp @@ -58,6 +58,12 @@ namespace BEEV { //print the input back bool print_STPinput_back = false; + enum BEEV::inputStatus input_status = NOT_DECLARED; + + // Used only in smtlib lexer/parser + ASTNode SingleBitOne; + ASTNode SingleBitZero; + //global BEEVMGR for the parser BeevMgr * globalBeevMgr_for_parser; @@ -1497,6 +1503,7 @@ namespace BEEV { for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { (it->second)->clear(); + delete (it->second); } _ASTNode_to_Bitvector.clear(); @@ -1556,6 +1563,7 @@ namespace BEEV { for(ASTtoBitvectorMap::iterator it=_ASTNode_to_Bitvector.begin(), itend=_ASTNode_to_Bitvector.end();it!=itend;it++) { (it->second)->clear(); + delete (it->second); } _ASTNode_to_Bitvector.clear(); diff --git a/AST/ASTUtil.h b/AST/ASTUtil.h index 9ae4255..1693847 100644 --- a/AST/ASTUtil.h +++ b/AST/ASTUtil.h @@ -77,6 +77,16 @@ namespace BEEV { //print the input back extern bool print_STPinput_back; + enum inputStatus + { + NOT_DECLARED =0, // Not included in the input file / stream + TO_BE_SATISFIABLE, + TO_BE_UNSATISFIABLE, + TO_BE_UNKNOWN // Specified in the input file as unknown. + }; + + extern enum inputStatus input_status; + extern void (*vc_error_hdlr)(const char* err_msg); /*Spacer class is basically just an int, but the new class allows overloading of << with a special definition that prints the int as diff --git a/AST/ToSAT.cpp b/AST/ToSAT.cpp index 3a73fc8..af3f0b4 100644 --- a/AST/ToSAT.cpp +++ b/AST/ToSAT.cpp @@ -1424,6 +1424,21 @@ namespace BEEV { //This function prints the output of the STP solver void BeevMgr::PrintOutput(bool true_iff_valid) { //self-explanatory + if(print_output) { + if(smtlib_parser_enable) + { + 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)) + { + cerr << "Warning. Expected unsatisfiable, FOUND satisfiable" << endl; + } + } + } + if(true_iff_valid) { ValidFlag = true; if(print_output) { diff --git a/parser/main.cpp b/parser/main.cpp index 547b9df..93a9370 100644 --- a/parser/main.cpp +++ b/parser/main.cpp @@ -33,6 +33,14 @@ extern int smtparse(); extern int cvcparse(); +namespace BEEV +{ +extern BEEV::ASTNode SingleBitOne; +extern BEEV::ASTNode SingleBitZero; +} + + + /* GLOBAL VARS: Some global vars for the Main function. * */ @@ -44,10 +52,6 @@ std::string helpstring = "\n\n"; // Amount of memory to ask for at beginning of main. static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; -// Used only in smtlib lexer/parser -BEEV::ASTNode SingleBitOne; -BEEV::ASTNode SingleBitZero; - /****************************************************************************** * MAIN FUNCTION: * @@ -205,8 +209,8 @@ int main(int argc, char ** argv) { BEEV::print_output = true; BEEV::globalBeevMgr_for_parser = new BEEV::BeevMgr(); - SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); - SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); + BEEV::SingleBitOne = BEEV::globalBeevMgr_for_parser->CreateOneConst(1); + BEEV::SingleBitZero = BEEV::globalBeevMgr_for_parser->CreateZeroConst(1); //BEEV::smtlib_parser_enable = true; if (smtlibParser) diff --git a/parser/smtlib.lex b/parser/smtlib.lex index a045e1f..c33682a 100644 --- a/parser/smtlib.lex +++ b/parser/smtlib.lex @@ -51,8 +51,11 @@ } } +namespace BEEV +{ extern BEEV::ASTNode SingleBitOne; extern BEEV::ASTNode SingleBitZero; + } /* Changed for smtlib speedup */ /* bv{DIGIT}+ { smtlval.node = new BEEV::ASTNode(BEEV::_bm->CreateBVConst(smttext+2, 10)); return BVCONST_TOK;} */ @@ -84,10 +87,10 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) bit{DIGIT}+ { char c = smttext[3]; if (c == '1') { - smtlval.node = new BEEV::ASTNode(SingleBitOne); + smtlval.node = new BEEV::ASTNode(BEEV::SingleBitOne); } else { - smtlval.node = new BEEV::ASTNode(SingleBitZero); + smtlval.node = new BEEV::ASTNode(BEEV::SingleBitZero); } return BITCONST_TOK; }; @@ -128,6 +131,7 @@ bit{DIGIT}+ { "not" { return NOT_TOK; } "implies" { return IMPLIES_TOK; } "ite" { return ITE_TOK;} +"if_then_else" { return ITE_TOK;} // This is in the SMTLIB benchmarks. "and" { return AND_TOK; } "or" { return OR_TOK; } "xor" { return XOR_TOK; } @@ -135,7 +139,6 @@ bit{DIGIT}+ { "let" { return LET_TOK; } "flet" { return FLET_TOK; } "notes" { return NOTES_TOK; } -"cvc_command" { return CVC_COMMAND_TOK; } "sorts" { return SORTS_TOK; } "funs" { return FUNS_TOK; } "preds" { return PREDS_TOK; } @@ -171,11 +174,7 @@ bit{DIGIT}+ { "nand" { return NAND_TOK;} "nor" { return NOR_TOK;} -"/=" { return NEQ_TOK; } - ":=" { return ASSIGN_TOK;} -"shift_left0" { return BVLEFTSHIFT_TOK;} "bvshl" { return BVLEFTSHIFT_1_TOK;} -"shift_right0" { return BVRIGHTSHIFT_TOK;} "bvlshr" { return BVRIGHTSHIFT_1_TOK;} "bvashr" { return BVARITHRIGHTSHIFT_TOK;} "bvadd" { return BVPLUS_TOK;} diff --git a/parser/smtlib.y b/parser/smtlib.y index ad49743..8a5dd65 100644 --- a/parser/smtlib.y +++ b/parser/smtlib.y @@ -322,10 +322,20 @@ logic_name: ; status: - SAT_TOK { $$ = NULL; } - | UNSAT_TOK { $$ = NULL; } - | UNKNOWN_TOK { $$ = NULL; } -; + SAT_TOK { + BEEV::input_status = BEEV::TO_BE_SATISFIABLE; + $$ = NULL; + } + | UNSAT_TOK { + BEEV::input_status = BEEV::TO_BE_UNSATISFIABLE; + $$ = NULL; + } + | UNKNOWN_TOK + { + BEEV::input_status = BEEV::TO_BE_UNKNOWN; + $$ = NULL; + } + ; /* annotations: */ -- 2.47.3