diff options
Diffstat (limited to 'lib/SMT/smtlib.y')
| -rw-r--r-- | lib/SMT/smtlib.y | 1222 |
1 files changed, 1222 insertions, 0 deletions
diff --git a/lib/SMT/smtlib.y b/lib/SMT/smtlib.y new file mode 100644 index 00000000..c9e7b990 --- /dev/null +++ b/lib/SMT/smtlib.y @@ -0,0 +1,1222 @@ +%{ +/*****************************************************************************/ +/*! + * \file smtlib.y + * + * Author: Clark Barrett + * + * Created: Apr 30 2005 + * + * <hr> + * + * 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. + * + * <hr> + * + */ +/*****************************************************************************/ +/* + This file contains the bison code for the parser that reads in CVC + commands in SMT-LIB language. +*/ + +#include "vc.h" +#include "parser_exception.h" +#include "parser_temp.h" + +// Exported shared data +namespace CVC3 { + extern ParserTemp* parserTemp; +} +// Define shortcuts for various things +#define TMP CVC3::parserTemp +#define EXPR CVC3::parserTemp->expr +#define VC (CVC3::parserTemp->vc) +#define ARRAYSENABLED (CVC3::parserTemp->arrFlag) +#define BVENABLED (CVC3::parserTemp->bvFlag) +#define BVSIZE (CVC3::parserTemp->bvSize) +#define RAT(args) CVC3::newRational args +#define QUERYPARSED CVC3::parserTemp->queryParsed + +// Suppress the bogus warning suppression in bison (it generates +// compile error) +#undef __GNUC_MINOR__ + +/* stuff that lives in smtlib.lex */ +extern int smtliblex(void); + +int smtliberror(const char *s) +{ + std::ostringstream ss; + ss << CVC3::parserTemp->fileName << ":" << CVC3::parserTemp->lineNum + << ": " << s; + return CVC3::parserTemp->error(ss.str()); +} + + + +#define YYLTYPE_IS_TRIVIAL 1 +#define YYMAXDEPTH 10485760 + +%} + +%union { + std::string *str; + std::vector<std::string> *strvec; + CVC3::Expr *node; + std::vector<CVC3::Expr> *vec; + std::pair<std::vector<CVC3::Expr>, std::vector<std::string> > *pat_ann; +}; + + +%start cmd + +/* strings are for better error messages. + "_TOK" is so macros don't conflict with kind names */ + +%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls +%type <vec> an_formulas quant_vars an_terms fun_symb patterns +%type <node> pattern +%type <node> benchmark bench_name bench_attribute +%type <node> status fun_symb_decl fun_sig pred_symb_decl pred_sig +%type <node> an_formula quant_var an_atom prop_atom +%type <node> an_term basic_term sort_symb pred_symb +%type <node> var fvar +%type <str> logic_name quant_symb connective user_value attribute annotation +%type <strvec> annotations +%type <pat_ann> patterns_annotations + +%token <str> NUMERAL_TOK +%token <str> SYM_TOK +%token <str> STRING_TOK +%token <str> AR_SYMB +%token <str> USER_VAL_TOK +%token TRUE_TOK +%token FALSE_TOK +%token ITE_TOK +%token NOT_TOK +%token IMPLIES_TOK +%token IF_THEN_ELSE_TOK +%token AND_TOK +%token OR_TOK +%token XOR_TOK +%token IFF_TOK +%token EXISTS_TOK +%token FORALL_TOK +%token LET_TOK +%token FLET_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 COLON_TOK +%token LBRACKET_TOK +%token RBRACKET_TOK +%token LCURBRACK_TOK +%token RCURBRACK_TOK +%token LPAREN_TOK +%token RPAREN_TOK +%token SAT_TOK +%token UNSAT_TOK +%token UNKNOWN_TOK +%token ASSUMPTION_TOK +%token FORMULA_TOK +%token STATUS_TOK +%token BENCHMARK_TOK +%token EXTRASORTS_TOK +%token EXTRAFUNS_TOK +%token EXTRAPREDS_TOK +%token LANGUAGE_TOK +%token DOLLAR_TOK +%token QUESTION_TOK +%token DISTINCT_TOK +%token SEMICOLON_TOK +%token EOF_TOK +%token PAT_TOK +%% + +cmd: + benchmark + { + EXPR = *$1; + delete $1; + YYACCEPT; + } +; + +benchmark: + LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK + { + if (!QUERYPARSED) + $4->push_back(CVC3::Expr(VC->listExpr("_CHECKSAT", CVC3::Expr(VC->idExpr("_TRUE_EXPR"))))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ",*$4)); + delete $4; + } + | EOF_TOK + { + TMP->done = true; + $$ = new CVC3::Expr(); + } +; + +bench_name: + SYM_TOK + { + $$ = NULL; + delete $1; + } +; + +bench_attributes: + bench_attribute + { + $$ = new std::vector<CVC3::Expr>; + if ($1) { + $$->push_back(*$1); + delete $1; + } + } + | bench_attributes bench_attribute + { + $$ = $1; + if ($2) { + $$->push_back(*$2); + delete $2; + } + } +; + +bench_attribute: + COLON_TOK ASSUMPTION_TOK an_formula + { + $$ = new CVC3::Expr(VC->listExpr("_ASSERT", *$3)); + delete $3; + } + | COLON_TOK FORMULA_TOK an_formula + { + $$ = new CVC3::Expr(VC->listExpr("_CHECKSAT", *$3)); + QUERYPARSED = true; + delete $3; + } + | COLON_TOK STATUS_TOK status + { + $$ = NULL; + } + | COLON_TOK LOGIC_TOK logic_name + { + ARRAYSENABLED = false; + BVENABLED = false; + if (*$3 == "QF_UF") { + $$ = new CVC3::Expr(VC->listExpr("_TYPE", VC->idExpr("U"))); + } + else if (*$3 == "QF_A" || + *$3 == "QF_AX") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> tmp; + tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Index"))); + tmp.push_back(VC->listExpr("_TYPE", VC->idExpr("Element"))); + tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), + VC->listExpr("_ARRAY", + VC->idExpr("Index"), + VC->idExpr("Element")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFLIA" || + *$3 == "AUFLIA") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> tmp; + tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), + VC->listExpr("_ARRAY", + VC->idExpr("_INT"), + VC->idExpr("_INT")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFLIRA" || + *$3 == "AUFLIRA" || + *$3 == "QF_AUFNIRA" || + *$3 == "AUFNIRA") { + ARRAYSENABLED = true; + std::vector<CVC3::Expr> tmp; + tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array1"), + VC->listExpr("_ARRAY", + VC->idExpr("_INT"), + VC->idExpr("_REAL")))); + tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array2"), + VC->listExpr("_ARRAY", + VC->idExpr("_INT"), + VC->idExpr("Array1")))); + $$ = new CVC3::Expr(VC->listExpr("_SEQ", tmp)); + } + else if (*$3 == "QF_AUFBV" || + *$3 == "QF_ABV") { + ARRAYSENABLED = true; + BVENABLED = true; + $$ = NULL; +// $$ = new CVC3::Expr(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), +// VC->listExpr("_ARRAY", +// VC->listExpr("_BITVECTOR", VC->ratExpr(32)), +// VC->listExpr("_BITVECTOR", VC->ratExpr(8))))); + } + else if (*$3 == "QF_BV" || + *$3 == "QF_UFBV") { + BVENABLED = true; + $$ = NULL; + } + // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode + else if (*$3 == "QF_LRA") { + $$ = new CVC3::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1))); + } + else { + $$ = NULL; + } + delete $3; + } + | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_TYPE", *$4)); + delete $4; + } + | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); + delete $4; + } + | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_SEQ", *$4)); + delete $4; + } + | COLON_TOK NOTES_TOK STRING_TOK + { + $$ = NULL; + delete $3; + } + | COLON_TOK CVC_COMMAND_TOK STRING_TOK + { + $$ = new CVC3::Expr(VC->listExpr(VC->idExpr("_"+*$3))); + delete $3; + } + | annotation + { + $$ = NULL; + delete $1; + } +; + +logic_name: + SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + BVSIZE = atoi($3->c_str()); + delete $3; + $$ = $1; + } + | SYM_TOK + { + $$ = $1; + } +; + +status: + SAT_TOK { $$ = NULL; } + | UNSAT_TOK { $$ = NULL; } + | UNKNOWN_TOK { $$ = NULL; } +; + +sort_symbs: + sort_symb + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | sort_symbs sort_symb + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +fun_symb_decls: + fun_symb_decl + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | + fun_symb_decls fun_symb_decl + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +fun_symb_decl: + LPAREN_TOK fun_sig annotations RPAREN_TOK + { + $$ = $2; + delete $3; + } + | LPAREN_TOK fun_sig RPAREN_TOK + { + $$ = $2; + } +; + +fun_sig: + fun_symb sort_symbs + { + if ($2->size() == 1) { + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0])); + } + else { + CVC3::Expr tmp(VC->listExpr("_ARROW", *$2)); + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp)); + } + delete $1; + delete $2; + } +; + +pred_symb_decls: + pred_symb_decl + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | + pred_symb_decls pred_symb_decl + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +pred_symb_decl: + LPAREN_TOK pred_sig annotations RPAREN_TOK + { + $$ = $2; + delete $3; + } + | LPAREN_TOK pred_sig RPAREN_TOK + { + $$ = $2; + } +; + +pred_sig: + pred_symb sort_symbs + { + std::vector<CVC3::Expr> tmp(*$2); + tmp.push_back(VC->idExpr("_BOOLEAN")); + CVC3::Expr tmp2(VC->listExpr("_ARROW", tmp)); + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2)); + delete $1; + delete $2; + } + | pred_symb + { + $$ = new CVC3::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), + VC->idExpr("_BOOLEAN"))); + delete $1; + } +; + +an_formulas: + an_formula + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | + an_formulas an_formula + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +an_formula: + an_atom + { + $$ = $1; + } + | LPAREN_TOK connective an_formulas annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK connective an_formulas RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + } + | LPAREN_TOK quant_symb quant_vars an_formula annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); + delete $2; + delete $3; + delete $4; + delete $5; + } + | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first))); + delete $2; + delete $3; + delete $4; + delete $5; + } + | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); + delete $4; + delete $5; + delete $7; + delete $8; + } + | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula RPAREN_TOK + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); + delete $4; + delete $5; + delete $7; + } + | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula annotations RPAREN_TOK + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); + delete $4; + delete $5; + delete $7; + delete $8; + } + | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_formula RPAREN_TOK + { + CVC3::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); + $$ = new CVC3::Expr(VC->listExpr("_LET", e, *$7)); + delete $4; + delete $5; + delete $7; + } +; + +patterns_annotations: + patterns + { + $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >; + $$->first = *$1; + delete $1; + } + | annotation + { + $$ = new std::pair<std::vector<CVC3::Expr>, std::vector<std::string> >; + $$->second.push_back(*$1); + delete $1; + } + | patterns_annotations patterns + { + $1->first.insert($1->first.end(), $2->begin(), $2->end()); + $$ = $1; + delete $2; + } + | patterns_annotations annotation + { + $1->second.push_back(*$2); + $$ = $1; + delete $2; + } + +patterns: + pattern + { + $$ = new std::vector<CVC3::Expr >; + $$->push_back(*$1); + delete $1; + } + | patterns pattern + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } + +pattern: + PAT_TOK LCURBRACK_TOK an_terms RCURBRACK_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$3)); + delete $3; + } + | PAT_TOK LCURBRACK_TOK an_formulas RCURBRACK_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$3)); + delete $3; + } + + + +quant_vars: + quant_var + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | quant_vars quant_var + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +quant_var: + LPAREN_TOK var sort_symb RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr(*$2, *$3)); + delete $2; + delete $3; + } +; + +quant_symb: + EXISTS_TOK + { + $$ = new std::string("_EXISTS"); + } + | FORALL_TOK + { + $$ = new std::string("_FORALL"); + } +; + +connective: + NOT_TOK + { + $$ = new std::string("_NOT"); + } + | IMPLIES_TOK + { + $$ = new std::string("_IMPLIES"); + } + | IF_THEN_ELSE_TOK + { + $$ = new std::string("_IF"); + } + | AND_TOK + { + $$ = new std::string("_AND"); + } + | OR_TOK + { + $$ = new std::string("_OR"); + } + | XOR_TOK + { + $$ = new std::string("_XOR"); + } + | IFF_TOK + { + $$ = new std::string("_IFF"); + } +; + +an_atom: + prop_atom + { + $$ = $1; + } + | LPAREN_TOK prop_atom annotations RPAREN_TOK + { + $$ = $2; + delete $3; + } + | LPAREN_TOK pred_symb an_terms annotations RPAREN_TOK + { + if ($4->size() == 1 && (*$4)[0] == "transclose" && + $3->size() == 2) { + $$ = new CVC3::Expr(VC->listExpr("_TRANS_CLOSURE", + *$2, (*$3)[0], (*$3)[1])); + } + else { + std::vector<CVC3::Expr> tmp; + tmp.push_back(*$2); + tmp.insert(tmp.end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(tmp)); + } + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK pred_symb an_terms RPAREN_TOK + { + std::vector<CVC3::Expr> tmp; + tmp.push_back(*$2); + tmp.insert(tmp.end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(tmp)); + delete $2; + delete $3; + } + | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); + +// std::vector<CVC3::Expr> tmp; +// tmp.push_back(*$2); +// tmp.insert(tmp.end(), $3->begin(), $3->end()); +// $$ = new CVC3::Expr(VC->listExpr(tmp)); +// for (unsigned i = 0; i < (*$3).size(); ++i) { +// tmp.push_back(($3)[i]) +// for (unsigned j = i+1; j < (*$3).size(); ++j) { +// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); +// } +// } +// $$ = new CVC3::Expr(VC->listExpr("_AND", tmp)); + delete $3; + delete $4; + } + | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_DISTINCT", *$3)); +// std::vector<CVC3::Expr> tmp; +// for (unsigned i = 0; i < (*$3).size(); ++i) { +// for (unsigned j = i+1; j < (*$3).size(); ++j) { +// tmp.push_back(VC->listExpr("_NEQ", (*$3)[i], (*$3)[j])); +// } +// } +// $$ = new CVC3::Expr(VC->listExpr("_AND", tmp)); + delete $3; + } +; + +prop_atom: + TRUE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR")); + } + | FALSE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR")); + } + | fvar + { + $$ = $1; + } + | pred_symb + { + $$ = $1; + } +; + +an_terms: + an_term + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(*$1); + delete $1; + } + | an_terms an_term + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } +; + +an_term: + basic_term + { + $$ = $1; + } + | LPAREN_TOK basic_term annotations RPAREN_TOK + { + $$ = $2; + delete $3; + } + | LPAREN_TOK fun_symb an_terms annotations RPAREN_TOK + { + $2->insert($2->end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(*$2)); + delete $2; + delete $3; + delete $4; + } + | LPAREN_TOK fun_symb an_terms RPAREN_TOK + { + $2->insert($2->end(), $3->begin(), $3->end()); + $$ = new CVC3::Expr(VC->listExpr(*$2)); + delete $2; + delete $3; + } + | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; + delete $6; + } + | LPAREN_TOK ITE_TOK an_formula an_term an_term RPAREN_TOK + { + $$ = new CVC3::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); + delete $3; + delete $4; + delete $5; + } +; + +basic_term: + | TRUE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_TRUE_EXPR")); + } + | FALSE_TOK + { + $$ = new CVC3::Expr(VC->idExpr("_FALSE_EXPR")); + } + | fvar + { + $$ = $1; + } + | var + { + $$ = $1; + } + | fun_symb + { + if ($1->size() == 1) { + $$ = new CVC3::Expr(((*$1)[0])); + } + else { + $$ = new CVC3::Expr(VC->listExpr(*$1)); + } + delete $1; + } +; + +annotations: + annotation + { + $$ = new std::vector<std::string>; + $$->push_back(*$1); + delete $1; + } + | annotations annotation + { + $1->push_back(*$2); + $$ = $1; + delete $2; + } + ; + + +annotation: + attribute + { $$ = $1; } + | attribute user_value + { $$ = $1; } +; + +user_value: + USER_VAL_TOK + { + $$ = NULL; + delete $1; + } +; + + +sort_symb: + SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + if (BVENABLED && *$1 == "BitVec") { + $$ = new CVC3::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3))); + } + else { + $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3))); + } + delete $1; + delete $3; + } + | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK + { + if (BVENABLED && ARRAYSENABLED && *$1 == "Array") { + $$ = new CVC3::Expr(VC->listExpr("_ARRAY", + VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)), + VC->listExpr("_BITVECTOR", VC->ratExpr(*$5)))); + } + else { + $$ = new CVC3::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5))); + } + delete $1; + delete $3; + delete $5; + } + | SYM_TOK + { + if (*$1 == "Real") { + $$ = new CVC3::Expr(VC->idExpr("_REAL")); + } else if (*$1 == "Int") { + $$ = new CVC3::Expr(VC->idExpr("_INT")); + } else { + $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } +; + +pred_symb: + SYM_TOK + { + if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { + $$ = new CVC3::Expr(VC->idExpr("_BVLT")); + } + else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { + $$ = new CVC3::Expr(VC->idExpr("_BVLE")); + } + else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { + $$ = new CVC3::Expr(VC->idExpr("_BVGE")); + } + else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { + $$ = new CVC3::Expr(VC->idExpr("_BVGT")); + } + else if (BVENABLED && *$1 == "bvslt") { + $$ = new CVC3::Expr(VC->idExpr("_BVSLT")); + } + else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { + $$ = new CVC3::Expr(VC->idExpr("_BVSLE")); + } + else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { + $$ = new CVC3::Expr(VC->idExpr("_BVSGE")); + } + else if (BVENABLED && *$1 == "bvsgt") { + $$ = new CVC3::Expr(VC->idExpr("_BVSGT")); + } + else { + $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } + | AR_SYMB + { + if ($1->length() == 1) { + switch ((*$1)[0]) { + case '=': $$ = new CVC3::Expr(VC->idExpr("_EQ")); break; + case '<': $$ = new CVC3::Expr(VC->idExpr("_LT")); break; + case '>': $$ = new CVC3::Expr(VC->idExpr("_GT")); break; + default: $$ = new CVC3::Expr(VC->idExpr(*$1)); break; + } + } + else { + if (*$1 == "<=") { + $$ = new CVC3::Expr(VC->idExpr("_LE")); + } else if (*$1 == ">=") { + $$ = new CVC3::Expr(VC->idExpr("_GE")); + } + else $$ = new CVC3::Expr(VC->idExpr(*$1)); + } + delete $1; + } +; + +fun_symb: + SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK + { + $$ = new std::vector<CVC3::Expr>; + if (BVENABLED && *$1 == "repeat") { + $$->push_back(VC->idExpr("_BVREPEAT")); + } + else if (BVENABLED && *$1 == "zero_extend") { + $$->push_back(VC->idExpr("_BVZEROEXTEND")); + } + else if (BVENABLED && *$1 == "sign_extend") { + $$->push_back(VC->idExpr("_SX")); + $$->push_back(VC->idExpr("_smtlib")); + } + else if (BVENABLED && *$1 == "rotate_left") { + $$->push_back(VC->idExpr("_BVROTL")); + } + else if (BVENABLED && *$1 == "rotate_right") { + $$->push_back(VC->idExpr("_BVROTR")); + } + else if (BVENABLED && + $1->size() > 2 && + (*$1)[0] == 'b' && + (*$1)[1] == 'v') { + int i = 2; + while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; + if ((*$1)[i] == '\0') { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr($1->substr(2), 10)); + } + else $$->push_back(VC->idExpr(*$1)); + } + else $$->push_back(VC->idExpr(*$1)); + $$->push_back(VC->ratExpr(*$3)); + delete $1; + delete $3; + } + | SYM_TOK LBRACKET_TOK NUMERAL_TOK COLON_TOK NUMERAL_TOK RBRACKET_TOK + { + $$ = new std::vector<CVC3::Expr>; + if (BVENABLED && *$1 == "extract") { + $$->push_back(VC->idExpr("_EXTRACT")); + } + else $$->push_back(VC->idExpr(*$1)); + $$->push_back(VC->ratExpr(*$3)); + $$->push_back(VC->ratExpr(*$5)); + delete $1; + delete $3; + delete $5; + } + | SYM_TOK + { + $$ = new std::vector<CVC3::Expr>; + if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { + $$->push_back(VC->idExpr("_BVLT")); + } + else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { + $$->push_back(VC->idExpr("_BVLE")); + } + else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { + $$->push_back(VC->idExpr("_BVGE")); + } + else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { + $$->push_back(VC->idExpr("_BVGT")); + } + else if (BVENABLED && *$1 == "bvslt") { + $$->push_back(VC->idExpr("_BVSLT")); + } + else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { + $$->push_back(VC->idExpr("_BVSLE")); + } + else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { + $$->push_back(VC->idExpr("_BVSGE")); + } + else if (BVENABLED && *$1 == "bvsgt") { + $$->push_back(VC->idExpr("_BVSGT")); + } + else if (ARRAYSENABLED && *$1 == "select") { + $$->push_back(VC->idExpr("_READ")); + } + else if (ARRAYSENABLED && *$1 == "store") { + $$->push_back(VC->idExpr("_WRITE")); + } + else if (BVENABLED && *$1 == "bit0") { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr(0)); + $$->push_back(VC->ratExpr(1)); + } + else if (BVENABLED && *$1 == "bit1") { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr(1)); + $$->push_back(VC->ratExpr(1)); + } + else if (BVENABLED && *$1 == "concat") { + $$->push_back(VC->idExpr("_CONCAT")); + } + else if (BVENABLED && *$1 == "bvnot") { + $$->push_back(VC->idExpr("_BVNEG")); + } + else if (BVENABLED && *$1 == "bvand") { + $$->push_back(VC->idExpr("_BVAND")); + } + else if (BVENABLED && *$1 == "bvor") { + $$->push_back(VC->idExpr("_BVOR")); + } + else if (BVENABLED && *$1 == "bvneg") { + $$->push_back(VC->idExpr("_BVUMINUS")); + } + else if (BVENABLED && *$1 == "bvadd") { + $$->push_back(VC->idExpr("_BVPLUS")); + } + else if (BVENABLED && *$1 == "bvmul") { + $$->push_back(VC->idExpr("_BVMULT")); + } + else if (BVENABLED && *$1 == "bvudiv") { + $$->push_back(VC->idExpr("_BVUDIV")); + } + else if (BVENABLED && *$1 == "bvurem") { + $$->push_back(VC->idExpr("_BVUREM")); + } + else if (BVENABLED && *$1 == "bvshl") { + $$->push_back(VC->idExpr("_BVSHL")); + } + else if (BVENABLED && *$1 == "bvlshr") { + $$->push_back(VC->idExpr("_BVLSHR")); + } + + else if (BVENABLED && *$1 == "bvxor") { + $$->push_back(VC->idExpr("_BVXOR")); + } + else if (BVENABLED && *$1 == "bvxnor") { + $$->push_back(VC->idExpr("_BVXNOR")); + } + else if (BVENABLED && *$1 == "bvcomp") { + $$->push_back(VC->idExpr("_BVCOMP")); + } + + else if (BVENABLED && *$1 == "bvsub") { + $$->push_back(VC->idExpr("_BVSUB")); + } + else if (BVENABLED && *$1 == "bvsdiv") { + $$->push_back(VC->idExpr("_BVSDIV")); + } + else if (BVENABLED && *$1 == "bvsrem") { + $$->push_back(VC->idExpr("_BVSREM")); + } + else if (BVENABLED && *$1 == "bvsmod") { + $$->push_back(VC->idExpr("_BVSMOD")); + } + else if (BVENABLED && *$1 == "bvashr") { + $$->push_back(VC->idExpr("_BVASHR")); + } + + // For backwards compatibility: + else if (BVENABLED && *$1 == "shift_left0") { + $$->push_back(VC->idExpr("_CONST_WIDTH_LEFTSHIFT")); + } + else if (BVENABLED && *$1 == "shift_right0") { + $$->push_back(VC->idExpr("_RIGHTSHIFT")); + } + else if (BVENABLED && *$1 == "sign_extend") { + $$->push_back(VC->idExpr("_SX")); + $$->push_back(VC->idExpr("_smtlib")); + } + + // Bitvector constants + else if (BVENABLED && + $1->size() > 2 && + (*$1)[0] == 'b' && + (*$1)[1] == 'v') { + bool done = false; + if ((*$1)[2] >= '0' && (*$1)[2] <= '9') { + int i = 3; + while ((*$1)[i] >= '0' && (*$1)[i] <= '9') ++i; + if ((*$1)[i] == '\0') { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr($1->substr(2), 10)); + $$->push_back(VC->ratExpr(32)); + done = true; + } + } + else if ($1->size() > 5) { + std::string s = $1->substr(0,5); + if (s == "bvbin") { + int i = 5; + while ((*$1)[i] >= '0' && (*$1)[i] <= '1') ++i; + if ((*$1)[i] == '\0') { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr($1->substr(5), 2)); + $$->push_back(VC->ratExpr(i-5)); + done = true; + } + } + else if (s == "bvhex") { + int i = 5; + char c = (*$1)[i]; + while ((c >= '0' && c <= '9') || + (c >= 'a' && c <= 'f') || + (c >= 'A' && c <= 'F')) { + ++i; + c =(*$1)[i]; + } + if ((*$1)[i] == '\0') { + $$->push_back(VC->idExpr("_BVCONST")); + $$->push_back(VC->ratExpr($1->substr(5), 16)); + $$->push_back(VC->ratExpr(i-5)); + done = true; + } + } + } + if (!done) $$->push_back(VC->idExpr(*$1)); + } + else { + $$->push_back(VC->idExpr(*$1)); + } + delete $1; + } + | AR_SYMB + { + $$ = new std::vector<CVC3::Expr>; + if ($1->length() == 1) { + switch ((*$1)[0]) { + case '+': $$->push_back(VC->idExpr("_PLUS")); break; + case '-': $$->push_back(VC->idExpr("_MINUS")); break; + case '*': $$->push_back(VC->idExpr("_MULT")); break; + case '~': $$->push_back(VC->idExpr("_UMINUS")); break; + case '/': $$->push_back(VC->idExpr("_DIVIDE")); break; + case '=': $$->push_back(VC->idExpr("_EQ")); break; + case '<': $$->push_back(VC->idExpr("_LT")); break; + case '>': $$->push_back(VC->idExpr("_GT")); break; + default: $$->push_back(VC->idExpr(*$1)); + } + } + else { + if (*$1 == "<=") { + $$->push_back(VC->idExpr("_LE")); + } else if (*$1 == ">=") { + $$->push_back(VC->idExpr("_GE")); + } + else $$->push_back(VC->idExpr(*$1)); + } + delete $1; + } + | NUMERAL_TOK + { + $$ = new std::vector<CVC3::Expr>; + $$->push_back(VC->ratExpr(*$1)); + delete $1; + } +; + +attribute: + COLON_TOK SYM_TOK + { + $$ = $2; + } +; + +var: + QUESTION_TOK SYM_TOK + { + $$ = new CVC3::Expr(VC->idExpr(*$2)); + delete $2; + } +; + +fvar: + DOLLAR_TOK SYM_TOK + { + $$ = new CVC3::Expr(VC->idExpr(*$2)); + delete $2; + } +; + +%% |