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 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 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
lingeling: Lingeling

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 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_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_NORMALIZE_SHARE_AWARE

Preprocessing: Normalization: Enable share awareness normlization

When enabled, this disables normalizations that may yield blow-up on the bit-level.

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.

}