This PR consolidates SetLanguage, ExprSetDepth and ExprDag into a single consistent utility. Also, it makes it play more nicely with users setting these options and removes some obsolete code.
omt/omt_optimizer.cpp
omt/omt_optimizer.h
options/decision_weight.h
+ options/io_utils.cpp
+ options/io_utils.h
options/language.cpp
options/language.h
options/managed_streams.cpp
options/options_handler.h
options/options_listener.h
options/options_public.h
- options/set_language.cpp
- options/set_language.h
preprocessing/assertion_pipeline.cpp
preprocessing/assertion_pipeline.h
preprocessing/learned_literal_manager.cpp
emptyset.h
emptybag.cpp
emptybag.h
- expr_iomanip.cpp
- expr_iomanip.h
kind_map.h
match_trie.cpp
match_trie.h
#include "expr/dtype_selector.h"
-#include "options/set_language.h"
-
using namespace cvc5::kind;
namespace cvc5 {
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 */
#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"
kind::metakind::nodeValueConstantToStream(out, d_nv);
}
- /**
- * 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.
*/
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;
}
}
}
-#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 */
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 */
* @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;
}
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 */
category = "regular"
long = "expr-depth=N"
type = "int64_t"
- default = "0"
+ default = "-1"
minimum = "-1"
predicates = ["setDefaultExprDepth"]
help = "print exprs to depth N (0 == default, -1 == no limit)"
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * IO manipulation classes.
+ */
+
+#include "options/io_utils.h"
+
+#include <iomanip>
+#include <iostream>
+
+namespace cvc5::options::ioutils {
+namespace {
+
+template <typename T>
+void setData(std::ios_base& ios, int iosIndex, T value)
+{
+ constexpr long offset = 1024;
+ ios.iword(iosIndex) = static_cast<long>(value) + offset;
+}
+template <typename T>
+T getData(std::ios_base& ios, int iosIndex, T defaultValue)
+{
+ // There is no good way to figure out whether the value was explicitly set.
+ // The default value is zero; we shift by some random constant such that
+ // zero is never a valid value, and we can still use both negative and
+ // positive values.
+ constexpr long offset = 1024;
+ long& l = ios.iword(iosIndex);
+ if (l == 0)
+ {
+ l = static_cast<long>(defaultValue) + offset;
+ }
+ return static_cast<T>(l - offset);
+}
+
+} // namespace
+
+const static int s_iosDagThresh = std::ios_base::xalloc();
+const static int s_iosNodeDepth = std::ios_base::xalloc();
+const static int s_iosOutputLang = std::ios_base::xalloc();
+
+static thread_local int64_t s_dagThreshDefault = 1;
+static thread_local int64_t s_nodeDepthDefault = -1;
+static thread_local Language s_outputLangDefault = Language::LANG_AUTO;
+
+void setDefaultDagThresh(int64_t value) { s_dagThreshDefault = value; }
+void setDefaultNodeDepth(int64_t value) { s_nodeDepthDefault = value; }
+void setDefaultOutputLang(Language value) { s_outputLangDefault = value; }
+
+void applyDagThresh(std::ios_base& ios, int64_t dagThresh)
+{
+ setData(ios, s_iosDagThresh, dagThresh);
+}
+void applyNodeDepth(std::ios_base& ios, int64_t nodeDepth)
+{
+ setData(ios, s_iosNodeDepth, nodeDepth);
+}
+void applyOutputLang(std::ios_base& ios, Language outputLang)
+{
+ setData(ios, s_iosOutputLang, outputLang);
+}
+
+void apply(std::ios_base& ios,
+ int64_t dagThresh,
+ int64_t nodeDepth,
+ Language outputLang)
+{
+ applyDagThresh(ios, dagThresh);
+ applyNodeDepth(ios, nodeDepth);
+ applyOutputLang(ios, outputLang);
+}
+
+int64_t getDagThresh(std::ios_base& ios)
+{
+ return getData(ios, s_iosDagThresh, s_dagThreshDefault);
+}
+int64_t getNodeDepth(std::ios_base& ios)
+{
+ return getData(ios, s_iosNodeDepth, s_nodeDepthDefault);
+}
+Language getOutputLang(std::ios_base& ios)
+{
+ return getData(ios, s_iosOutputLang, s_outputLangDefault);
+}
+
+Scope::Scope(std::ios_base& ios)
+ : d_ios(ios),
+ d_dagThresh(getDagThresh(ios)),
+ d_nodeDepth(getNodeDepth(ios)),
+ d_outputLang(getOutputLang(ios))
+{
+}
+Scope::~Scope() { apply(d_ios, d_dagThresh, d_nodeDepth, d_outputLang); }
+
+} // namespace cvc5::options::ioutils
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * 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.
+ * ****************************************************************************
+ *
+ * IO manipulation classes.
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__OPTIONS__IO_UTILS_H
+#define CVC5__OPTIONS__IO_UTILS_H
+
+#include <iosfwd>
+
+#include "options/language.h"
+
+/**
+ * A collection of utilities to apply options that change how we print objects
+ * (mostly nodes) to streams. The core idea is to attach the options to every
+ * stream via `std::ios_base::iword()`, allowing both persistent options that
+ * are associated to a stream (and thus in place even when the code using it has
+ * no access to options) and options that are different for different output
+ * streams.
+ *
+ * The options should call the appropriate `setDefault*` when an option is set,
+ * which changes the default for streams that have no values set yet.
+ * For any object derived from `std::ios_base` (this includes all standard
+ * streams), `apply*()` will set the given values on the given object while
+ * `get*()` retrieves the specified option.
+ */
+namespace cvc5::options::ioutils {
+/** Set the default dag threshold */
+void setDefaultDagThresh(int64_t value);
+/** Set the default node depth */
+void setDefaultNodeDepth(int64_t value);
+/** Set the default output language */
+void setDefaultOutputLang(Language value);
+
+/** Apply the given dag threshold to the ios object */
+void applyDagThresh(std::ios_base& ios, int64_t dagThresh);
+/** Apply the given node depth to the ios object */
+void applyNodeDepth(std::ios_base& ios, int64_t nodeDepth);
+/** Apply the given output language to the ios object */
+void applyOutputLang(std::ios_base& ios, Language outputLang);
+/** Apply the given values to the ios object */
+void apply(std::ios_base& ios,
+ int64_t dagThresh,
+ int64_t nodeDepth,
+ Language outputLang);
+
+/** Get the dag threshold from the ios object */
+int64_t getDagThresh(std::ios_base& ios);
+/** Get the node depth from the ios object */
+int64_t getNodeDepth(std::ios_base& ios);
+/** Get the output language from the ios object */
+Language getOutputLang(std::ios_base& ios);
+
+/**
+ * A scope to copy and restore the options on an `std::ios_base` object in an
+ * RAII-style fashion.
+ * The options are read from the ios object on construction and restored on
+ * destruction of the scope.
+ */
+class Scope
+{
+ public:
+ /** Copy the options from the ios object */
+ Scope(std::ios_base& ios);
+ /** Copy the options from the ios object */
+ ~Scope();
+
+ private:
+ /** The ios object */
+ std::ios_base& d_ios;
+ /** The stored dag threshold */
+ int64_t d_dagThresh;
+ /** The stored node depth */
+ int64_t d_nodeDepth;
+ /** The stored output language */
+ Language d_outputLang;
+};
+} // namespace cvc5::options::ioutils
+
+#endif /* CVC5__OPTIONS__IO_UTILS_H */
#include "base/exception.h"
#include "base/modal_exception.h"
#include "base/output.h"
-#include "expr/expr_iomanip.h"
#include "lib/strtok_r.h"
#include "options/base_options.h"
#include "options/bv_options.h"
#include "options/decision_options.h"
+#include "options/io_utils.h"
#include "options/language.h"
#include "options/option_exception.h"
-#include "options/set_language.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/command.h"
void OptionsHandler::applyOutputLanguage(const std::string& flag, Language lang)
{
- d_options->base.out << language::SetLanguage(lang);
+ ioutils::setDefaultOutputLang(lang);
+ ioutils::applyOutputLang(d_options->base.out, lang);
}
void OptionsHandler::setVerbosity(const std::string& flag, int value)
}
}
-void OptionsHandler::setDefaultExprDepth(const std::string& flag, int depth)
+void OptionsHandler::setDefaultExprDepth(const std::string& flag, int64_t depth)
{
- Debug.getStream() << expr::ExprSetDepth(depth);
- Trace.getStream() << expr::ExprSetDepth(depth);
- Warning.getStream() << expr::ExprSetDepth(depth);
+ ioutils::setDefaultNodeDepth(depth);
+ ioutils::applyNodeDepth(Debug.getStream(), depth);
+ ioutils::applyNodeDepth(Trace.getStream(), depth);
+ ioutils::applyNodeDepth(Warning.getStream(), depth);
}
-void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag)
+void OptionsHandler::setDefaultDagThresh(const std::string& flag, int64_t dag)
{
- Debug.getStream() << expr::ExprDag(dag);
- Trace.getStream() << expr::ExprDag(dag);
- Warning.getStream() << expr::ExprDag(dag);
+ ioutils::setDefaultDagThresh(dag);
+ ioutils::applyDagThresh(Debug.getStream(), dag);
+ ioutils::applyDagThresh(Trace.getStream(), dag);
+ ioutils::applyDagThresh(Warning.getStream(), dag);
}
static void print_config(const char* str, std::string config)
/******************************* expr options *******************************/
/** Set ExprSetDepth on all output streams */
- void setDefaultExprDepth(const std::string& flag, int depth);
+ void setDefaultExprDepth(const std::string& flag, int64_t depth);
/** Set ExprDag on all output streams */
- void setDefaultDagThresh(const std::string& flag, int dag);
+ void setDefaultDagThresh(const std::string& flag, int64_t dag);
/******************************* main options *******************************/
/** Show the solver build configuration and exit */
+++ /dev/null
-/******************************************************************************
- * 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.
- * ****************************************************************************
- *
- * Definition of input and output languages.
- */
-#include "options/set_language.h"
-
-#include <iosfwd>
-#include <iomanip>
-
-#include "options/base_options.h"
-#include "options/language.h"
-#include "options/options.h"
-
-namespace cvc5 {
-namespace language {
-
-const int SetLanguage::s_iosIndex = std::ios_base::xalloc();
-
-SetLanguage::Scope::Scope(std::ostream& out, Language language)
- : d_out(out), d_oldLanguage(SetLanguage::getLanguage(out))
-{
- SetLanguage::setLanguage(out, language);
-}
-
-SetLanguage::Scope::~Scope(){
- SetLanguage::setLanguage(d_out, d_oldLanguage);
-}
-
-SetLanguage::SetLanguage(Language l) : d_language(l) {}
-
-void SetLanguage::applyLanguage(std::ostream& out) {
- // (offset by one to detect whether default has been set yet)
- out.iword(s_iosIndex) = int(d_language) + 1;
-}
-
-Language SetLanguage::getLanguage(std::ostream& out)
-{
- 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)
- if(not Options::isCurrentNull()) {
- l = static_cast<long>(options::outputLanguage()) + 1;
- }
- if (l <= 0 || l > static_cast<long>(Language::LANG_MAX))
- {
- // 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_defaultOutputLanguage;
- }
- }
- return Language(l - 1);
-}
-
-void SetLanguage::setLanguage(std::ostream& out, Language l)
-{
- // (offset by one to detect whether default has been set yet)
- out.iword(s_iosIndex) = int(l) + 1;
-}
-
-std::ostream& operator<<(std::ostream& out, SetLanguage l) {
- l.applyLanguage(out);
- return out;
-}
-
-} // namespace language
-} // namespace cvc5
+++ /dev/null
-/******************************************************************************
- * 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.
- * ****************************************************************************
- *
- * Definition of input and output languages.
- */
-
-#include "cvc5_public.h"
-
-#ifndef CVC5__OPTIONS__SET_LANGUAGE_H
-#define CVC5__OPTIONS__SET_LANGUAGE_H
-
-#include <iostream>
-
-#include "cvc5_export.h"
-#include "options/language.h"
-
-namespace cvc5 {
-namespace language {
-
-/**
- * IOStream manipulator to set the output language for Exprs.
- */
-class CVC5_EXPORT SetLanguage
-{
- public:
- /**
- * Set a language on the output stream for the current stack scope.
- * This makes sure the old language 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, Language language);
- ~Scope();
- private:
- std::ostream& d_out;
- Language d_oldLanguage;
- };/* class SetLanguage::Scope */
-
- /**
- * Construct a ExprSetLanguage with the given setting.
- */
- SetLanguage(Language l);
-
- void applyLanguage(std::ostream& out);
-
- static Language getLanguage(std::ostream& out);
-
- static void setLanguage(std::ostream& out, Language l);
-
- private:
-
- /**
- * The allocated index in ios_base for our depth setting.
- */
- static const int s_iosIndex;
-
- /**
- * The default language to use, for ostreams that haven't yet had a
- * setlanguage() applied to them and where the current Options
- * information isn't available.
- */
- static const Language s_defaultOutputLanguage = Language::LANG_AUTO;
-
- /**
- * When this manipulator is used, the setting is stored here.
- */
- Language d_language;
-}; /* class SetLanguage */
-
-/**
- * Sets the output language when pretty-printing a Expr to an ostream.
- * This is used like this:
- *
- * // let out be an ostream, e an Expr
- * out << Expr::setlanguage(LANG_SMTLIB_V2_6) << e << endl;
- *
- * The setting stays permanently (until set again) with the stream.
- */
-std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC5_EXPORT;
-
-} // namespace language
-} // namespace cvc5
-
-#endif /* CVC5__OPTIONS__SET_LANGUAGE_H */
#include "api/cpp/cvc5.h"
#include "base/output.h"
-#include "options/set_language.h"
#include "parser/antlr_input.h"
#include "parser/parser.h"
#include "parser/smt2/smt2.h"
#include "proof/unsat_core.h"
#include "base/check.h"
-#include "expr/expr_iomanip.h"
#include "options/base_options.h"
+#include "options/io_utils.h"
#include "printer/printer.h"
#include "smt/solver_engine_scope.h"
}
void UnsatCore::toStream(std::ostream& out) const {
- expr::ExprDag::Scope scope(out, false);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
Printer::getPrinter(options::outputLanguage())->toStream(out, *this);
}
#include "base/check.h"
#include "base/modal_exception.h"
#include "base/output.h"
-#include "expr/expr_iomanip.h"
#include "expr/node.h"
#include "expr/symbol_manager.h"
#include "expr/type_node.h"
+#include "options/io_utils.h"
#include "options/main_options.h"
#include "options/options.h"
#include "options/printer_options.h"
std::ostream& operator<<(std::ostream& out, const Command& c)
{
c.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;
}
std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
{
- s.toStream(out, Node::setlanguage::getLanguage(out));
+ s.toStream(out, options::ioutils::getOutputLang(out));
return out;
}
}
else
{
- expr::ExprDag::Scope scope(out, false);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
out << d_result << endl;
}
}
}
else
{
- expr::ExprDag::Scope scope(out, false);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
if (d_resultStatus)
{
out << "(define-fun " << d_name << " () Bool " << d_result << ")"
}
else
{
- expr::ExprDag::Scope scope(out, false);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
if (d_resultStatus)
{
out << "(define-fun " << d_name << " () Bool " << d_result << ")"
#include "smt/model.h"
-#include "expr/expr_iomanip.h"
#include "options/base_options.h"
+#include "options/io_utils.h"
#include "printer/printer.h"
namespace cvc5 {
}
std::ostream& operator<<(std::ostream& out, const Model& m) {
- expr::ExprDag::Scope scope(out, false);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
Printer::getPrinter(options::outputLanguage())->toStream(out, m);
return out;
}
#include "context/cdlist.h"
#include "omt/omt_optimizer.h"
#include "options/base_options.h"
+#include "options/io_utils.h"
#include "options/language.h"
#include "options/smt_options.h"
#include "smt/assertions.h"
std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
{
// check the output language first
- Language lang = language::SetLanguage::getLanguage(out);
+ Language lang = options::ioutils::getOutputLang(out);
if (!language::isLangSmt2(lang))
{
Unimplemented()
const OptimizationObjective& objective)
{
// check the output language first
- Language lang = language::SetLanguage::getLanguage(out);
+ Language lang = options::ioutils::getOutputLang(out);
if (!language::isLangSmt2(lang))
{
Unimplemented()
#include "options/prop_options.h"
#include "options/quantifiers_options.h"
#include "options/sep_options.h"
-#include "options/set_language.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
#include "options/theory_options.h"
{
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
std::stringstream ss;
- ss << language::SetLanguage(options::outputLanguage());
+ options::ioutils::applyOutputLang(ss, options::outputLanguage());
ss << "e_" << tn;
Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
#include <string>
#include "base/check.h"
-#include "options/set_language.h"
+#include "options/io_utils.h"
using namespace std;
}
ostream& operator<<(ostream& out, const Result& r) {
- r.toStream(out, language::SetLanguage::getLanguage(out));
+ r.toStream(out, options::ioutils::getOutputLang(out));
return out;
} /* operator<<(ostream&, const Result&) */
#include <string>
#include "api/cpp/cvc5.h"
-#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
#include <sstream>
#include "api/cpp/cvc5.h"
-#include "options/set_language.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
int main()
{
- cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
-
std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
solver->setOption("input-language", "smtlib2");
solver->setOption("output-language", "smtlib2");
#include "expr/node_value.h"
#include "expr/skolem_manager.h"
#include "options/base_options.h"
+#include "options/io_utils.h"
#include "options/language.h"
#include "options/options_public.h"
#include "smt/solver_engine.h"
Node o = NodeBuilder() << n << n << kind::XOR;
std::stringstream sstr;
- sstr << Node::dag(false);
+ options::ioutils::applyDagThresh(sstr, 0);
n.toStream(sstr);
ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
sstr.str(std::string());
- sstr << Node::setdepth(0) << n;
+ options::ioutils::applyNodeDepth(sstr, -1);
+ sstr << n;
ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
sstr.str(std::string());
- sstr << Node::setdepth(0) << o;
+ sstr << o;
ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
sstr.str(std::string());
- sstr << Node::setdepth(1) << n;
+ options::ioutils::applyNodeDepth(sstr, 1);
+ sstr << n;
ASSERT_EQ(sstr.str(), "(AND w (OR (...) (...)) z)");
sstr.str(std::string());
- sstr << Node::setdepth(1) << o;
+ sstr << o;
ASSERT_EQ(sstr.str(),
"(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
sstr.str(std::string());
- sstr << Node::setdepth(2) << n;
+ options::ioutils::applyNodeDepth(sstr, 2);
+ sstr << n;
ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
sstr.str(std::string());
- sstr << Node::setdepth(2) << o;
+ sstr << o;
ASSERT_EQ(sstr.str(),
"(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
sstr.str(std::string());
- sstr << Node::setdepth(3) << n;
+ options::ioutils::applyNodeDepth(sstr, 3);
+ sstr << n;
ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
sstr.str(std::string());
- sstr << Node::setdepth(3) << o;
+ sstr << o;
ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
}
OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
std::stringstream sstr;
- sstr << Node::setdepth(-1) << Node::setlanguage(Language::LANG_SMTLIB_V2_6);
- sstr << Node::dag(false) << n; // never dagify
+ options::ioutils::apply(sstr, 0, -1, Language::LANG_SMTLIB_V2_6);
+ sstr << n; // never dagify
ASSERT_EQ(sstr.str(),
"(or (= (f (f (f x))) x) (= (f (f (f x))) y) (= (f x) (g x)) (= x "
"y) (= (f (g x)) (g y)))");
void checkToString(TNode n, const std::string& expected)
{
std::stringstream ss;
- ss << Node::setdepth(-1) << Node::setlanguage(Language::LANG_SMTLIB_V2_6)
- << n;
+ options::ioutils::applyNodeDepth(ss, -1);
+ options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+ ss << n;
ASSERT_EQ(ss.str(), expected);
}
};
#include <set>
#include <vector>
-#include "expr/expr_iomanip.h"
#include "expr/kind.h"
#include "expr/node.h"
+#include "options/io_utils.h"
#include "options/language.h"
-#include "options/set_language.h"
#include "smt_util/boolean_simplification.h"
#include "test_node.h"
// this test is designed for >= 10 removal threshold
Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
- std::cout << expr::ExprSetDepth(-1)
- << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyNodeDepth(std::cout, -1);
+ options::ioutils::applyOutputLang(std::cout, Language::LANG_SMTLIB_V2_6);
}
// assert equality up to commuting children
projects / cvc5.git / commitdiff