#include "expr/expr.h"
#include "expr/type.h"
#include "util/result.h"
+#include "util/sexpr.h"
namespace CVC4 {
std::string d_logic;
};/* class SetBenchmarkLogicCommand */
+class CVC4_PUBLIC SetInfoCommand : public Command {
+public:
+ SetInfoCommand(std::string flag, SExpr& sexpr);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ std::string d_flag;
+ SExpr d_sexpr;
+};/* class SetInfoCommand */
+
class CVC4_PUBLIC CommandSequence : public Command {
public:
CommandSequence();
out << "SetBenchmarkLogic(" << d_logic << ")";
}
+inline SetInfoCommand::SetInfoCommand(std::string flag, SExpr& sexpr) :
+ d_flag(flag),
+ d_sexpr(sexpr) {
+}
+
+inline void SetInfoCommand::invoke(SmtEngine* smt) { }
+
+inline void SetInfoCommand::toStream(std::ostream& out) const {
+ out << "SetInfo(" << d_flag << ", " << d_sexpr << ")";
+}
+
/* output stream insertion operator for benchmark statuses */
inline std::ostream& operator<<(std::ostream& out,
BenchmarkStatus status) {
AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
InputStream(name),
d_input(input) {
+ AlwaysAssert( input != NULL );
}
AntlrInputStream::~AntlrInputStream() {
return d_input;
}
-AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) {
+AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap)
+ throw (InputStreamException) {
+ pANTLR3_INPUT_STREAM input = NULL;
if( useMmap ) {
- return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) );
+ input = MemoryMappedInputBufferNew(name);
} else {
- return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) );
+ input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str());
}
-/*
- if( d_inputStream == NULL ) {
- throw ParserException("Couldn't open file: " + filename);
- }
-*/
+ if( input == NULL ) {
+ throw InputStreamException("Couldn't open file: " + name);
+ }
+ return new AntlrInputStream( name, input );
}
-AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{
+AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name)
+ throw (InputStreamException) {
char* inputStr = strdup(input.c_str());
char* nameStr = strdup(name.c_str());
-/*
- if( inputStr==NULL || nameStr==NULL ) {
+ AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
+ pANTLR3_INPUT_STREAM inputStream =
+ antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr,
+ input.size(),
+ (pANTLR3_UINT8) nameStr);
+ if( inputStream==NULL ) {
throw InputStreamException("Couldn't initialize string input: '" + input + "'");
}
-*/
- return new AntlrInputStream( name,
- antlr3NewAsciiStringInPlaceStream(
- (pANTLR3_UINT8)inputStr,input.size(),
- (pANTLR3_UINT8)nameStr) );
+ return new AntlrInputStream( name, inputStream );
}
-AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
+AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) {
AntlrInput* input;
switch(lang) {
return input;
}
-AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) :
+AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) :
Input(inputStream),
d_lookahead(lookahead),
d_lexer(NULL),
d_parser(NULL),
- d_antlr3InputStream( inputStream->getAntlr3InputStream() ),
+ d_antlr3InputStream( inputStream.getAntlr3InputStream() ),
d_tokenStream(NULL) {
}
* @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
* input will use the standard ANTLR3 I/O implementation.
*/
- static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false);
+ static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false)
+ throw (InputStreamException);
/** Create an input from an istream. */
// AntlrInputStream newInputStream(std::istream& input, const std::string& name);
* @param input the string to read
* @param name the "filename" to use when reporting errors
*/
- static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name);
+ static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name)
+ throw (InputStreamException);
};
class Parser;
* @param inputStream the input stream
*
* */
- static AntlrInput* newInput(InputLanguage lang, AntlrInputStream *inputStream);
+ static AntlrInput* newInput(InputLanguage lang, AntlrInputStream& inputStream);
/** Retrieve the text associated with a token. */
static std::string tokenText(pANTLR3_COMMON_TOKEN token);
* @param lookahead the lookahead needed to parse the input (i.e., k for
* an LL(k) grammar)
*/
- AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead);
+ AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead);
/** Retrieve the token stream for this parser. Must not be called before
* <code>setLexer()</code>. */
} else {
if(ex->expecting == ANTLR3_TOKEN_EOF) {
ss << "Missing end of file marker.";
+ } else if( ex->expecting == 0 ) {
+ ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
} else {
ss << "Missing " << tokenNames[ex->expecting] << ".";
}
} else {
if(ex->expecting == ANTLR3_TOKEN_EOF) {
ss << "Expected end of file.";
+ } else if( ex->expecting == 0 ) {
+ ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
} else {
ss << "Expected " << tokenNames[ex->expecting] << ".";
}
namespace parser {
/* Use lookahead=2 */
-CvcInput::CvcInput(AntlrInputStream *inputStream) :
+CvcInput::CvcInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream,2) {
- pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+ pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
AlwaysAssert( input != NULL );
d_pCvcLexer = CvcLexerNew(input);
*
* @param inputStream the input to parse
*/
- CvcInput(AntlrInputStream *inputStream);
+ CvcInput(AntlrInputStream& inputStream);
/** Create a string input.
*
namespace CVC4 {
namespace parser {
+InputStreamException::InputStreamException(const std::string& msg) :
+ Exception(msg) {
+}
+
const std::string InputStream::getName() const {
return d_name;
}
-Input::Input(InputStream *inputStream) :
- d_inputStream( inputStream ) {
+Input::Input(InputStream& inputStream) :
+ d_inputStream( &inputStream ) {
}
Input::~Input() {
}
Input* Input::newFileInput(InputLanguage lang,
- const std::string& filename, bool useMmap) {
+ const std::string& filename,
+ bool useMmap)
+ throw (InputStreamException) {
AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap);
- return AntlrInput::newInput(lang,inputStream);
+ return AntlrInput::newInput(lang,*inputStream);
}
Input* Input::newStringInput(InputLanguage lang,
- const std::string& str, const std::string& name) {
+ const std::string& str,
+ const std::string& name)
+ throw (InputStreamException) {
AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name);
- return AntlrInput::newInput(lang,inputStream);
+ return AntlrInput::newInput(lang,*inputStream);
}
}/* CVC4::parser namespace */
namespace parser {
+class CVC4_PUBLIC InputStreamException : public Exception {
+
+public:
+ InputStreamException(const std::string& msg);
+ virtual ~InputStreamException() throw() { }
+};
+
/** Wrapper around an ANTLR3 input stream. */
class InputStream {
* @param filename the input filename
* @param useMmap true if the parser should use memory-mapped I/O (default: false)
*/
- static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false);
+ static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false)
+ throw (InputStreamException);
/** Create an input for the given stream.
*
* @param input the input string
* @param name the name of the stream, for use in error messages
*/
- static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name);
+ static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name)
+ throw (InputStreamException);
protected:
*
* @param inputStream the input stream
*/
- Input(InputStream* inputStream);
+ Input(InputStream& inputStream);
/** Retrieve the input stream for this parser. */
InputStream *getInputStream();
namespace parser {
/* Use lookahead=2 */
-SmtInput::SmtInput(AntlrInputStream *inputStream) :
+SmtInput::SmtInput(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
- pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+ pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
AlwaysAssert( input != NULL );
d_pSmtLexer = SmtLexerNew(input);
*
* @param inputStream the input stream to use
*/
- SmtInput(AntlrInputStream *inputStream);
+ SmtInput(AntlrInputStream& inputStream);
/**
* Create a string input.
}
}
+static void
+setInfo(Parser *parser, const std::string& flag, const SExpr& sexpr) {
+ // TODO: ???
}
+}
/**
* Parses an expression.
Expr expr;
Type t;
std::vector<Type> sorts;
+ SExpr sexpr;
}
: /* set the logic */
SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_VARIABLE]
{ Debug("parser") << "set logic: '" << name << "' " << std::endl;
setLogic(PARSER_STATE,name);
- $cmd = new SetBenchmarkLogicCommand(name); }
- | SET_INFO_TOK c=setInfo
- { cmd = c; }
+ $cmd = new SetBenchmarkLogicCommand(name); }
+ | SET_INFO_TOK KEYWORD symbolicExpr[sexpr]
+ { name = AntlrInput::tokenText($KEYWORD);
+ setInfo(PARSER_STATE,name,sexpr);
+ cmd = new SetInfoCommand(name,sexpr); }
| /* sort declaration */
- DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL_TOK
+ DECLARE_SORT_TOK symbol[name,CHECK_UNDECLARED,SYM_SORT] n=NUMERAL
{ Debug("parser") << "declare sort: '" << name << "' arity=" << n << std::endl;
if( AntlrInput::tokenToInteger(n) > 0 ) {
Unimplemented("Parameterized user sorts.");
| /* checksat */
CHECKSAT_TOK
{ cmd = new CheckSatCommand(MK_CONST(true)); }
+ | EXIT_TOK
+ { // TODO: Explicitly represent exit as command?
+ cmd = 0; }
;
-setInfo returns [CVC4::Command* cmd]
-@declarations {
- BenchmarkStatus status;
+symbolicExpr[CVC4::SExpr& sexpr]
+@declarations {
+ std::vector<SExpr> children;
}
- : CATEGORY_TOK sym=SYMBOL {
- // FIXME?
- cmd = new EmptyCommand(":category");
- }
- | DIFFICULTY_TOK RATIONAL_TOK {
- // FIXME?
- cmd = new EmptyCommand(":difficulty");
- }
- | NOTES_TOK sym=SYMBOL {
- // FIXME?
- cmd = new EmptyCommand(":notes");
- }
- | SMT_VERSION_TOK RATIONAL_TOK {
- // FIXME?
- cmd = new EmptyCommand(":smt-lib-version");
- }
- | SOURCE_TOK sym=SYMBOL {
- // FIXME?
- cmd = new EmptyCommand(":source");
- }
- | STATUS_TOK benchmarkStatus[status]
- { cmd = new SetBenchmarkStatusCommand(status); }
-;
-
+ : NUMERAL
+ { sexpr = SExpr(AntlrInput::tokenText($NUMERAL)); }
+ | RATIONAL
+ { sexpr = SExpr(AntlrInput::tokenText($RATIONAL)); }
+ | STRING_LITERAL
+ { sexpr = SExpr(AntlrInput::tokenText($STRING_LITERAL)); }
+ | SYMBOL
+ { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
+ | KEYWORD
+ { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+ | LPAREN_TOK
+ (symbolicExpr[sexpr] { children.push_back(sexpr); } )*
+ RPAREN_TOK
+ { sexpr = SExpr(children); }
+ ;
+
/**
* Matches a term.
* @return the expression representing the formula
/* constants */
| TRUE_TOK { expr = MK_CONST(true); }
| FALSE_TOK { expr = MK_CONST(false); }
- | NUMERAL_TOK
- { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL_TOK) ); }
- | RATIONAL_TOK
+ | NUMERAL
+ { expr = MK_CONST( AntlrInput::tokenToInteger($NUMERAL) ); }
+ | RATIONAL
{ // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
- expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
+ expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL) ); }
// NOTE: Theory constants go here
;
// Base SMT-LIB tokens
ASSERT_TOK : 'assert';
BOOL_TOK : 'Bool';
-CATEGORY_TOK : ':category';
+//CATEGORY_TOK : ':category';
CHECKSAT_TOK : 'check-sat';
-DIFFICULTY_TOK : ':difficulty';
+//DIFFICULTY_TOK : ':difficulty';
DECLARE_FUN_TOK : 'declare-fun';
DECLARE_SORT_TOK : 'declare-sort';
+EXIT_TOK : 'exit';
FALSE_TOK : 'false';
ITE_TOK : 'ite';
LET_TOK : 'let';
LPAREN_TOK : '(';
-NOTES_TOK : ':notes';
+//NOTES_TOK : ':notes';
RPAREN_TOK : ')';
-SAT_TOK : 'sat';
+//SAT_TOK : 'sat';
SET_LOGIC_TOK : 'set-logic';
SET_INFO_TOK : 'set-info';
-SMT_VERSION_TOK : ':smt-lib-version';
-SOURCE_TOK : ':source';
-STATUS_TOK : ':status';
+//SMT_VERSION_TOK : ':smt-lib-version';
+//SOURCE_TOK : ':source';
+//STATUS_TOK : ':status';
TRUE_TOK : 'true';
-UNKNOWN_TOK : 'unknown';
-UNSAT_TOK : 'unsat';
+//UNKNOWN_TOK : 'unknown';
+//UNSAT_TOK : 'unsat';
// operators (NOTE: theory symbols go here)
AMPERSAND_TOK : '&';
XOR_TOK : 'xor';
/**
- * Matches a symbol from the input. A symbol a non-empty sequence of
- * letters, digits and the characters + - / * = % ? ! . $ ~ & ^ < > @ that
- * does not start with a digit or a sequence of printable ASCII characters
- * that starts and ends with | and does not otherwise contain |.
+ * Matches a symbol from the input. A symbol is a "simple" symbole or a
+ * sequence of printable ASCII characters that starts and ends with | and
+ * does not otherwise contain |.
*/
SYMBOL
+ : SIMPLE_SYMBOL
+ | '|' ~('|')+ '|'
+ ;
+
+/**
+ * Matches a keyword from the input. A keyword is a symbol symbol, prefixed
+ * with a colon.
+ */
+KEYWORD
+ : ':' SIMPLE_SYMBOL
+ ;
+
+/** Matches a "simple" symbol: a non-empty sequence of letters, digits and
+ * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
+ * digit.
+ */
+fragment SIMPLE_SYMBOL
: (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)*
- | '|' ~('|') '|'
;
/**
/**
* Matches a numeral from the input (non-empty sequence of digits).
*/
-NUMERAL_TOK
+NUMERAL
: DIGIT+
;
-RATIONAL_TOK
+RATIONAL
: DIGIT+ '.' DIGIT+
;
* Matches the digits (0-9)
*/
fragment DIGIT : '0'..'9';
-// fragment NON_ZERO_DIGIT : '1'..'9';
-// fragment NUMERAL_SEQ : '0' | NON_ZERO_DIGIT DIGIT*;
+/** Matches the characters that may appear in a "symbol" (i.e., an identifier)
+ */
fragment SYMBOL_CHAR
- : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~' | '&'
- | '^' | '<' | '>' | '@'
+ : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~'
+ | '&' | '^' | '<' | '>' | '@'
;
/**
namespace parser {
/* Use lookahead=2 */
-Smt2Input::Smt2Input(AntlrInputStream *inputStream) :
+Smt2Input::Smt2Input(AntlrInputStream& inputStream) :
AntlrInput(inputStream, 2) {
- pANTLR3_INPUT_STREAM input = inputStream->getAntlr3InputStream();
+ pANTLR3_INPUT_STREAM input = inputStream.getAntlr3InputStream();
AlwaysAssert( input != NULL );
d_pSmt2Lexer = Smt2LexerNew(input);
/** The ANTLR3 CVC parser for the input. */
pSmt2Parser d_pSmt2Parser;
+ /**
+ * Initialize the class. Called from the constructors once the input
+ * stream is initialized.
+ */
+ void init();
+
public:
/**
*
* @param inputStream the input stream to use
*/
- Smt2Input(AntlrInputStream *inputStream);
+ Smt2Input(AntlrInputStream& inputStream);
/**
* Create a string input.
// Smt2Input(ExprManager* exprManager, const std::string& input, const std::string& name);
/** Destructor. Frees the lexer and the parser. */
- ~Smt2Input();
+ virtual ~Smt2Input();
protected:
*/
Expr parseExpr() throw(ParserException);
-private:
-
- /**
- * Initialize the class. Called from the constructors once the input
- * stream is initialized.
- */
- void init();
-
};/* class Smt2Input */
}/* CVC4::parser namespace */
integer.cpp \
bitvector.h \
bitvector.cpp \
- gmp_util.h
+ gmp_util.h \
+ sexpr.h
--- /dev/null
+/********************* */
+/** sexpr.cpp
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Simple representation of SMT S-expressions.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SEXPR_H_
+#define __CVC4__SEXPR_H_
+
+#include "util/Assert.h"
+
+#include <vector>
+#include <string>
+
+namespace CVC4 {
+
+/**
+ * A simple S-expression. An S-expression is either an atom with a string value, or a
+ * list of other S-expressions.
+ */
+class CVC4_PUBLIC SExpr {
+
+ /** Flag telling us if this is an atom or a list. */
+ bool d_isAtom;
+
+ /** The value of an atomic S-expression. */
+ std::string d_value;
+
+ /** The children of a list S-expression. */
+ std::vector<SExpr> d_children;
+
+public:
+ SExpr() :
+ d_isAtom(true) {
+ }
+
+ SExpr(const std::string& value) :
+ d_isAtom(true),
+ d_value(value) {
+ }
+
+ SExpr(const std::vector<SExpr> children) :
+ d_isAtom(false),
+ d_children(children) {
+ }
+
+ /** Is this S-expression an atom? */
+ bool isAtom() const;
+
+ /** Get the string value of this S-expression. This will cause an error if this S-expression
+ * is not an atom.
+ */
+ const std::string getValue() const;
+
+ /** Get the children of this S-expression. This will cause an error if this S-expression
+ * is not a list.
+ */
+ const std::vector<SExpr> getChildren() const;
+};
+
+inline bool SExpr::isAtom() const {
+ return d_isAtom;
+}
+
+inline const std::string SExpr::getValue() const {
+ AlwaysAssert( d_isAtom );
+ return d_value;
+}
+
+inline const std::vector<SExpr> SExpr::getChildren() const {
+ AlwaysAssert( !d_isAtom );
+ return d_children;
+}
+
+inline std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
+ if( sexpr.isAtom() ) {
+ out << sexpr.getValue();
+ } else {
+ std::vector<SExpr> children = sexpr.getChildren();
+ out << "(";
+ bool first = true;
+ for( std::vector<SExpr>::iterator it = children.begin(); it != children.end(); ++it ) {
+ if( first ) {
+ first = false;
+ } else {
+ out << " ";
+ }
+ out << *it;
+ }
+ out << ")";
+ }
+ return out;
+}
+
+}
+
+#endif /* __CVC4__SEXPR_H_ */
projects / cvc5.git / commitdiff