diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/dtype_selector.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr_iomanip.cpp | 125 | ||||
-rw-r--r-- | src/expr/expr_iomanip.h | 177 | ||||
-rw-r--r-- | src/expr/node.h | 82 | ||||
-rw-r--r-- | src/expr/node_value.h | 28 | ||||
-rw-r--r-- | src/expr/type_node.h | 34 |
7 files changed, 8 insertions, 442 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index dcbc4aa97..a6a7c04e9 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -32,8 +32,6 @@ libcvc5_add_sources( emptyset.h emptybag.cpp emptybag.h - expr_iomanip.cpp - expr_iomanip.h kind_map.h match_trie.cpp match_trie.h diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index 30c9057f1..67a36798f 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -15,8 +15,6 @@ #include "expr/dtype_selector.h" -#include "options/set_language.h" - using namespace cvc5::kind; namespace cvc5 { diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp deleted file mode 100644 index 06fcaee66..000000000 --- a/src/expr/expr_iomanip.cpp +++ /dev/null @@ -1,125 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Kshitij Bansal - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Expr IO manipulation classes. - */ - -#include "expr/expr_iomanip.h" - -#include <iomanip> -#include <iostream> - -#include "options/options.h" -#include "options/expr_options.h" - -namespace cvc5 { -namespace expr { - -const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); -const int ExprDag::s_iosIndex = std::ios_base::xalloc(); - -ExprSetDepth::ExprSetDepth(long depth) : d_depth(depth) {} - -void ExprSetDepth::applyDepth(std::ostream& out) { - out.iword(s_iosIndex) = d_depth; -} - -long ExprSetDepth::getDepth(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default print depth on this ostream - if(not Options::isCurrentNull()) { - l = options::defaultExprDepth(); - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultPrintDepth; - } - } - return l; -} - -void ExprSetDepth::setDepth(std::ostream& out, long depth) { - out.iword(s_iosIndex) = depth; -} - - -ExprSetDepth::Scope::Scope(std::ostream& out, long depth) - : d_out(out), d_oldDepth(ExprSetDepth::getDepth(out)) -{ - ExprSetDepth::setDepth(out, depth); -} - -ExprSetDepth::Scope::~Scope() { - ExprSetDepth::setDepth(d_out, d_oldDepth); -} - -ExprDag::ExprDag(bool dag) : d_dag(dag ? 1 : 0) {} - -ExprDag::ExprDag(int dag) : d_dag(dag < 0 ? 0 : dag) {} - -void ExprDag::applyDag(std::ostream& out) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(d_dag) + 1; -} - -size_t ExprDag::getDag(std::ostream& out) { - long& l = out.iword(s_iosIndex); - if(l == 0) { - // set the default dag setting on this ostream - // (offset by one to detect whether default has been set yet) - if(not Options::isCurrentNull()) { - l = options::defaultDagThresh() + 1; - } - if(l == 0) { - // if called from outside the library, we may not have options - // available to us at this point (or perhaps the output language - // is not set in Options). Default to something reasonable, but - // don't set "l" since that would make it "sticky" for this - // stream. - return s_defaultDag + 1; - } - } - return static_cast<size_t>(l - 1); -} - -void ExprDag::setDag(std::ostream& out, size_t dag) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = static_cast<long>(dag) + 1; -} - -ExprDag::Scope::Scope(std::ostream& out, size_t dag) - : d_out(out), - d_oldDag(ExprDag::getDag(out)) { - ExprDag::setDag(out, dag); -} - -ExprDag::Scope::~Scope() { - ExprDag::setDag(d_out, d_oldDag); -} - -std::ostream& operator<<(std::ostream& out, ExprDag d) { - d.applyDag(out); - return out; -} - -std::ostream& operator<<(std::ostream& out, ExprSetDepth sd) { - sd.applyDepth(out); - return out; -} - -} // namespace expr -} // namespace cvc5 diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h deleted file mode 100644 index a04ed9f39..000000000 --- a/src/expr/expr_iomanip.h +++ /dev/null @@ -1,177 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Expr IO manipulation classes. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__EXPR__EXPR_IOMANIP_H -#define CVC5__EXPR__EXPR_IOMANIP_H - -#include <iosfwd> - -namespace cvc5 { -namespace expr { - -/** - * IOStream manipulator to set the maximum depth of Exprs when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << setdepth(3) << e; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same expr as above] - * - * gives "(OR a b (...))". - * - * The implementation of this class serves two purposes; it holds - * information about the depth setting (such as the index of the - * allocated word in ios_base), and serves also as the manipulator - * itself (as above). - */ -class ExprSetDepth -{ - public: - /** - * Construct a ExprSetDepth with the given depth. - */ - ExprSetDepth(long depth); - - void applyDepth(std::ostream& out); - - static long getDepth(std::ostream& out); - - static void setDepth(std::ostream& out, long depth); - - /** - * Set the expression depth on the output stream for the current - * stack scope. This makes sure the old depth is reset on the stream - * after normal OR exceptional exit from the scope, using the RAII - * C++ idiom. - */ - class Scope { - public: - Scope(std::ostream& out, long depth); - ~Scope(); - - private: - std::ostream& d_out; - long d_oldDepth; - };/* class ExprSetDepth::Scope */ - - private: - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default depth to print, for ostreams that haven't yet had a - * setdepth() applied to them. - */ - static const int s_defaultPrintDepth = -1; - - /** - * When this manipulator is used, the depth is stored here. - */ - long d_depth; -}; /* class ExprSetDepth */ - -/** - * IOStream manipulator to print expressions as a dag (or not). - */ -class ExprDag -{ - public: - /** - * Construct a ExprDag with the given setting (dagification on or off). - */ - explicit ExprDag(bool dag); - - /** - * Construct a ExprDag with the given setting (letify only common - * subexpressions that appear more than 'dag' times). dag <= 0 means - * don't dagify. - */ - explicit ExprDag(int dag); - - void applyDag(std::ostream& out); - - static size_t getDag(std::ostream& out); - - static void setDag(std::ostream& out, size_t dag); - - /** - * Set the dag state on the output stream for the current - * stack scope. This makes sure the old state is reset on the - * stream after normal OR exceptional exit from the scope, using the - * RAII C++ idiom. - */ - class Scope { - public: - Scope(std::ostream& out, size_t dag); - ~Scope(); - - private: - std::ostream& d_out; - size_t d_oldDag; - };/* class ExprDag::Scope */ - - private: - /** - * The allocated index in ios_base for our setting. - */ - static const int s_iosIndex; - - /** - * The default setting, for ostreams that haven't yet had a - * dag() applied to them. - */ - static const size_t s_defaultDag = 1; - - /** - * When this manipulator is used, the setting is stored here. - */ - size_t d_dag; -}; /* class ExprDag */ - -/** - * Sets the default dag setting when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::dag(true) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -std::ostream& operator<<(std::ostream& out, ExprDag d); - -/** - * Sets the default depth when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setdepth(n) << e << endl; - * - * The depth stays permanently (until set again) with the stream. - */ -std::ostream& operator<<(std::ostream& out, ExprSetDepth sd); - -} // namespace expr - -} // namespace cvc5 - -#endif /* CVC5__EXPR__EXPR_IOMANIP_H */ diff --git a/src/expr/node.h b/src/expr/node.h index afc648ed8..b3c72c05e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -32,11 +32,10 @@ #include "base/check.h" #include "base/exception.h" #include "base/output.h" -#include "expr/expr_iomanip.h" #include "expr/kind.h" #include "expr/metakind.h" +#include "options/io_utils.h" #include "options/language.h" -#include "options/set_language.h" #include "util/hash.h" #include "util/utility.h" @@ -833,32 +832,6 @@ public: } /** - * IOStream manipulator to set the maximum depth of Nodes when - * pretty-printing. -1 means print to any depth. E.g.: - * - * // let a, b, c, and d be VARIABLEs - * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d))) - * out << setdepth(3) << n; - * - * gives "(OR a b (AND c (NOT d)))", but - * - * out << setdepth(1) << [same node as above] - * - * gives "(OR a b (...))" - */ - typedef expr::ExprSetDepth setdepth; - - /** - * IOStream manipulator to print expressions as DAGs (or not). - */ - typedef expr::ExprDag dag; - - /** - * IOStream manipulator to set the output language for Exprs. - */ - typedef language::SetLanguage setlanguage; - - /** * Very basic pretty printer for Node. * @param out output stream to print to. * @param indent number of spaces to indent the formula by. @@ -893,9 +866,9 @@ public: */ inline std::ostream& operator<<(std::ostream& out, TNode n) { n.toStream(out, - Node::setdepth::getDepth(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); + options::ioutils::getNodeDepth(out), + options::ioutils::getDagThresh(out), + options::ioutils::getOutputLang(out)); return out; } @@ -1438,53 +1411,6 @@ Node NodeTemplate<ref_count>::substitute( } } -#ifdef CVC5_DEBUG -/** - * Pretty printer for use within gdb. This is not intended to be used - * outside of gdb. This writes to the Warning() stream and immediately - * flushes the stream. - * - * Note that this function cannot be a template, since the compiler - * won't instantiate it. Even if we explicitly instantiate. (Odd?) - * So we implement twice. We mark as __attribute__((used)) so that - * GCC emits code for it even though static analysis indicates it's - * never called. - * - * Tim's Note: I moved this into the node.h file because this allows gdb - * to find the symbol, and use it, which is the first standard this code needs - * to meet. A cleaner solution is welcomed. - */ -static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) { - Warning() << Node::setdepth(-1) << Node::dag(true) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) { - Warning() << Node::setdepth(-1) << Node::dag(false) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) { - n.printAst(Warning(), 0); - Warning().flush(); -} - -static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) { - Warning() << Node::setdepth(-1) << Node::dag(true) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) { - Warning() << Node::setdepth(-1) << Node::dag(false) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) { - n.printAst(Warning(), 0); - Warning().flush(); -} -#endif /* CVC5_DEBUG */ - } // namespace cvc5 #endif /* CVC5__NODE_H */ diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 19f66896d..b19417a66 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -508,36 +508,14 @@ inline T NodeValue::iterator<T>::operator*() const { inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { nv.toStream(out, - Node::setdepth::getDepth(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); + options::ioutils::getNodeDepth(out), + options::ioutils::getDagThresh(out), + options::ioutils::getOutputLang(out)); return out; } } // namespace expr -#ifdef CVC5_DEBUG -/** - * Pretty printer for use within gdb. This is not intended to be used - * outside of gdb. This writes to the Warning() stream and immediately - * flushes the stream. - */ -static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { - Warning() << Node::setdepth(-1) << Node::dag(true) - << Node::setlanguage(Language::LANG_AST) << *nv << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) { - Warning() << Node::setdepth(-1) << Node::dag(false) - << Node::setlanguage(Language::LANG_AST) << *nv << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) { - nv->printAst(Warning(), 0); - Warning().flush(); -} -#endif /* CVC5_DEBUG */ - } // namespace cvc5 #endif /* CVC5__EXPR__NODE_VALUE_H */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 8469344db..8dd27c400 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -729,7 +729,7 @@ private: * @return the stream */ inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) { - n.toStream(out, Node::setlanguage::getLanguage(out)); + n.toStream(out, options::ioutils::getOutputLang(out)); return out; } @@ -1005,38 +1005,6 @@ inline unsigned TypeNode::getFloatingPointSignificandSize() const { return getConst<FloatingPointSize>().significandWidth(); } -#ifdef CVC5_DEBUG -/** - * Pretty printer for use within gdb. This is not intended to be used - * outside of gdb. This writes to the Warning() stream and immediately - * flushes the stream. - * - * Note that this function cannot be a template, since the compiler - * won't instantiate it. Even if we explicitly instantiate. (Odd?) - * So we implement twice. We mark as __attribute__((used)) so that - * GCC emits code for it even though static analysis indicates it's - * never called. - * - * Tim's Note: I moved this into the node.h file because this allows gdb - * to find the symbol, and use it, which is the first standard this code needs - * to meet. A cleaner solution is welcomed. - */ -static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { - Warning() << Node::setdepth(-1) << Node::dag(true) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) { - Warning() << Node::setdepth(-1) << Node::dag(false) - << Node::setlanguage(Language::LANG_AST) << n << std::endl; - Warning().flush(); -} -static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { - n.printAst(Warning(), 0); - Warning().flush(); -} -#endif /* CVC5_DEBUG */ - } // namespace cvc5 #endif /* CVC5__NODE_H */ |