From c56eaf4423fbf65663a4e03c8a60ed937c99de7d Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Sat, 3 Jul 2021 10:44:30 -0700 Subject: [PATCH] Add output tags -o, --output. (#6826) Output tags are similar to debug/trace tags, but are always enabled (except for muzzled builds) to provide useful information for users. Available output tags can be queried via -o help/--output help and are specified in the base options module via enum values. Co-authored-by: Gereon Kremer --- src/base/output.cpp | 16 +++--- src/options/CMakeLists.txt | 2 + src/options/base_options.toml | 23 +++++++++ src/options/mkoptions.py | 49 +++++++++++-------- src/options/options_handler.cpp | 8 +++ src/options/options_handler.h | 4 ++ src/options/outputc.cpp | 26 ++++++++++ src/options/outputc.h | 38 ++++++++++++++ src/options/quantifiers_options.toml | 18 ------- src/theory/quantifiers/instantiate.cpp | 37 ++++++-------- .../quantifiers/sygus/synth_conjecture.cpp | 11 ++--- test/regress/regress0/sygus/print-debug.sy | 2 +- .../regress1/quantifiers/qid-debug-inst.smt2 | 2 +- 13 files changed, 158 insertions(+), 78 deletions(-) create mode 100644 src/options/outputc.cpp create mode 100644 src/options/outputc.h diff --git a/src/base/output.cpp b/src/base/output.cpp index a4003efd0..4ef76a772 100644 --- a/src/base/output.cpp +++ b/src/base/output.cpp @@ -17,27 +17,25 @@ #include -using namespace std; - namespace cvc5 { /* Definitions of the declared globals from output.h... */ null_streambuf null_sb; -ostream null_os(&null_sb); +std::ostream null_os(&null_sb); NullC nullStream; const std::string Cvc5ostream::s_tab = " "; -const int Cvc5ostream::s_indentIosIndex = ios_base::xalloc(); +const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc(); -DebugC DebugChannel(&cout); -WarningC WarningChannel(&cerr); -MessageC MessageChannel(&cout); +DebugC DebugChannel(&std::cout); +WarningC WarningChannel(&std::cerr); +MessageC MessageChannel(&std::cout); NoticeC NoticeChannel(&null_os); ChatC ChatChannel(&null_os); -TraceC TraceChannel(&cout); -std::ostream DumpOutC::dump_cout(cout.rdbuf());// copy cout stream buffer +TraceC TraceChannel(&std::cout); +std::ostream DumpOutC::dump_cout(std::cout.rdbuf()); // copy cout stream buffer DumpOutC DumpOutChannel(&DumpOutC::dump_cout); } // namespace cvc5 diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index cc7b621a8..926693185 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -31,6 +31,8 @@ libcvc5_add_sources( options_listener.h options_public.cpp options_public.h + outputc.cpp + outputc.h printer_modes.cpp printer_modes.h set_language.cpp diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 64d373509..315a38f10 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -203,3 +203,26 @@ public = true name = "resourceWeightHolder" category = "undocumented" type = "std::vector" + +[[option]] + name = "outputTag" + short = "o" + long = "output=TAG" + type = "OutputTag" + handler = "enableOutputTag" + category = "regular" + help = "Enable output tag." + help_mode = "Output tags." +[[option.mode.INST]] + name = "inst" + help = "print instantiations during solving" +[[option.mode.SYGUS]] + name = "sygus" + help = "print enumerated terms and candidates generated by the sygus solver" + +# Stores then enabled output tags. +[[option]] + name = "outputTagHolder" + category = "undocumented" + includes = [""] + type = "std::bitset" diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index e2fbd4cf1..45b1db4d6 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -129,7 +129,10 @@ TPL_DECL_MODE_ENUM = \ enum class {type} {{ {values} -}};""" +}}; + +static constexpr size_t {type}__numValues = {nvalues}; +""" TPL_DECL_MODE_FUNC = \ """ @@ -506,7 +509,10 @@ def help_mode_format(option): wrapper = textwrap.TextWrapper(width=78, break_on_hyphens=False) text = ['{}'.format(x) for x in wrapper.wrap(option.help_mode)] - text.append('Available modes for --{} are:'.format(option.long.split('=')[0])) + + optname, optvalue = option.long.split('=') + text.append('Available {}s for --{} are:'.format( + optvalue.lower(), optname)) for value, attrib in option.mode.items(): assert len(attrib) == 1 @@ -600,7 +606,8 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): mode_decl.append( TPL_DECL_MODE_ENUM.format( type=option.type, - values=',\n '.join(values))) + values=',\n '.join(values), + nvalues=len(values))) mode_decl.append(TPL_DECL_MODE_FUNC.format(type=option.type)) cases = [TPL_IMPL_MODE_CASE.format( type=option.type, enum=x) for x in values] @@ -730,6 +737,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ sorted(module.options, key=lambda x: x.long if x.long else x.name): assert option.type != 'void' or option.name is None assert option.name or option.short or option.long + mode_handler = option.handler and option.mode argument_req = option.type not in ['bool', 'void'] docgen_option(option, help_common, help_others) @@ -773,7 +781,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='option', value='true')) - elif option.type != 'void' and option.name: + elif option.type != 'void' and option.name and not mode_handler: cases.append( TPL_CALL_ASSIGN.format( module=module.id, @@ -809,7 +817,7 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ name=option.name, option='key', value='optionarg == "true"')) - elif argument_req and option.name: + elif argument_req and option.name and not mode_handler: setoption_handlers.append( TPL_CALL_ASSIGN.format( module=module.id, @@ -896,20 +904,21 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_ # Define handler assign/assignBool - if option.type == 'bool': - custom_handlers.append(TPL_ASSIGN_BOOL.format( - module=module.id, - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) - elif option.short or option.long: - custom_handlers.append(TPL_ASSIGN.format( - module=module.id, - name=option.name, - handler=handler, - predicates='\n'.join(predicates) - )) + if not mode_handler: + if option.type == 'bool': + custom_handlers.append(TPL_ASSIGN_BOOL.format( + module=module.id, + name=option.name, + handler=handler, + predicates='\n'.join(predicates) + )) + elif option.short or option.long: + custom_handlers.append(TPL_ASSIGN.format( + module=module.id, + name=option.name, + handler=handler, + predicates='\n'.join(predicates) + )) # Default option values default = option.default if option.default else '' @@ -1026,8 +1035,6 @@ def parse_module(filename, module): option = Option(attribs) if option.mode and not option.help_mode: perr(filename, 'defines modes but no help_mode', option) - if option.mode and option.handler: - perr(filename, 'defines modes and a handler', option) if option.mode and option.default and \ option.default not in option.mode.keys(): perr(filename, diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 07138dce3..6958dcb12 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -512,6 +512,14 @@ void OptionsHandler::enableDebugTag(const std::string& option, Trace.on(optarg); } +void OptionsHandler::enableOutputTag(const std::string& option, + const std::string& flag, + const std::string& optarg) +{ + d_options->base.outputTagHolder.set( + static_cast(stringToOutputTag(optarg))); +} + OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, const std::string& flag, const std::string& optarg) diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 3b3f80e6c..bf07729ae 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -156,6 +156,10 @@ public: const std::string& flag, const std::string& optarg); + void enableOutputTag(const std::string& option, + const std::string& flag, + const std::string& optarg); + private: /** Pointer to the containing Options object.*/ diff --git a/src/options/outputc.cpp b/src/options/outputc.cpp new file mode 100644 index 000000000..e14519123 --- /dev/null +++ b/src/options/outputc.cpp @@ -0,0 +1,26 @@ +#include "options/outputc.h" + +#include + +namespace cvc5 { + +OutputC OutputChannel(&std::cout); + +Cvc5ostream OutputC::operator()(const options::OutputTag tag) const +{ + if (options::outputTagHolder()[static_cast(tag)]) + { + return Cvc5ostream(d_os); + } + else + { + return Cvc5ostream(); + } +} + +bool OutputC::isOn(const options::OutputTag tag) const +{ + return options::outputTagHolder()[static_cast(tag)]; +} + +} // namespace cvc5 diff --git a/src/options/outputc.h b/src/options/outputc.h new file mode 100644 index 000000000..647b891db --- /dev/null +++ b/src/options/outputc.h @@ -0,0 +1,38 @@ +#include "cvc5_private_library.h" + +#ifndef CVC5__OPTIONS__OUTPUTC_H +#define CVC5__OPTIONS__OUTPUTC_H + +#include + +#include "cvc5_export.h" +#include "base/output.h" +#include "options/base_options.h" + +namespace cvc5 { + +class OutputC +{ + public: + explicit OutputC(std::ostream* os) : d_os(os) {} + + Cvc5ostream operator()(const options::OutputTag tag) const; + + bool isOn(const options::OutputTag tag) const; + + private: + std::ostream* d_os; + +}; /* class OutputC */ + +extern OutputC OutputChannel CVC5_EXPORT; + +#ifdef CVC5_MUZZLE +#define Output ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::OutputChannel +#else /* CVC5_MUZZLE */ +#define Output ::cvc5::OutputChannel +#endif /* CVC5_MUZZLE */ + +} + +#endif /* CVC5__OPTIONS__OUTPUTC_H */ diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cfb678991..4eb351199 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1538,14 +1538,6 @@ name = "Quantifiers" default = "false" help = "compute backwards filtering to compute whether previous solutions are filtered based on later ones" -[[option]] - name = "debugSygus" - category = "regular" - long = "debug-sygus" - type = "bool" - default = "false" - help = "print enumerated terms and candidates generated by the sygus solver (for debugging)" - # CEGQI applied to general quantified formulas [[option]] @@ -1834,16 +1826,6 @@ name = "Quantifiers" default = "true" help = "use store axiom during ho-elim" -### Output options - -[[option]] - name = "debugInst" - category = "regular" - long = "debug-inst" - type = "bool" - default = "false" - help = "print instantiations during solving (for debugging)" - ### SyGuS instantiation options [[option]] diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 157f0f64b..17fd089d6 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -17,6 +17,7 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" +#include "options/outputc.h" #include "options/printer_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -676,33 +677,27 @@ bool Instantiate::isProofEnabled() const { return d_pfInst != nullptr; } void Instantiate::notifyEndRound() { - bool debugInstTrace = Trace.isOn("inst-per-quant-round"); - if (options::debugInst() || debugInstTrace) + // debug information + if (Trace.isOn("inst-per-quant-round")) { - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.base.out; - // debug information - if (debugInstTrace) + for (std::pair& i : d_instDebugTemp) { - for (std::pair& i : d_instDebugTemp) - { - Trace("inst-per-quant-round") - << " * " << i.second << " for " << i.first << std::endl; - } + Trace("inst-per-quant-round") + << " * " << i.second << " for " << i.first << std::endl; } - if (options::debugInst()) + } + if (Output.isOn(options::OutputTag::INST)) + { + bool req = !options::printInstFull(); + for (std::pair& i : d_instDebugTemp) { - bool req = !options::printInstFull(); - for (std::pair& i : d_instDebugTemp) + Node name; + if (!d_qreg.getNameForQuant(i.first, name, req)) { - Node name; - if (!d_qreg.getNameForQuant(i.first, name, req)) - { - continue; - } - out << "(num-instantiations " << name << " " << i.second << ")" - << std::endl; + continue; } + Output(options::OutputTag::INST) << "(num-instantiations " << name << " " + << i.second << ")" << std::endl; } } } diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 4e8d7d46d..b2b69687c 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -20,6 +20,7 @@ #include "expr/skolem_manager.h" #include "options/base_options.h" #include "options/datatypes_options.h" +#include "options/outputc.h" #include "options/quantifiers_options.h" #include "printer/printer.h" #include "smt/logic_exception.h" @@ -384,7 +385,7 @@ bool SynthConjecture::doCheck(std::vector& lems) } } - bool printDebug = options::debugSygus(); + bool printDebug = Output.isOn(options::OutputTag::SYGUS); if (!constructed_cand) { // get the model value of the relevant terms from the master module @@ -454,12 +455,8 @@ bool SynthConjecture::doCheck(std::vector& lems) } } Trace("sygus-engine") << std::endl; - if (printDebug) - { - Options& sopts = smt::currentSmtEngine()->getOptions(); - std::ostream& out = *sopts.base.out; - out << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; - } + Output(options::OutputTag::SYGUS) + << "(sygus-enum" << sygusEnumOut.str() << ")" << std::endl; } Assert(candidate_values.empty()); constructed_cand = d_master->constructCandidates( diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy index aba9c715f..08b2f7c50 100644 --- a/test/regress/regress0/sygus/print-debug.sy +++ b/test/regress/regress0/sygus/print-debug.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --debug-sygus +; COMMAND-LINE: -o sygus ; EXPECT: (sygus-enum 0) ; EXPECT: (sygus-candidate (f 0)) ; EXPECT: (sygus-enum 1) diff --git a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 b/test/regress/regress1/quantifiers/qid-debug-inst.smt2 index b43c9697a..7b943f479 100644 --- a/test/regress/regress1/quantifiers/qid-debug-inst.smt2 +++ b/test/regress/regress1/quantifiers/qid-debug-inst.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --debug-inst --no-check-unsat-cores +; COMMAND-LINE: -o inst --no-check-unsat-cores ; EXPECT: (num-instantiations myQuant1 1) ; EXPECT: (num-instantiations myQuant2 1) ; EXPECT: unsat -- 2.30.2