#include "cvc4.h"
#include "parser/parser_exception.h"
#include "parser/parser_state.h"
+#include "cvc4_expr.h"
+#include "expr/expr_builder.h"
+#include "expr/expr_manager.h"
+#include "util/command.h"
//#include "rational.h"
// Exported shared data
#define TMP CVC4::parser::parserState
#define EXPR CVC4::parser::parserState->expr
#define VC (CVC4::parser::parserState->vc)
+#define EM (CVC4::parser::parserState->exprManager)
#define RAT(args) CVC4::newRational args
// Suppress the bogus warning suppression in bison (it generates
return CVC4::parser::parserState->error(ss.str());
}
-
-namespace CVC4 {
-
-// File-static auxiliary funcion to wrap accessors upto the index i
-// (not inclusive) around "e". Used to rebuild the UPDATE expressions.
-static Expr wrapAccessors(const Expr& e,
- const std::vector<Expr>& accessors,
- const int i) {
- DebugAssert((int)accessors.size() >= i, "wrapAccessors: too few accessors");
- Expr res(e);
- for(int j=0; j<i; j++) {
- const Expr& acc = accessors[j];
- switch(acc.getKind()) {
- case ID: // Datatype: apply the accessor directly to 'res'
- res = VC->listExpr(acc, res);
- break;
- case RAW_LIST:
- DebugAssert(acc.arity() == 2 && acc[0].getKind() == ID,
- "PL.y: wrong number of arguments in the accessor of WITH: "
- +acc.toString());
- res = VC->listExpr(acc[0], res, acc[1]);
- break;
- default:
- DebugAssert(false, "PL.y: Bad accessor in WITH: "+acc.toString());
- }
- }
- return res;
-}
-
-// Convert a complex WITH statement into a bunch of nested simple UPDATEs
-
-// Updator "e1 WITH accessors := e2" is represented as
-// (e1 (accessor1 accessor2 ... ) e2), where the accessors are:
-// (READ idx)
-// ID (datatype constructor's argument)
-// (RECORD_SELECT ID)
-// and (TUPLE_SELECT num).
-
-// We rebuild this into nested RECORD_UPDATE, WRITE,
-// TUPLE_UPDATE, and DATATYPE_UPDATE expressions. For example:
-//
-// e WITH [idx] car.f := newVal is transformed into
-// e WITH [idx] := (e[idx] WITH car := (car(e[idx]) WITH .f := newVal))
-// which is represented as
-// (WRITE e idx
-// (DATATYPE_UPDATE (READ e idx) car
-// (RECORD_UPDATE (car (READ e idx)) f newVal))).
-// Here "car" and "f" are identifiers (ID "car") and (ID "f").
-
-static Expr PLprocessUpdate(const CVC4::Expr& e,
- const CVC4::Expr& update) {
- TRACE("parser verbose", "PLprocessUpdate(", e, ") {");
- DebugAssert(update.arity() == 2,"PL.y: Bad WITH statement: "
- +update.toString());
- // Rebuild accessors: resolve ID in (READ (ID "name")) and leave
- // the rest alone
- TRACE("parser verbose", "PLprocessUpdate: update[0] = ", update[0], "");
- std::vector<Expr> acc;
- for(Expr::iterator i=update[0].begin(), iend=update[0].end(); i!=iend; ++i) {
- TRACE("parser verbose", "*i = ", *i, "");
- acc.push_back(*i);
- }
- TRACE("parser verbose", "acc.size() = ", acc.size(), "");
- TRACE("parser verbose", "accessors = ", VC->listExpr(acc), "");
- // 'res' serves as the accumulator of updators; initially it is
- // newVal (which is update[1]). We run through accessors in reverse
- // order, wrapping this accumulator with the corresponding
- // updators.
- Expr res(update[1]);
- // Rebuilding the original expression "e"
- // The main loop
- for(int i=acc.size()-1; i>=0; i--) {
- Expr ac(acc[i]); // The current accessor
- TRACE("parser verbose", "ac["+int2string(i)+"] = ", ac, "");
- // "e" with all preceding accessors
- Expr tmp(wrapAccessors(e, acc, i));
- TRACE("parser verbose", "tmp = ", tmp, "");
- switch(ac.getKind()) {
- case ID: // Datatype update
- res = VC->listExpr("_DATATYPE_UPDATE", tmp, ac, res);
- break;
- case RAW_LIST: {
- const std::string& kind = ac[0][0].getString();
- if(kind == "_READ") // Array update
- res = VC->listExpr("_WRITE", tmp, ac[1], res);
- else if(kind == "_RECORD_SELECT") // Record update
- res = VC->listExpr("_RECORD_UPDATE", tmp, ac[1], res);
- else if(kind == "_TUPLE_SELECT") // Tuple element
- res = VC->listExpr("_TUPLE_UPDATE", tmp, ac[1], res);
- else
- DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString());
- break;
- }
- default:
- DebugAssert(false, "PL.y: Bad accessor in WITH: "+ac.toString());
- }
- }
- TRACE("parser verbose", "PLprocessUpdate => ", res, " }");
- return res;
-}
-
-
-// Process a vector of simultaneous updates (from a single WITH)
-static Expr PLprocessUpdates(const CVC4::Expr& e,
- const std::vector<CVC4::Expr>& updates,
- size_t idx=0) {
- // Processed all the updates
- if(idx >= updates.size()) return e;
- return PLprocessUpdates(PLprocessUpdate(e, updates[idx]), updates, idx+1);
-}
-
-
-
-} // end of namespace CVC4
-
#define YYLTYPE_IS_TRIVIAL 1
#define YYMAXDEPTH 10485760
/* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */
#define YYERROR_VERBOSE 1
+
+using namespace CVC4;
+
%}
%union {
std::string *str;
- CVC4::Expr *node;
+ CVC4::Expr *expr;
+ CVC4::Command *cmd;
std::vector<CVC4::Expr> *vec;
int kind;
};
-%start cmd
+// %start cmd
+%start Query
/* strings are for better error messages.
"_TOK" is so macros don't conflict with kind names */
%nonassoc '{' '.' '('
%nonassoc BITVECTOR_TOK
-%type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors
-%type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls
-%type <vec> Exprs AndExpr OrExpr Pattern Patterns
-%type <vec> RecordEntries UpdatePosition Updates
-
-%type <node> Type /* IndexType */ TypeNotIdentifier TypeDef
-%type <node> DataType SingleDataType Constructor
-%type <node> FunctionType RecordType Real Int BitvectorType
-%type <node> FieldDecl TupleType
-%type <node> ArrayType ScalarType SubType BasicType SubrangeType
-%type <node> LeftBound RightBound
-%type <node> Expr Conditional UpdatePositionNode Update Lambda
-%type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral
-%type <node> LetDecl LetExpr LetDeclsNode
-%type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
-%type <node> BoundVarDecl BoundVarDeclNode VarDecl
-%type <node> ConstDecl TypeDecl
-%type <node> Identifier StringLiteral Numeral Binary Hex
-
-%type <node> Assert Query Help Dbg Trace Option
-%type <node> Transform Print Call Echo DumpCommand
-%type <node> Include Where Push Pop PopTo
-%type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute
-%type <node> other_cmd
-%type <node> Arith_Var_Order
+// %type <vec> FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors
+// %type <vec> LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls
+// %type <vec> Exprs AndExpr OrExpr Pattern Patterns
+// %type <vec> RecordEntries UpdatePosition Updates
+
+// %type <node> Type /* IndexType */ TypeNotIdentifier TypeDef
+// %type <node> DataType SingleDataType Constructor
+// %type <node> FunctionType RecordType Real Int BitvectorType
+// %type <node> FieldDecl TupleType
+// %type <node> ArrayType ScalarType SubType BasicType SubrangeType
+// %type <node> LeftBound RightBound
+%type <expr> Expr // Conditional UpdatePositionNode Update Lambda
+// %type <node> QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral
+// %type <node> LetDecl LetExpr LetDeclsNode
+// %type <node> TypeLetDecl TypeLetExpr TypeLetDeclsNode
+// %type <node> BoundVarDecl BoundVarDeclNode VarDecl
+// %type <node> ConstDecl TypeDecl
+ // %type <expr> Identifier // StringLiteral Numeral Binary Hex
+
+ // %type <cmd> cmd Assert Query // Help Dbg Trace Option
+%type <cmd> Query // Help Dbg Trace Option
+// %type <node> Transform Print Call Echo DumpCommand
+// %type <node> Include Where Push Pop PopTo
+// %type <node> Context Forget Get_Child Get_Op Get_Type Check_Type Substitute
+// %type <node> other_cmd
+// %type <node> Arith_Var_Order
%token <str> ID_TOK STRINGLIT_TOK NUMERAL_TOK HEX_TOK BINARY_TOK
%%
-cmd : TypeDecl ';'
- {
- EXPR = *$1;
- delete $1;
- YYACCEPT;
- }
- | ConstDecl ';'
- {
- EXPR = *$1;
- delete $1;
- YYACCEPT;
- }
- | other_cmd ';' {
- EXPR = *$1;
- delete $1;
- YYACCEPT;
- }
- | ';'
- {
- EXPR = CVC4::Expr();
- YYACCEPT;
- }
- | DONE_TOK
- {
- TMP->done = true;
- EXPR = CVC4::Expr();
- YYACCEPT;
- }
- ;
-
-other_cmd : Assert { $$ = $1; }
- | Query { $$ = $1; }
- | Dbg { $$ = $1; }
- | Trace { $$ = $1; }
- | Option { $$ = $1; }
- | Help { $$ = $1; }
- | Transform { $$ = $1; }
- | Print { $$ = $1; }
- | Call { $$ = $1; }
- | Echo { $$ = $1; }
- | Include { $$ = $1; }
- | DumpCommand { $$ = $1; }
- | Where { $$ = $1; }
- | Push { $$ = $1; }
- | Pop { $$ = $1; }
- | PopTo { $$ = $1; }
- | Context { $$ = $1; }
- | Substitute { $$ = $1; }
- | Get_Child { $$ = $1; }
- | Get_Op { $$ = $1; }
- | Get_Type { $$ = $1; }
- | Check_Type { $$ = $1; }
- | Forget { $$ = $1; }
- | Arith_Var_Order { $$ = $1; }
- ;
-
-Arith_Var_Order : ARITH_VAR_ORDER_TOK '(' Exprs ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_ARITH_VAR_ORDER", *$3));
- delete $3;
- }
- ;
-
-Assert : ASSERT_TOK Expr {
-
- $$ = new CVC4::Expr(VC->listExpr("_ASSERT", *$2));
- delete $2;
- }
- ;
-
-Query : QUERY_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_QUERY", *$2));
- delete $2;
- }
- | CHECKSAT_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_CHECKSAT", *$2));
- delete $2;
- }
- | CHECKSAT_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CHECKSAT")));
- }
- | CONTINUE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTINUE")));
- }
- | RESTART_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_RESTART", *$2));
- delete $2;
- }
- ;
-Dbg : DBG_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_DBG", *$2));
- delete $2;
- }
- | DBG_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DBG")));
- }
- ;
-Trace : TRACE_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_TRACE", *$2));
- delete $2;
- }
- | UNTRACE_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_UNTRACE", *$2));
- delete $2;
- }
- ;
-Option : OPTION_TOK StringLiteral Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, *$3));
- delete $2;
- delete $3;
- }
- | OPTION_TOK StringLiteral MINUS_TOK Numeral {
- CVC4::Rational value= -$4->getRational();
- CVC4::Expr e = CVC4::Expr(VC->ratExpr(value.toString()));
- $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, e));
- delete $2;
- delete $4;
- }
- | OPTION_TOK StringLiteral StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_OPTION", *$2, *$3));
- delete $2;
- delete $3;
- }
- ;
-Help : HELP_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_HELP", *$2));
- delete $2;
- }
- | HELP_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_HELP")));
- }
- ;
-
-Transform : TRANSFORM_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_TRANSFORM", *$2));
- delete $2;
- }
- ;
-
-Print : PRINT_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2));
- delete $2;
- }
- | PRINT_TYPE_TOK Type {
- $$ = new CVC4::Expr(VC->listExpr("_PRINT", *$2));
- delete $2;
- }
- ;
-
-Call : CALL_TOK Identifier Expr {
- $$ = new CVC4::Expr(VC->listExpr("_CALL", *$2, *$3));
- delete $2;
- delete $3;
- }
- ;
-
-Echo : ECHO_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_ECHO", *$2));
- delete $2;
- }
- | ECHO_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ECHO")));
- }
- ;
-
-Include : INCLUDE_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_INCLUDE", *$2));
- delete $2;
- }
- ;
-
-DumpCommand : DUMP_PROOF_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_PROOF")));
- }
- | DUMP_ASSUMPTIONS_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_ASSUMPTIONS")));
- }
- | DUMP_SIG_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_SIG")));
- }
- | DUMP_TCC_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC")));
- }
- | DUMP_TCC_ASSUMPTIONS_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_ASSUMPTIONS")));
- }
- | DUMP_TCC_PROOF_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_TCC_PROOF")));
- }
- | DUMP_CLOSURE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE")));
- }
- | DUMP_CLOSURE_PROOF_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_DUMP_CLOSURE_PROOF")));
- }
- ;
-
-Where : WHERE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_WHERE")));
- }
- | ASSERTIONS_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSERTIONS")));
- }
- | ASSUMPTIONS_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_ASSUMPTIONS")));
- }
- | COUNTEREXAMPLE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTEREXAMPLE")));
- }
- | COUNTERMODEL_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_COUNTERMODEL")));
- }
- ;
-Push : PUSH_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_PUSH", *$2));
- delete $2;
- }
- | PUSH_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH")));
- }
- | PUSH_SCOPE_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_PUSH_SCOPE", *$2));
- delete $2;
- }
- | PUSH_SCOPE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_PUSH_SCOPE")));
- }
- ;
-Pop : POP_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_POP", *$2));
- delete $2;
- }
- | POP_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP")));
- }
- | POP_SCOPE_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_POP_SCOPE", *$2));
- delete $2;
- }
- | POP_SCOPE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POP_SCOPE")));
- }
- ;
-PopTo : POPTO_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_POPTO", *$2));
- delete $2;
- }
- | POPTO_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO")));
- }
- | POPTO_SCOPE_TOK Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_POPTO_SCOPE", *$2));
- delete $2;
- }
- | POPTO_SCOPE_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POPTO_SCOPE")));
- }
- | RESET_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_RESET")));
- }
- ;
-Context : CONTEXT_TOK StringLiteral {
- $$ = new CVC4::Expr(VC->listExpr("_CONTEXT", *$2));
- delete $2;
- }
- | CONTEXT_TOK {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_CONTEXT")));
- }
- ;
-Forget : FORGET_TOK Identifier {
- $$ = new CVC4::Expr(VC->listExpr("_FORGET", *$2));
- delete $2;
- }
- ;
-Get_Type : GET_TYPE_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_GET_TYPE", *$2));
- delete $2;
- }
- ;
-Check_Type : CHECK_TYPE_TOK Expr ':' Type {
- $$ = new CVC4::Expr(VC->listExpr("_CHECK_TYPE",*$2, *$4));
- delete $2;
- delete $4;
- }
- ;
-Get_Child : GET_CHILD_TOK Expr Numeral {
- $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2, *$3));
- delete $2;
- delete $3;
- }
- ;
-Get_Op : GET_OP_TOK Expr {
- $$ = new CVC4::Expr(VC->listExpr("_GET_CHILD", *$2));
- delete $2;
- }
- ;
-Substitute : SUBSTITUTE_TOK Identifier ':' Type '=' Expr '[' Identifier ASSIGN_TOK Expr ']' {
- std::vector<CVC4::Expr> tmp;
- tmp.push_back(*$2);
- tmp.push_back(*$4);
- tmp.push_back(*$6);
- tmp.push_back(*$8);
- tmp.push_back(*$10);
- $$ = new CVC4::Expr(VC->listExpr("_SUBSTITUTE", tmp));
- delete $2;
- delete $4;
- delete $6;
- delete $8;
- delete $10;
- }
- ;
-Identifier : ID_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr(*$1));
- delete $1;
- }
- ;
-StringLiteral : STRINGLIT_TOK
- {
- $$ = new CVC4::Expr(VC->stringExpr(*$1));
- delete $1;
- }
- ;
-Numeral : NUMERAL_TOK
- {
- $$ = new CVC4::Expr(VC->ratExpr((*$1)));
- delete $1;
- }
- ;
-
-Binary : BINARY_TOK
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVCONST", VC->stringExpr(*$1)));
- delete $1;
- }
- ;
-
-
-Hex : HEX_TOK
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVCONST", VC->stringExpr(*$1), VC->ratExpr(16)));
- delete $1;
- }
- ;
-
-
-/* Grammar for Types */
-
-Type : Identifier { $$ = $1; }
- | TypeNotIdentifier { $$ = $1; }
- ;
-
-TypeNotIdentifier: ArrayType { $$ = $1; }
- | FunctionType { $$ = $1; }
- | BasicType { $$ = $1; }
- | SubrangeType { $$ = $1; }
- | TupleType { $$ = $1; }
- | RecordType { $$ = $1; }
- | TypeLetExpr { $$ = $1; }
- | BitvectorType {$$ = $1;}
- | SubType { $$ = $1; }
- | '(' Type ')' { $$ = $2; }
- ;
-
-TypeDef : Type { $$ = $1; }
- | ScalarType { $$ = $1; }
- ;
-
-DataType : DATATYPE_TOK SingleDataTypes END_TOK
- {
- $$ = new CVC4::Expr(
- VC->listExpr("_TYPEDEF",
- VC->listExpr("_DATATYPE", *$2)));
- delete $2;
- }
- ;
-
-SingleDataTypes : SingleDataType
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | SingleDataTypes ',' SingleDataType
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-SingleDataType : Identifier '=' Constructors
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, VC->listExpr(*$3)));
- delete $1;
- delete $3;
- }
- ;
-
-Constructors : Constructor
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | Constructors MID_TOK Constructor
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-Constructor : Identifier
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
- }
- | Identifier '(' VarDecls ')'
- {
- CVC4::Expr tmp = VC->listExpr(*$3);
- $$ = new CVC4::Expr(VC->listExpr(*$1, tmp));
- delete $1; delete $3;
- }
- ;
-
-VarDecls : VarDecl
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | VarDecls ',' VarDecl
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-VarDecl : Identifier ':' Type
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
- delete $1;
- delete $3;
- }
- ;
-
-FunctionType : '[' Type ARROW_TOK Type ']'
- {
- // Old style functions
- $$ = new CVC4::Expr(VC->listExpr("_OLD_ARROW", *$2, *$4));
- delete $2; delete $4;
- }
- | Type ARROW_TOK Type
- {
- std::vector<CVC4::Expr> temp;
- temp.push_back(*$1);
- temp.push_back(*$3);
-
- $$ = new CVC4::Expr(VC->listExpr("_ARROW", temp));
- delete $1; delete $3;
- }
- | '(' TypeList ')' ARROW_TOK Type
- {
- $2->push_back(*$5);
- $$ = new CVC4::Expr(VC->listExpr("_ARROW", *$2));
- delete $2; delete $5;
- }
- ;
-
-RecordType : SQHASH_TOK FieldDecls HASHSQ_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr(*$2));
- delete $2;
- }
- ;
+// cmd:
+// Assert { $$ = $1; }
+// | Query { $$ = $1; }
-FieldDecls : FieldDecl
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->idExpr("_RECORD_TYPE"));
- $$->push_back(*$1);
- delete $1;
- }
- | FieldDecls ',' FieldDecl
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
+// Assert:
+// ASSERT_TOK Expr {
+// $$ = NULL; // new CVC3::Expr(VC->listExpr("_ASSERT", *$2));
+// // delete $2;
+// } ;
-FieldDecl : Identifier ':' Type
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
- delete $1;
- delete $3;
- }
- ;
-
-TupleType : '[' TypeList ']'
- {
- $$ = new CVC4::Expr(VC->listExpr("_TUPLE_TYPE", *$2));
- delete $2;
- }
- ;
-
-TypeList : Type ',' Type
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- $$->push_back(*$3);
- delete $1;
- delete $3;
- }
- | TypeList ',' Type
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-/* IndexType : SubrangeType { $$ = $1; } */
-/* | Real /\* WART: maybe change to INTEGER when we */
-/* get that working? *\/ */
-/* | Int */
-/* { $$ = $1; } */
-/* | Identifier { $$ = $1; } */
-/* ; */
-
-ArrayType : ARRAY_TOK Type OF_TOK Type
- {
- $$ = new CVC4::Expr(VC->listExpr("_ARRAY", *$2, *$4));
- delete $2;
- delete $4;
- }
- ;
-
-ScalarType : '{' IDs '}'
- {
- std::vector<CVC4::Expr>::iterator theIter = $2->begin();
- $2->insert(theIter, VC->idExpr("_SCALARTYPE"));
- $$ = new CVC4::Expr(VC->listExpr(*$2));
- delete $2;
- }
- ;
-
-SubType : SUBTYPE_TOK '(' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3));
- delete $3;
- }
- | SUBTYPE_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_SUBTYPE", *$3, *$5));
- delete $3;
- delete $5;
- }
- ;
-
-BasicType : BOOLEAN_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr("_BOOLEAN"));
- }
- | Real
- | Int
- ;
-
-BitvectorType : BITVECTOR_TOK '(' Numeral ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BITVECTOR", *$3));
- delete $3;
- }
- ;
-
-Real : REAL_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr("_REAL"));
- }
- ;
-
-Int : INT_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr("_INT"));
- }
- ;
-SubrangeType : '[' LeftBound DOTDOT_TOK RightBound ']'
- {
- $$ = new CVC4::Expr(VC->listExpr("_SUBRANGE", *$2, *$4));
- delete $2;
- delete $4;
- }
- ;
-
-LeftBound : '_'
- {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_NEGINF")));
- }
- | Numeral { $$ = $1; }
- | MINUS_TOK Numeral {
- CVC4::Rational value= -$2->getRational();
- $$ = new CVC4::Expr(VC->ratExpr(value.toString()));
- delete $2;
- }
- ;
-
-RightBound : '_'
- {
- $$ = new CVC4::Expr(VC->listExpr(VC->idExpr("_POSINF")));
- }
- | Numeral { $$ = $1; }
- | MINUS_TOK Numeral {
- CVC4::Rational value= -$2->getRational();
- $$ = new CVC4::Expr(VC->ratExpr(value.toString()));
- delete $2;
- }
- ;
-
-/* right recursive to eliminate a conflict. Reverses order? */
-reverseIDs : Identifier
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | Identifier ',' reverseIDs
- {
- $3->push_back(*$1);
- $$ = $3;
- delete $1;
- }
- ;
-
-IDs : reverseIDs
- {
- $$ = new std::vector<CVC4::Expr>($1->rbegin(),
- $1->rend());
- delete $1;
- }
- ;
-
-/* Grammar for exprs */
-
-Expr : Identifier { $$ = $1; }
- | Numeral { $$ = $1; }
- | Binary { $$ = $1; }
- | Hex { $$ = $1; }
- | Expr '(' Exprs ')'
- {
- std::vector<CVC4::Expr> tmp;
- tmp.push_back(*$1);
- tmp.insert(tmp.end(), $3->begin(), $3->end());
- $$ = new CVC4::Expr(VC->listExpr(tmp));
- delete $1;
- delete $3;
- }
- | SIMULATE_TOK '(' Exprs ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_SIMULATE", *$3));
- delete $3;
- }
- | Expr '[' Expr ']'
- {
- $$ = new CVC4::Expr(VC->listExpr("_READ", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr '.' Identifier
- {
- $$ = new CVC4::Expr(VC->listExpr("_RECORD_SELECT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr '.' Numeral
- {
- $$ = new CVC4::Expr(VC->listExpr("_TUPLE_SELECT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr WITH_TOK Updates
- {
- $$ = new CVC4::Expr(CVC4::PLprocessUpdates(*$1, *$3));
- delete $1;
- delete $3;
- }
- | Lambda { $$ = $1; }
- | QuantExpr { $$ = $1; }
- | LetExpr { $$ = $1; }
-
- | ArrayLiteral { $$ = $1; }
-
- | RecordLiteral { $$ = $1; }
- | TupleLiteral { $$ = $1; }
- | Conditional { $$ = $1; }
-
- | TRUELIT_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr("_TRUE_EXPR"));
- }
- | FALSELIT_TOK
- {
- $$ = new CVC4::Expr(VC->idExpr("_FALSE_EXPR"));
- }
-
- | MINUS_TOK Expr %prec UMINUS_TOK
- {
- if ($2->isRational())
- {
- CVC4::Rational value= -$2->getRational();
- $$= new CVC4::Expr(VC->ratExpr(value.toString()));
- }
- else
- $$ = new CVC4::Expr(VC->listExpr("_UMINUS", *$2));
- delete $2;
- }
- | NOT_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_NOT", *$2));
- delete $2;
- }
- | IS_INTEGER_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_IS_INTEGER", *$2));
- delete $2;
- }
- | TCC_TOK '(' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_TCC", *$3));
- delete $3;
- }
- | Expr '=' Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_EQ", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr NEQ_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_NEQ", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr XOR_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_XOR", *$1, *$3));
- delete $1;
- delete $3;
- }
- | OrExpr %prec OR_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_OR", *$1));
- delete $1;
- }
- | AndExpr %prec AND_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_AND", *$1));
- delete $1;
- }
- | Expr IMPLIES_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_IMPLIES", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr IFF_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_IFF", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr PLUS_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_PLUS", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr MINUS_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_MINUS", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr MULT_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_TRANS_CLOSURE",
- *$1, *$4, *$6));
- delete $1;
- delete $4;
- delete $6;
- }
- | Expr MULT_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_MULT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr POW_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_POW", *$3, *$1));
- delete $1;
- delete $3;
- }
- | Expr DIV_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_DIVIDE", *$1, *$3));
- delete $1;
- delete $3;
- }
-// | Expr INTDIV_TOK Expr
-// {
-// $$ = new CVC4::Expr(VC->listExpr("_INTDIV", *$1, *$3));
-// delete $1;
-// delete $3;
-// }
-// | Expr MOD_TOK Expr
-// {
-// $$ = new CVC4::Expr(VC->listExpr("_MOD", *$1, *$3));
-// delete $1;
-// delete $3;
-// }
- | Expr GT_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_GT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr GE_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_GE", *$1, *$3));
- delete $1;
- delete $3;
- }
- | FLOOR_TOK '(' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_FLOOR", *$3));
- delete $3;
- }
- | Expr LT_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_LT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr LE_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_LE", *$1, *$3));
- delete $1;
- delete $3;
- }
- | '(' Expr ')'
- {
- $$ = $2;
- }
- | BVNEG_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVNEG", *$2));
- delete $2;
- }
- | Expr '[' NUMERAL_TOK ':' NUMERAL_TOK ']'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_EXTRACT", VC->ratExpr(*$3),
- VC->ratExpr(*$5), *$1));
- delete $1;
- delete $3;
- delete $5;
- }
- | Expr BVAND_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVAND", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr MID_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVOR", *$1, *$3));
- delete $1;
- delete $3;
- }
- | Expr LEFTSHIFT_TOK NUMERAL_TOK
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_LEFTSHIFT", *$1, VC->ratExpr(*$3)));
- delete $1;
- delete $3;
- }
- | Expr RIGHTSHIFT_TOK NUMERAL_TOK
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_RIGHTSHIFT", *$1, VC->ratExpr(*$3)));
- delete $1;
- delete $3;
- }
- | BVXOR_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVXOR", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVNAND_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVNAND", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVNOR_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVNOR", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVCOMP_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVCOMP", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVXNOR_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVXNOR", *$3, *$5));
- delete $3;
- delete $5;
- }
- | SX_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_SX",*$3,VC->ratExpr(*$5)));
- delete $3;
- delete $5;
- }
- | BVZEROEXTEND_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVZEROEXTEND",VC->ratExpr(*$5),*$3));
- delete $3;
- delete $5;
- }
- | BVREPEAT_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVREPEAT",VC->ratExpr(*$5),*$3));
- delete $3;
- delete $5;
- }
- | BVROTL_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVROTL",VC->ratExpr(*$5),*$3));
- delete $3;
- delete $5;
- }
- | BVROTR_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVROTR",VC->ratExpr(*$5),*$3));
- delete $3;
- delete $5;
- }
- | BVLT_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVLT", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVGT_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVGT", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVLE_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVLE", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVGE_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVGE", *$3, *$5));
- delete $3;
- delete $5;
- }
-
- | BVSLT_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVSLT", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSGT_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVSGT", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSLE_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVSLE", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSGE_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVSGE", *$3, *$5));
- delete $3;
- delete $5;
- }
- | Expr CONCAT_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_CONCAT", *$1, *$3));
- delete $1;
- delete $3;
- }
- | INTTOBV_TOK '(' Expr ',' NUMERAL_TOK ',' NUMERAL_TOK ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_INTTOBV", *$3, VC->ratExpr(*$5),
- VC->ratExpr(*$7)));
- delete $3;
- delete $5;
- delete $7;
- }
- | BVTOINT_TOK '(' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVTOINT", *$3));
- delete $3;
- }
- | BOOLEXTRACT_TOK '(' Expr ',' NUMERAL_TOK ')'
- {
- //FIXME: this function is not to be exposed
- //to the user counterexamples containing
- //this function can be translated into
- //BV-EXTRACT and comparison with 0 or 1
- $$ = new CVC4::Expr(VC->listExpr("_BOOLEXTRACT", *$3,
- VC->ratExpr(*$5)));
- delete $3;
- delete $5;
- }
- | BVPLUS_TOK '(' NUMERAL_TOK ',' Exprs ')'
- {
- std::vector<CVC4::Expr> k;
- k.push_back(VC->ratExpr(*$3));
- k.insert(k.end(), $5->begin(), $5->end());
- $$ = new CVC4::Expr(VC->listExpr("_BVPLUS", k));
- delete $3;
- delete $5;
- }
- | BVSUB_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVSUB", VC->ratExpr(*$3), *$5, *$7));
- delete $3;
- delete $5;
- delete $7;
- }
- | BVUDIV_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVUDIV", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSDIV_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVSDIV", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVUREM_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVUREM", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSREM_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVSREM", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSMOD_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVSMOD", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVSHL_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVSHL", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVASHR_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVASHR", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVLSHR_TOK '(' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVLSHR", *$3, *$5));
- delete $3;
- delete $5;
- }
- | BVUMINUS_TOK '(' Expr ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_BVUMINUS", *$3));
- delete $3;
- }
- | BVMULT_TOK '(' NUMERAL_TOK ',' Expr ',' Expr ')'
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_BVMULT", VC->ratExpr(*$3), *$5, *$7));
- delete $3;
- delete $5;
- delete $7;
- }
- | DISTINCT_TOK '(' Exprs ')'
- {
- $$ = new CVC4::Expr(VC->listExpr("_DISTINCT", *$3));
- delete $3;
- }
- ;
-AndExpr : AndExpr AND_TOK Expr
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
-
- | Expr AND_TOK Expr
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- $$->push_back(*$3);
- delete $1;
- delete $3;
- }
- ;
-
-
-OrExpr : OrExpr OR_TOK Expr
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
-
- | Expr OR_TOK Expr
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- $$->push_back(*$3);
- delete $1;
- delete $3;
- }
- ;
-Conditional : IF_TOK Expr THEN_TOK Expr ElseRest
- {
- $5->push_back(VC->listExpr(*$2, *$4));
- $5->push_back(VC->idExpr("_COND"));
- /* at this point, the list for ElseRest is
- in reverse order from what it should be. */
- std::vector<CVC4::Expr> tmp;
- tmp.insert(tmp.end(), $5->rbegin(), $5->rend());
- $$ = new CVC4::Expr(VC->listExpr(tmp));
- delete $2;
- delete $4;
- delete $5;
- }
- ;
-
-ElseRest : ELSE_TOK Expr ENDIF_TOK
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->listExpr("_ELSE",*$2));
- delete $2;
- }
- | ELSIF_TOK Expr THEN_TOK Expr ElseRest
- {
- /* NOTE that we're getting the list built
- up in the reverse order here. We'll fix
- things when we produce a Conditional. */
- $5->push_back(VC->listExpr(*$2, *$4));
- $$ = $5;
- delete $2;
- delete $4;
- }
- ;
-
-Exprs : Expr
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | Exprs ',' Expr
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-
-Pattern : PATTERN_TOK '(' Exprs ')' ':'
- {
- $$ = $3;
- }
-
-Patterns : Pattern
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->listExpr(*$1));
- delete $1;
- }
- | Patterns Pattern
- {
- $1->push_back(VC->listExpr(*$2));
- $$ = $1;
- delete $2;
- }
- ;
-
-Update : UpdatePositionNode ASSIGN_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
- delete $1;
- delete $3;
- }
- ;
-
-Updates : Update
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | Updates ',' Update
- {
- $$->push_back(*$3);
- delete $3;
- }
- ;
-
-UpdatePositionNode : UpdatePosition
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
- }
- ;
-
-UpdatePosition : '[' Expr ']'
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->listExpr("_READ", *$2));
- delete $2;
- }
- | Identifier
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | '.' Identifier
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->listExpr("_RECORD_SELECT", *$2));
- delete $2;
- }
- | '.' Numeral
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(VC->listExpr("_TUPLE_SELECT", *$2));
- delete $2;
- }
- | UpdatePosition '[' Expr ']'
- {
- $1->push_back(VC->listExpr("_READ", *$3));
- $$ = $1;
- delete $3;
- }
- | UpdatePosition Identifier
- {
- $1->push_back(*$2);
- $$ = $1;
- delete $2;
- }
- | UpdatePosition '.' Identifier
- {
- $1->push_back(VC->listExpr("_RECORD_SELECT",*$3));
- $$ = $1;
- delete $3;
- }
- | UpdatePosition '.' Numeral
- {
- $1->push_back(VC->listExpr("_TUPLE_SELECT", *$3));
- $$ = $1;
- delete $3;
- }
- ;
-
-Lambda : LAMBDA_TOK '(' BoundVarDecls ')' ':' Expr
- %prec ASSIGN_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_LAMBDA",
- VC->listExpr(*$3), (*$6)));
- delete $3;
- delete $6;
- }
- ;
-QuantExpr : FORALL_TOK '(' BoundVarDecls ')' ':' Expr
- %prec FORALL_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_FORALL",
- VC->listExpr(*$3), *$6));
- delete $3;
- delete $6;
- }
- | FORALL_TOK '(' BoundVarDecls ')' ':' Patterns Expr
- %prec FORALL_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_FORALL",
- VC->listExpr(*$3), *$7,
- VC->listExpr(*$6)));
- delete $3;
- delete $6;
- delete $7;
- }
- | EXISTS_TOK '(' BoundVarDecls ')' ':' Expr
- %prec EXISTS_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_EXISTS",
- VC->listExpr(*$3), (*$6)));
- delete $3;
- delete $6;
- }
- ;
- | EXISTS_TOK '(' BoundVarDecls ')' ':' Patterns Expr
- %prec EXISTS_TOK
- {
- $$ = new CVC4::Expr(VC->listExpr("_EXISTS",
- VC->listExpr(*$3), *$7,
- VC->listExpr(*$6)));
- delete $3;
- delete $6;
- delete $7;
- }
-
-ArrayLiteral : ARRAY_TOK '(' BoundVarDecl ')' ':' Expr
- %prec ASSIGN_TOK
- {
- $$ = new CVC4::Expr
- (VC->listExpr("_ARRAY_LITERAL", *$3, *$6));
- delete $3;
- delete $6;
- }
- ;
-RecordLiteral : PARENHASH_TOK RecordEntries HASHPAREN_TOK
- {
- $2->insert($2->begin(), VC->idExpr("_RECORD"));
- $$ = new CVC4::Expr(VC->listExpr(*$2));
- delete $2;
- }
- ;
-
-RecordEntries : RecordEntry
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | RecordEntries ',' RecordEntry
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-RecordEntry : Identifier ASSIGN_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
- delete $1;
- delete $3;
- }
- ;
-
-TupleLiteral : '(' Exprs ',' Expr ')'
- {
- $2->push_back(*$4);
- $2->insert($2->begin(),VC->idExpr("_TUPLE"));
- $$ = new CVC4::Expr(VC->listExpr(*$2));
- delete $2;
- delete $4;
- }
- ;
-
-LetDeclsNode : LetDecls
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
- }
- ;
-LetDecls : LetDecl {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | LetDecls ',' LetDecl
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-LetDecl : Identifier '=' Expr
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1,*$3));
- delete $1;
- delete $3;
- }
- | Identifier ':' Type '=' Expr
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1,*$5));
- delete $1;
- delete $3;
- delete $5;
- }
- ;
-
-LetExpr : LET_TOK LetDeclsNode IN_TOK Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4));
- delete $2;
- delete $4;
- }
- ;
-
-TypeLetDeclsNode : TypeLetDecls
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
- }
- ;
-TypeLetDecls : TypeLetDecl {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | TypeLetDecls ',' TypeLetDecl
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-TypeLetDecl : Identifier '=' Type
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1, *$3));
- delete $1;
- delete $3;
- }
- | Identifier ':' TYPE_TOK '=' Type
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1,*$5));
- delete $1;
- delete $5;
- }
- ;
-
-TypeLetExpr : LET_TOK TypeLetDeclsNode IN_TOK Type
- {
- $$ = new CVC4::Expr(VC->listExpr("_LET", *$2, *$4));
- delete $2;
- delete $4;
- }
- ;
-
-BoundVarDecl : IDs ':' Type
- {
- $1->push_back(*$3);
- delete $3;
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
-
- }
- ;
-
-BoundVarDecls : BoundVarDecl
- {
- $$ = new std::vector<CVC4::Expr>;
- $$->push_back(*$1);
- delete $1;
- }
- | BoundVarDecls ',' BoundVarDecl
- {
- $1->push_back(*$3);
- $$ = $1;
- delete $3;
- }
- ;
-
-BoundVarDeclNode: BoundVarDecls
- {
- $$ = new CVC4::Expr(VC->listExpr(*$1));
- delete $1;
- }
- ;
-
-ConstDecl : Identifier ':' Type '=' Expr
- {
- $$ = new CVC4::Expr(VC->listExpr("_CONST",
- *$1, *$3, *$5));
- delete $1;
- delete $3;
- delete $5;
- }
- | Identifier ':' Type
- {
- $$ =new CVC4::Expr
- (VC->listExpr("_CONST", VC->listExpr(*$1), *$3));
- delete $1;
- delete $3;
- }
- | Identifier '(' BoundVarDeclNode ')' ':' Type '=' Expr
- {
- std::vector<CVC4::Expr> tmp;
- tmp.push_back(VC->idExpr("_DEFUN"));
- tmp.push_back(*$1);
- tmp.push_back(*$3);
- tmp.push_back(*$6);
- tmp.push_back(*$8);
- $$ = new CVC4::Expr(VC->listExpr(tmp));
- delete $1;
- delete $3;
- delete $6;
- delete $8;
- }
- | Identifier '(' BoundVarDeclNode ')' ':' Type
- {
- std::vector<CVC4::Expr> tmp;
- tmp.push_back(VC->idExpr("_DEFUN"));
- tmp.push_back(*$1);
- tmp.push_back(*$3);
- tmp.push_back(*$6);
- $$ = new CVC4::Expr(VC->listExpr(tmp));
- delete $1;
- delete $3;
- delete $6;
- }
- | Identifier ',' IDs ':' Type
- {
- $3->insert($3->begin(), *$1);
- $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$3), *$5));
- delete $1;
- delete $3;
- delete $5;
- }
- ;
+Query:
+ QUERY_TOK Expr {
+ $$ = NULL; // exprManager->mkExpr(Kind.TRUE);
+ }
+ | CHECKSAT_TOK Expr {
+ $$ = NULL; //new CVC3::Expr(VC->listExpr("_CHECKSAT", *$2));
+ // delete $2;
+ }
+ | CHECKSAT_TOK {
+ $$ = NULL;
+ // new CVC3::Expr(VC->listExpr(VC->idExpr("_CHECKSAT")));
+ } ;
+
+Expr:
+// Identifier { $$ = $1; }
+// |
+ TRUELIT_TOK {
+ $$ = new Expr(EM->mkExpr(TRUE));
+ }
+ | FALSELIT_TOK {
+ $$ = new Expr(EM->mkExpr(FALSE));
+ }
+ | Expr OR_TOK Expr {
+ $$ = new Expr(EM->mkExpr(OR, *$1, *$3));
+ delete $1;
+ delete $3;
+ }
+ | Expr AND_TOK Expr {
+ $$ = new Expr(EM->mkExpr(AND, *$1, *$3));
+ delete $1;
+ delete $3;
+ }
+ // | Expr IMPLIES_TOK Expr
+ // {
+ // $$ = new CVC3::Expr(VC->listExpr("_IMPLIES", *$1, *$3));
+ // delete $1;
+ // delete $3;
+ // }
+ // | Expr IFF_TOK Expr
+ // {
+ // $$ = new CVC3::Expr(VC->listExpr("_IFF", *$1, *$3));
+ // delete $1;
+ // delete $3;
+ // }
+;
+
+
+// Identifier:
+// ID_TOK {
+// $$ = EM->mkExpr(VARIABLE, *$1);
+// delete $1;
+// }
-TypeDecl : DataType { $$ = $1; }
- | Identifier ':' TYPE_TOK '=' TypeDef
- {
- $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", *$1, *$5));
- delete $1;
- delete $5;
- }
- | Identifier ':' TYPE_TOK
- {
- $$ =new CVC4::Expr(VC->listExpr("_TYPE", *$1));
- delete $1;
- }
- | Identifier ',' IDs ':' TYPE_TOK
- {
- std::vector<CVC4::Expr> tmp;
- tmp.push_back(*$1);
- tmp.insert(tmp.end(), $3->begin(), $3->end());
- $$ = new CVC4::Expr(VC->listExpr("_TYPE", tmp));
- delete $1;
- delete $3;
- }
- ;
%%
projects / cvc5.git / commitdiff