From 561b989855693fed2e06101223b46f11f4a8963a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 22 Nov 2021 14:31:31 -0800 Subject: [PATCH] Refactor IO stream manipulators (#7555) 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. --- src/CMakeLists.txt | 4 +- src/expr/CMakeLists.txt | 2 - src/expr/dtype_selector.cpp | 2 - src/expr/expr_iomanip.cpp | 125 ------------- src/expr/expr_iomanip.h | 177 ------------------ src/expr/node.h | 82 +------- src/expr/node_value.h | 28 +-- src/expr/type_node.h | 34 +--- src/options/expr_options.toml | 2 +- src/options/io_utils.cpp | 105 +++++++++++ src/options/io_utils.h | 92 +++++++++ src/options/options_handler.cpp | 24 +-- src/options/options_handler.h | 4 +- src/options/set_language.cpp | 80 -------- src/options/set_language.h | 95 ---------- src/parser/smt2/Smt2.g | 1 - src/proof/unsat_core.cpp | 5 +- src/smt/command.cpp | 19 +- src/smt/model.cpp | 5 +- src/smt/optimization_solver.cpp | 5 +- src/smt/set_defaults.cpp | 1 - src/theory/quantifiers/term_database.cpp | 2 +- src/util/result.cpp | 4 +- test/api/cpp/ouroborous.cpp | 1 - test/api/cpp/smt2_compliance.cpp | 3 - test/unit/node/node_black.cpp | 27 +-- test/unit/printer/smt2_printer_black.cpp | 5 +- .../util/boolean_simplification_black.cpp | 7 +- 28 files changed, 268 insertions(+), 673 deletions(-) delete mode 100644 src/expr/expr_iomanip.cpp delete mode 100644 src/expr/expr_iomanip.h create mode 100644 src/options/io_utils.cpp create mode 100644 src/options/io_utils.h delete mode 100644 src/options/set_language.cpp delete mode 100644 src/options/set_language.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a04ea799d..e7b968ecc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -51,6 +51,8 @@ libcvc5_add_sources( 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 @@ -61,8 +63,6 @@ libcvc5_add_sources( 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 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 -#include - -#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(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(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(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 - -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" @@ -832,32 +831,6 @@ public: 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. @@ -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::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& 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& 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& n) { - n.printAst(Warning(), 0); - Warning().flush(); -} - -static void __attribute__((used)) debugPrintTNode(const NodeTemplate& 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& 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& 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::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().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 */ diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index c95fd3dfc..79bbc9f19 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -6,7 +6,7 @@ name = "Expression" 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)" diff --git a/src/options/io_utils.cpp b/src/options/io_utils.cpp new file mode 100644 index 000000000..5a51e6c3f --- /dev/null +++ b/src/options/io_utils.cpp @@ -0,0 +1,105 @@ +/****************************************************************************** + * 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 +#include + +namespace cvc5::options::ioutils { +namespace { + +template +void setData(std::ios_base& ios, int iosIndex, T value) +{ + constexpr long offset = 1024; + ios.iword(iosIndex) = static_cast(value) + offset; +} +template +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(defaultValue) + offset; + } + return static_cast(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 diff --git a/src/options/io_utils.h b/src/options/io_utils.h new file mode 100644 index 000000000..071c79c36 --- /dev/null +++ b/src/options/io_utils.h @@ -0,0 +1,92 @@ +/****************************************************************************** + * 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 + +#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 */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index aed851e8e..b0a08b359 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -27,14 +27,13 @@ #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" @@ -124,7 +123,8 @@ void OptionsHandler::languageIsNotAST(const std::string& flag, Language lang) 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) @@ -335,18 +335,20 @@ void OptionsHandler::setBitblastAig(const std::string& flag, bool arg) } } -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) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 884298930..475578c91 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -114,9 +114,9 @@ class OptionsHandler /******************************* 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 */ diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp deleted file mode 100644 index 63351ea04..000000000 --- a/src/options/set_language.cpp +++ /dev/null @@ -1,80 +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. - * **************************************************************************** - * - * Definition of input and output languages. - */ -#include "options/set_language.h" - -#include -#include - -#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(options::outputLanguage()) + 1; - } - if (l <= 0 || l > static_cast(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 diff --git a/src/options/set_language.h b/src/options/set_language.h deleted file mode 100644 index ae59a18f5..000000000 --- a/src/options/set_language.h +++ /dev/null @@ -1,95 +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. - * **************************************************************************** - * - * Definition of input and output languages. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__OPTIONS__SET_LANGUAGE_H -#define CVC5__OPTIONS__SET_LANGUAGE_H - -#include - -#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 */ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 211fb4c80..dbc65d90f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -102,7 +102,6 @@ namespace cvc5 { #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" diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index e2e3e85fe..68e0f9a85 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -16,8 +16,8 @@ #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" @@ -50,7 +50,8 @@ UnsatCore::const_iterator UnsatCore::end() const { } 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); } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 283925903..c3ceffc4e 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -26,10 +26,10 @@ #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" @@ -85,9 +85,9 @@ const CommandInterrupted* CommandInterrupted::s_instance = 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; } @@ -106,7 +106,7 @@ ostream& operator<<(ostream& out, const Command* c) 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; } @@ -1593,7 +1593,8 @@ void GetValueCommand::printResult(std::ostream& out) const } else { - expr::ExprDag::Scope scope(out, false); + options::ioutils::Scope scope(out); + options::ioutils::applyDagThresh(out, 0); out << d_result << endl; } } @@ -2014,7 +2015,8 @@ void GetInterpolCommand::printResult(std::ostream& out) const } 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 << ")" @@ -2103,7 +2105,8 @@ void GetAbductCommand::printResult(std::ostream& out) const } 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 << ")" diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 9a195cb51..5c427fa46 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -15,8 +15,8 @@ #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 { @@ -28,7 +28,8 @@ Model::Model(bool isKnownSat, const std::string& inputName) } 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; } diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 30c338d65..77157625a 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -19,6 +19,7 @@ #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" @@ -34,7 +35,7 @@ namespace smt { 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() @@ -68,7 +69,7 @@ std::ostream& operator<<(std::ostream& out, 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() diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 895e41c96..b2fe2b5d6 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -33,7 +33,6 @@ #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" diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0408d27da..b218c3590 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -168,7 +168,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) { 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 diff --git a/src/util/result.cpp b/src/util/result.cpp index 23f38b7ce..f424558be 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -21,7 +21,7 @@ #include #include "base/check.h" -#include "options/set_language.h" +#include "options/io_utils.h" using namespace std; @@ -289,7 +289,7 @@ ostream& operator<<(ostream& out, enum Result::UnknownExplanation e) } 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&) */ diff --git a/test/api/cpp/ouroborous.cpp b/test/api/cpp/ouroborous.cpp index 354e7ee02..4e5b81ce4 100644 --- a/test/api/cpp/ouroborous.cpp +++ b/test/api/cpp/ouroborous.cpp @@ -30,7 +30,6 @@ #include #include "api/cpp/cvc5.h" -#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" diff --git a/test/api/cpp/smt2_compliance.cpp b/test/api/cpp/smt2_compliance.cpp index 2a39b1d0b..8d484e3bc 100644 --- a/test/api/cpp/smt2_compliance.cpp +++ b/test/api/cpp/smt2_compliance.cpp @@ -18,7 +18,6 @@ #include #include "api/cpp/cvc5.h" -#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/command.h" @@ -32,8 +31,6 @@ void testGetInfo(api::Solver* solver, const char* s); int main() { - cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6); - std::unique_ptr solver = std::make_unique(); solver->setOption("input-language", "smtlib2"); solver->setOption("output-language", "smtlib2"); diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 50e766e61..71ce2d3e8 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -28,6 +28,7 @@ #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" @@ -562,7 +563,7 @@ TEST_F(TestNodeBlackNode, toStream) 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)"); @@ -579,37 +580,41 @@ TEST_F(TestNodeBlackNode, toStream) 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))"); } @@ -643,8 +648,8 @@ TEST_F(TestNodeBlackNode, dagifier) 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)))"); diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index 66304ec01..015875cc7 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -36,8 +36,9 @@ class TestPrinterBlackSmt2 : public TestSmt 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); } }; diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 3269e9bf2..bbb4b5840 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -17,11 +17,10 @@ #include #include -#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" @@ -71,8 +70,8 @@ class TestUtilBlackBooleanSimplification : public TestNode // 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 -- 2.30.2