diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-14 01:41:24 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-13 23:41:24 -0700 |
| commit | 1cd3c3c5dad84093aa6b2db164798c8fff473fec (patch) | |
| tree | 2cb4fe22f3ca9c97cf93c77aa50c5d08b30dc7d0 /src/options/quantifiers_options.toml | |
| parent | 34043bdcd93860969cfd9e87c683340175c640b9 (diff) | |
Debug instantiations output (#4739)
This prints # instantiations per round (during solving) for each quantified formula with `--debug-inst`, giving output like this:
```
(num-instantiations myQuant1 1)
(num-instantiations myQuant2 1)
unsat
```
It also changes the default value of print-inst-full to match the behavior of unsat-cores vs unsat-cores-full (by default, nameless quantifiers are ignored).
It fixes an issue with qid, where mkVar was accidentally used instead of mkConst, leading to assertion failures in debug. Marking major since this fixes debug regress1.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 2b47570ed..b62468cdd 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1992,9 +1992,17 @@ header = "options/quantifiers_options.h" category = "regular" long = "print-inst-full" type = "bool" - default = "true" + default = "false" help = "print instantiations for formulas that do not have given identifiers" +[[option]] + name = "debugInst" + category = "regular" + long = "debug-inst" + type = "bool" + default = "false" + help = "print instantiations during solving (for debugging)" + ### SyGuS instantiation options [[option]] |