void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
try {
vector<SExpr> v;
- v.push_back(SExpr(d_flag));
+ v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
v.push_back(smtEngine->getInfo(d_flag));
stringstream ss;
ss << SExpr(v);
SExpr sexpr;
}
: /* set the logic */
- SET_LOGIC_TOK SYMBOL
- { name = AntlrInput::tokenText($SYMBOL);
- Debug("parser") << "set logic: '" << name << "'" << std::endl;
+ SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
+ { Debug("parser") << "set logic: '" << name << "'" << std::endl;
if( PARSER_STATE->logicIsSet() ) {
PARSER_STATE->parseError("Only one set-logic is allowed.");
}
{ sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
| str[s]
{ sexpr = SExpr(s); }
- | SYMBOL
- { sexpr = SExpr(AntlrInput::tokenText($SYMBOL)); }
+ | symbol[s,CHECK_NONE,SYM_SORT]
+ { sexpr = SExpr(s); }
| builtinOp[k]
{ std::stringstream ss;
ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k);
// valid GMP rational string
expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); }
- | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK
+ | LPAREN_TOK INDEX_TOK bvLit=SIMPLE_SYMBOL size=INTEGER_LITERAL RPAREN_TOK
{ if(AntlrInput::tokenText($bvLit).find("bv") == 0) {
expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) );
} else {
;
/**
-* Matches a builtin operator symbol and sets kind to its associated Expr kind.
-*/
+ * Matches a builtin operator symbol and sets kind to its associated Expr kind.
+ */
builtinOp[CVC4::Kind& kind]
@init {
Debug("parser") << "builtin: " << AntlrInput::tokenText(LT(1)) << std::endl;
symbol[std::string& id,
CVC4::parser::DeclarationCheck check,
CVC4::parser::SymbolType type]
- : SYMBOL
- { id = AntlrInput::tokenText($SYMBOL);
- Debug("parser") << "symbol: " << id
- << " check? " << check
- << " type? " << type << std::endl;
- PARSER_STATE->checkDeclaration(id, check, type); }
+ : SIMPLE_SYMBOL
+ { id = AntlrInput::tokenText($SIMPLE_SYMBOL);
+ PARSER_STATE->checkDeclaration(id, check, type);
+ }
+ | QUOTED_SYMBOL
+ { id = AntlrInput::tokenText($QUOTED_SYMBOL);
+ /* strip off the quotes */
+ id = id.substr(1, id.size() - 2);
+ PARSER_STATE->checkDeclaration(id, check, type);
+ }
;
/**
BVSGE_TOK : 'bvsge';
/**
- * Matches a symbol from the input. A symbol is a "simple" symbol or a
- * sequence of printable ASCII characters that starts and ends with | and
- * does not otherwise contain |.
+ * A sequence of printable ASCII characters (except backslash) that starts
+ * and ends with | and does not otherwise contain |.
+ *
+ * You shouldn't generally use this in parser rules, as the |quoting|
+ * will be part of the token text. Use the symbol[] parser rule instead.
*/
-SYMBOL
- : SIMPLE_SYMBOL
- | '|' ~('|')+ '|'
+QUOTED_SYMBOL
+ : '|' ~('|' | '\\')* '|'
;
/**
* with a colon.
*/
KEYWORD
- : ':' SIMPLE_SYMBOL
+ : ':' (ALPHA | DIGIT | SYMBOL_CHAR)+
;
-/** Matches a "simple" symbol: a non-empty sequence of letters, digits and
+/**
+ * Matches a "simple" symbol: a non-empty sequence of letters, digits and
* the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a
- * digit, and is not the special reserved symbol '_'.
+ * digit, and is not the special reserved symbols '!' or '_'.
*/
-fragment SIMPLE_SYMBOL
+SIMPLE_SYMBOL
: (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+
| ALPHA
- | SYMBOL_CHAR_NOUNDERSCORE
+ | SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
;
/**
/**
- * Matches a double quoted string literal. Escaping is supported, and
+ * Matches a double quoted string literal. Escaping is supported, and
* escape character '\' has to be escaped.
+ *
+ * You shouldn't generally use this in parser rules, as the quotes
+ * will be part of the token text. Use the str[] parser rule instead.
*/
STRING_LITERAL
: '"' (ESCAPE | ~('"'|'\\'))* '"'
fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F';
/**
- * Matches the characters that may appear in a "symbol" (i.e., an identifier)
+ * Matches the characters that may appear as a one-character "symbol"
+ * (which excludes _ and !, which are reserved words in SMT-LIBv2).
*/
-fragment SYMBOL_CHAR_NOUNDERSCORE
- : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~'
+fragment SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE
+ : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '.' | '$' | '~'
| '&' | '^' | '<' | '>' | '@'
;
+/**
+ * Matches the characters that may appear in a "symbol" (i.e., an identifier)
+ */
fragment SYMBOL_CHAR
- : SYMBOL_CHAR_NOUNDERSCORE | '_'
+ : SYMBOL_CHAR_NOUNDERSCORE_NOATTRIBUTE | '_' | '!'
;
/**
* Matches an allowed escaped character.
*/
-fragment ESCAPE : '\\' ('"' | '\\' | 'n' | 't' | 'r');
+fragment ESCAPE : '\\' ('"' | '\\');
}/* CvcPrinter::toStream(Command*) */
+static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+ Printer::getPrinter(language::output::LANG_CVC4)->toStream(out, sexpr);
+}
+
template <class T>
static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
}/* CvcPrinter::toStream(CommandStatus*) */
-static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
- if(sexpr.isInteger()) {
- out << sexpr.getIntegerValue();
- } else if(sexpr.isRational()) {
- out << sexpr.getRationalValue();
- } else if(sexpr.isString()) {
- string s = sexpr.getValue();
- // escape backslash and quote
- for(size_t i = 0; i < s.size(); ++i) {
- if(s[i] == '"') {
- s.replace(i, 1, "\\\"");
- ++i;
- } else if(s[i] == '\\') {
- s.replace(i, 1, "\\\\");
- ++i;
- }
- }
- out << "\"" << s << "\"";
- } else {
- out << sexpr;
- }
-}
-
static void toStream(std::ostream& out, const AssertCommand* c) throw() {
out << "ASSERT " << c->getExpr() << ";";
}
#include "printer/cvc/cvc_printer.h"
#include "printer/ast/ast_printer.h"
+#include <string>
+
+using namespace std;
+
namespace CVC4 {
Printer* Printer::d_printers[language::output::LANG_MAX];
}
}/* Printer::toStream() */
+void Printer::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+ if(sexpr.isInteger()) {
+ out << sexpr.getIntegerValue();
+ } else if(sexpr.isRational()) {
+ out << sexpr.getRationalValue();
+ } else if(sexpr.isKeyword()) {
+ out << sexpr.getValue();
+ } else if(sexpr.isString()) {
+ string s = sexpr.getValue();
+ // escape backslash and quote
+ for(size_t i = 0; i < s.length(); ++i) {
+ if(s[i] == '"') {
+ s.replace(i, 1, "\\\"");
+ ++i;
+ } else if(s[i] == '\\') {
+ s.replace(i, 1, "\\\\");
+ ++i;
+ }
+ }
+ out << "\"" << s << "\"";
+ } else {
+ out << '(';
+ const vector<SExpr>& kids = sexpr.getChildren();
+ bool first = true;
+ for(vector<SExpr>::const_iterator i = kids.begin(); i != kids.end(); ++i) {
+ if(first) {
+ first = false;
+ } else {
+ out << ' ';
+ }
+ out << *i;
+ }
+ out << ')';
+ }
+}/* Printer::toStream() */
+
}/* CVC4 namespace */
#define __CVC4__PRINTER__PRINTER_H
#include "util/language.h"
+#include "util/sexpr.h"
#include "expr/node.h"
#include "expr/command.h"
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
+ /** Write an SExpr out to a stream with this Printer. */
+ virtual void toStream(std::ostream& out, const SExpr& sexpr) const throw();
+
/**
* Write a Result out to a stream with this Printer.
*
s->toStream(out, language::output::LANG_SMTLIB_V2);
}/* SmtPrinter::toStream() */
+void SmtPrinter::toStream(std::ostream& out, const SExpr& sexpr) const throw() {
+ Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
+}/* SmtPrinter::toStream() */
+
}/* CVC4::printer::smt namespace */
}/* CVC4::printer namespace */
}/* CVC4 namespace */
void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
void toStream(std::ostream& out, const CommandStatus* s) const throw();
+ void toStream(std::ostream& out, const SExpr& sexpr) const throw();
};/* class SmtPrinter */
}/* CVC4::printer::smt namespace */
#include "printer/dagification_visitor.h"
#include "util/node_visitor.h"
#include "theory/substitutions.h"
+#include "util/language.h"
using namespace std;
}/* Smt2Printer::toStream(Command*) */
-static void toStream(std::ostream& out, const SExpr& sexpr) throw() {
- if(sexpr.isInteger()) {
- out << sexpr.getIntegerValue();
- } else if(sexpr.isRational()) {
- out << sexpr.getRationalValue();
- } else if(sexpr.isString()) {
- string s = sexpr.getValue();
- // escape backslash and quote
- for(size_t i = 0; i < s.length(); ++i) {
- if(s[i] == '"') {
- s.replace(i, 1, "\\\"");
- ++i;
- } else if(s[i] == '\\') {
- s.replace(i, 1, "\\\\");
- ++i;
- }
- }
- out << "\"" << s << "\"";
- } else {
- out << sexpr;
- }
+static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
+ Printer::getPrinter(language::output::LANG_SMTLIB_V2)->toStream(out, sexpr);
}
template <class T>
}
static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
- out << "(set-info " << c->getFlag() << " ";
+ out << "(set-info :" << c->getFlag() << " ";
toStream(out, c->getSExpr());
out << ")";
}
static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
- out << "(get-info " << c->getFlag() << ")";
+ out << "(get-info :" << c->getFlag() << ")";
}
static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
- out << "(set-option " << c->getFlag() << " ";
+ out << "(set-option :" << c->getFlag() << " ";
toStream(out, c->getSExpr());
out << ")";
}
static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
- out << "(get-option " << c->getFlag() << ")";
+ out << "(get-option :" << c->getFlag() << ")";
}
static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
}
SExpr SmtEngine::getInfo(const std::string& key) const
- throw(BadOptionException) {
+ throw(BadOptionException, ModalException) {
SmtScope smts(this);
}
return stats;
} else if(key == ":error-behavior") {
- return SExpr("immediate-exit");
+ return SExpr::Keyword("immediate-exit");
} else if(key == ":name") {
return Configuration::getName();
} else if(key == ":version") {
} else if(key == ":status") {
return d_status.asSatisfiabilityResult().toString();
} else if(key == ":reason-unknown") {
- if(d_status.isUnknown()) {
+ if(!d_status.isNull() && d_status.isUnknown()) {
stringstream ss;
ss << d_status.whyUnknown();
- return ss.str();
+ return SExpr::Keyword(ss.str());
} else {
throw ModalException("Can't get-info :reason-unknown when the "
"last result wasn't unknown!");
* Query information about the SMT environment.
*/
SExpr getInfo(const std::string& key) const
- throw(BadOptionException);
+ throw(BadOptionException, ModalException);
/**
* Set an aspect of the current SMT execution environment.
*/
unsigned long getTimeRemaining() const throw(ModalException);
+ /**
+ * Permit access to the underlying ExprManager.
+ */
+ ExprManager* getExprManager() const {
+ return d_exprManager;
+ }
+
/**
* Permit access to the underlying StatisticsRegistry.
*/
matcher.h \
gmp_util.h \
sexpr.h \
+ sexpr.cpp \
stats.h \
stats.cpp \
dynamic_array.h \
--- /dev/null
+/********************* */
+/*! \file sexpr.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-2012 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 representation of S-expressions
+ **
+ ** Simple representation of S-expressions.
+ **/
+
+#include <iostream>
+#include <vector>
+
+#include "util/sexpr.h"
+#include "util/Assert.h"
+#include "printer/printer.h"
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) {
+ switch(type) {
+ case SExpr::SEXPR_STRING:
+ out << "SEXPR_STRING";
+ break;
+ case SExpr::SEXPR_KEYWORD:
+ out << "SEXPR_KEYWORD";
+ break;
+ case SExpr::SEXPR_INTEGER:
+ out << "SEXPR_INTEGER";
+ break;
+ case SExpr::SEXPR_RATIONAL:
+ out << "SEXPR_RATIONAL";
+ break;
+ case SExpr::SEXPR_NOT_ATOM:
+ out << "SEXPR_NOT_ATOM";
+ break;
+ default:
+ Unimplemented();
+ break;
+ }
+ return out;
+}
+
+std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) {
+ Printer::getPrinter(Expr::setlanguage::getLanguage(out))->toStream(out, sexpr);
+ return out;
+}
+
+}/* CVC4 namespace */
** Major contributors: mdeters
** 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)
+ ** Copyright (c) 2009-2012 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 representation of SMT S-expressions.
+ ** \brief Simple representation of S-expressions
**
- ** Simple representation of SMT S-expressions.
+ ** Simple representation of S-expressions.
**/
#include "cvc4_public.h"
*/
class CVC4_PUBLIC SExpr {
- enum SexprTypes {
+ enum SExprTypes {
SEXPR_STRING,
+ SEXPR_KEYWORD,
SEXPR_INTEGER,
SEXPR_RATIONAL,
SEXPR_NOT_ATOM
} d_sexprType;
- friend std::ostream& operator<<(std::ostream&, SexprTypes);
+ friend std::ostream& operator<<(std::ostream&, SExprTypes);
/** The value of an atomic integer-valued S-expression. */
CVC4::Integer d_integerValue;
std::vector<SExpr> d_children;
public:
+
+ class Keyword : protected std::string {
+ public:
+ Keyword(const std::string& s) : std::string(s) {}
+ const std::string& getString() const { return *this; }
+ };/* class Keyword */
+
SExpr() :
d_sexprType(SEXPR_STRING),
d_integerValue(0),
d_children() {
}
+ SExpr(const Keyword& value) :
+ d_sexprType(SEXPR_KEYWORD),
+ d_integerValue(0),
+ d_rationalValue(0),
+ d_stringValue(value.getString()),
+ d_children() {
+ }
+
SExpr(const std::vector<SExpr> children) :
d_sexprType(SEXPR_NOT_ATOM),
d_integerValue(0),
/** Is this S-expression a string? */
bool isString() const;
+ /** Is this S-expression a string? */
+ bool isKeyword() const;
+
/**
* Get the string value of this S-expression. This will cause an
* error if this S-expression is not an atom.
* 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;
+ const std::vector<SExpr>& getChildren() const;
};/* class SExpr */
-inline std::ostream& operator<<(std::ostream& out, SExpr::SexprTypes type) {
- switch(type) {
- case SExpr::SEXPR_STRING:
- out << "SEXPR_STRING";
- break;
- case SExpr::SEXPR_INTEGER:
- out << "SEXPR_INTEGER";
- break;
- case SExpr::SEXPR_RATIONAL:
- out << "SEXPR_RATIONAL";
- break;
- case SExpr::SEXPR_NOT_ATOM:
- out << "SEXPR_NOT_ATOM";
- break;
- default:
- Unimplemented();
- break;
- }
- return out;
-}
+std::ostream& operator<<(std::ostream& out, SExpr::SExprTypes type) CVC4_PUBLIC;
inline bool SExpr::isAtom() const {
return d_sexprType != SEXPR_NOT_ATOM;
return d_sexprType == SEXPR_STRING;
}
+inline bool SExpr::isKeyword() const {
+ return d_sexprType == SEXPR_KEYWORD;
+}
+
inline const std::string SExpr::getValue() const {
AlwaysAssert( isAtom() );
switch(d_sexprType) {
case SEXPR_RATIONAL:
return d_rationalValue.toString();
case SEXPR_STRING:
+ case SEXPR_KEYWORD:
return d_stringValue;
default:
Unhandled(d_sexprType);
return d_rationalValue;
}
-inline const std::vector<SExpr> SExpr::getChildren() const {
+inline const std::vector<SExpr>& SExpr::getChildren() const {
AlwaysAssert( !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;
-}
+std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC;
}/* CVC4 namespace */
projects / cvc5.git / commitdiff