diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index bc45e6051..222fc4425 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -36,7 +36,11 @@ option cnfQuant --cnf-quant bool :default false # forall x. P( x ) => f( S( x ) ) = x option preSkolemQuant --pre-skolem-quant bool :default false apply skolemization eagerly to bodies of quantified formulas - +option iteRemoveQuant --ite-remove-quant bool :default false + apply ite removal to bodies of quantifiers +# Whether to perform agressive miniscoping +option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false + perform aggressive miniscoping for quantifiers # Whether to perform quantifier macro expansion option macrosQuant --macros-quant bool :default false perform quantifiers macro expansions @@ -45,8 +49,8 @@ option macrosQuant --macros-quant bool :default false option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers -option relevantTriggers /--relevant-triggers bool :default true - prefer triggers that are more relevant based on SInE style method +option relevantTriggers /--disable-relevant-triggers bool :default true + prefer triggers that are more relevant based on SInE style analysis # Whether to consider terms in the bodies of quantifiers for matching option registerQuantBodyTerms --register-quant-body-terms bool :default false @@ -65,13 +69,14 @@ option cbqi --enable-cbqi/--disable-cbqi bool :default false turns on counterexample-based quantifier instantiation [off by default] /turns off counterexample-based quantifier instantiation + option userPatternsQuant /--ignore-user-patterns bool :default true ignore user-provided patterns for quantifier instantiation option flipDecision --flip-decision/ bool :default false turns on flip decision heuristic -option internalReps --disable-quant-internal-reps/ bool :default true +option internalReps /--disable-quant-internal-reps bool :default true disables instantiating with representatives chosen by quantifiers engine option finiteModelFind --finite-model-find bool :default false @@ -94,6 +99,8 @@ option fmfInstGen /--disable-fmf-inst-gen bool :default true disable Inst-Gen instantiation techniques for finite model finding option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false only perform Inst-Gen instantiation techniques on one quantifier per round +option fmfFreshDistConst --fmf-fresh-dc bool :default false + use fresh distinguished representative when applying Inst-Gen techniques option axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h" policy for instantiating axioms |