boolector/
option.rs

1//! This module exposes options which can be set on a `Btor` instance.
2
3/// Documentation for individual options and their possible values are
4/// more-or-less taken verbatim from the Boolector 3.0.0 docs.
5pub enum BtorOption {
6    /// Whether to generate a model (set of concrete solution values) for
7    /// satisfiable instances
8    ModelGen(ModelGen),
9    /// Enable/disable incremental mode. Note that the Boolector 3.0.0 docs say
10    /// that "disabling incremental usage is currently not supported".
11    Incremental(bool),
12    /// Set incremental mode for SMT-LIB v1 input. The default is
13    /// `IncrementalSMT1::Basic`.
14    IncrementalSMT1(IncrementalSMT1),
15    /// Input file format. The default is `InputFileFormat::Autodetect`.
16    InputFileFormat(InputFileFormat),
17    /// Format to output numbers in. The default is `NumberFormat::Binary`.
18    OutputNumberFormat(NumberFormat),
19    /// Output file format. The default is `FileFormat::BTOR`.
20    OutputFileFormat(OutputFileFormat),
21    /// Solver timeout. If `Some`, then operations lasting longer than the given
22    /// `Duration` will be aborted and return `SolverResult::Unknown`.
23    ///
24    /// If `None`, then any previously set solver timeout will be removed, and
25    /// there will be no time limit to solver operations.
26    SolverTimeout(Option<std::time::Duration>),
27    /// Solver engine. The default is `SolverEngine::Fun`.
28    SolverEngine(SolverEngine),
29    /// SAT solver. Each option requires that Boolector was compiled with support
30    /// for the corresponding solver.
31    SatEngine(SatEngine),
32    /// Enable/disable auto cleanup of all references held on exit.
33    AutoCleanup(bool),
34    /// Enable/disable pretty printing when dumping.
35    PrettyPrint(bool),
36    /// Seed for Boolector's internal random number generator. The default is 0.
37    Seed(u32),
38    /// Rewrite level. The default is `RewriteLevel::Full`.
39    ///
40    /// Boolector's docs say to not change this setting after creating expressions.
41    RewriteLevel(RewriteLevel),
42    /// Enable/disable skeleton preprocessing during simplification.
43    SkeletonPreproc(bool),
44    /// Enable/disable the eager addition of Ackermann constraints for function
45    /// applications.
46    Ackermann(bool),
47    /// Enable/disable the eager elimination of lambda expressions via beta
48    /// reduction.
49    BetaReduce(bool),
50    /// Enable/disable slice elimination on bit vector variables.
51    EliminateSlices(bool),
52    /// Enable/disable variable substitution during simplification.
53    VariableSubst(bool),
54    /// Enable/disable unconstrained optimization.
55    UnconstrainedOpt(bool),
56    /// Enable/disable merging of lambda expressions.
57    MergeLambdas(bool),
58    /// Enable/disable extraction of common array patterns as lambda terms.
59    ExtractLambdas(bool),
60    /// Enable/disable normalization of addition, multiplication, and bitwise
61    /// `and`.
62    Normalize(bool),
63    /// Enable/disable normalization of addition.
64    NormalizeAdd(bool),
65    /// For `SolverEngine::Fun`, enable/disable Prop engine preprocessing step
66    /// within sequential portfolio setting.
67    FunPreProp(bool),
68    /// For `SolverEngine::Fun`, enable/disable SLS engine preprocessing step
69    /// within sequential portfolio setting.
70    FunPreSLS(bool),
71    /// For `SolverEngine::Fun`, enable/disable dual propagation optimization.
72    FunDualProp(bool),
73    /// For `SolverEngine::Fun`, set the order in which inputs are assumed in
74    /// dual propagation clone. The default is `DualPropQsortOrder::Just`.
75    FunDualPropQsortOrder(DualPropQsortOrder),
76    /// For `SolverEngine::Fun`, enable/disable justification optimization.
77    FunJustification(bool),
78    /// For `SolverEngine::Fun`, set the path selection heuristic for
79    /// justification optimization. The default is
80    /// `JustificationHeuristic::MinApp`.
81    FunJustificationHeuristic(JustificationHeuristic),
82    /// For `SolverEngine::Fun`, enable/disable lazy synthesis of bitvector
83    /// expressions.
84    FunLazySynthesize(bool),
85    /// For `SolverEngine::Fun`, enable/disable eager generation of lemmas.
86    FunEagerLemmas(EagerLemmas),
87    /// For `SolverEngine::SLS`, set the number of bit flips used as a limit.
88    /// `0` indicates no limit.
89    SLSNumFlips(u32),
90    /// For `SolverEngine::SLS`, set the move strategy. The default is
91    /// `SLSMoveStrategy::BestMove`.
92    SLSMoveStrategy(SLSMoveStrategy),
93    /// For `SolverEngine::SLS`, enable/disable justification-based path
94    /// selection during candidate selection.
95    SLSJustification(bool),
96    /// For `SolverEngine::SLS`, enable/disable group-wise moves, where rather
97    /// than changing the assignment of one single candidate variable, all
98    /// candidate variables are set at the same time (using the same strategy).
99    SLSGroupWiseMoves(bool),
100    /// For `SolverEngine::SLS`, enable/disable range-wise bitflip moves, where
101    /// the bits within all ranges from 2 to the bitwidth (starting from the LSB)
102    /// are flipped at once.
103    SLSRangeWiseMoves(bool),
104    /// For `SolverEngine::SLS`, enable/disable segment-wise bitflip moves, where
105    /// the bits within segments of multiples of 2 are flipped at once.
106    SLSSegmentWiseMoves(bool),
107    /// For `SolverEngine::SLS`, enable/disable random walk moves, where one out
108    /// of all possible neighbors is randomly selected for a randomly selected
109    /// candidate variable.
110    SLSRandomWalkMoves(bool),
111    /// For `SolverEngine::SLS`, set the probability with which a random walk is
112    /// chosen if `SLSRandomWalkMoves` is enabled.
113    SLSRandomWalkProbability(u32),
114    /// For `SolverEngine::SLS`, enable/disable the randomization of all
115    /// candidate variables (rather than a single randomly selected candidate
116    /// variable) in case no best move has been found.
117    SLSRandomizeAll(bool),
118    /// For `SolverEngine::SLS`, enable/disable the randomization of bit ranges
119    /// (rather than all bits) of candidate variable(s) to be randomized in case
120    /// no best move has been found.
121    SLSRandomizeRange(bool),
122    /// For `SolverEngine::SLS`, enable/disable propagation moves.
123    SLSPropagationMoves(bool),
124    /// For `SolverEngine::SLS` when propagation moves are enabled, set the
125    /// number of propagation moves to be performed (this forms a ratio with
126    /// `SLSPropagationMovesNumRegular`).
127    SLSPropagationMovesNumProp(u32),
128    /// For `SolverEngine::SLS` when propagation moves are enabled, set the
129    /// number of regular moves to be performed (this forms a ratio with
130    /// `SLSPropagationMovesNumProp`).
131    SLSPropagationMovesNumRegular(u32),
132    /// For `SolverEngine::SLS`, enable/disable forcibly choosing random walks as
133    /// recovery moves when conflicts occur after a propagation move.
134    SLSForceRandomWalks(bool),
135    /// For `SolverEngine::SLS`, enable/disable that during best move selection,
136    /// if the current candidate variable with a previous neighbor yields the
137    /// currently best score, this neighbor assignment is used as a base for
138    /// further neighborhood exploration (rather than its current assignment).
139    SLSIncMoveTest(bool),
140    /// For `SolverEngine::SLS`, enable/disable restarts.
141    SLSRestarts(bool),
142    /// For `SolverEngine::SLS`, enable/disable the "bandit scheme" for selecting
143    /// root constraints. If disabled, candidate root constraints are selected
144    /// randomly.
145    SLSBanditScheme(bool),
146    /// For `SolverEngine::Prop`, set the number of propagation steps used as a
147    /// limit. `0` indicates no limit.
148    PropNumSteps(u32),
149    /// For `SolverEngine::Prop`, enable/disable restarts.
150    PropRestarts(bool),
151    /// For `SolverEngine::Prop`, enable/disable the "bandit scheme" for
152    /// selecting root constraints. If disabled, candidate root constraints are
153    /// selected randomly.
154    PropBanditScheme(bool),
155    /// For `SolverEngine::Prop`, choose the mode for path selection.
156    /// The default is `PropPathSelection::Essential`.
157    PropPathSelectionMode(PropPathSelection),
158    /// For `SolverEngine::Prop`, set the probability with which to choose
159    /// inverse values over consistent values.
160    PropInvValueProbability(u32),
161    /// For `SolverEngine::Prop`, set the probability with which to select the
162    /// path to the condition (in case of an if-then-else operation) rather than
163    /// the enabled branch during down propagation.
164    PropFlipConditionProbability(u32),
165    /// Like `PropFlipConditionProbability`, but for the case that either the
166    /// 'then' or 'else' branch is constant.
167    PropFlipConditionProbabilityConstant(u32),
168    /// For `SolverEngine::Prop`, set the limit for how often the path to the
169    /// condition may be selected before `PropFlipConditionProbabilityConstant`
170    /// is decreased or increased by `PropFlipConditionProbabilityConstantDelta`.
171    PropFlipConditionNumPaths(u32),
172    /// For `SolverEngine::Prop`, set the delta by which
173    /// `PropFlipConditionProbabilityConstant` is decreased or increased after
174    /// `PropFlipConditionNumPaths` is reached.
175    PropFlipConditionProbabilityConstantDelta(u32),
176    /// For `SolverEngine::Prop`, set the probability with which to keep the
177    /// current value of the don't care bits of a slice operation (rather than
178    /// fully randomizing all of them) when selecting an inverse or consistent
179    /// value.
180    PropSliceKeepDCProbability(u32),
181    /// For `SolverEngine::Prop`, set the probability with which to use the
182    /// corresponding slice of the current assignment with at most one of its
183    /// bits flipped as the result of consistent value selection for concats.
184    PropConcatFlipProbability(u32),
185    /// For `SolverEngine::Prop`, set the probability with which to use the
186    /// current assignment of the operand of a slice operation with one of the
187    /// don't care bits flipped, unless their current assignment is kept by
188    /// `PropSliceKeepDCProbability`.
189    PropSliceFlipProbability(u32),
190    /// For `SolverEngine::Prop`, set the probability with which the current
191    /// assignment of the selected node with one of its bits flipped (rather than
192    /// a fully randomized bitvector) is down-propagated in the case of an
193    /// inequality.
194    PropEqFlipProbability(u32),
195    /// For `SolverEngine::Prop`, set the probability with which the current
196    /// assignment of the don't care bits of the selected node with at most one
197    /// of its bits flipped in case of an `and` operation.
198    PropAndFlipProbability(u32),
199    /// For `SolverEngine::AIGProp`, enable/disable restarts.
200    AIGPropUseRestarts(bool),
201    /// For `SolverEngine::AIGProp`, select the synthesis mode for Skolem
202    /// functions.
203    AIGPropQuantSynthesis(AIGPropQuantSynthesis),
204    /// For `SolverEngine::AIGProp`, enable/disable solving the dual (negated)
205    /// version of the quantified bit-vector formula.
206    AIGPropQuantDualSolver(bool),
207    /// For `SolverEngine::AIGProp`, set the limit of enumerated expressions
208    /// for the enumerative learning synthesis algorithm.
209    AIGPropQuantSynthLimit(u32),
210    /// For `SolverEngine::AIGProp`, enable/disable generalization of
211    /// quantifier instantiations via enumerative learning.
212    AIGPropSynthQI(bool),
213    /// For `SolverEngine::AIGProp`, enable/disable destructive equality
214    /// resolution simplification.
215    AIGPropQuantDER(bool),
216    /// For `SolverEngine::AIGProp`, enable/disable constructive equality
217    /// resolution simplification.
218    AIGPropQuantCER(bool),
219    /// For `SolverEngine::AIGProp`, enable/disable miniscoping.
220    AIGPropQuantMiniscope(bool),
221}
222
223pub enum ModelGen {
224    /// Do not generate models
225    Disabled,
226    /// Generate models for asserted expressions only
227    Asserted,
228    /// Generate models for all expressions
229    All,
230}
231
232pub enum IncrementalSMT1 {
233    /// Stop after first satisfiable formula
234    Basic,
235    /// Solve all formulas
236    Continue,
237}
238
239pub enum InputFileFormat {
240    Autodetect,
241    Btor,
242    Btor2,
243    SMTLIBv1,
244    SMTLIBv2,
245}
246
247pub enum NumberFormat {
248    Binary,
249    Decimal,
250    Hexadecimal,
251}
252
253pub enum OutputFileFormat {
254    BTOR,
255    SMTLIBv2,
256    AigerASCII,
257    AigerBinary,
258}
259
260pub enum SolverEngine {
261    /// Default engine for all combinations of QF_AUFBV; uses lemmas on demand
262    /// for QF_AUFBV and eager bit-blasting for QF_BV
263    Fun,
264    /// Score-based local search QF_BV engine
265    SLS,
266    /// Propagation-based local search QF_BV engine
267    Prop,
268    /// Propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG layer)
269    AIGProp,
270    /// Quantifier engine (BV only)
271    Quant,
272}
273
274pub enum SatEngine {
275    /// CaDiCaL
276    CaDiCaL,
277    /// CryptoMiniSat
278    CMS,
279    /// Lingeling
280    Lingeling,
281    /// MiniSAT
282    MiniSAT,
283    /// PicoSAT
284    PicoSAT,
285}
286
287pub enum RewriteLevel {
288    /// "no rewriting"
289    None,
290    /// "term level rewriting"
291    TermLevel,
292    /// "more simplification techniques"
293    More,
294    /// "full rewriting/simplification"
295    Full,
296}
297
298pub enum DualPropQsortOrder {
299    /// Order by score, highest score first
300    Just,
301    /// Order by input id, ascending
302    Asc,
303    /// Order by input id, descending
304    Desc,
305}
306
307pub enum JustificationHeuristic {
308    /// Always choose the left branch
309    Left,
310    /// Choose the branch with the minimum number of applies
311    MinApp,
312    /// Choose the branch with the minimum depth
313    MinDepth,
314}
315
316pub enum EagerLemmas {
317    /// Do not generate lemmas eagerly (generate one single lemma per refinement
318    /// iteration)
319    None,
320    /// Only generate lemmas eagerly until the first conflict dependent on
321    /// another conflict is found
322    Conf,
323    /// In each refinement iterations, generate lemmas for all conflicts
324    All,
325}
326
327pub enum SLSMoveStrategy {
328    /// Always choose the best score improving move
329    BestMove,
330    /// Perform a random walk weighted by score
331    RandomWalk,
332    /// Always choose the first best move, even if another move may be better
333    FirstBestMove,
334    /// Choose a move even if its score is not better but the same as the score
335    /// of the previous best move
336    BestSameMove,
337    /// Always choose propagation move, and recover with SLS move in case of
338    /// conflict
339    AlwaysProp,
340}
341
342pub enum PropPathSelection {
343    /// Select path based on controlling inputs
344    Controlling,
345    /// Select path based on essential inputs
346    Essential,
347    /// Select path based on random inputs
348    Random,
349}
350
351pub enum AIGPropQuantSynthesis {
352    /// Do not synthesize skolem functions (use model values for instantiation)
353    None,
354    /// Use enumerative learning to synthesize skolem functions
355    EL,
356    /// Use enumerative learning modulo the predicates in the cone of influence
357    /// of the existential variables to synthesize skolem functions
358    ELMC,
359    /// Chain the `EL` and `ELMC` approaches to synthesize skolem functions
360    ELELMC,
361    /// Use enumerative learning modulo the given root constraints to synthesize
362    /// skolem functions
363    ELMR,
364}
boolector/option.rs

boolector/
option.rs
