summaryrefslogtreecommitdiff
path: root/src/parser/smtlib.ypp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/smtlib.ypp')
-rw-r--r--src/parser/smtlib.ypp1553
1 files changed, 1553 insertions, 0 deletions
diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp
new file mode 100644
index 000000000..1bc22675a
--- /dev/null
+++ b/src/parser/smtlib.ypp
@@ -0,0 +1,1553 @@
+%{
+/*****************************************************************************/
+/*!
+ * \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 CVC4 {
+ extern ParserTemp* parserTemp;
+}
+// Define shortcuts for various things
+#define TMP CVC4::parserTemp
+#define EXPR CVC4::parserTemp->expr
+#define VC (CVC4::parserTemp->vc)
+#define ARRAYSENABLED (CVC4::parserTemp->arrFlag)
+#define BVENABLED (CVC4::parserTemp->bvFlag)
+#define BVSIZE (CVC4::parserTemp->bvSize)
+#define RAT(args) CVC4::newRational args
+#define QUERYPARSED CVC4::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 << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+ << ": " << s;
+ return CVC4::parserTemp->error(ss.str());
+}
+
+
+
+#define YYLTYPE_IS_TRIVIAL 1
+#define YYMAXDEPTH 10485760
+
+%}
+
+%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;
+};
+
+
+%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_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 <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 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 DOLLAR_TOK
+%token QUESTION_TOK
+%token DISTINCT_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(CVC4::Expr(VC->listExpr("_CHECKSAT", CVC4::Expr(VC->idExpr("_TRUE_EXPR")))));
+ $$ = new CVC4::Expr(VC->listExpr("_SEQ",*$4));
+ delete $4;
+ }
+ | EOF_TOK
+ {
+ TMP->done = true;
+ $$ = new CVC4::Expr();
+ }
+;
+
+bench_name:
+ SYM_TOK
+ {
+ $$ = NULL;
+ delete $1;
+ }
+;
+
+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 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;
+ }
+;
+
+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;
+ }
+;
+
+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_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;
+ }
+;
+
+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:
+ 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");
+ }
+;
+
+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 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;
+ }
+;
+
+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;
+ }
+;
+
+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"));
+ }
+
+ // 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"));
+ }
+
+ // 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;
+ }
+;
+
+
+
+%%
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback