src/theory/quantifiers/options

   1 #
   2 # Option specification file for CVC4
   3 # See src/options/base_options for a description of this file format
   4 #
   5
   6 module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
   7
   8 # Whether to mini-scope quantifiers.
   9 # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
  10 # ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
  11 option miniscopeQuant /--disable-miniscope-quant bool :default true
  12  disable miniscope quantifiers
  13
  14 # Whether to mini-scope quantifiers based on formulas with no free variables.
  15 # For example, forall x. ( P( x ) V Q ) will be rewritten to
  16 # ( forall x. P( x ) ) V Q
  17 option miniscopeQuantFreeVar /--disable-miniscope-quant-fv bool :default true
  18  disable miniscope quantifiers for ground subformulas
  19
  20 # Whether to prenex (nested universal) quantifiers
  21 option prenexQuant /--disable-prenex-quant bool :default true
  22  disable prenexing of quantified formulas
  23
  24 # Whether to variable-eliminate quantifiers.
  25 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
  26 #   forall y. P( c, y )
  27 option varElimQuant /--disable-var-elim-quant bool :default true
  28  disable simple variable elimination for quantified formulas
  29
  30 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
  31  disable simple ite lifting for quantified formulas
  32
  33 # Whether to CNF quantifier bodies
  34 option cnfQuant --cnf-quant bool :default false
  35  apply CNF conversion to quantified formulas
  36
  37 option clauseSplit --clause-split bool :default false
  38  apply clause splitting to quantified formulas
  39
  40 # Whether to pre-skolemize quantifier bodies.
  41 # For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
  42 #   forall x. P( x ) => f( S( x ) ) = x
  43 option preSkolemQuant --pre-skolem-quant bool :read-write :default false
  44  apply skolemization eagerly to bodies of quantified formulas
  45 # Whether to perform agressive miniscoping
  46 option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
  47  perform aggressive miniscoping for quantifiers
  48 # Whether to perform quantifier macro expansion
  49 option macrosQuant --macros-quant bool :default false
  50  perform quantifiers macro expansions
  51 # Whether to perform first-order propagation
  52 option foPropQuant --fo-prop-quant bool :default false
  53  perform first-order propagation on quantifiers
  54
  55 # Whether to use smart triggers
  56 option smartTriggers /--disable-smart-triggers bool :default true
  57  disable smart triggers
  58 # Whether to use relevent triggers
  59 option relevantTriggers --relevant-triggers bool :default false
  60  prefer triggers that are more relevant based on SInE style analysis
  61 option relationalTriggers --relational-triggers bool :default false
  62  choose relational triggers such as x = f(y), x >= f(y)
  63
  64 # Whether to consider terms in the bodies of quantifiers for matching
  65 option registerQuantBodyTerms --register-quant-body-terms bool :default false
  66  consider ground terms within bodies of quantified formulas for matching
  67
  68 option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :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"
  69  when to apply instantiation
  70 option instMaxLevel --inst-max-level=N int :default -1
  71  maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
  72
  73 option eagerInstQuant --eager-inst-quant bool :default false
  74  apply quantifier instantiation eagerly
  75
  76 option fullSaturateQuant --full-saturate-quant bool :default false
  77  when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
  78
  79 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"
  80  choose literal matching mode
  81
  82 option cbqi --enable-cbqi bool :default false
  83  turns on counterexample-based quantifier instantiation
  84
  85 option recurseCbqi --cbqi-recurse bool :default false
  86  turns on recursive counterexample-based quantifier instantiation
  87
  88 option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToUserPatMode :handler-include "theory/quantifiers/options_handlers.h"
  89  policy for handling user-provided patterns for quantifier instantiation
  90
  91 option flipDecision --flip-decision/ bool :default false
  92  turns on flip decision heuristic
  93
  94 option internalReps /--disable-quant-internal-reps bool :default true
  95  disables instantiating with representatives chosen by quantifiers engine
  96
  97 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
  98  use finite model finding heuristic for quantifier instantiation
  99
 100 option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h"
 101  choose mode for model-based quantifier instantiation
 102 option fmfOneInstPerRound --mbqi-one-inst-per-round bool :default false
 103  only add one instantiation per quantifier per round for mbqi
 104 option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
 105  only add instantiations for one quantifier per round for mbqi
 106
 107 option fmfInstEngine --fmf-inst-engine bool :default false
 108  use instantiation engine in conjunction with finite model finding
 109 option fmfInstGen /--disable-fmf-inst-gen bool :default true
 110  disable Inst-Gen instantiation techniques for finite model finding
 111 option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
 112  only perform Inst-Gen instantiation techniques on one quantifier per round
 113 option fmfFreshDistConst --fmf-fresh-dc bool :default false
 114  use fresh distinguished representative when applying Inst-Gen techniques
 115 option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true
 116  disable simple models in full model check for finite model finding
 117 option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
 118  finite model finding on bounded integer quantification
 119
 120 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"
 121  policy for instantiating axioms
 122
 123 option quantConflictFind --quant-cf bool :read-write :default false
 124  enable conflict find mechanism for quantifiers
 125 option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfMode :handler-include "theory/quantifiers/options_handlers.h"
 126  what effort to apply conflict find mechanism
 127 option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h"
 128  when to invoke conflict find mechanism for quantifiers
 129 option qcfTConstraint --qcf-tconstraint bool :read-write :default false
 130  enable entailment checks for t-constraints in qcf algorithm
 131
 132 option quantRewriteRules --rewrite-rules bool :default true
 133  use rewrite rules module
 134 option rrOneInstPerRound --rr-one-inst-per-round bool :default false
 135  add one instance of rewrite rule per round
 136
 137 option dtStcInduction --dt-stc-ind bool :default false
 138  apply strengthening for existential quantification over datatypes based on structural induction
 139
 140 endmodule