diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
| commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
| tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory/quantifiers/options | |
| parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) | |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 391abe9eb..ab0526471 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -220,8 +220,12 @@ option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true reconstruct solutions for single invocation conjectures in original grammar option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true include constants when reconstruct solutions for single invocation conjectures in original grammar +option cegqiSingleInvPreRegInst --cegqi-si-prereg-inst bool :default true + preregister ground instantiations when single invocation option cegqiSingleInvAbort --cegqi-si-abort bool :default false - abort if our synthesis conjecture is not single invocation + abort if synthesis conjecture is not single invocation +option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false + abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form @@ -259,5 +263,10 @@ option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false option quantAlphaEquiv --quant-alpha-equiv bool :default true infer alpha equivalence between quantified formulas + +### recursive function options + +#option funDefs --fun-defs bool :default false +# enable specialized techniques for recursive function definitions endmodule |