z3 4.12.6 · OCaml Package

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

val is_bv : Expr.expr -> bool

val is_bv_numeral : Expr.expr -> bool

val is_bv_bit1 : Expr.expr -> bool

val is_bv_bit0 : Expr.expr -> bool

val is_bv_uminus : Expr.expr -> bool

val is_bv_add : Expr.expr -> bool

val is_bv_sub : Expr.expr -> bool

val is_bv_mul : Expr.expr -> bool

val is_bv_sdiv : Expr.expr -> bool

val is_bv_udiv : Expr.expr -> bool

val is_bv_SRem : Expr.expr -> bool

val is_bv_urem : Expr.expr -> bool

val is_bv_smod : Expr.expr -> bool

val is_bv_sdiv0 : Expr.expr -> bool

val is_bv_udiv0 : Expr.expr -> bool

val is_bv_srem0 : Expr.expr -> bool

val is_bv_urem0 : Expr.expr -> bool

val is_bv_smod0 : Expr.expr -> bool

val is_bv_ule : Expr.expr -> bool

val is_bv_sle : Expr.expr -> bool

val is_bv_uge : Expr.expr -> bool

val is_bv_sge : Expr.expr -> bool

val is_bv_ult : Expr.expr -> bool

val is_bv_slt : Expr.expr -> bool

val is_bv_ugt : Expr.expr -> bool

val is_bv_sgt : Expr.expr -> bool

val is_bv_and : Expr.expr -> bool

val is_bv_or : Expr.expr -> bool

val is_bv_not : Expr.expr -> bool

val is_bv_xor : Expr.expr -> bool

val is_bv_nand : Expr.expr -> bool

val is_bv_nor : Expr.expr -> bool

val is_bv_xnor : Expr.expr -> bool

val is_bv_concat : Expr.expr -> bool

val is_bv_signextension : Expr.expr -> bool

val is_bv_zeroextension : Expr.expr -> bool

val is_bv_extract : Expr.expr -> bool

val is_bv_repeat : Expr.expr -> bool

val is_bv_reduceor : Expr.expr -> bool

val is_bv_reduceand : Expr.expr -> bool

val is_bv_comp : Expr.expr -> bool

val is_bv_shiftleft : Expr.expr -> bool

val is_bv_shiftrightlogical : Expr.expr -> bool

val is_bv_shiftrightarithmetic : Expr.expr -> bool

val is_bv_rotateleft : Expr.expr -> bool

val is_bv_rotateright : Expr.expr -> bool

val is_bv_rotateleftextended : Expr.expr -> bool

val is_bv_rotaterightextended : Expr.expr -> bool

val is_int2bv : Expr.expr -> bool

val is_bv2int : Expr.expr -> bool

val is_bv_carry : Expr.expr -> bool

val is_bv_xor3 : Expr.expr -> bool

val get_size : Sort.sort -> int

val numeral_to_string : Expr.expr -> string

val mk_const : context -> Symbol.symbol -> int -> Expr.expr

val mk_const_s : context -> string -> int -> Expr.expr

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

val mk_numeral : context -> string -> int -> Expr.expr

package z3