From b9640022b7d848242c3905a622caa021bec3ff93 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Mon, 16 Oct 2023 18:38:04 +0200 Subject: [PATCH] Also translating on the native side --- src/lib/frontend/typechecker.ml | 55 ++++-- src/lib/structures/fpa_rounding.ml | 10 ++ src/lib/structures/fpa_rounding.mli | 11 +- tests/dune.inc | 270 ++++++++++++++++++++++++++++ 4 files changed, 329 insertions(+), 17 deletions(-) diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index ebb4b281a8..daf5e4314e 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -259,18 +259,29 @@ module Env = struct | [ x; y ] -> f x y | _ -> assert false - let add_builtin_enum = function - | Ty.Tsum (_, cstrs) as ty -> - let enum m h = - let s = Hstring.view h in - MString.add s (`Term ( - Symbols.Op (Constr h), - { args = []; result = ty }, - Other - )) m - in - fun m -> List.fold_left enum m cstrs - | _ -> assert false + let add_fpa_enum map = + let ty = Fpa_rounding.fpa_rounding_mode in + match ty with + | Ty.Tsum (_, cstrs) -> + List.fold_left + (fun m c -> + match Fpa_rounding.translate_smt_rounding_mode c with + | None -> + (* The constructors of the type are expected to be AE rounding + modes. *) + assert false + | Some hs -> + MString.add (Hstring.view hs) (`Term ( + Symbols.Op (Constr c), + { args = []; result = ty }, + Other + )) + m + ) + map + cstrs + | _ -> (* Fpa_rounding.fpa_rounding_mode is a sum type. *) + assert false let find_builtin_cstr ty n = match ty with @@ -315,10 +326,7 @@ module Env = struct let env = { env with types = Types.add_builtin env.types tname rm ; - builtins = - add_builtin_enum - Fpa_rounding.fpa_rounding_mode - env.builtins; + builtins = add_fpa_enum env.builtins; } in let builtins = env.builtins @@ -602,6 +610,21 @@ let check_pattern_matching missing dead loc = let mk_adequate_app p s te_args ty logic_kind = let hp = Hstring.make p in match logic_kind, te_args, ty with + (* | _, _, _ when Ty.equal ty Fpa_rounding.fpa_rounding_mode -> + * begin + * match s with + * | Symbols.Op (Symbols.Constr cstr ) -> + * begin + * match Fpa_rounding.translate_ae_rounding cstr with + * | None -> TTapp (s, te_args) + * | Some new_c -> + * let new_s = Symbols.Op (Symbols.Constr new_c) in + * TTapp (new_s, te_args) + * end + * | _ -> + * (\* Values of type fpa_rounding_mode should only by constructors *\) + * assert false + * end *) | (Env.AdtConstr | Env.EnumConstr | Env.Other), _, _ -> (* symbol 's' alreadt contains the information *) TTapp(s, te_args) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index e2f0072323..08880f57ff 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -121,6 +121,16 @@ let rounding_mode_of_ae_hs = rounding_mode_of_smt_hs key | Some res -> res +let translate_ae_rounding_mode hs = + match rounding_mode_of_ae_hs hs with + | res -> Some (Hstring.make (to_smt_string res)) + | exception (Failure _) -> None + +let translate_smt_rounding_mode hs = + match rounding_mode_of_smt_hs hs with + | res -> Some (Hstring.make (to_ae_string res)) + | exception (Failure _) -> None + (** Helper functions **) let mult_x_by_2_pow_n x n = diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index e24ae49228..115daf6583 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -51,12 +51,21 @@ val fpa_rounding_mode_ae_type_name : string val fpa_rounding_mode : Ty.t (** Transforms the Hstring corresponding to a RoundingMode element into - the [rounding_mode] equivalent. *) + the [rounding_mode] equivalent. Raises 'Failure' if the string does not + correspond to a valid rounding mode. *) val rounding_mode_of_smt_hs : Hstring.t -> rounding_mode (** Same, but for legacy's [rounding_mode] equivalent. *) val rounding_mode_of_ae_hs : Hstring.t -> rounding_mode +(** Returns the SMT rounding mode representation of the legacy rounding mode + in argument. Returns [None] if the string does not correspond to a valid + AE rounding mode. *) +val translate_ae_rounding_mode : Hstring.t -> Hstring.t option + +(** Same, but from AE modes to SMT2 modes. *) +val translate_smt_rounding_mode : Hstring.t -> Hstring.t option + (** Returns the string representation of the [rounding_mode] (SMT2 standard) *) val string_of_rounding_mode : rounding_mode -> string diff --git a/tests/dune.inc b/tests/dune.inc index a39d0925d5..e73f9d1d44 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -175626,6 +175626,276 @@ ; Auto-generated part begin (subdir float + (rule + (target test_float3_ci_cdcl_no_minimal_bj.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + --no-minimal-bj + %{input}))))))) + (rule + (deps test_float3_ci_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_cdcl_no_minimal_bj.output))) + (rule + (target test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_minimal_bj_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories_and_instantiation.output))) + (rule + (target test_float3_ci_no_tableaux_cdcl_in_instantiation.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-instantiation + %{input}))))))) + (rule + (deps test_float3_ci_no_tableaux_cdcl_in_instantiation.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_no_tableaux_cdcl_in_instantiation.output))) + (rule + (target test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-tableaux-cdcl-in-theories + %{input}))))))) + (rule + (deps test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_cdcl_tableaux_no_tableaux_cdcl_in_theories.output))) + (rule + (target test_float3_ci_tableaux_cdcl_no_minimal_bj.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL-Tableaux + --no-minimal-bj + %{input}))))))) + (rule + (deps test_float3_ci_tableaux_cdcl_no_minimal_bj.output) + (alias runtest-ci) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_ci_tableaux_cdcl_no_minimal_bj.output))) + (rule + (target test_float3_cdcl.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver CDCL + %{input}))))))) + (rule + (deps test_float3_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_cdcl.output))) + (rule + (target test_float3_tableaux_cdcl.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux-CDCL + %{input}))))))) + (rule + (deps test_float3_tableaux_cdcl.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_tableaux_cdcl.output))) + (rule + (target test_float3_tableaux.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + --sat-solver Tableaux + %{input}))))))) + (rule + (deps test_float3_tableaux.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_tableaux.output))) + (rule + (target test_float3_legacy.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend legacy + %{input}))))))) + (rule + (deps test_float3_legacy.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_legacy.output))) + (rule + (target test_float3_dolmen.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps test_float3_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_dolmen.output))) + (rule + (target test_float3_fpa.output) + (deps (:input test_float3.ae)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes 0 + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --enable-theories fpa + %{input}))))))) + (rule + (deps test_float3_fpa.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff test_float3.expected test_float3_fpa.output))) (rule (target test_float2.models_tableaux.output) (deps (:input test_float2.models.smt2))