From: Gereon Kremer Date: Wed, 1 Jun 2022 03:57:52 +0000 (-0700) Subject: Refactor how options are passed to the printer (#8827) X-Git-Tag: cvc5-1.0.1~81 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=735cbadb137362fbc876fd056ed6ba3a9768caf1;p=cvc5.git Refactor how options are passed to the printer (#8827) 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) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d231276be..71c8d7993 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -46,8 +46,6 @@ libcvc5_add_sources( 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 @@ -1226,8 +1224,8 @@ set(options_toml_files ) 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}) @@ -1270,6 +1268,8 @@ add_custom_command( 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 diff --git a/src/expr/node.h b/src/expr/node.h index eca26c0fa..86d4d740c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -815,12 +815,10 @@ public: * 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 @@ -862,9 +860,7 @@ public: * @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; } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index c197b8c9b..d18971ce9 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -37,21 +37,18 @@ namespace expr { 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 { @@ -94,9 +91,7 @@ NodeValue::iterator > operator+( 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; } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index eb530e10f..0ce8db340 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -228,9 +228,7 @@ class NodeValue 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; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 350ea6968..5a37b3cd0 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -520,7 +520,7 @@ bool TypeNode::isSygusDatatype() const std::string TypeNode::toString() const { std::stringstream ss; - d_nv->toStream(ss, -1, 0); + toStream(ss); return ss.str(); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index db46fc71e..9f3a14507 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -364,9 +364,10 @@ private: * @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); } /** diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 96b2a9655..bcf103535 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -40,22 +40,10 @@ name = "Base" 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" @@ -229,15 +217,6 @@ name = "Base" type = "std::bitset(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" diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index cee50824d..f38dca5d2 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -92,14 +92,6 @@ name = "Bitvector Theory" 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" diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml index cc237c9c3..2da442cd6 100644 --- a/src/options/expr_options.toml +++ b/src/options/expr_options.toml @@ -1,26 +1,6 @@ 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" diff --git a/src/options/io_utils.cpp b/src/options/io_utils.cpp deleted file mode 100644 index cf9a5fc1f..000000000 --- a/src/options/io_utils.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/****************************************************************************** - * 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 -#include - -namespace cvc5::internal::options::ioutils { -namespace { - -template -void setData(std::ios_base& ios, int iosIndex, T value) -{ - constexpr long offset = 1024; - ios.iword(iosIndex) = static_cast(value) + offset; -} -template -T getData(std::ios_base& ios, int iosIndex, T defaultValue) -{ - // There is no good way to figure out whether the value was explicitly set. - // The default value is zero; we shift by some random constant such that - // zero is never a valid value, and we can still use both negative and - // positive values. - constexpr long offset = 1024; - long& l = ios.iword(iosIndex); - if (l == 0) - { - l = static_cast(defaultValue) + offset; - } - return static_cast(l - offset); -} - -} // namespace - -const static int s_iosDagThresh = std::ios_base::xalloc(); -const static int s_iosNodeDepth = std::ios_base::xalloc(); -const static int s_iosOutputLang = std::ios_base::xalloc(); - -static thread_local int64_t s_dagThreshDefault = 1; -static thread_local int64_t s_nodeDepthDefault = -1; -static thread_local Language s_outputLangDefault = Language::LANG_AUTO; - -void setDefaultDagThresh(int64_t value) { s_dagThreshDefault = value; } -void setDefaultNodeDepth(int64_t value) { s_nodeDepthDefault = value; } -void setDefaultOutputLang(Language value) { s_outputLangDefault = value; } - -void applyDagThresh(std::ios_base& ios, int64_t dagThresh) -{ - setData(ios, s_iosDagThresh, dagThresh); -} -void applyNodeDepth(std::ios_base& ios, int64_t nodeDepth) -{ - setData(ios, s_iosNodeDepth, nodeDepth); -} -void applyOutputLang(std::ios_base& ios, Language outputLang) -{ - setData(ios, s_iosOutputLang, outputLang); -} - -void apply(std::ios_base& ios, - int64_t dagThresh, - int64_t nodeDepth, - Language outputLang) -{ - applyDagThresh(ios, dagThresh); - applyNodeDepth(ios, nodeDepth); - applyOutputLang(ios, outputLang); -} - -int64_t getDagThresh(std::ios_base& ios) -{ - return getData(ios, s_iosDagThresh, s_dagThreshDefault); -} -int64_t getNodeDepth(std::ios_base& ios) -{ - return getData(ios, s_iosNodeDepth, s_nodeDepthDefault); -} -Language getOutputLang(std::ios_base& ios) -{ - return getData(ios, s_iosOutputLang, s_outputLangDefault); -} - -Scope::Scope(std::ios_base& ios) - : d_ios(ios), - d_dagThresh(getDagThresh(ios)), - d_nodeDepth(getNodeDepth(ios)), - d_outputLang(getOutputLang(ios)) -{ -} -Scope::~Scope() { apply(d_ios, d_dagThresh, d_nodeDepth, d_outputLang); } - -} // namespace cvc5::internal::options::ioutils diff --git a/src/options/io_utils.h b/src/options/io_utils.h deleted file mode 100644 index 9ea65c11a..000000000 --- a/src/options/io_utils.h +++ /dev/null @@ -1,92 +0,0 @@ -/****************************************************************************** - * 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 - -#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 */ diff --git a/src/options/io_utils_template.cpp b/src/options/io_utils_template.cpp new file mode 100644 index 000000000..e9461cb70 --- /dev/null +++ b/src/options/io_utils_template.cpp @@ -0,0 +1,67 @@ +/****************************************************************************** + * 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 +#include + +#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 +void setData(std::ios_base& ios, int iosIndex, T value) +{ + ios.iword(iosIndex) = static_cast(value) + value_offset; +} +template +T getData(std::ios_base& ios, int iosIndex, T defaultValue) +{ + long& l = ios.iword(iosIndex); + if (l == 0) + { + return defaultValue; + } + return static_cast(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 diff --git a/src/options/io_utils_template.h b/src/options/io_utils_template.h new file mode 100644 index 000000000..b71f1b984 --- /dev/null +++ b/src/options/io_utils_template.h @@ -0,0 +1,70 @@ +/****************************************************************************** + * 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 + +#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 */ diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index b4c1aeed9..70ea64c11 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -77,9 +77,9 @@ def wrap_line(s, indent, **kwargs): 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): @@ -176,11 +176,16 @@ class Option(object): 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) @@ -313,7 +318,7 @@ def _set_handlers(option): 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: @@ -327,6 +332,9 @@ def _set_predicates(option): 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 @@ -342,7 +350,7 @@ def generate_set_impl(modules): 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( @@ -433,11 +441,8 @@ def generate_module_holder_decl(module): 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)) @@ -837,6 +842,51 @@ def generate_sphinx_output_tags(modules, src_dir, build_dir): 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 @@ -876,6 +926,13 @@ def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls): 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), @@ -1046,6 +1103,8 @@ def mkoptions_main(): {'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'}, diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index fd4d5be06..ecb1f250e 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -147,18 +147,17 @@ Languages currently supported as arguments to the --output-lang option: 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) @@ -291,13 +290,6 @@ void OptionsHandler::enableOutputTag(const std::string& flag, 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) { @@ -357,20 +349,6 @@ void OptionsHandler::checkBvSatSolver(const std::string& flag, SatSolverMode m) } } -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); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 14ea289f3..bf20da57e 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -77,10 +77,8 @@ class OptionsHandler /** 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 */ @@ -97,8 +95,6 @@ class OptionsHandler 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); @@ -107,12 +103,6 @@ class OptionsHandler /** 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); diff --git a/src/options/options_public_template.cpp b/src/options/options_public_template.cpp index 11b7b5fb2..670f129e6 100644 --- a/src/options/options_public_template.cpp +++ b/src/options/options_public_template.cpp @@ -15,6 +15,7 @@ #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" diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml index 3aa4e321a..7eb0652ba 100644 --- a/src/options/printer_options.toml +++ b/src/options/printer_options.toml @@ -1,6 +1,35 @@ 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" @@ -24,6 +53,14 @@ name = "Printing" 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" @@ -83,3 +120,19 @@ name = "Printing" [[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" diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml index c014cc310..5d49bfc5f 100644 --- a/src/options/proof_options.toml +++ b/src/options/proof_options.toml @@ -115,11 +115,3 @@ name = "Proof" 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" diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 8048d31c1..eca052ee7 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -21,6 +21,7 @@ #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" @@ -31,11 +32,10 @@ namespace cvc5::internal { 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); @@ -437,7 +437,7 @@ static bool tryToStream(std::ostream& out, const cvc5::Command* c) static void toStream(std::ostream& out, const cvc5::CommandSuccess* s) { - if (cvc5::Command::printsuccess::getPrintSuccess(out)) + if (options::ioutils::getPrintSuccess(out)) { out << "OK" << endl; } diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index a57ed0e7c..f349b1a4b 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -33,10 +33,7 @@ class AstPrinter : public cvc5::internal::Printer { 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; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index fa46350be..ea38b2012 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -19,6 +19,7 @@ #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" @@ -72,13 +73,6 @@ void Printer::toStream(std::ostream& out, const smt::Model& m) const } } -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) { @@ -129,30 +123,12 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const 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(lang)] == nullptr) { diff --git a/src/printer/printer.h b/src/printer/printer.h index f4ad5443d..3bdfd29f0 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -46,13 +46,10 @@ class Printer 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; @@ -314,11 +311,6 @@ class Printer 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. diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ff13b0600..3b154ea93 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -34,10 +34,8 @@ #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" @@ -125,6 +123,13 @@ void Smt2Printer::toStream(std::ostream& out, } } +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, @@ -200,7 +205,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::CONST_BITVECTOR: { const BitVector& bv = n.getConst(); - if (options::bvPrintConstsAsIndexedSymbols()) + if (options::ioutils::getBvPrintConstsAsIndexedSymbols(out)) { out << "(_ bv" << bv.getValue() << " " << bv.getSize() << ")"; } @@ -213,7 +218,7 @@ void Smt2Printer::toStream(std::ostream& out, case kind::CONST_FLOATINGPOINT: { out << n.getConst().toString( - options::bvPrintConstsAsIndexedSymbols()); + options::ioutils::getBvPrintConstsAsIndexedSymbols(out)); break; } case kind::CONST_ROUNDINGMODE: @@ -571,7 +576,7 @@ void Smt2Printer::toStream(std::ostream& out, 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; @@ -1435,20 +1440,18 @@ void Smt2Printer::toStreamModelSort(std::ostream& out, << 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) @@ -2121,7 +2124,7 @@ static void toStream(std::ostream& out, const cvc5::CommandSuccess* s, Variant v) { - if (cvc5::Command::printsuccess::getPrintSuccess(out)) + if (options::ioutils::getPrintSuccess(out)) { out << "success" << endl; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index a65be9a32..0e7712254 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -39,10 +39,8 @@ class Smt2Printer : public cvc5::internal::Printer 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; /** diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 10355ed0a..64a3c721c 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -32,19 +32,18 @@ namespace cvc5::internal { 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 @@ -53,7 +52,11 @@ 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; } diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h index e351a75e3..3d388d555 100644 --- a/src/printer/tptp/tptp_printer.h +++ b/src/printer/tptp/tptp_printer.h @@ -30,10 +30,7 @@ class TptpPrinter : public cvc5::internal::Printer { 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; /** diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp index a19122380..dec582579 100644 --- a/src/proof/dot/dot_printer.cpp +++ b/src/proof/dot/dot_printer.cpp @@ -31,9 +31,7 @@ namespace cvc5::internal { 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"}; @@ -207,7 +205,7 @@ void DotPrinter::print(std::ostream& out, const ProofNode* pn) ancestorHashs, ProofNodeClusterType::NOT_DEFINED); - if (options::printDotClusters()) + if (options::ioutils::getPrintDotClusters(out)) { // Print the sub-graphs for (unsigned i = 0; i < 5; i++) @@ -230,7 +228,7 @@ uint64_t DotPrinter::printInternal( uint64_t currentRuleID = d_ruleID; // Print DAG option enabled - if (options::proofDotDAG()) + if (options::ioutils::getPrintDotAsDAG(out)) { ProofNodeHashFunction hasher; size_t currentHash = hasher(pn); @@ -275,7 +273,7 @@ uint64_t DotPrinter::printInternal( } ProofNodeClusterType proofNodeType = ProofNodeClusterType::NOT_DEFINED; - if (options::printDotClusters()) + if (options::ioutils::getPrintDotClusters(out)) { // Define the type of this node proofNodeType = defineProofNodeType(pn, parentType); @@ -305,7 +303,7 @@ uint64_t DotPrinter::printInternal( ancestorHashs, proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; - if (options::proofDotDAG()) + if (options::ioutils::getPrintDotAsDAG(out)) { ancestorHashs.pop_back(); } @@ -323,7 +321,7 @@ uint64_t DotPrinter::printInternal( ancestorHashs, proofNodeType); out << "\t" << childId << " -> " << currentRuleID << ";\n"; - if (options::proofDotDAG()) + if (options::ioutils::getPrintDotAsDAG(out)) { ancestorHashs.pop_back(); } @@ -331,7 +329,7 @@ uint64_t DotPrinter::printInternal( } // 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(); } diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 738dac6b8..1b2111b3b 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -587,7 +587,7 @@ TypeNode LfscNodeConverter::postConvertType(TypeNode tn) // 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()) { diff --git a/src/proof/lfsc/lfsc_print_channel.cpp b/src/proof/lfsc/lfsc_print_channel.cpp index 8d1fe85d6..679a6a9fc 100644 --- a/src/proof/lfsc/lfsc_print_channel.cpp +++ b/src/proof/lfsc/lfsc_print_channel.cpp @@ -79,8 +79,8 @@ void LfscPrintChannelOut::printNodeInternal(std::ostream& out, Node n) { // 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; @@ -90,7 +90,7 @@ void LfscPrintChannelOut::printTypeNodeInternal(std::ostream& out, TypeNode tn) { // 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); diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index 9b8836962..c03528e0a 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -52,8 +52,7 @@ UnsatCore::const_iterator UnsatCore::end() const { 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) { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index efd7f18ce..52d1f56e4 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -78,17 +78,13 @@ std::string sexprToString(cvc5::Term sexpr) 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; } @@ -107,7 +103,7 @@ ostream& operator<<(ostream& out, const Command* c) std::ostream& operator<<(std::ostream& out, const CommandStatus& s) { - s.toStream(out, options::ioutils::getOutputLang(out)); + s.toStream(out); return out; } @@ -124,31 +120,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s) 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 */ /* -------------------------------------------------------------------------- */ @@ -205,9 +176,9 @@ std::string Command::toString() const 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 @@ -271,12 +242,9 @@ void EmptyCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) 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); } /* -------------------------------------------------------------------------- */ @@ -308,12 +276,9 @@ Command* EchoCommand::clone() const { return new EchoCommand(d_output); } 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); } /* -------------------------------------------------------------------------- */ @@ -340,12 +305,9 @@ Command* AssertCommand::clone() const { return new AssertCommand(d_term); } 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)); } /* -------------------------------------------------------------------------- */ @@ -370,12 +332,9 @@ void PushCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) 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); } /* -------------------------------------------------------------------------- */ @@ -400,12 +359,9 @@ void PopCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) 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); } /* -------------------------------------------------------------------------- */ @@ -453,12 +409,9 @@ Command* CheckSatCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -526,12 +479,9 @@ std::string CheckSatAssumingCommand::getCommandName() const 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)); } @@ -564,12 +514,9 @@ std::string DeclareSygusVarCommand::getCommandName() const 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)); } @@ -621,13 +568,10 @@ std::string SynthFunCommand::getCommandName() const 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 nodeVars = termVectorToNodes(d_vars); - Printer::getPrinter(language)->toStreamCmdSynthFun( + Printer::getPrinter(out)->toStreamCmdSynthFun( out, termToNode(d_fun), nodeVars, @@ -677,19 +621,15 @@ std::string SygusConstraintCommand::getCommandName() const 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)); } } @@ -740,12 +680,9 @@ std::string SygusInvConstraintCommand::getCommandName() const 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]), @@ -787,7 +724,10 @@ void CheckSynthCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) { std::vector 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); @@ -837,18 +777,15 @@ std::string CheckSynthCommand::getCommandName() const 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); } } @@ -873,12 +810,9 @@ void ResetCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) 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); } /* -------------------------------------------------------------------------- */ @@ -909,12 +843,9 @@ std::string ResetAssertionsCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -929,12 +860,9 @@ void QuitCommand::invoke(cvc5::Solver* solver, SymbolManager* sm) 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); } /* -------------------------------------------------------------------------- */ @@ -1027,26 +955,19 @@ CommandSequence::iterator CommandSequence::end() 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); } /* -------------------------------------------------------------------------- */ @@ -1094,12 +1015,9 @@ std::string DeclareFunctionCommand::getCommandName() const 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())); } @@ -1145,12 +1063,9 @@ std::string DeclarePoolCommand::getCommandName() const 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), @@ -1214,12 +1129,9 @@ std::string DeclareOracleFunCommand::getCommandName() const 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); } @@ -1257,13 +1169,9 @@ std::string DeclareSortCommand::getCommandName() const 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)); } /* -------------------------------------------------------------------------- */ @@ -1300,12 +1208,9 @@ Command* DefineSortCommand::clone() const 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)); } @@ -1370,12 +1275,9 @@ std::string DefineFunctionCommand::getCommandName() const 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), @@ -1443,10 +1345,7 @@ std::string DefineFunctionRecCommand::getCommandName() const 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> formals; formals.reserve(d_formals.size()); @@ -1455,7 +1354,7 @@ void DefineFunctionRecCommand::toStream(std::ostream& out, formals.push_back(termVectorToNodes(formal)); } - Printer::getPrinter(language)->toStreamCmdDefineFunctionRec( + Printer::getPrinter(out)->toStreamCmdDefineFunctionRec( out, termVectorToNodes(d_funcs), formals, termVectorToNodes(d_formulas)); } /* -------------------------------------------------------------------------- */ @@ -1484,12 +1383,9 @@ std::string DeclareHeapCommand::getCommandName() const 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)); } @@ -1534,12 +1430,9 @@ Command* SimplifyCommand::clone() const 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)); } /* -------------------------------------------------------------------------- */ @@ -1611,13 +1504,10 @@ Command* GetValueCommand::clone() const 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)); } /* -------------------------------------------------------------------------- */ @@ -1687,12 +1577,9 @@ std::string GetAssignmentCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -1740,12 +1627,9 @@ Command* GetModelCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -1780,12 +1664,9 @@ Command* BlockModelCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -1833,12 +1714,9 @@ std::string BlockModelValuesCommand::getCommandName() const 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)); } @@ -1884,12 +1762,9 @@ Command* GetProofCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -1944,12 +1819,9 @@ std::string GetInstantiationsCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2035,12 +1907,9 @@ std::string GetInterpolantCommand::getCommandName() const 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)); } @@ -2101,12 +1970,9 @@ std::string GetInterpolantNextCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2188,12 +2054,9 @@ Command* GetAbductCommand::clone() const 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)); } @@ -2254,12 +2117,9 @@ std::string GetAbductNextCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2328,12 +2188,9 @@ std::string GetQuantifierEliminationCommand::getCommandName() const 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); } @@ -2389,12 +2246,9 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2467,12 +2321,9 @@ std::string GetUnsatCoreCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2546,12 +2397,9 @@ std::string GetDifficultyCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2612,12 +2460,9 @@ std::string GetLearnedLiteralsCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2668,12 +2513,9 @@ std::string GetAssertionsCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2709,12 +2551,9 @@ std::string SetBenchmarkLogicCommand::getCommandName() const 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); } /* -------------------------------------------------------------------------- */ @@ -2758,12 +2597,9 @@ Command* SetInfoCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -2818,12 +2654,9 @@ Command* GetInfoCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -2866,12 +2699,9 @@ Command* SetOptionCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -2919,12 +2749,9 @@ Command* GetOptionCommand::clone() const 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); } /* -------------------------------------------------------------------------- */ @@ -2964,12 +2791,9 @@ std::string DatatypeDeclarationCommand::getCommandName() const 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)); } diff --git a/src/smt/command.h b/src/smt/command.h index d5801eb4b..6c0cf28e3 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -58,54 +58,6 @@ std::ostream& operator<<(std::ostream&, const Command*) CVC5_EXPORT; 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: @@ -114,9 +66,7 @@ class CVC5_EXPORT CommandStatus 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 */ @@ -185,7 +135,6 @@ class CVC5_EXPORT CommandRecoverableFailure : public CommandStatus class CVC5_EXPORT Command { public: - typedef CommandPrintSuccess printsuccess; Command(); Command(const Command& cmd); @@ -203,11 +152,7 @@ class CVC5_EXPORT Command 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; @@ -299,11 +244,7 @@ class CVC5_EXPORT EmptyCommand : 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; protected: std::string d_name; @@ -323,11 +264,7 @@ class CVC5_EXPORT EchoCommand : 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; protected: std::string d_output; @@ -347,11 +284,7 @@ class CVC5_EXPORT AssertCommand : 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 AssertCommand */ class CVC5_EXPORT PushCommand : public Command @@ -362,11 +295,7 @@ 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; @@ -380,11 +309,7 @@ class CVC5_EXPORT PopCommand : 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; @@ -418,11 +343,7 @@ class CVC5_EXPORT DeclareFunctionCommand : 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 DeclareFunctionCommand */ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand @@ -444,11 +365,7 @@ 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 @@ -465,11 +382,7 @@ 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 */ @@ -495,11 +408,7 @@ class CVC5_EXPORT DeclareSortCommand : 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 DeclareSortCommand */ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand @@ -520,11 +429,7 @@ 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 @@ -545,11 +450,7 @@ 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 */ @@ -582,11 +483,7 @@ class CVC5_EXPORT DefineFunctionRecCommand : 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; protected: /** functions we are defining */ @@ -612,11 +509,7 @@ class CVC5_EXPORT DeclareHeapCommand : 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; protected: /** The location sort */ @@ -638,11 +531,7 @@ class CVC5_EXPORT CheckSatCommand : 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; private: cvc5::Result d_result; @@ -665,11 +554,7 @@ class CVC5_EXPORT CheckSatAssumingCommand : 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; private: std::vector d_terms; @@ -691,11 +576,7 @@ class CVC5_EXPORT QueryCommand : 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 QueryCommand */ /* ------------------- sygus commands ------------------ */ @@ -722,11 +603,7 @@ class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand /** 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 */ @@ -771,11 +648,7 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand /** 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 */ @@ -808,11 +681,7 @@ class CVC5_EXPORT SygusConstraintCommand : public Command /** 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 */ @@ -853,11 +722,7 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command /** 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 @@ -889,11 +754,7 @@ class CVC5_EXPORT CheckSynthCommand : public Command /** 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 */ @@ -922,11 +783,7 @@ class CVC5_EXPORT SimplifyCommand : 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 SimplifyCommand */ class CVC5_EXPORT GetValueCommand : public Command @@ -945,11 +802,7 @@ 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 @@ -965,11 +818,7 @@ 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 @@ -980,11 +829,7 @@ 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 */ @@ -1000,11 +845,7 @@ class CVC5_EXPORT BlockModelCommand : 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: /** The mode to use for blocking. */ @@ -1021,11 +862,7 @@ class CVC5_EXPORT BlockModelValuesCommand : 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; protected: /** The terms we are blocking */ @@ -1043,11 +880,7 @@ class CVC5_EXPORT GetProofCommand : 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; private: /** the result of the getProof call */ @@ -1064,11 +897,7 @@ class CVC5_EXPORT GetInstantiationsCommand : 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: cvc5::Solver* d_solver; @@ -1104,11 +933,7 @@ class CVC5_EXPORT GetInterpolantCommand : 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: /** The name of the interpolation predicate */ @@ -1136,11 +961,7 @@ class CVC5_EXPORT GetInterpolantNextCommand : 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: /** The name of the interpolation predicate */ @@ -1181,11 +1002,7 @@ class CVC5_EXPORT GetAbductCommand : 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: /** The name of the abduction predicate */ @@ -1212,11 +1029,7 @@ class CVC5_EXPORT GetAbductNextCommand : 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: /** The name of the abduction predicate */ @@ -1244,11 +1057,7 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : 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 GetQuantifierEliminationCommand */ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command @@ -1260,11 +1069,7 @@ 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 d_result; @@ -1281,11 +1086,7 @@ class CVC5_EXPORT GetUnsatCoreCommand : 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; protected: /** The solver we were invoked with */ @@ -1307,11 +1108,7 @@ class CVC5_EXPORT GetDifficultyCommand : 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; protected: /** The symbol manager we were invoked with */ @@ -1331,11 +1128,7 @@ class CVC5_EXPORT GetLearnedLiteralsCommand : 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; protected: /** the result of the get learned literals call */ @@ -1355,11 +1148,7 @@ class CVC5_EXPORT GetAssertionsCommand : 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 GetAssertionsCommand */ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command @@ -1374,11 +1163,7 @@ 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 @@ -1396,11 +1181,7 @@ 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 @@ -1419,11 +1200,7 @@ 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 @@ -1441,11 +1218,7 @@ 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 @@ -1464,11 +1237,7 @@ 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 @@ -1484,11 +1253,7 @@ 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 @@ -1498,11 +1263,7 @@ 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 @@ -1512,11 +1273,7 @@ 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 @@ -1526,11 +1283,7 @@ 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 @@ -1564,20 +1317,12 @@ 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 diff --git a/src/smt/env.cpp b/src/smt/env.cpp index c454bfc9c..00a7a959c 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -19,6 +19,7 @@ #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" @@ -132,11 +133,6 @@ ResourceManager* Env::getResourceManager() const 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(tag)]; diff --git a/src/smt/env.h b/src/smt/env.h index a501223b3..260407161 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -136,12 +136,6 @@ class Env /* 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). diff --git a/src/smt/model.cpp b/src/smt/model.cpp index 8715a975a..825617e56 100644 --- a/src/smt/model.cpp +++ b/src/smt/model.cpp @@ -30,8 +30,7 @@ Model::Model(bool isKnownSat, const std::string& inputName) 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; } diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 2d516fd42..1a43213be 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -35,7 +35,7 @@ namespace smt { 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() @@ -69,7 +69,7 @@ std::ostream& operator<<(std::ostream& out, 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() diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 5f3921d45..1266a517a 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -464,7 +464,7 @@ void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as) void ProcessAssertions::dumpAssertionsToStream(std::ostream& os, Assertions& as) { - PrintBenchmark pb(&d_env.getPrinter()); + PrintBenchmark pb(Printer::getPrinter(os)); std::vector 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 diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index 5ef8257cb..059a9fe1d 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -361,10 +361,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) } 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") @@ -1969,8 +1969,6 @@ ResourceManager* SolverEngine::getResourceManager() const return d_env->getResourceManager(); } -const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); } - theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); } } // namespace cvc5::internal diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index ca4d763b0..69d19a1d8 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -858,9 +858,6 @@ class CVC5_EXPORT SolverEngine /** 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(); /** diff --git a/src/theory/quantifiers/instantiation_list.cpp b/src/theory/quantifiers/instantiation_list.cpp index 6d4a7a55b..749b25b3d 100644 --- a/src/theory/quantifiers/instantiation_list.cpp +++ b/src/theory/quantifiers/instantiation_list.cpp @@ -31,15 +31,13 @@ InstantiationVec::InstantiationVec(const std::vector& vec, 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; } diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index 3a49d46a2..8f542a713 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -20,6 +20,7 @@ #include #include "options/quantifiers_options.h" +#include "printer/printer.h" #include "smt/env.h" #include "smt/logic_exception.h" #include "smt/print_benchmark.h" @@ -62,7 +63,7 @@ void QueryGenerator::dumpQuery(Node qy, const Result& r) 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(); } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ee755b550..994aebc89 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -17,6 +17,7 @@ #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" @@ -168,7 +169,7 @@ Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn) { 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 diff --git a/src/util/result.cpp b/src/util/result.cpp index d4a3327c4..90338d6b2 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -142,7 +142,7 @@ ostream& operator<<(ostream& out, enum Result::Status s) } 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; diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 95e5faf6b..bd236e358 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -68,9 +68,8 @@ class TestNodeBlackNode : public TestNode 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 d_slvEngine; @@ -568,7 +567,7 @@ TEST_F(TestNodeBlackNode, toStream) 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()); @@ -648,7 +647,8 @@ TEST_F(TestNodeBlackNode, dagifier) 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 " diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index cddf93ae4..bf22393f5 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -37,7 +37,7 @@ class TestPrinterBlackSmt2 : public TestSmt { 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); } diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index da828a0cb..7349aff5c 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -386,7 +386,6 @@ TEST_F(TestTheoryWhiteArithCoverings, test_cdcac_proof_1) 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 diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index b6405c133..85712b89b 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -73,7 +73,8 @@ class TestUtilBlackBooleanSimplification : public TestNode 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