From 6a1b95c90b5014dca1ba3a07437812074d5d75e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Fri, 6 Sep 2024 16:46:57 +0200 Subject: [PATCH] feat: Support more Alt-Ergo primitives This patch adds typing support for the following Alt-Ergo primitives: - `fpa_rounding_mode` and its constructors (equivalent to `RoundingMode` in SMT-LIB); - `real_of_int` (equivalent to `to_real` in SMT-LIB); - `real_is_int` (equivalent to `is_int` in SMT-LIB); - `abs_int` (equivalent to `abs` in SMT-LIB); - `int_floor` (equialent to `floor_to_int` in SMT-LIB) --- src/interface/term.ml | 49 +++++++++++++++++++ src/interface/ty.ml | 14 ++++-- src/loop/typer.ml | 4 ++ src/typecheck/arith.ml | 18 +++++-- src/typecheck/float.ml | 40 +++++++++++++++ src/typecheck/float.mli | 13 +++++ .../triggers/fpa-theory-2019-10-08-19h00.ae | 26 ---------- 7 files changed, 132 insertions(+), 32 deletions(-) diff --git a/src/interface/term.ml b/src/interface/term.ml index 943d65bd0..fa467c436 100644 --- a/src/interface/term.ml +++ b/src/interface/term.ml @@ -761,6 +761,9 @@ module type Ae_Arith = sig val to_real : t -> t (** Conversion from an integer term to a real term. *) + val abs : t -> t + (** Arithmetic absolute value. *) + end module Real : sig @@ -769,6 +772,12 @@ module type Ae_Arith = sig val div : t -> t -> t (** Exact division on reals. *) + val is_int : t -> t + (** Integer testing *) + + val floor_to_int : t -> t + (** Greatest integer smaller than the given real *) + end end @@ -931,6 +940,46 @@ module type Ae_Bitv = sig end +module type Ae_Float_Float = sig + + type t + (** the type of terms *) + + val roundNearestTiesToEven: t + (** constant for rounding mode RNE *) + + val roundNearestTiesToAway: t + (** constant for rounding mode RNA *) + + val roundTowardPositive: t + (** constant for rounding mode RTP *) + + val roundTowardNegative: t + (** constant for rounding mode RTN *) + + val roundTowardZero: t + (** constant for rounding mode RTZ *) + +end + +(* Minimum required to type Ae floats *) +module type Ae_Float = sig + + type t + (** The type of terms *) + + type ty + (** The type of types. *) + + val ty : t -> ty + (** Type of a term. *) + + module Float : Ae_Float_Float with type t := t + (** Sub-module used for namespacing the floating number part + of the theory requirements *) + +end + (** Minimum required to type tptp's tff *) module type Tptp_Tff_Core = sig diff --git a/src/interface/ty.ml b/src/interface/ty.ml index 239abde50..84b83888d 100644 --- a/src/interface/ty.ml +++ b/src/interface/ty.ml @@ -232,6 +232,17 @@ module type Ae_Bitv = sig end +(** Signature required by types for typing ae's floats *) +module type Ae_Float = sig + + type t + (** The type of types *) + + val roundingMode: t + (** Type of the rounding modes *) + +end + (** Signature required by types for typing tptp *) module type Tptp_Base = sig @@ -432,6 +443,3 @@ module type Zf_Arith = sig (** The type of integers *) end - - - diff --git a/src/loop/typer.ml b/src/loop/typer.ml index e14e44e44..9389b64ca 100644 --- a/src/loop/typer.ml +++ b/src/loop/typer.ml @@ -20,6 +20,9 @@ module Ae_Arrays = module Ae_Bitv = Dolmen_type.Bitv.Ae.Tff(T) (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term.Bitv) +module Ae_Float = + Dolmen_type.Float.Ae.Tff(T) + (Dolmen.Std.Expr.Ty)(Dolmen.Std.Expr.Term) (* Dimacs builtin *) module Dimacs = @@ -1552,6 +1555,7 @@ module Typer(State : State.S) = struct Ae_Arith.parse; Ae_Arrays.parse; Ae_Bitv.parse; + Ae_Float.parse; ]) in T.empty_env ~order:First_order ~st:(State.get ty_state st).typer diff --git a/src/typecheck/arith.ml b/src/typecheck/arith.ml index b3c50ce51..f47e95f94 100644 --- a/src/typecheck/arith.ml +++ b/src/typecheck/arith.ml @@ -91,6 +91,19 @@ module Ae = struct | Type.Id { Id.ns = Value Hexadecimal; name = Simple name; } -> Type.builtin_term (Base.app0 (module Type) env s (T.real name)) + | Type.Id { Id.ns = Term; name = Simple name; } -> + begin match name with + | "real_of_int" -> + Type.builtin_term (Base.term_app1 (module Type) env s T.Int.to_real) + | "int_floor" -> + Type.builtin_term (Base.term_app1 (module Type) env s T.Real.floor_to_int) + | "real_is_int" -> + Type.builtin_term (Base.term_app1 (module Type) env s T.Real.is_int) + | "abs_int" -> + Type.builtin_term (Base.term_app1 (module Type) env s T.Int.abs) + | _ -> `Not_found + end + (* Arithmetic *) | Type.Builtin Term.Minus -> Type.builtin_term (Base.term_app1_ast (module Type) env s @@ -186,8 +199,8 @@ module Ae = struct (parse_in_interval env ~strict_lower ~strict_upper) ) - (* Catch-all *) - | _ -> `Not_found + (* Catch-all *) + | _ -> `Not_found end end @@ -1288,4 +1301,3 @@ module Zf = struct end end - diff --git a/src/typecheck/float.ml b/src/typecheck/float.ml index 41f86590b..c5bf2d005 100644 --- a/src/typecheck/float.ml +++ b/src/typecheck/float.ml @@ -2,6 +2,46 @@ module Id = Dolmen.Std.Id module Ast = Dolmen.Std.Term +(* Ae floating point *) +(* ************************************************************************ *) + +module Ae = struct + + module Tff + (Type : Tff_intf.S) + (Ty : Dolmen.Intf.Ty.Ae_Float with type t := Type.Ty.t) + (T : Dolmen.Intf.Term.Ae_Float with type t := Type.T.t + and type ty := Type.Ty.t) = struct + + module F = T.Float + + let parse env s = + match s with + + (* sorts *) + | Type.Id { ns = Sort; name = Simple "fpa_rounding_mode"; } -> + Type.builtin_ty (Base.app0 (module Type) env s Ty.roundingMode) + + (* terms *) + | Type.Id { ns = Term; name = Simple name; } -> + begin match name with + | "NearestTiesToEven" -> + Type.builtin_term (Base.app0 (module Type) env s F.roundNearestTiesToEven) + | "NearestTiesToAway" -> + Type.builtin_term (Base.app0 (module Type) env s F.roundNearestTiesToAway) + | "Up" -> + Type.builtin_term (Base.app0 (module Type) env s F.roundTowardPositive) + | "Down" -> + Type.builtin_term (Base.app0 (module Type) env s F.roundTowardNegative) + | "ToZero" -> + Type.builtin_term (Base.app0 (module Type) env s F.roundTowardZero) + | _ -> `Not_found + end + + | _ -> `Not_found + end +end + (* Smtlib Floating Point *) (* ************************************************************************ *) diff --git a/src/typecheck/float.mli b/src/typecheck/float.mli index 341f3a167..7120a197b 100644 --- a/src/typecheck/float.mli +++ b/src/typecheck/float.mli @@ -1,3 +1,16 @@ +(** Ae floating point builtins *) +module Ae : sig + + module Tff + (Type : Tff_intf.S) + (Ty : Dolmen.Intf.Ty.Ae_Float with type t := Type.Ty.t) + (T : Dolmen.Intf.Term.Ae_Float with type t := Type.T.t + and type ty := Type.Ty.t) : sig + + val parse : Type.builtin_symbols + end + +end (** Smtlib floating point builtins *) module Smtlib2 : sig diff --git a/tests/typing/pass/ae/triggers/fpa-theory-2019-10-08-19h00.ae b/tests/typing/pass/ae/triggers/fpa-theory-2019-10-08-19h00.ae index 2e1da08b6..4fbe4321e 100644 --- a/tests/typing/pass/ae/triggers/fpa-theory-2019-10-08-19h00.ae +++ b/tests/typing/pass/ae/triggers/fpa-theory-2019-10-08-19h00.ae @@ -9,23 +9,6 @@ (* *) (******************************************************************************) -type fpa_rounding_mode = - (* five standard/why3 fpa rounding modes *) - NearestTiesToEven (*ne in Gappa: to nearest, tie breaking to even mantissas*) - | ToZero (* zr in Gappa: toward zero *) - | Up (* up in Gappa: toward plus infinity *) - | Down (* dn in Gappa: toward minus infinity *) - | NearestTiesToAway (* na : to nearest, tie breaking away from zero *) - - (* additional Gappa rounding modes *) - | Aw (* aw in Gappa: away from zero **) - | Od (* od in Gappa: to odd mantissas *) - | No (* no in Gappa: to nearest, tie breaking to odd mantissas *) - | Nz (* nz in Gappa: to nearest, tie breaking toward zero *) - | Nd (* nd in Gappa: to nearest, tie breaking toward minus infinity *) - | Nu (* nu in Gappa: to nearest, tie breaking toward plus infinity *) - - (* the first argument is mantissas' size (including the implicit bit), the second one is the exp of the min representable normalized number, the third one is the rounding mode, and the last one is the real to @@ -51,9 +34,6 @@ logic float64d: real -> real (* rounds to nearest integer depending on rounding mode *) logic integer_round: fpa_rounding_mode, real -> int -(* type cast: from int to real *) -logic real_of_int : int -> real - (* abs value of a real *) logic abs_real : real -> real @@ -66,12 +46,6 @@ logic sqrt_real_default : real -> real (* sqrt value of a real by excess *) logic sqrt_real_excess : real -> real -(* abs value of an int *) -logic abs_int : int -> int - -(* (integer) floor of a rational *) -logic int_floor : real -> int - (* (integer) ceiling of a rational *) logic int_ceil : real -> int