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.

mk_bool_sort () create a Boolean sort.

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

• returns

  A Boolean sort.

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.

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.

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.

mk_rm_sort () create a Roundingmode sort.

• returns

  A Roundingmode sort.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

mk_rm_value rm create a rounding mode value.

• parameter rm

  The rounding mode value.

• returns

  A term representing the rounding mode value.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.