Right now, the printers expect some options to be passed explicitly and read other options statically from the options object.
This refactors this, using the `ioutils` utility which we already use to store option values in the private storage associated with output streams. In detail, does a couple of things:
- the `mkoptions.py` script now generates the `options/io_utils.*` files to handle all options defined in the `printer` options module
- reading the necessary options from the ostreams is pushed into the printers themselves
- explicit options are removed from (almost) all `toStream()` functions
- a few options are moved to the `printer` options module (making the `printSuccess` utility obsolete)
omt/integer_optimizer.h
omt/omt_optimizer.cpp
omt/omt_optimizer.h
- options/io_utils.cpp
- options/io_utils.h
options/language.cpp
options/language.h
options/managed_streams.cpp
)
string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files})
string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files})
-list(APPEND options_gen_cpp_files "options/options.cpp" "options/options_public.cpp" "main/options.cpp")
-list(APPEND options_gen_h_files "options/options.h")
+list(APPEND options_gen_cpp_files "options/io_utils.cpp" "options/options.cpp" "options/options_public.cpp" "main/options.cpp")
+list(APPEND options_gen_h_files "options/io_utils.h" "options/options.h")
libcvc5_add_sources(GENERATED ${options_gen_cpp_files} ${options_gen_h_files})
options/mkoptions.py
${options_toml_files}
main/options_template.cpp
+ options/io_utils_template.h
+ options/io_utils_template.cpp
options/module_template.h
options/module_template.cpp
options/options_public_template.cpp
* print it fully
* @param language the language in which to output
*/
- inline void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dagThreshold = 1) const
+ inline void toStream(std::ostream& out) const
{
assertTNodeNotExpired();
- d_nv->toStream(out, toDepth, dagThreshold);
+ d_nv->toStream(out);
}
void constToStream(std::ostream& out) const
* @return the stream
*/
inline std::ostream& operator<<(std::ostream& out, TNode n) {
- n.toStream(out,
- options::ioutils::getNodeDepth(out),
- options::ioutils::getDagThresh(out));
+ n.toStream(out);
return out;
}
string NodeValue::toString() const {
stringstream ss;
- toStream(ss, -1, false);
+ toStream(ss);
return ss.str();
}
-void NodeValue::toStream(std::ostream& out,
- int toDepth,
- size_t dag) const
+void NodeValue::toStream(std::ostream& out) const
{
// Ensure that this node value is live for the length of this call.
// It really breaks things badly if we don't have a nonzero ref
// count, even just for printing.
RefCountGuard guard(this);
- auto language = options::ioutils::getOutputLang(out);
- Printer::getPrinter(language)->toStream(out, TNode(this), toDepth, dag);
+ Printer::getPrinter(out)->toStream(out, TNode(this));
}
void NodeValue::printAst(std::ostream& out, int ind) const {
std::ostream& operator<<(std::ostream& out, const NodeValue& nv)
{
- nv.toStream(out,
- options::ioutils::getNodeDepth(out),
- options::ioutils::getDagThresh(out));
+ nv.toStream(out);
return out;
}
std::string toString() const;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1) const;
+ void toStream(std::ostream& out) const;
void printAst(std::ostream& out, int indent = 0) const;
std::string TypeNode::toString() const {
std::stringstream ss;
- d_nv->toStream(ss, -1, 0);
+ toStream(ss);
return ss.str();
}
* @param out the stream to serialize this node to
* @param language the language in which to output
*/
- inline void toStream(std::ostream& out) const
- {
- d_nv->toStream(out, -1, 0);
+ inline void toStream(std::ostream& out) const {
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyDagThresh(out, 0);
+ d_nv->toStream(out);
}
/**
type = "Language"
default = "Language::LANG_AUTO"
handler = "stringToLanguage"
- predicates = ["languageIsNotAST"]
+ predicates = ["setInputLanguage"]
includes = ["options/language.h"]
help = "force input language (default is \"auto\"; see --lang help)"
-[[option]]
- name = "outputLanguage"
- alias = ["output-language"]
- category = "common"
- long = "output-lang=LANG"
- type = "Language"
- default = "Language::LANG_AUTO"
- handler = "stringToLanguage"
- predicates = ["applyOutputLanguage"]
- includes = ["options/language.h"]
- help = "force output language (default is \"auto\"; see --output-lang help)"
-
[[option]]
name = "verbosity"
long = "verbosity=N"
type = "std::bitset<static_cast<size_t>(OutputTag::__MAX_VALUE)+1>"
default = '{}'
-[[option]]
- name = "printSuccess"
- category = "common"
- long = "print-success"
- type = "bool"
- default = "false"
- predicates = ["setPrintSuccess"]
- help = "print the \"success\" output required of SMT-LIBv2"
-
[[option]]
name = "cumulativeMillisecondLimit"
category = "common"
default = "false"
help = "simplify formula via Gaussian Elimination if applicable"
-[[option]]
- name = "bvPrintConstsAsIndexedSymbols"
- category = "regular"
- long = "bv-print-consts-as-indexed-symbols"
- type = "bool"
- default = "false"
- help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
-
[[option]]
name = "bvSolver"
category = "regular"
id = "EXPR"
name = "Expression"
-[[option]]
- name = "defaultExprDepth"
- category = "expert"
- long = "expr-depth=N"
- type = "int64_t"
- default = "-1"
- minimum = "-1"
- predicates = ["setDefaultExprDepth"]
- help = "print exprs to depth N (0 == default, -1 == no limit)"
-
-[[option]]
- name = "defaultDagThresh"
- category = "common"
- long = "dag-thresh=N"
- type = "int64_t"
- default = "1"
- minimum = "0"
- predicates = ["setDefaultDagThresh"]
- help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
-
[[option]]
name = "typeChecking"
category = "expert"
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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::internal::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::internal::options::ioutils
+++ /dev/null
-/******************************************************************************
- * Top contributors (to current version):
- * Gereon Kremer
- *
- * This file is part of the cvc5 project.
- *
- * Copyright (c) 2009-2022 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::internal::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::internal::options::ioutils
-
-#endif /* CVC5__OPTIONS__IO_UTILS_H */
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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 <iomanip>
+#include <iostream>
+
+#include "options/io_utils.h"
+
+namespace cvc5::internal::options::ioutils {
+namespace {
+
+// There is no good way to figure out whether the value behind iword() 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.
+static constexpr long value_offset = 1024;
+
+template <typename T>
+void setData(std::ios_base& ios, int iosIndex, T value)
+{
+ ios.iword(iosIndex) = static_cast<long>(value) + value_offset;
+}
+template <typename T>
+T getData(std::ios_base& ios, int iosIndex, T defaultValue)
+{
+ long& l = ios.iword(iosIndex);
+ if (l == 0)
+ {
+ return defaultValue;
+ }
+ return static_cast<T>(l - value_offset);
+}
+
+} // namespace
+
+// clang-format off
+${ioimpls}$
+// clang-format on
+
+Scope::Scope(std::ios_base& ios)
+ : d_ios(ios),
+// clang-format off
+${ioscope_memberinit}$
+// clang-format on
+{
+}
+
+Scope::~Scope()
+{
+// clang-format off
+${ioscope_restore}$
+// clang-format on
+}
+
+} // namespace cvc5::internal::options::ioutils
--- /dev/null
+/******************************************************************************
+ * Top contributors (to current version):
+ * Gereon Kremer
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2022 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"
+#include "options/printer_options.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::internal::options::ioutils {
+
+// clang-format off
+${iodecls}$
+// clang-format on
+
+/**
+ * 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;
+
+// clang-format off
+${ioscope_members}$
+// clang-format on
+};
+} // namespace cvc5::internal::options::ioutils
+
+#endif /* CVC5__OPTIONS__IO_UTILS_H */
textwrap.wrap(s, width=80 - indent, **kwargs))
-def concat_format(s, objs):
+def concat_format(s, objs, glue='\n'):
"""Helper method to render a string for a list of object"""
- return '\n'.join([s.format(**o.__dict__) for o in objs])
+ return glue.join([s.format(**o.__dict__) for o in objs])
def format_include(include):
self.alternate = True
self.long_name = None
self.long_opt = None
+ if self.name:
+ self.name_capitalized = self.name[0].capitalize() + self.name[1:]
if self.long:
r = self.long.split('=', 1)
self.long_name = r[0]
if len(r) > 1:
self.long_opt = r[1]
+ self.fqdefault = self.default
+ if self.mode and self.type not in self.default:
+ self.fqdefault = '{}::{}'.format(self.type, self.default)
self.names = set()
if self.long_name:
self.names.add(self.long_name)
return 'handlers::handleOption<{}>(name, optionarg)'.format(option.type)
-def _set_predicates(option):
+def _set_predicates(module, option):
"""Render predicate calls for options::set()."""
res = []
if option.minimum:
res += [
'opts.handler().{}(name, value);'.format(x) for x in option.predicates
]
+ if module.id == 'printer':
+ res.append('ioutils::setDefault{}(value);'.format(option.name_capitalized))
+
return res
else:
res.append('if ({}) {{'.format(cond))
res.append(' auto value = {};'.format(_set_handlers(option)))
- for pred in _set_predicates(option):
+ for pred in _set_predicates(module, option):
res.append(' {}'.format(pred))
if option.name:
res.append(' opts.write{module}().{name} = value;'.format(
for option in module.options:
if option.name is None:
continue
- if option.default:
- default = option.default
- if option.mode and option.type not in default:
- default = '{}::{}'.format(option.type, default)
- res.append('{} {} = {};'.format(option.type, option.name, default))
+ if option.fqdefault:
+ res.append('{} {} = {};'.format(option.type, option.name, option.fqdefault))
else:
res.append('{} {};'.format(option.type, option.name))
res.append('bool {}WasSetByUser = false;'.format(option.name))
return '\n'.join(res)
+################################################################################
+# for io_utils.h and io_utils.cpp
+
+
+def __get_printer_options(modules):
+ for mod, opt in all_options(modules):
+ if mod.id == 'printer':
+ yield opt
+
+
+def generate_iodecls(modules):
+ return concat_format(
+ '''
+void setDefault{name_capitalized}({type} value);
+void apply{name_capitalized}(std::ios_base& ios, {type} value);
+{type} get{name_capitalized}(std::ios_base& ios);''',
+ __get_printer_options(modules))
+
+
+def generate_ioimpls(modules):
+ return concat_format(
+ '''
+const static int s_ios{name_capitalized} = std::ios_base::xalloc();
+static thread_local {type} s_{name}Default = {fqdefault};
+void setDefault{name_capitalized}({type} value) {{ s_{name}Default = value; }}
+void apply{name_capitalized}(std::ios_base& ios, {type} value) {{ setData(ios, s_ios{name_capitalized}, value); }}
+{type} get{name_capitalized}(std::ios_base& ios) {{ return getData(ios, s_ios{name_capitalized}, s_{name}Default); }}
+''', __get_printer_options(modules))
+
+
+def generate_ioscope_members(modules):
+ return concat_format(' {type} d_{name};', __get_printer_options(modules))
+
+
+def generate_ioscope_memberinit(modules):
+ return concat_format(' d_{name}(get{name_capitalized}(d_ios))',
+ __get_printer_options(modules),
+ glue=',\n')
+
+
+def generate_ioscope_restore(modules):
+ return concat_format(' apply{name_capitalized}(d_ios, d_{name});',
+ __get_printer_options(modules))
+
+
################################################################################
# main code generation for individual modules
generate_sphinx_output_tags(modules, src_dir, build_dir))
data = {
+ # options/io_utils.h
+ 'ioscope_members': generate_ioscope_members(modules),
+ 'iodecls': generate_iodecls(modules),
+ # options/io_utils.cpp
+ 'ioimpls': generate_ioimpls(modules),
+ 'ioscope_memberinit': generate_ioscope_memberinit(modules),
+ 'ioscope_restore': generate_ioscope_restore(modules),
# options/options.h
'holder_fwd_decls': generate_holder_fwd_decls(modules),
'holder_mem_decls': generate_holder_mem_decls(modules),
{'input': 'options/module_template.cpp'},
]
global_tpls = [
+ {'input': 'options/io_utils_template.h'},
+ {'input': 'options/io_utils_template.cpp'},
{'input': 'options/options_template.h'},
{'input': 'options/options_template.cpp'},
{'input': 'options/options_public_template.cpp'},
Unreachable();
}
-void OptionsHandler::languageIsNotAST(const std::string& flag, Language lang)
+void OptionsHandler::setInputLanguage(const std::string& flag, Language lang)
{
if (lang == Language::LANG_AST)
{
throw OptionException("Language LANG_AST is not allowed for " + flag);
}
-}
-
-void OptionsHandler::applyOutputLanguage(const std::string& flag, Language lang)
-{
- ioutils::setDefaultOutputLang(lang);
- ioutils::applyOutputLang(d_options->base.out, lang);
+ if (!d_options->printer.outputLanguageWasSetByUser)
+ {
+ d_options->writePrinter().outputLanguage = lang;
+ ioutils::setDefaultOutputLanguage(lang);
+ }
}
void OptionsHandler::setVerbosity(const std::string& flag, int value)
d_options->writeBase().outputTagHolder.set(tagid);
}
-void OptionsHandler::setPrintSuccess(const std::string& flag, bool value)
-{
- TraceChannel.getStream() << cvc5::Command::printsuccess(value);
- Warning.getStream() << cvc5::Command::printsuccess(value);
- *d_options->base.out << cvc5::Command::printsuccess(value);
-}
-
void OptionsHandler::setResourceWeight(const std::string& flag,
const std::string& optarg)
{
}
}
-void OptionsHandler::setDefaultExprDepth(const std::string& flag, int64_t depth)
-{
- ioutils::setDefaultNodeDepth(depth);
- ioutils::applyNodeDepth(TraceChannel.getStream(), depth);
- ioutils::applyNodeDepth(Warning.getStream(), depth);
-}
-
-void OptionsHandler::setDefaultDagThresh(const std::string& flag, int64_t dag)
-{
- ioutils::setDefaultDagThresh(dag);
- ioutils::applyDagThresh(TraceChannel.getStream(), dag);
- ioutils::applyDagThresh(Warning.getStream(), dag);
-}
-
static void print_config(const char* str, std::string config)
{
std::string s(str);
/** Convert option value to Language enum */
Language stringToLanguage(const std::string& flag, const std::string& optarg);
- /** Check that lang is not LANG_AST (not allowed as input language) */
- void languageIsNotAST(const std::string& flag, Language lang);
- /** Apply the output language to the default output stream */
- void applyOutputLanguage(const std::string& flag, Language lang);
+ /** Set the input language. Check that lang is not LANG_AST */
+ void setInputLanguage(const std::string& flag, Language lang);
/** Apply verbosity to the different output channels */
void setVerbosity(const std::string& flag, int value);
/** Decrease verbosity and call setVerbosity */
void enableDebugTag(const std::string& flag, const std::string& optarg);
/** Enable a particular output tag */
void enableOutputTag(const std::string& flag, OutputTag optarg);
- /** Apply print success flag to the different output channels */
- void setPrintSuccess(const std::string& flag, bool value);
/** Pass the resource weight specification to the resource manager */
void setResourceWeight(const std::string& flag, const std::string& optarg);
/** Check that the sat solver mode is compatible with other bv options */
void checkBvSatSolver(const std::string& flag, SatSolverMode m);
- /******************************* expr options *******************************/
- /** Set ExprSetDepth on all output streams */
- void setDefaultExprDepth(const std::string& flag, int64_t depth);
- /** Set ExprDag on all output streams */
- void setDefaultDagThresh(const std::string& flag, int64_t dag);
-
/******************************* main options *******************************/
/** Show the solver build configuration and exit */
void showConfiguration(const std::string& flag, bool value);
#include "base/check.h"
#include "base/output.h"
+#include "options/io_utils.h"
#include "options/options.h"
#include "options/options_handler.h"
#include "options/options_listener.h"
id = "PRINTER"
name = "Printing"
+[[option]]
+ name = "outputLanguage"
+ alias = ["output-language"]
+ category = "common"
+ long = "output-lang=LANG"
+ type = "Language"
+ default = "Language::LANG_AUTO"
+ handler = "stringToLanguage"
+ includes = ["options/language.h"]
+ help = "force output language (default is \"auto\"; see --output-lang help)"
+
+[[option]]
+ name = "nodeDepth"
+ category = "expert"
+ long = "expr-depth=N"
+ type = "int64_t"
+ default = "-1"
+ minimum = "-1"
+ help = "print exprs to depth N (0 == default, -1 == no limit)"
+
+[[option]]
+ name = "dagThresh"
+ category = "common"
+ long = "dag-thresh=N"
+ type = "int64_t"
+ default = "1"
+ minimum = "0"
+ help = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
+
[[option]]
name = "printInstMode"
category = "common"
default = "true"
help = "print instantiations for formulas that do not have given identifiers"
+[[option]]
+ name = "printDotAsDAG"
+ category = "expert"
+ long = "proof-dot-dag"
+ type = "bool"
+ default = "false"
+ help = "Indicates if the dot proof will be printed as a DAG or as a tree"
+
[[option]]
name = "printDotClusters"
category = "regular"
[[option.mode.STANDARD]]
name = "sygus-standard"
help = "Print based on SyGuS standard."
+
+[[option]]
+ name = "bvPrintConstsAsIndexedSymbols"
+ category = "regular"
+ long = "bv-print-consts-as-indexed-symbols"
+ type = "bool"
+ default = "false"
+ help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x"
+
+[[option]]
+ name = "printSuccess"
+ category = "common"
+ long = "print-success"
+ type = "bool"
+ default = "false"
+ help = "print the \"success\" output required of SMT-LIBv2"
type = "bool"
default = "false"
help = "Add pivots to Alethe resolution steps"
-
-[[option]]
- name = "proofDotDAG"
- category = "expert"
- long = "proof-dot-dag"
- type = "bool"
- default = "false"
- help = "Indicates if the dot proof will be printed as a DAG or as a tree"
#include "expr/node_manager_attributes.h" // for VarNameAttr
#include "expr/node_visitor.h"
+#include "options/io_utils.h"
#include "options/language.h" // for LANG_AST
#include "printer/let_binding.h"
#include "smt/command.h"
namespace printer {
namespace ast {
-void AstPrinter::toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const
+void AstPrinter::toStream(std::ostream& out, TNode n) const
{
+ size_t dag = options::ioutils::getDagThresh(out);
+ int toDepth = options::ioutils::getNodeDepth(out);
if(dag != 0) {
LetBinding lbind(dag + 1);
toStreamWithLetify(out, n, toDepth, &lbind);
static void toStream(std::ostream& out, const cvc5::CommandSuccess* s)
{
- if (cvc5::Command::printsuccess::getPrintSuccess(out))
+ if (options::ioutils::getPrintSuccess(out))
{
out << "OK" << endl;
}
{
public:
using cvc5::internal::Printer::toStream;
- void toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const override;
+ void toStream(std::ostream& out, TNode n) const override;
void toStream(std::ostream& out, const cvc5::CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
#include "expr/node_manager_attributes.h"
#include "options/base_options.h"
#include "options/language.h"
+#include "options/printer_options.h"
#include "printer/ast/ast_printer.h"
#include "printer/smt2/smt2_printer.h"
#include "printer/tptp/tptp_printer.h"
}
}
-void Printer::toStreamUsing(Language lang,
- std::ostream& out,
- const smt::Model& m) const
-{
- getPrinter(lang)->toStream(out, m);
-}
-
void Printer::toStream(std::ostream& out, const UnsatCore& core) const
{
for(UnsatCore::iterator i = core.begin(); i != core.end(); ++i) {
out << ")" << std::endl;
}
-Printer* Printer::getPrinter(Language lang)
+Printer* Printer::getPrinter(std::ostream& out)
{
+ Language lang = options::ioutils::getOutputLanguage(out);
if (lang == Language::LANG_AUTO)
{
- // Infer the language to use for output.
- //
- // Options can be null in certain circumstances (e.g., when printing
- // the singleton "null" expr. So we guard against segfault
- if (not Options::isCurrentNull())
- {
- if (Options::current().base.outputLanguageWasSetByUser)
- {
- lang = options::outputLanguage();
- }
- if (lang == Language::LANG_AUTO
- && Options::current().base.inputLanguageWasSetByUser)
- {
- lang = options::inputLanguage();
- }
- }
- if (lang == Language::LANG_AUTO)
- {
- lang = Language::LANG_SMTLIB_V2_6; // default
- }
+ lang = Language::LANG_SMTLIB_V2_6; // default
}
if (d_printers[static_cast<size_t>(lang)] == nullptr)
{
virtual ~Printer() {}
/** Get the Printer for a given Language */
- static Printer* getPrinter(Language lang);
+ static Printer* getPrinter(std::ostream& out);
/** Write a Node out to a stream with this Printer. */
- virtual void toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const = 0;
+ virtual void toStream(std::ostream& out, TNode n) const = 0;
/** Write a CommandStatus out to a stream with this Printer. */
virtual void toStream(std::ostream& out, const CommandStatus* s) const = 0;
const Node& n,
const Node& value) const = 0;
- /** write model response to command using another language printer */
- void toStreamUsing(Language lang,
- std::ostream& out,
- const smt::Model& m) const;
-
/**
* Write an error to `out` stating that command `name` is not supported by
* this printer.
#include "expr/node_visitor.h"
#include "expr/sequence.h"
#include "expr/skolem_manager.h"
-#include "options/bv_options.h"
+#include "options/io_utils.h"
#include "options/language.h"
-#include "options/printer_options.h"
-#include "options/smt_options.h"
#include "printer/let_binding.h"
#include "proof/unsat_core.h"
#include "smt/command.h"
}
}
+void Smt2Printer::toStream(std::ostream& out, TNode n) const
+{
+ size_t dag = options::ioutils::getDagThresh(out);
+ int toDepth = options::ioutils::getNodeDepth(out);
+ toStream(out, n, toDepth, dag);
+}
+
void Smt2Printer::toStreamWithLetify(std::ostream& out,
Node n,
int toDepth,
case kind::CONST_BITVECTOR:
{
const BitVector& bv = n.getConst<BitVector>();
- if (options::bvPrintConstsAsIndexedSymbols())
+ if (options::ioutils::getBvPrintConstsAsIndexedSymbols(out))
{
out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")";
}
case kind::CONST_FLOATINGPOINT:
{
out << n.getConst<FloatingPoint>().toString(
- options::bvPrintConstsAsIndexedSymbols());
+ options::ioutils::getBvPrintConstsAsIndexedSymbols(out));
break;
}
case kind::CONST_ROUNDINGMODE:
case kind::APPLY_UF: break;
// higher-order
case kind::HO_APPLY:
- if (!options::flattenHOChains())
+ if (!options::ioutils::getFlattenHOChains(out))
{
out << smtKindString(k, d_variant) << ' ';
break;
<< tn << std::endl;
return;
}
+ auto modelUninterpPrint = options::ioutils::getModelUninterpPrint(out);
// print the cardinality
out << "; cardinality of " << tn << " is " << elements.size() << endl;
- if (options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DeclSortAndFun)
+ if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun)
{
toStreamCmdDeclareType(out, tn);
}
// print the representatives
for (const Node& trn : elements)
{
- if (options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DeclSortAndFun
- || options::modelUninterpPrint()
- == options::ModelUninterpPrintMode::DeclFun)
+ if (modelUninterpPrint == options::ModelUninterpPrintMode::DeclSortAndFun
+ || modelUninterpPrint == options::ModelUninterpPrintMode::DeclFun)
{
out << "(declare-fun ";
if (trn.getKind() == kind::UNINTERPRETED_SORT_VALUE)
const cvc5::CommandSuccess* s,
Variant v)
{
- if (cvc5::Command::printsuccess::getPrintSuccess(out))
+ if (options::ioutils::getPrintSuccess(out))
{
out << "success" << endl;
}
public:
Smt2Printer(Variant variant = no_variant) : d_variant(variant) {}
using cvc5::internal::Printer::toStream;
- void toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const override;
+ void toStream(std::ostream& out, TNode n) const override;
+ void toStream(std::ostream& out, TNode n, int toDepth, size_t dag) const;
void toStream(std::ostream& out, const cvc5::CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
/**
namespace printer {
namespace tptp {
-void TptpPrinter::toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const
+void TptpPrinter::toStream(std::ostream& out, TNode n) const
{
options::ioutils::Scope scope(out);
- options::ioutils::applyOutputLang(out, Language::LANG_SMTLIB_V2_6);
- n.toStream(out, toDepth, dag);
+ options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
+ n.toStream(out);
}/* TptpPrinter::toStream() */
void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const
{
- s->toStream(out, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
+ s->toStream(out);
}/* TptpPrinter::toStream() */
void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const
: "CandidateFiniteModel");
out << "% SZS output start " << statusName << " for " << m.getInputName()
<< endl;
- this->Printer::toStreamUsing(Language::LANG_SMTLIB_V2_6, out, m);
+ {
+ options::ioutils::Scope scope(out);
+ options::ioutils::applyOutputLanguage(out, Language::LANG_SMTLIB_V2_6);
+ getPrinter(out)->toStream(out, m);
+ }
out << "% SZS output end " << statusName << " for " << m.getInputName()
<< endl;
}
{
public:
using cvc5::internal::Printer::toStream;
- void toStream(std::ostream& out,
- TNode n,
- int toDepth,
- size_t dag) const override;
+ void toStream(std::ostream& out, TNode n) const override;
void toStream(std::ostream& out, const CommandStatus* s) const override;
void toStream(std::ostream& out, const smt::Model& m) const override;
/**
namespace proof {
DotPrinter::DotPrinter()
- : d_lbind(options::defaultDagThresh() ? options::defaultDagThresh() + 1
- : 0),
- d_ruleID(0)
+ : d_lbind(options::dagThresh() ? options::dagThresh() + 1 : 0), d_ruleID(0)
{
const std::string acronyms[5] = {"SAT", "CNF", "TL", "PP", "IN"};
const std::string colors[5] = {"purple", "yellow", "green", "brown", "blue"};
ancestorHashs,
ProofNodeClusterType::NOT_DEFINED);
- if (options::printDotClusters())
+ if (options::ioutils::getPrintDotClusters(out))
{
// Print the sub-graphs
for (unsigned i = 0; i < 5; i++)
uint64_t currentRuleID = d_ruleID;
// Print DAG option enabled
- if (options::proofDotDAG())
+ if (options::ioutils::getPrintDotAsDAG(out))
{
ProofNodeHashFunction hasher;
size_t currentHash = hasher(pn);
}
ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED;
- if (options::printDotClusters())
+ if (options::ioutils::getPrintDotClusters(out))
{
// Define the type of this node
proofNodeType = defineProofNodeType(pn, parentType);
ancestorHashs,
proofNodeType);
out << "\t" << childId << " -> " << currentRuleID << ";\n";
- if (options::proofDotDAG())
+ if (options::ioutils::getPrintDotAsDAG(out))
{
ancestorHashs.pop_back();
}
ancestorHashs,
proofNodeType);
out << "\t" << childId << " -> " << currentRuleID << ";\n";
- if (options::proofDotDAG())
+ if (options::ioutils::getPrintDotAsDAG(out))
{
ancestorHashs.pop_back();
}
}
// If it's a scope, then remove from the stack
- if (isSCOPE(r) && options::printDotClusters())
+ if (isSCOPE(r) && options::ioutils::getPrintDotClusters(out))
{
d_scopesArgs.pop_back();
}
// an uninterpreted sort, or an uninstantiatied (maybe parametric) datatype
d_declTypes.insert(tn);
std::stringstream ss;
- options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
tn.toStream(ss);
if (tn.isUninterpretedSortConstructor())
{
{
// due to use of special names in the node converter, we must clean symbols
std::stringstream ss;
- options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
- n.toStream(ss, -1, 0);
+ options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
+ n.toStream(ss);
std::string s = ss.str();
cleanSymbols(s);
out << s;
{
// due to use of special names in the node converter, we must clean symbols
std::stringstream ss;
- options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
tn.toStream(ss);
std::string s = ss.str();
cleanSymbols(s);
void UnsatCore::toStream(std::ostream& out) const {
options::ioutils::Scope scope(out);
options::ioutils::applyDagThresh(out, 0);
- auto language = options::ioutils::getOutputLang(out);
- Printer::getPrinter(language)->toStream(out, *this);
+ Printer::getPrinter(out)->toStream(out, *this);
}
std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
return ss.str();
}
-const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
const CommandInterrupted* CommandInterrupted::s_instance =
new CommandInterrupted();
std::ostream& operator<<(std::ostream& out, const Command& c)
{
- c.toStream(out,
- options::ioutils::getNodeDepth(out),
- options::ioutils::getDagThresh(out),
- options::ioutils::getOutputLang(out));
+ c.toStream(out);
return out;
}
std::ostream& operator<<(std::ostream& out, const CommandStatus& s)
{
- s.toStream(out, options::ioutils::getOutputLang(out));
+ s.toStream(out);
return out;
}
return out;
}
-/* -------------------------------------------------------------------------- */
-/* class CommandPrintSuccess */
-/* -------------------------------------------------------------------------- */
-
-void CommandPrintSuccess::applyPrintSuccess(std::ostream& out)
-{
- out.iword(s_iosIndex) = d_printSuccess;
-}
-
-bool CommandPrintSuccess::getPrintSuccess(std::ostream& out)
-{
- return out.iword(s_iosIndex);
-}
-
-void CommandPrintSuccess::setPrintSuccess(std::ostream& out, bool printSuccess)
-{
- out.iword(s_iosIndex) = printSuccess;
-}
-
-std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
-{
- cps.applyPrintSuccess(out);
- return out;
-}
-
/* -------------------------------------------------------------------------- */
/* class Command */
/* -------------------------------------------------------------------------- */
return ss.str();
}
-void CommandStatus::toStream(std::ostream& out, Language language) const
+void CommandStatus::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStream(out, this);
+ Printer::getPrinter(out)->toStream(out, this);
}
void Command::printResult(std::ostream& out) const
Command* EmptyCommand::clone() const { return new EmptyCommand(d_name); }
std::string EmptyCommand::getCommandName() const { return "empty"; }
-void EmptyCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void EmptyCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
+ Printer::getPrinter(out)->toStreamCmdEmpty(out, d_name);
}
/* -------------------------------------------------------------------------- */
std::string EchoCommand::getCommandName() const { return "echo"; }
-void EchoCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void EchoCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
+ Printer::getPrinter(out)->toStreamCmdEcho(out, d_output);
}
/* -------------------------------------------------------------------------- */
std::string AssertCommand::getCommandName() const { return "assert"; }
-void AssertCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void AssertCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdAssert(out, termToNode(d_term));
+ Printer::getPrinter(out)->toStreamCmdAssert(out, termToNode(d_term));
}
/* -------------------------------------------------------------------------- */
Command* PushCommand::clone() const { return new PushCommand(d_nscopes); }
std::string PushCommand::getCommandName() const { return "push"; }
-void PushCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void PushCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdPush(out, d_nscopes);
+ Printer::getPrinter(out)->toStreamCmdPush(out, d_nscopes);
}
/* -------------------------------------------------------------------------- */
Command* PopCommand::clone() const { return new PopCommand(d_nscopes); }
std::string PopCommand::getCommandName() const { return "pop"; }
-void PopCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void PopCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdPop(out, d_nscopes);
+ Printer::getPrinter(out)->toStreamCmdPop(out, d_nscopes);
}
/* -------------------------------------------------------------------------- */
std::string CheckSatCommand::getCommandName() const { return "check-sat"; }
-void CheckSatCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void CheckSatCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdCheckSat(out);
+ Printer::getPrinter(out)->toStreamCmdCheckSat(out);
}
/* -------------------------------------------------------------------------- */
return "check-sat-assuming";
}
-void CheckSatAssumingCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void CheckSatAssumingCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdCheckSatAssuming(
+ Printer::getPrinter(out)->toStreamCmdCheckSatAssuming(
out, termVectorToNodes(d_terms));
}
return "declare-var";
}
-void DeclareSygusVarCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclareSygusVarCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareVar(
+ Printer::getPrinter(out)->toStreamCmdDeclareVar(
out, termToNode(d_var), sortToTypeNode(d_sort));
}
return d_isInv ? "synth-inv" : "synth-fun";
}
-void SynthFunCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SynthFunCommand::toStream(std::ostream& out) const
{
std::vector<Node> nodeVars = termVectorToNodes(d_vars);
- Printer::getPrinter(language)->toStreamCmdSynthFun(
+ Printer::getPrinter(out)->toStreamCmdSynthFun(
out,
termToNode(d_fun),
nodeVars,
return d_isAssume ? "assume" : "constraint";
}
-void SygusConstraintCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SygusConstraintCommand::toStream(std::ostream& out) const
{
if (d_isAssume)
{
- Printer::getPrinter(language)->toStreamCmdAssume(out, termToNode(d_term));
+ Printer::getPrinter(out)->toStreamCmdAssume(out, termToNode(d_term));
}
else
{
- Printer::getPrinter(language)->toStreamCmdConstraint(out,
- termToNode(d_term));
+ Printer::getPrinter(out)->toStreamCmdConstraint(out, termToNode(d_term));
}
}
return "inv-constraint";
}
-void SygusInvConstraintCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SygusInvConstraintCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdInvConstraint(
+ Printer::getPrinter(out)->toStreamCmdInvConstraint(
out,
termToNode(d_predicates[0]),
termToNode(d_predicates[1]),
{
std::vector<cvc5::Term> synthFuns = sm->getFunctionsToSynthesize();
d_solution << "(" << std::endl;
- Printer* p = Printer::getPrinter(Language::LANG_SYGUS_V2);
+ options::ioutils::Scope scope(d_solution);
+ options::ioutils::applyOutputLanguage(d_solution,
+ Language::LANG_SYGUS_V2);
+ Printer* p = Printer::getPrinter(d_solution);
for (cvc5::Term& f : synthFuns)
{
cvc5::Term sol = solver->getSynthSolution(f);
return d_isNext ? "check-synth-next" : "check-synth";
}
-void CheckSynthCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void CheckSynthCommand::toStream(std::ostream& out) const
{
if (d_isNext)
{
- Printer::getPrinter(language)->toStreamCmdCheckSynthNext(out);
+ Printer::getPrinter(out)->toStreamCmdCheckSynthNext(out);
}
else
{
- Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
+ Printer::getPrinter(out)->toStreamCmdCheckSynth(out);
}
}
Command* ResetCommand::clone() const { return new ResetCommand(); }
std::string ResetCommand::getCommandName() const { return "reset"; }
-void ResetCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void ResetCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdReset(out);
+ Printer::getPrinter(out)->toStreamCmdReset(out);
}
/* -------------------------------------------------------------------------- */
return "reset-assertions";
}
-void ResetAssertionsCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void ResetAssertionsCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
+ Printer::getPrinter(out)->toStreamCmdResetAssertions(out);
}
/* -------------------------------------------------------------------------- */
Command* QuitCommand::clone() const { return new QuitCommand(); }
std::string QuitCommand::getCommandName() const { return "exit"; }
-void QuitCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void QuitCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdQuit(out);
+ Printer::getPrinter(out)->toStreamCmdQuit(out);
}
/* -------------------------------------------------------------------------- */
std::string CommandSequence::getCommandName() const { return "sequence"; }
-void CommandSequence::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void CommandSequence::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
- d_commandSequence);
+ Printer::getPrinter(out)->toStreamCmdCommandSequence(out, d_commandSequence);
}
/* -------------------------------------------------------------------------- */
/* class DeclarationSequence */
/* -------------------------------------------------------------------------- */
-void DeclarationSequence::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclarationSequence::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
- out, d_commandSequence);
+ Printer::getPrinter(out)->toStreamCmdDeclarationSequence(out,
+ d_commandSequence);
}
/* -------------------------------------------------------------------------- */
return "declare-fun";
}
-void DeclareFunctionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclareFunctionCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareFunction(
+ Printer::getPrinter(out)->toStreamCmdDeclareFunction(
out, d_symbol, sortToTypeNode(d_func.getSort()));
}
return "declare-pool";
}
-void DeclarePoolCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclarePoolCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclarePool(
+ Printer::getPrinter(out)->toStreamCmdDeclarePool(
out,
d_func.toString(),
sortToTypeNode(d_sort),
return "declare-oracle-fun";
}
-void DeclareOracleFunCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclareOracleFunCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareOracleFun(
+ Printer::getPrinter(out)->toStreamCmdDeclareOracleFun(
out, d_id, sortToTypeNode(d_sort), d_binName);
}
return "declare-sort";
}
-void DeclareSortCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclareSortCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareType(out,
- sortToTypeNode(d_sort));
+ Printer::getPrinter(out)->toStreamCmdDeclareType(out, sortToTypeNode(d_sort));
}
/* -------------------------------------------------------------------------- */
std::string DefineSortCommand::getCommandName() const { return "define-sort"; }
-void DefineSortCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DefineSortCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDefineType(
+ Printer::getPrinter(out)->toStreamCmdDefineType(
out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort));
}
return "define-fun";
}
-void DefineFunctionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DefineFunctionCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDefineFunction(
+ Printer::getPrinter(out)->toStreamCmdDefineFunction(
out,
d_symbol,
termVectorToNodes(d_formals),
return "define-fun-rec";
}
-void DefineFunctionRecCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DefineFunctionRecCommand::toStream(std::ostream& out) const
{
std::vector<std::vector<Node>> formals;
formals.reserve(d_formals.size());
formals.push_back(termVectorToNodes(formal));
}
- Printer::getPrinter(language)->toStreamCmdDefineFunctionRec(
+ Printer::getPrinter(out)->toStreamCmdDefineFunctionRec(
out, termVectorToNodes(d_funcs), formals, termVectorToNodes(d_formulas));
}
/* -------------------------------------------------------------------------- */
return "declare-heap";
}
-void DeclareHeapCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DeclareHeapCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDeclareHeap(
+ Printer::getPrinter(out)->toStreamCmdDeclareHeap(
out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort));
}
std::string SimplifyCommand::getCommandName() const { return "simplify"; }
-void SimplifyCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SimplifyCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdSimplify(out, termToNode(d_term));
+ Printer::getPrinter(out)->toStreamCmdSimplify(out, termToNode(d_term));
}
/* -------------------------------------------------------------------------- */
std::string GetValueCommand::getCommandName() const { return "get-value"; }
-void GetValueCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetValueCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetValue(
- out, termVectorToNodes(d_terms));
+ Printer::getPrinter(out)->toStreamCmdGetValue(out,
+ termVectorToNodes(d_terms));
}
/* -------------------------------------------------------------------------- */
return "get-assignment";
}
-void GetAssignmentCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetAssignmentCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
+ Printer::getPrinter(out)->toStreamCmdGetAssignment(out);
}
/* -------------------------------------------------------------------------- */
std::string GetModelCommand::getCommandName() const { return "get-model"; }
-void GetModelCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetModelCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetModel(out);
+ Printer::getPrinter(out)->toStreamCmdGetModel(out);
}
/* -------------------------------------------------------------------------- */
std::string BlockModelCommand::getCommandName() const { return "block-model"; }
-void BlockModelCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void BlockModelCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdBlockModel(out, d_mode);
+ Printer::getPrinter(out)->toStreamCmdBlockModel(out, d_mode);
}
/* -------------------------------------------------------------------------- */
return "block-model-values";
}
-void BlockModelValuesCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void BlockModelValuesCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdBlockModelValues(
+ Printer::getPrinter(out)->toStreamCmdBlockModelValues(
out, termVectorToNodes(d_terms));
}
std::string GetProofCommand::getCommandName() const { return "get-proof"; }
-void GetProofCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetProofCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetProof(out);
+ Printer::getPrinter(out)->toStreamCmdGetProof(out);
}
/* -------------------------------------------------------------------------- */
return "get-instantiations";
}
-void GetInstantiationsCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetInstantiationsCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
+ Printer::getPrinter(out)->toStreamCmdGetInstantiations(out);
}
/* -------------------------------------------------------------------------- */
return "get-interpolant";
}
-void GetInterpolantCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetInterpolantCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetInterpol(
+ Printer::getPrinter(out)->toStreamCmdGetInterpol(
out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}
return "get-interpolant-next";
}
-void GetInterpolantNextCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetInterpolantNextCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetInterpolNext(out);
+ Printer::getPrinter(out)->toStreamCmdGetInterpolNext(out);
}
/* -------------------------------------------------------------------------- */
std::string GetAbductCommand::getCommandName() const { return "get-abduct"; }
-void GetAbductCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetAbductCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetAbduct(
+ Printer::getPrinter(out)->toStreamCmdGetAbduct(
out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar));
}
return "get-abduct-next";
}
-void GetAbductNextCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetAbductNextCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetAbductNext(out);
+ Printer::getPrinter(out)->toStreamCmdGetAbductNext(out);
}
/* -------------------------------------------------------------------------- */
return d_doFull ? "get-qe" : "get-qe-disjunct";
}
-void GetQuantifierEliminationCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetQuantifierEliminationCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination(
+ Printer::getPrinter(out)->toStreamCmdGetQuantifierElimination(
out, termToNode(d_term), d_doFull);
}
return "get-unsat-assumptions";
}
-void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetUnsatAssumptionsCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
+ Printer::getPrinter(out)->toStreamCmdGetUnsatAssumptions(out);
}
/* -------------------------------------------------------------------------- */
return "get-unsat-core";
}
-void GetUnsatCoreCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetUnsatCoreCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
+ Printer::getPrinter(out)->toStreamCmdGetUnsatCore(out);
}
/* -------------------------------------------------------------------------- */
return "get-difficulty";
}
-void GetDifficultyCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetDifficultyCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetDifficulty(out);
+ Printer::getPrinter(out)->toStreamCmdGetDifficulty(out);
}
/* -------------------------------------------------------------------------- */
return "get-learned-literals";
}
-void GetLearnedLiteralsCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetLearnedLiteralsCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetLearnedLiterals(out);
+ Printer::getPrinter(out)->toStreamCmdGetLearnedLiterals(out);
}
/* -------------------------------------------------------------------------- */
return "get-assertions";
}
-void GetAssertionsCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetAssertionsCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
+ Printer::getPrinter(out)->toStreamCmdGetAssertions(out);
}
/* -------------------------------------------------------------------------- */
return "set-logic";
}
-void SetBenchmarkLogicCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SetBenchmarkLogicCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
+ Printer::getPrinter(out)->toStreamCmdSetBenchmarkLogic(out, d_logic);
}
/* -------------------------------------------------------------------------- */
std::string SetInfoCommand::getCommandName() const { return "set-info"; }
-void SetInfoCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SetInfoCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value);
+ Printer::getPrinter(out)->toStreamCmdSetInfo(out, d_flag, d_value);
}
/* -------------------------------------------------------------------------- */
std::string GetInfoCommand::getCommandName() const { return "get-info"; }
-void GetInfoCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetInfoCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
+ Printer::getPrinter(out)->toStreamCmdGetInfo(out, d_flag);
}
/* -------------------------------------------------------------------------- */
std::string SetOptionCommand::getCommandName() const { return "set-option"; }
-void SetOptionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void SetOptionCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value);
+ Printer::getPrinter(out)->toStreamCmdSetOption(out, d_flag, d_value);
}
/* -------------------------------------------------------------------------- */
std::string GetOptionCommand::getCommandName() const { return "get-option"; }
-void GetOptionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void GetOptionCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
+ Printer::getPrinter(out)->toStreamCmdGetOption(out, d_flag);
}
/* -------------------------------------------------------------------------- */
return "declare-datatypes";
}
-void DatatypeDeclarationCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- Language language) const
+void DatatypeDeclarationCommand::toStream(std::ostream& out) const
{
- Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
+ Printer::getPrinter(out)->toStreamCmdDatatypeDeclaration(
out, sortVectorToTypeNodes(d_datatypes));
}
std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC5_EXPORT;
std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC5_EXPORT;
-/**
- * IOStream manipulator to print success messages or not.
- *
- * out << Command::printsuccess(false) << CommandSuccess();
- *
- * prints nothing, but
- *
- * out << Command::printsuccess(true) << CommandSuccess();
- *
- * prints a success message (in a manner appropriate for the current
- * output language).
- */
-class CVC5_EXPORT CommandPrintSuccess
-{
- public:
- /** Construct a CommandPrintSuccess with the given setting. */
- CommandPrintSuccess(bool printSuccess) : d_printSuccess(printSuccess) {}
- void applyPrintSuccess(std::ostream& out);
- static bool getPrintSuccess(std::ostream& out);
- static void setPrintSuccess(std::ostream& out, bool printSuccess);
-
- private:
- /** The allocated index in ios_base for our depth setting. */
- static const int s_iosIndex;
-
- /**
- * The default setting, for ostreams that haven't yet had a setdepth()
- * applied to them.
- */
- static const int s_defaultPrintSuccess = false;
-
- /** When this manipulator is used, the setting is stored here. */
- bool d_printSuccess;
-
-}; /* class CommandPrintSuccess */
-
-/**
- * Sets the default print-success setting when pretty-printing an 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,
- CommandPrintSuccess cps) CVC5_EXPORT;
-
class CVC5_EXPORT CommandStatus
{
protected:
public:
virtual ~CommandStatus() {}
- void toStream(
- std::ostream& out,
- internal::Language language = internal::Language::LANG_AUTO) const;
+ void toStream(std::ostream& out) const;
virtual CommandStatus& clone() const = 0;
}; /* class CommandStatus */
class CVC5_EXPORT Command
{
public:
- typedef CommandPrintSuccess printsuccess;
Command();
Command(const Command& cmd);
SymbolManager* sm,
std::ostream& out);
- virtual void toStream(
- std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language = internal::Language::LANG_AUTO) const = 0;
+ virtual void toStream(std::ostream& out) const = 0;
std::string toString() const;
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
std::string d_name;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
std::string d_output;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class AssertCommand */
class CVC5_EXPORT PushCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
uint32_t d_nscopes;
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
uint32_t d_nscopes;
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class DeclareFunctionCommand */
class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class DeclarePoolCommand */
class CVC5_EXPORT DeclareOracleFunCommand : public Command
void invoke(Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The identifier */
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class DeclareSortCommand */
class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class DefineSortCommand */
class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The formal arguments for the function we are defining */
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** functions we are defining */
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The location sort */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
cvc5::Result d_result;
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
std::vector<cvc5::Term> d_terms;
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class QueryCommand */
/* ------------------- sygus commands ------------------ */
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** the declared variable */
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** the function-to-synthesize */
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** the declared constraint */
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** the place holder predicates with which to build the actual constraint
/** returns this command's name */
std::string getCommandName() const override;
/** prints this command */
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** Whether this is a check-synth-next call */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class SimplifyCommand */
class CVC5_EXPORT GetValueCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetValueCommand */
class CVC5_EXPORT GetAssignmentCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetAssignmentCommand */
class CVC5_EXPORT GetModelCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** Result of printing the model */
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
/** The mode to use for blocking. */
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The terms we are blocking */
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
private:
/** the result of the getProof call */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
cvc5::Solver* d_solver;
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The name of the interpolation predicate */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The name of the interpolation predicate */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The name of the abduction predicate */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The name of the abduction predicate */
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetQuantifierEliminationCommand */
class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
std::vector<cvc5::Term> d_result;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The solver we were invoked with */
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** The symbol manager we were invoked with */
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
protected:
/** the result of the get learned literals call */
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetAssertionsCommand */
class CVC5_EXPORT SetBenchmarkLogicCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class SetBenchmarkLogicCommand */
class CVC5_EXPORT SetInfoCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class SetInfoCommand */
class CVC5_EXPORT GetInfoCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetInfoCommand */
class CVC5_EXPORT SetOptionCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class SetOptionCommand */
class CVC5_EXPORT GetOptionCommand : public Command
void printResult(std::ostream& out) const override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class GetOptionCommand */
class CVC5_EXPORT DatatypeDeclarationCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class DatatypeDeclarationCommand */
class CVC5_EXPORT ResetCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class ResetCommand */
class CVC5_EXPORT ResetAssertionsCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class ResetAssertionsCommand */
class CVC5_EXPORT QuitCommand : public Command
void invoke(cvc5::Solver* solver, SymbolManager* sm) override;
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class QuitCommand */
class CVC5_EXPORT CommandSequence : public Command
Command* clone() const override;
std::string getCommandName() const override;
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
}; /* class CommandSequence */
class CVC5_EXPORT DeclarationSequence : public CommandSequence
{
- void toStream(std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- internal::Language language =
- internal::Language::LANG_AUTO) const override;
+ void toStream(std::ostream& out) const override;
};
} // namespace cvc5
#include "context/context.h"
#include "expr/node.h"
#include "options/base_options.h"
+#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/strings_options.h"
return d_resourceManager.get();
}
-const Printer& Env::getPrinter()
-{
- return *Printer::getPrinter(d_options.base.outputLanguage);
-}
-
bool Env::isOutputOn(OutputTag tag) const
{
return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
/* Option helpers---------------------------------------------------------- */
- /**
- * Get the current printer based on the current options
- * @return the current printer
- */
- const Printer& getPrinter();
-
/**
* Check whether the output for the given output tag is enabled. Output tags
* are enabled via the `output` option (or `-o` on the command line).
std::ostream& operator<<(std::ostream& out, const Model& m) {
options::ioutils::Scope scope(out);
options::ioutils::applyDagThresh(out, 0);
- auto language = options::ioutils::getOutputLang(out);
- Printer::getPrinter(language)->toStream(out, m);
+ Printer::getPrinter(out)->toStream(out, m);
return out;
}
std::ostream& operator<<(std::ostream& out, const OptimizationResult& result)
{
// check the output language first
- Language lang = options::ioutils::getOutputLang(out);
+ Language lang = options::ioutils::getOutputLanguage(out);
if (!language::isLangSmt2(lang))
{
Unimplemented()
const OptimizationObjective& objective)
{
// check the output language first
- Language lang = options::ioutils::getOutputLang(out);
+ Language lang = options::ioutils::getOutputLanguage(out);
if (!language::isLangSmt2(lang))
{
Unimplemented()
void ProcessAssertions::dumpAssertionsToStream(std::ostream& os, Assertions& as)
{
- PrintBenchmark pb(&d_env.getPrinter());
+ PrintBenchmark pb(Printer::getPrinter(os));
std::vector<Node> assertions;
// Notice that the following list covers define-fun and define-fun-rec
// from input. The former does not impact the assertions since define-fun are
}
getOptions().writeBase().inputLanguage = Language::LANG_SMTLIB_V2_6;
// also update the output language
- if (!getOptions().base.outputLanguageWasSetByUser)
+ if (!getOptions().printer.outputLanguageWasSetByUser)
{
setOption("output-language", "smtlib2.6");
- getOptions().writeBase().outputLanguageWasSetByUser = false;
+ getOptions().writePrinter().outputLanguageWasSetByUser = false;
}
}
else if (key == "status")
return d_env->getResourceManager();
}
-const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); }
-
theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); }
} // namespace cvc5::internal
/** Get the resource manager of this SMT engine */
ResourceManager* getResourceManager() const;
- /** Get the printer used by this SMT engine */
- const Printer& getPrinter() const;
-
/** Get a pointer to the Rewriter owned by this SolverEngine. */
theory::Rewriter* getRewriter();
/**
void InstantiationList::initialize(Node q) { d_quant = q; }
std::ostream& operator<<(std::ostream& out, const InstantiationList& ilist)
{
- auto language = options::ioutils::getOutputLang(out);
- Printer::getPrinter(language)->toStream(out, ilist);
+ Printer::getPrinter(out)->toStream(out, ilist);
return out;
}
std::ostream& operator<<(std::ostream& out, const SkolemList& skl)
{
- auto language = options::ioutils::getOutputLang(out);
- Printer::getPrinter(language)->toStream(out, skl);
+ Printer::getPrinter(out)->toStream(out, skl);
return out;
}
#include <sstream>
#include "options/quantifiers_options.h"
+#include "printer/printer.h"
#include "smt/env.h"
#include "smt/logic_exception.h"
#include "smt/print_benchmark.h"
std::stringstream fname;
fname << "query" << d_queryCount << ".smt2";
std::ofstream fs(fname.str(), std::ofstream::out);
- smt::PrintBenchmark pb(&d_env.getPrinter());
+ smt::PrintBenchmark pb(Printer::getPrinter(fs));
pb.printBenchmark(fs, d_env.getLogicInfo().getLogicString(), {}, {kqy});
fs.close();
}
#include "expr/skolem_manager.h"
#include "options/base_options.h"
+#include "options/printer_options.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/theory_options.h"
{
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
std::stringstream ss;
- options::ioutils::applyOutputLang(ss, options().base.outputLanguage);
+ options::ioutils::applyOutputLanguage(ss, options().printer.outputLanguage);
ss << "e_" << tn;
Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
}
ostream& operator<<(ostream& out, const Result& r) {
- Language language = options::ioutils::getOutputLang(out);
+ Language language = options::ioutils::getOutputLanguage(out);
switch (language) {
case Language::LANG_SYGUS_V2: r.toStreamSmt2(out); break;
case Language::LANG_TPTP: r.toStreamTptp(out); break;
TestNode::SetUp();
// setup an SMT engine so that options are in scope
Options opts;
- opts.writeBase().outputLanguage = Language::LANG_AST;
- opts.writeBase().outputLanguageWasSetByUser = true;
d_slvEngine.reset(new SolverEngine(d_nodeManager, &opts));
+ d_slvEngine->setOption("output-language", "ast");
}
std::unique_ptr<SolverEngine> d_slvEngine;
ASSERT_EQ(sstr.str(), "(AND w (OR x y) z)");
sstr.str(std::string());
- o.toStream(sstr, -1, 0);
+ o.toStream(sstr);
ASSERT_EQ(sstr.str(), "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
sstr.str(std::string());
OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
std::stringstream sstr;
- options::ioutils::apply(sstr, 0, -1, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyDagThresh(sstr, 0);
+ options::ioutils::applyOutputLanguage(sstr, 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 "
{
std::stringstream ss;
options::ioutils::applyNodeDepth(ss, -1);
- options::ioutils::applyOutputLang(ss, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyOutputLanguage(ss, Language::LANG_SMTLIB_V2_6);
ss << n;
ASSERT_EQ(ss.str(), expected);
}
opts.writeSmt().proofMode = options::ProofMode::FULL;
opts.writeSmt().produceProofs = true;
Env env(NodeManager::currentNM(), &opts);
- opts.handler().setDefaultDagThresh("--dag-thresh", 0);
smt::PfManager pfm(env);
EXPECT_TRUE(env.isTheoryProofProducing());
// register checkers that we need
Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
options::ioutils::applyNodeDepth(std::cout, -1);
- options::ioutils::applyOutputLang(std::cout, Language::LANG_SMTLIB_V2_6);
+ options::ioutils::applyOutputLanguage(std::cout,
+ Language::LANG_SMTLIB_V2_6);
}
// assert equality up to commuting children
projects / cvc5.git / commitdiff