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/sexpr.cpp | |
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/sexpr.cpp')
-rw-r--r-- | src/util/sexpr.cpp | 58 |
1 files changed, 58 insertions, 0 deletions
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 */ |