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.
SMT-LIB:
:produce-models
Values:
true: enable
false: disable [default]
-
enumerator PRODUCE_UNSAT_ASSUMPTIONS
Unsat assumptions generation.
SMT-LIB:
:produce-unsat-assumptions
Values:
true: enable
false: disable [default]
-
enumerator PRODUCE_UNSAT_CORES
Unsat core generation.
SMT-LIB:
:produce-unsat-core
Values:
true: enable
false: disable [default]
-
enumerator SEED
Seed for the random number generator.
Values:
min: 1
max: UINT32_MAX
default: 27644437
-
enumerator VERBOSITY
Verbosity level.
Values:
An unsigned integer value <= 4. [default: 0]
-
enumerator TIME_LIMIT_PER
Time limit per satisfiability check in milliseconds.
A configuration value of 0 disables the time limit (no time limit).
Values:
An unsigned 64-bit integer. [default: 0]
-
enumerator MEMORY_LIMIT
Memory limit per satisfiability check in MB.
A configuration value of 0 disables the memory limit (no memory limit).
Values:
An unsigned 64-bit integer. [default: 0]
-
enumerator NTHREADS
Number of parallel threads.
Values:
min: 1
max: UINT64_MAX
default: 1
-
enumerator BV_SOLVER
Configure the bit-vector solver engine.
Values:
bitblast: The classical bit-blasting approach. [default]
preprop: Sequential portfolio of
bitblast
andprop
.
Note
Propagation-based local search is only able to determine satisfiability.
-
enumerator REWRITE_LEVEL
Rewrite level.
Values:
0: no rewriting
1: term level rewriting (only “cheap” rewrites)
2: term level rewriting (full) and preprocessing [default]
Warning
This is an expert option to configure rewriting.
-
enumerator SAT_SOLVER
Configure the SAT solver engine.
Values:
cadical: Use CaDiCaL as the backend SAT solver. [default]
cms: Use CryptoMiniSat as the backend SAT solver.
kissat: Use Kissat as the backend SAT solver.
-
enumerator WRITE_AIGER
Print bit-vector abstraction as AIG in binary or ascii AIGER format.
Expects a filename (as string) as the configuration value. The filename suffix determines whether binary (.aig) or ascii (.aag) AIGER is used. A configuration value representing the empty string disables the option.
Values:
A string denoting the filename the AIGER output is written to. [default: “”]
Note
Incremental queries to the SAT solver will overwrite the file with the latest AIG.
-
enumerator WRITE_CNF
Print bit-vector abstraction as CNF in DIMACS format.
Expects a filename (as string) as the configuration value. A configuration value representing the empty string disables the option.
Values:
A string denoting the filename the DIMACS output is written to. [default: “”]
Note
Incremental queries to the SAT solver will overwrite the file with the latest CNF.
-
enumerator PROP_CONST_BITS
Propagation-based local search solver engine: Constant bits.
Enable/disable constant bit propagation in the propagation-based local search engine (requires bit-blasting to AIG).
Our procedure for augmenting propagation-based local search with constant bit information is described in [NP20].
Values:
true: enable [default]
false: disable
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator PROP_INFER_INEQ_BOUNDS
Propagation-based local search solver engine: Infer bounds.
When enabled, infer bounds for value computation for inequalities based on satisfied top level inequalities.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the
prop
bit-vector 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]
See also
Warning
This is an expert option to configure the
prop
bit-vector 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]
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator PROP_OPT_LT_CONCAT_SEXT
Propagation-based local search solver engine: Concat optimization.
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:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the
prop
bit-vector 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.
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator PROP_PROB_RANDOM_INPUT
Propagation-based local search solver engine: Input probability.
Configure the probability for selecting random (over essential) input when selecting the propagation path.
Values:
An unsigned integer value <= 1000 (= 100%). [default: 10 (= 1%)]
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator PROP_PROB_USE_INV_VALUE
Propagation-based local search solver engine: Value probability.
Configure the probability for selcting an inverse value over a consistent value (if an inverse value exists).
Values:
An unsigned integer value <= 1000 (= 100%). [default: 990 (= 99%)]
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator PROP_SEXT
Propagation-based local search solver engine: Sign extension.
When enabled, treat concat nodes that represent sign extension natively as sign extension.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the
prop
bit-vector solver engine.
-
enumerator ABSTRACTION
Abstraction module.
Our bit-vector abstraction procedure is described in [NPZ24].
Values:
1: enable
0: disable [default]
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_BV_SIZE
Abstraction module. Minimum bit-vector term size.
Configure the minimum size for considered bit-vector operations to be abstracted.
Values:
min: >=3
max: UINT64_MAX
default: 32
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_EAGER_REFINE
Abstraction module: Eager mode.
When enabled, violated refinement lemmas are added eagerly.
Values:
1: enable
0: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_VALUE_LIMIT
Abstraction module: Value instantiation limit.
Configure
n
for value instantiation limitbit-width/<n>
. The value instantiation limit defines the maximum number of value instantiation lemmas to be added for an abstracted term. A configuration value of 0 disables adding value instantiation lemmas.Values:
An unsigned 64-bit integer. [default: 8]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_VALUE_ONLY
Abstraction module: Value instantiations only.
When enabled, only adds value instantiations.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_ASSERT
Abstraction module: Abstract assertions.
When enabled, abstracts assertions.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_ASSERT_REFS
Abstraction module: Assertion refinements.
Maximum number of assertion refinements added per check.
Values:
An unsigned 64-bit integer value > 0. [default: 100]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_INITIAL_LEMMAS
Abstraction module: Use initial lemmas only.
Initial lemmas are those lemmas not generated through abduction.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_INC_BITBLAST
Abstraction module: Incrementally bit-blast bvmul and bvadd terms.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_BV_ADD
Abstraction module: Abstract bit-vector addition terms.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_BV_MUL
Abstraction module: Abstract bit-vector multiplication terms.
Values:
true: enable [default]
false: disable
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_BV_UDIV
Abstraction module: Abstract bit-vector unsigned division terms.
Values:
true: enable [default]
false: disable
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_BV_UREM
Abstraction module: Abstract bit-vector unsigned remainder terms.
Values:
true: enable [default]
false: disable
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_EQUAL
Abstraction module: Abstract equality terms.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator ABSTRACTION_ITE
Abstraction module: Abstract ITE terms.
Values:
true: enable
false: disable [default]
See also
Warning
This is an expert option to configure the abstraction module.
-
enumerator PREPROCESS
Preprocessing.
When enabled, applies all enabled preprocessing passes.
Values:
true: enable [default]
false: disable
-
enumerator PP_CONTRADICTING_ANDS
Preprocessing: Find contradicting bit-vector ands.
When enabled, substitutes contradicting nodes of kind BV_AND with zero.
Values:
true: enable
false: disable [default]
-
enumerator PP_ELIM_BV_EXTRACTS
Preprocessing: Eliminate bit-vector extracts on bit-vector constants.
When enabled, eliminates bit-vector extracts on constants.
Values:
true: enable
false: 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:
true: enable
false: 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:
true: enable [default]
false: disable
-
enumerator PP_FLATTEN_AND
Preprocessing: AND flattening.
Values:
true: enable [default]
false: disable
-
enumerator PP_NORMALIZE
Preprocessing: Normalization.
Values:
true: enable [default]
false: disable
-
enumerator PP_SKELETON_PREPROC
Preprocessing: Boolean skeleton preprocessing.
Values:
true: enable [default]
false: disable
-
enumerator PP_VARIABLE_SUBST
Preprocessing: Variable substitution.
Values:
true: enable [default]
false: disable
-
enumerator PP_VARIABLE_SUBST_NORM_EQ
Preprocessing: Variable substitution: Equality normalization.
Values:
true: enable [default]
false: disable
-
enumerator PP_VARIABLE_SUBST_NORM_DISEQ
Preprocessing: Variable substitution: Disequality Normalization.
Values:
true: enable [default]
false: disable
-
enumerator PP_VARIABLE_SUBST_NORM_BV_INEQ
Preprocessing: Variable substitution: Bit-Vector Inequality Normalization.
Values:
true: enable [default]
false: disable
-
enumerator DBG_RW_NODE_THRESH
Debug: Recursive rewrite threshold.
Threshold for number of new nodes introduced for recursive call of rewrite(). Prints a warning when number of newly introduced nodes is above threshold.
Warning
This is an expert debug option.
-
enumerator DBG_PP_NODE_THRESH
Debug: Formula size increase threshold.
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
}