BitwuzlaOption

The kind of a Bitwuzla configuration option.

Options are configured via a BitwuzlaOptions instance, which must be configured before creating a Bitwuzla instance.

Note

Some options are labeled as “expert” options. Use with caution.

enum BitwuzlaOption

enum BitwuzlaOption

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 via bitwuzla_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. Use bitwuzla_get_option_str to query enum options for the corresponding string representation.

Values:

enumerator BITWUZLA_OPT_LOGLEVEL

Log level.

Values:

An unsigned integer value. [default: 0]

enumerator BITWUZLA_OPT_PRODUCE_MODELS

Model generation.

SMT-LIB: :produce-models

Values:

true: enable
false: disable [default]

enumerator BITWUZLA_OPT_PRODUCE_UNSAT_ASSUMPTIONS

Unsat assumptions generation.

SMT-LIB: :produce-unsat-assumptions

Values:

true: enable
false: disable [default]

enumerator BITWUZLA_OPT_PRODUCE_UNSAT_CORES

Unsat core generation.

SMT-LIB: :produce-unsat-core

Values:

true: enable
false: disable [default]

enumerator BITWUZLA_OPT_SEED

Seed for the random number generator.

Values:

min: 1
max: UINT32_MAX
default: 27644437

enumerator BITWUZLA_OPT_VERBOSITY

Verbosity level.

Values:

An unsigned integer value <= 4. [default: 0]

enumerator BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_NTHREADS

Number of parallel threads.

Values:

min: 1
max: UINT64_MAX
default: 1

enumerator BITWUZLA_OPT_BV_SOLVER

Configure the bit-vector solver engine.

Values:

bitblast: The classical bit-blasting approach. [default]
prop: Propagation-based local search, see [NP20, NPB17].
preprop: Sequential portfolio of bitblast and prop.

Note

Propagation-based local search is only able to determine satisfiability.

enumerator BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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

#BV_SOLVER

Warning

This is an expert option to configure the prop bit-vector solver engine.

enumerator BITWUZLA_OPT_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 BITWUZLA_OPT_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

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_EAGER_REFINE

Abstraction module: Eager mode.

When enabled, violated refinement lemmas are added eagerly.

Values:

1: enable
0: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_VALUE_LIMIT

Abstraction module: Value instantiation limit.

Configure n for value instantiation limit bit-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

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_VALUE_ONLY

Abstraction module: Value instantiations only.

When enabled, only adds value instantiations.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_ASSERT

Abstraction module: Abstract assertions.

When enabled, abstracts assertions.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_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

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_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

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_INC_BITBLAST

Abstraction module: Incrementally bit-blast bvmul and bvadd terms.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_BV_ADD

Abstraction module: Abstract bit-vector addition terms.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_BV_MUL

Abstraction module: Abstract bit-vector multiplication terms.

Values:

true: enable [default]
false: disable

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_BV_UDIV

Abstraction module: Abstract bit-vector unsigned division terms.

Values:

true: enable [default]
false: disable

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_BV_UREM

Abstraction module: Abstract bit-vector unsigned remainder terms.

Values:

true: enable [default]
false: disable

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_EQUAL

Abstraction module: Abstract equality terms.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_ABSTRACTION_ITE

Abstraction module: Abstract ITE terms.

Values:

true: enable
false: disable [default]

See also

#ABSTRACTION

Warning

This is an expert option to configure the abstraction module.

enumerator BITWUZLA_OPT_PREPROCESS

Preprocessing.

When enabled, applies all enabled preprocessing passes.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_PP_FLATTEN_AND

Preprocessing: AND flattening.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_NORMALIZE

Preprocessing: Normalization.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_SKELETON_PREPROC

Preprocessing: Boolean skeleton preprocessing.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_VARIABLE_SUBST

Preprocessing: Variable substitution.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_EQ

Preprocessing: Variable substitution: Equality normalization.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_DISEQ

Preprocessing: Variable substitution: Disequality Normalization.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_PP_VARIABLE_SUBST_NORM_BV_INEQ

Preprocessing: Variable substitution: Bit-Vector Inequality Normalization.

Values:

true: enable [default]
false: disable

enumerator BITWUZLA_OPT_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 BITWUZLA_OPT_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 BITWUZLA_OPT_DBG_CHECK_MODEL: Debug: Check models for each satisfiable query.

Warning

This is an expert debug option.

enumerator BITWUZLA_OPT_DBG_CHECK_UNSAT_CORE: Debug: Check unsat core for each unsatisfiable query.

Warning

This is an expert debug option.