Add documentation on output tags (#7499)

This PR adds documentation on how users can use -o. After some offline discussion, we decided it makes sense to generate them automatically in mkoptions.py and also include example outputs.

diff --git a/.github/actions/install-dependencies/action.yml b/.github/actions/install-dependencies/action.yml
index 254354de3f974ac23d548f9ab127aa93b4305c09..f019594b28d65292719afabc774df2dcd53ef229 100644 (file)
--- a/.github/actions/install-dependencies/action.yml
+++ b/.github/actions/install-dependencies/action.yml
@@ -75,4 +75,5 @@ runs:
         if [[ "${{ inputs.with-documentation }}" != "true" ]]; then exit 0; fi
         sudo apt-get install -y doxygen python3-docutils python3-jinja2
         python3 -m pip install \
-          sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe
+          sphinxcontrib-bibtex sphinx-tabs sphinx-rtd-theme breathe \
+          sphinxcontrib-programoutput

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index d9a847954edc6fbdd0232d173c18c2aebfdd8f08..f505a7fb486c4e3fda9eec808cc50427204f676e 100644 (file)
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -26,7 +26,7 @@ configure_file(conf.py.in ${CMAKE_CURRENT_BINARY_DIR}/conf.py)
 
 add_custom_target(
   docs
-  DEPENDS docs-cpp docs-java docs-python gen-options
+  DEPENDS docs-cpp docs-java docs-python gen-options cvc5-bin
   COMMAND
     ${SPHINX_EXECUTABLE} -v -b html -c ${CMAKE_CURRENT_BINARY_DIR}
     # Tell Breathe where to find the Doxygen output

diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst
index d583c82d771d163d44b7dbd3d4e59891adbcfd3a..91e2493e79c6df81c58648895d9406806f8c4dbf 100644 (file)
--- a/docs/binary/binary.rst
+++ b/docs/binary/binary.rst
@@ -7,4 +7,5 @@ Binary Documentation
     :maxdepth: 2
 
     quickstart
-    options
\ No newline at end of file
+    options
+    output-tags

diff --git a/docs/binary/output-tags.rst b/docs/binary/output-tags.rst
new file mode 100644 (file)
index 0000000..62aba5c
--- /dev/null
+++ b/docs/binary/output-tags.rst
@@ -0,0 +1,10 @@
+Output tags
+===========
+
+cvc5 supports printing information about certain aspects of the solving process
+that is intended for regular users. These can be enabled using the
+:ref:`-o <lbl-option-output>` command line flag.
+
+As of now, the following output tags are supported:
+
+.. include-build-file:: output_tags_generated.rst

diff --git a/docs/conf.py.in b/docs/conf.py.in
index 71982b992dc563f4cf743c7315717ed1914bbd9c..f919976464acf363f40662486e5d31de58a9e6ef 100644 (file)
--- a/docs/conf.py.in
+++ b/docs/conf.py.in
@@ -42,6 +42,7 @@ extensions = [
         'sphinx.ext.autodoc',
         'sphinx.ext.autosectionlabel',
         'sphinxcontrib.bibtex',
+        'sphinxcontrib.programoutput',
         'sphinx_tabs.tabs',
         'examples',
         'include_build_file',

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 316810ae240d7b49b19ad5904d4518b7f2b46a29..69e0a853be0598fde7bf3147438d67b538e027c4 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -162,15 +162,23 @@ name   = "Base"
 [[option.mode.INST]]
   name = "inst"
   help = "print instantiations during solving"
+  description = "With ``-o inst``, cvc5 prints information about quantifier instantions for individual quantifers."
+  example-file = "regress1/quantifiers/qid-debug-inst.smt2"
 [[option.mode.SYGUS]]
   name = "sygus"
   help = "print enumerated terms and candidates generated by the sygus solver"
+  description = "With ``-o sygus``, cvc5 prints information about the internal SyGuS solver including enumerated terms and generated candidates."
+  example-file = "regress0/sygus/print-debug.sy"
 [[option.mode.TRIGGER]]
   name = "trigger"
   help = "print selected triggers for quantified formulas"
+  description = "With ``-o trigger``, cvc5 prints the selected triggers when solving a quantified formula."
+  example-file = "regress1/quantifiers/qid-debug-inst.smt2"
 [[option.mode.RAW_BENCHMARK]]
   name = "raw-benchmark"
   help = "print the benchmark back on the output verbatim as it is processed"
+  description = "With ``-o raw_benchmark``, cvc5 prints the benchmark back just as it has been parsed."
+  example-file = "regress0/datatypes/datatype-dump.cvc.smt2"
 
 # Stores then enabled output tags.
 [[option]]

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index 7288ede51b790a24ceb74f81cc5f69e8366a1248..70eb138cc7cb5ba0d5c7d51a78294031623fed0d 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -816,6 +816,38 @@ def generate_sphinx_help(modules):
     return '\n'.join(res)
 
 
+################################################################################
+# sphinx documentation for --output @ docs/output_tags_generated.rst
+
+
+def generate_sphinx_output_tags(modules, src_dir, build_dir):
+    """Render help for the --output option for sphinx."""
+    base = next(filter(lambda m: m.id == 'base', modules))
+    opt = next(filter(lambda o: o.name == 'outputTag', base.options))
+
+    # The programoutput extension has weird semantics about the cwd:
+    # https://sphinxcontrib-programoutput.readthedocs.io/en/latest/#usage
+    cwd = '/' + os.path.relpath(build_dir, src_dir)
+
+    res = []
+    for name,info in opt.mode.items():
+        info = info[0]
+        if 'description' not in info:
+            continue
+        res.append('{} (``-o {}``)'.format(name, info['name']))
+        res.append('~' * len(res[-1]))
+        res.append('')
+        res.append(info['description'])
+        if 'example-file' in info:
+            res.append('')
+            res.append('.. command-output:: bin/cvc5 -o {} ../test/regress/{}'.format(info['name'], info['example-file']))
+            res.append('  :cwd: {}'.format(cwd))
+        res.append('')
+        res.append('')
+
+    return '\n'.join(res)
+
+
 ################################################################################
 # main code generation for individual modules
 
@@ -843,7 +875,7 @@ def codegen_module(module, dst_dir, tpls):
 # main code generation
 
 
-def codegen_all_modules(modules, build_dir, dst_dir, tpls):
+def codegen_all_modules(modules, src_dir, build_dir, dst_dir, tpls):
     """Generate code for all option modules."""
     short, cmdline_opts, parseinternal = generate_parsing(modules)
     help_common, help_others = generate_cli_help(modules)
@@ -851,6 +883,8 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpls):
     if os.path.isdir('{}/docs/'.format(build_dir)):
         write_file('{}/docs/'.format(build_dir), 'options_generated.rst',
                    generate_sphinx_help(modules))
+        write_file('{}/docs/'.format(build_dir), 'output_tags_generated.rst',
+                   generate_sphinx_output_tags(modules, src_dir, build_dir))
 
     data = {
         # options/options.h
@@ -1045,7 +1079,7 @@ def mkoptions_main():
     # Generate code
     for module in modules:
         codegen_module(module, dst_dir, module_tpls)
-    codegen_all_modules(modules, build_dir, dst_dir, global_tpls)
+    codegen_all_modules(modules, src_dir, build_dir, dst_dir, global_tpls)
 
     # Generate output file to signal cmake when this script was run last
     open(os.path.join(dst_dir, 'options/options.stamp'), 'w').write('')