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.ypp1509
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; }
+ ;
%%
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback