diff options
Diffstat (limited to 'src/parser/smtlib.ypp')
-rw-r--r-- | src/parser/smtlib.ypp | 1509 |
1 files changed, 84 insertions, 1425 deletions
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index e616b3a65..8e6d99f6e 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,42 +11,29 @@ ** commands in SMT-LIB language. **/ -#include "smt/smt_engine.h" -#include "parser/parser_exception.h" +#include "cvc4_expr.h" #include "parser/parser_state.h" - -#include <vector> +#include "util/command.h" // Exported shared data namespace CVC4 { - extern ParserState* parserState; +namespace parser { + extern ParserState* _global_parser_state; +} } -// Define shortcuts for various things -#define TMP CVC4::parserState -#define EXPR CVC4::parserState->expr -#define VC (CVC4::parserState->vc) -#define ARRAYSENABLED (CVC4::parserState->arrFlag) -#define BVENABLED (CVC4::parserState->bvFlag) -#define BVSIZE (CVC4::parserState->bvSize) -#define RAT(args) CVC4::newRational args -#define QUERYPARSED CVC4::parserState->queryParsed -// Suppress the bogus warning suppression in bison (it generates -// compile error) +using namespace std; +using namespace CVC4; +using namespace CVC4::parser; + +// Suppress the bogus warning suppression in bison (it generates compile error) #undef __GNUC_MINOR__ -/* stuff that lives in smtlib.lex */ +/** stuff that lives in smtlib_scanner.lpp */ extern int smtliblex(void); -int smtliberror(const char *s) -{ - std::ostringstream ss; - ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum - << ": " << s; - return CVC4::parserState->error(ss.str()); -} - - +/** Error call */ +int smtliberror(const char *s) { return _global_parser_state->parseError(s); } #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 10485760 @@ -54,36 +41,29 @@ int smtliberror(const char *s) %} %union { - std::string *str; - std::vector<std::string> *strvec; - CVC4::Expr *node; - std::vector<CVC4::Expr> *vec; - std::pair<std::vector<CVC4::Expr>, std::vector<std::string> > *pat_ann; -}; + std::string *p_string; + std::vector<std::string*> *p_string_vector; + + CVC4::Expr *p_expression; + std::vector<CVC4::Expr*> *p_expression_vector; + + CVC4::Command *p_command; + std::vector<CVC4::Command*> *p_command_vector; -%start cmd + CVC4::parser::ParserState::BenchmarkStatus d_bench_status; + + CVC4::Kind d_kind; + +}; -/* strings are for better error messages. - "_TOK" is so macros don't conflict with kind names */ +%start benchmark -%type <vec> bench_attributes sort_symbs fun_symb_decls pred_symb_decls -%type <vec> an_exprs an_formulas quant_vars an_terms fun_symb fun_pred_symb -%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_expr 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 <p_string> NUMERAL_TOK +%token <p_string> SYM_TOK +%token <p_string> STRING_TOK +%token <p_string> USER_VAL_TOK -%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 @@ -94,20 +74,10 @@ int smtliberror(const char *s) %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 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 @@ -118,1424 +88,113 @@ int smtliberror(const char *s) %token EXTRASORTS_TOK %token EXTRAFUNS_TOK %token EXTRAPREDS_TOK +%token DISTINCT_TOK +%token COLON_TOK +%token LBRACKET_TOK +%token RBRACKET_TOK +%token LPAREN_TOK +%token RPAREN_TOK %token DOLLAR_TOK %token QUESTION_TOK -%token DISTINCT_TOK + %token EOF_TOK -%token PAT_TOK -%% -cmd: - benchmark - { - EXPR = *$1; - delete $1; - YYACCEPT; - } -; +%type <p_string> bench_name logic_name pred_symb attribute user_value +%type <d_bench_status> status +%type <p_expression> an_formula an_atom prop_atom +%type <p_expression_vector> an_formulas; +%type <d_kind> connective; + +%% benchmark: - LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK - { - if (!QUERYPARSED) - $4->push_back(CVC4::Expr(VC->listExpr("_CHECKSAT", CVC4::Expr(VC->idExpr("_TRUE_EXPR"))))); - $$ = new CVC4::Expr(VC->listExpr("_SEQ",*$4)); - delete $4; - } + LPAREN_TOK BENCHMARK_TOK bench_name bench_attributes RPAREN_TOK { + _global_parser_state->setBenchmarkName(*$3); + } | EOF_TOK - { - TMP->done = true; - $$ = new CVC4::Expr(); - } -; +; -bench_name: - SYM_TOK - { - $$ = NULL; - delete $1; - } -; +bench_name: SYM_TOK; bench_attributes: bench_attribute - { - $$ = new std::vector<CVC4::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 CVC4::Expr(VC->listExpr("_ASSERT", *$3)); - delete $3; - } - | COLON_TOK FORMULA_TOK an_formula - { - $$ = new CVC4::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; - CVC4::Expr cmd; - if (*$3 == "QF_UF") { - cmd = CVC4::Expr(VC->listExpr("_TYPE", VC->idExpr("U"))); - } - else if (*$3 == "QF_A" || - *$3 == "QF_AX") { - ARRAYSENABLED = true; - std::vector<CVC4::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")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFLIA" || - *$3 == "AUFLIA") { - ARRAYSENABLED = true; - std::vector<CVC4::Expr> tmp; - tmp.push_back(VC->listExpr("_TYPEDEF", VC->idExpr("Array"), - VC->listExpr("_ARRAY", - VC->idExpr("_INT"), - VC->idExpr("_INT")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFLIRA" || - *$3 == "AUFLIRA" || - *$3 == "QF_AUFNIRA" || - *$3 == "AUFNIRA") { - ARRAYSENABLED = true; - std::vector<CVC4::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")))); - cmd = CVC4::Expr(VC->listExpr("_SEQ", tmp)); - } - else if (*$3 == "QF_AUFBV" || - *$3 == "QF_ABV") { - ARRAYSENABLED = true; - BVENABLED = true; -// $$ = new CVC4::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; - } - // This enables the new arith for QF_LRA, but this results in assertion failures in DEBUG mode -// else if (*$3 == "QF_LRA") { -// cmd = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("arith-new"), VC->ratExpr(1))); -// } - - CVC4::Expr cmd2; - if (*$3 == "AUFLIA" || - *$3 == "AUFLIRA" || - *$3 == "AUFNIRA" || - *$3 == "LRA" || - *$3 == "UFNIA") { - cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("quant-complete-inst"), VC->ratExpr(1))); - } -// else if (*$3 == "QF_NIA" || -// *$3 == "QF_UFNRA") { -// cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("unknown-check-model"), VC->ratExpr(1))); -// } -// else if (*$3 == "QF_LIA" || -// *$3 == "QF_AUFLIA" || -// *$3 == "QF_AX") { -// cmd2 = CVC4::Expr(VC->listExpr("_OPTION", VC->stringExpr("pp-budget"), VC->ratExpr(5000))); -// } - - if (cmd.isNull()) { - if (cmd2.isNull()) { - $$ = NULL; - } - else $$ = new CVC4::Expr(cmd2); - } - else { - if (!cmd2.isNull()) { - cmd = CVC4::Expr(VC->listExpr("_SEQ", cmd, cmd2)); - } - $$ = new CVC4::Expr(cmd); - } - delete $3; - } - | COLON_TOK EXTRASORTS_TOK LPAREN_TOK sort_symbs RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_TYPE", *$4)); - delete $4; - } - | COLON_TOK EXTRAFUNS_TOK LPAREN_TOK fun_symb_decls RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4)); - delete $4; - } + | COLON_TOK FORMULA_TOK an_formula { _global_parser_state->addCommand(new CheckSatCommand(*$3)); delete $3; } + | COLON_TOK STATUS_TOK status { _global_parser_state->setBenchmarkStatus($3); } + | COLON_TOK LOGIC_TOK logic_name { _global_parser_state->setBenchmarkLogic(*$3); delete $3; } | COLON_TOK EXTRAPREDS_TOK LPAREN_TOK pred_symb_decls RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_SEQ", *$4)); - delete $4; - } - | COLON_TOK NOTES_TOK STRING_TOK - { - $$ = NULL; - delete $3; - } - | COLON_TOK CVC_COMMAND_TOK STRING_TOK - { - $$ = new CVC4::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<CVC4::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<CVC4::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; - } -; +; + +logic_name: SYM_TOK; -fun_sig: - fun_symb sort_symbs - { - if ($2->size() == 1) { - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), (*$2)[0])); - } - else { - CVC4::Expr tmp(VC->listExpr("_ARROW", *$2)); - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp)); - } - delete $1; - delete $2; - } +status: + SAT_TOK { $$ = ParserState::SATISFIABLE; } + | UNSAT_TOK { $$ = ParserState::UNSATISFIABLE; } + | UNKNOWN_TOK { $$ = ParserState::UNKNOWN; } ; pred_symb_decls: pred_symb_decl - { - $$ = new std::vector<CVC4::Expr>; - $$->push_back(*$1); - delete $1; - } - | - pred_symb_decls pred_symb_decl - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } + | pred_symb_decls pred_symb_decl ; 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<CVC4::Expr> tmp(*$2); - tmp.push_back(VC->idExpr("_BOOLEAN")); - CVC4::Expr tmp2(VC->listExpr("_ARROW", tmp)); - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), tmp2)); - delete $1; - delete $2; - } - | pred_symb - { - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$1), - VC->idExpr("_BOOLEAN"))); - delete $1; - } + pred_symb { _global_parser_state->declareNewPredicate(*$1); delete $1; } ; an_formulas: - an_formula - { - $$ = new std::vector<CVC4::Expr>; - $$->push_back(*$1); - delete $1; - } - | - an_formulas an_formula - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } + an_formula { $$ = new vector<Expr*>; $$->push_back($1); delete $1; } + | an_formulas an_formula { $$ = $1; $$->push_back($2); delete $2; } ; an_formula: an_atom - { - $$ = $1; - } - | LPAREN_TOK connective an_formulas annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK connective an_formulas RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - } - | LPAREN_TOK quant_symb quant_vars an_formula patterns_annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4, VC->listExpr((*$5).first))); - delete $2; - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK quant_symb quant_vars an_formula RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2, VC->listExpr(*$3), *$4)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_formula annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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 - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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 - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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 - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -patterns_annotations: - pattern - { - $$ = new std::pair<std::vector<CVC4::Expr>, std::vector<std::string> >; - $$->first.push_back(*$1); - delete $1; - } - | annotation - { - $$ = new std::pair<std::vector<CVC4::Expr>, std::vector<std::string> >; - $$->second.push_back(*$1); - delete $1; - } - | patterns_annotations pattern - { - $1->first.push_back(*$2); - $$ = $1; - delete $2; - } - | patterns_annotations annotation - { - $1->second.push_back(*$2); - $$ = $1; - delete $2; - } - -pattern: - PAT_TOK LCURBRACK_TOK an_exprs RCURBRACK_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$3)); - delete $3; - } - -quant_vars: - quant_var - { - $$ = new std::vector<CVC4::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 CVC4::Expr(VC->listExpr(*$2, *$3)); - delete $2; - delete $3; - } -; - -quant_symb: - EXISTS_TOK - { - $$ = new std::string("_EXISTS"); - } - | FORALL_TOK - { - $$ = new std::string("_FORALL"); - } + | LPAREN_TOK connective an_formulas RPAREN_TOK { $$ = _global_parser_state->newExpression($2, *$3); delete $3; } ; 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"); - } + NOT_TOK { $$ = NOT; } + | IMPLIES_TOK { $$ = IMPLIES; } + | IF_THEN_ELSE_TOK { $$ = ITE; } + | AND_TOK { $$ = AND; } + | OR_TOK { $$ = OR; } + | XOR_TOK { $$ = XOR; } + | IFF_TOK { $$ = 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 CVC4::Expr(VC->listExpr("_TRANS_CLOSURE", - *$2, (*$3)[0], (*$3)[1])); - } - else { - std::vector<CVC4::Expr> tmp; - tmp.push_back(*$2); - tmp.insert(tmp.end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(tmp)); - } - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK pred_symb an_terms RPAREN_TOK - { - std::vector<CVC4::Expr> tmp; - tmp.push_back(*$2); - tmp.insert(tmp.end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(tmp)); - delete $2; - delete $3; - } - | LPAREN_TOK DISTINCT_TOK an_terms annotations RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3)); - -// std::vector<CVC4::Expr> tmp; -// tmp.push_back(*$2); -// tmp.insert(tmp.end(), $3->begin(), $3->end()); -// $$ = new CVC4::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 CVC4::Expr(VC->listExpr("_AND", tmp)); - delete $3; - delete $4; - } - | LPAREN_TOK DISTINCT_TOK an_terms RPAREN_TOK - { - $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3)); -// std::vector<CVC4::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 CVC4::Expr(VC->listExpr("_AND", tmp)); - delete $3; - } -; +an_atom: prop_atom; prop_atom: - TRUE_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR")); - } - | FALSE_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR")); - } - | fvar - { - $$ = $1; - } - | pred_symb - { - $$ = $1; - } + TRUE_TOK { $$ = _global_parser_state->getNewTrue(); } + | FALSE_TOK { $$ = _global_parser_state->getNewFalse(); } + | pred_symb { $$ = _global_parser_state->getNewVariableByName(*$1); delete $1; } ; -an_terms: - an_term - { - $$ = new std::vector<CVC4::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 CVC4::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 CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - } - | LPAREN_TOK ITE_TOK an_formula an_term an_term annotations RPAREN_TOK - { - $$ = new CVC4::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 CVC4::Expr(VC->listExpr("_IF", *$3, *$4, *$5)); - delete $3; - delete $4; - delete $5; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_term annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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_term RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_term annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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_term RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -basic_term: - var - { - $$ = $1; - } - | fun_symb - { - if ($1->size() == 1) { - $$ = new CVC4::Expr(((*$1)[0])); - } - else { - $$ = new CVC4::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 CVC4::Expr(VC->listExpr("_BITVECTOR", VC->ratExpr(*$3))); - } - else { - $$ = new CVC4::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 CVC4::Expr(VC->listExpr("_ARRAY", - VC->listExpr("_BITVECTOR", VC->ratExpr(*$3)), - VC->listExpr("_BITVECTOR", VC->ratExpr(*$5)))); - } - else { - $$ = new CVC4::Expr(VC->listExpr(*$1, VC->ratExpr(*$3), VC->ratExpr(*$5))); - } - delete $1; - delete $3; - delete $5; - } - | SYM_TOK - { - if (*$1 == "Real") { - $$ = new CVC4::Expr(VC->idExpr("_REAL")); - } else if (*$1 == "Int") { - $$ = new CVC4::Expr(VC->idExpr("_INT")); - } else { - $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } -; - -pred_symb: - SYM_TOK - { - if (BVENABLED && (*$1 == "bvlt" || *$1 == "bvult")) { - $$ = new CVC4::Expr(VC->idExpr("_BVLT")); - } - else if (BVENABLED && (*$1 == "bvleq" || *$1 == "bvule")) { - $$ = new CVC4::Expr(VC->idExpr("_BVLE")); - } - else if (BVENABLED && (*$1 == "bvgeq" || *$1 == "bvuge")) { - $$ = new CVC4::Expr(VC->idExpr("_BVGE")); - } - else if (BVENABLED && (*$1 == "bvgt" || *$1 == "bvugt")) { - $$ = new CVC4::Expr(VC->idExpr("_BVGT")); - } - else if (BVENABLED && *$1 == "bvslt") { - $$ = new CVC4::Expr(VC->idExpr("_BVSLT")); - } - else if (BVENABLED && (*$1 == "bvsleq" || *$1 == "bvsle")) { - $$ = new CVC4::Expr(VC->idExpr("_BVSLE")); - } - else if (BVENABLED && (*$1 == "bvsgeq" || *$1 == "bvsge")) { - $$ = new CVC4::Expr(VC->idExpr("_BVSGE")); - } - else if (BVENABLED && *$1 == "bvsgt") { - $$ = new CVC4::Expr(VC->idExpr("_BVSGT")); - } - else { - $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } - | AR_SYMB - { - if ($1->length() == 1) { - switch ((*$1)[0]) { - case '=': $$ = new CVC4::Expr(VC->idExpr("_EQ")); break; - case '<': $$ = new CVC4::Expr(VC->idExpr("_LT")); break; - case '>': $$ = new CVC4::Expr(VC->idExpr("_GT")); break; - default: $$ = new CVC4::Expr(VC->idExpr(*$1)); break; - } - } - else { - if (*$1 == "<=") { - $$ = new CVC4::Expr(VC->idExpr("_LE")); - } else if (*$1 == ">=") { - $$ = new CVC4::Expr(VC->idExpr("_GE")); - } - else $$ = new CVC4::Expr(VC->idExpr(*$1)); - } - delete $1; - } -; - -fun_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector<CVC4::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<CVC4::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<CVC4::Expr>; - 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 == "bvnand") { - $$->push_back(VC->idExpr("_BVNAND")); - } - else if (BVENABLED && *$1 == "bvnor") { - $$->push_back(VC->idExpr("_BVNOR")); - } - 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<CVC4::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<CVC4::Expr>; - $$->push_back(VC->ratExpr(*$1)); - delete $1; - } -; - -attribute: - COLON_TOK SYM_TOK - { - $$ = $2; - } -; - -var: - QUESTION_TOK SYM_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_"+*$2)); - delete $2; - } -; - -fvar: - DOLLAR_TOK SYM_TOK - { - $$ = new CVC4::Expr(VC->idExpr("_"+*$2)); - delete $2; - } -; - -an_exprs: - an_expr - { - $$ = new std::vector<CVC4::Expr>; - $$->push_back(*$1); - delete $1; - } - | - an_exprs an_expr - { - $1->push_back(*$2); - $$ = $1; - delete $2; - } -; - -an_expr: - var - { - $$ = $1; - } - | fvar - { - $$ = $1; - } - | LPAREN_TOK fun_pred_symb an_terms annotations RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - delete $4; - } - | LPAREN_TOK fun_pred_symb an_terms RPAREN_TOK - { - $2->insert($2->end(), $3->begin(), $3->end()); - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - delete $3; - } - | LPAREN_TOK LET_TOK LPAREN_TOK var an_term RPAREN_TOK an_expr annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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_expr RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } - | LPAREN_TOK FLET_TOK LPAREN_TOK fvar an_formula RPAREN_TOK an_expr annotations RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::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_expr RPAREN_TOK - { - CVC4::Expr e(VC->listExpr(VC->listExpr(*$4, *$5))); - $$ = new CVC4::Expr(VC->listExpr("_LET", e, *$7)); - delete $4; - delete $5; - delete $7; - } -; - -fun_pred_symb: - SYM_TOK LBRACKET_TOK NUMERAL_TOK RBRACKET_TOK - { - $$ = new std::vector<CVC4::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<CVC4::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<CVC4::Expr>; - 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 == "bvnand") { - $$->push_back(VC->idExpr("_BVNAND")); - } - else if (BVENABLED && *$1 == "bvnor") { - $$->push_back(VC->idExpr("_BVNOR")); - } - 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")); - } + attribute { delete $1; } + | attribute user_value { delete $1; delete $2; } + ; - // predicates - else 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")); - } +user_value: USER_VAL_TOK; - // 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")); - } +pred_symb: SYM_TOK; - // 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<CVC4::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<CVC4::Expr>; - $$->push_back(VC->ratExpr(*$1)); - delete $1; - } -; +attribute: + COLON_TOK SYM_TOK { $$ = $2; } + ; %% |