From b553807f7703a93317c9b52babd246b49d70c7fb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Fri, 13 Oct 2023 12:39:29 +0000
Subject: [PATCH] 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  | 37 +++++++++++++++++++++++++++++++++++++
 src/lib/structures/expr.mli | 31 +++++++++++++++++++++++++++++++
 2 files changed, 68 insertions(+)

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index d544058ba..baf2525a4 100644
--- a/src/lib/structures/expr.ml
+++ b/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.
 
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 03010b631..76fbeef37 100644
--- a/src/lib/structures/expr.mli
+++ b/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.