blob: a0e42c425854b1197f19c357d368d781bbb9cac4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
#
# 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 /--disable-var-elim-quant bool :default true
disable simple variable elimination for quantified formulas
# Whether to CNF quantifier bodies
option cnfQuant --cnf-quant bool :default false
apply CNF conversion to quantified formulas
option clauseSplit --clause-split bool :default false
apply clause splitting 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
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
# Whether to perform first-order propagation
option foPropQuant --fo-prop-quant bool :default false
perform first-order propagation on quantifiers
# Whether to use smart triggers
option smartTriggers /--disable-smart-triggers bool :default true
disable smart triggers
# Whether to use relevent triggers
option relevantTriggers /--disable-relevant-triggers bool :default true
prefer triggers that are more relevant based on SInE style analysis
option relationalTriggers --relational-triggers bool :default false
choose relational triggers such as x = f(y), x >= f(y)
# 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 :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/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
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
disables instantiating with representatives chosen by quantifiers engine
option finiteModelFind --finite-model-find bool :default false
use finite model finding heuristic for quantifier instantiation
option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
disable model-based quantifier instantiation for finite model finding
option fmfFullModelCheck --fmf-fmc bool :default false
enable full model check for finite model finding
option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
disable simple models in full model check 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 fmfNewInstGen --fmf-new-inst-gen bool :default false
use new inst gen technique for answering sat without exhaustive instantiation
option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
enable Inst-Gen instantiation techniques for finite model finding (default)
/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 fmfBoundInt --fmf-bound-int bool :default false
finite model finding on bounded integer quantification
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
|
