Enum boolector::option::BtorOption
source · [−]pub enum BtorOption {
Show 70 variants
ModelGen(ModelGen),
Incremental(bool),
IncrementalSMT1(IncrementalSMT1),
InputFileFormat(InputFileFormat),
OutputNumberFormat(NumberFormat),
OutputFileFormat(OutputFileFormat),
SolverTimeout(Option<Duration>),
SolverEngine(SolverEngine),
SatEngine(SatEngine),
AutoCleanup(bool),
PrettyPrint(bool),
Seed(u32),
RewriteLevel(RewriteLevel),
SkeletonPreproc(bool),
Ackermann(bool),
BetaReduce(bool),
EliminateSlices(bool),
VariableSubst(bool),
UnconstrainedOpt(bool),
MergeLambdas(bool),
ExtractLambdas(bool),
Normalize(bool),
NormalizeAdd(bool),
FunPreProp(bool),
FunPreSLS(bool),
FunDualProp(bool),
FunDualPropQsortOrder(DualPropQsortOrder),
FunJustification(bool),
FunJustificationHeuristic(JustificationHeuristic),
FunLazySynthesize(bool),
FunEagerLemmas(EagerLemmas),
SLSNumFlips(u32),
SLSMoveStrategy(SLSMoveStrategy),
SLSJustification(bool),
SLSGroupWiseMoves(bool),
SLSRangeWiseMoves(bool),
SLSSegmentWiseMoves(bool),
SLSRandomWalkMoves(bool),
SLSRandomWalkProbability(u32),
SLSRandomizeAll(bool),
SLSRandomizeRange(bool),
SLSPropagationMoves(bool),
SLSPropagationMovesNumProp(u32),
SLSPropagationMovesNumRegular(u32),
SLSForceRandomWalks(bool),
SLSIncMoveTest(bool),
SLSRestarts(bool),
SLSBanditScheme(bool),
PropNumSteps(u32),
PropRestarts(bool),
PropBanditScheme(bool),
PropPathSelectionMode(PropPathSelection),
PropInvValueProbability(u32),
PropFlipConditionProbability(u32),
PropFlipConditionProbabilityConstant(u32),
PropFlipConditionNumPaths(u32),
PropFlipConditionProbabilityConstantDelta(u32),
PropSliceKeepDCProbability(u32),
PropConcatFlipProbability(u32),
PropSliceFlipProbability(u32),
PropEqFlipProbability(u32),
PropAndFlipProbability(u32),
AIGPropUseRestarts(bool),
AIGPropQuantSynthesis(AIGPropQuantSynthesis),
AIGPropQuantDualSolver(bool),
AIGPropQuantSynthLimit(u32),
AIGPropSynthQI(bool),
AIGPropQuantDER(bool),
AIGPropQuantCER(bool),
AIGPropQuantMiniscope(bool),
}
Expand description
Documentation for individual options and their possible values are more-or-less taken verbatim from the Boolector 3.0.0 docs.
Variants
ModelGen(ModelGen)
Whether to generate a model (set of concrete solution values) for satisfiable instances
Incremental(bool)
Enable/disable incremental mode. Note that the Boolector 3.0.0 docs say that “disabling incremental usage is currently not supported”.
IncrementalSMT1(IncrementalSMT1)
Set incremental mode for SMT-LIB v1 input. The default is
IncrementalSMT1::Basic
.
InputFileFormat(InputFileFormat)
Input file format. The default is InputFileFormat::Autodetect
.
OutputNumberFormat(NumberFormat)
Format to output numbers in. The default is NumberFormat::Binary
.
OutputFileFormat(OutputFileFormat)
Output file format. The default is FileFormat::BTOR
.
SolverTimeout(Option<Duration>)
Solver timeout. If Some
, then operations lasting longer than the given
Duration
will be aborted and return SolverResult::Unknown
.
If None
, then any previously set solver timeout will be removed, and
there will be no time limit to solver operations.
SolverEngine(SolverEngine)
Solver engine. The default is SolverEngine::Fun
.
SatEngine(SatEngine)
SAT solver. Each option requires that Boolector was compiled with support for the corresponding solver.
AutoCleanup(bool)
Enable/disable auto cleanup of all references held on exit.
PrettyPrint(bool)
Enable/disable pretty printing when dumping.
Seed(u32)
Seed for Boolector’s internal random number generator. The default is 0.
RewriteLevel(RewriteLevel)
Rewrite level. The default is RewriteLevel::Full
.
Boolector’s docs say to not change this setting after creating expressions.
SkeletonPreproc(bool)
Enable/disable skeleton preprocessing during simplification.
Ackermann(bool)
Enable/disable the eager addition of Ackermann constraints for function applications.
BetaReduce(bool)
Enable/disable the eager elimination of lambda expressions via beta reduction.
EliminateSlices(bool)
Enable/disable slice elimination on bit vector variables.
VariableSubst(bool)
Enable/disable variable substitution during simplification.
UnconstrainedOpt(bool)
Enable/disable unconstrained optimization.
MergeLambdas(bool)
Enable/disable merging of lambda expressions.
ExtractLambdas(bool)
Enable/disable extraction of common array patterns as lambda terms.
Normalize(bool)
Enable/disable normalization of addition, multiplication, and bitwise
and
.
NormalizeAdd(bool)
Enable/disable normalization of addition.
FunPreProp(bool)
For SolverEngine::Fun
, enable/disable Prop engine preprocessing step
within sequential portfolio setting.
FunPreSLS(bool)
For SolverEngine::Fun
, enable/disable SLS engine preprocessing step
within sequential portfolio setting.
FunDualProp(bool)
For SolverEngine::Fun
, enable/disable dual propagation optimization.
FunDualPropQsortOrder(DualPropQsortOrder)
For SolverEngine::Fun
, set the order in which inputs are assumed in
dual propagation clone. The default is DualPropQsortOrder::Just
.
FunJustification(bool)
For SolverEngine::Fun
, enable/disable justification optimization.
FunJustificationHeuristic(JustificationHeuristic)
For SolverEngine::Fun
, set the path selection heuristic for
justification optimization. The default is
JustificationHeuristic::MinApp
.
FunLazySynthesize(bool)
For SolverEngine::Fun
, enable/disable lazy synthesis of bitvector
expressions.
FunEagerLemmas(EagerLemmas)
For SolverEngine::Fun
, enable/disable eager generation of lemmas.
SLSNumFlips(u32)
For SolverEngine::SLS
, set the number of bit flips used as a limit.
0
indicates no limit.
SLSMoveStrategy(SLSMoveStrategy)
For SolverEngine::SLS
, set the move strategy. The default is
SLSMoveStrategy::BestMove
.
SLSJustification(bool)
For SolverEngine::SLS
, enable/disable justification-based path
selection during candidate selection.
SLSGroupWiseMoves(bool)
For SolverEngine::SLS
, enable/disable group-wise moves, where rather
than changing the assignment of one single candidate variable, all
candidate variables are set at the same time (using the same strategy).
SLSRangeWiseMoves(bool)
For SolverEngine::SLS
, enable/disable range-wise bitflip moves, where
the bits within all ranges from 2 to the bitwidth (starting from the LSB)
are flipped at once.
SLSSegmentWiseMoves(bool)
For SolverEngine::SLS
, enable/disable segment-wise bitflip moves, where
the bits within segments of multiples of 2 are flipped at once.
SLSRandomWalkMoves(bool)
For SolverEngine::SLS
, enable/disable random walk moves, where one out
of all possible neighbors is randomly selected for a randomly selected
candidate variable.
SLSRandomWalkProbability(u32)
For SolverEngine::SLS
, set the probability with which a random walk is
chosen if SLSRandomWalkMoves
is enabled.
SLSRandomizeAll(bool)
For SolverEngine::SLS
, enable/disable the randomization of all
candidate variables (rather than a single randomly selected candidate
variable) in case no best move has been found.
SLSRandomizeRange(bool)
For SolverEngine::SLS
, enable/disable the randomization of bit ranges
(rather than all bits) of candidate variable(s) to be randomized in case
no best move has been found.
SLSPropagationMoves(bool)
For SolverEngine::SLS
, enable/disable propagation moves.
SLSPropagationMovesNumProp(u32)
For SolverEngine::SLS
when propagation moves are enabled, set the
number of propagation moves to be performed (this forms a ratio with
SLSPropagationMovesNumRegular
).
SLSPropagationMovesNumRegular(u32)
For SolverEngine::SLS
when propagation moves are enabled, set the
number of regular moves to be performed (this forms a ratio with
SLSPropagationMovesNumProp
).
SLSForceRandomWalks(bool)
For SolverEngine::SLS
, enable/disable forcibly choosing random walks as
recovery moves when conflicts occur after a propagation move.
SLSIncMoveTest(bool)
For SolverEngine::SLS
, enable/disable that during best move selection,
if the current candidate variable with a previous neighbor yields the
currently best score, this neighbor assignment is used as a base for
further neighborhood exploration (rather than its current assignment).
SLSRestarts(bool)
For SolverEngine::SLS
, enable/disable restarts.
SLSBanditScheme(bool)
For SolverEngine::SLS
, enable/disable the “bandit scheme” for selecting
root constraints. If disabled, candidate root constraints are selected
randomly.
PropNumSteps(u32)
For SolverEngine::Prop
, set the number of propagation steps used as a
limit. 0
indicates no limit.
PropRestarts(bool)
For SolverEngine::Prop
, enable/disable restarts.
PropBanditScheme(bool)
For SolverEngine::Prop
, enable/disable the “bandit scheme” for
selecting root constraints. If disabled, candidate root constraints are
selected randomly.
PropPathSelectionMode(PropPathSelection)
For SolverEngine::Prop
, choose the mode for path selection.
The default is PropPathSelection::Essential
.
PropInvValueProbability(u32)
For SolverEngine::Prop
, set the probability with which to choose
inverse values over consistent values.
PropFlipConditionProbability(u32)
For SolverEngine::Prop
, set the probability with which to select the
path to the condition (in case of an if-then-else operation) rather than
the enabled branch during down propagation.
PropFlipConditionProbabilityConstant(u32)
Like PropFlipConditionProbability
, but for the case that either the
‘then’ or ‘else’ branch is constant.
PropFlipConditionNumPaths(u32)
For SolverEngine::Prop
, set the limit for how often the path to the
condition may be selected before PropFlipConditionProbabilityConstant
is decreased or increased by PropFlipConditionProbabilityConstantDelta
.
PropFlipConditionProbabilityConstantDelta(u32)
For SolverEngine::Prop
, set the delta by which
PropFlipConditionProbabilityConstant
is decreased or increased after
PropFlipConditionNumPaths
is reached.
PropSliceKeepDCProbability(u32)
For SolverEngine::Prop
, set the probability with which to keep the
current value of the don’t care bits of a slice operation (rather than
fully randomizing all of them) when selecting an inverse or consistent
value.
PropConcatFlipProbability(u32)
For SolverEngine::Prop
, set the probability with which to use the
corresponding slice of the current assignment with at most one of its
bits flipped as the result of consistent value selection for concats.
PropSliceFlipProbability(u32)
For SolverEngine::Prop
, set the probability with which to use the
current assignment of the operand of a slice operation with one of the
don’t care bits flipped, unless their current assignment is kept by
PropSliceKeepDCProbability
.
PropEqFlipProbability(u32)
For SolverEngine::Prop
, set the probability with which the current
assignment of the selected node with one of its bits flipped (rather than
a fully randomized bitvector) is down-propagated in the case of an
inequality.
PropAndFlipProbability(u32)
For SolverEngine::Prop
, set the probability with which the current
assignment of the don’t care bits of the selected node with at most one
of its bits flipped in case of an and
operation.
AIGPropUseRestarts(bool)
For SolverEngine::AIGProp
, enable/disable restarts.
AIGPropQuantSynthesis(AIGPropQuantSynthesis)
For SolverEngine::AIGProp
, select the synthesis mode for Skolem
functions.
AIGPropQuantDualSolver(bool)
For SolverEngine::AIGProp
, enable/disable solving the dual (negated)
version of the quantified bit-vector formula.
AIGPropQuantSynthLimit(u32)
For SolverEngine::AIGProp
, set the limit of enumerated expressions
for the enumerative learning synthesis algorithm.
AIGPropSynthQI(bool)
For SolverEngine::AIGProp
, enable/disable generalization of
quantifier instantiations via enumerative learning.
AIGPropQuantDER(bool)
For SolverEngine::AIGProp
, enable/disable destructive equality
resolution simplification.
AIGPropQuantCER(bool)
For SolverEngine::AIGProp
, enable/disable constructive equality
resolution simplification.
AIGPropQuantMiniscope(bool)
For SolverEngine::AIGProp
, enable/disable miniscoping.
Auto Trait Implementations
impl RefUnwindSafe for BtorOption
impl Send for BtorOption
impl Sync for BtorOption
impl Unpin for BtorOption
impl UnwindSafe for BtorOption
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more