package bitwuzla-cxx

  1. Overview
  2. Docs
SMT solver for AUFBVFP (C++ API)

Install 

dune-project
 Dependency

bitwuzla.github.io Readme Changelog MIT License Edit opam file Versions (10)

Authors

  1. F
    Frédéric Recoules

Maintainers

  1. F
    Frédéric Recoules <frederic.recoules@cea.fr>

Sources

bitwuzla-cxx-0.4.0.tbz
sha256=87d43d446390cdfb24ed4e2dfb8e5435bd678a0cec2171a840b4a5d5c025cb68
sha512=2a9b97f316e3fd56e060dad51956bcc11d832237136b38c97f1cf16f8e1befd722a0569585c3a4f804392a71b64cc00a17c229434ea04ffaf81b1e581ac5f83e

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

Module Bitwuzla_cxx.OptionsSource

Options

Sourcetype _ key =
  1. | Log_level : int key
    (*

    Log level.

    Values:

    • An unsigned integer value (default: 0).
    *)
  2. | Produce_models : bool key
    (*

    Model generation.

    Values:

    • true: enable
    • false: disable [default]

    This option cannot be enabled in combination with option Pp_unconstrained_optimization.

    *)
  3. | Produce_unsat_assumptions : bool key
    (*

    Unsat assumptions generation.

    Values:

    • true: enable
    • false: disable [default]
    *)
  4. | Produce_unsat_cores : bool key
    (*

    Unsat core generation.

    Values:

    • true: enable
    • false: disable [default].
    *)
  5. | Seed : int key
    (*

    Seed for random number generator.

    Values:

    • An unsigned integer value [default: 42].
    *)
  6. | Verbosity : int key
    (*

    Verbosity level.

    Values:

    • An unsigned integer value <= 4 [default: 0].
    *)
  7. | Time_limit_per : int key
    (*

    Time limit in milliseconds per satisfiability check.

    Values:

    • An unsigned integer for the time limit in milliseconds. [default: 0].
    *)
  8. | Memory_limit : int key
    (*

    Memory limit in MB.

    Values:

    • An unsigned integer for the memory limit in MB. [default: 0].
    *)
  9. | Bv_solver : bv_solver key
  10. | 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.

    *)
  11. | 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)
    *)
  12. | 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.

    *)
  13. | 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.

    *)
  14. | 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.

    *)
  15. | 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.

    *)
  16. | 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.

    *)
  17. | 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.

    *)
  18. | 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.

    *)
  19. | 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.

    *)
  20. | 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.

    *)
  21. | 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.

    *)
  22. | Preprocess : bool key
    (*

    Preprocessing

    When enabled, applies all enabled preprocessing passes.

    Values:

    • true: enable [default]
    • false: disable
    *)
  23. | 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
    *)
  24. | 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 [default]
    • false: disable
    *)
  25. | 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
    *)
  26. | Pp_flatten_and : bool key
    (*

    Preprocessing: AND flattening

    Values:

    • true: enable [default]
    • false: disable
    *)
  27. | Pp_normalize : bool key
    (*

    Preprocessing: Normalization

    Values:

    • true: enable [default]
    • false: disable
    *)
  28. | Pp_normalize_share_aware : bool key
    (*

    Preprocessing: Normalization: Enable share awareness normlization

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

    Values:

    • true: enable [default]
    • false: disable
    *)
  29. | Pp_skeleton_preproc : bool key
    (*

    Preprocessing: Boolean skeleton preprocessing

    Values:

    • true: enable [default]
    • false: disable
    *)
  30. | Pp_variable_subst : bool key
    (*

    Preprocessing: Variable substitution

    Values:

    • true: enable [default]
    • false: disable
    *)
  31. | Pp_variable_subst_norm_eq : bool key
    (*

    Preprocessing: Variable substitution: Equality Normalization

    Values:

    • true: enable [default]
    • false: disable
    *)
  32. | Pp_variable_subst_norm_diseq : bool key
    (*

    Preprocessing: Variable substitution: Bit-Vector Inequality Normalization

    Values:

    • true: enable [default]
    • false: disable
    *)
  33. | Pp_variable_subst_norm_bv_ineq : bool key
    (*

    Preprocessing: Variable substitution: Bit-Vector Inequality

    Values:

    • true: enable [default]
    • false: disable
    *)
  34. | 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.

    *)
  35. | 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.

    *)
  36. | Check_model : bool key
    (*

    Debug: Check models for each satisfiable query.

    This is an expert debug option.

    *)
  37. | 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 =
  1. | Bitblast
  2. | Preprop
  3. | Prop
Sourceand sat_solver =
  1. | Cadical
  2. | Cms
  3. | Kissat
Sourceand prop_path_sel =
  1. | Essential
  2. | Random
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.