From b08ef33d5ab27471fd26e53b9a8b2d1833424f55 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 21 Mar 2022 22:19:11 +0100 Subject: [PATCH] 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. --- docs/binary/binary.rst | 15 ++-- docs/binary/languages.rst | 8 -- docs/binary/options.rst | 7 -- docs/conf.py.in | 3 + docs/ext/run_command.py | 57 ++++++++++++ docs/index.rst | 4 + docs/options.rst | 30 +++++++ docs/{binary => }/output-tags.rst | 2 +- docs/{binary => }/resource-limits.rst | 12 +-- docs/{binary => }/statistics.rst | 34 ++++--- src/options/base_options.toml | 17 +++- src/options/main_options.toml | 8 ++ src/options/mkoptions.py | 125 ++++++++++++++------------ src/options/parser_options.toml | 2 + src/options/quantifiers_options.toml | 2 + src/options/smt_options.toml | 7 ++ 16 files changed, 226 insertions(+), 107 deletions(-) delete mode 100644 docs/binary/languages.rst delete mode 100644 docs/binary/options.rst create mode 100644 docs/ext/run_command.py create mode 100644 docs/options.rst rename docs/{binary => }/output-tags.rst (84%) rename docs/{binary => }/resource-limits.rst (89%) rename docs/{binary => }/statistics.rst (74%) 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/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/binary/output-tags.rst b/docs/output-tags.rst similarity index 84% rename from docs/binary/output-tags.rst rename to docs/output-tags.rst index 62aba5c81..689e03ab8 100644 --- a/docs/binary/output-tags.rst +++ b/docs/output-tags.rst @@ -3,7 +3,7 @@ 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. +:ref:`output ` option. As of now, the following output tags are supported: diff --git a/docs/binary/resource-limits.rst b/docs/resource-limits.rst similarity index 89% rename from docs/binary/resource-limits.rst rename to docs/resource-limits.rst index f9fe06b5a..bc20ed10e 100644 --- a/docs/binary/resource-limits.rst +++ b/docs/resource-limits.rst @@ -13,15 +13,15 @@ Except for the overall time limit (see below), the limits are checked by cvc5 it 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 `) --------------------------------------------------------- +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`. +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. +Setting :ref:`tlimit ` via the API or the ``(set-option)`` SMT-LIB command has thus no effect. Resource manager and resource spending @@ -35,4 +35,4 @@ Then, it returns `unknown` (with an :cpp:enum:`explanation ` option, for example with `--rweight=RestartStep=5`. \ No newline at end of file +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/statistics.rst similarity index 74% rename from docs/binary/statistics.rst rename to docs/statistics.rst index e7fa9fcab..ea4410df4 100644 --- a/docs/binary/statistics.rst +++ b/docs/statistics.rst @@ -1,15 +1,21 @@ 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 +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. -The :cpp:func:`Solver::getStatistics() ` -method returns a snapshot of the statistics values that is decoupled from the +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 either by iterating over the +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 @@ -23,15 +29,6 @@ minor versions of cvc5. There is no such guarantee for internal statistics. 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++). @@ -44,9 +41,8 @@ A statistic value can be any of the following types: Printing statistics on the command line looks like this: -.. command-output:: bin/cvc5 --stats ../test/regress/regress0/auflia/bug336.smt2 - :cwd: /../build_debug +.. 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::*``). \ No newline at end of file +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]] -- 2.30.2