Add RCF functions to OCaml API (#6932)

src/api/ml/z3.ml

@@ -2077,6 +2077,43 @@ struct
 end
 
 
+module RCF =
+struct
+  type rcf_num = Z3native.rcf_num
+
+  let del (ctx:context) (a:rcf_num) = Z3native.rcf_del ctx a
+  let mk_rational (ctx:context) (v:string) = Z3native.rcf_mk_rational ctx v
+  let mk_small_int (ctx:context) (v:int) = Z3native.rcf_mk_small_int ctx v
+
+  let mk_pi (ctx:context) = Z3native.rcf_mk_pi ctx
+  let mk_e (ctx:context) = Z3native.rcf_mk_e ctx
+  let mk_infinitesimal (ctx:context) = Z3native.rcf_mk_infinitesimal ctx
+
+  let mk_roots (ctx:context) (n:int) (a:rcf_num list) = let n, r = Z3native.rcf_mk_roots ctx n a in r
+
+  let add (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_add ctx a b
+  let sub (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_sub ctx a b
+  let mul (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_mul ctx a b
+  let div (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_div ctx a b
+
+  let neg (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+  let inv (ctx:context) (a:rcf_num) = Z3native.rcf_neg ctx a
+
+  let power (ctx:context) (a:rcf_num) (k:int) = Z3native.rcf_power ctx a k
+
+  let lt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_lt ctx a b
+  let gt (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_gt ctx a b
+  let le (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_le ctx a b
+  let ge (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_ge ctx a b
+  let eq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_eq ctx a b
+  let neq (ctx:context) (a:rcf_num) (b:rcf_num) = Z3native.rcf_neq ctx a b
+
+  let num_to_string (ctx:context) (a:rcf_num) (compact:bool) (html:bool) = Z3native.rcf_num_to_string ctx a compact html
+  let num_to_decimal_string (ctx:context) (a:rcf_num) (prec:int) = Z3native.rcf_num_to_decimal_string ctx a prec
+  let get_numerator_denominator (ctx:context) (a:rcf_num) = Z3native.rcf_get_numerator_denominator ctx a
+end
+
+
 let set_global_param = Z3native.global_param_set
 
 let get_global_param id =

src/api/ml/z3.mli

@@ -3535,6 +3535,81 @@ sig
   val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> AST.ASTVector.ast_vector
 end
 
+(** Real closed field *)
+module RCF :
+sig
+    type rcf_num
+
+    (** Delete a RCF numeral created using the RCF API. *)
+    val del : context -> rcf_num -> unit
+
+    (** Return a RCF rational using the given string. *)
+    val mk_rational : context -> string -> rcf_num
+
+    (** Return a RCF small integer. *)
+    val mk_small_int : context -> int -> rcf_num
+
+    (** Return Pi *)
+    val mk_pi : context -> rcf_num
+
+    (** Return e (Euler's constant) *)
+    val mk_e : context -> rcf_num
+
+    (** Return a new infinitesimal that is smaller than all elements in the Z3 field. *)
+    val mk_infinitesimal : context -> rcf_num
+
+    (** Extract the roots of a polynomial. Precondition: The input polynomial is not the zero polynomial. *)
+    val mk_roots : context -> int -> rcf_num list -> rcf_num list
+
+    (** Addition *)
+    val add : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Subtraction *)
+    val sub : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Multiplication *)
+    val mul : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Division *)
+    val div : context -> rcf_num -> rcf_num -> rcf_num
+
+    (** Negation *)
+    val neg : context -> rcf_num -> rcf_num
+
+    (** Multiplicative Inverse *)
+    val inv : context -> rcf_num -> rcf_num
+
+    (** Power *)
+    val power : context -> rcf_num -> int -> rcf_num
+
+    (** less-than *)
+    val lt : context -> rcf_num -> rcf_num -> bool
+
+    (** greater-than *)
+    val gt : context -> rcf_num -> rcf_num -> bool
+
+    (** less-than or equal *)
+    val le : context -> rcf_num -> rcf_num -> bool
+
+    (** greater-than or equal *)
+    val ge : context -> rcf_num -> rcf_num -> bool
+
+    (** equality *)
+    val eq : context -> rcf_num -> rcf_num -> bool
+
+    (** not equal *)
+    val neq : context -> rcf_num -> rcf_num -> bool
+
+    (** Convert the RCF numeral into a string. *)
+    val num_to_string : context -> rcf_num -> bool -> bool -> string
+
+    (** Convert the RCF numeral into a string in decimal notation. *)
+    val num_to_decimal_string : context -> rcf_num -> int -> string
+
+    (** Extract the "numerator" and "denominator" of the given RCF numeral.
+        We have that \ccode{a = n/d}, moreover \c n and \c d are not represented using rational functions. *)
+    val get_numerator_denominator : context -> rcf_num -> (rcf_num * rcf_num)
+end
 
 (** Set a global (or module) parameter, which is shared by all Z3 contexts.