diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 19:31:24 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-04 19:31:24 +0000 |
commit | 67a3ba16218ca0a936a6f2430dce721a076885f3 (patch) | |
tree | dff41999a0fb7a043c3421272e451cb2718010a4 /src/util/sexpr.h | |
parent | 437686e2050a622a3f7e68077aff46fd6af83cbd (diff) |
Adding general support for SMT2 set-info command
Diffstat (limited to 'src/util/sexpr.h')
-rw-r--r-- | src/util/sexpr.h | 108 |
1 files changed, 108 insertions, 0 deletions
diff --git a/src/util/sexpr.h b/src/util/sexpr.h new file mode 100644 index 000000000..cf9298c4e --- /dev/null +++ b/src/util/sexpr.h @@ -0,0 +1,108 @@ +/********************* */ +/** 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_ */ |