Add Expr constructors for Reals and Reals_Ints

This patch adds constructors for the `Reals` and `Reals_Ints` SMT-LIB
theories.

src/lib/structures/expr.ml

@@ -2886,6 +2886,76 @@ 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 theories of real numbers and integers.
+
+    Constants and comparisons are not provided to avoid type confusion bugs. Use
+    the constants and comparisons from [Reals] or [Ints] as appropriate.
+
+    https://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml *)
+module Reals_Ints = struct
+  (* Integer operators *)
+  let ( - ) = Ints.( - )
+  let ( ~- ) = Ints.( ~- )
+  let ( + ) = Ints.( + )
+  let ( * ) = Ints.( * )
+  let ( / ) = Ints.( / )
+  let ( mod ) = Ints.( mod )
+  let abs = Ints.abs
+  let ( ** ) = Ints.( ** )
+
+  (* Real operators *)
+  let ( -. ) = Reals.( - )
+  let ( ~-. ) = Reals.( ~- )
+  let ( +. ) = Reals.( + )
+  let ( *. ) = Reals.( * )
+  let ( /. ) = Reals.( / )
+  let ( **. ) = Reals.( ** )
+
+  (* Conversion operators *)
+  let to_real n = mk_term (Op Real_of_int) [ n ] Treal
+
+  let to_int n = mk_term (Op Int_floor) [ n ] Tint
+
+  let is_int n = mk_term (Op Real_is_int) [ n ] Tbool
+end
+
 (** Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV
     logic.
 

src/lib/structures/expr.mli

@@ -383,6 +383,68 @@ 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 theories of real numbers and integers.
+
+    Constants and comparisons are not provided to avoid type confusion bugs. Use
+    the constants and comparisons from [Reals] or [Ints] as appropriate.
+
+    https://smtlib.cs.uiowa.edu/theories-Reals_Ints.shtml *)
+module Reals_Ints : sig
+  (* Integer operations *)
+  val ( + ) : t -> t -> t
+  val ( - ) : t -> t -> t
+  val ( ~- ) : t -> t
+  val ( * ) : t -> t -> t
+  val ( / ) : t -> t -> t
+  val ( mod ) : t -> t -> t
+  val abs : t -> t
+  val ( ** ) : t -> t -> t
+
+  (* Real operations *)
+  val ( +. ) : t -> t -> t
+  val ( -. ) : t -> t -> t
+  val ( ~-. ) : t -> t
+  val ( *. ) : t -> t -> t
+  val ( /. ) : t -> t -> t
+  val ( **. ) : t -> t -> t
+
+  (* Conversions *)
+  val to_real : t -> t
+  val to_int : t -> t
+  val is_int : t -> t
+end
+
 (** Constructors from the smtlib theory of fixed-size bit-vectors and the QF_BV
     logic.