From 158d49fe86b5e96b04ae387dc013f980295c2a18 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Mon, 28 Mar 2022 18:59:53 +0200 Subject: [PATCH] Removed unnecessary extra runtime function --- compiler/runtime.ml | 2 -- compiler/runtime.mli | 1 - compiler/verification/z3backend.real.ml | 4 ++-- 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/compiler/runtime.ml b/compiler/runtime.ml index 92795786..49a91c94 100644 --- a/compiler/runtime.ml +++ b/compiler/runtime.ml @@ -187,8 +187,6 @@ let duration_to_string (d : duration) : string = let duration_to_years_months_days (d : duration) : int * int * int = CalendarLib.Date.Period.ymd d -let duration_to_nb_days (d : duration) : int = CalendarLib.Date.Period.nb_days d - let handle_default : 'a. (unit -> 'a) array -> (unit -> bool) -> (unit -> 'a) -> 'a = fun exceptions just cons -> diff --git a/compiler/runtime.mli b/compiler/runtime.mli index 12cb7f4c..be16be9c 100644 --- a/compiler/runtime.mli +++ b/compiler/runtime.mli @@ -129,7 +129,6 @@ val date_of_numbers : int -> int -> int -> date val duration_of_numbers : int -> int -> int -> duration val duration_to_years_months_days : duration -> int * int * int -val duration_to_nb_days : duration -> int val duration_to_string : duration -> string (**{1 Defaults} *) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 7d9e4abe..9b92ec4a 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -377,12 +377,12 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = 1, 1900 *) | LDate d -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (date_to_int d) | LDuration d -> - let y, m, _ = Runtime.duration_to_years_months_days d in + let y, m, d = Runtime.duration_to_years_months_days d in if y <> 0 || m <> 0 then failwith "[Z3 encoding]: Duration literals containing years or months not \ supported"; - Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.duration_to_nb_days d) + Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 d (** [find_or_create_funcdecl] attempts to retrieve the Z3 function declaration corresponding to the variable [v]. If no such function declaration exists