package bitwuzla-c

  1. Overview
  2. Docs

This is a straight one to one binding of the Bitwuzla C API.

Context

type t

The Bitwuzla solver.

val create : unit -> t

create t create a new Bitwuzla instance.

The returned instance can be deleted earlier via delete.

  • returns

    A pointer to the created Bitwuzla instance.

val delete : t -> unit

delete t delete a Bitwuzla instance.

The given instance must have been created via create.

  • parameter t

    The Bitwuzla instance to delete.

val reset : t -> unit

reset t reset a Bitwuzla instance.

This deletes the given instance and creates a new instance in place. The given instance must have been created via create.

All sorts and terms associated with the given instance are released and thus invalidated.

  • parameter t

    The Bitwuzla instance to reset.

copyright t get copyright information.

  • parameter t

    The Bitwuzla instance.

val version : t -> string

version t get version information.

  • parameter t

    The Bitwuzla instance.

val terminate : t -> bool

terminate t if termination callback function has been configured via set_termination_callback, call this termination function.

  • parameter t

    The Bitwuzla instance.

  • returns

    true if t has been terminated.

A termination callback cookie

val set_termination_callback : t -> ('a -> int) -> 'a -> 'a cookie

set_termination_callback t f a configure a termination callback function.

The state a of the callback can be retrieved via get_termination_callback_state.

  • parameter t

    The Bitwuzla instance.

  • parameter f

    The callback function, returns a value > 0 if t has been terminated.

  • parameter a

    The argument to the callback function.

  • returns

    A cookie to retrieve the state a.

val get_termination_callback_state : 'a cookie -> 'a

get_termination_callback_state c get the state of the termination callback function.

The returned object representing the state of the callback corresponds to the state a configured as argument to the callback function via set_termination_callback.

  • parameter c

    The termination callback cookie.

  • returns

    The object passed as argument a to the callback function.

Option

type opt =
  1. | Engine
    (*

    Configure the solver engine.

    Values:

    • "aigprop": The propagation-based local search QF_BV engine that operates on the bit-blasted formula (the AIG circuit layer).
    • "fun" [default]: The default engine for all combinations of QF_AUFBVFP, uses lemmas on demand for QF_AUFBVFP, and eager bit-blasting (optionally with local searchin a sequential portfolio) for QF_BV.
    • "prop": The propagation-based local search QF_BV engine.
    • "sls": The stochastic local search QF_BV engine.
    • "quant": The quantifier engine.
    *)
  2. | Exit_codes
    (*

    Use non-zero exit codes for sat and unsat results.

    When enabled, use Bitwuzla exit codes When disabled, return 0 on success (sat, unsat, unknown), and a non-zero exit code otherwise.

    Values:

    • 1: enable [default]
    • 0: disable
    *)
  3. | Input_format
    (*

    Configure input file format.

    If unspecified, Bitwuzla will autodetect the input file format.

    Values:

    • "none" [default]: Auto-detect input file format.
    • "btor": BTOR format
    • "btor2": BTOR2 format
    • "smt2": SMT-LIB v2 format
    *)
  4. | Incremental
    (*

    Incremental solving.

    Values:

    • 1: enable
    • 0: disable [default]

    Enabling this option turns off some optimization techniques. Enabling/disabling incremental solving after bitwuzla_check_sat() has been called is not supported. This option cannot be enabled in combination with option Pp_unconstrained_optimization.

    *)
  5. | Loglevel
    (*

    Log level.

    Values:

    • An unsigned integer value (default: 0).
    *)
  6. | Output_format
    (*

    Configure output number format for bit-vector values.

    If unspecified, Bitwuzla will use BTOR format.

    Values:

    • "aiger": AIGER ascii format
    • "aigerbin": AIGER binary format
    • "btor" [default]: BTOR format
    • "smt2": SMT-LIB v2 format
    *)
  7. | Output_number_format
    (*

    Configure output number format for bit-vector values.

    If unspecified, Bitwuzla will use binary representation.

    Values:

    • "bin" [default]: Binary number format.
    • "hex": Hexadecimal number format.
    • "dec": Decimal number format.
    *)
  8. | Pretty_print
    (*

    Pretty printing.

    Values:

    • 1: enable [default]
    • 0: disable
    *)
  9. | Print_dimacs
    (*

    Print DIMACS.

    Print the CNF sent to the SAT solver in DIMACS format to stdout.

    Values:

    • 1: enable
    • 0: disable [default]
    *)
  10. | Produce_models
    (*

    Model generation.

    Values:

    • 1: enable, generate model for assertions only
    • 2: enable, generate model for all created terms
    • 0: disable [default]

    This option cannot be enabled in combination with option Pp_unconstrained_optimization.

    *)
  11. | Produce_unsat_cores
    (*

    Unsat core generation.

    Values:

    • 1: enable
    • 0: disable [default]
    *)
  12. | Seed
    (*

    Seed for random number generator.

    Values:

    • An unsigned integer value (default: 0).
    *)
  13. | Verbosity
    (*

    Verbosity level.

    Values:

    • An unsigned integer value <= 4 (default: 0).
    *)
  14. | Pp_ackermann
  15. | Pp_beta_reduce
  16. | Pp_eliminate_extracts
  17. | Pp_eliminate_ites
  18. | Pp_extract_lambdas
  19. | Pp_merge_lambdas
  20. | Pp_nondestr_subst
  21. | Pp_normalize_add
  22. | Pp_skeleton_preproc
  23. | Pp_unconstrained_optimization
  24. | Pp_var_subst
  25. | Rw_extract_arith
  26. | Rw_level
  27. | Rw_normalize
  28. | Rw_normalize_add
  29. | Rw_simplify_constraints
  30. | Rw_slt
  31. | Rw_sort_aig
  32. | Rw_sort_aigvec
  33. | Rw_sort_exp
  34. | Fun_dual_prop
  35. | Fun_dual_prop_qsort
  36. | Fun_eager_lemmas
  37. | Fun_lazy_synthesize
  38. | Fun_just
  39. | Fun_just_heuristic
  40. | Fun_preprop
  41. | Fun_presls
  42. | Fun_store_lambdas
  43. | Sls_just
  44. | Sls_move_gw
  45. | Sls_move_inc_move_test
  46. | Sls_move_prop
  47. | Sls_move_prop_force_rw
  48. | Sls_move_prop_nprops
  49. | Sls_move_prop_nslss
  50. | Sls_move_rand_all
  51. | Sls_move_rand_range
  52. | Sls_move_rand_walk
  53. | Sls_move_range
  54. | Sls_move_segment
  55. | Sls_prob_move_rand_walk
  56. | Sls_nflips
  57. | Sls_strategy
  58. | Sls_use_restarts
  59. | Sls_use_bandit
  60. | Prop_ashr
  61. | Prop_const_bits
  62. | Prop_const_domains
  63. | Prop_entailed
  64. | Prop_flip_cond_const_delta
  65. | Prop_flip_cond_const_npathsel
  66. | Prop_infer_ineq_bounds
  67. | Prop_no_move_on_conflict
  68. | Prop_nprops
  69. | Prop_nupdates
  70. | Prop_path_sel
  71. | Prop_prob_fallback_random_value
  72. | Prop_prob_and_flip
  73. | Prop_prob_eq_flip
  74. | Prop_prob_flip_cond
  75. | Prop_prob_flip_cond_const
  76. | Prop_prob_random_input
  77. | Prop_prob_slice_flip
  78. | Prop_prob_slice_keep_dc
  79. | Prop_prob_use_inv_value
  80. | Prop_use_bandit
  81. | Prop_use_inv_lt_concat
  82. | Prop_use_restarts
  83. | Prop_sext
  84. | Prop_skip_no_progress
  85. | Prop_xor
  86. | Aigprop_nprops
  87. | Aigprop_use_bandit
  88. | Aigprop_use_restarts
  89. | Quant_cer
  90. | Quant_der
  91. | Quant_dual_solver
  92. | Quant_miniscope
  93. | Quant_synth
  94. | Quant_fixsynth
  95. | Quant_synth_ite_complete
  96. | Quant_synth_limit
  97. | Quant_synth_qi
  98. | Check_model
  99. | Check_unconstrained
  100. | Check_unsat_assumptions
  101. | Declsort_bv_witdh
  102. | Ls_share_sat
  103. | Parse_interactive
  104. | Sat_engine_cadical_freeze

The options supported by Bitwuzla.

val set_option : t -> opt -> int -> unit

set_option t option value set option.

  • parameter t

    The Bitwuzla instance.

  • parameter option

    The option.

  • parameter value

    The option value.

val set_option_str : t -> opt -> string -> unit

set_option_str t option value set option value for string options.

  • parameter t

    The Bitwuzla instance.

  • parameter option

    The option.

  • parameter value

    The option string value.

val get_option : t -> opt -> int

get_option t option get the current value of an option.

  • parameter t

    The Bitwuzla instance.

  • parameter option

    The option.

  • returns

    The option value.

val get_option_str : t -> opt -> string

get_option_str t option get the current value of an option as a string if option can be configured via a string value.

  • parameter t

    The Bitwuzla instance.

  • parameter option

    The option.

  • returns

    The option value.

Sort

type sort

A Bitwuzla sort.

Constructor

val mk_array_sort : t -> sort -> sort -> sort

mk_array_sort t index element create an array sort.

  • parameter t

    The Bitwuzla instance.

  • parameter index

    The index sort of the array sort.

  • parameter element

    The element sort of the array sort.

  • returns

    An array sort which maps sort index to sort element.

val mk_bool_sort : t -> sort

mk_bool_sort t create a Boolean sort.

A Boolean sort is a bit-vector sort of size 1.

  • parameter t

    The Bitwuzla instance.

  • returns

    A Boolean sort.

val mk_bv_sort : t -> int -> sort

mk_bv_sort t size create a bit-vector sort of given size.

  • parameter t

    The Bitwuzla instance.

  • parameter size

    The size of the bit-vector sort.

  • returns

    A bit-vector sort of given size.

val mk_fp_sort : t -> int -> int -> sort

mk_fp_sort t exp_size sig_size create a floating-point sort of given exponent and significand size.

  • parameter t

    The Bitwuzla instance.

  • parameter exp_size

    The size of the exponent.

  • parameter sig_size

    The size of the significand (including sign bit).

  • returns

    A floating-point sort of given format.

val mk_fun_sort : t -> sort array -> sort -> sort

mk_fun_sort t domain codomain create a function sort.

  • parameter t

    The Bitwuzla instance.

  • parameter domain

    The domain sorts (the sorts of the arguments).

  • parameter codomain

    The codomain sort (the sort of the return value).

  • returns

    A function sort of given domain and codomain sorts.

val mk_rm_sort : t -> sort

mk_rm_sort t create a Roundingmode sort.

  • parameter t

    The Bitwuzla instance.

  • returns

    A Roundingmode sort.

Util

val sort_dump : sort -> [ `Btor | `Smt2 ] -> Stdlib.Format.formatter -> unit

sort_dump sort format pp print sort.

  • parameter sort

    The sort.

  • parameter format

    The output format for printing the term. Either `Btor for the BTOR format, or `Smt2 for the SMT-LIB v2 format. Note for the `Btor this function won't do anything since BTOR sorts are printed when printing the term via term_dump.

  • parameter pp

    The outpout formatter.

Query

val sort_hash : sort -> int

sort_hash sort compute the hash value for a sort.

  • parameter sort

    The sort.

  • returns

    The hash value of the sort.

val sort_bv_get_size : sort -> int

bv_get_size sort get the size of a bit-vector sort.

Requires that given sort is a bit-vector sort.

  • parameter sort

    The sort.

  • returns

    The size of the bit-vector sort.

val sort_fp_get_exp_size : sort -> int

sort_fp_get_exp_size sort get the exponent size of a floating-point sort.

Requires that given sort is a floating-point sort.

  • parameter sort

    The sort.

  • returns

    The exponent size of the floating-point sort.

val sort_fp_get_sig_size : sort -> int

sort_fp_get_sig_size sort get the significand size of a floating-point sort.

Requires that given sort is a floating-point sort.

  • parameter sort

    The sort.

  • returns

    The significand size of the floating-point sort.

val sort_array_get_index : sort -> sort

sort_array_get_index sort get the index sort of an array sort.

Requires that given sort is an array sort.

  • parameter sort

    The sort.

  • returns

    The index sort of the array sort.

val sort_array_get_element : sort -> sort

sort_array_get_element sort get the element sort of an array sort.

Requires that given sort is an array sort.

  • parameter sort

    The sort.

  • returns

    The element sort of the array sort.

val sort_fun_get_domain_sorts : sort -> sort array

sort_fun_get_domain_sorts sort get the domain sorts of a function sort.

Requires that given sort is a function sort.

  • parameter sort

    The sort.

  • returns

    The domain sorts of the function sort as an array of sort.

val sort_fun_get_codomain : sort -> sort

sort_fun_get_codomain sort get the codomain sort of a function sort.

Requires that given sort is a function sort.

  • parameter sort

    The sort.

  • returns

    The codomain sort of the function sort.

val sort_fun_get_arity : sort -> int

sort_fun_get_arity sort get the arity of a function sort.

  • parameter sort

    The sort.

  • returns

    The number of arguments of the function sort.

val sort_is_equal : sort -> sort -> bool

sort_is_equal sort0 sort1 determine if two sorts are equal.

  • parameter sort0

    The first sort.

  • parameter sort1

    The second sort.

  • returns

    true if the given sorts are equal.

val sort_is_array : sort -> bool

sort_is_array sort determine if a sort is an array sort.

  • parameter sort

    The sort.

  • returns

    true if sort is an array sort.

val sort_is_bv : sort -> bool

sort_is_bv sort determine if a sort is a bit-vector sort.

  • parameter sort

    The sort.

  • returns

    true if sort is a bit-vector sort.

val sort_is_fp : sort -> bool

sort_is_fp sort determine if a sort is a floating-point sort.

  • parameter sort

    The sort.

  • returns

    true if sort is a floating-point sort.

val sort_is_fun : sort -> bool

sort_is_fun sort determine if a sort is a function sort.

  • parameter sort

    The sort.

  • returns

    true if sort is a function sort.

val sort_is_rm : sort -> bool

sort_is_rm sort determine if a sort is a Roundingmode sort.

  • parameter sort

    The sort.

  • returns

    true if sort is a Roundingmode sort.

Term

type term

A Bitwuzla term.

type bvbase =
  1. | Bin
    (*

    binary

    *)
  2. | Dec
    (*

    decimal

    *)
  3. | Hex
    (*

    hexadecimal

    *)

The base for strings representing bit-vector values.

type roundingmode =
  1. | Rne
    (*

    Round to the nearest even number. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with an even least significant digit will be delivered.

    SMT-LIB: RNE roundNearestTiesToEven

    *)
  2. | Rna
    (*

    Round to the nearest number away from zero. If the two nearest floating-point numbers bracketing an unrepresentable infinitely precise result are equally near, the one with larger magnitude will be selected.

    SMT-LIB: RNA roundNearestTiesToAway

    *)
  3. | Rtn
    (*

    Round towards negative infinity (-oo). The result shall be the format’s floating-point number (possibly -oo) closest to and no less than the infinitely precise result.

    SMT-LIB: RTN roundTowardNegative

    *)
  4. | Rtp
    (*

    Round towards positive infinity (+oo). The result shall be the format’s floating-point number (possibly +oo) closest to and no less than the infinitely precise result.

    SMT-LIB: RTP roundTowardPositive

    *)
  5. | Rtz
    (*

    Round towards zero. The result shall be the format’s floating-point number closest to and no greater in magnitude than the infinitely precise result.

    SMT-LIB: RTZ roundTowardZero

    *)

Rounding mode for floating-point operations.

For some floating-point operations, infinitely precise results may not be representable in a given format. Hence, they are rounded modulo one of five rounding modes to a representable floating-point number.

The following rounding modes follow the SMT-LIB theory for floating-point arithmetic, which in turn is based on IEEE Standard 754. The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE Standard 754.

type kind =
  1. | And
    (*

    Boolean and.

    SMT-LIB: and

    *)
  2. | Apply
    (*

    Function application.

    *)
  3. | Array_select
    (*

    Array select.

    SMT-LIB: select

    *)
  4. | Array_store
    (*

    Array store.

    SMT-LIB: store

    *)
  5. | Bv_add
    (*

    Bit-vector addition.

    SMT-LIB: bvadd

    *)
  6. | Bv_and
    (*

    Bit-vector and.

    SMT-LIB: bvand

    *)
  7. | Bv_ashr
    (*

    Bit-vector arithmetic right shift.

    SMT-LIB: bvashr

    *)
  8. | Bv_comp
    (*

    Bit-vector comparison.

    SMT-LIB: bvcomp

    *)
  9. | Bv_concat
    (*

    Bit-vector concat.

    SMT-LIB: concat

    *)
  10. | Bv_dec
    (*

    Bit-vector decrement.

    Decrement by one.

    *)
  11. | Bv_inc
    (*

    Bit-vector increment.

    Increment by one.

    *)
  12. | Bv_mul
    (*

    Bit-vector multiplication.

    SMT-LIB: bvmul

    *)
  13. | Bv_nand
    (*

    Bit-vector nand.

    SMT-LIB: bvnand

    *)
  14. | Bv_neg
    (*

    Bit-vector negation (two's complement).

    SMT-LIB: bvneg

    *)
  15. | Bv_nor
    (*

    Bit-vector nor.

    SMT-LIB: bvnor

    *)
  16. | Bv_not
    (*

    Bit-vector not (one's complement).

    SMT-LIB: bvnot

    *)
  17. | Bv_or
    (*

    Bit-vector or.

    SMT-LIB: bvor

    *)
  18. | Bv_redand
    (*

    Bit-vector and reduction.

    Bit-wise and reduction, all bits are and'ed together into a single bit. This corresponds to bit-wise and reduction as known from Verilog.

    *)
  19. | Bv_redor
    (*

    Bit-vector reduce or.

    Bit-wise or reduction, all bits are or'ed together into a single bit. This corresponds to bit-wise or reduction as known from Verilog.

    *)
  20. | Bv_redxor
    (*

    Bit-vector reduce xor.

    Bit-wise xor reduction, all bits are xor'ed together into a single bit. This corresponds to bit-wise xor reduction as known from Verilog.

    *)
  21. | Bv_rol
    (*

    Bit-vector rotate left (not indexed).

    This is a non-indexed variant of SMT-LIB rotate_left.

    *)
  22. | Bv_ror
    (*

    Bit-vector rotate right.

    This is a non-indexed variant of SMT-LIB rotate_right.

    *)
  23. | Bv_sadd_overflow
    (*

    Bit-vector signed addition overflow test.

    Single bit to indicate if signed addition produces an overflow.

    *)
  24. | Bv_sdiv_overflow
    (*

    Bit-vector signed division overflow test.

    Single bit to indicate if signed division produces an overflow.

    *)
  25. | Bv_sdiv
    (*

    Bit-vector signed division.

    SMT-LIB: bvsdiv

    *)
  26. | Bv_sge
    (*

    Bit-vector signed greater than or equal.

    SMT-LIB: bvsge

    *)
  27. | Bv_sgt
    (*

    Bit-vector signed greater than.

    SMT-LIB: bvsgt

    *)
  28. | Bv_shl
    (*

    Bit-vector logical left shift.

    SMT-LIB: bvshl

    *)
  29. | Bv_shr
    (*

    Bit-vector logical right shift.

    SMT-LIB: bvshr

    *)
  30. | Bv_sle
    (*

    Bit-vector signed less than or equal.

    SMT-LIB: bvsle

    *)
  31. | Bv_slt
    (*

    Bit-vector signed less than.

    SMT-LIB: bvslt

    *)
  32. | Bv_smod
    (*

    Bit-vector signed modulo.

    SMT-LIB: bvsmod

    *)
  33. | Bv_smul_overflow
    (*

    Bit-vector signed multiplication overflow test.

    SMT-LIB: bvsmod

    *)
  34. | Bv_srem
    (*

    Bit-vector signed remainder.

    SMT-LIB: bvsrem

    *)
  35. | Bv_ssub_overflow
    (*

    Bit-vector signed subtraction overflow test.

    Single bit to indicate if signed subtraction produces an overflow.

    *)
  36. | Bv_sub
    (*

    Bit-vector subtraction.

    SMT-LIB: bvsub

    *)
  37. | Bv_uadd_overflow
    (*

    Bit-vector unsigned addition overflow test.

    Single bit to indicate if unsigned addition produces an overflow.

    *)
  38. | Bv_udiv
    (*

    Bit-vector unsigned division.

    SMT-LIB: bvudiv

    *)
  39. | Bv_uge
    (*

    Bit-vector unsigned greater than or equal.

    SMT-LIB: bvuge

    *)
  40. | Bv_ugt
    (*

    Bit-vector unsigned greater than.

    SMT-LIB: bvugt

    *)
  41. | Bv_ule
    (*

    Bit-vector unsigned less than or equal.

    SMT-LIB: bvule

    *)
  42. | Bv_ult
    (*

    Bit-vector unsigned less than.

    SMT-LIB: bvult

    *)
  43. | Bv_umul_overflow
    (*

    Bit-vector unsigned multiplication overflow test.

    Single bit to indicate if unsigned multiplication produces an overflow.

    *)
  44. | Bv_urem
    (*

    Bit-vector unsigned remainder.

    SMT-LIB: bvurem

    *)
  45. | Bv_usub_overflow
    (*

    Bit-vector unsigned subtraction overflow test.

    Single bit to indicate if unsigned subtraction produces an overflow.

    *)
  46. | Bv_xnor
    (*

    Bit-vector xnor.

    SMT-LIB: bvxnor

    *)
  47. | Bv_xor
    (*

    Bit-vector xor.

    SMT-LIB: bvxor

    *)
  48. | Distinct
    (*

    Disequality.

    SMT-LIB: distinct

    *)
  49. | Equal
    (*

    Equality.

    SMT-LIB: =

    *)
  50. | Exists
    (*

    Existential quantification.

    SMT-LIB: exists

    *)
  51. | Forall
    (*

    Universal quantification.

    SMT-LIB: forall

    *)
  52. | Fp_abs
    (*

    Floating-point absolute value.

    SMT-LIB: fp.abs

    *)
  53. | Fp_add
    (*

    Floating-point addition.

    SMT-LIB: fp.add

    *)
  54. | Fp_div
    (*

    Floating-point division.

    SMT-LIB: fp.div

    *)
  55. | Fp_eq
    (*

    Floating-point equality.

    SMT-LIB: fp.eq

    *)
  56. | Fp_fma
    (*

    Floating-point fused multiplcation and addition.

    SMT-LIB: fp.fma

    *)
  57. | Fp_fp
    (*

    Floating-point IEEE 754 value.

    SMT-LIB: fp

    *)
  58. | Fp_geq
    (*

    Floating-point greater than or equal.

    SMT-LIB: fp.geq

    *)
  59. | Fp_gt
    (*

    Floating-point greater than.

    SMT-LIB: fp.gt

    *)
  60. | Fp_is_inf
    (*

    Floating-point is infinity tester.

    SMT-LIB: fp.isInfinite

    *)
  61. | Fp_is_nan
    (*

    Floating-point is Nan tester.

    SMT-LIB: fp.isNaN

    *)
  62. | Fp_is_neg
    (*

    Floating-point is negative tester.

    SMT-LIB: fp.isNegative

    *)
  63. | Fp_is_normal
    (*

    Floating-point is normal tester.

    SMT-LIB: fp.isNormal

    *)
  64. | Fp_is_pos
    (*

    Floating-point is positive tester.

    SMT-LIB: fp.isPositive

    *)
  65. | Fp_is_subnormal
    (*

    Floating-point is subnormal tester.

    SMT-LIB: fp.isSubnormal

    *)
  66. | Fp_is_zero
    (*

    Floating-point is zero tester.

    SMT-LIB: fp.isZero

    *)
  67. | Fp_leq
    (*

    Floating-point less than or equal.

    SMT-LIB: fp.leq

    *)
  68. | Fp_lt
    (*

    Floating-point less than.

    SMT-LIB: fp.lt

    *)
  69. | Fp_max
    (*

    Floating-point max.

    SMT-LIB: fp.max

    *)
  70. | Fp_min
    (*

    Floating-point min.

    SMT-LIB: fp.min

    *)
  71. | Fp_mul
    (*

    Floating-point multiplcation.

    SMT-LIB: fp.mul

    *)
  72. | Fp_neg
    (*

    Floating-point negation.

    SMT-LIB: fp.neg

    *)
  73. | Fp_rem
    (*

    Floating-point remainder.

    SMT-LIB: fp.rem

    *)
  74. | Fp_rti
    (*

    Floating-point round to integral.

    SMT-LIB: fp.roundToIntegral

    *)
  75. | Fp_sqrt
    (*

    Floating-point round to square root.

    SMT-LIB: fp.sqrt

    *)
  76. | Fp_sub
    (*

    Floating-point round to subtraction.

    SMT-LIB: fp.sqrt

    *)
  77. | Iff
    (*

    Boolean if and only if.

    SMT-LIB: =

    *)
  78. | Implies
    (*

    Boolean implies.

    SMT-LIB: =>

    *)
  79. | Ite
    (*

    If-then-else.

    SMT-LIB: ite

    *)
  80. | Lambda
    (*

    Lambda.

    *)
  81. | Not
    (*

    Boolean not.

    SMT-LIB: not

    *)
  82. | Or
    (*

    Boolean or.

    SMT-LIB: or

    *)
  83. | Xor
    (*

    Boolean xor.

    SMT-LIB: xor

    *)
  84. | Bv_extract
    (*

    Bit-vector extract.

    SMT-LIB: extract (indexed)

    *)
  85. | Bv_repeat
    (*

    Bit-vector repeat.

    SMT-LIB: repeat (indexed)

    *)
  86. | Bv_roli
    (*

    Bit-vector rotate left by integer.

    SMT-LIB: rotate_left (indexed)

    *)
  87. | Bv_rori
    (*

    Bit-vector rotate right by integer.

    SMT-LIB: rotate_right (indexed)

    *)
  88. | Bv_sign_extend
    (*

    Bit-vector sign extend.

    SMT-LIB: sign_extend (indexed)

    *)
  89. | Bv_zero_extend
    (*

    Bit-vector zero extend.

    SMT-LIB: zero_extend (indexed)

    *)
  90. | Fp_to_fp_from_bv
    (*

    Floating-point to_fp from IEEE 754 bit-vector.

    SMT-LIB: to_fp (indexed)

    *)
  91. | Fp_to_fp_from_fp
    (*

    Floating-point to_fp from floating-point.

    SMT-LIB: to_fp (indexed)

    *)
  92. | Fp_to_fp_from_sbv
    (*

    Floating-point to_fp from signed bit-vector value.

    SMT-LIB: to_fp (indexed)

    *)
  93. | Fp_to_fp_from_ubv
    (*

    Floating-point to_fp from unsigned bit-vector value.

    SMT-LIB: to_fp_unsigned (indexed)

    *)
  94. | Fp_to_sbv
    (*

    Floating-point to_sbv.

    SMT-LIB: fp.to_sbv (indexed)

    *)
  95. | Fp_to_ubv
    (*

    Floating-point to_ubv.

    SMT-LIB: fp.to_ubv (indexed)

    *)

The term kind.

Constructor

Value

val mk_true : t -> term

mk_true t create a true value.

This creates a bit-vector value 1 of size 1.

  • parameter t

    The Bitwuzla instance.

  • returns

    A term representing the bit-vector value 1 of size 1.

val mk_false : t -> term

mk_false t create a false value.

This creates a bit-vector value 0 of size 1.

  • parameter t

    The Bitwuzla instance.

  • returns

    A term representing the bit-vector value 0 of size 1.

val mk_bv_zero : t -> sort -> term

mk_bv_zero t sort create a bit-vector value zero.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value 0 of given sort.

val mk_bv_one : t -> sort -> term

mk_bv_one t sort create a bit-vector value one.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value 1 of given sort.

val mk_bv_ones : t -> sort -> term

mk_bv_ones t sort create a bit-vector value where all bits are set to 1.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where all bits are set to 1.

val mk_bv_min_signed : t -> sort -> term

mk_bv_min_signed t sort create a bit-vector minimum signed value.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where the MSB is set to 1 and all remaining bits are set to 0.

val mk_bv_max_signed : t -> sort -> term

mk_bv_max_signed t sort create a bit-vector maximum signed value.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the bit-vector value of given sort where the MSB is set to 0 and all remaining bits are set to 1.

val mk_fp_pos_zero : t -> sort -> term

mk_fp_pos_zero t sort create a floating-point positive zero value (SMT-LIB: +zero).

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the floating-point positive zero value of given floating-point sort.

val mk_fp_neg_zero : t -> sort -> term

mk_fp_neg_zero t sort create a floating-point negative zero value (SMT-LIB: -zero).

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the floating-point negative zero value of given floating-point sort.

val mk_fp_pos_inf : t -> sort -> term

mk_fp_pos_inf t sort create a floating-point positive infinity value (SMT-LIB: +oo).

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the floating-point positive infinity value of given floating-point sort.

val mk_fp_neg_inf : t -> sort -> term

mk_fp_neg_inf t sort create a floating-point negative infinity value (SMT-LIB: -oo).

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the floating-point negative infinity value of given floating-point sort.

val mk_fp_nan : t -> sort -> term

mk_fp_nan t sort create a floating-point NaN value.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • returns

    A term representing the floating-point NaN value of given floating-point sort.

val mk_bv_value : t -> sort -> string -> bvbase -> term

mk_bv_value t sort value base create a bit-vector value from its string representation.

Parameter base determines the base of the string representation.

Given value must fit into a bit-vector of given size (sort).

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • parameter value

    A string representing the value.

  • parameter base

    The base in which the string is given.

  • returns

    A term representing the bit-vector value of given sort.

val mk_bv_value_int : t -> sort -> int -> term

mk_bv_value_int t sort value create a bit-vector value from its unsigned integer representation.

If given value does not fit into a bit-vector of given size (sort), the value is truncated to fit.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • parameter value

    The unsigned integer representation of the bit-vector value.

  • returns

    A term representing the bit-vector value of given sort.

val mk_fp_value : t -> term -> term -> term -> term

mk_fp_value t bv_sign bv_exponent bv_significand create a floating-point value from its IEEE 754 standard representation given as three bitvectors representing the sign bit, the exponent and the significand.

  • parameter t

    The Bitwuzla instance.

  • parameter bv_sign

    The sign bit.

  • parameter bv_exponent

    The exponent bit-vector.

  • parameter bv_significand

    The significand bit-vector.

  • returns

    A term representing the floating-point value.

val mk_fp_value_from_real : t -> sort -> term -> string -> term

mk_fp_value_from_real t sort rm real create a floating-point value from its real representation, given as a decimal string, with respect to given rounding mode.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • parameter rm

    The rounding mode.

  • parameter real

    The decimal string representing a real value.

  • returns

    A term representing the floating-point value of given sort.

val mk_fp_value_from_rational : t -> sort -> term -> string -> string -> term

mk_fp_value_from_rational t sort rm num den create a floating-point value from its rational representation, given as a two decimal strings representing the numerator and denominator, with respect to given rounding mode.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the value.

  • parameter rm

    The rounding mode.

  • parameter num

    The decimal string representing the numerator.

  • parameter den

    The decimal string representing the denominator.

  • returns

    A term representing the floating-point value of given sort.

val mk_rm_value : t -> roundingmode -> term

mk_rm_value t rm create a rounding mode value.

  • parameter t

    The Bitwuzla instance.

  • parameter rm

    The rounding mode value.

  • returns

    A term representing the rounding mode value.

Expression

val mk_term1 : t -> kind -> term -> term

mk_term1 t kind arg create a term of given kind with one argument term.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg

    The argument to the operator.

  • returns

    A term representing an operation of given kind.

val mk_term2 : t -> kind -> term -> term -> term

mk_term2 t kind arg0 arg1 create a term of given kind with two argument terms.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg0

    The first argument to the operator.

  • parameter arg1

    The second argument to the operator.

  • returns

    A term representing an operation of given kind.

val mk_term3 : t -> kind -> term -> term -> term -> term

mk_term3 t kind arg0 arg1 arg2 create a term of given kind with three argument terms.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg0

    The first argument to the operator.

  • parameter arg1

    The second argument to the operator.

  • parameter arg2

    The third argument to the operator.

  • returns

    A term representing an operation of given kind.

val mk_term : t -> kind -> term array -> term

mk_term t kind args create a term of given kind with the given argument terms.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter args

    The argument terms.

  • returns

    A term representing an operation of given kind.

val mk_term1_indexed1 : t -> kind -> term -> int -> term

mk_term1_indexed1 t kind arg idx create an indexed term of given kind with one argument term and one index.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg

    The argument term.

  • parameter idx

    The index.

  • returns

    A term representing an indexed operation of given kind.

val mk_term1_indexed2 : t -> kind -> term -> int -> int -> term

mk_term1_indexed2 t kind arg idx0 idx1 create an indexed term of given kind with one argument term and two indices.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg

    The argument term.

  • parameter idx0

    The first index.

  • parameter idx1

    The second index.

  • returns

    A term representing an indexed operation of given kind.

val mk_term2_indexed1 : t -> kind -> term -> term -> int -> term

mk_term2_indexed1 t kind arg0 arg1 idx create an indexed term of given kind with two argument terms and one index.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg0

    The first argument term.

  • parameter arg1

    The second argument term.

  • parameter idx

    The index.

  • returns

    A term representing an indexed operation of given kind.

val mk_term2_indexed2 : t -> kind -> term -> term -> int -> int -> term

mk_term2_indexed2 t kind arg0 arg1 idx0 idx1 create an indexed term of given kind with two argument terms and two indices.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter arg0

    The first argument term.

  • parameter arg1

    The second argument term.

  • parameter idx0

    The first index.

  • parameter idx1

    The second index.

  • returns

    A term representing an indexed operation of given kind.

val mk_term_indexed : t -> kind -> term array -> int array -> term

mk_term_indexed t kind args idxs create an indexed term of given kind with the given argument terms and indices.

  • parameter t

    The Bitwuzla instance.

  • parameter kind

    The operator kind.

  • parameter args

    The argument terms.

  • parameter idxs

    The indices.

  • returns

    A term representing an indexed operation of given kind.

val mk_const : t -> sort -> string -> term

mk_const t sort symbol create a (first-order) constant of given sort with given symbol.

This creates a 0-arity function symbol.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the constant.

  • parameter symbol

    The symbol of the constant.

  • returns

    A term representing the constant.

val mk_const_array : t -> sort -> term -> term

mk_const_array t sort value create a one-dimensional constant array of given sort, initialized with given value.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the array.

  • parameter value

    The value to initialize the elements of the array with.

  • returns

    A term representing a constant array of given sort.

val mk_var : t -> sort -> string -> term

mk_var t sort symbol create a variable of given sort with given symbol.

This creates a variable to be bound by quantifiers or lambdas.

  • parameter t

    The Bitwuzla instance.

  • parameter sort

    The sort of the variable.

  • parameter symbol

    The symbol of the variable.

  • returns

    A term representing the variable.

Util

val substitute_term : t -> term -> (term * term) array -> term

substitute t term map substitute a set of keys with their corresponding values in the given term.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term in which the keys are to be substituted.

  • parameter map

    The key/value associations.

  • returns

    The resulting term from this substitution.

val substitute_terms : t -> term array -> (term * term) array -> unit

substitute_terms t terms map substitute a set of keys with their corresponding values in the set of given terms.

The terms in terms are replaced with the terms resulting from this substitutions.

  • parameter t

    The Bitwuzla instance.

  • parameter terms

    The terms in which the keys are to be substituted.

  • parameter map

    The key/value associations.

val term_dump : term -> [ `Btor | `Smt2 ] -> Stdlib.Format.formatter -> unit

term_dump term format pp print term.

  • parameter term

    The term.

  • parameter format

    The output format for printing the term. Either `Btor for the BTOR format, or `Smt2 for the SMT-LIB v2 format.

  • parameter pp

    The outpout formatter.

Query

val term_hash : term -> int

term_hash term compute the hash value for a term.

  • parameter term

    The term.

  • returns

    The hash value of the term.

val term_get_kind : term -> kind

term_get_kind term get the kind of a term.

  • parameter term

    The term.

  • returns

    The kind of the given term.

val term_get_children : term -> term array

term_get_children term get the child terms of a term.

  • parameter term

    The term.

  • returns

    The children of term as an array of terms.

val term_get_indices : term -> int array

term_get_indices term get the indices of an indexed term.

Requires that given term is an indexed term.

  • parameter term

    The term.

  • returns

    The children of term as an array of terms.

val term_is_indexed : term -> bool

term_is_indexed term determine if a term is an indexed term.

  • parameter term

    The term.

  • returns

    true if term is an indexed term.

val term_get_sort : term -> sort

term_get_sort term get the sort of a term.

  • parameter term

    The term.

  • returns

    The sort of the term.

val term_array_get_index_sort : term -> sort

term_array_get_index_sort term get the index sort of an array term.

Requires that given term is an array or an array store term.

  • parameter term

    The term.

  • returns

    The index sort of the array term.

val term_array_get_element_sort : term -> sort

term_array_get_element_sort term get the element sort of an array term.

Requires that given term is an array or an array store term.

  • parameter term

    The term.

  • returns

    The element sort of the array term.

val term_fun_get_domain_sorts : term -> sort array

term_fun_get_domain_sorts term get the domain sorts of a function term.

Requires that given term is an uninterpreted function, a lambda term, an array store term, or an ite term over function terms.

  • parameter term

    The term.

  • returns

    The domain sorts of the function term.

val term_fun_get_codomain_sort : term -> sort

term_fun_get_codomain_sort term get the codomain sort of a function term.

Requires that given term is an uninterpreted function, a lambda term, an array store term, or an ite term over function terms.

  • parameter term

    The term.

  • returns

    The codomain sort of the function term.

val term_bv_get_size : term -> int

term_bv_get_size term get the bit-width of a bit-vector term.

Requires that given term is a bit-vector term.

  • parameter term

    The term.

  • returns

    The bit-width of the bit-vector term.

val term_fp_get_exp_size : term -> int

term_fp_get_exp_size term get the bit-width of the exponent of a floating-point term.

Requires that given term is a floating-point term.

  • parameter term

    The term.

  • returns

    The bit-width of the exponent of the floating-point term.

val term_fp_get_sig_size : term -> int

term_fp_get_sig_size term get the bit-width of the significand of a floating-point term.

Requires that given term is a floating-point term.

  • parameter term

    The term.

  • returns

    The bit-width of the significand of the floating-point term.

val term_fun_get_arity : term -> int

term_fp_get_arity term get the arity of a function term.

Requires that given term is a function term.

  • parameter term

    The term.

  • returns

    The arity of the function term.

val term_get_symbol : term -> string

term_get_symbol term get the symbol of a term.

  • parameter term

    The term.

  • returns

    The symbol of term.

  • raises Not_found

    if no symbol is defined.

val term_set_symbol : term -> string -> unit

term_set_symbol term symbol set the symbol of a term.

  • parameter term

    The term.

  • parameter symbol

    The symbol.

val term_is_equal_sort : term -> term -> bool

term_is_equal_sort term0 term1 determine if the sorts of two terms are equal.

  • parameter term0

    The first term.

  • parameter term1

    The second term.

  • returns

    true if the sorts of term0 and term1 are equal.

val term_is_array : term -> bool

term_is_array term determine if a term is an array term.

  • parameter term

    The term.

  • returns

    true if term is an array term.

val term_is_const : term -> bool

term_is_const term determine if a term is a constant.

  • parameter term

    The term.

  • returns

    true if term is a constant.

val term_is_fun : term -> bool

term_is_fun term determine if a term is a function.

  • parameter term

    The term.

  • returns

    true if term is a function.

val term_is_var : term -> bool

term_is_var term determine if a term is a variable.

  • parameter term

    The term.

  • returns

    true if term is a variable.

val term_is_bound_var : term -> bool

term_is_bound_var term determine if a term is a bound variable.

  • parameter term

    The term.

  • returns

    true if term is a variable and bound.

val term_is_value : term -> bool

term_is_value term determine if a term is a value.

  • parameter term

    The term.

  • returns

    true if term is a value.

val term_is_bv_value : term -> bool

term_is_bv_value term determine if a term is a bit-vector value.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector value.

val term_is_fp_value : term -> bool

term_is_fp_value term determine if a term is a floating-point value.

  • parameter term

    The term.

  • returns

    true if term is a floating-point value.

val term_is_rm_value : term -> bool

term_is_rm_value term determine if a term is a rounding mode value.

  • parameter term

    The term.

  • returns

    true if term is a rounding mode value.

val term_is_bv : term -> bool

term_is_bv term determine if a term is a bit-vector term.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector term.

val term_is_fp : term -> bool

term_is_fp term determine if a term is a floating-point term.

  • parameter term

    The term.

  • returns

    true if term is a floating-point term.

val term_is_rm : term -> bool

term_is_rm term determine if a term is a rounding mode term.

  • parameter term

    The term.

  • returns

    true if term is a rounding mode term.

val term_is_bv_value_zero : term -> bool

term_is_bv_value_zero term determine if a term is a bit-vector value representing zero.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector zero value.

val term_is_bv_value_one : term -> bool

term_is_bv_value_one term determine if a term is a bit-vector value representing one.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector one value.

val term_is_bv_value_ones : term -> bool

term_is_bv_value_ones term determine if a term is a bit-vector value with all bits set to one.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector value with all bits set to one.

val term_is_bv_value_min_signed : term -> bool

term_is_bv_value_min_signed term determine if a term is a bit-vector minimum signed value.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector value with the most significant bit set to 1 and all other bits set to 0.

val term_is_bv_value_max_signed : term -> bool

term_is_bv_value_max_signed term determine if a term is a bit-vector maximum signed value.

  • parameter term

    The term.

  • returns

    true if term is a bit-vector value with the most significant bit set to 0 and all other bits set to 1.

val term_is_fp_value_pos_zero : term -> bool

term_is_fp_value_pos_zero term determine if a term is a floating-point positive zero (+zero) value.

  • parameter term

    The term.

  • returns

    true if term is a floating-point +zero value.

val term_is_fp_value_neg_zero : term -> bool

term_is_fp_value_neg_zero term determine if a term is a floating-point value negative zero (-zero).

  • parameter term

    The term.

  • returns

    true if term is a floating-point value negative zero.

val term_is_fp_value_pos_inf : term -> bool

term_is_fp_value_pos_inf term determine if a term is a floating-point positive infinity (+oo) value.

  • parameter term

    The term.

  • returns

    true if term is a floating-point +oo value.

val term_is_fp_value_neg_inf : term -> bool

term_is_fp_value_neg_inf term determine if a term is a floating-point negative infinity (-oo) value.

  • parameter term

    The term.

  • returns

    true if term is a floating-point -oo value.

val term_is_fp_value_nan : term -> bool

term_is_fp_value_nan term determine if a term is a floating-point NaN value.

  • parameter term

    The term.

  • returns

    true if term is a floating-point NaN value.

val term_is_const_array : term -> bool

term_is_const_array term determine if a term is a constant array.

  • parameter term

    The term.

  • returns

    true if term is a constant array.

Solver

type result =
  1. | Sat
    (*

    sat

    *)
  2. | Unsat
    (*

    unsat

    *)
  3. | Unknown
    (*

    unknown

    *)

A satisfiability result.

val parse : t -> string -> Stdlib.Format.formatter -> result

parse t input pp parse input file.

The format of the input file is auto detected. Requires that no terms have been created yet.

  • parameter t

    The Bitwuzla instance.

  • parameter input

    The input file.

  • parameter pp

    The output log.

  • returns

    Sat if the input formula was simplified to true, Unsat if it was simplified to false, and Unknown otherwise.

  • raises Failure

    in case of parsing error.

val parse_format : t -> [ `Btor | `Btor2 | `Smt2 ] -> string -> Stdlib.Format.formatter -> result

parse_format t format input pp parse input file, assumed to be given in the specified format.

Requires that no terms have been created yet.

  • parameter t

    The Bitwuzla instance.

  • parameter format

    The input format for printing the model. Either `Btor for the BTOR format, `Btor2 for the BTOR2 format, or `Smt2 for the SMT-LIB v2 format.

  • parameter input

    The input file.

  • parameter pp

    The output log.

  • returns

    Sat if the input formula was simplified to true, Unsat if it was simplified to false, and Unknown otherwise.

  • raises Failure

    in case of parsing error.

Formula

val push : t -> int -> unit

push t nlevels push context levels.

Requires that incremental solving has been enabled via set_option.

Assumptions added via this bitwuzla_assume are not affected by context level changes and are only valid until the next check_sat call, no matter at which level they were assumed.

  • parameter t

    The Bitwuzla instance.

  • parameter nlevels

    The number of context levels to push.

val pop : t -> int -> unit

pop t nlevels pop context levels.

Requires that incremental solving has been enabled via set_option.

Assumptions added via this assume are not affected by context level changes and are only valid until the next check_sat call, no matter at which level they were assumed.

  • parameter t

    The Bitwuzla instance.

  • parameter nlevels

    The number of context levels to pop.

val mk_assert : t -> term -> unit

mk_assert t term assert formula.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The formula to assert.

val mk_assume : t -> term -> unit

mk_assume t term assume formula.

Requires that incremental solving has been enabled via set_option.

Assumptions added via this function are not affected by context level changes and are only valid until the next check_sat call, no matter at which level they were assumed.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The formula to assume.

val fixate_assumptions : t -> unit

fixate_assumptions t assert all added assumptions.

  • parameter t

    The Bitwuzla instance.

val reset_assumptions : t -> unit

reset_assumptions t reset all added assumptions.

  • parameter t

    The Bitwuzla instance.

val dump_formula : t -> [ `Aiger_ascii | `Aiger_binary | `Btor | `Smt2 ] -> Stdlib.Format.formatter -> unit

dump_formula t format pp print the current input formula.

Requires that incremental solving is not enabled.

  • parameter t

    The Bitwuzla instance.

  • parameter format

    The output format for printing the formula. Either `Aiger_ascii for the AIGER ascii format, `Aiger_binary for the binary AIGER format, `Btor for the BTOR format, or `Smt2 for the SMT-LIB v2 format.

  • parameter pp

    The outpout formatter.

Check

val simplify : t -> result

simplify t simplify the current input formula.

Assumptions are not considered for simplification.

  • parameter t

    The Bitwuzla instance.

  • returns

    Sat if the input formula was simplified to true, Unsat if it was simplified to false, and Unknown otherwise.

val check_sat : t -> result

check_sat t check satisfiability of current input formula.

An input formula consists of assertions added via mk_assert. The search for a solution can by guided by making assumptions via mk_assume.

Assertions and assumptions are combined via Boolean and. Multiple calls to this function require enabling incremental solving via set_option.

  • parameter t

    The Bitwuzla instance.

  • returns

    Sat if the input formula is satisfiable and Unsat if it is unsatisfiable, and Unknown when neither satisfiability nor unsatisfiability was determined. This can happen when t was terminated via a termination callback.

Sat

val get_value : t -> term -> term

get_value t term get a term representing the model value of a given term.

Requires that the last check_sat query returned Sat.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    A term representing the model value of term term.

val get_bv_value : t -> term -> string

get_bv_value t term get string representation of the current model value of given bit-vector term.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    Binary string representation of current model value of term term.

val get_fp_value : t -> term -> string * string * string

get_fp_value t term get string of IEEE 754 standard representation of the current model value of given floating-point term.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    Binary string representations of the sign bit, the exponent bit-vector and significand bit-vector values.

val get_rm_value : t -> term -> string

get_rm_value t term get string representation of the current model value of given rounding mode term.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The rounding mode term to query a model value for.

  • returns

    String representation of rounding mode (RNA, RNE, RTN, RTP, RTZ).

val get_array_value : t -> term -> (term * term) array * term option

get_array_value t term get the current model value of given array term.

The string representation of indices and values can be queried via get_bv_value, get_fp_value, and get_rm_value.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    An array of associations between indices and values. The value of all other indices is Some default when base array is constant array, otherwise, it is None.

val get_fun_value : t -> term -> term array array

get_fun_value t term get the current model value of given function term.

The string representation of arguments and values can be queried via get_bv_value, get_fp_value, and get_rm_value.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The term to query a model value for.

  • returns

    An array of associations between `arity` arguments and a value.

val print_model : t -> [ `Btor | `Smt2 ] -> Stdlib.Format.formatter -> unit

print_model t print a model for the current input formula.

Requires that the last check_sat query returned Sat.

  • parameter t

    The Bitwuzla instance.

  • parameter format

    The output format for printing the model. Either "btor" for the BTOR format, or "smt2" for the SMT-LIB v2 format.

  • parameter file

    The file to print the model to.

Unsat

val is_unsat_assumption : t -> term -> bool

is_unsat_assumption t term determine if an assumption is an unsat assumption.

Unsat assumptions are assumptions that force an input formula to become unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to failed assumptions in MiniSAT.

Requires that incremental solving has been enabled via set_option.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • parameter term

    The assumption to check for.

  • returns

    true if given assumption is an unsat assumption.

val get_unsat_assumptions : t -> term array

get_unsat_assumptions t get the set of unsat assumptions.

Unsat assumptions are assumptions that force an input formula to become unsatisfiable. Unsat assumptions handling in Bitwuzla is analogous to failed assumptions in MiniSAT.

Requires that incremental solving has been enabled via set_option.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • returns

    An array with unsat assumptions.

val get_unsat_core : t -> term array

get_unsat_core t get the set unsat core (unsat assertions).

The unsat core consists of the set of assertions that force an input formula to become unsatisfiable.

Requires that the last check_sat query returned Unsat.

  • parameter t

    The Bitwuzla instance.

  • returns

    An array with unsat assertions.

OCaml

Innovation. Community. Security.