From 3a1945838c63cf335e786583f7bac8e2a022a82b Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 26 May 2023 17:04:03 +0200 Subject: [PATCH 1/2] Add the forgotten case --- src/lib/util/options.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index c1169665c..e921d5878 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -316,8 +316,11 @@ let set_unsat_core b = unsat_core := b let equal_mode a b = match a, b with - | INone, INone | IFirst, IFirst | IEvery, IEvery -> true - | _ -> false + | INone, INone | IFirst, IFirst | IEvery, IEvery | ILast, ILast -> true + | INone, (IFirst | IEvery | ILast) + | IFirst, (INone | IEvery | ILast) + | IEvery, (INone | IFirst | ILast) + | ILast, (INone | IFirst | IEvery) -> false let equal_output_format a b = match a, b with From 4c0875ed8dc5514fdbf3405c01d79ca8101467c5 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 26 May 2023 17:20:49 +0200 Subject: [PATCH 2/2] Improve the readability of comparison functions --- src/lib/util/options.ml | 28 ++++++++++++++++------------ 1 file changed, 16 insertions(+), 12 deletions(-) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index e921d5878..010b2afe8 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -316,25 +316,29 @@ let set_unsat_core b = unsat_core := b let equal_mode a b = match a, b with - | INone, INone | IFirst, IFirst | IEvery, IEvery | ILast, ILast -> true - | INone, (IFirst | IEvery | ILast) - | IFirst, (INone | IEvery | ILast) - | IEvery, (INone | IFirst | ILast) - | ILast, (INone | IFirst | IEvery) -> false + | INone, INone -> true + | INone, _ | _, INone -> false + | IFirst, IFirst -> true + | IFirst, _ | _, IFirst -> false + | IEvery, IEvery -> true + | IEvery, _ | _, IEvery -> false + | ILast, ILast -> true let equal_output_format a b = match a, b with - | Smtlib2, Smtlib2 | Native, Native | Why3, Why3 -> true + | Smtlib2, Smtlib2 -> true + | Smtlib2, _ | _, Smtlib2 -> false | Unknown n1, Unknown n2 -> String.equal n1 n2 - | Smtlib2, (Native | Why3 | Unknown _) - | Native, (Smtlib2 | Why3 | Unknown _) - | Why3, (Smtlib2 | Native | Unknown _) - | Unknown _, (Smtlib2 | Native | Why3) -> false + | Unknown _, _ | _, Unknown _ -> false + | Native, Native -> true + | Native, _ | _, Native -> false + | Why3, Why3 -> true let equal_mode_type a b = match a, b with - | Constraints, Constraints | Value, Value -> true - | Constraints, Value | Value, Constraints -> false + | Constraints, Constraints -> true + | Constraints, _ | _, Constraints -> false + | Value, Value -> true let get_interpretation () = not @@ equal_mode !interpretation INone let get_first_interpretation () = equal_mode !interpretation IFirst