diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-22 08:52:42 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-22 09:00:56 -0500 |
| commit | 620ebbaf88f07abc36399499cfa6dfef8c3369d9 (patch) | |
| tree | fe18fdae38b0fcd64ea9d3014a3dd7846b6c7202 /src/options | |
| parent | 18d2fd549d5058a6ea3ee782568bbc3ce00189ea (diff) | |
Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.
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 cf8fca2fa..585ef3dc2 100644 --- a/src/options/quantifiers_options +++ b/src/options/quantifiers_options @@ -253,6 +253,8 @@ option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default include constants when reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvAbort --cegqi-si-abort bool :default false abort if synthesis conjecture is not single invocation +option cegqiUnifCondSol --cegqi-unif-csol bool :default false + enable approach which unifies conditional solutions option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form |