diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-12 20:38:10 +0000 |
commit | 13a6669a35aee32c03f8d29fe386aca95d2fbd8f (patch) | |
tree | b126afb6c384dd45db0249e8096cf733a74daa95 /src/parser | |
parent | 5b5474281c4cdc880bff8b9e38b84dc84f88e50c (diff) |
parser, minisat, other things..
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 18 | ||||
-rw-r--r-- | src/parser/parser.cpp | 21 | ||||
-rw-r--r-- | src/parser/pl.ypp | 1993 | ||||
-rw-r--r-- | src/parser/pl_scanner.lpp | 352 | ||||
-rw-r--r-- | src/parser/smtlib.ypp | 1553 | ||||
-rw-r--r-- | src/parser/smtlib_scanner.lpp | 260 |
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."); } +%% + |