2 # Option specification file for CVC4
3 # See src/options/base_options for a description of this file format
6 module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers
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
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
20 # Whether to prenex (nested universal) quantifiers
21 option prenexQuant /--disable-prenex-quant bool :default true
22 disable prenexing of quantified formulas
24 # Whether to variable-eliminate quantifiers.
25 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
27 option varElimQuant /--disable-var-elim-quant bool :default true
28 disable simple variable elimination for quantified formulas
30 option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
31 disable simple ite lifting for quantified formulas
33 # Whether to CNF quantifier bodies
34 option cnfQuant --cnf-quant bool :default false
35 apply CNF conversion to quantified formulas
37 option clauseSplit --clause-split bool :default false
38 apply clause splitting to quantified formulas
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
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)
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
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)
73 option eagerInstQuant --eager-inst-quant bool :default false
74 apply quantifier instantiation eagerly
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
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
82 option cbqi --enable-cbqi bool :default false
83 turns on counterexample-based quantifier instantiation
85 option recurseCbqi --cbqi-recurse bool :default false
86 turns on recursive counterexample-based quantifier instantiation
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
91 option flipDecision --flip-decision/ bool :default false
92 turns on flip decision heuristic
94 option internalReps /--disable-quant-internal-reps bool :default true
95 disables instantiating with representatives chosen by quantifiers engine
97 option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
98 use finite model finding heuristic for quantifier instantiation
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
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
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
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
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
137 option dtStcInduction --dt-stc-ind bool :default false
138 apply strengthening for existential quantification over datatypes based on structural induction