Add RCF functions to OCaml API (#6932)

examples/ml/ml_example.ml

@@ -315,7 +315,21 @@ let fpa_example ( ctx : context ) =
 	  Printf.printf "Test passed.\n"
   ) 
 
-let _ = 
+(**
+	A basic example of RCF usage
+**)
+let rcf_example ( ctx : context ) =
+  Printf.printf "RCFExample\n" ;
+  let pi = RCF.mk_pi ctx in
+  let e = RCF.mk_e ctx in
+  (Printf.printf "e: %s,  pi: %s, e==pi: %b, e < pi: %b\n"
+    (RCF.num_to_string ctx e true false)
+    (RCF.num_to_string ctx pi true false)
+    (RCF.eq ctx e pi)
+    (RCF.lt ctx e pi)) ;
+  Printf.printf "Test passed.\n"
+
+let _ =
   try (
     if not (Log.open_ "z3.log") then
       raise (TestFailedException "Log couldn't be opened.")
@@ -340,6 +354,7 @@ let _ =
 	basic_tests ctx ;
 	quantifier_example1 ctx ;
 	fpa_example ctx ;
+  rcf_example ctx ;
 	Printf.printf "Disposing...\n";
 	Gc.full_major ()
       );

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.