//! This module exposes options which can be set on a `Btor` instance.
/// Documentation for individual options and their possible values are
/// more-or-less taken verbatim from the Boolector 3.0.0 docs.
pub enum BtorOption {
/// Whether to generate a model (set of concrete solution values) for
/// satisfiable instances
ModelGen(ModelGen),
/// Enable/disable incremental mode. Note that the Boolector 3.0.0 docs say
/// that "disabling incremental usage is currently not supported".
Incremental(bool),
/// Set incremental mode for SMT-LIB v1 input. The default is
/// `IncrementalSMT1::Basic`.
IncrementalSMT1(IncrementalSMT1),
/// Input file format. The default is `InputFileFormat::Autodetect`.
InputFileFormat(InputFileFormat),
/// Format to output numbers in. The default is `NumberFormat::Binary`.
OutputNumberFormat(NumberFormat),
/// Output file format. The default is `FileFormat::BTOR`.
OutputFileFormat(OutputFileFormat),
/// 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.
SolverTimeout(Option<std::time::Duration>),
/// Solver engine. The default is `SolverEngine::Fun`.
SolverEngine(SolverEngine),
/// SAT solver. Each option requires that Boolector was compiled with support
/// for the corresponding solver.
SatEngine(SatEngine),
/// Enable/disable auto cleanup of all references held on exit.
AutoCleanup(bool),
/// Enable/disable pretty printing when dumping.
PrettyPrint(bool),
/// Seed for Boolector's internal random number generator. The default is 0.
Seed(u32),
/// Rewrite level. The default is `RewriteLevel::Full`.
///
/// Boolector's docs say to not change this setting after creating expressions.
RewriteLevel(RewriteLevel),
/// Enable/disable skeleton preprocessing during simplification.
SkeletonPreproc(bool),
/// Enable/disable the eager addition of Ackermann constraints for function
/// applications.
Ackermann(bool),
/// Enable/disable the eager elimination of lambda expressions via beta
/// reduction.
BetaReduce(bool),
/// Enable/disable slice elimination on bit vector variables.
EliminateSlices(bool),
/// Enable/disable variable substitution during simplification.
VariableSubst(bool),
/// Enable/disable unconstrained optimization.
UnconstrainedOpt(bool),
/// Enable/disable merging of lambda expressions.
MergeLambdas(bool),
/// Enable/disable extraction of common array patterns as lambda terms.
ExtractLambdas(bool),
/// Enable/disable normalization of addition, multiplication, and bitwise
/// `and`.
Normalize(bool),
/// Enable/disable normalization of addition.
NormalizeAdd(bool),
/// For `SolverEngine::Fun`, enable/disable Prop engine preprocessing step
/// within sequential portfolio setting.
FunPreProp(bool),
/// For `SolverEngine::Fun`, enable/disable SLS engine preprocessing step
/// within sequential portfolio setting.
FunPreSLS(bool),
/// For `SolverEngine::Fun`, enable/disable dual propagation optimization.
FunDualProp(bool),
/// For `SolverEngine::Fun`, set the order in which inputs are assumed in
/// dual propagation clone. The default is `DualPropQsortOrder::Just`.
FunDualPropQsortOrder(DualPropQsortOrder),
/// For `SolverEngine::Fun`, enable/disable justification optimization.
FunJustification(bool),
/// For `SolverEngine::Fun`, set the path selection heuristic for
/// justification optimization. The default is
/// `JustificationHeuristic::MinApp`.
FunJustificationHeuristic(JustificationHeuristic),
/// For `SolverEngine::Fun`, enable/disable lazy synthesis of bitvector
/// expressions.
FunLazySynthesize(bool),
/// For `SolverEngine::Fun`, enable/disable eager generation of lemmas.
FunEagerLemmas(EagerLemmas),
/// For `SolverEngine::SLS`, set the number of bit flips used as a limit.
/// `0` indicates no limit.
SLSNumFlips(u32),
/// For `SolverEngine::SLS`, set the move strategy. The default is
/// `SLSMoveStrategy::BestMove`.
SLSMoveStrategy(SLSMoveStrategy),
/// For `SolverEngine::SLS`, enable/disable justification-based path
/// selection during candidate selection.
SLSJustification(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).
SLSGroupWiseMoves(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.
SLSRangeWiseMoves(bool),
/// For `SolverEngine::SLS`, enable/disable segment-wise bitflip moves, where
/// the bits within segments of multiples of 2 are flipped at once.
SLSSegmentWiseMoves(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.
SLSRandomWalkMoves(bool),
/// For `SolverEngine::SLS`, set the probability with which a random walk is
/// chosen if `SLSRandomWalkMoves` is enabled.
SLSRandomWalkProbability(u32),
/// 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.
SLSRandomizeAll(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.
SLSRandomizeRange(bool),
/// For `SolverEngine::SLS`, enable/disable propagation moves.
SLSPropagationMoves(bool),
/// For `SolverEngine::SLS` when propagation moves are enabled, set the
/// number of propagation moves to be performed (this forms a ratio with
/// `SLSPropagationMovesNumRegular`).
SLSPropagationMovesNumProp(u32),
/// For `SolverEngine::SLS` when propagation moves are enabled, set the
/// number of regular moves to be performed (this forms a ratio with
/// `SLSPropagationMovesNumProp`).
SLSPropagationMovesNumRegular(u32),
/// For `SolverEngine::SLS`, enable/disable forcibly choosing random walks as
/// recovery moves when conflicts occur after a propagation move.
SLSForceRandomWalks(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).
SLSIncMoveTest(bool),
/// For `SolverEngine::SLS`, enable/disable restarts.
SLSRestarts(bool),
/// For `SolverEngine::SLS`, enable/disable the "bandit scheme" for selecting
/// root constraints. If disabled, candidate root constraints are selected
/// randomly.
SLSBanditScheme(bool),
/// For `SolverEngine::Prop`, set the number of propagation steps used as a
/// limit. `0` indicates no limit.
PropNumSteps(u32),
/// For `SolverEngine::Prop`, enable/disable restarts.
PropRestarts(bool),
/// For `SolverEngine::Prop`, enable/disable the "bandit scheme" for
/// selecting root constraints. If disabled, candidate root constraints are
/// selected randomly.
PropBanditScheme(bool),
/// For `SolverEngine::Prop`, choose the mode for path selection.
/// The default is `PropPathSelection::Essential`.
PropPathSelectionMode(PropPathSelection),
/// For `SolverEngine::Prop`, set the probability with which to choose
/// inverse values over consistent values.
PropInvValueProbability(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.
PropFlipConditionProbability(u32),
/// Like `PropFlipConditionProbability`, but for the case that either the
/// 'then' or 'else' branch is constant.
PropFlipConditionProbabilityConstant(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`.
PropFlipConditionNumPaths(u32),
/// For `SolverEngine::Prop`, set the delta by which
/// `PropFlipConditionProbabilityConstant` is decreased or increased after
/// `PropFlipConditionNumPaths` is reached.
PropFlipConditionProbabilityConstantDelta(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.
PropSliceKeepDCProbability(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.
PropConcatFlipProbability(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`.
PropSliceFlipProbability(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.
PropEqFlipProbability(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.
PropAndFlipProbability(u32),
/// For `SolverEngine::AIGProp`, enable/disable restarts.
AIGPropUseRestarts(bool),
/// For `SolverEngine::AIGProp`, select the synthesis mode for Skolem
/// functions.
AIGPropQuantSynthesis(AIGPropQuantSynthesis),
/// For `SolverEngine::AIGProp`, enable/disable solving the dual (negated)
/// version of the quantified bit-vector formula.
AIGPropQuantDualSolver(bool),
/// For `SolverEngine::AIGProp`, set the limit of enumerated expressions
/// for the enumerative learning synthesis algorithm.
AIGPropQuantSynthLimit(u32),
/// For `SolverEngine::AIGProp`, enable/disable generalization of
/// quantifier instantiations via enumerative learning.
AIGPropSynthQI(bool),
/// For `SolverEngine::AIGProp`, enable/disable destructive equality
/// resolution simplification.
AIGPropQuantDER(bool),
/// For `SolverEngine::AIGProp`, enable/disable constructive equality
/// resolution simplification.
AIGPropQuantCER(bool),
/// For `SolverEngine::AIGProp`, enable/disable miniscoping.
AIGPropQuantMiniscope(bool),
}
pub enum ModelGen {
/// Do not generate models
Disabled,
/// Generate models for asserted expressions only
Asserted,
/// Generate models for all expressions
All,
}
pub enum IncrementalSMT1 {
/// Stop after first satisfiable formula
Basic,
/// Solve all formulas
Continue,
}
pub enum InputFileFormat {
Autodetect,
Btor,
Btor2,
SMTLIBv1,
SMTLIBv2,
}
pub enum NumberFormat {
Binary,
Decimal,
Hexadecimal,
}
pub enum OutputFileFormat {
BTOR,
SMTLIBv2,
AigerASCII,
AigerBinary,
}
pub enum SolverEngine {
/// Default engine for all combinations of QF_AUFBV; uses lemmas on demand
/// for QF_AUFBV and eager bit-blasting for QF_BV
Fun,
/// Score-based local search QF_BV engine
SLS,
/// Propagation-based local search QF_BV engine
Prop,
/// Propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG layer)
AIGProp,
/// Quantifier engine (BV only)
Quant,
}
pub enum SatEngine {
/// CaDiCaL
CaDiCaL,
/// CryptoMiniSat
CMS,
/// Lingeling
Lingeling,
/// MiniSAT
MiniSAT,
/// PicoSAT
PicoSAT,
}
pub enum RewriteLevel {
/// "no rewriting"
None,
/// "term level rewriting"
TermLevel,
/// "more simplification techniques"
More,
/// "full rewriting/simplification"
Full,
}
pub enum DualPropQsortOrder {
/// Order by score, highest score first
Just,
/// Order by input id, ascending
Asc,
/// Order by input id, descending
Desc,
}
pub enum JustificationHeuristic {
/// Always choose the left branch
Left,
/// Choose the branch with the minimum number of applies
MinApp,
/// Choose the branch with the minimum depth
MinDepth,
}
pub enum EagerLemmas {
/// Do not generate lemmas eagerly (generate one single lemma per refinement
/// iteration)
None,
/// Only generate lemmas eagerly until the first conflict dependent on
/// another conflict is found
Conf,
/// In each refinement iterations, generate lemmas for all conflicts
All,
}
pub enum SLSMoveStrategy {
/// Always choose the best score improving move
BestMove,
/// Perform a random walk weighted by score
RandomWalk,
/// Always choose the first best move, even if another move may be better
FirstBestMove,
/// Choose a move even if its score is not better but the same as the score
/// of the previous best move
BestSameMove,
/// Always choose propagation move, and recover with SLS move in case of
/// conflict
AlwaysProp,
}
pub enum PropPathSelection {
/// Select path based on controlling inputs
Controlling,
/// Select path based on essential inputs
Essential,
/// Select path based on random inputs
Random,
}
pub enum AIGPropQuantSynthesis {
/// Do not synthesize skolem functions (use model values for instantiation)
None,
/// Use enumerative learning to synthesize skolem functions
EL,
/// Use enumerative learning modulo the predicates in the cone of influence
/// of the existential variables to synthesize skolem functions
ELMC,
/// Chain the `EL` and `ELMC` approaches to synthesize skolem functions
ELELMC,
/// Use enumerative learning modulo the given root constraints to synthesize
/// skolem functions
ELMR,
}