sig
  type rcf_num
  val del : Z3.context -> Z3.RCF.rcf_num -> unit
  val del_list : Z3.context -> Z3.RCF.rcf_num list -> unit
  val mk_rational : Z3.context -> string -> Z3.RCF.rcf_num
  val mk_small_int : Z3.context -> int -> Z3.RCF.rcf_num
  val mk_pi : Z3.context -> Z3.RCF.rcf_num
  val mk_e : Z3.context -> Z3.RCF.rcf_num
  val mk_infinitesimal : Z3.context -> Z3.RCF.rcf_num
  val mk_roots : Z3.context -> Z3.RCF.rcf_num list -> Z3.RCF.rcf_num list
  val add : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val sub : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val mul : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val div : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val neg : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val inv : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num
  val power : Z3.context -> Z3.RCF.rcf_num -> int -> Z3.RCF.rcf_num
  val lt : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val gt : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val le : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val ge : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val eq : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val neq : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num -> bool
  val num_to_string : Z3.context -> Z3.RCF.rcf_num -> bool -> bool -> string
  val num_to_decimal_string : Z3.context -> Z3.RCF.rcf_num -> int -> string
  val get_numerator_denominator :
    Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num * Z3.RCF.rcf_num
  val is_rational : Z3.context -> Z3.RCF.rcf_num -> bool
  val is_algebraic : Z3.context -> Z3.RCF.rcf_num -> bool
  val is_infinitesimal : Z3.context -> Z3.RCF.rcf_num -> bool
  val is_transcendental : Z3.context -> Z3.RCF.rcf_num -> bool
  val extension_index : Z3.context -> Z3.RCF.rcf_num -> int
  val transcendental_name : Z3.context -> Z3.RCF.rcf_num -> Z3.Symbol.symbol
  val infinitesimal_name : Z3.context -> Z3.RCF.rcf_num -> Z3.Symbol.symbol
  val num_coefficients : Z3.context -> Z3.RCF.rcf_num -> int
  val get_coefficient : Z3.context -> Z3.RCF.rcf_num -> int -> Z3.RCF.rcf_num
  val coefficients : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.rcf_num list
  val sign_condition_sign : Z3.context -> Z3.RCF.rcf_num -> int -> int
  val num_sign_condition_coefficients :
    Z3.context -> Z3.RCF.rcf_num -> int -> int
  val sign_condition_coefficient :
    Z3.context -> Z3.RCF.rcf_num -> int -> int -> Z3.RCF.rcf_num
  val sign_conditions :
    Z3.context -> Z3.RCF.rcf_num -> (Z3.RCF.rcf_num list * int) list
  type interval = {
    lower_is_inf : bool;
    lower_is_open : bool;
    lower : Z3.RCF.rcf_num;
    upper_is_inf : bool;
    upper_is_open : bool;
    upper : Z3.RCF.rcf_num;
  }
  val root_interval : Z3.context -> Z3.RCF.rcf_num -> Z3.RCF.interval option
  type root = {
    obj : Z3.RCF.rcf_num;
    polynomial : Z3.RCF.rcf_num list;
    interval : Z3.RCF.interval option;
    sign_conditions : (Z3.RCF.rcf_num list * int) list;
  }
  val roots : Z3.context -> Z3.RCF.rcf_num list -> Z3.RCF.root list
  val del_root : Z3.context -> Z3.RCF.root -> unit
  val del_roots : Z3.context -> Z3.RCF.root list -> unit
end