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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
|
#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#
module SMT "options/smt_options.h" SMT layer
common-option dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode
dump preprocessed assertions, etc., see --dump=help
common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile
all dumping goes to FILE (instead of stdout)
expert-option forceLogicString force-logic --force-logic=LOGIC std::string :default "" :notify notifyForceLogic
set the logic, and override all further user attempts to change it
option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h"
choose simplification mode, see --simplification=help
alias --no-simplification = --simplification=none
turn off all simplification (same as --simplification=none)
option doStaticLearning static-learning --static-learning bool :default true
use static learning (on by default)
option expandDefinitions expand-definitions bool :default false
always expand symbol definitions in output
common-option produceModels produce-models -m --produce-models bool :default false :notify notifyBeforeSearch
support the get-value and get-model commands
option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :notify notifyBeforeSearch
after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models
output models after every SAT/INVALID/UNKNOWN response
option omitDontCares --omit-dont-cares bool :default false
When producing a model, omit variables whose value does not matter
option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch
turn on proof generation
option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate LFSCEnabledBuild :notify notifyBeforeSearch :read-write
after UNSAT/VALID, machine-check the generated proof
option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs
output proofs after every UNSAT/VALID response
option dumpInstantiations --dump-instantiations bool :default false
output instantiations of quantified formulas after every UNSAT/VALID response
option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
output mode for sygus
option sygusPrintCallbacks --sygus-print-callbacks bool :default true
use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)
option dumpSynth --dump-synth bool :read-write :default false
output solution for synthesis conjectures after every UNSAT/VALID response
option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
turn on unsat core generation
option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
after UNSAT/VALID, produce and check an unsat core (expensive)
option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :notify notifyBeforeSearch
output unsat cores after every UNSAT/VALID response
option dumpUnsatCoresFull dump-unsat-cores-full --dump-unsat-cores-full bool :default false :link --dump-unsat-cores :link-smt dump-unsat-cores :notify notifyBeforeSearch
dump the full unsat core, including unlabeled assertions
option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch
support the get-assignment command
undocumented-option interactiveMode interactive-mode bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
deprecated name for produce-assertions
common-option produceAssertions produce-assertions --produce-assertions bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
keep an assertions list (enables get-assertions command)
option doITESimp --ite-simp bool :read-write
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
do the ite simplification pass again if repeating simplification
option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
enables simplifyWithCare in ite simplificiation
option compressItes --simp-ite-compress bool :default false :read-write
enables compressing ites after ite simplification
option unconstrainedSimp --unconstrained-simp bool :default false :read-write
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
option repeatSimp --repeat-simp bool :read-write
make multiple passes with nonclausal simplifier
option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
post ite compression enables zombie removal while the number of nodes is above this threshold
option sortInference --sort-inference bool :read-write :default false
calculate sort inference of input problem, convert the input based on monotonic sorts
common-option incrementalSolving incremental -i --incremental bool :default true
enable incremental solving
option abstractValues abstract-values --abstract-values bool :default false
in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
option modelUninterpDtEnum --model-u-dt-enum bool :default false
in models, output uninterpreted sorts as datatype enumerations
option regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel
set the regular output channel of the solver
option diagnosticChannelName diagnostic-output-channel std::string :notify notifySetDiagnosticOutputChannel
set the diagnostic output channel of the solver
common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler tlimitHandler :notify notifyTlimit
enable time limiting (give milliseconds)
common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" :handler tlimitPerHandler :notify notifyTlimitPer
enable time limiting per query (give milliseconds)
common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler rlimitHandler :notify notifyRlimit
enable resource limiting (currently, roughly the number of SAT conflicts)
common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler rlimitPerHandler :notify notifyRlimitPer
enable resource limiting per query
common-option hardLimit hard-limit --hard-limit bool :default false
the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
common-option cpuTime cpu-time --cpu-time bool :default false
measures CPU time if set to true and wall time if false (default false)
# Resource spending options for SPARK
expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
amount of resources spent for each rewrite step
expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
amount of resources spent for each theory check call
expert-option decisionStep decision-step --decision-step unsigned :default 1
amount of getNext decision calls in the decision engine
expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
amount of resources spent for each bitblast step
expert-option parseStep parse-step --parse-step unsigned :default 1
amount of resources spent for each command/expression parsing
expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
amount of resources spent when adding lemmas
expert-option restartStep restart-step --restart-step unsigned :default 1
amount of resources spent for each theory restart
expert-option cnfStep cnf-step --cnf-step unsigned :default 1
amount of resources spent for each call to cnf conversion
expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
amount of resources spent for each preprocessing step in SmtEngine
expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
amount of resources spent for quantifier instantiations
expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
amount of resources spent for each sat conflict (main sat solver)
expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
amount of resources spent for each sat conflict (bitvectors)
expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
# --replay is currently broken; don't document it for 1.0
undocumented-option replayInputFilename --replay=FILE std::string :handler checkReplayFilename
replay decisions from file
# --replay is currently broken; don't document it for 1.0
undocumented-option replayLogFilename --replay-log=FILE std::string :handler checkReplayFilename :notify notifySetReplayLogFilename :notify notifyBeforeSearch
replay decisions from file
option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
Force no CPU limit when dumping models and proofs
undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0
attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)
undocumented-option solveRealAsInt --solve-real-as-int bool :default false
attempt to solve a pure real satisfiable problem as a integer problem (for non-linear)
endmodule
|
