Option
The kind of a Bitwuzla configuration option.
Options are configured via a bitwuzla::Options
instance,
which must be configured before creating a bitwuzla::Bitwuzla
instance.
Note
Some options are labeled as “expert” options. Use with caution.
enum
bitwuzla::Option
namespace bitwuzla {
-
enum class bitwuzla::Option
The configuration options supported by Bitwuzla.
Options that list string values can be configured via
bitwuzla_set_option_str
. Options with integer configuration values are configured viabitwuzla_set_option
.For all options, the current configuration value can be queried via
bitwuzla_get_option
. Options with string configuration values internally represent these values as enum values. For these options,bitwuzla_get_opiton
will return such an enum value. Usebitwuzla_get_option_str
to query enum options for the corresponding string representation.Values:
-
enumerator LOGLEVEL
Log level.
Values:
An unsigned integer value. [default: 0]
-
enumerator PRODUCE_MODELS
Model generation.
Values:
1: enable, generate model for assertions only
2: enable, generate model for all created terms
0: disable [default]
Note
This option cannot be enabled in combination with option
EVALUE(PP_UNCONSTRAINED_OPTIMIZATION
.
-
enumerator PRODUCE_UNSAT_ASSUMPTIONS
Unsat assumptions generation.
Values:
1: enable
0: disable [default]
-
enumerator PRODUCE_UNSAT_CORES
Unsat core generation.
Values:
1: enable
0: disable [default]
-
enumerator SEED
Seed for random number generator.
Values:
An unsigned integer value. [default: 0]
-
enumerator VERBOSITY
Verbosity level.
Values:
An unsigned integer value <= 4. [default: 0]
-
enumerator TIME_LIMIT_PER
Time limit in milliseconds per satisfiability check.
Values:
An unsigned integer for the time limit in milliseconds. [default: 0]
-
enumerator MEMORY_LIMIT
** Memory limit in MB.**
Values:
An unsigned integer for the memory limit in MB. [default: 0]
-
enumerator NTHREADS
** Number of parallel threads.**
Values:
An unsigned integer > 0. [default: 1]
-
enumerator RELEVANT_TERMS
Check relevant terms only.
Theory solvers only perform checks on relevant terms.
Values:
1: enable
0: disabe [default]
Warning
This is an expert option to configure theory solvers.
-
enumerator BV_SOLVER
Configure the bit-vector solver engine.
Values:
bitblast: The classical bit-blasting approach. [default]
prop: Propagation-based local search (sat only).
preprop: Sequential portfolio combination of bit-blasting and propagation-based local search.
-
enumerator REWRITE_LEVEL
Rewrite level.
Values:
0: no rewriting
1: term level rewriting
2: term level rewriting and basic preprocessing
3: term level rewriting and full preprocessing [default]
Note
Configuring the rewrite level after terms have been created is not allowed.
Warning
This is an expert option to configure rewriting.
-
enumerator SAT_SOLVER
Configure the SAT solver engine.
Values:
cadical: CaDiCaL [default]
cms: CryptoMiniSat
kissat: Kissat
-
enumerator PROP_CONST_BITS
Propagation-based local search solver engine: Constant bits.
Configure constant bit propagation (requires bit-blasting to AIG).
Values:
1: enable [default]
0: disable
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_INFER_INEQ_BOUNDS
Propagation-based local search solver engine: Infer bounds for inequalities for value computation.
When enabled, infer bounds for value computation for inequalities based on satisfied top level inequalities.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_NPROPS
Propagation-based local search solver engine: Number of propagations.
Configure the number of propagations used as a limit for the propagation-based local search solver engine. No limit if 0.
Values:
An unsigned integer value. [default: 0]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_NUPDATES
Propagation-based local search solver engine: Number of updates.
Configure the number of model value updates used as a limit for the propagation-based local search solver engine. No limit if 0.
Values:
An unsigned integer value. [default: 0]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_OPT_LT_CONCAT_SEXT
Propagation-based local search solver engine: Optimization for inverse value computation of inequalities over concat and sign extension operands.
When enabled, use optimized inverse value value computation for inequalities over concats.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_PATH_SEL
Propagation-based local search solver engine: Path selection.
Configure mode for path selection.
Values:
essential: Select path based on essential inputs. [default]
random: Select path randomly.
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_PROB_RANDOM_INPUT
Propagation-based local search solver engine: Probability for selecting random input.
Configure the probability with which to select a random input instead of an essential input when selecting the path.
Values:
An unsigned integer value <= 1000 (= 100%). [default: 0]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_PROB_USE_INV_VALUE
Propagation-based local search solver engine: Probability for inverse values.
Configure the probability with which to choose an inverse value over a consistent value when aninverse value exists.
Values:
An unsigned integer value <= 1000 (= 100%). [default: 990]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_SEXT
Propagation-based local search solver engine: Value computation for sign extension.
When enabled, detect sign extension operations (are rewritten on construction) and use value computation for sign extension.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PROP_NORMALIZE
Propagation-based local search solver engine: Local search specific normalization.
When enabled, perform normalizations for local search, on the local search layer (does not affect node layer).
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION
Abstraction module
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_BV_SIZE
**Abstraction module: Minimum bit-vector term size. **
Specifies at which size supported bit-vector operators should be abstracted.
Values:
>0: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_EAGER_REFINE
**Bit-vector bitblasting solver: Abstraction module eager mode. **
When enabled, eagerly adds violated refinement lemmas.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_VALUE_LIMIT
**Bit-vector bitblasting solver: Abstraction module value instantiation limit. **
Specifies the limit on the number of value instantiations per abstaction. If the limit is hit, we fall back to fully bit-blasting the specific term.
Values:
>0: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_VALUE_ONLY
**Bit-vector bitblasting solver: Abstraction module value instantiations only. **
When enabled, only adds value instantiations.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_ASSERT
**Abstraction module: Abstract assertions. **
When enabled, abstracts assertions.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_ASSERT_REFS
**Abstraction module: Assertion refinements. **
Maximum number of assertion refinements added per check.
Values:
An unsigned integer value > 0.
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_INITIAL_LEMMAS
**Abstraction module: Use initial lemmas only. **
Initial lemmas are those lemmas not generated through abduction.
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_INC_BITBLAST
**Abstraction module: Incrementally bit-blast bvmul and bvadd terms. **
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_BV_ADD
**Abstraction module: Abstract bit-vector addition terms. **
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_BV_MUL
**Abstraction module: Abstract bit-vector multiplication terms. **
Values:
1: enable [default]
0: disable
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_BV_UDIV
**Abstraction module: Abstract bit-vector unsigned division terms. **
Values:
1: enable [default]
0: disable
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_BV_UREM
**Abstraction module: Abstract bit-vector unsigned remainder terms. **
Values:
1: enable [default]
0: disable
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_EQUAL
**Abstraction module: Abstract equality terms. **
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator ABSTRACTION_ITE
**Abstraction module: Abstract ITE terms. **
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the prop solver engine.
-
enumerator PREPROCESS
Preprocessing
When enabled, applies all enabled preprocessing passes.
Values:
1: enable [default]
0: disable
-
enumerator PP_CONTRADICTING_ANDS
Preprocessing: Find contradicting bit-vector ands
When enabled, substitutes contradicting nodes of kind BV_AND with zero.
Values:
1: enable [default]
0: disable
-
enumerator PP_ELIM_BV_EXTRACTS
Preprocessing: Eliminate bit-vector extracts on bit-vector constants
When enabled, eliminates bit-vector extracts on constants.
Values:
1: enable
0: disable [default]
-
enumerator PP_ELIM_BV_UDIV
Preprocessing: Eliminate bit-vector operators bvudiv and bvurem
When enabled, eliminates bit-vector unsigned division and remainder operation in terms of multiplication.
Values:
1: enable
0: disable [default]
-
enumerator PP_EMBEDDED_CONSTR
Preprocessing: Embedded constraint substitution
When enabled, substitutes assertions that occur as sub-expression in the formula with their respective Boolean value.
Values:
1: enable [default]
0: disable
-
enumerator PP_FLATTEN_AND
Preprocessing: AND flattening
Values:
1: enable [default]
0: disable
-
enumerator PP_NORMALIZE
Preprocessing: Normalization
Values:
1: enable [default]
0: disable
-
enumerator PP_SKELETON_PREPROC
Preprocessing: Boolean skeleton preprocessing
Values:
1: enable [default]
0: disable
-
enumerator PP_VARIABLE_SUBST
Preprocessing: Variable substitution
Values:
1: enable [default]
0: disable
-
enumerator PP_VARIABLE_SUBST_NORM_EQ
Preprocessing: Variable substitution: Equality Normalization
Values:
1: enable [default]
0: disable
-
enumerator PP_VARIABLE_SUBST_NORM_DISEQ
Preprocessing: Variable substitution: Disequality Normalization
Values:
1: enable [default]
0: disable
-
enumerator PP_VARIABLE_SUBST_NORM_BV_INEQ
Preprocessing: Variable substitution: Bit-Vector Inequality Normalization
Values:
1: enable [default]
0: disable
-
enumerator DBG_RW_NODE_THRESH
**Debug: Threshold for number of new nodes introduced for recursive call of rewrite(). **
Prints a warning number of newly introduced nodes is above threshold.
Warning
This is an expert debug option.
-
enumerator DBG_PP_NODE_THRESH
**Debug: Threshold for formula size increase after preprocessing in percent. **
Prints a warning if formula size increase is above threshold.
Warning
This is an expert debug option.
-
enumerator DBG_CHECK_MODEL
**Debug: Check models for each satisfiable query. **
Warning
This is an expert debug option.
-
enumerator DBG_CHECK_UNSAT_CORE
**Debug: Check unsat core for each unsatisfiable query. **
Warning
This is an expert debug option.
-
enumerator LOGLEVEL
}