Module `Bitwuzla_cxx.Options`Source

Options

Sourcetype _ 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_interpolants : bool key
(*
Interpolant generation.
Values:
- true: enable
- false: disable [default]
*)
| 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].
*)
| Nthreads : int key
(*
Number of parallel threads.
Values:
- An unsigned integer > 0. [default: 1].
*)
| 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)
*)
| Write_aiger : string key
(*
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.
Note. Incremental queries to the SAT solver will overwrite the file with the latest AIG.
Values:
- A string denoting the filename the AIGER output is written to. [default: ""]
*)
| Write_cnf : string key
(*
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.
Note. Incremental queries to the SAT solver will overwrite the file with the latest CNF.
Values:
- A string denoting the filename the DIMACS output is written to. [default: ""]
*)
| 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.
*)
| 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_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.
*)
| Interpolants_algo : interpolants_algo key
(*
Interpolant generation.
The bit-level algorithm used for interpolant generation.
Values:
- Mcmillan: Use the asymmetric interpolant generation via McMillan's algorithm [default]
- Pudlak: Use the symmetric interpolant generation via Pudlak's algorithm
Warning: This is an expert option to configure interpolant generation.
*)
| Interpolants_lift : bool key
(*
Interpolant generation.
When enabled, the generated interpolant is lifted as much as possible to the theory level. Else, the resulting interpolant exactly corresponds to the bit-level AIG interpolant.
Values:
- true: enable
- false: disable [default]
Warning; This is an expert option to configure interpolant generation.
*)
| Interpolants_subst : bool key
(*
Interpolant generation.
When enabled, the generated interpolant is computed via substituitions. If all A-local symbols are eliminated via substitution, the resulting A is an interpolant. If all B-local symbols are eliminated via substitution, ~B is an interpolant.
Values:
- true: enable
- false: disable [default]
Warning; This is an expert option to configure interpolant generation.
*)
| Interpolants_simp : bool key
(*
Interpolant generation.
When enabled, the generated bit-level interpolant is simplified by applying several post-processing steps that try to recover more word-level structure.
Values:
- true: enable
- false: disable [default]
Warning: This is an expert option to configure interpolant generation.
*)
| Interpolants_stats : bool key
(*
Interpolant generation.
When enabled, compute statistics about generated interpolant.
Values:
- true: enable
- false: disable [default]
Warning: This is an expert option to configure interpolant generation.
*)
| Interpolants_print_stats : bool key
(*
Interpolant generation.
When enabled, prints statistics to stdout.
Values:
- true: enable
- false: disable [default]
Warning: This is an expert option to configure interpolant generation.
*)
| 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_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_interpolant : bool key
(*
Debug: Check interpolants for each get-interpolant query.
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.

Sourceand bv_solver =

| Bitblast
| Preprop
| Prop

Sourceand sat_solver =

| Cadical
| Cms
| Gimsatul
| Kissat

Sourceand prop_path_sel =

| Essential
| Random

Sourceand interpolants_algo =

| Mcmillan
| Pudlak

Sourceval to_string : 'a key -> string

to_string opt Returns the long name of this option.

Sourceval description : 'a key -> string

description opt Returns the description of this option.

Sourceval default_value : 'a key -> 'a

default_value opt Returns the default value of this option.

Sourceval min : int key -> int

min opt Returns the minimum numeric option value.

Sourceval max : int key -> int

max opt Returns the maximum numeric option value.

Option set

Sourcetype t

A given set of options.

Sourceval default : unit -> t

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

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

set t opt value set option value.

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

get t opt get the current option value.

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/bitwuzla-cxx/Bitwuzla_cxx/Options/index.html

Module `Bitwuzla_cxx.Options`Source

Options

Option set

package bitwuzla-cxx

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/bitwuzla-cxx/Bitwuzla_cxx/Options/index.html

Module Bitwuzla_cxx.OptionsSource

Options

Option set

dune-project
Dependency

Module `Bitwuzla_cxx.Options`Source