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/util | |
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/util')
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/sexpr.cpp | 58 | ||||
-rw-r--r-- | src/util/sexpr.h | 81 |
3 files changed, 92 insertions, 48 deletions
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 */ |