diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:52:37 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-20 11:52:37 -0500 |
| commit | daf2eca9a4bb32680cbf35945bb09cfd13be76a7 (patch) | |
| tree | fd387c71b6d1bd03e79e4e3403041c12a906a98a /src/options | |
| parent | ae7434f94a1bc66ee12474414985249a71881b6c (diff) | |
Print only instantiations that are in the unsat core when --proof is enabled. Add option to minimize sygus solutions based on unsat core (disabled by default).
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/quantifiers_options | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options index 0a94ad890..37178510d 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -242,6 +242,8 @@ option cegqiSingleInvPartial --cegqi-si-partial bool :default false combined techniques for synthesis conjectures that are partially single invocation option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar +option cegqiSolMinCore --cegqi-si-sol-min-core bool :default false + minimize solutions for single invocation conjectures based on unsat core option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false |