summaryrefslogtreecommitdiff
path: root/src/parser
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2009-11-12 20:38:10 +0000
committerMorgan Deters <mdeters@gmail.com>2009-11-12 20:38:10 +0000
commit13a6669a35aee32c03f8d29fe386aca95d2fbd8f (patch)
treeb126afb6c384dd45db0249e8096cf733a74daa95 /src/parser
parent5b5474281c4cdc880bff8b9e38b84dc84f88e50c (diff)
parser, minisat, other things..
Diffstat (limited to 'src/parser')
-rw-r--r--src/parser/Makefile.am18
-rw-r--r--src/parser/parser.cpp21
-rw-r--r--src/parser/pl.ypp1993
-rw-r--r--src/parser/pl_scanner.lpp352
-rw-r--r--src/parser/smtlib.ypp1553
-rw-r--r--src/parser/smtlib_scanner.lpp260
6 files changed, 4197 insertions, 0 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
new file mode 100644
index 000000000..0ebcad8c7
--- /dev/null
+++ b/src/parser/Makefile.am
@@ -0,0 +1,18 @@
+INCLUDES = -I@srcdir@/../include
+
+noinst_LIBRARIES = libparser.a
+
+libparser_a_SOURCES = \
+ pl_scanner.lpp \
+ pl.ypp \
+ smtlib_scanner.lpp \
+ smtlib.ypp \
+ parser.cpp
+
+BUILT_SOURCES = \
+ pl_scanner.lpp \
+ pl.ypp \
+ smtlib_scanner.lpp \
+ smtlib.ypp
+
+
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
new file mode 100644
index 000000000..35ca74ecd
--- /dev/null
+++ b/src/parser/parser.cpp
@@ -0,0 +1,21 @@
+/********************* -*- C++ -*- */
+/** parser.cpp
+ ** This file is part of the CVC4 prototype.
+ **
+ ** Parser implementation.
+ **
+ ** The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ **/
+
+#include "parser.h"
+#include "parser_temp.h"
+#include "parser_exception.h"
+
+namespace CVC4 {
+
+ParserTemp *parserTemp;
+
+}/* CVC4 namespace */
+
diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp
new file mode 100644
index 000000000..dfed55dbb
--- /dev/null
+++ b/src/parser/pl.ypp
@@ -0,0 +1,1993 @@
+%{
+/*****************************************************************************/
+/*!
+ * \file PL.y
+ *
+ * Author: Sergey Berezin
+ *
+ * Created: Feb 06 03:00:43 GMT 2003
+ *
+ * <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>
+ *
+ */
+/*****************************************************************************/
+/* PL.y
+ Aaron Stump, 4/14/01
+
+ This file contains the bison code for the parser that reads in CVC
+ commands in the presentation language (hence "PL").
+*/
+
+#include "vc.h"
+#include "parser_exception.h"
+#include "parser_temp.h"
+#include "rational.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 RAT(args) CVC4::newRational args
+
+// Suppress the bogus warning suppression in bison (it generates
+// compile error)
+#undef __GNUC_MINOR__
+
+/* stuff that lives in PL.lex */
+extern int PLlex(void);
+
+int PLerror(const char *s)
+{
+ std::ostringstream ss;
+ ss << CVC4::parserTemp->fileName << ":" << CVC4::parserTemp->lineNum
+ << ": " << s;
+ return CVC4::parserTemp->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
+%}
+
+%union {
+ std::string *str;
+ CVC4::Expr *node;
+ std::vector<CVC4::Expr> *vec;
+ int kind;
+};
+
+
+%start cmd
+
+/* strings are for better error messages.
+ "_TOK" is so macros don't conflict with kind names */
+
+%token DISTINCT_TOK "DISTINCT"
+%token AND_TOK "AND"
+%token ARRAY_TOK "ARRAY"
+%token BOOLEAN_TOK "BOOLEAN"
+%token DATATYPE_TOK "DATATYPE"
+%token ELSE_TOK "ELSE"
+%token ELSIF_TOK "ELSIF"
+%token END_TOK "END"
+%token ENDIF_TOK "ENDIF"
+%token EXISTS_TOK "EXISTS"
+%token FALSELIT_TOK "FALSE"
+%token FORALL_TOK "FORALL"
+%token IN_TOK "IN"
+%token IF_TOK "IF"
+%token LAMBDA_TOK "LAMBDA"
+%token SIMULATE_TOK "SIMULATE"
+%token LET_TOK "LET"
+%token NOT_TOK "NOT"
+%token IS_INTEGER_TOK "IS_INTEGER"
+%token OF_TOK "OF"
+%token OR_TOK "OR"
+%token REAL_TOK "REAL"
+%token INT_TOK "INT"
+%token SUBTYPE_TOK "SUBTYPE"
+%token BITVECTOR_TOK "BITVECTOR"
+%token THEN_TOK "THEN"
+%token TRUELIT_TOK "TRUE"
+%token TYPE_TOK "TYPE"
+%token WITH_TOK "WITH"
+%token XOR_TOK "XOR"
+%token TCC_TOK "TCC"
+%token PATTERN_TOK "PATTERN"
+%token '_'
+%token DONE_TOK
+
+%token DOTDOT_TOK ".."
+%token ASSIGN_TOK ":="
+%token NEQ_TOK "/="
+%token IMPLIES_TOK "=>"
+%token IFF_TOK "<=>"
+%token PLUS_TOK "+"
+%token MINUS_TOK "-"
+%token MULT_TOK "*"
+%token POW_TOK "^"
+%token DIV_TOK "/"
+%token MOD_TOK "MOD"
+%token INTDIV_TOK "DIV"
+%token LT_TOK "<"
+%token LE_TOK "<="
+%token GT_TOK ">"
+%token GE_TOK ">="
+%token FLOOR_TOK "FLOOR"
+%token LEFTSHIFT_TOK "<<"
+%token RIGHTSHIFT_TOK ">>"
+%token BVPLUS_TOK "BVPLUS"
+%token BVSUB_TOK "BVSUB"
+%token BVUDIV_TOK "BVUDIV"
+%token BVSDIV_TOK "BVSDIV"
+%token BVUREM_TOK "BVUREM"
+%token BVSREM_TOK "BVSREM"
+%token BVSMOD_TOK "BVSMOD"
+%token BVSHL_TOK "BVSHL"
+%token BVASHR_TOK "BVASHR"
+%token BVLSHR_TOK "BVLSHR"
+%token BVUMINUS_TOK "BVUMINUS"
+%token BVMULT_TOK "BVMULT"
+%token SQHASH_TOK "[#"
+%token HASHSQ_TOK "#]"
+%token PARENHASH_TOK "(#"
+%token HASHPAREN_TOK "#)"
+%token ARROW_TOK "->"
+%token BVNEG_TOK "~"
+%token BVAND_TOK "&"
+%token MID_TOK "|"
+%token BVXOR_TOK "BVXOR"
+%token BVNAND_TOK "BVNAND"
+%token BVNOR_TOK "BVNOR"
+%token BVCOMP_TOK "BVCOMP"
+%token BVXNOR_TOK "BVXNOR"
+%token CONCAT_TOK "@"
+%token BVTOINT_TOK "BVTOINT"
+%token INTTOBV_TOK "INTTOBV"
+%token BOOLEXTRACT_TOK "BOOLEXTRACT"
+%token BVLT_TOK "BVLT"
+%token BVGT_TOK "BVGT"
+%token BVLE_TOK "BVLE"
+%token BVGE_TOK "BVGE"
+%token SX_TOK "SX"
+%token BVZEROEXTEND_TOK "BVZEROEXTEND"
+%token BVREPEAT_TOK "BVREPEAT"
+%token BVROTL_TOK "BVROTL"
+%token BVROTR_TOK "BVROTR"
+%token BVSLT_TOK "BVSLT"
+%token BVSGT_TOK "BVSGT"
+%token BVSLE_TOK "BVSLE"
+%token BVSGE_TOK "BVSGE"
+
+
+/* commands given in prefix syntax */
+%token ARITH_VAR_ORDER_TOK "ARITH_VAR_ORDER"
+%token ASSERT_TOK "ASSERT"
+%token QUERY_TOK "QUERY"
+%token CHECKSAT_TOK "CHECKSAT"
+%token CONTINUE_TOK "CONTINUE"
+%token RESTART_TOK "RESTART"
+%token HELP_TOK "HELP"
+%token DBG_TOK "DBG"
+%token TRACE_TOK "TRACE"
+%token UNTRACE_TOK "UNTRACE"
+%token OPTION_TOK "OPTION"
+%token TRANSFORM_TOK "TRANSFORM"
+%token PRINT_TOK "PRINT"
+%token PRINT_TYPE_TOK "PRINT_TYPE"
+%token CALL_TOK "CALL"
+%token ECHO_TOK "ECHO"
+%token INCLUDE_TOK "INCLUDE"
+%token DUMP_PROOF_TOK "DUMP_PROOF"
+%token DUMP_ASSUMPTIONS_TOK "DUMP_ASSUMPTIONS"
+%token DUMP_SIG_TOK "DUMP_SIG"
+%token DUMP_TCC_TOK "DUMP_TCC"
+%token DUMP_TCC_ASSUMPTIONS_TOK "DUMP_TCC_ASSUMPTIONS"
+%token DUMP_TCC_PROOF_TOK "DUMP_TCC_PROOF"
+%token DUMP_CLOSURE_TOK "DUMP_CLOSURE"
+%token DUMP_CLOSURE_PROOF_TOK "DUMP_CLOSURE_PROOF"
+%token WHERE_TOK "WHERE"
+%token ASSERTIONS_TOK "ASSERTIONS"
+%token ASSUMPTIONS_TOK "ASSUMPTIONS"
+%token COUNTEREXAMPLE_TOK "COUNTEREXAMPLE"
+%token COUNTERMODEL_TOK "COUNTERMODEL"
+%token PUSH_TOK "PUSH"
+%token POP_TOK "POP"
+%token POPTO_TOK "POPTO"
+%token PUSH_SCOPE_TOK "PUSH_SCOPE"
+%token POP_SCOPE_TOK "POP_SCOPE"
+%token POPTO_SCOPE_TOK "POPTO_SCOPE"
+%token RESET_TOK "RESET"
+%token CONTEXT_TOK "CONTEXT"
+%token FORGET_TOK "FORGET"
+%token GET_TYPE_TOK "GET_TYPE"
+%token CHECK_TYPE_TOK "CHECK_TYPE"
+%token GET_CHILD_TOK "GET_CHILD"
+%token GET_OP_TOK "GET_OP"
+%token SUBSTITUTE_TOK "SUBSTITUTE"
+
+%nonassoc ASSIGN_TOK IN_TOK
+%nonassoc FORALL_TOK EXISTS_TOK
+%left IFF_TOK
+%right IMPLIES_TOK
+%left OR_TOK XOR_TOK
+%left AND_TOK
+%left NOT_TOK
+
+%nonassoc '=' NEQ_TOK
+%nonassoc LE_TOK LT_TOK GE_TOK GT_TOK FLOOR_TOK
+%left PLUS_TOK MINUS_TOK
+%left MULT_TOK INTDIV_TOK DIV_TOK MOD_TOK
+%left POW_TOK
+%left WITH_TOK
+%left UMINUS_TOK
+%left CONCAT_TOK
+%left MID_TOK
+%left BVAND_TOK
+%left BVXOR_TOK
+%left BVNAND_TOK
+%left BVNOR_TOK BVCOMP_TOK
+%left BVXNOR_TOK
+%left BVNEG_TOK
+%left BVUMINUS_TOK BVPLUS_TOK BVSUB_TOK
+%left BVUDIV_TOK BVSDIV_TOK BVUREM_TOK BVSREM_TOK BVSMOD_TOK BVSHL_TOK BVASHR_TOK BVLSHR_TOK
+%left SX_TOK BVZEROEXTEND_TOK BVREPEAT_TOK BVROTL_TOK BVROTR_TOK
+%left LEFTSHIFT_TOK RIGHTSHIFT_TOK
+%nonassoc BVLT_TOK BVLE_TOK BVGT_TOK BVGE_TOK
+%nonassoc BVSLT_TOK BVSLE_TOK BVSGT_TOK BVSGE_TOK
+%right IS_INTEGER_TOK
+%left ARROW_TOK
+
+%nonassoc '['
+%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
+
+%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;
+ }
+ ;
+
+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;
+ }
+ ;
+
+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;
+ }
+ ;
+
+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;
+ }
+ ;
+%%
diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp
new file mode 100644
index 000000000..d203a1e9a
--- /dev/null
+++ b/src/parser/pl_scanner.lpp
@@ -0,0 +1,352 @@
+%{
+/*****************************************************************************/
+/*!
+ * \file PL.lex
+ *
+ * Author: Sergey Berezin
+ *
+ * Created: Feb 06 03:00:43 GMT 2003
+ *
+ * <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>
+ *
+ */
+/*****************************************************************************/
+
+#include <iostream>
+#include "parser_temp.h"
+#include "expr_manager.h" /* for the benefit of parsePL_defs.h */
+#include "parsePL_defs.h"
+#include "debug.h"
+
+namespace CVC4 {
+ extern ParserTemp* parserTemp;
+}
+
+/* prefixing hack from gdb (via automake docs) */
+#define yymaxdepth PL_maxdepth
+#define yyparse PL_parse
+#define yylex PL_lex
+#define yyerror PL_error
+#define yylval PL_lval
+#define yychar PL_char
+#define yydebug PL_debug
+#define yypact PL_pact
+#define yyr1 PL_r1
+#define yyr2 PL_r2
+#define yydef PL_def
+#define yychk PL_chk
+#define yypgo PL_pgo
+#define yyact PL_act
+#define yyexca PL_exca
+#define yyerrflag PL_errflag
+#define yynerrs PL_nerrs
+#define yyps PL_ps
+#define yypv PL_pv
+#define yys PL_s
+#define yy_yys PL_yys
+#define yystate PL_state
+#define yytmp PL_tmp
+#define yyv PL_v
+#define yy_yyv PL_yyv
+#define yyval PL_val
+#define yylloc PL_lloc
+#define yyreds PL_reds
+#define yytoks PL_toks
+#define yylhs PL_yylhs
+#define yylen PL_yylen
+#define yydefred PL_yydefred
+#define yydgoto PL_yydgoto
+#define yysindex PL_yysindex
+#define yyrindex PL_yyrindex
+#define yygindex PL_yygindex
+#define yytable PL_yytable
+#define yycheck PL_yycheck
+#define yyname PL_yyname
+#define yyrule PL_yyrule
+
+extern int PL_inputLine;
+extern char *PLtext;
+
+extern int PLerror (const char *msg);
+
+static int PLinput(std::istream& is, char* buf, int size) {
+ int res;
+ if(is) {
+ // If interactive, read line by line; otherwise read as much as we
+ // can gobble
+ if(CVC4::parserTemp->interactive) {
+ // Print the current prompt
+ std::cout << CVC4::parserTemp->getPrompt() << std::flush;
+ // Set the prompt to "middle of the command" one
+ CVC4::parserTemp->setPrompt2();
+ // Read the line
+ is.getline(buf, size-1);
+ } else // Set the terminator char to 0
+ is.getline(buf, size-1, 0);
+ // If failbit is set, but eof is not, it means the line simply
+ // didn't fit; so we clear the state and keep on reading.
+ bool partialStr = is.fail() && !is.eof();
+ if(partialStr)
+ is.clear();
+
+ for(res = 0; res<size && buf[res] != 0; res++);
+ if(res == size) PLerror("Lexer bug: overfilled the buffer");
+ if(!partialStr) { // Insert \n into the buffer
+ buf[res++] = '\n';
+ buf[res] = '\0';
+ }
+ } else {
+ res = YY_NULL;
+ }
+ return res;
+}
+
+// Redefine the input buffer function to read from an istream
+#define YY_INPUT(buf,result,max_size) \
+ result = PLinput(*CVC4::parserTemp->is, buf, max_size);
+
+int PL_bufSize() { return YY_BUF_SIZE; }
+YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; }
+
+/* some wrappers for methods that need to refer to a struct.
+ These are used by CVC4::Parser. */
+void *PL_createBuffer(int sz) {
+ return (void *)PL_create_buffer(NULL, sz);
+}
+void PL_deleteBuffer(void *buf_state) {
+ PL_delete_buffer((struct yy_buffer_state *)buf_state);
+}
+void PL_switchToBuffer(void *buf_state) {
+ PL_switch_to_buffer((struct yy_buffer_state *)buf_state);
+}
+void *PL_bufState() {
+ return (void *)PL_buf_state();
+}
+
+void PL_setInteractive(bool is_interactive) {
+ yy_set_interactive(is_interactive);
+}
+
+// File-static (local to this file) variables and functions
+static std::string _string_lit;
+
+ static char escapeChar(char c) {
+ switch(c) {
+ case 'n': return '\n';
+ case 't': return '\t';
+ default: return c;
+ }
+ }
+
+// for now, we don't have subranges.
+//
+// ".." { return DOTDOT_TOK; }
+/*OPCHAR (['!#?\_$&\|\\@])*/
+
+%}
+
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+
+%x COMMENT
+%x STRING_LITERAL
+
+LETTER ([a-zA-Z])
+HEX ([0-9a-fA-F])
+BITS ([0-1])
+DIGIT ([0-9])
+OPCHAR (['?\_$~])
+ANYTHING ({LETTER}|{DIGIT}|{OPCHAR})
+
+%%
+
+[\n] { CVC4::parserTemp->lineNum++; }
+
+[ \t\r\f] { /* skip whitespace */ }
+
+0bin{BITS}+ {PLlval.str = new std::string(PLtext+4);return BINARY_TOK;
+ }
+0hex{HEX}+ {PLlval.str = new std::string(PLtext+4);return HEX_TOK;
+ }
+{DIGIT}+ {PLlval.str = new std::string(PLtext);return NUMERAL_TOK;
+ }
+
+"%" { BEGIN COMMENT; }
+<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */
+ CVC4::parserTemp->lineNum++; }
+<COMMENT>. { /* stay in comment mode */ }
+
+<INITIAL>"\"" { BEGIN STRING_LITERAL;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */
+ _string_lit.insert(_string_lit.end(),
+ escapeChar(PLtext[1])); }
+<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */
+ PLlval.str = new std::string(_string_lit);
+ return STRINGLIT_TOK; }
+<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*PLtext); }
+
+[()[\]{},.;:'!#?_=] { return PLtext[0]; }
+
+".." { return DOTDOT_TOK; }
+":=" { return ASSIGN_TOK; }
+"/=" { return NEQ_TOK; }
+"=>" { return IMPLIES_TOK; }
+"<=>" { return IFF_TOK; }
+"+" { return PLUS_TOK; }
+"-" { return MINUS_TOK; }
+"*" { return MULT_TOK; }
+"^" { return POW_TOK; }
+"/" { return DIV_TOK; }
+"MOD" { return MOD_TOK; }
+"DIV" { return INTDIV_TOK; }
+"<" { return LT_TOK; }
+"<=" { return LE_TOK; }
+">" { return GT_TOK; }
+">=" { return GE_TOK; }
+"FLOOR" { return FLOOR_TOK; }
+
+"[#" { return SQHASH_TOK; }
+"#]" { return HASHSQ_TOK; }
+"(#" { return PARENHASH_TOK; }
+"#)" { return HASHPAREN_TOK; }
+"->" { return ARROW_TOK; }
+"ARROW" { return ARROW_TOK; }
+"@" { return CONCAT_TOK;}
+"~" { return BVNEG_TOK;}
+"&" { return BVAND_TOK;}
+"|" { return MID_TOK;}
+"BVXOR" { return BVXOR_TOK;}
+"BVNAND" { return BVNAND_TOK;}
+"BVNOR" { return BVNOR_TOK;}
+"BVCOMP" { return BVCOMP_TOK;}
+"BVXNOR" { return BVXNOR_TOK;}
+"<<" { return LEFTSHIFT_TOK;}
+">>" { return RIGHTSHIFT_TOK;}
+"BVSLT" { return BVSLT_TOK;}
+"BVSGT" { return BVSGT_TOK;}
+"BVSLE" { return BVSLE_TOK;}
+"BVSGE" { return BVSGE_TOK;}
+"SX" { return SX_TOK;}
+"BVZEROEXTEND" { return BVZEROEXTEND_TOK;}
+"BVREPEAT" { return BVREPEAT_TOK;}
+"BVROTL" { return BVROTL_TOK;}
+"BVROTR" { return BVROTR_TOK;}
+"BVLT" { return BVLT_TOK;}
+"BVGT" { return BVGT_TOK;}
+"BVLE" { return BVLE_TOK;}
+"BVGE" { return BVGE_TOK;}
+
+"DISTINCT" { return DISTINCT_TOK; }
+"BVTOINT" { return BVTOINT_TOK;}
+"INTTOBV" { return INTTOBV_TOK;}
+"BOOLEXTRACT" { return BOOLEXTRACT_TOK;}
+"BVPLUS" { return BVPLUS_TOK;}
+"BVUDIV" { return BVUDIV_TOK;}
+"BVSDIV" { return BVSDIV_TOK;}
+"BVUREM" { return BVUREM_TOK;}
+"BVSREM" { return BVSREM_TOK;}
+"BVSMOD" { return BVSMOD_TOK;}
+"BVSHL" { return BVSHL_TOK;}
+"BVASHR" { return BVASHR_TOK;}
+"BVLSHR" { return BVLSHR_TOK;}
+"BVSUB" { return BVSUB_TOK;}
+"BVUMINUS" { return BVUMINUS_TOK;}
+"BVMULT" { return BVMULT_TOK;}
+"AND" { return AND_TOK; }
+"ARRAY" { return ARRAY_TOK; }
+"BOOLEAN" { return BOOLEAN_TOK; }
+"DATATYPE" { return DATATYPE_TOK; }
+"ELSE" { return ELSE_TOK; }
+"ELSIF" { return ELSIF_TOK; }
+"END" { return END_TOK; }
+"ENDIF" { return ENDIF_TOK; }
+"EXISTS" { return EXISTS_TOK; }
+"FALSE" { return FALSELIT_TOK; }
+"FORALL" { return FORALL_TOK; }
+"IF" { return IF_TOK; }
+"IN" { return IN_TOK; }
+"LAMBDA" { return LAMBDA_TOK; }
+"SIMULATE" { return SIMULATE_TOK; }
+"LET" { return LET_TOK; }
+"NOT" { return NOT_TOK; }
+"IS_INTEGER" { return IS_INTEGER_TOK; }
+"OF" { return OF_TOK; }
+"OR" { return OR_TOK; }
+"REAL" { return REAL_TOK; }
+"INT" { return INT_TOK;}
+"SUBTYPE" { return SUBTYPE_TOK;}
+"BITVECTOR" { return BITVECTOR_TOK;}
+
+"THEN" { return THEN_TOK; }
+"TRUE" { return TRUELIT_TOK; }
+"TYPE" { return TYPE_TOK; }
+"WITH" { return WITH_TOK; }
+"XOR" { return XOR_TOK; }
+"TCC" { return TCC_TOK; }
+"PATTERN" { return PATTERN_TOK; }
+
+"ARITH_VAR_ORDER" { return ARITH_VAR_ORDER_TOK; }
+"ASSERT" { return ASSERT_TOK; }
+"QUERY" { return QUERY_TOK; }
+"CHECKSAT" { return CHECKSAT_TOK; }
+"CONTINUE" { return CONTINUE_TOK; }
+"RESTART" { return RESTART_TOK; }
+"DBG" { return DBG_TOK; }
+"TRACE" { return TRACE_TOK; }
+"UNTRACE" { return UNTRACE_TOK; }
+"OPTION" { return OPTION_TOK; }
+"HELP" { return HELP_TOK; }
+"TRANSFORM" { return TRANSFORM_TOK; }
+"PRINT" { return PRINT_TOK; }
+"PRINT_TYPE" { return PRINT_TYPE_TOK; }
+"CALL" { return CALL_TOK; }
+"ECHO" { return ECHO_TOK; }
+"INCLUDE" { return INCLUDE_TOK; }
+"DUMP_ASSUMPTIONS" { return DUMP_ASSUMPTIONS_TOK; }
+"DUMP_PROOF" { return DUMP_PROOF_TOK; }
+"DUMP_SIG" { return DUMP_SIG_TOK; }
+"DUMP_TCC" { return DUMP_TCC_TOK; }
+"DUMP_TCC_ASSUMPTIONS" { return DUMP_TCC_ASSUMPTIONS_TOK; }
+"DUMP_TCC_PROOF" { return DUMP_TCC_PROOF_TOK; }
+"DUMP_CLOSURE" { return DUMP_CLOSURE_TOK; }
+"DUMP_CLOSURE_PROOF" { return DUMP_CLOSURE_PROOF_TOK; }
+"WHERE" { return WHERE_TOK; }
+"ASSERTIONS" { return ASSERTIONS_TOK; }
+"ASSUMPTIONS" { return ASSUMPTIONS_TOK; }
+"COUNTEREXAMPLE" { return COUNTEREXAMPLE_TOK; }
+"COUNTERMODEL" { return COUNTERMODEL_TOK; }
+"PUSH" { return PUSH_TOK; }
+"POP" { return POP_TOK; }
+"POPTO" { return POPTO_TOK; }
+"PUSH_SCOPE" { return PUSH_SCOPE_TOK; }
+"POP_SCOPE" { return POP_SCOPE_TOK; }
+"POPTO_SCOPE" { return POPTO_SCOPE_TOK; }
+"RESET" { return RESET_TOK; }
+"CONTEXT" { return CONTEXT_TOK; }
+"FORGET" { return FORGET_TOK; }
+"GET_TYPE" { return GET_TYPE_TOK; }
+"CHECK_TYPE" { return CHECK_TYPE_TOK; }
+"GET_CHILD" { return GET_CHILD_TOK; }
+"GET_OP" { return GET_OP_TOK; }
+"SUBSTITUTE" { return SUBSTITUTE_TOK; }
+
+(({LETTER})|(_)({ANYTHING}))({ANYTHING})* { PLlval.str = new std::string(PLtext); return ID_TOK; }
+
+<<EOF>> { return DONE_TOK; }
+
+. { PLerror("Illegal input character."); }
+%%
+
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;
+ }
+;
+
+
+
+%%
diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp
new file mode 100644
index 000000000..d5bdaaf26
--- /dev/null
+++ b/src/parser/smtlib_scanner.lpp
@@ -0,0 +1,260 @@
+%{
+/*****************************************************************************/
+/*!
+ * \file smtlib.lex
+ *
+ * Author: Clark Barrett
+ *
+ * Created: 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>
+ *
+ */
+/*****************************************************************************/
+
+#include <iostream>
+#include "parser_temp.h"
+#include "expr_manager.h" /* for the benefit of parsesmtlib_defs.h */
+#include "parsesmtlib_defs.h"
+#include "debug.h"
+
+namespace CVC4 {
+ extern ParserTemp* parserTemp;
+}
+
+/* prefixing hack from gdb (via automake docs) */
+#define yymaxdepth smtlib_maxdepth
+#define yyparse smtlib_parse
+#define yylex smtlib_lex
+#define yyerror smtlib_error
+#define yylval smtlib_lval
+#define yychar smtlib_char
+#define yydebug smtlib_debug
+#define yypact smtlib_pact
+#define yyr1 smtlib_r1
+#define yyr2 smtlib_r2
+#define yydef smtlib_def
+#define yychk smtlib_chk
+#define yypgo smtlib_pgo
+#define yyact smtlib_act
+#define yyexca smtlib_exca
+#define yyerrflag smtlib_errflag
+#define yynerrs smtlib_nerrs
+#define yyps smtlib_ps
+#define yypv smtlib_pv
+#define yys smtlib_s
+#define yy_yys smtlib_yys
+#define yystate smtlib_state
+#define yytmp smtlib_tmp
+#define yyv smtlib_v
+#define yy_yyv smtlib_yyv
+#define yyval smtlib_val
+#define yylloc smtlib_lloc
+#define yyreds smtlib_reds
+#define yytoks smtlib_toks
+#define yylhs smtlib_yylhs
+#define yylen smtlib_yylen
+#define yydefred smtlib_yydefred
+#define yydgoto smtlib_yydgoto
+#define yysindex smtlib_yysindex
+#define yyrindex smtlib_yyrindex
+#define yygindex smtlib_yygindex
+#define yytable smtlib_yytable
+#define yycheck smtlib_yycheck
+#define yyname smtlib_yyname
+#define yyrule smtlib_yyrule
+
+extern int smtlib_inputLine;
+extern char *smtlibtext;
+
+extern int smtliberror (const char *msg);
+
+static int smtlibinput(std::istream& is, char* buf, int size) {
+ int res;
+ if(is) {
+ // If interactive, read line by line; otherwise read as much as we
+ // can gobble
+ if(CVC4::parserTemp->interactive) {
+ // Print the current prompt
+ std::cout << CVC4::parserTemp->getPrompt() << std::flush;
+ // Set the prompt to "middle of the command" one
+ CVC4::parserTemp->setPrompt2();
+ // Read the line
+ is.getline(buf, size-1);
+ } else // Set the terminator char to 0
+ is.getline(buf, size-1, 0);
+ // If failbit is set, but eof is not, it means the line simply
+ // didn't fit; so we clear the state and keep on reading.
+ bool partialStr = is.fail() && !is.eof();
+ if(partialStr)
+ is.clear();
+
+ for(res = 0; res<size && buf[res] != 0; res++);
+ if(res == size) smtliberror("Lexer bug: overfilled the buffer");
+ if(!partialStr) { // Insert \n into the buffer
+ buf[res++] = '\n';
+ buf[res] = '\0';
+ }
+ } else {
+ res = YY_NULL;
+ }
+ return res;
+}
+
+// Redefine the input buffer function to read from an istream
+#define YY_INPUT(buf,result,max_size) \
+ result = smtlibinput(*CVC4::parserTemp->is, buf, max_size);
+
+int smtlib_bufSize() { return YY_BUF_SIZE; }
+YY_BUFFER_STATE smtlib_buf_state() { return YY_CURRENT_BUFFER; }
+
+/* some wrappers for methods that need to refer to a struct.
+ These are used by CVC4::Parser. */
+void *smtlib_createBuffer(int sz) {
+ return (void *)smtlib_create_buffer(NULL, sz);
+}
+void smtlib_deleteBuffer(void *buf_state) {
+ smtlib_delete_buffer((struct yy_buffer_state *)buf_state);
+}
+void smtlib_switchToBuffer(void *buf_state) {
+ smtlib_switch_to_buffer((struct yy_buffer_state *)buf_state);
+}
+void *smtlib_bufState() {
+ return (void *)smtlib_buf_state();
+}
+
+void smtlib_setInteractive(bool is_interactive) {
+ yy_set_interactive(is_interactive);
+}
+
+// File-static (local to this file) variables and functions
+static std::string _string_lit;
+
+ static char escapeChar(char c) {
+ switch(c) {
+ case 'n': return '\n';
+ case 't': return '\t';
+ default: return c;
+ }
+ }
+
+// for now, we don't have subranges.
+//
+// ".." { return DOTDOT_TOK; }
+/*OPCHAR (['!#?\_$&\|\\@])*/
+
+%}
+
+%option interactive
+%option noyywrap
+%option nounput
+%option noreject
+%option noyymore
+%option yylineno
+
+%x COMMENT
+%x STRING_LITERAL
+%x USER_VALUE
+%s PAT_MODE
+
+LETTER ([a-zA-Z])
+DIGIT ([0-9])
+OPCHAR (['\.\_])
+IDCHAR ({LETTER}|{DIGIT}|{OPCHAR})
+%%
+
+[\n] { CVC4::parserTemp->lineNum++; }
+[ \t\r\f] { /* skip whitespace */ }
+
+{DIGIT}+"\."{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK; }
+{DIGIT}+ { smtliblval.str = new std::string(smtlibtext); return NUMERAL_TOK;
+ }
+
+";" { BEGIN COMMENT; }
+<COMMENT>"\n" { BEGIN INITIAL; /* return to normal mode */
+ CVC4::parserTemp->lineNum++; }
+<COMMENT>. { /* stay in comment mode */ }
+
+<INITIAL>"\"" { BEGIN STRING_LITERAL;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+<STRING_LITERAL>"\\". { /* escape characters (like \n or \") */
+ _string_lit.insert(_string_lit.end(),
+ escapeChar(smtlibtext[1])); }
+<STRING_LITERAL>"\"" { BEGIN INITIAL; /* return to normal mode */
+ smtliblval.str = new std::string(_string_lit);
+ return STRING_TOK; }
+<STRING_LITERAL>. { _string_lit.insert(_string_lit.end(),*smtlibtext); }
+
+<INITIAL>":pat" { BEGIN PAT_MODE;
+ return PAT_TOK;}
+<PAT_MODE>"}" { BEGIN INITIAL;
+ return RCURBRACK_TOK; }
+<INITIAL>"{" { BEGIN USER_VALUE;
+ _string_lit.erase(_string_lit.begin(),
+ _string_lit.end()); }
+<USER_VALUE>"\\"[{}] { /* escape characters */
+ _string_lit.insert(_string_lit.end(),smtlibtext[1]); }
+
+<USER_VALUE>"}" { BEGIN INITIAL; /* return to normal mode */
+ smtliblval.str = new std::string(_string_lit);
+ return USER_VAL_TOK; }
+
+<USER_VALUE>"\n" { _string_lit.insert(_string_lit.end(),'\n');
+ CVC4::parserTemp->lineNum++; }
+<USER_VALUE>. { _string_lit.insert(_string_lit.end(),*smtlibtext); }
+
+"true" { return TRUE_TOK; }
+"false" { return FALSE_TOK; }
+"ite" { return ITE_TOK; }
+"not" { return NOT_TOK; }
+"implies" { return IMPLIES_TOK; }
+"if_then_else" { return IF_THEN_ELSE_TOK; }
+"and" { return AND_TOK; }
+"or" { return OR_TOK; }
+"xor" { return XOR_TOK; }
+"iff" { return IFF_TOK; }
+"exists" { return EXISTS_TOK; }
+"forall" { return FORALL_TOK; }
+"let" { return LET_TOK; }
+"flet" { return FLET_TOK; }
+"notes" { return NOTES_TOK; }
+"cvc_command" { return CVC_COMMAND_TOK; }
+"logic" { return LOGIC_TOK; }
+"sat" { return SAT_TOK; }
+"unsat" { return UNSAT_TOK; }
+"unknown" { return UNKNOWN_TOK; }
+"assumption" { return ASSUMPTION_TOK; }
+"formula" { return FORMULA_TOK; }
+"status" { return STATUS_TOK; }
+"benchmark" { return BENCHMARK_TOK; }
+"extrasorts" { return EXTRASORTS_TOK; }
+"extrafuns" { return EXTRAFUNS_TOK; }
+"extrapreds" { return EXTRAPREDS_TOK; }
+"distinct" { return DISTINCT_TOK; }
+":pattern" { return PAT_TOK; }
+":" { return COLON_TOK; }
+"\[" { return LBRACKET_TOK; }
+"\]" { return RBRACKET_TOK; }
+"{" { return LCURBRACK_TOK;}
+"}" { return RCURBRACK_TOK;}
+"(" { return LPAREN_TOK; }
+")" { return RPAREN_TOK; }
+"$" { return DOLLAR_TOK; }
+"?" { return QUESTION_TOK; }
+
+[=<>&@#+\-*/%|~]+ { smtliblval.str = new std::string(smtlibtext); return AR_SYMB; }
+({LETTER})({IDCHAR})* {smtliblval.str = new std::string(smtlibtext); return SYM_TOK; }
+
+<<EOF>> { return EOF_TOK; }
+
+. { smtliberror("Illegal input character."); }
+%%
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback