diff options
Diffstat (limited to 'src/theory/quantifiers/options')
| -rw-r--r-- | src/theory/quantifiers/options | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 91e831092..a28ccb423 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -45,13 +45,13 @@ option smartTriggers /--disable-smart-triggers bool :default true 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" +option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "theory/quantifiers/modes.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" +option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.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 @@ -67,23 +67,23 @@ option flipDecision --enable-flip-decision/ bool :default false 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 fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false + only add instantiations for one 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) +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 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 endmodule |