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 <nafur42@gmail.com>

diff --git a/src/base/output.cpp b/src/base/output.cpp
index a4003efd04c2a4307eeec418c81a6dbb79d92021..4ef76a772281cfad3ccdba8becb17c34c41e0fb5 100644 (file)
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -17,27 +17,25 @@
 
 #include <iostream>
 
-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 cc7b621a8e72cf25da882ce860b61dfce3256720..92669318542a03a0257ff55ae9ffbeb1ce638127 100644 (file)
--- 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 64d373509acb7eb88518dcae4347a31beb3a14b4..315a38f10df5928a52215c7ebba88e6afa8104c4 100644 (file)
--- 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<std::string>"
+
+[[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   = ["<bitset>"]
+  type       = "std::bitset<OutputTag__numValues>"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index e2fbd4cf1738a83006df3557233755c21c885e5b..45b1db4d6e05f3cac207f6bc6d66544dbc095f20 100644 (file)
--- 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 07138dce35c4715a80a41b1d1b0a6c8c1d3ec946..6958dcb122b94f3667ea57f90a218f2fdc6124ad 100644 (file)
--- 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<size_t>(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 3b3f80e6cd62fa8dad4e532c453d211e40fd6e04..bf07729ae73e5781e276e6d181c2654ef5164b7a 100644 (file)
--- 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 (file)
index 0000000..e145191
--- /dev/null
+++ b/src/options/outputc.cpp
@@ -0,0 +1,26 @@
+#include "options/outputc.h"
+
+#include <iostream>
+
+namespace cvc5 {
+
+OutputC OutputChannel(&std::cout);
+
+Cvc5ostream OutputC::operator()(const options::OutputTag tag) const
+{
+  if (options::outputTagHolder()[static_cast<size_t>(tag)])
+  {
+    return Cvc5ostream(d_os);
+  }
+  else
+  {
+    return Cvc5ostream();
+  }
+}
+
+bool OutputC::isOn(const options::OutputTag tag) const
+{
+  return options::outputTagHolder()[static_cast<size_t>(tag)];
+}
+
+}  // namespace cvc5

diff --git a/src/options/outputc.h b/src/options/outputc.h
new file mode 100644 (file)
index 0000000..647b891
--- /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 <iostream>
+
+#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 cfb678991257c02c280671931f4048d31583f029..4eb3511996a1d9d120b4a3a872d992328d774831 100644 (file)
--- 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 157f0f64ba16eb22f2790a44d9e122a91c32bed2..17fd089d63b7df8a7362e6cfa1cdc4c855368c2c 100644 (file)
--- 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<const Node, uint32_t>& i : d_instDebugTemp)
     {
-      for (std::pair<const Node, uint32_t>& 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<const Node, uint32_t>& i : d_instDebugTemp)
     {
-      bool req = !options::printInstFull();
-      for (std::pair<const Node, uint32_t>& 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 4e8d7d46d1228d4cfb5cf3da002f5dfa87d1961f..b2b69687c16d5de9b50f630cedc9960bb87e50be 100644 (file)
--- 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<Node>& 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<Node>& 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 aba9c715f2dc70d08bc58a88057b24777d8a3e7b..08b2f7c501b3758709ea0cb23466496f053b540c 100644 (file)
--- 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 b43c9697a58628f967d8b1ec5fc07f97fce43d58..7b943f47931e18dcf165c7f2a8201d5fe06346d0 100644 (file)
--- 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