diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-22 21:10:51 +0000 |
commit | e2611a54c5479086df0c4a80f56597aae80b5c4e (patch) | |
tree | b0d98600bd70147f28197883d3481614b87d76f6 /src/util/sexpr.h | |
parent | 8b106b77c11d12d16abac845ed704845ef888bd2 (diff) |
Separate public-facing and internal-facing interfaces to Statistics.
The external interface (e.g., what's answered by ExprManager::getStatistics() and SmtEngine::getStatistics()) is a snapshot of the current statistics (rather than a reference to the actual StatisticsRegistry).
The StatisticsRegistry is now internal-only. However, it's built as a convenience library so that the parser and driver can use it too (by re-linking against it).
This is part of the ongoing effort to clean up the public interface.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r-- | src/util/sexpr.h | 31 |
1 files changed, 29 insertions, 2 deletions
diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 0734dec6c..4feffc18f 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -23,6 +23,8 @@ #include <vector> #include <string> +#include <iomanip> +#include <sstream> #include "util/integer.h" #include "util/rational.h" @@ -151,6 +153,12 @@ public: */ const std::vector<SExpr>& getChildren() const; + /** Is this S-expression equal to another? */ + bool operator==(const SExpr& s) const; + + /** Is this S-expression different from another? */ + bool operator!=(const SExpr& s) const; + };/* class SExpr */ inline bool SExpr::isAtom() const { @@ -178,8 +186,15 @@ inline std::string SExpr::getValue() const { switch(d_sexprType) { case SEXPR_INTEGER: return d_integerValue.toString(); - case SEXPR_RATIONAL: - return d_rationalValue.toString(); + case SEXPR_RATIONAL: { + // We choose to represent rationals as decimal strings rather than + // "numerator/denominator." Perhaps an additional SEXPR_DECIMAL + // could be added if we need both styles, even if it's backed by + // the same Rational object. + std::stringstream ss; + ss << std::fixed << d_rationalValue.getDouble(); + return ss.str(); + } case SEXPR_STRING: case SEXPR_KEYWORD: return d_stringValue; @@ -204,6 +219,18 @@ inline const std::vector<SExpr>& SExpr::getChildren() const { return d_children; } +inline bool SExpr::operator==(const SExpr& s) const { + return d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue && + d_children == s.d_children; +} + +inline bool SExpr::operator!=(const SExpr& s) const { + return !(*this == s); +} + std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) CVC4_PUBLIC; }/* CVC4 namespace */ |