Add RoundingMode sort

Author: filipeom

src/smtml/bitwuzla_mappings.default.ml

@@ -79,6 +79,8 @@ module Fresh_bitwuzla (B : Bitwuzla_cxx.S) : M = struct
 
     let float ebits sbits = mk_fp_sort ebits sbits
 
+    let roundingMode = mk_rm_sort ()
+
     let ty t = Term.sort t
 
     let to_ety _ = Fmt.failwith "Bitwuzla_mappings: to_ety not implemented"

src/smtml/cvc5_mappings.default.ml

@@ -77,6 +77,8 @@ module Fresh_cvc5 () = struct
 
     let float ebits sbits = Sort.mk_fp_sort tm ebits sbits
 
+    let roundingMode = Sort.mk_rm_sort tm
+
     let ty t = Term.sort t
 
     let to_ety _ = assert false

src/smtml/dolmenexpr_to_expr.mli

@@ -90,6 +90,8 @@ module DolmenIntf : sig
 
     val float : int -> int -> ty
 
+    val roundingMode : ty
+
     val ty : term -> ty
 
     val to_ety : ty -> Ty.t

src/smtml/eval.ml

@@ -1049,7 +1049,8 @@ let op int real bool str lst bv f32 f64 ty op =
   | Ty_bitv _ -> bv op
   | Ty_fp 32 -> f32 op
   | Ty_fp 64 -> f64 op
-  | Ty_fp _ | Ty_app | Ty_unit | Ty_none | Ty_regexp -> assert false
+  | Ty_fp _ | Ty_app | Ty_unit | Ty_none | Ty_regexp | Ty_roundingMode ->
+    assert false
 [@@inline]
 
 let unop =

src/smtml/mappings.ml

@@ -65,6 +65,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty_bitv n -> M.Types.bitv n
       | Ty_fp 32 -> f32
       | Ty_fp 64 -> f64
+      | Ty_roundingMode -> M.Types.roundingMode
       | (Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp) as ty ->
         Fmt.failwith "Unsupported theory: %a@." Ty.pp ty
 
@@ -598,7 +599,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.unop
       | Ty.Ty_fp 32 -> Float32_impl.unop
       | Ty.Ty_fp 64 -> Float64_impl.unop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none ->
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none
+      | Ty_roundingMode ->
         assert false
 
     let binop = function
@@ -612,7 +614,8 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_bitv 64 -> I64.binop
       | Ty.Ty_fp 32 -> Float32_impl.binop
       | Ty.Ty_fp 64 -> Float64_impl.binop
-      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none ->
+      | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none
+      | Ty_roundingMode ->
         assert false
 
     let triop = function
@@ -625,7 +628,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_fp 32 -> Float32_impl.triop
       | Ty.Ty_fp 64 -> Float64_impl.triop
       | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none
-      | Ty_regexp ->
+      | Ty_regexp | Ty_roundingMode ->
         assert false
 
     let relop = function
@@ -639,7 +642,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_fp 32 -> Float32_impl.relop
       | Ty.Ty_fp 64 -> Float64_impl.relop
       | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none
-      | Ty_regexp ->
+      | Ty_regexp | Ty_roundingMode ->
         assert false
 
     let cvtop = function
@@ -653,7 +656,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_fp 32 -> Float32_impl.cvtop
       | Ty.Ty_fp 64 -> Float64_impl.cvtop
       | Ty.Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none
-      | Ty_regexp ->
+      | Ty_regexp | Ty_roundingMode ->
         assert false
 
     let naryop = function
@@ -662,18 +665,19 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | Ty.Ty_regexp -> Regexp_impl.naryop
       | ty -> Fmt.failwith "Naryop for type \"%a\" not implemented" Ty.pp ty
 
-    let get_rounding_mode rm =
+    let get_rounding_mode ctx rm =
       match Expr.view rm with
       | Symbol { name = Simple ("roundNearestTiesToEven" | "RNE"); _ } ->
-        M.Float.Rounding_mode.rne
+        (ctx, M.Float.Rounding_mode.rne)
       | Symbol { name = Simple ("roundNearestTiesToAway" | "RNA"); _ } ->
-        M.Float.Rounding_mode.rna
+        (ctx, M.Float.Rounding_mode.rna)
       | Symbol { name = Simple ("roundTowardPositive" | "RTP"); _ } ->
-        M.Float.Rounding_mode.rtp
+        (ctx, M.Float.Rounding_mode.rtp)
       | Symbol { name = Simple ("roundTowardNegative" | "RTN"); _ } ->
-        M.Float.Rounding_mode.rtn
+        (ctx, M.Float.Rounding_mode.rtn)
       | Symbol { name = Simple ("roundTowardZero" | "RTZ"); _ } ->
-        M.Float.Rounding_mode.rtz
+        (ctx, M.Float.Rounding_mode.rtz)
+      | Symbol rm -> make_symbol ctx rm
       | _ -> Fmt.failwith "unknown rouding mode: %a" Expr.pp rm
 
     let rec encode_expr ctx (hte : Expr.t) : symbol_ctx * M.term =
@@ -688,36 +692,36 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
       | App ({ name = Simple "fp.add"; _ }, [ rm; a; b ]) ->
         let ctx, a = encode_expr ctx a in
         let ctx, b = encode_expr ctx b in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.add ~rm a b)
       | App ({ name = Simple "fp.sub"; _ }, [ rm; a; b ]) ->
         let ctx, a = encode_expr ctx a in
         let ctx, b = encode_expr ctx b in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.sub ~rm a b)
       | App ({ name = Simple "fp.mul"; _ }, [ rm; a; b ]) ->
         let ctx, a = encode_expr ctx a in
         let ctx, b = encode_expr ctx b in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.mul ~rm a b)
       | App ({ name = Simple "fp.div"; _ }, [ rm; a; b ]) ->
         let ctx, a = encode_expr ctx a in
         let ctx, b = encode_expr ctx b in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.div ~rm a b)
       | App ({ name = Simple "fp.fma"; _ }, [ rm; a; b; c ]) ->
         let ctx, a = encode_expr ctx a in
         let ctx, b = encode_expr ctx b in
         let ctx, c = encode_expr ctx c in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.fma ~rm a b c)
       | App ({ name = Simple "fp.sqrt"; _ }, [ rm; a ]) ->
         let ctx, a = encode_expr ctx a in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.sqrt ~rm a)
       | App ({ name = Simple "fp.roundToIntegral"; _ }, [ rm; a ]) ->
         let ctx, a = encode_expr ctx a in
-        let rm = get_rounding_mode rm in
+        let ctx, rm = get_rounding_mode ctx rm in
         (ctx, M.Float.round_to_integral ~rm a)
       | App (sym, args) ->
         let name =
@@ -822,7 +826,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let float = M.Interp.to_float v 11 53 in
         Value.Num (F64 (Int64.bits_of_float float))
       | Ty_bitv _ | Ty_fp _ | Ty_list | Ty_app | Ty_unit | Ty_none | Ty_regexp
-        ->
+      | Ty_roundingMode ->
         assert false
 
     let value ({ model = m; ctx } : model) (c : Expr.t) : Value.t =

src/smtml/mappings.nop.ml

@@ -10,9 +10,9 @@ module Nop = struct
       let is_available = false
     end
 
-    type ty = unit
+    type ty = [ `Ty ]
 
-    type term = unit
+    type term = [ `Term ]
 
     type interp
 
@@ -24,11 +24,11 @@ module Nop = struct
 
     type optimizer
 
-    type func_decl = unit
+    type func_decl = [ `Func_decl ]
 
-    let true_ = ()
+    let true_ = `Term
 
-    let false_ = ()
+    let false_ = `Term
 
     let int _ = assert false
 
@@ -61,17 +61,19 @@ module Nop = struct
     let exists _ _ = assert false
 
     module Types = struct
-      let int = ()
+      let int = `Ty
 
-      let real = ()
+      let real = `Ty
 
-      let bool = ()
+      let bool = `Ty
 
-      let string = ()
+      let string = `Ty
 
-      let bitv _ = ()
+      let bitv _ = `Ty
 
-      let float _ _ = ()
+      let float _ _ = `Ty
+
+      let roundingMode = `Ty
 
       let ty _ = assert false
 
@@ -262,15 +264,15 @@ module Nop = struct
 
     module Float = struct
       module Rounding_mode = struct
-        let rne = ()
+        let rne = `Term
 
-        let rna = ()
+        let rna = `Term
 
-        let rtp = ()
+        let rtp = `Term
 
-        let rtn = ()
+        let rtn = `Term
 
-        let rtz = ()
+        let rtz = `Term
       end
 
       let v _ = assert false
@@ -339,9 +341,9 @@ module Nop = struct
     end
 
     module Func = struct
-      let make _ _ _ = ()
+      let make _ _ _ = `Func_decl
 
-      let apply () _ = ()
+      let apply `Func_decl _ = `Term
     end
 
     module Model = struct

src/smtml/mappings_intf.ml

@@ -120,6 +120,8 @@ module type M = sig
         significand width [s]. *)
     val float : int -> int -> ty
 
+    val roundingMode : ty
+
     (** [ty t] retrieves the type of the term [t]. *)
     val ty : term -> ty
 

src/smtml/rewrite.ml

@@ -21,15 +21,18 @@ let debug fmt k = if debug then k (Fmt.epr fmt)
 
 (* FIXME: This is a very basic way to infer types. I'm surprised it even works *)
 let rewrite_ty unknown_ty tys =
-  debug "  rewrite_ty: %a@." (fun k -> k Ty.pp unknown_ty);
   match (unknown_ty, tys) with
-  | Ty_none, [ ty ] -> ty
+  | Ty.Ty_none, [ ty ] ->
+    debug "  rewrite_ty: %a -> %a@." (fun k -> k Ty.pp unknown_ty Ty.pp ty);
+    ty
   | Ty_none, [ ty1; ty2 ] ->
-    debug "  rewrite_ty: %a %a@." (fun k -> k Ty.pp ty1 Ty.pp ty2);
+    debug "  rewrite_ty: %a -> (%a %a)@." (fun k ->
+      k Ty.pp unknown_ty Ty.pp ty1 Ty.pp ty2 );
     assert (Ty.equal ty1 ty2);
     ty1
   | Ty_none, ty1 :: ty2 :: [ ty3 ] ->
-    debug "  rewrite_ty: %a %a %a@." (fun k -> k Ty.pp ty1 Ty.pp ty2 Ty.pp ty3);
+    debug "  rewrite_ty: %a ->(%a %a %a)@." (fun k ->
+      k Ty.pp unknown_ty Ty.pp ty1 Ty.pp ty2 Ty.pp ty3 );
     assert (Ty.equal ty1 ty2);
     assert (Ty.equal ty2 ty3);
     ty1
@@ -55,11 +58,13 @@ let rec rewrite_expr (type_map, expr_map) hte =
   | App
       ( ({ name = Simple ("fp.add" | "fp.sub" | "fp.mul" | "fp.div"); _ } as sym)
       , [ rm; a; b ] ) ->
+    let rm = rewrite_expr (type_map, expr_map) rm in
     let a = rewrite_expr (type_map, expr_map) a in
     let b = rewrite_expr (type_map, expr_map) b in
     let ty = rewrite_ty Ty_none [ Expr.ty a; Expr.ty b ] in
     Expr.app { sym with ty } [ rm; a; b ]
   | App (({ name = Simple "fp.fma"; _ } as sym), [ rm; a; b; c ]) ->
+    let rm = rewrite_expr (type_map, expr_map) rm in
     let a = rewrite_expr (type_map, expr_map) a in
     let b = rewrite_expr (type_map, expr_map) b in
     let c = rewrite_expr (type_map, expr_map) c in
@@ -68,6 +73,7 @@ let rec rewrite_expr (type_map, expr_map) hte =
   | App
       ( ({ name = Simple ("fp.sqrt" | "fp.roundToIntegral"); _ } as sym)
       , [ rm; a ] ) ->
+    let rm = rewrite_expr (type_map, expr_map) rm in
     let a = rewrite_expr (type_map, expr_map) a in
     let ty = rewrite_ty Ty_none [ Expr.ty a ] in
     Expr.app { sym with ty } [ rm; a ]

src/smtml/smtlib.ml

@@ -30,19 +30,24 @@ module Term = struct
 
   let const ?loc (id : Symbol.t) : t =
     match (Symbol.namespace id, Symbol.name id) with
-    | Sort, Simple name -> (
+    | Sort, Simple name -> begin
       match name with
       | "Int" -> Expr.symbol { id with ty = Ty_int }
       | "Real" -> Expr.symbol { id with ty = Ty_real }
       | "Bool" -> Expr.symbol { id with ty = Ty_bool }
       | "String" -> Expr.symbol { id with ty = Ty_str }
       | "Float32" -> Expr.symbol { id with ty = Ty_fp 32 }
       | "Float64" -> Expr.symbol { id with ty = Ty_fp 64 }
-      | _ -> (
+      | "RoundingMode" -> Expr.symbol { id with ty = Ty_roundingMode }
+      | _ -> begin
         match Hashtbl.find_opt custom_sorts name with
+        | Some ty -> Expr.symbol { id with ty }
         | None ->
-          Fmt.failwith "%acould not find sort: %a" pp_loc loc Symbol.pp id
-        | Some ty -> Expr.symbol { id with ty } ) )
+          Logs.err (fun k ->
+            k "%acould not find sort: %a" pp_loc loc Symbol.pp id );
+          Expr.symbol id
+      end
+    end
     | Sort, Indexed { basename; indices } -> (
       match (basename, indices) with
       | "BitVec", [ n ] -> (
@@ -78,7 +83,7 @@ module Term = struct
         fp_of_size (Float.neg Float.zero) ebits sbits
       | "NaN", [ ebits; sbits ] -> fp_of_size Float.nan ebits sbits
       | _ ->
-        Log.debug (fun k -> k "const: Unknown %a making app" Symbol.pp id);
+        Log.debug (fun k -> k "const: unknown %a making app" Symbol.pp id);
         Expr.symbol id
     end
     | Attr, Simple _ -> Expr.symbol id
@@ -90,12 +95,12 @@ module Term = struct
   let int ?loc (x : string) =
     match int_of_string_opt x with
     | Some x -> Expr.value (Int x)
-    | None -> Fmt.failwith "%aInvalid int" pp_loc loc
+    | 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
+    | None -> Fmt.failwith "%ainvalid real" pp_loc loc
 
   let hexa ?loc:_ (h : string) =
     let len = String.length h in