Library
Module
Module type
Parameter
Class
Class type
This is a straight one to one binding of the Bitwuzla C++ API.
module Options : sig ... end
module Sort : sig ... end
module RoundingMode : sig ... end
module Kind : sig ... end
module Term : sig ... end
module Result : sig ... end
module Solver : sig ... end
val mk_bool_sort : unit -> Sort.t
mk_bool_sort ()
create a Boolean sort.
A Boolean sort is a bit-vector sort of size 1.
val mk_bv_sort : int -> Sort.t
mk_bv_sort size
create a bit-vector sort of given size.
val mk_fp_sort : int -> int -> Sort.t
mk_fp_sort exp_size sig_size
create a floating-point sort of given exponent and significand size.
mk_fun_sort domain codomain
create a function sort.
val mk_rm_sort : unit -> Sort.t
mk_rm_sort ()
create a Roundingmode sort.
val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.t
mk_uninterpreted_sort name
create an uninterpreted sort.
Only 0-arity uninterpreted sorts are supported.
val mk_true : unit -> Term.t
mk_true ()
create a true value.
This creates a bit-vector value 1 of size 1.
val mk_false : unit -> Term.t
mk_false ()
create a false value.
This creates a bit-vector value 0 of size 1.
mk_bv_ones sort
create a bit-vector value where all bits are set to 1.
mk_bv_min_signed sort
create a bit-vector minimum signed value.
mk_bv_max_signed sort
create a bit-vector maximum signed value.
mk_bv_value 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).
mk_bv_value_int 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.
mk_bv_value_int64 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.
mk_fp_pos_zero sort
create a floating-point positive zero value (SMT-LIB: +zero
).
mk_fp_neg_zero sort
create a floating-point negative zero value (SMT-LIB: -zero
).
mk_fp_pos_inf sort
create a floating-point positive infinity value (SMT-LIB: +oo
).
mk_fp_neg_inf sort
create a floating-point negative infinity value (SMT-LIB: -oo
).
mk_fp_value 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.
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.
mk_fp_value_from_rational 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.
val mk_rm_value : RoundingMode.t -> Term.t
mk_rm_value rm
create a rounding mode value.
mk_term1 kind arg
create a term of given kind with one argument term.
mk_term2 kind arg0 arg1
create a term of given kind with two argument terms.
mk_term3 kind arg0 arg1 arg2
create a term of given kind with three argument terms.
mk_term1_indexed1 kind arg idx
create an indexed term of given kind with one argument term and one index.
mk_term1_indexed2 kind arg idx0 idx1
create an indexed term of given kind with one argument term and two indices.
mk_term2_indexed1 t kind arg0 arg1 idx
create an indexed term of given kind with two argument terms and one index.
mk_term2_indexed2 t kind arg0 arg1 idx0 idx1
create an indexed term of given kind with two argument terms and two indices.
mk_term kind args ~indices
create an indexed term of given kind with the given argument terms and indices.
mk_const sort ~symbol
create a (first-order) constant of given sort with given symbol.
This creates a 0-arity function symbol.
mk_const_array sort value
create a one-dimensional constant array of given sort, initialized with given value.
mk_var sort ~symbol
create a variable of given sort with given symbol.
This creates a variable to be bound by quantifiers or lambdas.
substitute t term map
substitute a set of keys with their corresponding values in the given term.