z3 4.13.0 · OCaml Package

type rcf_num

val del : context -> rcf_num -> unit

val del_list : context -> rcf_num list -> unit

val mk_rational : context -> string -> rcf_num

val mk_small_int : context -> int -> rcf_num

val mk_pi : context -> rcf_num

val mk_e : context -> rcf_num

val mk_infinitesimal : context -> rcf_num

val mk_roots : context -> rcf_num list -> rcf_num list

val add : context -> rcf_num -> rcf_num -> rcf_num

val sub : context -> rcf_num -> rcf_num -> rcf_num

val mul : context -> rcf_num -> rcf_num -> rcf_num

val div : context -> rcf_num -> rcf_num -> rcf_num

val neg : context -> rcf_num -> rcf_num

val inv : context -> rcf_num -> rcf_num

val power : context -> rcf_num -> int -> rcf_num

val lt : context -> rcf_num -> rcf_num -> bool

val gt : context -> rcf_num -> rcf_num -> bool

val le : context -> rcf_num -> rcf_num -> bool

val ge : context -> rcf_num -> rcf_num -> bool

val eq : context -> rcf_num -> rcf_num -> bool

val neq : context -> rcf_num -> rcf_num -> bool

val num_to_string : context -> rcf_num -> bool -> bool -> string

val num_to_decimal_string : context -> rcf_num -> int -> string

val get_numerator_denominator : context -> rcf_num -> rcf_num * rcf_num

val is_rational : context -> rcf_num -> bool

val is_algebraic : context -> rcf_num -> bool

val is_infinitesimal : context -> rcf_num -> bool

val is_transcendental : context -> rcf_num -> bool

val extension_index : context -> rcf_num -> int

val transcendental_name : context -> rcf_num -> Symbol.symbol

val infinitesimal_name : context -> rcf_num -> Symbol.symbol

val num_coefficients : context -> rcf_num -> int

val get_coefficient : context -> rcf_num -> int -> rcf_num

val coefficients : context -> rcf_num -> rcf_num list

val sign_condition_sign : context -> rcf_num -> int -> int

val num_sign_condition_coefficients : context -> rcf_num -> int -> int

val sign_condition_coefficient : context -> rcf_num -> int -> int -> rcf_num

val sign_conditions : context -> rcf_num -> (rcf_num list * int) list

type interval = {

lower_is_inf : bool;
lower_is_open : bool;
lower : rcf_num;
upper_is_inf : bool;
upper_is_open : bool;
upper : rcf_num;

}

val root_interval : context -> rcf_num -> interval option

type root = {

obj : rcf_num;
polynomial : rcf_num list;
interval : interval option;
sign_conditions : (rcf_num list * int) list;

}

val roots : context -> rcf_num list -> root list

val del_root : context -> root -> unit

val del_roots : context -> root list -> unit

package z3