diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 89 |
1 files changed, 89 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options new file mode 100644 index 000000000..91e831092 --- /dev/null +++ b/src/theory/quantifiers/options @@ -0,0 +1,89 @@ +# +# Option specification file for CVC4 +# See src/options/base_options for a description of this file format +# + +module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers + +# Whether to mini-scope quantifiers. +# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to +# ( forall x. P( x ) ) ^ ( forall x. Q( x ) ) +option miniscopeQuant /--disable-miniscope-quant bool :default true + disable miniscope quantifiers + +# Whether to mini-scope quantifiers based on formulas with no free variables. +# For example, forall x. ( P( x ) V Q ) will be rewritten to +# ( forall x. P( x ) ) V Q +option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true + disable miniscope quantifiers for ground subformulas + +# Whether to prenex (nested universal) quantifiers +option prenexQuant /--disable-prenex-quant bool :default true + disable prenexing of 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 ) +option varElimQuant --var-elim-quant bool :default false + enable variable elimination of quantified formulas + +# Whether to CNF quantifier bodies +option cnfQuant --cnf-quant bool :default false + apply CNF conversion to quantified formulas + +# Whether to pre-skolemize quantifier bodies. +# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to +# forall x. P( x ) => f( S( x ) ) = x +option preSkolemQuant --pre-skolem-quant bool :default false + apply skolemization eagerly to bodies of quantified formulas + +# Whether to use smart triggers +option smartTriggers /--disable-smart-triggers bool :default true + disable smart triggers + +# Whether to consider terms in the bodies of quantifiers for matching +option registerQuantBodyTerms --register-quant-body-terms bool :default false + consider ground terms within bodies of quantified formulas for matching + +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :include "theory/quantifiers/inst_when_mode.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h" + when to apply instantiation + +option eagerInstQuant --eager-inst-quant bool :default false + apply quantifier instantiation eagerly + +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/literal_match_mode.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h" + choose literal matching mode + +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 --enable-flip-decision/ bool :default false + turns on flip decision heuristic + +option finiteModelFind --finite-model-find bool :default false + use finite model finding heuristic for quantifier instantiation + +option ufssRegions /--disable-uf-ss-regions bool :default true + disable region-based method for discovering cliques and splits in uf strong solver +option ufssEagerSplits --uf-ss-eager-split bool :default false + add splits eagerly for uf strong solver +option ufssColoringSat --uf-ss-coloring-sat bool :default false + use coloring-based SAT heuristic for uf strong solver + +option fmfModelBasedInst /--disable-fmf-mbqi bool :default true + disable model-based quantifier instantiation for finite model finding + +option fmfInstGen /--disable-fmf-inst-gen bool :default true + disable Inst-Gen instantiation techniques for finite model finding +option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false + only add one instantiation per quantifier per round for fmf +option fmfInstEngine --fmf-inst-engine bool :default false + use instantiation engine in conjunction with finite model finding +option fmfRelevantDomain --fmf-relevant-domain bool :default false + use relevant domain computation, similar to complete instantiation (Ge, deMoura 09) + +endmodule |