diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 14:53:19 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-01-23 14:53:19 +0100 |
| commit | 97d43d56d74f3af68d1d022c66ee158a41b24757 (patch) | |
| tree | d8a4871505bf1b94558046d53f6280ac90d454d8 /src/theory/quantifiers/options | |
| parent | 7ff0098a91df9c912cbe98fb128fcf2cbc71e95c (diff) | |
CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied selectors.
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 009a0ada6..560e29c3b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -198,7 +198,7 @@ option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMo if and how to apply fairness for cegqi option sygusDecompose --sygus-decompose bool :default false decompose single invocation synthesis conjectures -option sygusNormalForm --sygus-normal-form bool :default true +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 |