diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-07-17 22:07:59 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-07-17 22:07:59 +0000 |
commit | 4923b53ad705acc04348da693f03f83f8d9853db (patch) | |
tree | b557cb22ce1f21bcbcca9d6ebdcbf205e5537b58 /src | |
parent | 2b83291d229c957e2becf7397d186040959602df (diff) |
SMT-LIBv2 compliance updates:
* more correct support for get-info responses
* printer infrastructure extended to SExprs
* parser updates to correctly handle symbols and strings
(there were some minor differences from the spec)
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/command.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 74 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 27 | ||||
-rw-r--r-- | src/printer/printer.cpp | 40 | ||||
-rw-r--r-- | src/printer/printer.h | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt/smt_printer.h | 1 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 32 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 9 | ||||
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/sexpr.cpp | 58 | ||||
-rw-r--r-- | src/util/sexpr.h | 81 |
13 files changed, 208 insertions, 133 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 5b889712d..f48e07887 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -991,7 +991,7 @@ std::string GetInfoCommand::getFlag() const throw() { 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); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 577438d37..bddb64c3c 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -174,9 +174,8 @@ command returns [CVC4::Command* cmd = NULL] 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."); } @@ -407,8 +406,8 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] { 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); @@ -636,7 +635,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] // 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 { @@ -759,8 +758,8 @@ str[std::string& s] ; /** -* 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; @@ -952,12 +951,16 @@ symbolList[std::vector<std::string>& names, 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); + } ; /** @@ -1133,13 +1136,14 @@ BVSGT_TOK : 'bvsgt'; 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 + : '|' ~('|' | '\\')* '|' ; /** @@ -1147,17 +1151,18 @@ 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 ; /** @@ -1219,8 +1224,11 @@ BINARY_LITERAL /** - * 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 | ~('"'|'\\'))* '"' @@ -1250,18 +1258,22 @@ fragment DIGIT : '0'..'9'; 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 : '\\' ('"' | '\\'); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index e4a25e008..664ea58fc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -709,6 +709,10 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, }/* 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(); @@ -725,29 +729,6 @@ void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const 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() << ";"; } diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 5229400b5..0881b814b 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -25,6 +25,10 @@ #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]; @@ -87,4 +91,40 @@ void Printer::toStream(std::ostream& out, const Result& r) const throw() { } }/* 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 */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 8d1931a83..e3b1d6f40 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -22,6 +22,7 @@ #define __CVC4__PRINTER__PRINTER_H #include "util/language.h" +#include "util/sexpr.h" #include "expr/node.h" #include "expr/command.h" @@ -62,6 +63,9 @@ public: /** 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. * diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index f74a1e07d..fa46523a4 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -47,6 +47,10 @@ void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw 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 */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 612dfd19e..6e1c607bf 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -34,6 +34,7 @@ public: 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 */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 640f4209c..a3b22ac24 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -27,6 +27,7 @@ #include "printer/dagification_visitor.h" #include "util/node_visitor.h" #include "theory/substitutions.h" +#include "util/language.h" using namespace std; @@ -503,27 +504,8 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, }/* 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> @@ -679,23 +661,23 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw } 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() { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a182d8927..81a212edd 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -660,7 +660,7 @@ void SmtEngine::setInfo(const std::string& key, const SExpr& value) } SExpr SmtEngine::getInfo(const std::string& key) const - throw(BadOptionException) { + throw(BadOptionException, ModalException) { SmtScope smts(this); @@ -677,7 +677,7 @@ SExpr SmtEngine::getInfo(const std::string& key) const } 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") { @@ -687,10 +687,10 @@ SExpr SmtEngine::getInfo(const std::string& key) const } 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!"); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 4df9054a7..efb2425a1 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -309,7 +309,7 @@ public: * 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. @@ -536,6 +536,13 @@ public: unsigned long getTimeRemaining() const throw(ModalException); /** + * Permit access to the underlying ExprManager. + */ + ExprManager* getExprManager() const { + return d_exprManager; + } + + /** * Permit access to the underlying StatisticsRegistry. */ StatisticsRegistry* getStatisticsRegistry() const; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 08b5d05f5..a3c6a00e9 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -46,6 +46,7 @@ libutil_la_SOURCES = \ matcher.h \ gmp_util.h \ sexpr.h \ + sexpr.cpp \ stats.h \ stats.cpp \ dynamic_array.h \ diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp new file mode 100644 index 000000000..ff6ff6872 --- /dev/null +++ b/src/util/sexpr.cpp @@ -0,0 +1,58 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9d568bad8..a49da4b48 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -5,15 +5,15 @@ ** 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" @@ -36,13 +36,14 @@ namespace CVC4 { */ 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; @@ -57,6 +58,13 @@ class CVC4_PUBLIC SExpr { 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), @@ -89,6 +97,14 @@ public: 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), @@ -109,6 +125,9 @@ public: /** 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. @@ -131,30 +150,11 @@ public: * 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; @@ -172,6 +172,10 @@ inline bool SExpr::isString() const { 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) { @@ -180,6 +184,7 @@ inline const std::string SExpr::getValue() const { case SEXPR_RATIONAL: return d_rationalValue.toString(); case SEXPR_STRING: + case SEXPR_KEYWORD: return d_stringValue; default: Unhandled(d_sexprType); @@ -197,32 +202,12 @@ inline const CVC4::Rational& SExpr::getRationalValue() const { 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 */ |