Previous  Up  Next

Module Z3.RCF

module RCF: sig .. end

Real closed field

type rcf_num 
val del : context -> rcf_num -> unit

Delete a RCF numeral created using the RCF API.

val del_list : context -> rcf_num list -> unit

Delete RCF numerals created using the RCF API.

val mk_rational : context -> string -> rcf_num

Return a RCF rational using the given string.

val mk_small_int : context -> int -> rcf_num

Return a RCF small integer.

val mk_pi : context -> rcf_num

Return Pi

val mk_e : context -> rcf_num

Return e (Euler's constant)

val mk_infinitesimal : context -> rcf_num

Return a new infinitesimal that is smaller than all elements in the Z3 field.

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

Extract the roots of a polynomial. Precondition: The input polynomial is not the zero polynomial.

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

Addition

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

Subtraction

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

Multiplication

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

Division

val neg : context -> rcf_num -> rcf_num

Negation

val inv : context -> rcf_num -> rcf_num

Multiplicative Inverse

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

Power

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

less-than

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

greater-than

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

less-than or equal

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

greater-than or equal

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

equality

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

not equal

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

Convert the RCF numeral into a string.

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

Convert the RCF numeral into a string in decimal notation.

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

Extract the "numerator" and "denominator" of the given RCF numeral. We have that \ccode, moreover \c n and \c d are not represented using rational functions.

val is_rational : context -> rcf_num -> bool

Return \c true if \c a represents a rational number.

val is_algebraic : context -> rcf_num -> bool

Return \c true if \c a represents an algebraic number.

val is_infinitesimal : context -> rcf_num -> bool

Return \c true if \c a represents an infinitesimal.

val is_transcendental : context -> rcf_num -> bool

Return \c true if \c a represents a transcendental number.

val extension_index : context -> rcf_num -> int

Return the index of a field extension.

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

Return the name of a transcendental.

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

Return the name of an infinitesimal.

val num_coefficients : context -> rcf_num -> int

Return the number of coefficients in an algebraic number.

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

Extract a coefficient from an algebraic number.

val coefficients : context -> rcf_num -> rcf_num list

Extract the coefficients from an algebraic number.

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

Extract the sign of a sign condition from an algebraic number.

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

Return the size of a sign condition polynomial.

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

Extract a sign condition polynomial coefficient from an algebraic number.

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

Extract sign conditions from an algebraic number.

type interval = {
   lower_is_inf : bool;
   lower_is_open : bool;
   lower : rcf_num;
   upper_is_inf : bool;
   upper_is_open : bool;
   upper : rcf_num;
}

Extract the interval from an algebraic number.

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