From: trevor_hansen Date: Fri, 21 May 2010 15:55:33 +0000 (+0000) Subject: An initial version of an smtlib2 format parser. It has these problems: X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c220bc350564955d73af2645d4dcbe470ec242d0;p=francis%2Fstp.git An initial version of an smtlib2 format parser. It has these problems: * Leaks memory * Doesn't allow for annotations on terms. * Ignores the commands sent to it. It just solves the problem specified. Other changes: * Long options are no longer case senstive. * If the input file ends with .smt2 or .smt the appropriate parser is selected. * The simplifying node factory is disabled during parsing when printing back is enabled. This allows STP to be used as a better, but still low-fidelity translator between formats. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@774 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index 672759e..85e0e5a 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -88,7 +88,7 @@ namespace BEEV //print the input back bool print_STPinput_back_flag; bool print_STPinput_back_C_flag; - bool print_STPinput_back_SMTLIB_flag; + bool print_STPinput_back_SMTLIB2_flag; bool print_STPinput_back_SMTLIB1_flag; bool print_STPinput_back_CVC_flag; bool print_STPinput_back_dot_flag; @@ -99,7 +99,8 @@ namespace BEEV bool output_bench_flag; //Flag to switch on the smtlib parser - bool smtlib_parser_flag; + bool smtlib1_parser_flag; + bool smtlib2_parser_flag; bool division_by_zero_returns_one_flag; @@ -188,12 +189,13 @@ namespace BEEV xor_flatten_flag = false; //Flag to switch on the smtlib parser - smtlib_parser_flag = false; + smtlib1_parser_flag = false; + smtlib2_parser_flag = false; //print the input back print_STPinput_back_flag = false; print_STPinput_back_C_flag = false; - print_STPinput_back_SMTLIB_flag = false; + print_STPinput_back_SMTLIB2_flag = false; print_STPinput_back_SMTLIB1_flag = false; print_STPinput_back_CVC_flag = false; print_STPinput_back_GDL_flag = false; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index f1bc9f7..28ee921 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -105,7 +105,7 @@ void vc_setFlags(VC vc, char c, int param_value) { b->UserFlags.print_output_flag = true; break; case 'm': - b->UserFlags.smtlib_parser_flag=true; + b->UserFlags.smtlib1_parser_flag=true; b->UserFlags.division_by_zero_returns_one_flag = true; break; case 'p': @@ -1766,7 +1766,7 @@ Expr vc_parseExpr(VC vc, const char* infile) { BEEV::ASTVec * AssertsQuery = new BEEV::ASTVec; - if (b->UserFlags.smtlib_parser_flag) + if (b->UserFlags.smtlib1_parser_flag) { smtin = cvcin; cvcin = NULL; @@ -1998,7 +1998,7 @@ int vc_parseMemExpr(VC vc, const char* s, Expr* oquery, Expr* oasserts ) { BEEV::parserInterface = π BEEV::ASTVec AssertsQuery; - if (b->UserFlags.smtlib_parser_flag) + if (b->UserFlags.smtlib1_parser_flag) { //YY_BUFFER_STATE bstat = smt_scan_string(s); //smt_switch_to_buffer(bstat); diff --git a/src/main/main.cpp b/src/main/main.cpp index b1f73f3..c6a4c44 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -23,9 +23,11 @@ using namespace __gnu_cxx; using namespace BEEV; extern int smtparse(void*); +extern int smt2parse(void*); extern int cvcparse(void*); extern int cvclex_destroy(void); extern int smtlex_destroy(void); +extern int smt2lex_destroy(void); // callback for SIGALRM. void handle_time_out(int parameter){ @@ -36,6 +38,16 @@ void handle_time_out(int parameter){ bool onePrintBack =false; +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; +} + + + // Amount of memory to ask for at beginning of main. static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; /******************************************************************** @@ -49,12 +61,13 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; * step 5. Call SAT to determine if input is SAT or UNSAT ********************************************************************/ -typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType; +typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB2,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER, SMT_LIB2_FORMAT, SMT_LIB1_FORMAT} OptionType; int main(int argc, char ** argv) { - char * infile; + char * infile = NULL; extern FILE *cvcin; extern FILE *smtin; + extern FILE *smt2in; // Grab some memory from the OS upfront to reduce system time when // individual hash tables are being allocated @@ -106,7 +119,7 @@ int main(int argc, char ** argv) { helpstring += "-j : CNF Dumping. Creates a DIMACS equivalent file of the input STP file\n"; helpstring += - "-m : use the SMTLIB parser\n"; + "-m : use the SMTLIB1 parser\n"; helpstring += "--output-CNF : save the CNF into output.cnf\n"; helpstring += "--output-bench : save in ABC's bench format to output.bench\n"; @@ -119,7 +132,7 @@ int main(int argc, char ** argv) { helpstring += "--print-back-CVC : print input in CVC format, then exit\n"; helpstring += - "--print-back-SMTLIB : print input in SMT-LIB2 format, then exit\n"; + "--print-back-SMTLIB2 : print input in SMT-LIB2 format, then exit\n"; helpstring += "--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n"; helpstring += @@ -130,12 +143,14 @@ int main(int argc, char ** argv) { "-r : switch refinement off (optimizations are ON by default)\n"; helpstring += "-s : print function statistics\n"; - - #if !defined CRYPTOMINISAT2 +#if !defined CRYPTOMINISAT2 +helpstring += + "--simplifying-minisat : use simplifying-minisat rather than minisat\n"; +#endif helpstring += - "--simplifying-minisat : use simplifying-minisat rather than minisat\n"; - #endif - + "--SMTLIB1 : use the SMT-LIB1 format parser\n"; + helpstring += + "--SMTLIB2 : use the SMT-LIB2 format parser\n"; helpstring += "-t : print quick statistics\n"; helpstring += @@ -155,18 +170,19 @@ int main(int argc, char ** argv) { { // long options. map lookup; - lookup.insert(make_pair("--print-back-C",PRINT_BACK_C)); - lookup.insert(make_pair("--print-back-CVC",PRINT_BACK_CVC)); - lookup.insert(make_pair("--print-back-SMTLIB",PRINT_BACK_SMTLIB)); - lookup.insert(make_pair("--print-back-SMTLIB1",PRINT_BACK_SMTLIB1)); - lookup.insert(make_pair("--print-back-GDL",PRINT_BACK_GDL)); - lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT)); - lookup.insert(make_pair("--output-CNF",OUTPUT_CNF)); - lookup.insert(make_pair("--output-bench",OUTPUT_BENCH)); - lookup.insert(make_pair("--simplifying-minisat",USE_SIMPLIFYING_SOLVER)); - - - switch(lookup[argv[i]]) + lookup.insert(make_pair(tolower("--print-back-C"),PRINT_BACK_C)); + lookup.insert(make_pair(tolower("--print-back-CVC"),PRINT_BACK_CVC)); + lookup.insert(make_pair(tolower("--print-back-SMTLIB2"),PRINT_BACK_SMTLIB2)); + lookup.insert(make_pair(tolower("--print-back-SMTLIB1"),PRINT_BACK_SMTLIB1)); + lookup.insert(make_pair(tolower("--print-back-GDL"),PRINT_BACK_GDL)); + lookup.insert(make_pair(tolower("--print-back-dot"),PRINT_BACK_DOT)); + lookup.insert(make_pair(tolower("--output-CNF"),OUTPUT_CNF)); + lookup.insert(make_pair(tolower("--output-bench"),OUTPUT_BENCH)); + lookup.insert(make_pair(tolower("--simplifying-minisat"),USE_SIMPLIFYING_SOLVER)); + lookup.insert(make_pair(tolower("--SMTLIB2"),SMT_LIB2_FORMAT)); + lookup.insert(make_pair(tolower("--SMTLIB1"),SMT_LIB1_FORMAT)); + + switch(lookup[tolower(argv[i])]) { case PRINT_BACK_C: bm->UserFlags.print_STPinput_back_C_flag = true; @@ -176,8 +192,8 @@ int main(int argc, char ** argv) { bm->UserFlags.print_STPinput_back_CVC_flag = true; onePrintBack = true; break; - case PRINT_BACK_SMTLIB: - bm->UserFlags.print_STPinput_back_SMTLIB_flag = true; + case PRINT_BACK_SMTLIB2: + bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true; onePrintBack = true; break; case PRINT_BACK_SMTLIB1: @@ -199,6 +215,19 @@ int main(int argc, char ** argv) { case OUTPUT_BENCH: bm->UserFlags.output_bench_flag = true; break; + case SMT_LIB2_FORMAT: + bm->UserFlags.smtlib2_parser_flag = true; + bm->UserFlags.division_by_zero_returns_one_flag = true; + if (bm->UserFlags.smtlib1_parser_flag) + FatalError("Can't use both the smtlib and smtlib2 parsers"); + break; + case SMT_LIB1_FORMAT: + bm->UserFlags.smtlib1_parser_flag = true; + bm->UserFlags.division_by_zero_returns_one_flag = true; + if (bm->UserFlags.smtlib2_parser_flag) + FatalError("Can't use both the smtlib and smtlib2 parsers"); + break; + #if !defined CRYPTOMINISAT && !defined CRYPTOMINISAT2 case USE_SIMPLIFYING_SOLVER: @@ -275,12 +304,15 @@ int main(int argc, char ** argv) { bm->UserFlags.print_cnf_flag = true; bm->UserFlags.cnf_dump_filename = argv[++i]; break; - case 'n': - bm->UserFlags.print_output_flag = true; - break; case 'm': - bm->UserFlags.smtlib_parser_flag=true; + bm->UserFlags.smtlib1_parser_flag=true; bm->UserFlags.division_by_zero_returns_one_flag = true; + if (bm->UserFlags.smtlib2_parser_flag) + FatalError("Can't use both the smtlib and smtlib2 parsers"); + + break; + case 'n': + bm->UserFlags.print_output_flag = true; break; case 'p': bm->UserFlags.print_counterexample_flag = true; @@ -324,27 +356,62 @@ int main(int argc, char ** argv) { } } } else { - infile = argv[i]; - if (bm->UserFlags.smtlib_parser_flag) - { - smtin = fopen(infile,"r"); - if(smtin == NULL) - { - fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); - FatalError(""); - } - } - else + if (NULL != infile) + FatalError("One input file only."); + infile = argv[i]; + } + } + + if (!bm->UserFlags.smtlib1_parser_flag && !bm->UserFlags.smtlib2_parser_flag) + { + // No parser is explicity requested. + if (NULL != infile && strlen(infile)>=5) + { + string f(infile); + if (!f.compare(f.length()-4, 4,".smt")) + { + bm->UserFlags.smtlib1_parser_flag = true; + } + if (!f.compare(f.length()-5, 5,".smt2")) + { + bm->UserFlags.smtlib2_parser_flag = true; + } + } + } + + // If we're not reading the file from stdin. + if (infile != NULL) + { + if (bm->UserFlags.smtlib1_parser_flag) + { + smtin = fopen(infile,"r"); + if(smtin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + FatalError(""); + } + } else + if (bm->UserFlags.smtlib2_parser_flag) { - cvcin = fopen(infile,"r"); - if(cvcin == NULL) + smt2in = fopen(infile,"r"); + if(smt2in == NULL) { fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); FatalError(""); } } - } + + else + { + cvcin = fopen(infile,"r"); + if(cvcin == NULL) + { + fprintf(stderr,"%s: Error: cannot open %s\n",prog,infile); + FatalError(""); + } } + } + //want to print the output always from the commandline. bm->UserFlags.print_output_flag = true; @@ -357,17 +424,28 @@ int main(int argc, char ** argv) { bm->GetRunTimes()->start(RunTimes::Parsing); { - // Wrap a typchecking node factory around the default node factory. - // Every node created is typechecked. - SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory, *bm); - TypeChecker nf(simpNF, *bm); + SimplifyingNodeFactory simpNF(*bm->defaultNodeFactory, *bm); + TypeChecker nfTypeCheckSimp(simpNF, *bm); + TypeChecker nfTypeCheckDefault(*bm->defaultNodeFactory, *bm); + + ParserInterface piTypeCheckSimp(*bm, &nfTypeCheckSimp); + ParserInterface piTypeCheckDefault(*bm, &nfTypeCheckDefault); + + // If you are converting formats, you probably don't want it simplifying (at least I dont). + if (false && onePrintBack) + { + parserInterface = &piTypeCheckDefault; + } + else + parserInterface = &piTypeCheckSimp; - ParserInterface pi(*bm, &nf); - parserInterface = π - if (bm->UserFlags.smtlib_parser_flag) { + if (bm->UserFlags.smtlib1_parser_flag) { smtparse((void*) AssertsQuery); smtlex_destroy(); + } else if (bm->UserFlags.smtlib2_parser_flag) { + smt2parse((void*) AssertsQuery); + smt2lex_destroy(); } else { cvcparse((void*) AssertsQuery); cvclex_destroy(); @@ -399,8 +477,8 @@ int main(int argc, char ** argv) { if(bm->UserFlags.print_STPinput_back_flag) { - if(bm->UserFlags.smtlib_parser_flag) - bm->UserFlags.print_STPinput_back_SMTLIB_flag = true; + if(bm->UserFlags.smtlib1_parser_flag) + bm->UserFlags.print_STPinput_back_SMTLIB2_flag = true; else bm->UserFlags.print_STPinput_back_CVC_flag = true; } @@ -416,7 +494,7 @@ int main(int argc, char ** argv) { printer::SMTLIB1_PrintBack(cout, original_input); } - if (bm->UserFlags.print_STPinput_back_SMTLIB_flag) + if (bm->UserFlags.print_STPinput_back_SMTLIB2_flag) { printer::SMTLIB2_PrintBack(cout, original_input); } diff --git a/src/parser/.PL.y.swp b/src/parser/.PL.y.swp deleted file mode 100644 index 026355a..0000000 Binary files a/src/parser/.PL.y.swp and /dev/null differ diff --git a/src/parser/.parsePL.cpp.swp b/src/parser/.parsePL.cpp.swp deleted file mode 100644 index 6afa034..0000000 Binary files a/src/parser/.parsePL.cpp.swp and /dev/null differ diff --git a/src/parser/LetMgr.cpp b/src/parser/LetMgr.cpp index c9f75fc..614fd19 100644 --- a/src/parser/LetMgr.cpp +++ b/src/parser/LetMgr.cpp @@ -80,7 +80,7 @@ namespace BEEV { // I don't know what this does. Commenting it out and all the regression // tests still pass. -#if 0 +//#if 0 ASTNodeMap::iterator it = _letid_expr_map->begin(); ASTNodeMap::iterator itend = _letid_expr_map->end(); for(;it!=itend;it++) { @@ -89,7 +89,7 @@ namespace BEEV { it->first.SetIndexWidth(0); } } -#endif +//#endif // May contain lots of buckets, so reset. delete _letid_expr_map; diff --git a/src/parser/Makefile b/src/parser/Makefile index e4c6c12..f68807f 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -4,7 +4,7 @@ include $(TOP)/scripts/Makefile.common LEX=flex YACC=bison -d -y --debug -v -SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp LetMgr.cpp +SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp LetMgr.cpp parse2SMT.cpp lex2SMT.cpp OBJS = $(SRCS:.cpp=.o) LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) @@ -34,6 +34,15 @@ parseSM%_defs.h parseSM%.cpp:smtlib.y @cp smt.tab.c parseSMT.cpp @cp smt.tab.h parseSMT_defs.h +lex2SMT.cpp: parseSMT2_defs.h smtlib2.lex ../AST/AST.h + $(LEX) -olex2SMT.cpp -Psmt2 smtlib2.lex + +parse2SM%_defs.h parse2SM%.cpp:smtlib2.y + $(YACC) -o smt2.tab.c -p smt2 smtlib2.y + @cp smt2.tab.c parse2SMT.cpp + @cp smt2.tab.h parse2SMT_defs.h + + clean: - rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* cvc.tab.* lex.yy.c libparser.a .#* + rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* smt2.tab.* cvc.tab.* lex.yy.c libparser.a parse2SMT.cpp parse2SMT_defs.h lex2SMT.cpp .#* diff --git a/src/parser/smtlib2.lex b/src/parser/smtlib2.lex new file mode 100644 index 0000000..0021155 --- /dev/null +++ b/src/parser/smtlib2.lex @@ -0,0 +1,269 @@ +%{ + /******************************************************************** + * AUTHORS: Trevor Hansen, Vijay Ganesh, David L. Dill + * + * BEGIN DATE: July, 2006 + * + * This file is modified version of the CVCL's smtlib.lex file. Please + * see CVCL license below + ********************************************************************/ + + /******************************************************************** + * \file smtlib.lex + * + * Author: Sergey Berezin, Clark Barrett + * + * Created: Apr 30 2005 + * + *
+ * Copyright (C) 2004 by the Board of Trustees of Leland Stanford + * Junior University and by New York University. + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. In particular: + * + * - The above copyright notice and this permission notice must appear + * in all copies of the software and related documentation. + * + * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, + * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. + * + *
+ ********************************************************************/ + // -*- c++ -*-L +#include +#include "parser.h" +#include "parse2SMT_defs.h" +#include "ParserInterface.h" + + using namespace std; + using namespace BEEV; + + extern char *smt2text; + extern int smt2error (const char *msg); + + // File-static (local to this file) variables and functions + static std::string _string_lit; + static char escapeChar(char c) { + switch(c) { + case 'n': return '\n'; + case 't': return '\t'; + default: return c; + } + } +%} + +%option noyywrap +%option nounput +%option noreject +%option noyymore +%option yylineno + +%x COMMENT +%x STRING_LITERAL +%x USER_VALUE + +LETTER ([a-zA-Z]) +DIGIT ([0-9]) +OPCHAR (['\.\_]) +ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) + +%% +[ \n\t\r\f] { /* sk'ip whitespace */ } +{DIGIT}+ { smt2lval.uintval = strtoul(smt2text, NULL, 10); return NUMERAL_TOK; } + + + bv{DIGIT}+ { smt2lval.str = new std::string(smt2text+2); return BVCONST_TOK; } + +bit{DIGIT}+ { + char c = smt2text[3]; + if (c == '1') { + smt2lval.node = new BEEV::ASTNode(parserInterface->CreateOneConst(1)); + } + else { + smt2lval.node = new BEEV::ASTNode(parserInterface->CreateZeroConst(1)); + } + return BITCONST_TOK; + }; + + +";" { BEGIN COMMENT; } +"\n" { BEGIN INITIAL; /* return to normal mode */} +. { /* stay in comment mode */ } + +"\"" { BEGIN STRING_LITERAL; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +"\\". { /* escape characters (like \n or \") */ + _string_lit.insert(_string_lit.end(), + escapeChar(smt2text[1])); } + + "\"" { BEGIN INITIAL; + smt2lval.str = new std::string(_string_lit); + return STRING_TOK; } + +. { _string_lit.insert(_string_lit.end(),*smt2text); } + +"|" { BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } +"|" { BEGIN INITIAL; /* return to normal mode */ + smt2lval.str = new std::string(_string_lit); + return USER_VAL_TOK; } +"\n" { _string_lit.insert(_string_lit.end(),'\n');} +. { _string_lit.insert(_string_lit.end(),*smt2text); } + + + /* + "{" { BEGIN USER_VALUE; + _string_lit.erase(_string_lit.begin(), + _string_lit.end()); } + "\\"[{}] { + _string_lit.insert(_string_lit.end(),smt2text[1]); } + + "}" { BEGIN INITIAL; + smt2lval.str = new std::string(_string_lit); + return USER_VAL_TOK; } + "\n" { _string_lit.insert(_string_lit.end(),'\n');} + . { _string_lit.insert(_string_lit.end(),*smt2text); } +*/ + +"notes" { return NOTES_TOK; } +"sorts" { return SORTS_TOK; } +"funs" { return FUNS_TOK; } +"preds" { return PREDS_TOK; } +"extensions" { return EXTENSIONS_TOK; } +"definition" { return DEFINITION_TOK; } +"axioms" { return AXIOMS_TOK; } +"sat" { return SAT_TOK; } +"unsat" { return UNSAT_TOK; } +"unknown" { return UNKNOWN_TOK; } +"assumption" { return ASSUMPTION_TOK; } +"status" { return STATUS_TOK; } + +"benchmark" { return BENCHMARK_TOK; } +"extrasorts" { return EXTRASORTS_TOK; } +"extrapreds" { return EXTRAPREDS_TOK; } +"language" { return LANGUAGE_TOK; } +":" { return COLON_TOK; } +"\[" { return LBRACKET_TOK; } +"\]" { return RBRACKET_TOK; } +"(" { return LPAREN_TOK; } +")" { return RPAREN_TOK; } +"$" { return DOLLAR_TOK; } +"?" { return QUESTION_TOK; } +"_" { return UNDERSCORE_TOK; } +"\|" { return PIPE_TOK; } +"." { return DOT_TOK; } + + /* Set info types */ +"source" { return SOURCE_TOK;} +"category" { return CATEGORY_TOK;} +"difficulty" { return DIFFICULTY_TOK; } +"smt-lib-version" { return VERSION_TOK; } + + /* COMMANDS */ +"set-logic" { return LOGIC_TOK; } +"set-info" { return NOTES_TOK; } +"declare-fun" { return DECLARE_FUNCTION_TOK; } + /* + "set-option" + "declare-sort" + "define-sort" + "push" + "pop" +*/ +"assert" { return FORMULA_TOK; } +"check-sat" { return CHECK_SAT_TOK; } + /* + "get-assertions" + "get-proof" + "get-unsat-core" + "get-value" + "get-assignment" + "get-option" + "get-info" +*/ +"exit" {return EXIT_TOK;} + + /* Types for QF_BV and QF_AUFBV. */ +"BitVec" { return BITVEC_TOK;} +"Array" { return ARRAY_TOK;} +"Bool" { return BOOL_TOK;} + + + /* CORE THEORY pg. 29 of the SMT-LIB2 standard 30-March-2010. */ +"true" { return TRUE_TOK; } +"false" { return FALSE_TOK; } +"not" { return NOT_TOK; } +"and" { return AND_TOK; } +"or" { return OR_TOK; } +"xor" { return XOR_TOK;} +"ite" { return ITE_TOK;} // PARAMETRIC +"=" { return EQ_TOK;} +"=>" { return IMPLIES_TOK; } + + /* CORE THEORY. But not on pg 29. */ +"distinct" { return DISTINCT_TOK; } // variadic +"let" { return LET_TOK; } + + /* Functions for QF_BV and QF_AUFBV. */ +"bvshl" { return BVLEFTSHIFT_1_TOK;} +"bvlshr" { return BVRIGHTSHIFT_1_TOK;} +"bvashr" { return BVARITHRIGHTSHIFT_TOK;} +"bvadd" { return BVPLUS_TOK;} +"bvsub" { return BVSUB_TOK;} +"bvnot" { return BVNOT_TOK;} +"bvmul" { return BVMULT_TOK;} +"bvudiv" { return BVDIV_TOK;} +"bvsdiv" { return SBVDIV_TOK;} +"bvurem" { return BVMOD_TOK;} +"bvsrem" { return SBVREM_TOK;} +"bvsmod" { return SBVMOD_TOK;} +"bvneg" { return BVNEG_TOK;} +"bvand" { return BVAND_TOK;} +"bvor" { return BVOR_TOK;} +"bvxor" { return BVXOR_TOK;} +"bvnand" { return BVNAND_TOK;} +"bvnor" { return BVNOR_TOK;} +"bvxnor" { return BVXNOR_TOK;} +"concat" { return BVCONCAT_TOK;} +"extract" { return BVEXTRACT_TOK;} +"bvult" { return BVLT_TOK;} +"bvugt" { return BVGT_TOK;} +"bvule" { return BVLE_TOK;} +"bvuge" { return BVGE_TOK;} +"bvslt" { return BVSLT_TOK;} +"bvsgt" { return BVSGT_TOK;} +"bvsle" { return BVSLE_TOK;} +"bvsge" { return BVSGE_TOK;} +"bvcomp" { return BVCOMP_TOK;} +"zero_extend" { return BVZX_TOK;} +"sign_extend" { return BVSX_TOK;} +"repeat" { return BVREPEAT_TOK;} +"rotate_left" { return BVROTATE_LEFT_TOK;} +"rotate_right" { return BVROTATE_RIGHT_TOK;} + + /* Functions for QF_AUFBV. */ +"select" { return SELECT_TOK; } +"store" { return STORE_TOK; } + + +(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { + BEEV::ASTNode nptr = parserInterface->CreateSymbol(smt2text); + + // Check valuesize to see if it's a prop var. I don't like doing + // type determination in the lexer, but it's easier than rewriting + // the whole grammar to eliminate the term/formula distinction. + smt2lval.node = new BEEV::ASTNode(parserInterface->letMgr.ResolveID(nptr)); + //smt2lval.node = new BEEV::ASTNode(nptr); + if ((smt2lval.node)->GetType() == BOOLEAN_TYPE) + return FORMID_TOK; + else + return TERMID_TOK; + +} +. { smt2error("Illegal input character."); } +%% diff --git a/src/parser/smtlib2.y b/src/parser/smtlib2.y new file mode 100644 index 0000000..b38b755 --- /dev/null +++ b/src/parser/smtlib2.y @@ -0,0 +1,1160 @@ +%{ + /******************************************************************** + * AUTHORS: Trevor Hansen, Vijay Ganesh + * + * BEGIN DATE: July, 2006 + * + * This file is modified version of the CVCL's smtlib.y file. Please + * see CVCL license below + ********************************************************************/ + + /******************************************************************** + * + * \file smtlib.y + * + * Author: Sergey Berezin, Clark Barrett + * + * Created: Apr 30 2005 + * + *
+ * Copyright (C) 2004 by the Board of Trustees of Leland Stanford + * Junior University and by New York University. + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. In particular: + * + * - The above copyright notice and this permission notice must appear + * in all copies of the software and related documentation. + * + * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, + * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. + * + *
+ ********************************************************************/ + // -*- c++ -*- + +#include "ParserInterface.h" + + using namespace std; + using namespace BEEV; + + // Suppress the bogus warning suppression in bison (it generates + // compile error) +#undef __GNUC_MINOR__ + + extern char* smt2text; + extern int smt2lineno; + extern int smt2lex(void); + + int yyerror(const char *s) { + cout << "syntax error: line " << smt2lineno << "\n" << s << endl; + cout << " token: " << smt2text << endl; + FatalError(""); + return 1; + } + + ASTNode querysmt2; + ASTVec assertionsSMT2; + vector commands; +#define YYLTYPE_IS_TRIVIAL 1 +#define YYMAXDEPTH 104857600 +#define YYERROR_VERBOSE 1 +#define YY_EXIT_FAILURE -1 +#define YYPARSE_PARAM AssertsQuery + %} + +%union { + // FIXME: Why is this not an UNSIGNED int? + int uintval; /* for numerals in types. */ + + // for BV32 BVCONST + unsigned long long ullval; + + struct { + //stores the indexwidth and valuewidth + //indexwidth is 0 iff type is bitvector. positive iff type is + //array, and stores the width of the indexing bitvector + unsigned int indexwidth; + //width of the bitvector type + unsigned int valuewidth; + } indexvaluewidth; + + //ASTNode,ASTVec + BEEV::ASTNode *node; + BEEV::ASTVec *vec; + std::string *str; +}; + +%start cmd + +%type sort_symb sort_symbs +%type status +%type bench_attributes an_formulas an_terms + +%type benchmark bench_name bench_attribute +%type an_term an_nonbvconst_term an_formula + +%type var fvar logic_name +%type user_value + +%token NUMERAL_TOK +%token BVCONST_TOK +%token BITCONST_TOK +%token FORMID_TOK TERMID_TOK +%token STRING_TOK +%token USER_VAL_TOK + + /* set-info tokens */ +%token SOURCE_TOK +%token CATEGORY_TOK +%token DIFFICULTY_TOK +%token VERSION_TOK + + +%token NOTES_TOK +%token CVC_COMMAND_TOK +%token SORTS_TOK +%token FUNS_TOK +%token PREDS_TOK +%token EXTENSIONS_TOK +%token DEFINITION_TOK +%token AXIOMS_TOK +%token LOGIC_TOK +%token ASSUMPTION_TOK +%token FORMULA_TOK +%token STATUS_TOK +%token BENCHMARK_TOK +%token EXTRASORTS_TOK +%token DECLARE_FUNCTION_TOK +%token EXTRAPREDS_TOK +%token LANGUAGE_TOK + + /* ASCII Symbols */ +%token DOLLAR_TOK +%token QUESTION_TOK +%token SEMICOLON_TOK +%token UNDERSCORE_TOK +%token PIPE_TOK +%token DOT_TOK +%token COLON_TOK +%token LBRACKET_TOK +%token RBRACKET_TOK +%token LPAREN_TOK +%token RPAREN_TOK + + /* Status */ +%token SAT_TOK +%token UNSAT_TOK +%token UNKNOWN_TOK + + /*BV SPECIFIC TOKENS*/ +%token BVLEFTSHIFT_1_TOK +%token BVRIGHTSHIFT_1_TOK +%token BVARITHRIGHTSHIFT_TOK +%token BVPLUS_TOK +%token BVSUB_TOK +%token BVNOT_TOK //bvneg in CVCL +%token BVMULT_TOK +%token BVDIV_TOK +%token SBVDIV_TOK +%token BVMOD_TOK +%token SBVREM_TOK +%token SBVMOD_TOK +%token BVNEG_TOK //bvuminus in CVCL +%token BVAND_TOK +%token BVOR_TOK +%token BVXOR_TOK +%token BVNAND_TOK +%token BVNOR_TOK +%token BVXNOR_TOK +%token BVCONCAT_TOK +%token BVLT_TOK +%token BVGT_TOK +%token BVLE_TOK +%token BVGE_TOK +%token BVSLT_TOK +%token BVSGT_TOK +%token BVSLE_TOK +%token BVSGE_TOK + +%token BVSX_TOK +%token BVEXTRACT_TOK +%token BVZX_TOK +%token BVROTATE_RIGHT_TOK +%token BVROTATE_LEFT_TOK +%token BVREPEAT_TOK +%token BVCOMP_TOK + + /* Types for QF_BV and QF_AUFBV. */ +%token BITVEC_TOK +%token ARRAY_TOK +%token BOOL_TOK + +/* CORE THEORY pg. 29 of the SMT-LIB2 standard 30-March-2010. */ +%token TRUE_TOK; +%token FALSE_TOK; +%token NOT_TOK; +%token AND_TOK; +%token OR_TOK; +%token XOR_TOK; +%token ITE_TOK; +%token EQ_TOK; +%token IMPLIES_TOK; + + /* CORE THEORY. But not on pg 29. */ +%token DISTINCT_TOK; +%token LET_TOK; + +// COMMANDS +%token EXIT_TOK +%token CHECK_SAT_TOK + +%left LBRACKET_TOK RBRACKET_TOK + + /* Functions for QF_AUFBV. */ +%token SELECT_TOK; +%token STORE_TOK; + + +%% +cmd: commands +{ + if(querysmt2.IsNull()) + { + querysmt2 = parserInterface->CreateNode(FALSE); + } + + ((ASTVec*)AssertsQuery)->push_back(parserInterface->nf->CreateNode(AND,assertionsSMT2)); + ((ASTVec*)AssertsQuery)->push_back(querysmt2); + parserInterface->letMgr.cleanupParserSymbolTable(); + YYACCEPT; +} +; + + +commands: cmdi commands +| cmdi +{} +; + +cmdi: + LPAREN_TOK EXIT_TOK RPAREN_TOK + { + commands.push_back("exit"); + } +| LPAREN_TOK CHECK_SAT_TOK RPAREN_TOK + { + commands.push_back("check-sat"); + } +| + LPAREN_TOK LOGIC_TOK logic_name RPAREN_TOK + { + if (!(0 == strcmp($3->GetName(),"QF_BV") || + 0 == strcmp($3->GetName(),"QF_AUFBV"))) { + yyerror("Wrong input logic:"); + } + delete $3; + } +| LPAREN_TOK NOTES_TOK attribute user_value RPAREN_TOK + {} +| LPAREN_TOK NOTES_TOK attribute FORMID_TOK RPAREN_TOK + {} +| LPAREN_TOK NOTES_TOK attribute NUMERAL_TOK DOT_TOK NUMERAL_TOK RPAREN_TOK + {} +| LPAREN_TOK NOTES_TOK attribute STRING_TOK RPAREN_TOK + {} +| LPAREN_TOK NOTES_TOK attribute RPAREN_TOK + {} +| LPAREN_TOK DECLARE_FUNCTION_TOK var_decl RPAREN_TOK + {} +| LPAREN_TOK FORMULA_TOK an_formula RPAREN_TOK + { + assertionsSMT2.push_back(*$3); + } +| +benchmark +{ + ASTNode assumptions; + if($1 == NULL) + { + assumptions = parserInterface->CreateNode(TRUE); + } + else + { + assumptions = *$1; + } +} +; + +benchmark: +LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK +{ + if($4 != NULL){ + if($4->size() > 1) + $$ = new ASTNode(parserInterface->nf->CreateNode(AND,*$4)); + else + $$ = new ASTNode((*$4)[0]); + delete $4; + } + else { + $$ = NULL; + } + delete $3; //discard the benchmarkname. +} +; + +bench_name: +FORMID_TOK +{ +} +; + +bench_attributes: +bench_attribute +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + parserInterface->AddAssert(*$1); + delete $1; + } +} +| bench_attributes bench_attribute +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + parserInterface->AddAssert(*$2); + $$ = $1; + delete $2; + } +} +; + +bench_attribute: +COLON_TOK ASSUMPTION_TOK an_formula +{ + //assumptions are like asserts + $$ = $3; +} +| COLON_TOK FORMULA_TOK an_formula +{ + // Previously this would call AddQuery() on the negation. + // But if multiple formula were (eroneously) present + // it discarded all but the last formula. Allowing multiple + // formula and taking the conjunction of them along with all + // the assumptions is what the other solvers do. + + //assumptions are like asserts + $$ = $3; +} + +| COLON_TOK EXTRAPREDS_TOK LPAREN_TOK var_decls RPAREN_TOK +{ + $$ = NULL; +} +| annotation +{ + $$ = NULL; +} +; + +logic_name: +FORMID_TOK +{ + $$ = $1; +} +; + +status: +SAT_TOK { + input_status = TO_BE_SATISFIABLE; + $$ = NULL; +} +| UNSAT_TOK { + input_status = TO_BE_UNSATISFIABLE; + $$ = NULL; + } +| UNKNOWN_TOK +{ + input_status = TO_BE_UNKNOWN; + $$ = NULL; +} +; + +annotation: +attribute +{ +} +| attribute user_value +{ +} +; + +user_value: +USER_VAL_TOK +{ + //cerr << "Printing user_value: " << *$1 << endl; +} +; + +attribute: +COLON_TOK SOURCE_TOK +{ +} +| COLON_TOK CATEGORY_TOK +{} +| COLON_TOK DIFFICULTY_TOK +{} +| COLON_TOK VERSION_TOK +{} +| COLON_TOK STATUS_TOK status +{} +; + +sort_symbs: +sort_symb +{ + //a single sort symbol here means either a BitVec or a Boolean + $$.indexwidth = $1.indexwidth; + $$.valuewidth = $1.valuewidth; +} +| sort_symb sort_symb +{ + //two sort symbols mean f: type --> type + $$.indexwidth = $1.valuewidth; + $$.valuewidth = $2.valuewidth; +} +; + +var_decls: +var_decl +{ +} +| +var_decls var_decl +{ +} +; + +var_decl: +FORMID_TOK LPAREN_TOK RPAREN_TOK LPAREN_TOK UNDERSCORE_TOK BITVEC_TOK NUMERAL_TOK RPAREN_TOK +{ + parserInterface->letMgr._parser_symbol_table.insert(*$1); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $1->SetIndexWidth(0); + $1->SetValueWidth($7); + delete $1; +} +| FORMID_TOK LPAREN_TOK RPAREN_TOK BOOL_TOK +{ + $1->SetIndexWidth(0); + $1->SetValueWidth(0); + parserInterface->letMgr._parser_symbol_table.insert(*$1); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + //delete $2; +} +| LPAREN_TOK FORMID_TOK sort_symbs RPAREN_TOK +{ + parserInterface->letMgr._parser_symbol_table.insert(*$2); + //Sort_symbs has the indexwidth/valuewidth. Set those fields in + //var + $2->SetIndexWidth($3.indexwidth); + $2->SetValueWidth($3.valuewidth); + delete $2; +} +| FORMID_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 +{ + parserInterface->letMgr._parser_symbol_table.insert(*$1); + unsigned int index_len = $9; + unsigned int value_len = $14; + if(index_len > 0) { + $1->SetIndexWidth($9); + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } + + if(value_len > 0) { + $1->SetValueWidth($14); + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } +} + +; + +an_formulas: +an_formula +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + delete $1; + } +} +| +an_formulas an_formula +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +} +; + +an_formula: +TRUE_TOK +{ + $$ = new ASTNode(parserInterface->CreateNode(TRUE)); + assert(0 == $$->GetIndexWidth()); + assert(0 == $$->GetValueWidth()); +} +| FALSE_TOK +{ + $$ = new ASTNode(parserInterface->CreateNode(FALSE)); + assert(0 == $$->GetIndexWidth()); + assert(0 == $$->GetValueWidth()); +} +| fvar +{ + $$ = $1; +} +| LPAREN_TOK EQ_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(EQ,*$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK +{ + using namespace BEEV; + + ASTVec terms = *$3; + ASTVec forms; + + for(ASTVec::const_iterator it=terms.begin(),itend=terms.end(); + it!=itend; it++) { + for(ASTVec::const_iterator it2=it+1; it2!=itend; it2++) { + ASTNode n = (parserInterface->nf->CreateNode(NOT, parserInterface->nf->CreateNode(EQ, *it, *it2))); + + + forms.push_back(n); + } + } + + if(forms.size() == 0) + FatalError("empty distinct"); + + $$ = (forms.size() == 1) ? + new ASTNode(forms[0]) : + new ASTNode(parserInterface->nf->CreateNode(AND, forms)); + + delete $3; +} + +| LPAREN_TOK BVSLT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLT, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSLE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSLE, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSGT_TOK an_term an_term RPAREN_TOK + //| LPAREN_TOK BVSGT_TOK an_term an_term annotations RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGT, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVSGE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVSGE, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVLT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLT, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVLE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVLE, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVGT_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGT, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK BVGE_TOK an_term an_term RPAREN_TOK +{ + ASTNode * n = new ASTNode(parserInterface->nf->CreateNode(BVGE, *$3, *$4)); + $$ = n; + delete $3; + delete $4; +} +| LPAREN_TOK an_formula RPAREN_TOK +{ + $$ = $2; +} +| LPAREN_TOK NOT_TOK an_formula RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(NOT, *$3)); + delete $3; +} +| LPAREN_TOK IMPLIES_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(IMPLIES, *$3, *$4)); + delete $3; + delete $4; +} +| LPAREN_TOK ITE_TOK an_formula an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(ITE, *$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; +} +| LPAREN_TOK AND_TOK an_formulas RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(AND, *$3)); + delete $3; +} +| LPAREN_TOK OR_TOK an_formulas RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(OR, *$3)); + delete $3; +} +| LPAREN_TOK XOR_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(XOR, *$3, *$4)); + delete $3; + delete $4; +} +| LPAREN_TOK EQ_TOK an_formula an_formula RPAREN_TOK +{ + $$ = new ASTNode(parserInterface->nf->CreateNode(IFF, *$3, *$4)); + delete $3; + delete $4; +} +| LPAREN_TOK LET_TOK LPAREN_TOK lets RPAREN_TOK an_formula RPAREN_TOK +{ + $$ = $6; + //Cleanup the LetIDToExprMap + parserInterface->letMgr.CleanupLetIDMap(); +} +; + +lets: let lets +| let +{}; + +let: LPAREN_TOK QUESTION_TOK FORMID_TOK an_formula RPAREN_TOK +{ + //set the valuewidth of the identifier + $3->SetValueWidth($4->GetValueWidth()); + $3->SetIndexWidth($4->GetIndexWidth()); + + //populate the hashtable from LET-var --> + //LET-exprs and then process them: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + parserInterface->letMgr.LetExprMgr(*$3,*$4); + + //delete $5; + //delete $6; +} +| LPAREN_TOK QUESTION_TOK FORMID_TOK an_term RPAREN_TOK +{ + //set the valuewidth of the identifier + $3->SetValueWidth($4->GetValueWidth()); + $3->SetIndexWidth($4->GetIndexWidth()); + + //populate the hashtable from LET-var --> + //LET-exprs and then process them: + // + //1. ensure that LET variables do not clash + //1. with declared variables. + // + //2. Ensure that LET variables are not + //2. defined more than once + parserInterface->letMgr.LetExprMgr(*$3,*$4); + + //delete $5; + //delete $6; +} +; + + + +an_terms: +an_term +{ + $$ = new ASTVec; + if ($1 != NULL) { + $$->push_back(*$1); + delete $1; + } +} +| +an_terms an_term +{ + if ($1 != NULL && $2 != NULL) { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +} +; + +an_term: +BVCONST_TOK +{ + $$ = new ASTNode(parserInterface->CreateBVConst($1, 10, 32)); +} +| BVCONST_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +{ + $$ = new ASTNode(parserInterface->CreateBVConst($1,10,$3)); + delete $1; +} +| an_nonbvconst_term +; + +an_nonbvconst_term: +BITCONST_TOK { $$ = $1; } +| var +{ + $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + delete $1; +} +| LPAREN_TOK an_term RPAREN_TOK + //| LPAREN_TOK an_term annotations RPAREN_TOK +{ + $$ = $2; + //$$ = new ASTNode(parserInterface->SimplifyTerm(*$2)); + //delete $2; +} +| SELECT_TOK an_term an_term +{ + //ARRAY READ + // valuewidth is same as array, indexwidth is 0. + ASTNode array = *$2; + ASTNode index = *$3; + unsigned int width = array.GetValueWidth(); + ASTNode * n = + new ASTNode(parserInterface->nf->CreateTerm(READ, width, array, index)); + $$ = n; + delete $2; + delete $3; +} +| STORE_TOK an_term an_term an_term +{ + //ARRAY WRITE + unsigned int width = $4->GetValueWidth(); + ASTNode array = *$2; + ASTNode index = *$3; + ASTNode writeval = *$4; + ASTNode write_term = parserInterface->nf->CreateArrayTerm(WRITE,$2->GetIndexWidth(),width,array,index,writeval); + ASTNode * n = new ASTNode(write_term); + $$ = n; + delete $2; + delete $3; + delete $4; +} +| LPAREN_TOK UNDERSCORE_TOK BVEXTRACT_TOK NUMERAL_TOK NUMERAL_TOK RPAREN_TOK an_term +{ + int width = $4 - $5 + 1; + if (width < 0) + yyerror("Negative width in extract"); + + if((unsigned)$4 >= $7->GetValueWidth()) + yyerror("Parsing: Wrong width in BVEXTRACT\n"); + + ASTNode hi = parserInterface->CreateBVConst(32, $4); + ASTNode low = parserInterface->CreateBVConst(32, $5); + ASTNode output = parserInterface->nf->CreateTerm(BVEXTRACT, width, *$7,hi,low); + ASTNode * n = new ASTNode(output); + $$ = n; + //delete $7; +} +| LPAREN_TOK UNDERSCORE_TOK BVZX_TOK NUMERAL_TOK RPAREN_TOK an_term +{ + if (0 != $4) + { + unsigned w = $6->GetValueWidth() + $4; + ASTNode leading_zeroes = parserInterface->CreateZeroConst($4); + ASTNode *n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,w,leading_zeroes,*$6)); + $$ = n; + //delete $5; + } + else + $$ = $6; +} +| LPAREN_TOK UNDERSCORE_TOK BVSX_TOK NUMERAL_TOK RPAREN_TOK an_term +{ + unsigned w = $6->GetValueWidth() + $4; + ASTNode width = parserInterface->CreateBVConst(32,w); + ASTNode *n = new ASTNode(parserInterface->nf->CreateTerm(BVSX,w,*$6,width)); + $$ = n; + //delete $5; +} + +| ITE_TOK an_formula an_term an_term +{ + const unsigned int width = $3->GetValueWidth(); + $$ = new ASTNode(parserInterface->nf->CreateArrayTerm(ITE,$4->GetIndexWidth(), width,*$2, *$3, *$4)); + delete $2; + delete $3; + delete $4; +} +| BVCONCAT_TOK an_term an_term +{ + const unsigned int width = $2->GetValueWidth() + $3->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| BVNOT_TOK an_term +{ + //this is the BVNEG (term) in the CVCL language + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, *$2)); + $$ = n; + delete $2; +} +| BVNEG_TOK an_term +{ + //this is the BVUMINUS term in CVCL langauge + unsigned width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVUMINUS,width,*$2)); + $$ = n; + delete $2; +} +| BVAND_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| BVOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| BVXOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVXOR, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} + | BVXNOR_TOK an_term an_term + { +// (bvxnor s t) abbreviates (bvor (bvand s t) (bvand (bvnot s) (bvnot t))) + + + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode( + parserInterface->nf->CreateTerm( BVOR, width, + parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3), + parserInterface->nf->CreateTerm(BVAND, width, + parserInterface->nf->CreateTerm(BVNEG, width, *$2), + parserInterface->nf->CreateTerm(BVNEG, width, *$3) + ))); + + $$ = n; + delete $2; + delete $3; + + } + | BVCOMP_TOK an_term an_term + { + + + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(ITE, 1, + parserInterface->nf->CreateNode(EQ, *$2, *$3), + parserInterface->CreateOneConst(1), + parserInterface->CreateZeroConst(1))); + + $$ = n; + delete $2; + delete $3; + } + + +| BVSUB_TOK an_term an_term +{ + const unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSUB, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| BVPLUS_TOK an_term an_term +{ + const unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVPLUS, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; + +} +| BVMULT_TOK an_term an_term +{ + const unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMULT, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} + +| BVDIV_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVDIV, width, *$2, *$3)); + $$ = n; + + delete $2; + delete $3; +} +| BVMOD_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVMOD, width, *$2, *$3)); + $$ = n; + + delete $2; + delete $3; +} +| SBVDIV_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVDIV, width, *$2, *$3)); + $$ = n; + + delete $2; + delete $3; +} +| SBVREM_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVREM, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| SBVMOD_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(SBVMOD, width, *$2, *$3)); + $$ = n; + delete $2; + delete $3; +} +| BVNAND_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVAND, width, *$2, *$3))); + $$ = n; + delete $2; + delete $3; +} +| BVNOR_TOK an_term an_term +{ + unsigned int width = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVNEG, width, parserInterface->nf->CreateTerm(BVOR, width, *$2, *$3))); + $$ = n; + delete $2; + delete $3; +} +| BVLEFTSHIFT_1_TOK an_term an_term +{ + // shifting left by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVLEFTSHIFT,w,*$2,*$3)); + $$ = n; + delete $2; + delete $3; +} +| BVRIGHTSHIFT_1_TOK an_term an_term +{ + // shifting right by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVRIGHTSHIFT,w,*$2,*$3)); + $$ = n; + delete $2; + delete $3; +} +| BVARITHRIGHTSHIFT_TOK an_term an_term +{ + // shifting arithmetic right by who know how much? + unsigned int w = $2->GetValueWidth(); + ASTNode * n = new ASTNode(parserInterface->nf->CreateTerm(BVSRSHIFT,w,*$2,*$3)); + $$ = n; + delete $2; + delete $3; +} +| LPAREN_TOK UNDERSCORE_TOK BVROTATE_LEFT_TOK NUMERAL_TOK RPAREN_TOK an_term +{ + + ASTNode *n; + unsigned width = $6->GetValueWidth(); + unsigned rotate = $4; + if (0 == rotate) + { + n = $6; + } + else if (rotate < width) + { + ASTNode high = parserInterface->CreateBVConst(32,width-1); + ASTNode zero = parserInterface->CreateBVConst(32,0); + ASTNode cut = parserInterface->CreateBVConst(32,width-rotate); + ASTNode cutMinusOne = parserInterface->CreateBVConst(32,width-rotate-1); + + ASTNode top = parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$6,high, cut); + ASTNode bottom = parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$6,cutMinusOne,zero); + n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top)); + delete $6; + } + else + { + n = NULL; // remove gcc warning. + yyerror("Rotate must be strictly less than the width."); + } + + $$ = n; + +} +| LPAREN_TOK UNDERSCORE_TOK BVROTATE_RIGHT_TOK NUMERAL_TOK RPAREN_TOK an_term +{ + + ASTNode *n; + unsigned width = $6->GetValueWidth(); + unsigned rotate = $4; + if (0 == rotate) + { + n = $6; + } + else if (rotate < width) + { + ASTNode high = parserInterface->CreateBVConst(32,width-1); + ASTNode zero = parserInterface->CreateBVConst(32,0); + ASTNode cut = parserInterface->CreateBVConst(32,rotate); + ASTNode cutMinusOne = parserInterface->CreateBVConst(32,rotate-1); + + ASTNode bottom = parserInterface->nf->CreateTerm(BVEXTRACT,rotate,*$6,cutMinusOne, zero); + ASTNode top = parserInterface->nf->CreateTerm(BVEXTRACT,width-rotate,*$6,high,cut); + n = new ASTNode(parserInterface->nf->CreateTerm(BVCONCAT,width,bottom,top)); + delete $6; + } + else + { + n = NULL; // remove gcc warning. + yyerror("Rotate must be strictly less than the width."); + } + + $$ = n; + +} + | BVREPEAT_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK an_term + { + unsigned count = $3; + if (count < 1) + FatalError("One or more repeats please"); + + unsigned w = $5->GetValueWidth(); + ASTNode n = *$5; + + for (unsigned i =1; i < count; i++) + { + n = parserInterface->nf->CreateTerm(BVCONCAT,w*(i+1),n,*$5); + } + $$ = new ASTNode(n); + } +| UNDERSCORE_TOK BVCONST_TOK NUMERAL_TOK +{ + $$ = new ASTNode(parserInterface->CreateBVConst($2, 10, $3)); + $$->SetValueWidth($3); +} +; + +sort_symb: +BITVEC_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK +{ + // Just return BV width. If sort is BOOL, width is 0. + // Otherwise, BITVEC[w] returns w. + // + //((indexwidth is 0) && (valuewidth>0)) iff type is BV + $$.indexwidth = 0; + unsigned int length = $3; + if(length > 0) { + $$.valuewidth = length; + } + else { + FatalError("Fatal Error: parsing: BITVECTORS must be of positive length: \n"); + } +} +; + +var: +TERMID_TOK +{ + $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + delete $1; +} +| QUESTION_TOK TERMID_TOK +{ + $$ = $2; +} +; + +fvar: +DOLLAR_TOK FORMID_TOK +{ + $$ = $2; +} +| FORMID_TOK +{ + $$ = new ASTNode(parserInterface->letMgr.ResolveID(*$1)); + delete $1; +} +| QUESTION_TOK FORMID_TOK +{ + $$ = $2; +} +; +%% diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 994dca3..ecca806 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -369,7 +369,7 @@ namespace BEEV if (bm->UserFlags.print_output_flag) { - if (bm->UserFlags.smtlib_parser_flag) + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) { if (true_iff_valid && (input_status == TO_BE_SATISFIABLE)) @@ -391,7 +391,7 @@ namespace BEEV bm->ValidFlag = true; if (bm->UserFlags.print_output_flag) { - if (bm->UserFlags.smtlib_parser_flag) + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) cout << "unsat\n"; else cout << "Valid.\n"; @@ -402,7 +402,7 @@ namespace BEEV bm->ValidFlag = false; if (bm->UserFlags.print_output_flag) { - if (bm->UserFlags.smtlib_parser_flag) + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) cout << "sat\n"; else cout << "Invalid.\n";