diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-27 10:32:32 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-27 10:32:32 -0600 |
| commit | 8795787c2ef337e73b46778b99f5bfa6c2a19f93 (patch) | |
| tree | 0989e95f24c2eeedd177d2281069d266b31d971d /src/options/quantifiers_options.toml | |
| parent | a6d3c9e7fb765704f34815900712b10e85687edc (diff) | |
(proof-new) Improvements to quantifiers engine and instantiate interfaces (#5814)
This makes printing instantiations done at the SmtEngine level instead of deeply embedded within the Instantiate module. This provides much better flexibility for future uses of instantiations (e.g. how they are minimized in the new proof infrastructure).
Note this PR breaks the functionality that instantiations are minimized based on the old unsat cores infrastructure (see the disabled regression). This will be fixed once proof-new is fully merged.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index d3b3502fc..4b98cb84d 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1889,29 +1889,6 @@ header = "options/quantifiers_options.h" ### Output options [[option]] - name = "printInstMode" - category = "regular" - long = "print-inst=MODE" - type = "PrintInstMode" - default = "LIST" - help = "print format for printing instantiations" - help_mode = "Print format for printing instantiations." -[[option.mode.LIST]] - name = "list" - help = "Print the list of instantiations per quantified formula, when non-empty." -[[option.mode.NUM]] - name = "num" - help = "Print the total number of instantiations per quantified formula, when non-zero." - -[[option]] - name = "printInstFull" - category = "regular" - long = "print-inst-full" - type = "bool" - default = "false" - help = "print instantiations for formulas that do not have given identifiers" - -[[option]] name = "debugInst" category = "regular" long = "debug-inst" |