From 6f6a6bc95e661996a08b882ef6c7fdbdd0140e80 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 24 Nov 2009 21:28:03 +0000 Subject: [PATCH] Partial parser for booleans --- README | 9 +- src/include/theory.h | 81 ++ src/parser/Makefile.am | 16 +- src/parser/parser_state.h | 2 + src/parser/pl.ypp | 1828 ++----------------------------------- src/parser/pl_scanner.lpp | 1 + src/util/command.h | 3 +- 7 files changed, 198 insertions(+), 1742 deletions(-) create mode 100644 src/include/theory.h diff --git a/README b/README index b6b20aba8..3608dfef0 100644 --- a/README +++ b/README @@ -2,9 +2,12 @@ This is a prerelease version of CVC4; distribution is restricted. For a suggestion of editing CVC4 code with emacs, see README.emacs. -To build, use the top-level script "autogen.sh" to invoke various -autotools. You'll need reasonably new automake, autoconf, and libtool -installed. Then ./configure && make as usual. +To build, you'll need reasonably new automake, autoconf, and libtool +installed. Execute, + + ./autogen.sh + ./configure + make To build a source release, use "make dist"; this will include the configure script and all the bits of automake/autoconf/libtool that diff --git a/src/include/theory.h b/src/include/theory.h new file mode 100644 index 000000000..47b4a2d92 --- /dev/null +++ b/src/include/theory.h @@ -0,0 +1,81 @@ +/********************* -*- C++ -*- */ +/** theory.h + ** This file is part of the CVC4 prototype. + ** + ** The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + **/ + +#ifndef __CVC4_THEORY_H +#define __CVC4_THEORY_H + +#include "expr.h" +#include "literal.h" + +namespace CVC4 { + +/** + * Base class for T-solvers. Abstract DPLL(T). + */ +class Theory { +public: + /** + * Subclasses of Theory may add additional efforts. DO NOT CHECK + * equality with one of these values (e.g. if STANDARD xxx) but + * rather use range checks (or use the helper functions below). + * Normally we call QUICK_CHECK or STANDARD; at the leaves we call + * with MAX_EFFORT. + */ + enum Effort { + MIN_EFFORT = 0, + QUICK_CHECK = 10, + STANDARD = 50, + FULL_EFFORT = 100 + };/* enum Effort */ + + // TODO add compiler annotation "constant function" here + static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; } + static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; } + static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; } + static bool standardEffortOrMore(Effort e) { return e >= STANDARD; } + static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; } + static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } + + /** + * Prepare for an Expr. + */ + virtual void setup(Expr) = 0; + + /** + * Assert a literal in the current context. + */ + virtual void assert(Literal) = 0; + + /** + * Check the current assignment's consistency. Return false iff inconsistent. + */ + virtual bool check(Effort level = FULL_EFFORT) = 0; + + /** + * T-propagate new literal assignments in the current context. + */ + // TODO design decisoin: instead of returning a set of literals + // here, perhaps we have an interface back into the prop engine + // where we assert directly. we might sometimes unknowingly assert + // something clearly inconsistent (esp. in a parallel context). + // This would allow the PropEngine to cancel our further work since + // we're already inconsistent---also could strategize dynamically on + // whether enough theory prop work has occurred. + virtual void propagate(Callback propagator, Effort level = FULL_EFFORT) = 0; + + /** + * Return an explanation for the literal (which was previously propagated by this theory).. + */ + virtual Expr explain(Literal) = 0; + +};/* class Theory */ + +}/* CVC4 namespace */ + +#endif /* __CVC4_THEORY_H */ diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index e83605d29..7965b88f9 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -6,18 +6,18 @@ noinst_LTLIBRARIES = libparser.la libparser_la_SOURCES = \ pl_scanner.lpp \ - pl.ypp \ - smtlib_scanner.lpp \ - smtlib.ypp \ - parser.cpp + pl.ypp # \ + # smtlib_scanner.lpp \ + # smtlib.ypp \ + # parser.cpp BUILT_SOURCES = \ pl_scanner.cpp \ pl.cpp \ - pl.hpp \ - smtlib_scanner.cpp \ - smtlib.cpp \ - smtlib.hpp + pl.hpp # \ + # smtlib_scanner.cpp \ + # smtlib.cpp \ + # smtlib.hpp # produce headers too AM_YFLAGS = -d diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index c1fd0ae96..4eda5eb38 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -20,6 +20,7 @@ #include #include #include "cvc4_expr.h" +#include "expr/expr_manager.h" #include "util/exception.h" namespace CVC4 { @@ -40,6 +41,7 @@ private: std::string prompt; public: SmtEngine* vc; + ExprManager* exprManager; std::istream* is; // The current input line int lineNum; diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index 012f468eb..71809b049 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -16,6 +16,10 @@ #include "cvc4.h" #include "parser/parser_exception.h" #include "parser/parser_state.h" +#include "cvc4_expr.h" +#include "expr/expr_builder.h" +#include "expr/expr_manager.h" +#include "util/command.h" //#include "rational.h" // Exported shared data @@ -29,6 +33,7 @@ namespace CVC4 { #define TMP CVC4::parser::parserState #define EXPR CVC4::parser::parserState->expr #define VC (CVC4::parser::parserState->vc) +#define EM (CVC4::parser::parserState->exprManager) #define RAT(args) CVC4::newRational args // Suppress the bogus warning suppression in bison (it generates @@ -46,136 +51,26 @@ int PLerror(const char *s) return CVC4::parser::parserState->error(ss.str()); } - -namespace CVC4 { - -// File-static auxiliary funcion to wrap accessors upto the index i -// (not inclusive) around "e". Used to rebuild the UPDATE expressions. -static Expr wrapAccessors(const Expr& e, - const std::vector& accessors, - const int i) { - DebugAssert((int)accessors.size() >= i, "wrapAccessors: too few accessors"); - Expr res(e); - for(int j=0; jlistExpr(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 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& updates, - size_t idx=0) { - // Processed all the updates - if(idx >= updates.size()) return e; - return PLprocessUpdates(PLprocessUpdate(e, updates[idx]), updates, idx+1); -} - - - -} // end of namespace CVC4 - #define YYLTYPE_IS_TRIVIAL 1 #define YYMAXDEPTH 10485760 /* Prefer YYERROR_VERBOSE over %error-verbose to avoid errors in older bison */ #define YYERROR_VERBOSE 1 + +using namespace CVC4; + %} %union { std::string *str; - CVC4::Expr *node; + CVC4::Expr *expr; + CVC4::Command *cmd; std::vector *vec; int kind; }; -%start cmd +// %start cmd +%start Query /* strings are for better error messages. "_TOK" is so macros don't conflict with kind names */ @@ -360,1625 +255,98 @@ static Expr PLprocessUpdates(const CVC4::Expr& e, %nonassoc '{' '.' '(' %nonassoc BITVECTOR_TOK -%type FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors -%type LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls -%type Exprs AndExpr OrExpr Pattern Patterns -%type RecordEntries UpdatePosition Updates - -%type Type /* IndexType */ TypeNotIdentifier TypeDef -%type DataType SingleDataType Constructor -%type FunctionType RecordType Real Int BitvectorType -%type FieldDecl TupleType -%type ArrayType ScalarType SubType BasicType SubrangeType -%type LeftBound RightBound -%type Expr Conditional UpdatePositionNode Update Lambda -%type QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral -%type LetDecl LetExpr LetDeclsNode -%type TypeLetDecl TypeLetExpr TypeLetDeclsNode -%type BoundVarDecl BoundVarDeclNode VarDecl -%type ConstDecl TypeDecl -%type Identifier StringLiteral Numeral Binary Hex - -%type Assert Query Help Dbg Trace Option -%type Transform Print Call Echo DumpCommand -%type Include Where Push Pop PopTo -%type Context Forget Get_Child Get_Op Get_Type Check_Type Substitute -%type other_cmd -%type Arith_Var_Order +// %type FieldDecls TypeList IDs reverseIDs SingleDataTypes Constructors +// %type LetDecls TypeLetDecls BoundVarDecls ElseRest VarDecls +// %type Exprs AndExpr OrExpr Pattern Patterns +// %type RecordEntries UpdatePosition Updates + +// %type Type /* IndexType */ TypeNotIdentifier TypeDef +// %type DataType SingleDataType Constructor +// %type FunctionType RecordType Real Int BitvectorType +// %type FieldDecl TupleType +// %type ArrayType ScalarType SubType BasicType SubrangeType +// %type LeftBound RightBound +%type Expr // Conditional UpdatePositionNode Update Lambda +// %type QuantExpr ArrayLiteral RecordLiteral RecordEntry TupleLiteral +// %type LetDecl LetExpr LetDeclsNode +// %type TypeLetDecl TypeLetExpr TypeLetDeclsNode +// %type BoundVarDecl BoundVarDeclNode VarDecl +// %type ConstDecl TypeDecl + // %type Identifier // StringLiteral Numeral Binary Hex + + // %type cmd Assert Query // Help Dbg Trace Option +%type Query // Help Dbg Trace Option +// %type Transform Print Call Echo DumpCommand +// %type Include Where Push Pop PopTo +// %type Context Forget Get_Child Get_Op Get_Type Check_Type Substitute +// %type other_cmd +// %type Arith_Var_Order %token 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 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; - $$->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; - $$->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; - $$->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 temp; - temp.push_back(*$1); - temp.push_back(*$3); - - $$ = new CVC4::Expr(VC->listExpr("_ARROW", temp)); - delete $1; delete $3; - } - | '(' TypeList ')' ARROW_TOK Type - { - $2->push_back(*$5); - $$ = new CVC4::Expr(VC->listExpr("_ARROW", *$2)); - delete $2; delete $5; - } - ; - -RecordType : SQHASH_TOK FieldDecls HASHSQ_TOK - { - $$ = new CVC4::Expr(VC->listExpr(*$2)); - delete $2; - } - ; +// cmd: +// Assert { $$ = $1; } +// | Query { $$ = $1; } -FieldDecls : FieldDecl - { - $$ = new std::vector; - $$->push_back(VC->idExpr("_RECORD_TYPE")); - $$->push_back(*$1); - delete $1; - } - | FieldDecls ',' FieldDecl - { - $1->push_back(*$3); - $$ = $1; - delete $3; - } - ; +// Assert: +// ASSERT_TOK Expr { +// $$ = NULL; // new CVC3::Expr(VC->listExpr("_ASSERT", *$2)); +// // delete $2; +// } ; -FieldDecl : Identifier ':' Type - { - $$ = new CVC4::Expr(VC->listExpr(*$1, *$3)); - delete $1; - delete $3; - } - ; - -TupleType : '[' TypeList ']' - { - $$ = new CVC4::Expr(VC->listExpr("_TUPLE_TYPE", *$2)); - delete $2; - } - ; - -TypeList : Type ',' Type - { - $$ = new std::vector; - $$->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::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; - $$->push_back(*$1); - delete $1; - } - | Identifier ',' reverseIDs - { - $3->push_back(*$1); - $$ = $3; - delete $1; - } - ; - -IDs : reverseIDs - { - $$ = new std::vector($1->rbegin(), - $1->rend()); - delete $1; - } - ; - -/* Grammar for exprs */ - -Expr : Identifier { $$ = $1; } - | Numeral { $$ = $1; } - | Binary { $$ = $1; } - | Hex { $$ = $1; } - | Expr '(' Exprs ')' - { - std::vector 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 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; - $$->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; - $$->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 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; - $$->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; - $$->push_back(*$1); - delete $1; - } - | Exprs ',' Expr - { - $1->push_back(*$3); - $$ = $1; - delete $3; - } - ; - - -Pattern : PATTERN_TOK '(' Exprs ')' ':' - { - $$ = $3; - } - -Patterns : Pattern - { - $$ = new std::vector; - $$->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; - $$->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; - $$->push_back(VC->listExpr("_READ", *$2)); - delete $2; - } - | Identifier - { - $$ = new std::vector; - $$->push_back(*$1); - delete $1; - } - | '.' Identifier - { - $$ = new std::vector; - $$->push_back(VC->listExpr("_RECORD_SELECT", *$2)); - delete $2; - } - | '.' Numeral - { - $$ = new std::vector; - $$->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; - $$->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; - $$->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; - $$->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; - $$->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 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 tmp; - tmp.push_back(VC->idExpr("_DEFUN")); - tmp.push_back(*$1); - tmp.push_back(*$3); - tmp.push_back(*$6); - $$ = new CVC4::Expr(VC->listExpr(tmp)); - delete $1; - delete $3; - delete $6; - } - | Identifier ',' IDs ':' Type - { - $3->insert($3->begin(), *$1); - $$ = new CVC4::Expr(VC->listExpr("_CONST", VC->listExpr(*$3), *$5)); - delete $1; - delete $3; - delete $5; - } - ; +Query: + QUERY_TOK Expr { + $$ = NULL; // exprManager->mkExpr(Kind.TRUE); + } + | CHECKSAT_TOK Expr { + $$ = NULL; //new CVC3::Expr(VC->listExpr("_CHECKSAT", *$2)); + // delete $2; + } + | CHECKSAT_TOK { + $$ = NULL; + // new CVC3::Expr(VC->listExpr(VC->idExpr("_CHECKSAT"))); + } ; + +Expr: +// Identifier { $$ = $1; } +// | + TRUELIT_TOK { + $$ = new Expr(EM->mkExpr(TRUE)); + } + | FALSELIT_TOK { + $$ = new Expr(EM->mkExpr(FALSE)); + } + | Expr OR_TOK Expr { + $$ = new Expr(EM->mkExpr(OR, *$1, *$3)); + delete $1; + delete $3; + } + | Expr AND_TOK Expr { + $$ = new Expr(EM->mkExpr(AND, *$1, *$3)); + delete $1; + delete $3; + } + // | Expr IMPLIES_TOK Expr + // { + // $$ = new CVC3::Expr(VC->listExpr("_IMPLIES", *$1, *$3)); + // delete $1; + // delete $3; + // } + // | Expr IFF_TOK Expr + // { + // $$ = new CVC3::Expr(VC->listExpr("_IFF", *$1, *$3)); + // delete $1; + // delete $3; + // } +; + + +// Identifier: +// ID_TOK { +// $$ = EM->mkExpr(VARIABLE, *$1); +// delete $1; +// } -TypeDecl : DataType { $$ = $1; } - | Identifier ':' TYPE_TOK '=' TypeDef - { - $$ = new CVC4::Expr(VC->listExpr("_TYPEDEF", *$1, *$5)); - delete $1; - delete $5; - } - | Identifier ':' TYPE_TOK - { - $$ =new CVC4::Expr(VC->listExpr("_TYPE", *$1)); - delete $1; - } - | Identifier ',' IDs ':' TYPE_TOK - { - std::vector 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 index 262eb5c88..5ffd6b93b 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -22,6 +22,7 @@ #include #include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */ +#include "util/command.h" #include "parser/parser_state.h" #include "parser/pl.hpp" #include "util/debug.h" diff --git a/src/util/command.h b/src/util/command.h index d1257f323..36097b7a5 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -14,7 +14,8 @@ namespace CVC4 { -class Command { // distinct from Exprs +class Command { + // distinct from Exprs }; }/* CVC4 namespace */ -- 2.30.2