package bitwuzla-cxx

  1. Overview
  2. Docs

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 ... end
module RoundingMode : sig ... end
module Kind : sig ... end
module Term : sig ... end
module Result : sig ... end
module Solver : sig ... end

Sort constructor

val mk_array_sort : Sort.t -> Sort.t -> Sort.t

mk_array_sort index element create an array sort.

  • 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 : unit -> Sort.t

mk_bool_sort () create a Boolean sort.

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

  • returns

    A Boolean sort.

val mk_bv_sort : int -> Sort.t

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

  • parameter size

    The size of the bit-vector sort.

  • returns

    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.

  • 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 : Sort.t array -> Sort.t -> Sort.t

mk_fun_sort domain codomain create a function sort.

  • 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 : unit -> Sort.t

mk_rm_sort () create a Roundingmode sort.

  • returns

    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.

  • parameter symbol

    The symbol of the sort.

  • returns

    An uninterpreted sort.

Term constructor

Value

val mk_true : unit -> Term.t

mk_true () create a true value.

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

  • returns

    A term representing the 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.

  • returns

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

val mk_bv_zero : Sort.t -> Term.t

mk_bv_zero sort create a bit-vector value zero.

  • parameter sort

    The sort of the value.

  • returns

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

val mk_bv_one : Sort.t -> Term.t

mk_bv_one sort create a bit-vector value one.

  • parameter sort

    The sort of the value.

  • returns

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

val mk_bv_ones : Sort.t -> Term.t

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

  • 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 : Sort.t -> Term.t

mk_bv_min_signed sort create a bit-vector minimum signed value.

  • 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 : Sort.t -> Term.t

mk_bv_max_signed sort create a bit-vector maximum signed value.

  • 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_bv_value : Sort.t -> string -> int -> Term.t

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

  • 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 : Sort.t -> int -> Term.t

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.

  • 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_bv_value_int64 : Sort.t -> int64 -> Term.t

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.

  • 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_pos_zero : Sort.t -> Term.t

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

  • 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 : Sort.t -> Term.t

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

  • 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 : Sort.t -> Term.t

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

  • 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 : Sort.t -> Term.t

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

  • 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 : Sort.t -> Term.t

mk_fp_nan sort create a floating-point NaN value.

  • parameter sort

    The sort of the value.

  • returns

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

val mk_fp_value : Term.t -> Term.t -> Term.t -> Term.t

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.

  • 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 : Sort.t -> Term.t -> string -> Term.t

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 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 : Sort.t -> Term.t -> string -> string -> Term.t

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.

  • 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 : RoundingMode.t -> Term.t

mk_rm_value rm create a rounding mode value.

  • parameter rm

    The rounding mode value.

  • returns

    A term representing the rounding mode value.

Expression

val mk_term1 : Kind.t -> Term.t -> Term.t

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

  • parameter kind

    The operator kind.

  • parameter arg

    The argument to the operator.

  • returns

    A term representing an operation of given kind.

val mk_term2 : Kind.t -> Term.t -> Term.t -> Term.t

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

  • 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 : Kind.t -> Term.t -> Term.t -> Term.t -> Term.t

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

  • 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_term1_indexed1 : Kind.t -> Term.t -> int -> Term.t

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

  • 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 : Kind.t -> Term.t -> int -> int -> Term.t

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

  • 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 : Kind.t -> Term.t -> Term.t -> int -> Term.t

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

  • 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 : Kind.t -> Term.t -> Term.t -> int -> int -> Term.t

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

  • 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 : Kind.t -> ?indices:int array -> Term.t array -> Term.t

mk_term kind args ~indices create an indexed term of given kind with the given argument terms and indices.

  • parameter kind

    The operator kind.

  • parameter args

    The argument terms.

  • parameter indices

    The indices.

  • returns

    A term representing an indexed operation of given kind.

val mk_const : ?symbol:string -> Sort.t -> Term.t

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

This creates a 0-arity function symbol.

  • parameter sort

    The sort of the constant.

  • parameter symbol

    The symbol of the constant.

  • returns

    A term representing the constant.

val mk_const_array : Sort.t -> Term.t -> Term.t

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

  • 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 : ?symbol:string -> Sort.t -> Term.t

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

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

  • parameter sort

    The sort of the variable.

  • parameter symbol

    The symbol of the variable.

  • returns

    A term representing the variable.

Util

val substitute_term : Term.t -> (Term.t * Term.t) array -> Term.t

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

  • 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 : Term.t array -> (Term.t * Term.t) 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 terms

    The terms in which the keys are to be substituted.

  • parameter map

    The key/value associations.

OCaml

Innovation. Community. Security.