diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-07-01 10:07:39 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-07-01 10:07:39 -0500 |
| commit | bdf46b42d6bd66121a5b5175a81408cd64d7ecfa (patch) | |
| tree | 2aae6c707375616964afd88437be3b48f1dbe45a /src/options/quantifiers_options.toml | |
| parent | d288f52dd82fe6590950758289e86ebcb039350d (diff) | |
Add option to limit the number of instantiation rounds (#6818)
This adds an option to limit the number of instantiation rounds used by quantifiers engine.
This option may be generally useful for making quantifiers terminating. It also is necessary to update the new default behavior of SyGuS + recursive functions. A followup PR will make sygus verification calls set the option added on this PR automatically, so that we use incomplete + termination strategies for (non-PBE) sygus in the presence of recursive functions.
This PR also makes minor improvements to the quantifier utility infrastructure.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 20376c053..45341a6a6 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -475,6 +475,14 @@ name = "Quantifiers" help = "only input terms are assigned instantiation level zero" [[option]] + name = "instMaxRounds" + category = "regular" + long = "inst-max-rounds=N" + type = "int" + default = "-1" + help = "maximum number of instantiation rounds (-1 == no limit, default)" + +[[option]] name = "quantRepMode" category = "regular" long = "quant-rep-mode=MODE" |