On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package bitwuzla-cxx
Create a new independent Bitwuzla instance that can run in parallel to all other ones.
Signature of a Bitwuzla instance.
Each instance can create and share Terms between several Solvers. However, an instance is not thread safe. Thus multicore users should ensure that only one Domain uses a bitwuzla instance at a given time.
Parameters
Signature
module Sort : sig ... endmodule RoundingMode : sig ... endmodule Kind : sig ... endmodule Term : sig ... endmodule Result : sig ... endmodule Solver : sig ... endSort constructor
val mk_bool_sort : unit -> Sort.tmk_bool_sort () create a Boolean sort.
A Boolean sort is a bit-vector sort of size 1.
val mk_bv_sort : int -> Sort.tmk_bv_sort size create a bit-vector sort of given size.
val mk_fp_sort : int -> int -> Sort.tmk_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.tmk_rm_sort () create a Roundingmode sort.
val mk_uninterpreted_sort : ?symbol:string -> unit -> Sort.tmk_uninterpreted_sort name create an uninterpreted sort.
Only 0-arity uninterpreted sorts are supported.
Term constructor
Value
val mk_true : unit -> Term.tmk_true () create a true value.
This creates a bit-vector value 1 of size 1.
val mk_false : unit -> Term.tmk_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.tmk_rm_value rm create a rounding mode value.
Expression
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.
Util
substitute t term map substitute a set of keys with their corresponding values in the given term.
On This Page