feat: Exact precision representable reals

src/smtml/eval.ml

@@ -38,6 +38,7 @@ type error_kind =
   | `Integer_overflow
   | `Index_out_of_bounds
   | `Invalid_format_conversion
+  | `Negative_sqrt
   | `Unsupported_operator of op_type * Ty.t
   | `Unsupported_theory of Ty.t
   | `Type_error of type_error_info
@@ -194,41 +195,112 @@ module Int = struct
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     match op with
     | OfBool -> to_int (of_bool v)
-    | Reinterpret_float -> Int (Int.of_float (of_real 1 (`Cvtop op) v))
+    | Reinterpret_float ->
+      Int
+        begin match of_real 1 (`Cvtop op) v with
+        | Exact v -> Q.to_int v
+        | Approx v -> Int.of_float v
+        end
     | _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_int))
 end
 
 module Real = struct
   let unop (op : Ty.Unop.t) (v : Value.t) : Value.t =
     let v = of_real 1 (`Unop op) v in
-    match op with
-    | Neg -> to_real @@ Float.neg v
-    | Abs -> to_real @@ Float.abs v
-    | Sqrt -> to_real @@ Float.sqrt v
-    | Nearest -> to_real @@ Float.round v
-    | Ceil -> to_real @@ Float.ceil v
-    | Floor -> to_real @@ Float.floor v
-    | Trunc -> to_real @@ Float.trunc v
-    | Is_nan -> if Float.is_nan v then Value.True else Value.False
-    | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    let sqrt_q (q : Q.t) =
+      let n = Q.num q in
+      let d = Q.den q in
+      if Z.sign n < 0 then eval_error `Negative_sqrt
+      else
+        let n_root, n_rem = Z.sqrt_rem n in
+        let d_root, d_rem = Z.sqrt_rem d in
+        if Z.equal n_rem Z.zero && Z.equal d_rem Z.zero then
+          to_real (Exact (Q.make n_root d_root))
+        else to_real (Approx (Q.to_float q |> sqrt))
+    in
+    let nearest_q (q : Q.t) =
+      let n = Q.num q in
+      let d = Q.den q in
+      let near =
+        if Z.geq n Z.zero then Z.div (Z.add n (Z.div d (Z.of_int 2))) d
+        else Z.div (Z.sub n (Z.div d (Z.of_int 2))) d
+      in
+      to_real (Exact (Q.of_bigint near))
+    in
+    let approx_ops =
+     fun v ->
+      let to_real v = to_real (Approx v) in
+      match op with
+      | Neg -> to_real @@ Float.neg v
+      | Abs -> to_real @@ Float.abs v
+      | Sqrt -> to_real @@ Float.sqrt v
+      | Nearest -> to_real @@ Float.round v
+      | Ceil -> to_real @@ Float.ceil v
+      | Floor -> to_real @@ Float.floor v
+      | Trunc -> to_real @@ Float.trunc v
+      | Is_nan -> if Float.is_nan v then Value.True else Value.False
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    in
+    let exact_ops =
+     fun v ->
+      let to_real v = to_real (Exact v) in
+      match op with
+      | Neg -> to_real @@ Q.neg v
+      | Abs -> to_real @@ Q.abs v
+      | Sqrt -> sqrt_q v
+      | Nearest -> nearest_q v
+      | Ceil -> to_real @@ Q.of_bigint @@ Z.cdiv (Q.num v) (Q.den v)
+      | Floor -> to_real @@ Q.of_bigint @@ Z.fdiv (Q.num v) (Q.den v)
+      | Trunc -> to_real @@ Q.of_bigint @@ Z.div (Q.num v) (Q.den v)
+      | Is_nan -> (
+        match Q.classify v with Q.UNDEF -> Value.True | _ -> Value.False )
+      | _ -> eval_error (`Unsupported_operator (`Unop op, Ty_real))
+    in
+    match v with Exact v -> exact_ops v | Approx v -> approx_ops v
 
   let binop (op : Ty.Binop.t) (v1 : Value.t) (v2 : Value.t) : Value.t =
-    let f =
+    let rem_q (a : Q.t) (b : Q.t) : Q.t =
+      if Q.equal b Q.zero then eval_error `Divide_by_zero;
+      let div = Q.div a b in
+      let k = Q.of_bigint (Z.div (Q.num div) (Q.den div)) in
+      Q.sub a (Q.mul b k)
+    in
+    let approx_op v1 v2 : Value.real =
+      match op with
+      | Add -> Approx (Float.add v1 v2)
+      | Sub -> Approx (Float.sub v1 v2)
+      | Mul -> Approx (Float.mul v1 v2)
+      | Div -> Approx (Float.div v1 v2)
+      | Rem -> Approx (Float.rem v1 v2)
+      | Min -> Approx (Float.min v1 v2)
+      | Max -> Approx (Float.max v1 v2)
+      | Pow -> Approx (Float.pow v1 v2)
+      | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))
+    in
+    let exact_op v1 v2 : Value.real =
       match op with
-      | Add -> Float.add
-      | Sub -> Float.sub
-      | Mul -> Float.mul
-      | Div -> Float.div
-      | Rem -> Float.rem
-      | Min -> Float.min
-      | Max -> Float.max
-      | Pow -> Float.pow
+      | Add -> Exact (Q.add v1 v2)
+      | Sub -> Exact (Q.sub v1 v2)
+      | Mul -> Exact (Q.mul v1 v2)
+      | Div -> Exact (Q.div v1 v2)
+      | Rem -> Exact (rem_q v1 v2)
+      | Min -> Exact (Q.min v1 v2)
+      | Max -> Exact (Q.max v1 v2)
+      | Pow -> Approx (Float.pow (Q.to_float v1) (Q.to_float v2))
       | _ -> eval_error (`Unsupported_operator (`Binop op, Ty_real))
     in
-    to_real (f (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
+    let push_approx_op (v1 : Value.real) (v2 : Value.real) =
+      match (v1, v2) with
+      | Exact v1, Exact v2 -> exact_op v1 v2
+      | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
+      | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
+      | Approx v1, Approx v2 -> approx_op v1 v2
+    in
+    to_real
+      (push_approx_op (of_real 1 (`Binop op) v1) (of_real 2 (`Binop op) v2))
 
   let relop (op : Ty.Relop.t) (v1 : Value.t) (v2 : Value.t) : bool =
-    let f =
+    let approx_op =
       match op with
       | Lt -> Float.Infix.( < )
       | Le -> Float.Infix.( <= )
@@ -238,19 +310,53 @@ module Real = struct
       | Ne -> Float.Infix.( <> )
       | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))
     in
-    f (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)
+    let exact_op =
+      match op with
+      | Lt -> Q.lt
+      | Le -> Q.leq
+      | Gt -> Q.gt
+      | Ge -> Q.geq
+      | Eq -> Q.equal
+      | Ne -> fun v1 v2 -> Fun.negate (Q.equal v1) v2
+      | _ -> eval_error (`Unsupported_operator (`Relop op, Ty_real))
+    in
+    let push_approx_op (v1 : Value.real) (v2 : Value.real) =
+      match (v1, v2) with
+      | Exact v1, Exact v2 -> exact_op v1 v2
+      | Exact v1, Approx v2 -> approx_op (Q.to_float v1) v2
+      | Approx v1, Exact v2 -> approx_op v1 (Q.to_float v2)
+      | Approx v1, Approx v2 -> approx_op v1 v2
+    in
+    push_approx_op (of_real 1 (`Relop op) v1) (of_real 2 (`Relop op) v2)
 
   let cvtop (op : Ty.Cvtop.t) (v : Value.t) : Value.t =
     let op' = `Cvtop op in
     match op with
-    | ToString -> Str (Float.to_string (of_real 1 op' v))
+    | ToString ->
+      Str
+        begin match of_real 1 op' v with
+        | Exact v -> Q.to_string v
+        | Approx v -> Float.to_string v
+        end
     | OfString -> begin
-      match float_of_string_opt (of_str 1 op' v) with
-      | None -> eval_error `Invalid_format_conversion
-      | Some v -> to_real v
+      match of_str 1 op' v with
+      | float_str when String.contains float_str '.' -> begin
+        match Float.of_string_opt float_str with
+        | Some f -> to_real (Approx f)
+        | None -> eval_error `Invalid_format_conversion
+      end
+      | q_str -> begin
+        try to_real (Exact (Q.of_string q_str))
+        with _ -> eval_error `Invalid_format_conversion
+      end
     end
-    | Reinterpret_int -> to_real (float_of_int (of_int 1 op' v))
-    | Reinterpret_float -> to_int (Float.to_int (of_real 1 op' v))
+    | Reinterpret_int -> to_real (Exact (Q.of_int @@ of_int 1 op' v))
+    | Reinterpret_float ->
+      to_int
+        begin match of_real 1 op' v with
+        | Exact v -> Q.to_int v
+        | Approx v -> Float.to_int v
+        end
     | _ -> eval_error (`Unsupported_operator (op', Ty_real))
 end
 
@@ -408,7 +514,7 @@ module Str = struct
       let s = of_str 1 op' v in
       match float_of_string_opt s with
       | None -> eval_error `Invalid_format_conversion
-      | Some f -> to_real f
+      | Some f -> to_real (Approx f)
     end
     | _ -> eval_error (`Unsupported_operator (`Cvtop op, Ty_str))
 

src/smtml/eval.mli

@@ -37,6 +37,7 @@ type error_kind =
   | `Integer_overflow
   | `Index_out_of_bounds
   | `Invalid_format_conversion
+  | `Negative_sqrt
   | `Unsupported_operator of op_type * Ty.t
   | `Unsupported_theory of Ty.t
   | `Type_error of type_error_info

src/smtml/expr.ml

@@ -277,7 +277,7 @@ let normalize_eq_or_ne op (ty', e1, e2) =
       make_relop binop zero
     | Ty_real ->
       let binop = make (Binop (ty1, Sub, e1, e2)) in
-      let zero = make (Val (Real 0.)) in
+      let zero = make (Val (Real (Exact Q.zero))) in
       make_relop binop zero
     | _ -> make_relop e1 e2
   end
@@ -394,12 +394,16 @@ let raw_relop ty op hte1 hte2 = make (Relop (ty, op, hte1, hte2)) [@@inline]
 let rec relop ty op hte1 hte2 =
   match (op, view hte1, view hte2) with
   | op, Val v1, Val v2 -> value (if Eval.relop ty op v1 v2 then True else False)
-  | Ty.Relop.Ne, Val (Real v), _ | Ne, _, Val (Real v) ->
+  | Ty.Relop.Ne, Val (Real (Approx v)), _ | Ne, _, Val (Real (Approx v)) ->
     if Float.is_nan v || Float.is_infinite v then value True
     else raw_relop ty op hte1 hte2
-  | _, Val (Real v), _ | _, _, Val (Real v) ->
+  | Ty.Relop.Ne, Val (Real (Exact v)), _ | Ne, _, Val (Real (Exact v)) ->
+    if Fun.negate Q.is_real v then value True else raw_relop ty op hte1 hte2
+  | _, Val (Real (Approx v)), _ | _, _, Val (Real (Approx v)) ->
     if Float.is_nan v || Float.is_infinite v then value False
     else raw_relop ty op hte1 hte2
+  | _, Val (Real (Exact v)), _ | _, _, Val (Real (Exact v)) ->
+    if Fun.negate Q.is_real v then value False else raw_relop ty op hte1 hte2
   | Eq, _, Val Nothing | Eq, Val Nothing, _ -> value False
   | Ne, _, Val Nothing | Ne, Val Nothing, _ -> value True
   | Eq, _, Val (App (`Op "symbol", [ Str _ ]))

src/smtml/mappings.ml

@@ -162,8 +162,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let open M in
         match op with
         | Unop.Neg -> Real.neg e
-        | Abs -> ite (Real.gt e (real 0.)) e (Real.neg e)
-        | Sqrt -> Real.pow e (v 0.5)
+        | Abs -> ite (Real.gt e (real (Exact Q.zero))) e (Real.neg e)
+        | Sqrt -> Real.pow e (v (Exact (Q.make (Z.of_int 1) (Z.of_int 2))))
         | Ceil ->
           let x_int = M.Real.to_int e in
           ite (eq (Int.to_real x_int) e) x_int (Int.add x_int (int 1))

src/smtml/mappings_intf.ml

@@ -47,7 +47,7 @@ module type M = sig
   val int : int -> term
 
   (** [real f] constructs a real number term from the given float [f]. *)
-  val real : float -> term
+  val real : Value.real -> term
 
   (** [const name ty] constructs a constant term with the given name and type.
   *)
@@ -143,7 +143,7 @@ module type M = sig
     val to_int : interp -> int
 
     (** [to_real interp] converts an interpretation to a real number. *)
-    val to_real : interp -> float
+    val to_real : interp -> Value.real
 
     (** [to_bool interp] converts an interpretation to a Boolean. *)
     val to_bool : interp -> bool

src/smtml/parser.mly

@@ -88,7 +88,7 @@ let paren_op :=
 
 let spec_constant :=
   | x = NUM; { Int x }
-  | x = DEC; { Real x }
+  | x = DEC; { Real (Approx x) }
   | x = STR; { Str x }
   | x = BOOL; { if x then True else False }
   | LPAREN; ty = TYPE; x = NUM; RPAREN;

src/smtml/smtlib.ml

@@ -107,9 +107,8 @@ module Term = struct
     | None -> Fmt.failwith "%ainvalid int" pp_loc loc
 
   let real ?loc (x : string) =
-    match float_of_string_opt x with
-    | Some x -> Expr.value (Real x)
-    | None -> Fmt.failwith "%ainvalid real" pp_loc loc
+    try Expr.value (Real (Exact (Q.of_string x)))
+    with _ -> Fmt.failwith "%ainvalid real" pp_loc loc
 
   let hexa ?loc:_ (h : string) =
     let len = String.length h in

src/smtml/value.ml

@@ -4,12 +4,16 @@
 
 open Ty
 
+type real =
+  | Exact of Q.t
+  | Approx of float
+
 type t =
   | True
   | False
   | Unit
   | Int of int
-  | Real of float
+  | Real of real
   | Str of string
   | Num of Num.t
   | Bitv of Bitvector.t
@@ -49,7 +53,10 @@ let rec compare (a : t) (b : t) : int =
   | False, True -> -1
   | True, False -> 1
   | Int a, Int b -> Int.compare a b
-  | Real a, Real b -> Float.compare a b
+  | Real (Exact a), Real (Exact b) -> Q.compare a b
+  | Real (Approx a), Real (Approx b) -> Float.compare a b
+  | Real (Approx _), Real (Exact _) -> -1
+  | Real (Exact _), Real (Approx _) -> 1
   | Str a, Str b -> String.compare a b
   | Num a, Num b -> Num.compare a b
   | Bitv a, Bitv b -> Bitvector.compare a b
@@ -67,7 +74,9 @@ let rec equal (v1 : t) (v2 : t) : bool =
   match (v1, v2) with
   | True, True | False, False | Unit, Unit | Nothing, Nothing -> true
   | Int a, Int b -> Int.equal a b
-  | Real a, Real b -> Float.equal a b
+  | Real (Exact a), Real (Exact b) -> Q.equal a b
+  | Real (Approx a), Real (Approx b) -> Float.equal a b
+  | Real (Approx _), Real (Exact _) | Real (Exact _), Real (Approx _) -> false
   | Str a, Str b -> String.equal a b
   | Num a, Num b -> Num.equal a b
   | Bitv a, Bitv b -> Bitvector.equal a b
@@ -88,7 +97,8 @@ let rec pp fmt = function
   | False -> Fmt.string fmt "false"
   | Unit -> Fmt.string fmt "unit"
   | Int x -> Fmt.int fmt x
-  | Real x -> Fmt.pf fmt "%F" x
+  | Real (Exact x) -> Q.pp_print fmt x
+  | Real (Approx x) -> Fmt.pf fmt "%F" x
   | Num x -> Num.pp fmt x
   | Bitv bv -> Bitvector.pp fmt bv
   | Str x -> Fmt.pf fmt "%S" x
@@ -117,9 +127,8 @@ let of_string (cast : Ty.t) v =
     | None -> Fmt.error_msg "invalid value %s, expected integer" v
     | Some n -> Ok (Int n) )
   | Ty_real -> (
-    match float_of_string_opt v with
-    | None -> Fmt.error_msg "invalid value %s, expected real" v
-    | Some n -> Ok (Real n) )
+    try Ok (Real (Exact (Q.of_string v)))
+    with _ -> Fmt.error_msg "invalid value %s, expected real" v )
   | Ty_str -> Ok (Str v)
   | Ty_app | Ty_list | Ty_none | Ty_unit | Ty_regexp | Ty_roundingMode ->
     Fmt.error_msg "unsupported parsing values of type %a" Ty.pp cast
@@ -130,7 +139,11 @@ let rec to_json (v : t) : Yojson.Basic.t =
   | False -> `Bool false
   | Unit -> `String "unit"
   | Int int -> `Int int
-  | Real real -> `Float real
+  | Real (Exact r) ->
+    let num = r |> Q.num |> Z.to_int in
+    let den = r |> Q.den |> Z.to_int in
+    `Assoc [ ("num", `Int num); ("den", `Int den) ]
+  | Real (Approx r) -> `Float r
   | Str str -> `String str
   | Num n -> Num.to_json n
   | Bitv bv -> Bitvector.to_json bv
@@ -143,7 +156,8 @@ module Smtlib = struct
     | True -> Fmt.string fmt "true"
     | False -> Fmt.string fmt "false"
     | Int x -> Fmt.int fmt x
-    | Real x -> Fmt.pf fmt "%F" x
+    | Real (Exact x) -> Q.pp_print fmt x
+    | Real (Approx x) -> Fmt.pf fmt "%F" x
     | Num x -> Num.pp fmt x
     | Bitv bv -> Bitvector.pp fmt bv
     | Str x -> Fmt.pf fmt "%S" x