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]}
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 {
* @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.
parser.cpp \
parser_builder.h \
parser_builder.cpp \
- parser_exception.h
+ parser_exception.h \
+ antlr_tracing.h
libcvc4parser_noinst_la_SOURCES = \
antlr_input.h \
parser.cpp \
parser_builder.h \
parser_builder.cpp \
- parser_exception.h
+ parser_exception.h \
+ antlr_tracing.h
+EXTRA_DIST = \
+ Makefile.antlr_tracing
--- /dev/null
+# -*-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
+
--- /dev/null
+/********************* */
+/*! \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 */
** 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
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
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)
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)
** 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;
// 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';
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';
RBRACKET = ']';
SEMICOLON = ';';
BAR = '|';
- DOT = '.';
- DOTDOT = '..';
UNDERSCORE = '_';
SQHASH = '[#';
PARENHASH = '(#';
HASHPAREN = '#)';
+ DOT = '.';
+ DOTDOT = '..';
+
// Operators
ARROW_TOK = '->';
BVSGT_TOK = 'BVSGT';
BVSLE_TOK = 'BVSLE';
BVSGE_TOK = 'BVSGE';
-}
+}/* tokens */
@parser::members {
case IMPLIES_TOK: return true;
default: return false;
}
-}
+}/* isRightToLeft() */
int getOperatorPrecedence(int type) {
switch(type) {
default:
Unhandled(CvcParserTokenNames[type]);
}
-}
+}/* getOperatorPrecedence() */
Kind getOperatorKind(int type, bool& negate) {
negate = false;
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;
default:
Unhandled(CvcParserTokenNames[type]);
}
-}
+}/* getOperatorKind() */
unsigned findPivot(const std::vector<unsigned>& operators,
unsigned startIndex, unsigned stopIndex) {
}
}
return pivot;
-}
+}/* findPivot() */
Expr createPrecedenceTree(ExprManager* em,
const std::vector<CVC4::Expr>& expressions,
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,
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) {
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. */
* 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;
* 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;
#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.
* @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.
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
}
: 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()); } )
;
/**
( COMMA identifier[id,check,type] { idList.push_back(id); } )*
;
-
/**
* Matches an identifier and returns a string.
*/
}
/* named types */
: identifier[id,check,SYM_SORT]
+ parameterization[check]?
{ if(check == CHECK_DECLARED ||
PARSER_STATE->isDeclared(id, SYM_SORT)) {
t = PARSER_STATE->getSort(id);
/* 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); }
/* 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 */
}
;
-/**
- * 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;
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());
}
| 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()));
}
;
| 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. */
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
;
/* BV neg */
: BVNEG_TOK bvNegTerm[f]
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
- | selectExtractShift[f]
+ | postfixTerm[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 */
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]
std::string name;
std::vector<Expr> args;
Debug("parser-extra") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
+ Type t;
}
/* if-then-else */
: iteTerm[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 );
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.
*/
*/
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
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);
* 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
;
/**
- * 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.
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.
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 = \
BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
-EXTRA_DIST = @srcdir@/stamp-generated
+EXTRA_DIST = \
+ @srcdir@/stamp-generated \
+ README
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
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
--- /dev/null
+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
+
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 );
*/
inline void unimplementedFeature(const std::string& msg) throw(ParserException) {
if(!d_parseOnly) {
- parseError(msg);
+ parseError("Unimplemented feature: " + msg);
}
}
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 = \
# 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
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
* 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;
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 = \
# 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
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;
}
* Otherwise, we have to let the lexer detect the encoding at runtime.
*/
#define ANTLR3_INLINE_INPUT_ASCII
+
+#include "parser/antlr_tracing.h"
}
@lexer::postinclude {
#include "parser/smt2/smt2.h"
#include "parser/antlr_input.h"
+#include "parser/antlr_tracing.h"
using namespace CVC4;
using namespace CVC4::parser;
// 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] << ')';
}
}
}
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)
# 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)
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
--- /dev/null
+/********************* */
+/*! \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 */
+
** 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"
#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);
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);
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){
/** 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 */
/** 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 */
--- /dev/null
+/********************* */
+/*! \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 */
# Regression tests for PL inputs
CVC_TESTS = \
+ subranges.cvc \
boolean-prec.cvc \
hole6.cvc \
ite.cvc \
--- /dev/null
+% 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;
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"
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
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++;
#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"
ExprManager *d_exprManager;
protected:
+ Options d_options;
+
/* Set up declaration context for expr inputs */
virtual void setupContext(Parser& parser) {
/* a, b, c: BOOLEAN */
Parser *parser =
ParserBuilder(d_exprManager,"test")
.withStringInput(goodInput)
+ .withOptions(d_options)
.withInputLanguage(d_lang)
.build();
TS_ASSERT( !parser->done() );
Parser *parser =
ParserBuilder(d_exprManager,"test")
.withStringInput(badInput)
+ .withOptions(d_options)
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
Parser *parser =
ParserBuilder(d_exprManager,"test")
.withStringInput(goodExpr)
+ .withOptions(d_options)
.withInputLanguage(d_lang)
.build();
Parser *parser =
ParserBuilder(d_exprManager,"test")
.withStringInput(badExpr)
+ .withOptions(d_options)
.withInputLanguage(d_lang)
.withStrictMode(strictMode)
.build();
void setUp() {
d_exprManager = new ExprManager;
+ d_options.parseOnly = true;
}
void tearDown() {
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() {
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() {
--- /dev/null
+/********************* */
+/*! \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 */
+
--- /dev/null
+/********************* */
+/*! \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 */
+
projects / cvc5.git / commitdiff