diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-11-15 22:57:14 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-11-15 22:57:14 +0000 |
commit | 5e5956d492ab18b5b4d4bb51117ac760867a525d (patch) | |
tree | 0c151baa58810722288ad986dfa13123de273739 /src/expr | |
parent | ec4e1bdba56565d6372cb19ded12c9cadc506870 (diff) |
Pretty-printer infrastructure created (in src/printer) and SMT-LIBv2 printer
implemented. This new infrastructure removes support for pretty-printing
(even in the AST language) an Expr with reference count 0. Previously,
this was supported in a few places internally to the expr package, for
example in NodeBuilder. (Now, a NodeBuilder cannot be prettyprinted, you
must extract the Node before printing it.)
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr_template.h | 16 | ||||
-rw-r--r-- | src/expr/metakind_template.h | 15 | ||||
-rw-r--r-- | src/expr/node.h | 8 | ||||
-rw-r--r-- | src/expr/node_builder.h | 19 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 63 |
5 files changed, 32 insertions, 89 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index be089bca8..2e27b4f66 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -648,15 +648,23 @@ public: ExprSetLanguage(OutputLanguage l) : d_language(l) {} inline void applyLanguage(std::ostream& out) { - out.iword(s_iosIndex) = int(d_language); + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(d_language) + 1; } static inline OutputLanguage getLanguage(std::ostream& out) { - return OutputLanguage(out.iword(s_iosIndex)); + long& l = out.iword(s_iosIndex); + if(l == 0) { + // set the default language on this ostream + // (offset by one to detect whether default has been set yet) + l = s_defaultLanguage + 1; + } + return OutputLanguage(l - 1); } static inline void setLanguage(std::ostream& out, OutputLanguage l) { - out.iword(s_iosIndex) = int(l); + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(l) + 1; } };/* class ExprSetLanguage */ @@ -664,7 +672,7 @@ public: ${getConst_instantiations} -#line 659 "${template}" +#line 676 "${template}" namespace expr { diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index cb9730d34..c4604d40e 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -88,11 +88,6 @@ struct NodeValueCompare { inline static size_t constHash(const ::CVC4::expr::NodeValue* nv); };/* struct NodeValueCompare */ -struct NodeValueConstPrinter { - inline static void toStream(std::ostream& out, - const ::CVC4::expr::NodeValue* nv); -}; - /** * "metakinds" represent the "kinds" of kinds at the meta-level. * "metakind" is an ugly name but it's not used by client code, just @@ -264,6 +259,12 @@ ${metakind_constHashes} } } +struct NodeValueConstPrinter { + inline static void toStream(std::ostream& out, + const ::CVC4::expr::NodeValue* nv); + inline static void toStream(std::ostream& out, TNode n); +}; + inline void NodeValueConstPrinter::toStream(std::ostream& out, const ::CVC4::expr::NodeValue* nv) { Assert(nv->getMetaKind() == kind::metakind::CONSTANT); @@ -275,6 +276,10 @@ ${metakind_constPrinters} } } +inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { + toStream(out, n.d_nv); +} + /** * Cleanup to be performed when a NodeValue zombie is collected, and * it has CONSTANT metakind. This calls the destructor for the underlying diff --git a/src/expr/node.h b/src/expr/node.h index c30e2e856..bd4864fed 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -105,6 +105,12 @@ class NodeValue; class ExprSetDepth; }/* CVC4::expr namespace */ +namespace kind { + namespace metakind { + struct NodeValueConstPrinter; + }/* CVC4::kind::metakind namespace */ +}/* CVC4::kind namespace */ + /** * Encapsulation of an NodeValue pointer. The reference count is * maintained in the NodeValue if ref_count is true. @@ -149,6 +155,8 @@ class NodeTemplate { friend class ::CVC4::expr::attr::AttributeManager; + friend struct ::CVC4::kind::metakind::NodeValueConstPrinter; + /** * Assigns the expression value and does reference counting. No assumptions * are made on the expression, and should only be used if we know what we diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index ce0928209..cc8c780a8 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -178,9 +178,6 @@ namespace CVC4 { namespace CVC4 { -template <unsigned nchild_thresh> -inline std::ostream& operator<<(std::ostream&, const NodeBuilder<nchild_thresh>&); - /* see expr/convenience_node_builders.h */ class AndNodeBuilder; class OrNodeBuilder; @@ -692,13 +689,6 @@ public: operator Node(); operator Node() const; - inline void toStream(std::ostream& out, int depth = -1, bool types = false, - OutputLanguage language = language::output::LANG_AST) const { - Assert(!isUsed(), "NodeBuilder is one-shot only; " - "attempt to access it after conversion"); - d_nv->toStream(out, depth, types, language); - } - NodeBuilder<nchild_thresh>& operator&=(TNode); NodeBuilder<nchild_thresh>& operator|=(TNode); NodeBuilder<nchild_thresh>& operator+=(TNode); @@ -1250,15 +1240,6 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { } } -template <unsigned nchild_thresh> -inline std::ostream& operator<<(std::ostream& out, - const NodeBuilder<nchild_thresh>& b) { - b.toStream(out, - Node::setdepth::getDepth(out), - Node::printtypes::getPrintTypes(out)); - return out; -} - }/* CVC4 namespace */ #endif /* __CVC4__NODE_BUILDER_H */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index a5fff2095..666462875 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -25,6 +25,7 @@ #include "expr/kind.h" #include "expr/metakind.h" #include "util/language.h" +#include "printer/printer.h" #include <sstream> using namespace std; @@ -44,67 +45,7 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out, int toDepth, bool types, OutputLanguage language) const { - using namespace CVC4; - using namespace CVC4::kind; - using namespace CVC4::language::output; - - switch(language) { - case LANG_CVC4: - // FIXME support cvc output language - case LANG_SMTLIB: - // FIXME support smt-lib output language - case LANG_SMTLIB_V2: - // FIXME support smt-lib v2 output language - case LANG_AST: - if(getKind() == kind::NULL_EXPR) { - out << "null"; - } else if(getMetaKind() == kind::metakind::VARIABLE) { - if(getKind() != kind::VARIABLE && - getKind() != kind::SORT_TYPE) { - out << getKind() << ':'; - } - - string s; - NodeManager* nm = NodeManager::currentNM(); - - // conceptually "this" is const, and hasAttribute() doesn't change - // its argument, but it requires a non-const key arg (for now) - if(nm->getAttribute(const_cast<NodeValue*>(this), - VarNameAttr(), s)) { - out << s; - } else { - out << "var_" << d_id; - } - if(types) { - // print the whole type, but not *its* type - out << ":"; - nm->getType(TNode(this)).toStream(out, -1, false, language); - } - } else { - out << '(' << Kind(d_kind); - if(getMetaKind() == kind::metakind::CONSTANT) { - out << ' '; - kind::metakind::NodeValueConstPrinter::toStream(out, this); - } else { - for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) { - if(i != nv_end()) { - out << ' '; - } - if(toDepth != 0) { - (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1, - types, language); - } else { - out << "(...)"; - } - } - } - out << ')'; - } - break; - - default: - out << "[output language " << language << " unsupported]"; - }// end switch(language) + Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, types); } void NodeValue::printAst(std::ostream& out, int ind) const { |