z3 4.11.2 · OCaml Package

module RoundingMode : sig ... end

val mk_sort : context -> int -> int -> Sort.sort

val mk_sort_half : context -> Sort.sort

val mk_sort_16 : context -> Sort.sort

val mk_sort_single : context -> Sort.sort

val mk_sort_32 : context -> Sort.sort

val mk_sort_double : context -> Sort.sort

val mk_sort_64 : context -> Sort.sort

val mk_sort_quadruple : context -> Sort.sort

val mk_sort_128 : context -> Sort.sort

val mk_nan : context -> Sort.sort -> Expr.expr

val mk_inf : context -> Sort.sort -> bool -> Expr.expr

val mk_zero : context -> Sort.sort -> bool -> Expr.expr

val mk_fp : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr

val mk_numeral_f : context -> float -> Sort.sort -> Expr.expr

val mk_numeral_i : context -> int -> Sort.sort -> Expr.expr

val mk_numeral_i_u : 
  context ->
  bool ->
  int64 ->
  int64 ->
  Sort.sort ->
  Expr.expr

val mk_numeral_s : context -> string -> Sort.sort -> Expr.expr

val is_fp : Expr.expr -> bool

val is_abs : Expr.expr -> bool

val is_neg : Expr.expr -> bool

val is_add : Expr.expr -> bool

val is_sub : Expr.expr -> bool

val is_mul : Expr.expr -> bool

val is_div : Expr.expr -> bool

val is_fma : Expr.expr -> bool

val is_sqrt : Expr.expr -> bool

val is_rem : Expr.expr -> bool

val is_round_to_integral : Expr.expr -> bool

val is_min : Expr.expr -> bool

val is_max : Expr.expr -> bool

val is_leq : Expr.expr -> bool

val is_lt : Expr.expr -> bool

val is_geq : Expr.expr -> bool

val is_gt : Expr.expr -> bool

val is_eq : Expr.expr -> bool

val is_is_normal : Expr.expr -> bool

val is_is_subnormal : Expr.expr -> bool

val is_is_zero : Expr.expr -> bool

val is_is_infinite : Expr.expr -> bool

val is_is_nan : Expr.expr -> bool

val is_is_negative : Expr.expr -> bool

val is_is_positive : Expr.expr -> bool

val is_to_fp : Expr.expr -> bool

val is_to_fp_unsigned : Expr.expr -> bool

val is_to_ubv : Expr.expr -> bool

val is_to_sbv : Expr.expr -> bool

val is_to_real : Expr.expr -> bool

val is_to_ieee_bv : Expr.expr -> bool

val mk_const : context -> Symbol.symbol -> Sort.sort -> Expr.expr

val mk_const_s : context -> string -> Sort.sort -> Expr.expr

val mk_abs : context -> Expr.expr -> Expr.expr

val mk_neg : context -> Expr.expr -> Expr.expr

val mk_add : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr

val mk_sub : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr

val mk_mul : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr

val mk_div : context -> Expr.expr -> Expr.expr -> Expr.expr -> Expr.expr

val mk_fma : 
  context ->
  Expr.expr ->
  Expr.expr ->
  Expr.expr ->
  Expr.expr ->
  Expr.expr

val mk_sqrt : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_rem : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_round_to_integral : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_min : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_max : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_leq : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_lt : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_geq : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_gt : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_eq : context -> Expr.expr -> Expr.expr -> Expr.expr

val mk_is_normal : context -> Expr.expr -> Expr.expr

val mk_is_subnormal : context -> Expr.expr -> Expr.expr

val mk_is_zero : context -> Expr.expr -> Expr.expr

val mk_is_infinite : context -> Expr.expr -> Expr.expr

val mk_is_nan : context -> Expr.expr -> Expr.expr

val mk_is_negative : context -> Expr.expr -> Expr.expr

val mk_is_positive : context -> Expr.expr -> Expr.expr

val mk_to_fp_bv : context -> Expr.expr -> Sort.sort -> Expr.expr

val mk_to_fp_float : 
  context ->
  Expr.expr ->
  Expr.expr ->
  Sort.sort ->
  Expr.expr

val mk_to_fp_real : context -> Expr.expr -> Expr.expr -> Sort.sort -> Expr.expr

val mk_to_fp_signed : 
  context ->
  Expr.expr ->
  Expr.expr ->
  Sort.sort ->
  Expr.expr

val mk_to_fp_unsigned : 
  context ->
  Expr.expr ->
  Expr.expr ->
  Sort.sort ->
  Expr.expr

val mk_to_ubv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr

val mk_to_sbv : context -> Expr.expr -> Expr.expr -> int -> Expr.expr

val mk_to_real : context -> Expr.expr -> Expr.expr

val get_ebits : context -> Sort.sort -> int

val get_sbits : context -> Sort.sort -> int

val get_numeral_sign : context -> Expr.expr -> bool * int

val get_numeral_sign_bv : context -> Expr.expr -> Expr.expr

val get_numeral_exponent_string : context -> Expr.expr -> bool -> string

val get_numeral_exponent_int : context -> Expr.expr -> bool -> bool * int64

val get_numeral_exponent_bv : context -> Expr.expr -> bool -> Expr.expr

val get_numeral_significand_bv : context -> Expr.expr -> Expr.expr

val get_numeral_significand_string : context -> Expr.expr -> string

val get_numeral_significand_uint : context -> Expr.expr -> bool * int64

val is_numeral_nan : context -> Expr.expr -> bool

val is_numeral_inf : context -> Expr.expr -> bool

val is_numeral_zero : context -> Expr.expr -> bool

val is_numeral_normal : context -> Expr.expr -> bool

val is_numeral_subnormal : context -> Expr.expr -> bool

val is_numeral_positive : context -> Expr.expr -> bool

val is_numeral_negative : context -> Expr.expr -> bool

val mk_to_ieee_bv : context -> Expr.expr -> Expr.expr

val mk_to_fp_int_real : 
  context ->
  Expr.expr ->
  Expr.expr ->
  Expr.expr ->
  Sort.sort ->
  Expr.expr

val numeral_to_string : Expr.expr -> string