From: Gereon Kremer Date: Wed, 27 Oct 2021 23:27:31 +0000 (-0700) Subject: Add documentation on output tags (#7499) X-Git-Tag: cvc5-1.0.0~950 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5ea33ca829d257d408a242974b28bd6defafff6e;p=cvc5.git 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 254354de3..f019594b2 100644 --- 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 d9a847954..f505a7fb4 100644 --- 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 d583c82d7..91e2493e7 100644 --- 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 index 000000000..62aba5c81 --- /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 ` 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 71982b992..f91997646 100644 --- 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 316810ae2..69e0a853b 100644 --- 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 7288ede51..70eb138cc 100644 --- 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('')