From: Gereon Kremer Date: Mon, 21 Mar 2022 21:19:11 +0000 (+0100) Subject: Refactor documentation (#8288) X-Git-Tag: cvc5-1.0.0~219 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b08ef33d5ab27471fd26e53b9a8b2d1833424f55;p=cvc5.git Refactor documentation (#8288) This PR moves some stuff around in our documentation. Most notably, it moves some sections out of the "Binary documentation" to become their own top-level sections. While doing so, it refactors a few things in options and statistics to be more agnostic to the way cvc5 is used. To allow for command-output being used in regular (not auto-generated) documentation, we add a new extension that takes care of injecting the build folder into a new wrapper run-command. --- diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index fe868c879..f51160bcb 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -3,8 +3,14 @@ Binary Documentation The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line. The :doc:`quickstart guide ` gives a short introduction on how to use cvc5 via the SMT-LIBv2 -interface, but cvc5 also supports other :doc:`input languages `. -The behavior of cvc5 can be changed with a number of :doc:`options `, and :doc:`output tags ` allow to extract structured information about the solving process. +interface. + +The cvc5 binary supports the following input languages: + +* `SMT-LIB v2 `_ +* `SyGuS-IF `_ +* `TPTP `_ + Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages. @@ -13,8 +19,3 @@ Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different prog :maxdepth: 2 quickstart - languages - options - output-tags - resource-limits - statistics diff --git a/docs/binary/languages.rst b/docs/binary/languages.rst deleted file mode 100644 index 34c536017..000000000 --- a/docs/binary/languages.rst +++ /dev/null @@ -1,8 +0,0 @@ -Input Languages -=============== - -cvc5 supports the following input languages: - -* `SMT-LIB v2 `_ -* `SyGuS-IF `_ -* `TPTP `_ diff --git a/docs/binary/options.rst b/docs/binary/options.rst deleted file mode 100644 index d301c7045..000000000 --- a/docs/binary/options.rst +++ /dev/null @@ -1,7 +0,0 @@ -Commandline Options -=================== - -Below is an exhaustive list of commandline options supported by cvc5. - -.. include-build-file:: options_generated.rst - diff --git a/docs/binary/output-tags.rst b/docs/binary/output-tags.rst deleted file mode 100644 index 62aba5c81..000000000 --- a/docs/binary/output-tags.rst +++ /dev/null @@ -1,10 +0,0 @@ -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/binary/resource-limits.rst b/docs/binary/resource-limits.rst deleted file mode 100644 index f9fe06b5a..000000000 --- a/docs/binary/resource-limits.rst +++ /dev/null @@ -1,38 +0,0 @@ -Resource limits -=============== - -cvc5 supports limiting the time or *resources* it uses during solving via the options -:ref:`tlimit `, :ref:`tlimit-per `, -:ref:`rlimit `, and :ref:`rlimit-per `. -All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of *resources*. - -The limits configured using :ref:`tlimit ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. -In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`checkEntailed `, etc). - -Except for the overall time limit (see below), the limits are checked by cvc5 itself and the solver is in a safe state after exhausting a limit. -Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed. - - -Overall time limit (:ref:`--tlimit `) --------------------------------------------------------- - -The :ref:`tlimit ` option limits the overall running time of the cvc5 solver binary. -It is implemented using an asynchronous interrupt that is usually managed by the operating system (using `setitimer`). -When this interrupt occurs, cvc5 outputs a corresponding message, prints the current statistics and immediately terminates its process. The same is done when an external resource limiting mechanism is in place, for example `ulimit`. - -This mechanism is inherently unsuited when cvc5 is used within another application process via one of its APIs: therefore, it is only honored when running as a standalone binary. -Setting :ref:`tlimit ` via the API or the `(set-option)` SMT-LIB command has thus no effect. - - -Resource manager and resource spending --------------------------------------- - -All other limits are enforced centrally by the resource manager as follows. -Whenever certain parts of the solver execute, they instruct the resource manager to *spend* a resource. -As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check. -To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components. -Then, it returns `unknown` (with an :cpp:enum:`explanation `). - -The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time. -Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks. -In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the :ref:`rweight ` option, for example with `--rweight=RestartStep=5`. \ No newline at end of file diff --git a/docs/binary/statistics.rst b/docs/binary/statistics.rst deleted file mode 100644 index e7fa9fcab..000000000 --- a/docs/binary/statistics.rst +++ /dev/null @@ -1,52 +0,0 @@ -Statistics -========== - -cvc5 collects a wide variety of statistics that can be inspected via the -:cpp:func:`Solver::getStatistics() ` API -function. -Statistics collection is only availble if the ``ENABLE_STATISTICS`` cmake option -is set to true, which is the case for all but competition builds. -The :cpp:func:`Solver::getStatistics() ` -method returns a snapshot of the statistics values that is decoupled from the -solver object and will not change when the solver is used again or deallocated. -Individual statistics values can be obtained either by iterating over the -:cpp:class:`Statistics ` object or by querying it by name. - -A statistic value (of type :cpp:class:`Stat `) has two general -properties, :cpp:func:`isInternal() ` and -:cpp:func:`isDefault() `. -:cpp:func:`isInternal() ` indicates whether a -statistic is considered public or internal. Public statistics are considered to -be part of the public API and should therefore remain stable across different -minor versions of cvc5. There is no such guarantee for internal statistics. -:cpp:func:`isDefault() ` checks whether the -current value of a statistics is still the default value, or whether its value -was changed. - -In addition to the -:cpp:func:`Solver::getStatistics() ` API -function, statistics can be printed using the following options: - -- :ref:`stats ` prints public statistics with non-default values -- :ref:`stats-all ` also prints statistics with default values -- :ref:`stats-internal ` also prints internal statistics -- :ref:`stats-every-query ` prints statistics after every (incremental) check - -A statistic value can be any of the following types: - -- integer, more specifically a signed 64-bit integer (``int64_t`` in C++). -- double, a 64-bit floating-point value (``double`` in C++). -- string, a character sequence (``std::string`` in C++). Timer statistics are - exported as string values as well, given as ``"ms"``. -- histogram, a mapping from some integral or enumeration type to their count. - The integral or enumeration types are exported as string representations - (``std::map`` in C++). - -Printing statistics on the command line looks like this: - -.. command-output:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2 - :cwd: /../build_debug - -Public statistics include some general information about the input file -(``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``) -and the lemmas each theory sent to the core solver (``theory::*``). \ No newline at end of file diff --git a/docs/conf.py.in b/docs/conf.py.in index c9a79909a..b01722073 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -48,6 +48,7 @@ extensions = [ 'autoenum', 'examples', 'include_build_file', + 'run_command', ] bibtex_bibfiles = ['references.bib'] @@ -79,6 +80,8 @@ html_show_sourcelink = False html_extra_path = [] +runcmd_build = '/' + os.path.relpath('${CMAKE_BINARY_DIR}', '${CMAKE_CURRENT_SOURCE_DIR}') + # -- Configuration for examples extension ------------------------------------ # Configuration for tabs: title, language and group for detecting missing files examples_types = { diff --git a/docs/ext/run_command.py b/docs/ext/run_command.py new file mode 100644 index 000000000..55676be52 --- /dev/null +++ b/docs/ext/run_command.py @@ -0,0 +1,57 @@ +from docutils import nodes +from docutils.parsers.rst import directives +from docutils.statemachine import StringList +from sphinx.util.docutils import SphinxDirective + + +class RunCommand(SphinxDirective): + """Add directive `run-command` that enhances `command-output` by proper usage + of the build directory. It is used just the same as `command-output`: + + .. run-command:: + :cwd: /directory + + The only difference to `command-output` is that the current working directory + defaults to the current build folder, and the directory (optionally) given + to the `cwd` option allows for the following placeholders: + + - ``: current build folder + + The path of the build folder needs to be configured in the `runcmd_build` option. + """ + + has_content = True + option_spec = { + 'cwd': directives.path + } + + def run(self): + self.state.document.settings.env.note_dependency(__file__) + + cwd = self.env.config.runcmd_build + if 'cwd' in self.options: + repl = { + '': self.env.config.runcmd_build, + } + cwd = self.options['cwd'] + for r,s in repl.items(): + cwd = cwd.replace(r, s) + + content = [ + '.. command-output:: ' + ''.join(self.content), + ' :cwd: ' + cwd] + + node = nodes.Element() + self.state.nested_parse(StringList(content), 0, node) + return node.children + + +def setup(app): + app.setup_extension('sphinxcontrib.programoutput') + app.add_config_value('runcmd_build', '', 'env') + app.add_directive("run-command", RunCommand) + return { + 'version': '0.1', + 'parallel_read_safe': True, + 'parallel_write_safe': True, + } diff --git a/docs/index.rst b/docs/index.rst index a533ff4b6..746b18dac 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -17,7 +17,11 @@ Table of Contents installation/installation binary/binary api/api + options + output-tags proofs/proofs + resource-limits + statistics examples/examples theories/theories references diff --git a/docs/options.rst b/docs/options.rst new file mode 100644 index 000000000..abcd3b3e9 --- /dev/null +++ b/docs/options.rst @@ -0,0 +1,30 @@ +Options +======= + +cvc5 can be configured at runtime using a wide range of options. +When cvc5 is used as a binary, options can be set on the command line. +Also, options can be set and inspected using the respective commands of the input language and the corresponding API functions: + +- C++ API: :cpp:func:`setOption() `, + :cpp:func:`getOption() `, + :cpp:func:`getOptionNames() `, + :cpp:func:`getOptionInfo() ` +- Java API: ``setOption()``, ``getOption()``, ``getOptionNames()``, ``getOptionInfo()`` +- Base Python API: :py:func:`setOption() `, + :py:func:`getOption() `, + :py:func:`getOptionNames() `, + :py:func:`getOptionInfo() ` + +Generally, all options are identified by a name, and they can additionally have one or more aliases (that can be used instead of their name anywhere) and a short name (a single letter). +Internally, options are strongly typed and must be either Boolean, (signed or unsigned) integers, floating-point numbers, strings, or an enumeration type. Values for options with a numeric type may be restricted to an interval. A few options have custom types (for example :ref:`err `) that require special treatment internally. +The usage of such options is documented as part of the documentation for the corresponding options. + +On the command line, a Boolean option can be set to true by ``--`` or ``-``. +Most Boolean options can also be set to false by ``--no-``. +In the different APIs, this is done via ``setOption("", "true" | "false")``. +For all other types, values can be given on the command line using ``--=`` or ``-- `` and ``setOption("", "")`` in the different APIs. +The given value must be convertible to the appropriate type, in particular for numeric and enumeration types. + +Below is an exhaustive list of options supported by cvc5. + +.. include-build-file:: options_generated.rst diff --git a/docs/output-tags.rst b/docs/output-tags.rst new file mode 100644 index 000000000..689e03ab8 --- /dev/null +++ b/docs/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:`output ` option. + +As of now, the following output tags are supported: + +.. include-build-file:: output_tags_generated.rst diff --git a/docs/resource-limits.rst b/docs/resource-limits.rst new file mode 100644 index 000000000..bc20ed10e --- /dev/null +++ b/docs/resource-limits.rst @@ -0,0 +1,38 @@ +Resource limits +=============== + +cvc5 supports limiting the time or *resources* it uses during solving via the options +:ref:`tlimit `, :ref:`tlimit-per `, +:ref:`rlimit `, and :ref:`rlimit-per `. +All these options take a single non-negative number as an argument where giving zero explicitly disables the respective limit. For time limits the number is interpreted as the number of milliseconds, and for resource limits it indicates the amount of *resources*. + +The limits configured using :ref:`tlimit ` and :ref:`rlimit ` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver ` object, respectively. +In contrast to that, :ref:`tlimit-per ` and :ref:`rlimit-per ` apply to every check individually (:cpp:func:`checkSat `, :cpp:func:`checkSatAssuming `, :cpp:func:`checkEntailed `, etc). + +Except for the overall time limit (see below), the limits are checked by cvc5 itself and the solver is in a safe state after exhausting a limit. +Due to the way cvc5 checks these limits (see below), cvc5 may not precisely honor per-call time limits: if a subroutine requires a long time to finish without spending resources itself, cvc5 only realizes afterwards that the timeout has (long) passed. + + +Overall time limit (:ref:`tlimit ` option) +------------------------------------------------------------- + +The :ref:`tlimit ` option limits the overall running time of the cvc5 solver binary. +It is implemented using an asynchronous interrupt that is usually managed by the operating system (using ``setitimer``). +When this interrupt occurs, cvc5 outputs a corresponding message, prints the current statistics and immediately terminates its process. The same is done when an external resource limiting mechanism is in place, for example ``ulimit``. + +This mechanism is inherently unsuited when cvc5 is used within another application process via one of its APIs: therefore, it is only honored when running as a standalone binary. +Setting :ref:`tlimit ` via the API or the ``(set-option)`` SMT-LIB command has thus no effect. + + +Resource manager and resource spending +-------------------------------------- + +All other limits are enforced centrally by the resource manager as follows. +Whenever certain parts of the solver execute, they instruct the resource manager to *spend* a resource. +As soon as the resource manager realizes that some limit is exhausted (either the resource limit or the per-check time limit is reached), it asynchronously instructs the core solver to interrupt the check. +To not invalidate the internal state of the solver, and allow to use it again after an interrupt, the solver continues its work until it reaches a safe point in one of the core solving components. +Then, it returns `unknown` (with an :cpp:enum:`explanation `). + +The intention of a resource limit is to be a deterministic measure that grows (linearly, if possible) with actual running time. +Resources are spent when lemmas are generated and during a few select events like preprocessing, rewriting, decisions and restarts in the SAT solver, or theory checks. +In case the resource spending does not properly reflect the running time, the weights of the individual resources can be modified using the :ref:`rweight ` option, for example with ``--rweight=RestartStep=5``. \ No newline at end of file diff --git a/docs/statistics.rst b/docs/statistics.rst new file mode 100644 index 000000000..ea4410df4 --- /dev/null +++ b/docs/statistics.rst @@ -0,0 +1,48 @@ +Statistics +========== + +cvc5 collects a wide variety of statistics that give some insight on how it solves a particular input. +The statistics can be inspected via the :cpp:func:`Solver::getStatistics() ` API +function, or printed using the following options: + +- :ref:`stats ` prints public statistics with non-default values +- :ref:`stats-all ` also prints statistics with default values +- :ref:`stats-internal ` also prints internal statistics +- :ref:`stats-every-query ` prints statistics after every (incremental) check + +Statistics collection is only available if the ``ENABLE_STATISTICS`` cmake option +is set to true, which is the case for all but competition builds. +Statistics, obtained via :cpp:func:`Solver::getStatistics() `, +are always a snapshot of the statistics values that is decoupled from the +solver object and will not change when the solver is used again or deallocated. +Individual statistics values can be obtained via the API either by iterating over the +:cpp:class:`Statistics ` object or by querying it by name. + +A statistic value (of type :cpp:class:`Stat `) has two general +properties, :cpp:func:`isInternal() ` and +:cpp:func:`isDefault() `. +:cpp:func:`isInternal() ` indicates whether a +statistic is considered public or internal. Public statistics are considered to +be part of the public API and should therefore remain stable across different +minor versions of cvc5. There is no such guarantee for internal statistics. +:cpp:func:`isDefault() ` checks whether the +current value of a statistics is still the default value, or whether its value +was changed. + +A statistic value can be any of the following types: + +- integer, more specifically a signed 64-bit integer (``int64_t`` in C++). +- double, a 64-bit floating-point value (``double`` in C++). +- string, a character sequence (``std::string`` in C++). Timer statistics are + exported as string values as well, given as ``"ms"``. +- histogram, a mapping from some integral or enumeration type to their count. + The integral or enumeration types are exported as string representations + (``std::map`` in C++). + +Printing statistics on the command line looks like this: + +.. run-command:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2 + +Public statistics include some general information about the input file +(``driver::filename`` and ``api::*``), the overall runtime (``global::totalTime``) +and the lemmas each theory sent to the core solver (``theory::*``). diff --git a/src/options/base_options.toml b/src/options/base_options.toml index cd04406c1..4bf13ec25 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -6,6 +6,7 @@ name = "Base" category = "regular" long = "err=erroutput" type = "ManagedErr" + default = '{}' alias = ["diagnostic-output-channel"] predicates = ["setErrStream"] includes = ["", "options/managed_streams.h"] @@ -16,6 +17,7 @@ name = "Base" category = "regular" long = "in=input" type = "ManagedIn" + default = '{}' includes = ["", "options/managed_streams.h"] help = "Set the error (or diagnostic) output channel. Reads from stdin for \"stdin\" or \"--\" and the given filename otherwise." @@ -24,6 +26,7 @@ name = "Base" category = "regular" long = "out=output" type = "ManagedOut" + default = '{}' alias = ["regular-output-channel"] includes = ["", "options/managed_streams.h"] help = "Set the error (or diagnostic) output channel. Writes to stdout for \"stdout\" or \"--\", stderr for \"stderr\" or the given filename otherwise." @@ -94,6 +97,7 @@ name = "Base" long = "stats" category = "common" type = "bool" + default = "false" predicates = ["setStats"] help = "give statistics on exit" @@ -102,6 +106,7 @@ name = "Base" long = "stats-all" category = "expert" type = "bool" + default = "false" predicates = ["setStatsDetail"] help = "print unchanged (defaulted) statistics as well" @@ -110,6 +115,7 @@ name = "Base" long = "stats-internal" category = "expert" type = "bool" + default = "false" predicates = ["setStatsDetail"] help = "print internal (non-public) statistics as well" @@ -118,8 +124,8 @@ name = "Base" long = "stats-every-query" category = "regular" type = "bool" - predicates = ["setStatsDetail"] default = "false" + predicates = ["setStatsDetail"] help = "in incremental mode, print stats after every satisfiability or validity query" [[option]] @@ -127,6 +133,7 @@ name = "Base" category = "regular" long = "parse-only" type = "bool" + default = "false" help = "exit after parsing input" [[option]] @@ -134,6 +141,7 @@ name = "Base" category = "regular" long = "preprocess-only" type = "bool" + default = "false" help = "exit after preprocessing input" [[option]] @@ -215,12 +223,14 @@ name = "Base" category = "undocumented" includes = [""] type = "std::bitset(OutputTag::__MAX_VALUE)+1>" + default = '{}' [[option]] name = "printSuccess" category = "regular" long = "print-success" type = "bool" + default = "false" predicates = ["setPrintSuccess"] help = "print the \"success\" output required of SMT-LIBv2" @@ -229,6 +239,7 @@ name = "Base" category = "common" long = "tlimit=MS" type = "uint64_t" + default = "0" help = "set time limit in milliseconds of wall clock time" [[option]] @@ -236,6 +247,7 @@ name = "Base" category = "common" long = "tlimit-per=MS" type = "uint64_t" + default = "0" help = "set time limit per query in milliseconds" [[option]] @@ -243,6 +255,7 @@ name = "Base" category = "common" long = "rlimit=N" type = "uint64_t" + default = "0" help = "set resource limit" [[option]] @@ -251,6 +264,7 @@ name = "Base" category = "common" long = "rlimit-per=N" type = "uint64_t" + default = "0" help = "set resource limit per query" # --rweight is used to override the default of one particular resource weight. @@ -272,3 +286,4 @@ name = "Base" name = "resourceWeightHolder" category = "undocumented" type = "std::vector" + default = '{}' diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 10c58016d..ac63b1fb1 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -7,6 +7,7 @@ name = "Driver" short = "V" long = "version" type = "bool" + default = "false" predicates = ["showVersion"] alternate = false help = "identify this cvc5 binary" @@ -17,6 +18,7 @@ name = "Driver" short = "h" long = "help" type = "bool" + default = "false" alternate = false help = "full command line reference" @@ -25,6 +27,7 @@ name = "Driver" category = "common" long = "show-config" type = "bool" + default = "false" predicates = ["showConfiguration"] alternate = false help = "show cvc5 static configuration" @@ -34,6 +37,7 @@ name = "Driver" category = "common" long = "copyright" type = "bool" + default = "false" predicates = ["showCopyright"] alternate = false help = "show cvc5 copyright information" @@ -52,6 +56,7 @@ name = "Driver" category = "regular" long = "show-debug-tags" type = "bool" + default = "false" predicates = ["showDebugTags"] alternate = false help = "show all available tags for debugging" @@ -61,6 +66,7 @@ name = "Driver" category = "regular" long = "show-trace-tags" type = "bool" + default = "false" predicates = ["showTraceTags"] alternate = false help = "show all available tags for tracing" @@ -78,6 +84,7 @@ name = "Driver" category = "regular" long = "interactive" type = "bool" + default = "false" help = "force interactive shell/non-interactive mode" [[option]] @@ -85,6 +92,7 @@ name = "Driver" category = "undocumented" long = "filename=FILENAME" type = "std::string" + default = '""' help = "filename of the input" [[option]] diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index da3e98117..de76dbe52 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -185,6 +185,9 @@ class Option(object): self.names.add(self.long_name) if self.alias: self.names.update(self.alias) + if self.mode: + self.mode_name = { k: v[0]['name'] for k,v in self.mode.items() } + self.mode_help = { k: v[0].get('help', None) for k,v in self.mode.items() } def __lt__(self, other): if self.long_name and other.long_name: @@ -683,78 +686,82 @@ def generate_cli_help(modules): def _sphinx_help_add(module, option, common, others): """Analyze an option and add it to either common or others.""" - names = [] - if option.long: - if option.long_opt: - names.append('--{}={}'.format(option.long_name, option.long_opt)) - else: - names.append('--{}'.format(option.long_name)) - - if option.alias: - if option.long_opt: - names.extend( - ['--{}={}'.format(a, option.long_opt) for a in option.alias]) - else: - names.extend(['--{}'.format(a) for a in option.alias]) + if option.category == 'common': + common.append(option) + else: + if module.name not in others: + others[module.name] = [] + others[module.name].append(option) - if option.short: - if option.long_opt: - names.append('-{} {}'.format(option.short, option.long_opt)) - else: - names.append('-{}'.format(option.short)) - modes = None - if option.mode: - modes = {} - for _, data in option.mode.items(): - assert len(data) == 1 - modes[data[0]['name']] = data[0].get('help', '') +def _sphinx_help_render_option(res, opt): + """Render an option to be displayed with sphinx.""" + names = [] + if opt.short: + names.append(opt.short) + names.append(opt.long_name) + if opt.alias: + names.extend(opt.alias) data = { - 'long_name': option.long_name, - 'name': names, - 'help': option.help, - 'expert': option.category == 'expert', - 'alternate': option.alternate, - 'help_mode': option.help_mode, - 'modes': modes, + 'names': ' | '.join(names), + 'alternate': '', + 'type': '', + 'default': '', } - if option.category == 'common': - common.append(data) + if opt.alternate: + data['alternate'] = ' (also ``--no-*``)' + + if opt.type == 'bool': + data['type'] = 'type ``bool``' + elif opt.type == 'std::string': + data['type'] = 'type ``string``' + elif is_numeric_cpp_type(opt.type): + data['type'] = 'type ``{}``'.format(opt.type) + if opt.minimum and opt.maximum: + data['type'] += ', ``{} <= {} <= {}``'.format( + opt.minimum, opt.long_opt, opt.maximum) + elif opt.minimum: + data['type'] += ', ``{} <= {}``'.format(opt.minimum, opt.long_opt) + elif opt.maximum: + data['type'] += ', ``{} <= {}``'.format(opt.long_opt, opt.maximum) + elif opt.mode: + data['type'] = '``' + ' | '.join(opt.mode_name.values()) + '``' else: - if module.name not in others: - others[module.name] = [] - others[module.name].append(data) + data['type'] = 'custom ``{}``'.format(opt.type) + if opt.default: + if opt.mode: + data['default'] = ', default ``{}``'.format( + opt.mode_name[opt.default]) + else: + data['default'] = ', default ``{}``'.format(opt.default) -def _sphinx_help_render_option(res, opt): - """Render an option to be displayed with sphinx.""" - indent = ' ' * 4 - desc = '``{}``' - if opt['alternate']: - desc += ' (also ``--no-*``)' - val = indent + '{}' + desc = '``{names}`` [{type}{default}]{alternate}'.format(**data) - res.append('.. _lbl-option-{}:'.format(opt['long_name'])) + res.append('.. _lbl-option-{}:'.format(opt.long_name)) res.append('') - if opt['expert']: + if opt.category == 'expert': res.append('.. rst-class:: expert-option simple') res.append('') - desc += '\n{0}.. rst-class:: float-right\n\n{0}**[experts only]**\n'.format(indent) + desc += ''' + .. rst-class:: float-right - res.append(desc.format(' | '.join(opt['name']))) - res.append(val.format(opt['help'])) + **[experts only]** +''' - if opt['modes']: - res.append(val.format('')) - res.append(val.format(opt['help_mode'])) - res.append(val.format('')) - for k, v in opt['modes'].items(): - if v == '': - continue - res.append(val.format(':{}: {}'.format(k, v))) - res.append(indent) + res.append(desc) + res.append(' ' + opt.help) + + if opt.mode: + res.append(' ') + res.append(' ' + opt.help_mode) + res.append(' ') + for m in opt.mode.keys(): + if opt.mode_help[m]: + res.append(' :``{}``: {}'.format(opt.mode_name[m], opt.mode_help[m])) + res.append(' ') def generate_sphinx_help(modules): @@ -805,7 +812,7 @@ def generate_sphinx_output_tags(modules, src_dir, build_dir): info = info[0] if 'description' not in info: continue - res.append('{} (``-o {}``)'.format(name, info['name'])) + res.append(opt.mode_name[name]) res.append('~' * len(res[-1])) res.append('') res.append(info['description']) @@ -968,6 +975,8 @@ class Checker: self.perr('has aliases but no long', option=o) if o.alternate and o.type != 'bool': self.perr('is alternate but not bool', option=o) + if o.name and o.default is None: + self.perr('has no default', option=o) if o.long: self.__check_option_long(o, o.long_name) if o.alternate: diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 254c99486..4dccd4c2e 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -6,6 +6,7 @@ name = "Parser" category = "common" long = "strict-parsing" type = "bool" + default = "false" help = "be less tolerant of non-conforming inputs" [[option]] @@ -49,4 +50,5 @@ name = "Parser" category = "expert" long = "force-logic=LOGIC" type = "std::string" + default = '""' help = "set the logic, and override all further user attempts to change it" diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 6ee27dfb0..3be0a607b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1081,6 +1081,7 @@ name = "Quantifiers" category = "regular" long = "sygus-repair-const-timeout=N" type = "uint64_t" + default = "0" help = "timeout (in milliseconds) for the satisfiability check to repair constants in sygus candidate solutions" [[option]] @@ -1453,6 +1454,7 @@ name = "Quantifiers" category = "regular" long = "sygus-expr-miner-check-timeout=N" type = "uint64_t" + default = "0" help = "timeout (in milliseconds) for satisfiability checks in expression miners" [[option]] diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 8e961a3bd..fdf65f5ec 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -63,6 +63,7 @@ name = "SMT Layer" category = "regular" long = "check-models" type = "bool" + default = "false" help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions" [[option]] @@ -70,6 +71,7 @@ name = "SMT Layer" category = "regular" long = "debug-check-models" type = "bool" + default = "false" help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions" [[option]] @@ -137,6 +139,7 @@ name = "SMT Layer" category = "regular" long = "check-proofs" type = "bool" + default = "false" help = "after UNSAT/VALID, check the generated proof (with proof)" [[option]] @@ -165,6 +168,7 @@ name = "SMT Layer" category = "regular" long = "produce-unsat-cores" type = "bool" + default = "false" help = "turn on unsat core generation. Unless otherwise specified, cores will be produced using SAT soving under assumptions and preprocessing proofs." [[option]] @@ -215,6 +219,7 @@ name = "SMT Layer" category = "regular" long = "check-unsat-cores" type = "bool" + default = "false" help = "after UNSAT/VALID, produce and check an unsat core (expensive)" [[option]] @@ -281,6 +286,7 @@ name = "SMT Layer" category = "regular" long = "ite-simp" type = "bool" + default = "false" help = "turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)" [[option]] @@ -346,6 +352,7 @@ name = "SMT Layer" category = "regular" long = "repeat-simp" type = "bool" + default = "false" help = "make multiple passes with nonclausal simplifier" [[option]]