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

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.