summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt4
-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
-rw-r--r--src/options/expr_options.toml2
-rw-r--r--src/options/io_utils.cpp105
-rw-r--r--src/options/io_utils.h92
-rw-r--r--src/options/options_handler.cpp24
-rw-r--r--src/options/options_handler.h4
-rw-r--r--src/options/set_language.cpp80
-rw-r--r--src/options/set_language.h95
-rw-r--r--src/parser/smt2/Smt2.g1
-rw-r--r--src/proof/unsat_core.cpp5
-rw-r--r--src/smt/command.cpp19
-rw-r--r--src/smt/model.cpp5
-rw-r--r--src/smt/optimization_solver.cpp5
-rw-r--r--src/smt/set_defaults.cpp1
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/util/result.cpp4
23 files changed, 246 insertions, 652 deletions
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 <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 */
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 <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
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 <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 */
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 <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
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 <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 */
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 <string>
#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&) */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback