summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/CMakeLists.txt2
-rw-r--r--src/expr/dtype_selector.cpp2
-rw-r--r--src/expr/expr_iomanip.cpp125
-rw-r--r--src/expr/expr_iomanip.h177
-rw-r--r--src/expr/node.h82
-rw-r--r--src/expr/node_value.h28
-rw-r--r--src/expr/type_node.h34
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback