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.

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:

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.

}