bitwuzla-cxx 0.6.1 (latest)

Options

type _ key =

| Log_level : int key
(*
Log level.
Values:
- An unsigned integer value (default: 0).
*)
| Produce_models : bool key
(*
Model generation.
Values:
- true: enable
- false: disable [default]
This option cannot be enabled in combination with option Pp_unconstrained_optimization.
*)
| Produce_unsat_assumptions : bool key
(*
Unsat assumptions generation.
Values:
- true: enable
- false: disable [default]
*)
| Produce_unsat_cores : bool key
(*
Unsat core generation.
Values:
- true: enable
- false: disable [default].
*)
| Seed : int key
(*
Seed for random number generator.
Values:
- An unsigned integer value [default: 42].
*)
| Verbosity : int key
(*
Verbosity level.
Values:
- An unsigned integer value <= 4 [default: 0].
*)
| Time_limit_per : int key
(*
Time limit in milliseconds per satisfiability check.
Values:
- An unsigned integer for the time limit in milliseconds. [default: 0].
*)
| Memory_limit : int key
(*
Memory limit in MB.
Values:
- An unsigned integer for the memory limit in MB. [default: 0].
*)
| Relevant_terms : bool key
(*
Check relevant terms only.
Theory solvers only perform checks on relevant terms.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure theory solvers.
*)
| Bv_solver : bv_solver key
| Rewrite_level : int key
(*
Rewrite level.
Values:
- 0: no rewriting
- 1: term level rewriting
- 2: term level rewriting and full preprocessing [default]
This is an expert option to configure rewriting.
*)
| Sat_solver : sat_solver key
(*
Configure the SAT solver engine.
Values:
- Cadical [default]: [CaDiCaL](https://github.com/arminbiere/cadical)
- Cms: [CryptoMiniSat](https://github.com/msoos/cryptominisat)
- Kissat: [Kissat](https://github.com/arminbiere/kissat)
*)
| Prop_const_bits : bool key
(*
Propagation-based local search solver engine: Constant bits.
Configure constant bit propagation (requries bit-blasting to AIG).
Values:
- true: enable [default]
- false: disable
This is an expert option to configure the prop solver engine.
*)
| Prop_ineq_bounds : bool key
(*
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:
- true: enable
- false: disable [default]
This is an expert option to configure the prop solver engine.
*)
| Prop_nprops : int key
(*
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].
This is an expert option to configure the prop solver engine.
*)
| Prop_nupdates : int key
(*
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].
This is an expert option to configure the prop solver engine.
*)
| Prop_opt_lt_concat_sext : bool key
(*
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:
- true: enable
- false: disable [default]
This is an expert option to configure the prop solver engine.
*)
| Prop_path_sel : prop_path_sel key
(*
Propagation-based local search solver engine: Path selection.
Configure mode for path selection.
Values:
- Essential [default]: Select path based on essential inputs.
- Random: Select path randomly.
This is an expert option to configure the prop solver engine.
*)
| Prop_prob_pick_rand_input : int key
(*
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].
This is an expert option to configure the prop solver engine.
*)
| Prop_prob_pick_inv_value : int key
(*
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].
This is an expert option to configure the prop solver engine.
*)
| Prop_sext : bool key
(*
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:
- true: enable
- false: disable [default]
This is an expert option to configure the prop solver engine.
*)
| Prop_normalize : bool key
(*
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:
- true: enable
- false: disable [default]
This is an expert option to configure the prop solver engine.
*)
| Abstraction : bool key
(*
Abstraction module
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_bv_size : int key
(*
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.
*)
| Abstraction_eager_refine : bool key
(*
Bit-vector bitblasting solver: Abstraction module eager mode.
When enabled, eagerly adds violated refinement lemmas.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_value_limit : int key
(*
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.
*)
| Abstraction_value_only : bool key
(*
Bit-vector bitblasting solver: Abstraction module value instantiations only.
When enabled, only adds value instantiations.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_assert : bool key
(*
Abstraction module: Abstract assertions.
When enabled, abstracts assertions.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_assert_refs : int key
(*
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.
*)
| Abstraction_initial_lemmas : bool key
(*
Abstraction module: Use initial lemmas only.
Initial lemmas are those lemmas not generated through abduction.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_inc_bitblast : bool key
(*
Abstraction module: Incrementally bit-blast bvmul and bvadd terms.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_bvadd : bool key
(*
Abstraction module: Abstract bit-vector addition terms.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_bvmul : bool key
(*
Abstraction module: Abstract bit-vector multiplication terms.
Values:
- true: enable [default]
- false: disable
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_bvudiv : bool key
(*
Abstraction module: Abstract bit-vector unsigned division terms.
Values:
- true: enable [default]
- false: disable
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_bvurem : bool key
(*
Abstraction module: Abstract bit-vector unsigned remainder terms.
Values:
- true: enable [default]
- false: disable
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_eq : bool key
(*
Abstraction module: Abstract equality terms.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Abstraction_ite : bool key
(*
Abstraction module: Abstract ITE terms.
Values:
- true: enable
- false: disable [default]
@warning This is an expert option to configure the prop solver engine.
*)
| Preprocess : bool key
(*
Preprocessing
When enabled, applies all enabled preprocessing passes.
Values:
- true: enable [default]
- false: disable
*)
| Pp_contr_ands : bool key
(*
Preprocessing: Find contradicting bit-vector ands
When enabled, substitutes contradicting nodes of kind #BV_AND with zero.
Values:
- true: enable [default]
- false: disable
*)
| Pp_elim_extracts : bool key
(*
Preprocessing: Eliminate bit-vector extracts on bit-vector constants
When enabled, eliminates bit-vector extracts on constants.
Values:
- true: enable
- false: disable [default]
*)
| Pp_elim_bvudiv : bool key
(*
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]
*)
| Pp_embedded : bool key
(*
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
*)
| Pp_flatten_and : bool key
(*
Preprocessing: AND flattening
Values:
- true: enable [default]
- false: disable
*)
| Pp_normalize : bool key
(*
Preprocessing: Normalization
Values:
- true: enable [default]
- false: disable
*)
| Pp_skeleton_preproc : bool key
(*
Preprocessing: Boolean skeleton preprocessing
Values:
- true: enable [default]
- false: disable
*)
| Pp_variable_subst : bool key
(*
Preprocessing: Variable substitution
Values:
- true: enable [default]
- false: disable
*)
| Pp_variable_subst_norm_eq : bool key
(*
Preprocessing: Variable substitution: Equality Normalization
Values:
- true: enable [default]
- false: disable
*)
| Pp_variable_subst_norm_diseq : bool key
(*
Preprocessing: Variable substitution: Bit-Vector Inequality Normalization
Values:
- true: enable [default]
- false: disable
*)
| Pp_variable_subst_norm_bv_ineq : bool key
(*
Preprocessing: Variable substitution: Bit-Vector Inequality
Values:
- true: enable [default]
- false: disable
*)
| Dbg_rw_node_thresh : int key
(*
Debug: Threshold for number of new nodes introduced for recursive call of rewrite().
Prints a warning number of newly introduced nodes is above threshold.
This is an expert debug option.
*)
| Dbg_pp_node_thresh : int key
(*
Debug: Threshold for formula size increase after preprocessing in percent.
Prints a warning if formula size increase is above threshold.
This is an expert debug option.
*)
| Check_model : bool key
(*
Debug: Check models for each satisfiable query.
This is an expert debug option.
*)
| Check_unsat_core : bool key
(*
Debug: Check unsat core for each unsatisfiable query.
This is an expert debug option.
*)

The options supported by Bitwuzla.

and bv_solver =

| Bitblast
| Preprop
| Prop

and sat_solver =

| Cadical
| Cms
| Kissat

and prop_path_sel =

| Essential
| Random

val to_string : 'a key -> string

to_string opt Returns the long name of this option.

val description : 'a key -> string

description opt Returns the description of this option.

val default_value : 'a key -> 'a

default_value opt Returns the default value of this option.

val min : int key -> int

min opt Returns the minimum numeric option value.

val max : int key -> int

max opt Returns the maximum numeric option value.

Option set

type t

A given set of options.

val default : unit -> t

default () creates a set of options initialized with default values.

val set : t -> 'a key -> 'a -> unit

set t opt value set option value.

val get : t -> 'a key -> 'a

get t opt get the current option value.

package bitwuzla-cxx

Options

Option set