package z3

  1. Overview
  2. Docs
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 = {
  1. lower_is_inf : bool;
  2. lower_is_open : bool;
  3. lower : rcf_num;
  4. upper_is_inf : bool;
  5. upper_is_open : bool;
  6. upper : rcf_num;
}
val root_interval : context -> rcf_num -> interval option
type root = {
  1. obj : rcf_num;
  2. polynomial : rcf_num list;
  3. interval : interval option;
  4. 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