diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e34465d9b..231392a9a 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -19,7 +19,7 @@ option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write disable miniscope quantifiers for ground subformulas # Whether to prenex (nested universal) quantifiers option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToPrenexQuantMode :handler-include "theory/quantifiers/options_handlers.h" - disable prenexing of quantified formulas + prenex mode for quantified formulas # Whether to variable-eliminate quantifiers. # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to # forall y. P( c, y ) @@ -27,13 +27,16 @@ option varElimQuant --var-elim-quant bool :default true disable simple variable elimination for quantified formulas option dtVarExpandQuant --dt-var-exp-quant bool :default true expand datatype variables bound to one constructor in quantifiers +#ite lift mode for quantified formulas +option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "theory/quantifiers/modes.h" :read-write :handler CVC4::theory::quantifiers::stringToIteLiftQuantMode :handler-include "theory/quantifiers/options_handlers.h" + ite lifting mode for quantified formulas option iteCondVarSplitQuant --ite-cond-var-split-quant bool :default true split variables occurring as conditions of ITE in quantifiers -option simpleIteLiftQuant --ite-lift-quant bool :default true - disable simple ite lifting for quantified formulas +option iteDtTesterSplitQuant --ite-dtt-split-quant bool :default false + split ites with dt testers as conditions # Whether to CNF quantifier bodies -option cnfQuant --cnf-quant bool :default false - apply CNF conversion to quantified formulas +# option cnfQuant --cnf-quant bool :default false +# apply CNF conversion to quantified formulas # Whether to NNF quantifier bodies option nnfQuant --nnf-quant bool :default true apply NNF conversion to quantified formulas @@ -159,6 +162,8 @@ option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode : when to invoke conflict find mechanism for quantifiers option qcfTConstraint --qcf-tconstraint bool :read-write :default false enable entailment checks for t-constraints in qcf algorithm +option qcfAllConflict --qcf-all-conflict bool :read-write :default false + add all available conflicting instances during conflict-based instantiation option instNoEntail --inst-no-entail bool :read-write :default true do not consider instances of quantified formulas that are currently entailed @@ -191,7 +196,7 @@ option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write filter based on canonicity option conjectureFilterModel --conjecture-filter-model bool :read-write :default true filter based on model -option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 0 +option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50 number of ground terms to generate for model filtering option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false more aggressive merging for universal equality engine, introduces terms |