Enum boolector::option::BtorOption

pub enum BtorOption {
    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),
}

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.