diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:09:49 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-01 13:11:13 +0200 |
| commit | 3ac872f4a3f65bd1b38c1362b8ca9d351ed89333 (patch) | |
| tree | c62a424af1b419155af0f59612d376fc10e7a6b6 /src/theory/quantifiers/options | |
| parent | 9350915de95c1b569eea8262c4602708dfa6c3fa (diff) | |
Improvements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def. Add skolemization options.
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 62790432d..a529e37d0 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -44,6 +44,10 @@ option clauseSplit --clause-split bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :read-write :default false apply skolemization eagerly to bodies of quantified formulas +option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true + apply skolemization to nested quantified formulass +option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true + apply skolemization to quantified formulas aggressively # Whether to perform agressive miniscoping option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false perform aggressive miniscoping for quantifiers |