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.

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 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 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]

  • 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 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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

BV_SOLVER

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

ABSTRACTION

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

ABSTRACTION

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 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 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 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 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 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 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 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 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 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 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 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 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 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.

}