diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-01 20:54:28 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-02-01 20:54:28 +0100 |
| commit | 011cd46ecf51502344b568c2613f420691724c83 (patch) | |
| tree | 8b6a40af787923dc1f8469b9d1535d579e2a2476 /src/theory/quantifiers | |
| parent | 1c78459ede8c4668a0f7d14a63d4505fdb7a4472 (diff) | |
Generalization of sygus lemmas based on arguments and content.
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/options | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 4a093b617..92285bf12 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -202,10 +202,14 @@ 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 +option sygusNormalFormGlobal --sygus-nf-sym bool :default true narrow sygus search space based on global state of current candidate program -option sygusNormalFormGlobalGen --sygus-nf-global-gen bool :default true - generalize conflict lemmas for global search space narrowing +option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true + generalize lemmas for global search space narrowing +option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true + generalize based on arguments in global search space narrowing +option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true + generalize based on content in global search space narrowing option localTheoryExt --local-t-ext bool :default false do instantiation based on local theory extensions |