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.
The easiest way to use cvc5 is usually to invoke the cvc5 binary via the command line.
The :doc:`quickstart guide <quickstart>` gives a short introduction on how to use cvc5 via the SMT-LIBv2
-interface, but cvc5 also supports other :doc:`input languages <languages>`.
-The behavior of cvc5 can be changed with a number of :doc:`options <options>`, and :doc:`output tags <output-tags>` allow to extract structured information about the solving process.
+interface.
+
+The cvc5 binary supports the following input languages:
+
+* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
+* `SyGuS-IF <https://sygus.org/language/>`_
+* `TPTP <http://www.tptp.org/>`_
+
Alternatively, cvc5 features :doc:`several APIs <../api/api>` for different programming languages.
:maxdepth: 2
quickstart
- languages
- options
- output-tags
- resource-limits
- statistics
+++ /dev/null
-Input Languages
-===============
-
-cvc5 supports the following input languages:
-
-* `SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_
-* `SyGuS-IF <https://sygus.org/language/>`_
-* `TPTP <http://www.tptp.org/>`_
+++ /dev/null
-Commandline Options
-===================
-
-Below is an exhaustive list of commandline options supported by cvc5.
-
-.. include-build-file:: options_generated.rst
-
+++ /dev/null
-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
+++ /dev/null
-Resource limits
-===============
-
-cvc5 supports limiting the time or *resources* it uses during solving via the options
-:ref:`tlimit <lbl-option-tlimit>`, :ref:`tlimit-per <lbl-option-tlimit-per>`,
-:ref:`rlimit <lbl-option-rlimit>`, and :ref:`rlimit-per <lbl-option-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 <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::api::Solver>` object, respectively.
-In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::api::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::api::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::api::Solver::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 <lbl-option-tlimit>`)
---------------------------------------------------------
-
-The :ref:`tlimit <lbl-option-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 <lbl-option-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 <cvc5::api::Result::UnknownExplanation>`).
-
-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 <lbl-option-rweight>` option, for example with `--rweight=RestartStep=5`.
\ No newline at end of file
+++ /dev/null
-Statistics
-==========
-
-cvc5 collects a wide variety of statistics that can be inspected via the
-:cpp:func:`Solver::getStatistics() <cvc5::api::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() <cvc5::api::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 <cvc5::api::Statistics>` object or by querying it by name.
-
-A statistic value (of type :cpp:class:`Stat <cvc5::api::Stat>`) has two general
-properties, :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` and
-:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>`.
-:cpp:func:`isInternal() <cvc5::api::Stat::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() <cvc5::api::Stat::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() <cvc5::api::Solver::getStatistics()>` API
-function, statistics can be printed using the following options:
-
-- :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
-- :ref:`stats-all <lbl-option-stats-all>` also prints statistics with default values
-- :ref:`stats-internal <lbl-option-stats-internal>` also prints internal statistics
-- :ref:`stats-every-query <lbl-option-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 ``"<value>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<std::string, uint64_t>`` 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
'autoenum',
'examples',
'include_build_file',
+ 'run_command',
]
bibtex_bibfiles = ['references.bib']
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 = {
--- /dev/null
+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:: <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:
+
+ - `<build>`: 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 = {
+ '<build>': 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,
+ }
installation/installation
binary/binary
api/api
+ options
+ output-tags
proofs/proofs
+ resource-limits
+ statistics
examples/examples
theories/theories
references
--- /dev/null
+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() <cvc5::api::Solver::setOption()>`,
+ :cpp:func:`getOption() <cvc5::api::Solver::getOption()>`,
+ :cpp:func:`getOptionNames() <cvc5::api::Solver::getOptionNames()>`,
+ :cpp:func:`getOptionInfo() <cvc5::api::Solver::getOptionInfo()>`
+- Java API: ``setOption()``, ``getOption()``, ``getOptionNames()``, ``getOptionInfo()``
+- Base Python API: :py:func:`setOption() <cvc5.Solver.setOption()>`,
+ :py:func:`getOption() <cvc5.Solver.getOption()>`,
+ :py:func:`getOptionNames() <cvc5.Solver.getOptionNames()>`,
+ :py:func:`getOptionInfo() <cvc5.Solver.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 <lbl-option-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 ``--<name>`` or ``-<short>``.
+Most Boolean options can also be set to false by ``--no-<name>``.
+In the different APIs, this is done via ``setOption("<name>", "true" | "false")``.
+For all other types, values can be given on the command line using ``--<name>=<value>`` or ``--<name> <value>`` and ``setOption("<name>", "<value>")`` 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
--- /dev/null
+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 <lbl-option-output>` option.
+
+As of now, the following output tags are supported:
+
+.. include-build-file:: output_tags_generated.rst
--- /dev/null
+Resource limits
+===============
+
+cvc5 supports limiting the time or *resources* it uses during solving via the options
+:ref:`tlimit <lbl-option-tlimit>`, :ref:`tlimit-per <lbl-option-tlimit-per>`,
+:ref:`rlimit <lbl-option-rlimit>`, and :ref:`rlimit-per <lbl-option-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 <lbl-option-tlimit>` and :ref:`rlimit <lbl-option-rlimit>` restrict time and resource usage over the whole lifetime of the :cpp:class:`solver <cvc5::api::Solver>` object, respectively.
+In contrast to that, :ref:`tlimit-per <lbl-option-tlimit-per>` and :ref:`rlimit-per <lbl-option-rlimit-per>` apply to every check individually (:cpp:func:`checkSat <cvc5::api::Solver::checkSat>`, :cpp:func:`checkSatAssuming <cvc5::api::Solver::checkSatAssuming>`, :cpp:func:`checkEntailed <cvc5::api::Solver::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 <lbl-option-tlimit>` option)
+-------------------------------------------------------------
+
+The :ref:`tlimit <lbl-option-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 <lbl-option-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 <cvc5::api::Result::UnknownExplanation>`).
+
+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 <lbl-option-rweight>` option, for example with ``--rweight=RestartStep=5``.
\ No newline at end of file
--- /dev/null
+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() <cvc5::api::Solver::getStatistics()>` API
+function, or printed using the following options:
+
+- :ref:`stats <lbl-option-stats>` prints public statistics with non-default values
+- :ref:`stats-all <lbl-option-stats-all>` also prints statistics with default values
+- :ref:`stats-internal <lbl-option-stats-internal>` also prints internal statistics
+- :ref:`stats-every-query <lbl-option-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() <cvc5::api::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 <cvc5::api::Statistics>` object or by querying it by name.
+
+A statistic value (of type :cpp:class:`Stat <cvc5::api::Stat>`) has two general
+properties, :cpp:func:`isInternal() <cvc5::api::Stat::isInternal()>` and
+:cpp:func:`isDefault() <cvc5::api::Stat::isDefault()>`.
+:cpp:func:`isInternal() <cvc5::api::Stat::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() <cvc5::api::Stat::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 ``"<value>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<std::string, uint64_t>`` 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::*``).
category = "regular"
long = "err=erroutput"
type = "ManagedErr"
+ default = '{}'
alias = ["diagnostic-output-channel"]
predicates = ["setErrStream"]
includes = ["<iostream>", "options/managed_streams.h"]
category = "regular"
long = "in=input"
type = "ManagedIn"
+ default = '{}'
includes = ["<iostream>", "options/managed_streams.h"]
help = "Set the error (or diagnostic) output channel. Reads from stdin for \"stdin\" or \"--\" and the given filename otherwise."
category = "regular"
long = "out=output"
type = "ManagedOut"
+ default = '{}'
alias = ["regular-output-channel"]
includes = ["<iostream>", "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."
long = "stats"
category = "common"
type = "bool"
+ default = "false"
predicates = ["setStats"]
help = "give statistics on exit"
long = "stats-all"
category = "expert"
type = "bool"
+ default = "false"
predicates = ["setStatsDetail"]
help = "print unchanged (defaulted) statistics as well"
long = "stats-internal"
category = "expert"
type = "bool"
+ default = "false"
predicates = ["setStatsDetail"]
help = "print internal (non-public) statistics as well"
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]]
category = "regular"
long = "parse-only"
type = "bool"
+ default = "false"
help = "exit after parsing input"
[[option]]
category = "regular"
long = "preprocess-only"
type = "bool"
+ default = "false"
help = "exit after preprocessing input"
[[option]]
category = "undocumented"
includes = ["<bitset>"]
type = "std::bitset<static_cast<size_t>(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"
category = "common"
long = "tlimit=MS"
type = "uint64_t"
+ default = "0"
help = "set time limit in milliseconds of wall clock time"
[[option]]
category = "common"
long = "tlimit-per=MS"
type = "uint64_t"
+ default = "0"
help = "set time limit per query in milliseconds"
[[option]]
category = "common"
long = "rlimit=N"
type = "uint64_t"
+ default = "0"
help = "set resource limit"
[[option]]
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.
name = "resourceWeightHolder"
category = "undocumented"
type = "std::vector<std::string>"
+ default = '{}'
short = "V"
long = "version"
type = "bool"
+ default = "false"
predicates = ["showVersion"]
alternate = false
help = "identify this cvc5 binary"
short = "h"
long = "help"
type = "bool"
+ default = "false"
alternate = false
help = "full command line reference"
category = "common"
long = "show-config"
type = "bool"
+ default = "false"
predicates = ["showConfiguration"]
alternate = false
help = "show cvc5 static configuration"
category = "common"
long = "copyright"
type = "bool"
+ default = "false"
predicates = ["showCopyright"]
alternate = false
help = "show cvc5 copyright information"
category = "regular"
long = "show-debug-tags"
type = "bool"
+ default = "false"
predicates = ["showDebugTags"]
alternate = false
help = "show all available tags for debugging"
category = "regular"
long = "show-trace-tags"
type = "bool"
+ default = "false"
predicates = ["showTraceTags"]
alternate = false
help = "show all available tags for tracing"
category = "regular"
long = "interactive"
type = "bool"
+ default = "false"
help = "force interactive shell/non-interactive mode"
[[option]]
category = "undocumented"
long = "filename=FILENAME"
type = "std::string"
+ default = '""'
help = "filename of the input"
[[option]]
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:
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):
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'])
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:
category = "common"
long = "strict-parsing"
type = "bool"
+ default = "false"
help = "be less tolerant of non-conforming inputs"
[[option]]
category = "expert"
long = "force-logic=LOGIC"
type = "std::string"
+ default = '""'
help = "set the logic, and override all further user attempts to change it"
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]]
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]]
category = "regular"
long = "check-models"
type = "bool"
+ default = "false"
help = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
[[option]]
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]]
category = "regular"
long = "check-proofs"
type = "bool"
+ default = "false"
help = "after UNSAT/VALID, check the generated proof (with proof)"
[[option]]
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]]
category = "regular"
long = "check-unsat-cores"
type = "bool"
+ default = "false"
help = "after UNSAT/VALID, produce and check an unsat core (expensive)"
[[option]]
category = "regular"
long = "ite-simp"
type = "bool"
+ default = "false"
help = "turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)"
[[option]]
category = "regular"
long = "repeat-simp"
type = "bool"
+ default = "false"
help = "make multiple passes with nonclausal simplifier"
[[option]]
projects / cvc5.git / commitdiff