Add Expr constructors for the Reals SMT-LIB theory (#878)

This patch follows `Expr.Int` and adds constructors from the `Reals`
SMT-LIB theory to the `Expr` module.

src/lib/structures/expr.ml

@@ -2886,6 +2886,43 @@ module Ints = struct
   let ( > ) x y = y < x
 end
 
+
+(** Constructors from the smtlib theory of real numbers.
+    https://smtlib.cs.uiowa.edu/theories-Reals.shtml *)
+module Reals = struct
+  let of_int n = real (string_of_int n)
+
+  let ( ~$ ) = of_int
+
+  let of_Z n = real (Z.to_string n)
+
+  let ( ~$$ ) = of_Z
+
+  let of_Q q = real (Q.to_string q)
+
+  let ( ~$$$ ) = of_Q
+
+  let ( - ) x y = mk_term (Op Minus) [ x; y ] Treal
+
+  let ( ~- ) x = ~$0 - x
+
+  let ( + ) x y = mk_term (Op Plus) [ x; y ] Treal
+
+  let ( * ) x y = mk_term (Op Mult) [ x; y ] Treal
+
+  let ( / ) x y = mk_term (Op Div) [ x; y ] Treal
+
+  let ( ** ) x y = mk_term (Op Pow) [ x; y ] Treal
+
+  let ( <= ) x y = mk_builtin ~is_pos:true LE [ x; y ]
+
+  let ( >= ) x y = y <= x
+
+  let ( < ) x y = mk_builtin ~is_pos:true LT [x; y ]
+
+  let ( > ) x y = y < x
+end
+
 (** Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV
     logic.
 

src/lib/structures/expr.mli

@@ -383,6 +383,37 @@ module Ints : sig
   val ( > ) : t -> t -> t
 end
 
+(** Constructors from the smtlib theory of reals.
+    https://smtlib.cs.uiowa.edu/theories-Reals.shtml *)
+module Reals : sig
+  (* Conversion from int *)
+  val of_int : int -> t
+  val ( ~$ ) : int -> t
+
+  (* Conversion from ZArith *)
+  val of_Z : Z.t -> t
+  val ( ~$$ ) : Z.t -> t
+
+  val of_Q : Q.t -> t
+  val ( ~$$$ ) : Q.t -> t
+
+  (* Arithmetic operations *)
+  val ( + ) : t -> t -> t
+  val ( - ) : t -> t -> t
+  val ( ~- ) : t -> t
+  val ( * ) : t -> t -> t
+  val ( / ) : t -> t -> t
+
+  (* Exponentiation *)
+  val ( ** ) : t -> t -> t
+
+  (* Comparisons *)
+  val ( <= ) : t -> t -> t
+  val ( >= ) : t -> t -> t
+  val ( < ) : t -> t -> t
+  val ( > ) : t -> t -> t
+end
+
 (** Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV
     logic.