diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-26 17:55:09 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-26 17:55:16 -0500 |
| commit | 4cff52d94318646415fe89dfe3b97750451eb7c1 (patch) | |
| tree | 2bc60458c4ac8075ffc3ffe74175b5e76136dd1a /src/options/quantifiers_options | |
| parent | e6d75ab22dfb56df202b916ecd9b4327f931c782 (diff) | |
Add option to minimize sygus solutions based on using weakest implicants of instantiations in unsat cores.
Diffstat (limited to 'src/options/quantifiers_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 37178510d..953150e42 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -244,6 +244,8 @@ 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 cegqiSolMinInst --cegqi-si-sol-min-inst bool :default true + minimize individual instantiations 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 |