diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-23 05:15:56 +0000 |
| commit | 57b8c4c8581d2d3ffcf3d3a1bb228271cb4d074a (patch) | |
| tree | 1c1781cc83118e4bbd2ad6939b16734c30a69f1a | |
| parent | 673d0e86b91094a58433c3ca71591fb0a0c60f84 (diff) | |
* reviewed BooleanSimplification, added documentation & unit test
* work around a lexer ambiguity in CVC grammar
* add support for tracing antlr parser/lexer
* add parsing support for more language features
* initial parameterized types parsing work to support Andy's work
31 files changed, 1337 insertions, 195 deletions
diff --git a/contrib/switch-config b/contrib/switch-config index 83351da29..98ed10329 100755 --- a/contrib/switch-config +++ b/contrib/switch-config @@ -38,7 +38,7 @@ if ! [ -e builds/current ]; then exit 1 fi -current=(`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]\+\)/\(.*\),\1 \2,'`) +current=(`grep '^CURRENT_BUILD' builds/current | sed 's,^CURRENT_BUILD *= *\([^/]*\)/\(.*\),\1 \2,'`) arch=${current[0]} build=${current[1]} diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 74bfd3f2b..b7000fea6 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -188,11 +188,11 @@ size_t Expr::getNumChildren() const { return d_node->getNumChildren(); } -Expr Expr::getChild(unsigned int i) const { +Expr Expr::operator[](unsigned i) const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(i >= 0 && i < d_node->getNumChildren(), "Child index out of bounds"); - return Expr(d_exprManager,new Node((*d_node)[i])); + return Expr(d_exprManager, new Node((*d_node)[i])); } bool Expr::hasOperator() const { diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 291016044..24cb6dc5d 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -267,7 +267,7 @@ public: * @param i the index of the child to retrieve * @return the child */ - Expr getChild(unsigned int i) const; + Expr operator[](unsigned i) const; /** * Check if this is an expression that has an operator. diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 9ec8774f0..2b90da502 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -53,7 +53,8 @@ libcvc4parser_la_SOURCES = \ parser.cpp \ parser_builder.h \ parser_builder.cpp \ - parser_exception.h + parser_exception.h \ + antlr_tracing.h libcvc4parser_noinst_la_SOURCES = \ antlr_input.h \ @@ -71,5 +72,8 @@ libcvc4parser_noinst_la_SOURCES = \ parser.cpp \ parser_builder.h \ parser_builder.cpp \ - parser_exception.h + parser_exception.h \ + antlr_tracing.h +EXTRA_DIST = \ + Makefile.antlr_tracing diff --git a/src/parser/Makefile.antlr_tracing b/src/parser/Makefile.antlr_tracing new file mode 100644 index 000000000..087554c52 --- /dev/null +++ b/src/parser/Makefile.antlr_tracing @@ -0,0 +1,21 @@ +# -*-makefile-*- +# +# This makefile is included from parser directories in order to +# do antlr tracing. THIS IS VERY MUCH A HACK, and is only enabled +# if CVC4_TRACE_ANTLR is defined (and not 0). In ANTLR 3.2, we +# have to #define +# + +ifeq ($(CVC4_TRACE_ANTLR),) +else + +ifeq ($(CVC4_TRACE_ANTLR),0) +else + +AM_CPPFLAGS += -DCVC4_TRACE_ANTLR +ANTLR_OPTS += -trace + +endif + +endif + diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h new file mode 100644 index 000000000..2c3e66c12 --- /dev/null +++ b/src/parser/antlr_tracing.h @@ -0,0 +1,87 @@ +/********************* */ +/*! \file antlr_tracing.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#ifndef __CVC4__PARSER__ANTLR_TRACING_H +#define __CVC4__PARSER__ANTLR_TRACING_H + +// only enable the hack with -DCVC4_TRACE_ANTLR +#ifdef CVC4_TRACE_ANTLR + +#include <iostream> +#include <string> +#include "util/output.h" + +/* The ANTLR lexer generator, as of v3.2, puts Java trace commands + * into our beautiful generated C lexer! How awful! This is clearly + * a bug (the parser generator traces with printf()), but we have to + * do something about it. Basically, the things look like this: + * + * System.out.println("something"+somethingElse+"another thing"); + * + * What to do to make this C++?! Alas, you cannot + * "#define System.out.println", because it has dots in it. + * So we do the following. Sigh. + * + * This is all C++, and the generated lexer/parser is C++, but that's + * ok here, we use the C++ compiler anyway! Plus, this is only code + * for **debugging** lexers and parsers. + */ + +/** A "System" object, just like in Java! */ +static struct __Cvc4System { + /** + * Helper class just to handle arbitrary string concatenation + * with Java syntax. In C++ you cannot do "char*" + "char*", + * so instead we fool the type system into calling + * JavaPrinter::operator+() for each item successively. + */ + struct JavaPrinter { + template <class T> + JavaPrinter operator+(const T& t) const { + ::CVC4::Message() << t; + return JavaPrinter(); + } + };/* struct JavaPrinter */ + + /** A "System.out" object, just like in Java! */ + struct { + /** + * By the time println() is called, we've completely + * evaluated (and thus printed) its entire argument, thanks + * to the call-by-value semantics of C. All that's left to + * do is print the newline. + */ + void println(JavaPrinter) { ::CVC4::Message() << std::endl; } + } out; +} System; + +// Now define println(): this kicks off the successive operator+() calls +// Also define "failed" because ANTLR 3.3 uses "failed" improperly. +// These are highly dependent on the bugs in a particular ANTLR release. +// These seem to work with ANTLR 3.3 as of 4/23/2011. A different trick +// works with ANTLR 3.2. EXPECT LOTS OF COMPILER WARNINGS. +#define println(x) println(({int failed=0;__Cvc4System::JavaPrinter()+x;})) +#undef ANTLR3_FPRINTF +#define ANTLR3_FPRINTF(args...) {int failed=0;fprintf(args);} +#undef ANTLR3_PRINTF +#define ANTLR3_PRINTF(args...) {int failed=0;printf(args);} + +#endif /* CVC4_TRACE_ANTLR */ + +#endif /* __CVC4__PARSER__ANTLR_TRACING_H */ diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 6a94d877a..d77f72bfa 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -385,7 +385,8 @@ dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) static ANTLR3_MARKER mark (pANTLR3_INT_STREAM is) { - Unreachable(); + is->lastMarker = is->index(is); + return is->lastMarker; } /// As per mark() but with a call to tell the debugger we are doing this @@ -435,7 +436,7 @@ rewindLast (pANTLR3_INT_STREAM is) static void rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - Unreachable(); + is->seek(is, (ANTLR3_UINT32)(marker)); } static void dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) @@ -446,7 +447,13 @@ dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) static void seek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - Unreachable(); + pANTLR3_COMMON_TOKEN_STREAM cts; + pANTLR3_TOKEN_STREAM ts; + + ts = (pANTLR3_TOKEN_STREAM) is->super; + cts = (pANTLR3_COMMON_TOKEN_STREAM) ts->super; + + cts->p = (ANTLR3_UINT32)index; } static void dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 543538f32..bd0524f61 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -11,9 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Parser for CVC-LIB input language. + ** \brief Parser for CVC presentation input language ** - ** Parser for CVC-LIB input language. + ** Parser for CVC input language. **/ grammar Cvc; @@ -26,16 +26,63 @@ options { // defaultErrorHandler = false; // Only lookahead of <= k requested (disable for LL* parsing) - k = 2; -} + // Note that CVC4's BoundedTokenBuffer requires a fixed k ! + // If you change this k, change it also in cvc_input.cpp ! + k = 3; +}/* options */ tokens { - // Keywords + /* commands */ - AND_TOK = 'AND'; ASSERT_TOK = 'ASSERT'; - BOOLEAN_TOK = 'BOOLEAN'; + QUERY_TOK = 'QUERY'; CHECKSAT_TOK = 'CHECKSAT'; + OPTION_TOK = 'OPTION'; + PUSH_TOK = 'PUSH'; + POP_TOK = 'POP'; + POPTO_TOK = 'POPTO'; + PUSH_SCOPE_TOK = 'PUSH_SCOPE'; + POP_SCOPE_TOK = 'POP_SCOPE'; + POPTO_SCOPE_TOK = 'POPTO_SCOPE'; + RESET_TOK = 'RESET'; + DATATYPE_TOK = 'DATATYPE'; + END_TOK = 'END'; + CONTEXT_TOK = 'CONTEXT'; + FORGET_TOK = 'FORGET'; + GET_TYPE_TOK = 'GET_TYPE'; + CHECK_TYPE_TOK = 'CHECK_TYPE'; + GET_CHILD_TOK = 'GET_CHILD'; + GET_OP_TOK = 'GET_OP'; + SUBSTITUTE_TOK = 'SUBSTITUTE'; + DBG_TOK = 'DBG'; + TRACE_TOK = 'TRACE'; + UNTRACE_TOK = 'UNTRACE'; + HELP_TOK = 'HELP'; + TRANSFORM_TOK = 'TRANSFORM'; + PRINT_TOK = 'PRINT'; + PRINT_TYPE_TOK = 'PRINT_TYPE'; + CALL_TOK = 'CALL'; + ECHO_TOK = 'ECHO'; + INCLUDE_TOK = 'INCLUDE'; + DUMP_PROOF_TOK = 'DUMP_PROOF'; + DUMP_ASSUMPTIONS_TOK = 'DUMP_ASSUMPTIONS'; + DUMP_SIG_TOK = 'DUMP_SIG'; + DUMP_TCC_TOK = 'DUMP_TCC'; + DUMP_TCC_ASSUMPTIONS_TOK = 'DUMP_TCC_ASSUMPTIONS'; + DUMP_TCC_PROOF_TOK = 'DUMP_TCC_PROOF'; + DUMP_CLOSURE_TOK = 'DUMP_CLOSURE'; + DUMP_CLOSURE_PROOF_TOK = 'DUMP_CLOSURE_PROOF'; + WHERE_TOK = 'WHERE'; + ASSERTIONS_TOK = 'ASSERTIONS'; + ASSUMPTIONS_TOK = 'ASSUMPTIONS'; + COUNTEREXAMPLE_TOK = 'COUNTEREXAMPLE'; + COUNTERMODEL_TOK = 'COUNTERMODEL'; + ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER'; + + /* operators */ + + AND_TOK = 'AND'; + BOOLEAN_TOK = 'BOOLEAN'; ECHO_TOK = 'ECHO'; ELSEIF_TOK = 'ELSIF'; ELSE_TOK = 'ELSE'; @@ -46,22 +93,13 @@ tokens { INT_TOK = 'INT'; LET_TOK = 'LET'; NOT_TOK = 'NOT'; - OPTION_TOK = 'OPTION'; OR_TOK = 'OR'; - POPTO_TOK = 'POPTO'; - POP_TOK = 'POP'; - PRINT_TOK = 'PRINT'; - PUSH_TOK = 'PUSH'; - QUERY_TOK = 'QUERY'; REAL_TOK = 'REAL'; THEN_TOK = 'THEN'; TRUE_TOK = 'TRUE'; TYPE_TOK = 'TYPE'; XOR_TOK = 'XOR'; - DATATYPE_TOK = 'DATATYPE'; - END_TOK = 'END'; - ARRAY_TOK = 'ARRAY'; OF_TOK = 'OF'; WITH_TOK = 'WITH'; @@ -86,8 +124,6 @@ tokens { RBRACKET = ']'; SEMICOLON = ';'; BAR = '|'; - DOT = '.'; - DOTDOT = '..'; UNDERSCORE = '_'; SQHASH = '[#'; @@ -95,6 +131,9 @@ tokens { PARENHASH = '(#'; HASHPAREN = '#)'; + DOT = '.'; + DOTDOT = '..'; + // Operators ARROW_TOK = '->'; @@ -158,7 +197,7 @@ tokens { BVSGT_TOK = 'BVSGT'; BVSLE_TOK = 'BVSLE'; BVSGE_TOK = 'BVSGE'; -} +}/* tokens */ @parser::members { @@ -171,7 +210,7 @@ bool isRightToLeft(int type) { case IMPLIES_TOK: return true; default: return false; } -} +}/* isRightToLeft() */ int getOperatorPrecedence(int type) { switch(type) { @@ -247,7 +286,7 @@ int getOperatorPrecedence(int type) { default: Unhandled(CvcParserTokenNames[type]); } -} +}/* getOperatorPrecedence() */ Kind getOperatorKind(int type, bool& negate) { negate = false; @@ -276,7 +315,7 @@ Kind getOperatorKind(int type, bool& negate) { case DIV_TOK: return kind::DIVISION; case EXP_TOK: Unhandled(CvcParserTokenNames[type]); - // concatBitwiseBinop + // bvBinop case CONCAT_TOK: return kind::BITVECTOR_CONCAT; case BAR: return kind::BITVECTOR_OR; case BVAND_TOK: return kind::BITVECTOR_AND; @@ -284,7 +323,7 @@ Kind getOperatorKind(int type, bool& negate) { default: Unhandled(CvcParserTokenNames[type]); } -} +}/* getOperatorKind() */ unsigned findPivot(const std::vector<unsigned>& operators, unsigned startIndex, unsigned stopIndex) { @@ -305,7 +344,7 @@ unsigned findPivot(const std::vector<unsigned>& operators, } } return pivot; -} +}/* findPivot() */ Expr createPrecedenceTree(ExprManager* em, const std::vector<CVC4::Expr>& expressions, @@ -327,7 +366,7 @@ Expr createPrecedenceTree(ExprManager* em, createPrecedenceTree(em, expressions, operators, startIndex, pivot), createPrecedenceTree(em, expressions, operators, pivot + 1, stopIndex)); return negate ? em->mkExpr(kind::NOT, e) : e; -} +}/* createPrecedenceTree() recursive variant */ Expr createPrecedenceTree(ExprManager* em, const std::vector<CVC4::Expr>& expressions, @@ -348,7 +387,7 @@ Expr createPrecedenceTree(ExprManager* em, Debug("prec") << "=> " << e << std::endl; } return e; -} +}/* createPrecedenceTree() base variant */ /** Add n NOTs to the front of e and return the result. */ Expr addNots(ExprManager* em, size_t n, Expr e) { @@ -356,22 +395,23 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { e = em->mkExpr(kind::NOT, e); } return e; -} +}/* addNots() */ }/* @parser::members */ @header { /** ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing ** information. **/ -} +}/* @header */ @lexer::includes { + /** This suppresses warnings about the redefinition of token symbols between different * parsers. The redefinitions should be harmless as long as no client: (a) #include's * the lexer headers for two grammars AND (b) uses the token symbol definitions. */ @@ -383,11 +423,20 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { * Otherwise, we have to let the lexer detect the encoding at runtime. */ #define ANTLR3_INLINE_INPUT_ASCII -} + +#include "parser/antlr_tracing.h" +#include "util/integer.h" +#include "parser/antlr_input.h" +#include "parser/parser.h" + +}/* @lexer::includes */ @parser::includes { + #include "expr/command.h" #include "parser/parser.h" +#include "util/subrange_bound.h" +#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; @@ -402,27 +451,55 @@ namespace CVC4 { * them to be constructible by a uintptr_t. So we derive the string * class to provide just such a conversion. */ - class mystring : public std::string { + class myString : public std::string { public: - mystring(const std::string& s) : std::string(s) {} - mystring(uintptr_t) : std::string() {} - mystring() : std::string() {} - };/* class mystring */ + myString(const std::string& s) : std::string(s) {} + myString(uintptr_t) : std::string() {} + myString() : std::string() {} + };/* class myString */ + + /** + * Just exists to give us the uintptr_t construction that + * ANTLR requires. + */ + class mySubrangeBound : public CVC4::SubrangeBound { + public: + mySubrangeBound() : CVC4::SubrangeBound() {} + mySubrangeBound(uintptr_t) : CVC4::SubrangeBound() {} + mySubrangeBound(const Integer& i) : CVC4::SubrangeBound(i) {} + mySubrangeBound(const SubrangeBound& b) : CVC4::SubrangeBound(b) {} + };/* class mySubrangeBound */ }/* CVC4::parser::cvc namespace */ }/* CVC4::parser namespace */ }/* CVC4 namespace */ -} +}/* @parser::includes */ @parser::postinclude { + #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "util/output.h" + #include <vector> +#define REPEAT_COMMAND(k, CommandCtor) \ + ({ \ + unsigned __k = (k); \ + (__k <= 1) \ + ? (Command*) new CommandCtor \ + : ({ \ + CommandSequence* __seq = new CommandSequence(); \ + while(__k-- > 0) { \ + __seq->addCommand(new CommandCtor); \ + } \ + (Command*) __seq; \ + }); \ + }) + using namespace CVC4; using namespace CVC4::parser; @@ -436,8 +513,9 @@ using namespace CVC4::parser; #define MK_EXPR EXPR_MANAGER->mkExpr #undef MK_CONST #define MK_CONST EXPR_MANAGER->mkConst -} +#define UNSUPPORTED PARSER_STATE->unimplementedFeature +}/* @parser::postinclude */ /** * Parses an expression. @@ -453,30 +531,78 @@ parseExpr returns [CVC4::Expr expr] * @return the command of the benchmark */ parseCommand returns [CVC4::Command* cmd] - : c = command { $cmd = c; } + : c=command { $cmd = c; } + | EOF { $cmd = NULL; } ; /** * Matches a command of the input. If a declaration, it will return an empty * command. */ -command returns [CVC4::Command* cmd = 0] +command returns [CVC4::Command* cmd = NULL] + : ( mainCommand[cmd] SEMICOLON + | SEMICOLON + | LET_TOK { PARSER_STATE->pushScope(); } + typeOrVarLetDecl[CHECK_DECLARED] ( COMMA typeOrVarLetDecl[CHECK_DECLARED] )* + IN_TOK c=command + { $cmd = c; + PARSER_STATE->popScope(); + } + ) + { if($cmd == NULL) { + cmd = new EmptyCommand(); + } + } + ; + +typeOrVarLetDecl[CVC4::parser::DeclarationCheck check] +options { backtrack = true; } + : letDecl | typeLetDecl[check] + ; + +mainCommand[CVC4::Command*& cmd] @init { Expr f; SExpr sexpr; - std::string s; + std::string id; Type t; std::vector<CVC4::Datatype> dts; Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl; + std::string s; + k = 0; } - : ASSERT_TOK formula[f] SEMICOLON { cmd = new AssertCommand(f); } - | QUERY_TOK formula[f] SEMICOLON { cmd = new QueryCommand(f); } - | CHECKSAT_TOK formula[f] SEMICOLON { cmd = new CheckSatCommand(f); } - | CHECKSAT_TOK SEMICOLON { cmd = new CheckSatCommand(MK_CONST(true)); } - | OPTION_TOK STRING_LITERAL symbolicExpr[sexpr] SEMICOLON - { cmd = new SetOptionCommand(AntlrInput::tokenText($STRING_LITERAL), sexpr); } - | PUSH_TOK SEMICOLON { cmd = new PushCommand(); } - | POP_TOK SEMICOLON { cmd = new PopCommand(); } + /* our bread & butter */ + : ASSERT_TOK formula[f] { cmd = new AssertCommand(f); } + + | QUERY_TOK formula[f] { cmd = new QueryCommand(f); } + | CHECKSAT_TOK formula[f] { cmd = new CheckSatCommand(f); } + | CHECKSAT_TOK { cmd = new CheckSatCommand(MK_CONST(true)); } + + /* options */ + | OPTION_TOK + ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + symbolicExpr[sexpr] + { cmd = new SetOptionCommand(s, sexpr); } + + /* push / pop */ + | PUSH_TOK k=numeral? + { cmd = REPEAT_COMMAND(k, PushCommand()); } + | POP_TOK k=numeral? + { cmd = REPEAT_COMMAND(k, PopCommand()); } + | POPTO_TOK k=numeral? + { UNSUPPORTED("POPTO command"); } + + /* push / pop scopes */ + | PUSH_SCOPE_TOK k=numeral? + { UNSUPPORTED("PUSH_SCOPE command"); } + | POP_SCOPE_TOK k=numeral? + { UNSUPPORTED("POP_SCOPE command"); } + | POPTO_SCOPE_TOK k=numeral? + { UNSUPPORTED("POPTO_SCOPE command"); } + + | RESET_TOK + { UNSUPPORTED("RESET command"); } + // Datatypes can be mututally-recursive if they're in the same // definition block, separated by a comma. So we parse everything // and then ask the ExprManager to resolve everything in one go. @@ -485,24 +611,117 @@ command returns [CVC4::Command* cmd = 0] PARSER_STATE->pushScope(); } datatypeDef[dts] ( COMMA datatypeDef[dts] )* - END_TOK SEMICOLON + END_TOK { PARSER_STATE->popScope(); cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + + | CONTEXT_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { UNSUPPORTED("CONTEXT command"); } + | { UNSUPPORTED("CONTEXT command"); } + ) + + | FORGET_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] + { UNSUPPORTED("FORGET command"); } + + | GET_TYPE_TOK formula[f] + { UNSUPPORTED("GET_TYPE command"); } + + | CHECK_TYPE_TOK formula[f] COLON type[t,CHECK_DECLARED] + { UNSUPPORTED("CHECK_TYPE command"); } + + | GET_CHILD_TOK formula[f] k=numeral + { UNSUPPORTED("GET_CHILD command"); } + + | GET_OP_TOK formula[f] + { UNSUPPORTED("GET_OP command"); } + + | SUBSTITUTE_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED] EQUAL_TOK + formula[f] LBRACKET identifier[id,CHECK_NONE,SYM_VARIABLE] ASSIGN_TOK formula[f] RBRACKET + { UNSUPPORTED("SUBSTITUTE command"); } + + /* Like the --debug command line option, DBG turns on both tracing + * and debugging. */ + | DBG_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { Debug.on(s); Trace.on(s); } + | { Message() << "Please specify what to debug." << std::endl; } + ) + + | TRACE_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { Trace.on(s); } + | { Message() << "Please specify something to trace." << std::endl; } + ) + | UNTRACE_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { Trace.off(s); } + | { Message() << "Please specify something to untrace." << std::endl; } + ) + + | HELP_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { Message() << "No help available for `" << s << "'." << std::endl; } + | { Message() << "Please use --help at the command line for help." << std::endl; } + ) + + | TRANSFORM_TOK formula[f] + { UNSUPPORTED("TRANSFORM command"); } + + | PRINT_TOK formula[f] + { UNSUPPORTED("PRINT command"); } + | PRINT_TYPE_TOK type[t,CHECK_DECLARED] + { UNSUPPORTED("PRINT_TYPE command"); } + + | CALL_TOK identifier[id,CHECK_NONE,SYM_VARIABLE] formula[f] + { UNSUPPORTED("CALL command"); } + + | ECHO_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { CVC4::Message() << s << std::endl; } + | { CVC4::Message() << std::endl; } + ) + + | INCLUDE_TOK + ( ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } ) + { UNSUPPORTED("INCLUDE command"); } + | { PARSER_STATE->parseError("No filename given to INCLUDE command"); } + ) + + | ( DUMP_PROOF_TOK + | DUMP_ASSUMPTIONS_TOK + | DUMP_SIG_TOK + | DUMP_TCC_TOK + | DUMP_TCC_ASSUMPTIONS_TOK + | DUMP_TCC_PROOF_TOK + | DUMP_CLOSURE_TOK + | DUMP_CLOSURE_PROOF_TOK + ) { UNSUPPORTED("DUMP* command"); } + + /* these are all synonyms */ + | ( WHERE_TOK | ASSERTIONS_TOK | ASSUMPTIONS_TOK ) + { cmd = new GetAssertionsCommand(); } + + | COUNTEREXAMPLE_TOK + { UNSUPPORTED("COUNTEREXAMPLE command"); } + | COUNTERMODEL_TOK + { UNSUPPORTED("COUNTERMODEL command"); } + + | ARITH_VAR_ORDER_TOK LPAREN formula[f] ( COMMA formula[f] )* RPAREN + { UNSUPPORTED("ARITH_VAR_ORDER command"); } + | toplevelDeclaration[cmd] - | SEMICOLON c=command { $cmd = c; } - | EOF ; symbolicExpr[CVC4::SExpr& sexpr] @declarations { std::vector<SExpr> children; + std::string s; } - : INTEGER_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($INTEGER_LITERAL)); } - | DECIMAL_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($DECIMAL_LITERAL)); } - | STRING_LITERAL - { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); } + : INTEGER_LITERAL ('.' DIGIT+)? + { sexpr = SExpr((const char*)$symbolicExpr.text->chars); } + | str[s] + { sexpr = SExpr(s); } | IDENTIFIER { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); } | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN @@ -520,7 +739,7 @@ toplevelDeclaration[CVC4::Command*& cmd] } : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON ( declareVariables[t,ids,true] { cmd = new DeclarationCommand(ids, t); } - | declareTypes[ids] { cmd = new DeclarationCommand(ids, EXPR_MANAGER->kindType()); } ) SEMICOLON + | declareTypes[ids] { cmd = new DeclarationCommand(ids, EXPR_MANAGER->kindType()); } ) ; /** @@ -681,7 +900,6 @@ identifierList[std::vector<std::string>& idList, ( COMMA identifier[id,check,type] { idList.push_back(id); } )* ; - /** * Matches an identifier and returns a string. */ @@ -774,6 +992,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } /* named types */ : identifier[id,check,SYM_SORT] + parameterization[check]? { if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(id, SYM_SORT)) { t = PARSER_STATE->getSort(id); @@ -788,15 +1007,23 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, /* subtypes */ | SUBTYPE_TOK LPAREN formula[f] ( COMMA formula[f] )? RPAREN - { PARSER_STATE->unimplementedFeature("subtypes not supported yet"); + { UNSUPPORTED("subtypes not supported yet"); t = Type(); } /* subrange types */ -/* parsing not working -- some kind of conflict betw [0..1] and 0.0 - | bounds - { PARSER_STATE->unimplementedFeature("subranges not supported yet"); + | LBRACKET k1=bound DOTDOT k2=bound RBRACKET + { std::stringstream ss; + ss << "subranges not supported yet: [" << k1 << ":" << k2 << ']'; + UNSUPPORTED(ss.str()); + if(k1.hasBound() && k2.hasBound() && + k1.getBound() > k2.getBound()) { + ss.str(""); + ss << "Subrange [" << k1.getBound() << ".." << k2.getBound() + << "] inappropriate: range must be nonempty!"; + PARSER_STATE->parseError(ss.str()); + } + Debug("subranges") << ss.str() << std::endl; t = Type(); } -*/ /* tuple types / old-style function types */ | LBRACKET type[t,check] { types.push_back(t); } @@ -817,7 +1044,7 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, /* record types */ | SQHASH identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] ( COMMA identifier[id,CHECK_NONE,SYM_SORT] COLON type[t,check] )* HASHSQ - { PARSER_STATE->unimplementedFeature("records not supported yet"); + { UNSUPPORTED("records not supported yet"); t = Type(); } /* bitvector types */ @@ -839,26 +1066,19 @@ restrictedTypePossiblyFunctionLHS[CVC4::Type& t, } ; -/** - * Matches a type identifier. Returns the identifier. If the type is - * declared, returns the Type in the 't' parameter; otherwise a null - * Type is returned in 't'. If 'check' is CHECK_DECLARED and the type - * is not declared, an exception is thrown. - * - * @return the type identifier - */ -typeSymbol[CVC4::Type& t, - CVC4::parser::DeclarationCheck check] returns [CVC4::parser::cvc::mystring id] +parameterization[CVC4::parser::DeclarationCheck check] @init { - Debug("parser-extra") << "type symbol: " << AntlrInput::tokenText(LT(1)) << std::endl; + Type t; } - : identifier[id,check,SYM_SORT] - { bool isNew = (check == CHECK_UNDECLARED || check == CHECK_NONE) && - !PARSER_STATE->isDeclared(id, SYM_SORT); - t = isNew ? Type() : PARSER_STATE->getSort(id); - } + : LBRACKET restrictedType[t,check] ( COMMA restrictedType[t,check] )* RBRACKET + { UNSUPPORTED("parameterized types not yet supported"); } ; +bound returns [CVC4::parser::cvc::mySubrangeBound bound] + : UNDERSCORE { $bound = SubrangeBound(); } + | k=integer { $bound = SubrangeBound(k); } +; + typeLetDecl[CVC4::parser::DeclarationCheck check] @init { Type t; @@ -934,14 +1154,14 @@ prefixFormula[CVC4::Expr& f] boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN COLON instantiationPatterns? formula[f] { PARSER_STATE->popScope(); - PARSER_STATE->unimplementedFeature("quantifiers not supported yet"); + UNSUPPORTED("quantifiers not supported yet"); f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); } | EXISTS_TOK { PARSER_STATE->pushScope(); } LPAREN boundVarDecl[ids,t] (COMMA boundVarDecl[ids,t])* RPAREN COLON instantiationPatterns? formula[f] { PARSER_STATE->popScope(); - PARSER_STATE->unimplementedFeature("quantifiers not supported yet"); + UNSUPPORTED("quantifiers not supported yet"); f = EXPR_MANAGER->mkVar(EXPR_MANAGER->booleanType()); } @@ -968,7 +1188,7 @@ prefixFormula[CVC4::Expr& f] | ARRAY_TOK { PARSER_STATE->pushScope(); } LPAREN boundVarDecl[ids,t] RPAREN COLON formula[f] { PARSER_STATE->popScope(); - PARSER_STATE->unimplementedFeature("array literals not supported yet"); + UNSUPPORTED("array literals not supported yet"); f = EXPR_MANAGER->mkVar(EXPR_MANAGER->mkArrayType(t, f.getType())); } ; @@ -1055,16 +1275,40 @@ arithmeticBinop[unsigned& op] | EXP_TOK ; -/** Parses an array store term. */ +/** Parses an array assignment term. */ storeTerm[CVC4::Expr& f] + : uminusTerm[f] + ( WITH_TOK arrayStore[f] ( COMMA arrayStore[f] )* )* + ; + +/** + * Parses just part of the array assignment (and constructs + * the store terms). + */ +arrayStore[CVC4::Expr& f] @init { Expr f2, f3; + std::vector<Expr> dims; } - : uminusTerm[f] ( WITH_TOK - LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] - { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } - ( COMMA LBRACKET formula[f2] RBRACKET ASSIGN_TOK uminusTerm[f3] - { f = MK_EXPR(CVC4::kind::STORE, f, f2, f3); } )* )* + : ( LBRACKET formula[f2] { dims.push_back(f2); } RBRACKET )+ + ASSIGN_TOK uminusTerm[f3] + { Assert(dims.size() >= 1); + // these loops are a bit complicated; they're only used for the + // multidimensional ...WITH [a][b] :=... syntax + for(unsigned i = 0; i < dims.size() - 1; ++i) { + f = MK_EXPR(CVC4::kind::SELECT, f, dims[i]); + } + // a[i][j][k] := v turns into + // store(a, i, store(a[i], j, store(a[i][j], k, v))) + for(unsigned i = dims.size() - 1; i > 0; --i) { + f3 = MK_EXPR(CVC4::kind::STORE, f, dims[i], f3); + // strip off one layer of the select + f = f[0]; + } + + // outermost wrapping + f = MK_EXPR(CVC4::kind::STORE, f, dims[0], f3); + } ; /** Parses a unary minus term. */ @@ -1073,29 +1317,28 @@ uminusTerm[CVC4::Expr& f] unsigned minusCount = 0; } /* Unary minus */ - : (MINUS_TOK { ++minusCount; })+ concatBitwiseTerm[f] + : (MINUS_TOK { ++minusCount; })+ bvBinaryOpTerm[f] { while(minusCount > 0) { --minusCount; f = MK_EXPR(CVC4::kind::UMINUS, f); } } - | concatBitwiseTerm[f] + | bvBinaryOpTerm[f] ; -/** Parses bitvectors. */ - -concatBitwiseTerm[CVC4::Expr& f] +/** Parses bitvectors. Starts with binary operators @, &, and |. */ +bvBinaryOpTerm[CVC4::Expr& f] @init { std::vector<CVC4::Expr> expressions; std::vector<unsigned> operators; unsigned op; } : bvNegTerm[f] { expressions.push_back(f); } - ( concatBitwiseBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )* + ( bvBinop[op] bvNegTerm[f] { operators.push_back(op); expressions.push_back(f); } )* { f = createPrecedenceTree(EXPR_MANAGER, expressions, operators); } ; -concatBitwiseBinop[unsigned& op] +bvBinop[unsigned& op] @init { op = LT(1)->getType(LT(1)); } : CONCAT_TOK - | BAR + | BAR // bitwise OR | BVAND_TOK ; @@ -1103,7 +1346,7 @@ bvNegTerm[CVC4::Expr& f] /* BV neg */ : BVNEG_TOK bvNegTerm[f] { f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); } - | selectExtractShift[f] + | postfixTerm[f] ; /** @@ -1115,11 +1358,12 @@ bvNegTerm[CVC4::Expr& f] * brackets ], so we left-factor as much out as possible to make ANTLR * happy. */ -selectExtractShift[CVC4::Expr& f] +postfixTerm[CVC4::Expr& f] @init { Expr f2; bool extract, left; std::vector<Expr> args; + std::string id; } : bvTerm[f] ( /* array select / bitvector extract */ @@ -1172,7 +1416,21 @@ selectExtractShift[CVC4::Expr& f] Unhandled(t); } } + + /* record / tuple select */ + | DOT + ( identifier[id,CHECK_NONE,SYM_VARIABLE] + { UNSUPPORTED("record select not implemented yet"); + f = Expr(); } + | k=numeral + { UNSUPPORTED("tuple select not implemented yet"); + // This will assert-fail if k too big or f not a tuple + // that's ok for now, once a TUPLE_SELECT operator exists, + // that will do any necessary type checking + f = EXPR_MANAGER->mkVar(TupleType(f.getType()).getTypes()[k]); } + ) )* + typeAscription[f]? ; bvTerm[CVC4::Expr& f] @@ -1315,6 +1573,7 @@ simpleTerm[CVC4::Expr& f] std::string name; std::vector<Expr> args; Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; + Type t; } /* if-then-else */ : iteTerm[f] @@ -1334,8 +1593,11 @@ simpleTerm[CVC4::Expr& f] | TRUE_TOK { f = MK_CONST(true); } | FALSE_TOK { f = MK_CONST(false); } /* arithmetic literals */ - | INTEGER_LITERAL { f = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); } - | DECIMAL_LITERAL { f = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + /* syntactic predicate: never match INTEGER.DIGIT as an integer and a dot! + * This is a rational constant! Otherwise the parser interprets it as a tuple + * selector! */ + | (INTEGER_LITERAL DOT DIGIT)=> r=decimal_literal { f = MK_CONST(r); } + | INTEGER_LITERAL { f = MK_CONST(AntlrInput::tokenToInteger($INTEGER_LITERAL)); } /* bitvector literals */ | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("0hex") == 0 ); @@ -1347,23 +1609,44 @@ simpleTerm[CVC4::Expr& f] f = MK_CONST( BitVector(binString, 2) ); } /* record literals */ | PARENHASH recordEntry (COMMA recordEntry)+ HASHPAREN - { PARSER_STATE->unimplementedFeature("records not implemented yet"); + { UNSUPPORTED("records not implemented yet"); f = Expr(); } /* variable / zero-ary constructor application */ | identifier[name,CHECK_DECLARED,SYM_VARIABLE] - { f = PARSER_STATE->getVariable(name); - // datatypes: zero-ary constructors - Type t = PARSER_STATE->getType(name); - if(t.isConstructor() && ConstructorType(t).getArity() == 0) { - // don't require parentheses, immediately turn it into an - // apply + /* ascriptions will be required for parameterized zero-ary constructors */ + { f = PARSER_STATE->getVariable(name); } + { // datatypes: zero-ary constructors + Type t2 = PARSER_STATE->getType(name); + if(t2.isConstructor() && ConstructorType(t2).getArity() == 0) { + // don't require parentheses, immediately turn it into an apply f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, f); } } ; /** + * Matches (and performs) a type ascription. + * The f arg is the term to check (it is an input-only argument). + */ +typeAscription[const CVC4::Expr& f] +@init { + Type t; +} + : COLON COLON type[t,CHECK_DECLARED] + { if(f.getType() != t) { + std::stringstream ss; + ss << Expr::setlanguage(language::output::LANG_CVC4) + << "type ascription not satisfied\n" + << "term: " << f << '\n' + << "has type: " << f.getType() << '\n' + << "ascribed: " << t; + PARSER_STATE->parseError(ss.str()); + } + } + ; + +/** * Matches an entry in a record literal. */ recordEntry @@ -1409,9 +1692,16 @@ iteElseTerm[CVC4::Expr& f] */ datatypeDef[std::vector<CVC4::Datatype>& datatypes] @init { - std::string id; + std::string id, id2; } + /* This really needs to be CHECK_NONE, or mutually-recursive datatypes + * won't work, because this type will already be "defined" as an + * unresolved type; don't worry, we check below. */ : identifier[id,CHECK_NONE,SYM_SORT] + ( LBRACKET identifier[id2,CHECK_NONE,SYM_SORT] + ( COMMA identifier[id2,CHECK_NONE,SYM_SORT] )* RBRACKET + { UNSUPPORTED("parameterized datatypes not yet supported"); } + )? { datatypes.push_back(Datatype(id)); if(!PARSER_STATE->isUnresolvedType(id)) { // if not unresolved, must be undeclared @@ -1453,7 +1743,7 @@ constructorDef[CVC4::Datatype& type] selector[CVC4::Datatype::Constructor& ctor] @init { std::string id; - Type t; + Type t, t2; } : identifier[id,CHECK_UNDECLARED,SYM_SORT] COLON type[t,CHECK_NONE] { ctor.addArg(id, t); @@ -1465,12 +1755,24 @@ selector[CVC4::Datatype::Constructor& ctor] * Matches an identifier from the input. An identifier is a sequence of letters, * digits and "_", "'", "." symbols, starting with a letter. */ -IDENTIFIER : ALPHA (ALPHA | DIGIT | '_' | '\'' | '.')*; +IDENTIFIER : (ALPHA | '_') (ALPHA | DIGIT | '_' | '\'' | '\\' | '?' | '$' | '~')*; /** * Matches an integer literal. */ -INTEGER_LITERAL: DIGIT+; +INTEGER_LITERAL + : ( '0' + | '1'..'9' DIGIT* + ) + ; + +/** + * Matches a decimal literal. + */ +decimal_literal returns [CVC4::Rational r] + : k=(INTEGER_LITERAL '.' DIGIT+) + { $r = AntlrInput::tokenToRational($k); } + ; /** * Same as an integer literal converted to an unsigned int, but @@ -1484,9 +1786,25 @@ numeral returns [unsigned k] ; /** - * Matches a decimal literal. + * Similar to numeral but for arbitrary-precision, signed integer. */ -DECIMAL_LITERAL: DIGIT+ DOT DIGIT+; +integer returns [CVC4::Integer k] + : INTEGER_LITERAL + { $k = AntlrInput::tokenToInteger($INTEGER_LITERAL); } + | MINUS_TOK INTEGER_LITERAL + { $k = -AntlrInput::tokenToInteger($INTEGER_LITERAL); } + ; + +/** + * Similar to numeral but for strings. + */ +str[std::string& s] + : STRING_LITERAL + { s = AntlrInput::tokenText($STRING_LITERAL); + /* strip off the quotes */ + s = s.substr(1, s.size() - 2); + } + ; /** * Matches a hexadecimal constant. @@ -1514,21 +1832,24 @@ STRING_LITERAL: '"' (ESCAPE | ~('"'|'\\'))* '"'; fragment ALPHA : 'a'..'z' | 'A'..'Z'; /** - * Matches the digits (0-9) + * Matches the decimal digits (0-9) */ fragment DIGIT : '0'..'9'; +/** + * Matches the hexidecimal digits (0-9, a-f, A-F) + */ fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; /** * Matches and skips whitespace in the input and ignores it. */ -WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP();; }; +WHITESPACE : (' ' | '\t' | '\f' | '\r' | '\n')+ { SKIP(); }; /** * Matches the comments and ignores them */ -COMMENT : '%' (~('\n' | '\r'))* { SKIP();; }; +COMMENT : '%' (~('\n' | '\r'))* { SKIP(); }; /** * Matches an allowed escaped character. diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index ea67ef356..f20406c20 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -7,6 +7,11 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-f CC=$(CXX) AM_CFLAGS = $(AM_CXXFLAGS) +ANTLR_OPTS = + +# hide this included makefile from automake +@mk_include@ @srcdir@/../Makefile.antlr_tracing + noinst_LTLIBRARIES = libparsercvc.la ANTLR_TOKEN_STUFF = \ @@ -30,7 +35,9 @@ libparsercvc_la_SOURCES = \ BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated -EXTRA_DIST = @srcdir@/stamp-generated +EXTRA_DIST = \ + @srcdir@/stamp-generated \ + README MAINTAINERCLEANFILES = $(ANTLR_STUFF) maintainer-clean-local: @@ -44,7 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/CvcLexer.h: Cvc.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) - $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Cvc.g" + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -o "@srcdir@/generated" "@srcdir@/Cvc.g" # These don't actually depend on CvcLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/cvc/README b/src/parser/cvc/README new file mode 100644 index 000000000..513a8e85a --- /dev/null +++ b/src/parser/cvc/README @@ -0,0 +1,98 @@ +Notes on CVC4's CVC language parser. + +This language parser attempts to maintain some backward compatibility +with previous versions of the language. However, as the language +evolves, new features need to be supported, and deprecated, +difficult-to-maintain, or grammar-conflicting syntax and features +need to be removed. + +In order to support our users, we have tried to parse what CVC3 could +and (at least) offer an error when a feature is unavailable or +unimplemented. But this is not always possible. Please report a +bug if a particular discrepancy between CVC3 and CVC4 handling of +the CVC language is a concern to you; we may be able to add a +compatibility mode, or at least offer better warnings or errors. + +Below is a list of the known differences between CVC3's and CVC4's +version of the CVC language. This is the list of differences in +language design and parsing ONLY. The featureset of CVC4 is +rapidly expanding, but does not match CVC3's breadth yet. However, +CVC4 should tell you of an unimplemented feature if you try to use +it (rather than giving a cryptic parse or assertion error). + +* CVC4 does not add the current assumptions to the scope after + SAT/INVALID responses like CVC3 did. + +* CVC4 no longer supports the "old" function syntax: + + f : [INT -> INT]; + + This syntax was deprecated in CVC3, and will no longer be + supported. Functions are now written as follows: + + unary : INT -> INT; + binary : (INT, INT) -> INT; + ternary : (INT, INT, INT) -> INT; + +* QUERY and CHECKSAT do not add their argument to the current + list of assertions like CVC3 did. + +* CVC4 allows datatypes to hold complex types that contain self- + or mutual references. For example, + + DATATYPE tree = node(children:ARRAY INT OF tree) | leaf(data:INT) END; + + is permissible in CVC4 but not in CVC3. + +* CVC4 supports parameterized types in datatype definitions, e.g. + + DATATYPE list[T] = cons(car:T) | nil END; + + You can then declare "x : list[INT];" or "x : list[list[INT]];", + for example. + +* CVC4 supports type ascriptions, e.g. + + U : TYPE; + f : INT -> U; + QUERY f(5) : U = f(6); + QUERY f(5) : U = f(6) : U; + QUERY ( f(5) = f(6) ) : BOOLEAN; + QUERY f(5) : U = f(6) : U : BOOLEAN; + + You probably won't need it that much, but it can be handy for + debugging. If a term (or formula) isn't the same type as its + ascription, and it cannot be "up-casted" safely, an error is + immediately generated at parse time. Sometimes this up-cast is + necessary; consider the "nil" constructor of list[T] above. + To use "nil," you must cast it to something: + + DATATYPE Item = Carrots | Butter | Milk | Bread END; + groceries : list[Item] = cons(Butter, cons(Bread, nil:list[INT])); + +* CVC4 supports stronger distinction between type and variable names. + This means that CVC4 may allow you to declare things that CVC3 does + not: + + a : TYPE; + a : INT; % CVC3 complains + a : a; % CVC4 complains, `a' cannot both be INT and `a' + b : a; % No problem, `a' is both the type of `b', and an INT + +* CVC4 supports a command-level LET syntax, e.g.: + + LET double = LAMBDA(x:INT) : 2*x IN + QUERY double(5) = 10; + + It works for types also, and mixes of the two: + + LET x = INT, y = 5, z = x IN + w : x = y; + QUERY y = 5; % error: y undefined + QUERY w = 5; % valid + + The scope of such a LET is exactly one command (until a semicolon). + (It would conflict with POP_SCOPE if it lasted longer.) + +-- Morgan Deters <mdeters@cs.nyu.edu> Wed, 20 Apr 2011 18:32:32 -0400 + diff --git a/src/parser/cvc/cvc_input.cpp b/src/parser/cvc/cvc_input.cpp index 3532b8aa7..541ac0eac 100644 --- a/src/parser/cvc/cvc_input.cpp +++ b/src/parser/cvc/cvc_input.cpp @@ -28,9 +28,9 @@ namespace CVC4 { namespace parser { -/* Use lookahead=2 */ +/* Use lookahead=3 */ CvcInput::CvcInput(AntlrInputStream& inputStream) : - AntlrInput(inputStream,2) { + AntlrInput(inputStream,6) { pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream(); AlwaysAssert( input != NULL ); diff --git a/src/parser/parser.h b/src/parser/parser.h index 033abb42a..6509b192b 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -434,7 +434,7 @@ public: */ inline void unimplementedFeature(const std::string& msg) throw(ParserException) { if(!d_parseOnly) { - parseError(msg); + parseError("Unimplemented feature: " + msg); } } diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index 19665b0f7..236416c1a 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -7,6 +7,11 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-f AM_CFLAGS = $(AM_CXXFLAGS) CC=$(CXX) +ANTLR_OPTS = + +# hide this included makefile from automake +@mk_include@ @srcdir@/../Makefile.antlr_tracing + noinst_LTLIBRARIES = libparsersmt.la ANTLR_TOKEN_STUFF = \ @@ -46,7 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/SmtLexer.h: Smt.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) - $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt.g" + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -o "@srcdir@/generated" "@srcdir@/Smt.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index 86682f9a9..e964c020a 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -19,15 +19,22 @@ grammar Smt; options { - language = 'C'; // C output for antlr -// defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + // C output for antlr + language = 'C'; + + // Skip the default error handling, just break with exceptions + // defaultErrorHandler = false; + + // Only lookahead of <= k requested (disable for LL* parsing) + // Note that CVC4's BoundedTokenBuffer requires a fixed k ! + // If you change this k, change it also in smt_input.cpp ! k = 2; } @header { /** ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -49,11 +56,14 @@ options { * Otherwise, we have to let the lexer detect the encoding at runtime. */ #define ANTLR3_INLINE_INPUT_ASCII + +#include "parser/antlr_tracing.h" } @parser::includes { #include "expr/command.h" #include "parser/parser.h" +#include "parser/antlr_tracing.h" namespace CVC4 { class Expr; diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index 99ff0daba..85b511f40 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -7,6 +7,11 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-f AM_CFLAGS = $(AM_CXXFLAGS) CC=$(CXX) +ANTLR_OPTS = + +# hide this included makefile from automake +@mk_include@ @srcdir@/../Makefile.antlr_tracing + noinst_LTLIBRARIES = libparsersmt2.la ANTLR_TOKEN_STUFF = \ @@ -46,7 +51,7 @@ maintainer-clean-local: # antlr doesn't overwrite output files, it just leaves them. So we have to delete them first. @srcdir@/generated/Smt2Lexer.h: Smt2.g @srcdir@/stamp-generated -$(AM_V_at)rm -f $(ANTLR_STUFF) - $(AM_V_GEN)$(ANTLR) -o "@srcdir@/generated" "@srcdir@/Smt2.g" + $(AM_V_GEN)$(ANTLR) $(ANTLR_OPTS) -o "@srcdir@/generated" "@srcdir@/Smt2.g" # These don't actually depend on SmtLexer.h, but if we're doing parallel # make and the lexer needs to be rebuilt, we have to keep the rules diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4f141891b..9466f8753 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -19,8 +19,15 @@ grammar Smt2; options { - language = 'C'; // C output for antlr - //defaultErrorHandler = false; // Skip the default error handling, just break with exceptions + // C output for antlr + language = 'C'; + + // Skip the default error handling, just break with exceptions + // defaultErrorHandler = false; + + // Only lookahead of <= k requested (disable for LL* parsing) + // Note that CVC4's BoundedTokenBuffer requires a fixed k ! + // If you change this k, change it also in smt2_input.cpp ! k = 2; } @@ -50,6 +57,8 @@ options { * Otherwise, we have to let the lexer detect the encoding at runtime. */ #define ANTLR3_INLINE_INPUT_ASCII + +#include "parser/antlr_tracing.h" } @lexer::postinclude { @@ -57,6 +66,7 @@ options { #include "parser/smt2/smt2.h" #include "parser/antlr_input.h" +#include "parser/antlr_tracing.h" using namespace CVC4; using namespace CVC4::parser; diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index b83fd42dc..77696465c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -289,19 +289,31 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, // collapse NOT-over-EQUAL out << n[0][0] << " /= " << n[0][1]; } else if(n.getNumChildren() == 2) { - // infix operator + // infix binary operator out << '(' << n[0] << ' ' << n.getOperator() << ' ' << n[1] << ')'; + } else if(n.getKind() == kind::AND || + n.getKind() == kind::OR) { + // infix N-ary operator + TNode::iterator i = n.begin(); + out << '(' << *i++; + while(i != n.end()) { + out << ' ' << n.getOperator() << ' ' << *i++; + } + out << ')'; } else if(k == kind::BITVECTOR_NOT) { // precedence on ~ is a little unexpected; add parens out << "(~(" << n[0] << "))"; } else { - // prefix operator - out << n.getOperator() << ' '; - if(n.getNumChildren() > 0) { + // prefix N-ary operator for N != 2 + if(n.getNumChildren() == 0) { + // no parens or spaces + out << n.getOperator(); + } else { + out << '(' << n.getOperator() << ' '; if(n.getNumChildren() > 1) { copy(n.begin(), n.end() - 1, ostream_iterator<TNode>(out, " ")); } - out << n[n.getNumChildren() - 1]; + out << n[n.getNumChildren() - 1] << ')'; } } } diff --git a/src/util/Assert.h b/src/util/Assert.h index ec942e00b..0ff89bedf 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -250,8 +250,8 @@ void debugAssertionFailed(const AssertionException& thisException, if(EXPECT_FALSE( ! (cond) )) { \ /* save the last assertion failure */ \ const char* lastException = s_debugLastException; \ - AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - debugAssertionFailed(exception, lastException); \ + CVC4::AssertionException exception(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + CVC4::debugAssertionFailed(exception, lastException); \ } \ } while(0) @@ -261,27 +261,27 @@ void debugAssertionFailed(const AssertionException& thisException, # define AlwaysAssert(cond, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw CVC4::AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) #endif /* CVC4_DEBUG */ #define Unreachable(msg...) \ - throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ - throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unimplemented(msg...) \ - throw UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::UnimplementedOperationException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define InternalError(msg...) \ - throw InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::InternalErrorException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define IllegalArgument(arg, msg...) \ - throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) + throw CVC4::IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define CheckArgument(cond, arg, msg...) \ AlwaysAssertArgument(cond, arg, ## msg) #define AlwaysAssertArgument(cond, arg, msg...) \ do { \ if(EXPECT_FALSE( ! (cond) )) { \ - throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + throw CVC4::IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ } \ } while(0) diff --git a/src/util/Makefile.am b/src/util/Makefile.am index aaf9ca03b..e76858d80 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -46,9 +46,11 @@ libutil_la_SOURCES = \ dynamic_array.h \ language.h \ triple.h \ + subrange_bound.h \ trans_closure.h \ trans_closure.cpp \ - boolean_simplification.h + boolean_simplification.h \ + boolean_simplification.cpp libutil_la_LIBADD = \ @builddir@/libutilcudd.la diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp new file mode 100644 index 000000000..a154f342f --- /dev/null +++ b/src/util/boolean_simplification.cpp @@ -0,0 +1,45 @@ +/********************* */ +/*! \file boolean_simplification.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Simple routines for Boolean simplification + ** + ** Simple, commonly-used routines for Boolean simplification. + **/ + +#include "util/boolean_simplification.h" + +namespace CVC4 { + +void +BooleanSimplification::push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException) { + Node::iterator i = n.begin(), end = n.end(); + for(; i != end; ++i){ + Node child = *i; + if(child.getKind() == k){ + push_back_associative_commute_recursive(child, buffer, k, notK, negateNode); + }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ + push_back_associative_commute_recursive(child, buffer, notK, k, !negateNode); + }else{ + if(negateNode){ + buffer.push_back(negate(child)); + }else{ + buffer.push_back(child); + } + } + } +}/* BooleanSimplification::push_back_associative_commute_recursive() */ + +}/* CVC4 namespace */ + diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index 95d5fb435..e938a2b38 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -11,10 +11,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief [[ Add one-line brief description here ]] + ** \brief Simple routines for Boolean simplification ** - ** [[ Add lengthier description here ]] - ** \todo document this file + ** Simple, commonly-used routines for Boolean simplification. **/ #include "cvc4_private.h" @@ -22,30 +21,62 @@ #ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H #define __CVC4__BOOLEAN_SIMPLIFICATION_H -#include "expr/node.h" -#include "util/Assert.h" #include <vector> +#include <algorithm> +#include "expr/node.h" +#include "util/Assert.h" namespace CVC4 { +/** + * A class to contain a number of useful functions for simple + * simplification of nodes. One never uses it as an object (and + * it cannot be constructed). It is used as a namespace. + */ class BooleanSimplification { + // cannot construct one of these + BooleanSimplification() CVC4_UNUSED; + BooleanSimplification(const BooleanSimplification&) CVC4_UNUSED; + + static void push_back_associative_commute_recursive + (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode) + throw(AssertionException); + public: + /** + * The threshold for removing duplicates. (See removeDuplicates().) + */ static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10; - static void removeDuplicates(std::vector<Node>& buffer){ - if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){ + /** + * Remove duplicate nodes from a vector, modifying it in-place. + * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this + * function is a no-op. + */ + static void removeDuplicates(std::vector<Node>& buffer) + throw(AssertionException) { + if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) { std::sort(buffer.begin(), buffer.end()); - std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end()); + std::vector<Node>::iterator new_end = + std::unique(buffer.begin(), buffer.end()); buffer.erase(new_end, buffer.end()); } } - static Node simplifyConflict(Node andNode){ - Assert(andNode.getKind() == kind::AND); + /** + * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyConflict(Node andNode) throw(AssertionException) { + AssertArgument(!andNode.isNull(), andNode); + AssertArgument(andNode.getKind() == kind::AND, andNode); + std::vector<Node> buffer; - push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false); + push_back_associative_commute(andNode, buffer, kind::AND, kind::OR); removeDuplicates(buffer); @@ -54,10 +85,18 @@ public: return nb; } - static Node simplifyClause(Node orNode){ - Assert(orNode.getKind() == kind::OR); + /** + * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded + * children of it (as far as possible---see + * push_back_associative_commute()), removes duplicates, and returns + * the resulting Node. + */ + static Node simplifyClause(Node orNode) throw(AssertionException) { + AssertArgument(!orNode.isNull(), orNode); + AssertArgument(orNode.getKind() == kind::OR, orNode); + std::vector<Node> buffer; - push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false); + push_back_associative_commute(orNode, buffer, kind::OR, kind::AND); removeDuplicates(buffer); @@ -66,34 +105,63 @@ public: return nb; } - static Node simplifyHornClause(Node implication){ - Assert(implication.getKind() == kind::IMPLIES); + /** + * Takes a node with kind IMPLIES, converts it to an OR, then + * simplifies the result with simplifyClause(). + * + * The input doesn't actually have to be Horn, it seems, but that's + * the common case(?), hence the name. + */ + static Node simplifyHornClause(Node implication) throw(AssertionException) { + AssertArgument(implication.getKind() == kind::IMPLIES, implication); + TNode left = implication[0]; TNode right = implication[1]; - Node notLeft = NodeBuilder<1>(kind::NOT)<<left; - Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right; + + Node notLeft = negate(left); + Node clause = NodeBuilder<2>(kind::OR) << notLeft << right; + return simplifyClause(clause); } - static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){ - Node::iterator i = n.begin(), end = n.end(); - for(; i != end; ++i){ - Node child = *i; - if(child.getKind() == k){ - push_back_associative_commute(child, buffer, k, notK, negateNode); - }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){ - push_back_associative_commute(child, buffer, notK, k, !negateNode); - }else{ - if(negateNode){ - buffer.push_back(negate(child)); - }else{ - buffer.push_back(child); - } - } - } - } + /** + * Aids in reforming a node. Takes a node of (N-ary) kind k and + * copies its children into an output vector, collapsing its k-kinded + * children into it. Also collapses negations of notK. For example: + * + * push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]], + * buffer, kind::OR, kind::AND ) + * yields a "buffer" vector of [a b b c d e f] + * + * @param n the node to operate upon + * @param buffer the output vector (must be empty on entry) + * @param k the kind to collapse (should equal the kind of node n) + * @param notK the "negation" of kind k (e.g. OR's negation is AND), + * or kind::UNDEFINED_KIND if none. + */ + static inline void + push_back_associative_commute(Node n, std::vector<Node>& buffer, + Kind k, Kind notK) + throw(AssertionException) { + AssertArgument(buffer.empty(), buffer); + AssertArgument(!n.isNull(), n); + AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k); + AssertArgument(notK != kind::NULL_EXPR, notK); + AssertArgument(n.getKind() == k, n, + "expected node to have kind %s", kindToString(k).c_str()); + + push_back_associative_commute_recursive(n, buffer, k, notK, false); + }/* push_back_associative_commute() */ + + /** + * Negates a node, doing all the double-negation elimination + * that's possible. + * + * @param n the node to negate (cannot be the null node) + */ + static Node negate(TNode n) throw(AssertionException) { + AssertArgument(!n.isNull(), n); - static Node negate(TNode n){ bool polarity = true; TNode base = n; while(base.getKind() == kind::NOT){ diff --git a/src/util/output.h b/src/util/output.h index 0b1c86afd..d3eb3a831 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -273,7 +273,7 @@ public: /** The debug output singleton */ extern DebugC DebugChannel CVC4_PUBLIC; #ifdef CVC4_DEBUG -# define Debug DebugChannel +# define Debug CVC4::DebugChannel #else /* CVC4_DEBUG */ # define Debug CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::DebugChannel #endif /* CVC4_DEBUG */ @@ -290,7 +290,7 @@ extern ChatC Chat CVC4_PUBLIC; /** The trace output singleton */ extern TraceC TraceChannel CVC4_PUBLIC; #ifdef CVC4_TRACING -# define Trace TraceChannel +# define Trace CVC4::TraceChannel #else /* CVC4_TRACING */ # define Trace CVC4::__cvc4_true() ? CVC4::debugNullCvc4Stream : CVC4::TraceChannel #endif /* CVC4_TRACING */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h new file mode 100644 index 000000000..fc6a259b4 --- /dev/null +++ b/src/util/subrange_bound.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file subrange_bound.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of subrange bounds + ** + ** Simple class to represent a subrange bound, either infinite + ** (no bound) or finite (an arbitrary precision integer). + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__SUBRANGE_BOUND_H +#define __CVC4__SUBRANGE_BOUND_H + +#include "util/integer.h" +#include "util/Assert.h" + +namespace CVC4 { + +/** + * Representation of a subrange bound. A bound can either exist and be + * a finite arbitrary-precision integer, or not exist (and thus be + * an infinite bound). For example, the CVC language subrange [-5.._] + * has a lower bound of -5 and an infinite upper bound. + */ +class SubrangeBound { + bool d_nobound; + Integer d_bound; + +public: + + /** Construct an infinite SubrangeBound. */ + SubrangeBound() throw() : + d_nobound(true), + d_bound() { + } + + /** Construct a finite SubrangeBound. */ + SubrangeBound(const Integer& i) throw() : + d_nobound(false), + d_bound(i) { + } + + ~SubrangeBound() throw() { + } + + /** Get the finite SubrangeBound, failing an assertion if infinite. */ + Integer getBound() const throw(IllegalArgumentException) { + CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); + return d_bound; + } + + /** Returns true iff this is a finite SubrangeBound. */ + bool hasBound() const throw() { + return !d_nobound; + } + + /** Test two SubrangeBounds for equality. */ + bool operator==(const SubrangeBound& b) const throw() { + return hasBound() == b.hasBound() && + (!hasBound() || getBound() == b.getBound()); + } + + /** Test two SubrangeBounds for disequality. */ + bool operator!=(const SubrangeBound& b) const throw() { + return !(*this == b); + } + +};/* class SubrangeBound */ + +inline std::ostream& +operator<<(std::ostream& out, const SubrangeBound& bound) throw() { + if(bound.hasBound()) { + out << bound.getBound(); + } else { + out << '_'; + } + + return out; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__SUBRANGE_BOUND_H */ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 12e2bb347..323e61ca4 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -38,6 +38,7 @@ SMT2_TESTS = \ # Regression tests for PL inputs CVC_TESTS = \ + subranges.cvc \ boolean-prec.cvc \ hole6.cvc \ ite.cvc \ diff --git a/test/regress/regress0/subranges.cvc b/test/regress/regress0/subranges.cvc new file mode 100644 index 000000000..d8351c7f1 --- /dev/null +++ b/test/regress/regress0/subranges.cvc @@ -0,0 +1,17 @@ +% COMMAND-LINE: --parse-only +% EXPECT: +% EXIT: 0 + +A : [0..0]; +B : [ -5 .. 8]; +C : [1..3]; +D : [1..2]; +E : [-100 ..-1]; +F : [-100 ..0]; +G : [-100 ..1]; +H : [-1 ..1]; +I : [0..10]; +J : [-10..-9]; +J : [-10..-10]; + +QUERY TRUE; diff --git a/test/regress/run_regression b/test/regress/run_regression index a7a6630b9..8f2e385d7 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -114,12 +114,13 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then - expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` + expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then error "cannot determine expected output of \`$benchmark': " \ "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" fi + expected_output=$(echo "$expected_output" | sed 's,^% EXPECT: ,,;s,\r,,') expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,;s,\r,,'` if [ -z "$expected_exit_status" ]; then error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 646ebf9bb..13d28f3bb 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -44,6 +44,8 @@ UNIT_TESTS = \ util/rational_white \ util/stats_black \ util/trans_closure_black \ + util/boolean_simplification_black \ + util/subrange_bound_white \ main/interactive_shell_black export VERBOSE = 1 diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h index 3b1e96084..e37c197ab 100644 --- a/test/unit/expr/expr_manager_public.h +++ b/test/unit/expr/expr_manager_public.h @@ -46,7 +46,7 @@ private: worklist.pop_back(); if( current.getKind() == kind ) { for( unsigned int i = 0; i < current.getNumChildren(); ++i ) { - worklist.push_back( current.getChild(i) ); + worklist.push_back( current[i] ); } } else { childrenFound++; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 632db2b91..53050eece 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -27,6 +27,7 @@ #include "parser/parser_builder.h" #include "parser/smt2/smt2.h" #include "expr/command.h" +#include "util/options.h" #include "util/output.h" #include "util/language.h" @@ -40,6 +41,8 @@ class ParserBlack { ExprManager *d_exprManager; protected: + Options d_options; + /* Set up declaration context for expr inputs */ virtual void setupContext(Parser& parser) { /* a, b, c: BOOLEAN */ @@ -69,6 +72,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(goodInput) + .withOptions(d_options) .withInputLanguage(d_lang) .build(); TS_ASSERT( !parser->done() ); @@ -96,6 +100,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(badInput) + .withOptions(d_options) .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); @@ -118,6 +123,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(goodExpr) + .withOptions(d_options) .withInputLanguage(d_lang) .build(); @@ -155,6 +161,7 @@ protected: Parser *parser = ParserBuilder(d_exprManager,"test") .withStringInput(badExpr) + .withOptions(d_options) .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); @@ -177,6 +184,7 @@ protected: void setUp() { d_exprManager = new ExprManager; + d_options.parseOnly = true; } void tearDown() { @@ -217,6 +225,14 @@ public: tryGoodInput("% a comment\nASSERT TRUE; %a command\n% another comment"); tryGoodInput("a : BOOLEAN; a: BOOLEAN;"); // double decl, but compatible tryGoodInput("a : INT = 5; a: INT;"); // decl after define, compatible + tryGoodInput("a : TYPE; a : INT;"); // ok, sort and variable symbol spaces distinct + tryGoodInput("a : TYPE; a : INT; b : a;"); // ok except a is both INT and sort `a' + tryGoodInput("a : [0..0]; b : [-5..5]; c : [-1..1]; d : [ _ .._];"); // subranges + tryGoodInput("a : [ _..1]; b : [_.. 0]; c :[_..-1];"); + tryGoodInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE cons = null END;"); + tryGoodInput("DATATYPE tree = node(data:list), list = cons(car:tree,cdr:list) END;"); + tryGoodInput("DATATYPE tree = node(data:[list,list,ARRAY tree OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); + tryGoodInput("DATATYPE trex = Foo | Bar END; DATATYPE tree = node(data:[list,list,ARRAY trex OF list]), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); } void testBadCvc4Inputs() { @@ -232,6 +248,14 @@ public: tryBadInput("A : TYPE; A: TYPE;"); // types can't be double-declared tryBadInput("a : INT; a: INT = 5;"); // can't define after decl tryBadInput("a : INT = 5; a: BOOLEAN;"); // decl w/ incompatible type + tryBadInput("a : TYPE; a : INT; a : a;"); // ok except a is both INT and sort `a' + tryBadInput("a : [1..-1];"); // bad subrange + tryBadInput("a : [0. .0];"); // bad subrange + tryBadInput("a : [..0];"); // bad subrange + tryBadInput("a : [0.0];"); // bad subrange + tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list = nil | cons(car:INT,cdr:list) END;"); + tryBadInput("DATATYPE list = nil | cons(car:INT,cdr:list) END; DATATYPE list2 = nil END;"); + tryBadInput("DATATYPE tree = node(data:(list,list,ARRAY trex OF list)), list = cons(car:ARRAY list OF tree,cdr:BITVECTOR(32)) END;"); } void testGoodCvc4Exprs() { diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h new file mode 100644 index 000000000..8dafd202e --- /dev/null +++ b/test/unit/util/boolean_simplification_black.h @@ -0,0 +1,224 @@ +/********************* */ +/*! \file boolean_simplification_black.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Black box testing of CVC4::BooleanSimplification + ** + ** Black box testing of CVC4::BooleanSimplification. + **/ + +#include "context/context.h" +#include "util/language.h" +#include "expr/node.h" +#include "expr/kind.h" +#include "expr/node_manager.h" +#include "util/boolean_simplification.h" + +#include <algorithm> +#include <vector> +#include <set> + +using namespace CVC4; +using namespace CVC4::context; +using namespace std; + +class BooleanSimplificationBlack : public CxxTest::TestSuite { + + Context* d_context; + NodeManager* d_nm; + NodeManagerScope* d_scope; + + Node a, b, c, d, e, f, g, h; + Node fa, fb, fc, ga, ha, hc, ffb, fhc, hfc, gfb; + Node ac, ffbd, efhc, dfa; + + // assert equality up to commuting children + void ASSERT_NODES_EQUAL(TNode n1, TNode n2) { + cout << "ASSERTING: " << n1 << endl + << " ~= " << n2 << endl; + TS_ASSERT_EQUALS( n1.getKind(), n2.getKind() ); + TS_ASSERT_EQUALS( n1.getNumChildren(), n2.getNumChildren() ); + vector<TNode> v1(n1.begin(), n1.end()); + vector<TNode> v2(n2.begin(), n2.end()); + sort(v1.begin(), v1.end()); + sort(v2.begin(), v2.end()); + TS_ASSERT_EQUALS( v1, v2 ); + } + + // assert that node's children have same elements as the set + // (so no duplicates); also n is asserted to have kind k + void ASSERT_NODE_EQUALS_SET(TNode n, Kind k, set<TNode> elts) { + vector<TNode> v(n.begin(), n.end()); + + // BooleanSimplification implementation sorts its output nodes, BUT + // that's an implementation detail, not part of the contract, so we + // should be robust to it here; this is a black-box test! + sort(v.begin(), v.end()); + + TS_ASSERT_EQUALS( n.getKind(), k ); + TS_ASSERT_EQUALS( elts.size(), n.getNumChildren() ); + TS_ASSERT( equal(n.begin(), n.end(), elts.begin()) ); + } + +public: + + void setUp() { + d_context = new Context(); + d_nm = new NodeManager(d_context, NULL); + d_scope = new NodeManagerScope(d_nm); + + a = d_nm->mkVar("a", d_nm->booleanType()); + b = d_nm->mkVar("b", d_nm->booleanType()); + c = d_nm->mkVar("c", d_nm->booleanType()); + d = d_nm->mkVar("d", d_nm->booleanType()); + e = d_nm->mkVar("e", d_nm->booleanType()); + f = d_nm->mkVar("f", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); + g = d_nm->mkVar("g", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); + h = d_nm->mkVar("h", d_nm->mkFunctionType(d_nm->booleanType(), + d_nm->booleanType())); + fa = d_nm->mkNode(kind::APPLY_UF, f, a); + fb = d_nm->mkNode(kind::APPLY_UF, f, b); + fc = d_nm->mkNode(kind::APPLY_UF, f, c); + ga = d_nm->mkNode(kind::APPLY_UF, g, a); + ha = d_nm->mkNode(kind::APPLY_UF, h, a); + hc = d_nm->mkNode(kind::APPLY_UF, h, c); + ffb = d_nm->mkNode(kind::APPLY_UF, f, fb); + fhc = d_nm->mkNode(kind::APPLY_UF, f, hc); + hfc = d_nm->mkNode(kind::APPLY_UF, h, fc); + gfb = d_nm->mkNode(kind::APPLY_UF, g, fb); + + ac = d_nm->mkNode(kind::IFF, a, c); + ffbd = d_nm->mkNode(kind::IFF, ffb, d); + efhc = d_nm->mkNode(kind::IFF, e, fhc); + dfa = d_nm->mkNode(kind::IFF, d, fa); + + // this test is designed for >= 10 removal threshold + TS_ASSERT_LESS_THAN_EQUALS(10u, + BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD); + + cout << Expr::setdepth(-1) + << Expr::setlanguage(language::output::LANG_CVC4); + } + + void tearDown() { + a = b = c = d = e = f = g = h = Node(); + fa = fb = fc = ga = ha = hc = ffb = fhc = hfc = gfb = Node(); + ac = ffbd = efhc = dfa = Node(); + + delete d_scope; + delete d_nm; + delete d_context; + } + + void testNegate() { + Node in, out; + + in = d_nm->mkNode(kind::NOT, a); + out = a; + ASSERT_NODES_EQUAL( out, BooleanSimplification::negate(in) ); + ASSERT_NODES_EQUAL( in, BooleanSimplification::negate(out) ); + + in = fa.andNode(ac).notNode().notNode().notNode().notNode(); + out = fa.andNode(ac).notNode(); + ASSERT_NODES_EQUAL( out, BooleanSimplification::negate(in) ); + +#ifdef CVC4_ASSERTIONS + in = Node(); + TS_ASSERT_THROWS( BooleanSimplification::negate(in), IllegalArgumentException ); +#endif /* CVC4_ASSERTIONS */ + } + + void testRemoveDuplicates() { + } + + void testPushBackAssociativeCommute() { + } + + void testSimplifyClause() { + Node in, out; + + in = a.orNode(b); + out = in; + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in)); + + in = d_nm->mkNode(kind::OR, a, d.andNode(b)); + out = in; + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in)); + + in = d_nm->mkNode(kind::OR, a, d.orNode(b)); + out = d_nm->mkNode(kind::OR, a, d, b); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in)); + + in = d_nm->mkNode(kind::OR, fa, ga.orNode(c).notNode(), hfc, ac, d.andNode(b)); + out = NodeBuilder<>(kind::OR) << fa << ga.orNode(c).notNode() << hfc << ac << d.andNode(b); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in)); + + in = d_nm->mkNode(kind::OR, fa, ga.andNode(c).notNode(), hfc, ac, d.andNode(b)); + out = NodeBuilder<>(kind::OR) << fa << ga.notNode() << c.notNode() << hfc << ac << d.andNode(b); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyClause(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nm->mkNode(kind::AND, a, b); + TS_ASSERT_THROWS( BooleanSimplification::simplifyClause(in), IllegalArgumentException ); +#endif /* CVC4_ASSERTIONS */ + } + + void testSimplifyHorn() { + Node in, out; + + in = a.impNode(b); + out = a.notNode().orNode(b); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in)); + + in = a.notNode().impNode(ac.andNode(b)); + out = d_nm->mkNode(kind::OR, a, ac.andNode(b)); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in)); + + in = a.andNode(b).impNode(d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b))); + out = d_nm->mkNode(kind::OR, a.notNode(), b.notNode(), d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b))); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in)); + + in = a.andNode(b).impNode(d_nm->mkNode(kind::OR, fa, ga.orNode(c).notNode(), hfc.orNode(ac), d.andNode(b).notNode())); + out = NodeBuilder<>(kind::OR) << a.notNode() << b.notNode() << fa << ga.orNode(c).notNode() << hfc << ac << d.notNode(); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyHornClause(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nm->mkNode(kind::OR, a, b); + TS_ASSERT_THROWS( BooleanSimplification::simplifyHornClause(in), IllegalArgumentException ); +#endif /* CVC4_ASSERTIONS */ + } + + void testSimplifyConflict() { + Node in, out; + + in = a.andNode(b); + out = in; + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in)); + + in = d_nm->mkNode(kind::AND, a, d.andNode(b)); + out = d_nm->mkNode(kind::AND, a, d, b); + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in)); + + in = d_nm->mkNode(kind::AND, fa, ga.orNode(c).notNode(), fa, hfc.orNode(ac), d.andNode(b)); + out = NodeBuilder<>(kind::AND) << fa << ga.notNode() << c.notNode() << hfc.orNode(ac) << d << b; + ASSERT_NODES_EQUAL(out, BooleanSimplification::simplifyConflict(in)); + +#ifdef CVC4_ASSERTIONS + in = d_nm->mkNode(kind::OR, a, b); + TS_ASSERT_THROWS( BooleanSimplification::simplifyConflict(in), IllegalArgumentException ); +#endif /* CVC4_ASSERTIONS */ + } + +};/* class BooleanSimplificationBlack */ + diff --git a/test/unit/util/subrange_bound_white.h b/test/unit/util/subrange_bound_white.h new file mode 100644 index 000000000..a41f75af9 --- /dev/null +++ b/test/unit/util/subrange_bound_white.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \file subrange_bound_white.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief White box testing of CVC4::SubrangeBound + ** + ** White box testing of CVC4::SubrangeBound. + **/ + +#include "util/subrange_bound.h" +#include "util/integer.h" + +#include <string> +#include <sstream> + +using namespace CVC4; +using namespace std; + +class SubrangeBoundWhite : public CxxTest::TestSuite { + stringstream ss; + +public: + + void testInfinite() { + SubrangeBound b; + TS_ASSERT( ! b.hasBound() ); + TS_ASSERT_THROWS( b.getBound(), IllegalArgumentException ); + ss.str(""); ss << b; + TS_ASSERT_EQUALS( ss.str(), "_" ); + } + + void testZero() { + SubrangeBound b1(0), b2(string("0")), b3(Integer("1")); + TS_ASSERT( b1.hasBound() && b2.hasBound() && b3.hasBound() ); + TS_ASSERT( b1.getBound() == 0 && b2.getBound() == 0 && b3.getBound() == 1 ); + TS_ASSERT( b1 == b2 ); TS_ASSERT( b2 == b1 ); + TS_ASSERT( !(b1 == b3) ); TS_ASSERT( !(b3 == b1) ); + TS_ASSERT( !(b2 == b3) ); TS_ASSERT( !(b3 == b2) ); + TS_ASSERT( !(b1 != b2) ); TS_ASSERT( !(b2 != b1) ); + TS_ASSERT( b1 != b3 ); TS_ASSERT( b3 != b1 ); + TS_ASSERT( b2 != b3 ); TS_ASSERT( b3 != b2 ); + ss.str(""); ss << b1; + TS_ASSERT( ss.str() == "0" ); + ss.str(""); ss << b2; + TS_ASSERT( ss.str() == "0" ); + ss.str(""); ss << b3; + TS_ASSERT( ss.str() == "1" ); + } + + void testOne() { + SubrangeBound b(string("1")); + TS_ASSERT( b.hasBound() ); + TS_ASSERT( b.getBound() == 1 ); + ss.str(""); ss << b; + TS_ASSERT( ss.str() == "1" ); + } + + void testMinusOne() { + } + + void testLarge() { + } + + void testSmall() { + } + +};/* class SubrangeBoundWhite */ + |