package bitwuzla-cxx

You can search for identifiers within the package.

in-package search v0.2.0

bitwuzla-cxx
- Bitwuzla_cxx
  - Kind
  - Make
    
    Kind
    
    Result
    
    RoundingMode
    
    Solver
    
    Sort
    
    Term
  - Options
  - Result
  - RoundingMode
  - S
    
    Kind
    
    Result
    
    RoundingMode
    
    Solver
    
    Sort
    
    Term
  - Solver
  - Sort
  - Term

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

see https://bitwuzla.github.io/docs/cpp/api.html

val copyright : unit -> string

copyright () get copyright information.

val version : unit -> string

version () get version information.

module Options : sig ... end

module type S = sig ... end

Signature of a Bitwuzla instance.

module Make () : S

Create a new independent Bitwuzla instance that can run in parallel to all other ones.

include S

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.