diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 10:17:58 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-29 10:17:58 +0100 |
| commit | 4a8045f5f57c1e71dc4a2cdadc02ca09114c70af (patch) | |
| tree | 549ebb569c6567e02679ffe739460fa8e8454367 /src/theory/quantifiers | |
| parent | 4c3c59a67f3729e929c13ee6f0f2376f78b501fb (diff) | |
Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/options | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 6fc13498c..9d4281186 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -196,12 +196,14 @@ option ceGuidedInst --cegqi bool :default false :read-write counterexample-guided quantifier instantiation option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToCegqiFairMode :handler-include "theory/quantifiers/options_handlers.h" if and how to apply fairness for cegqi -option sygusDecompose --sygus-decompose bool :default false - decompose single invocation synthesis conjectures +option sygusSingleInv --sygus-single-inv bool :default false + process single invocation synthesis conjectures option sygusNormalForm --sygus-nf bool :default true only search for sygus builtin terms that are in normal form option sygusNormalFormArg --sygus-nf-arg bool :default true account for relationship between arguments of operations in sygus normal form +option sygusNormalFormGlobal --sygus-nf-global bool :default true + narrow sygus search space based on global state of current candidate program option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions |