From 634f3c9a1e835aa44ee84a49ef708780af5a447a Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 16 Oct 2023 10:17:48 +0200 Subject: [PATCH] Clean up --- src/lib/frontend/cnf.ml | 5 +---- src/lib/frontend/d_cnf.ml | 2 +- src/lib/structures/expr.ml | 5 +++-- 3 files changed, 5 insertions(+), 7 deletions(-) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index b650ccf56d..a8088c5a8f 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -239,13 +239,10 @@ and make_form up_qv name_base ~toplevel f loc ~decl_kind : E.t = let res = make_term up_qv name_base t in if negated then E.neg res else res - | TAneq lt -> + | TAneq lt | TAdistinct lt -> let lt = List.map (make_term up_qv name_base) lt in E.mk_distinct ~iff:true lt - | TAdistinct lt -> - E.mk_distinct ~iff:true (List.map (make_term up_qv name_base) lt) - | TAle [t1;t2] -> E.mk_builtin ~is_pos:true Sy.LE [make_term up_qv name_base t1; diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 328c94a6e3..c63843a789 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1337,7 +1337,7 @@ let rec mk_expr end | B.Distinct, _ -> - E.mk_distinct ~iff:true (List.map aux_mk_expr args) + E.mk_distinct ~iff:true (List.map (fun t -> aux_mk_expr t) args) | B.Constructor _, _ -> let name = get_basename path in diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 5dc0d89bb0..caac9828fa 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1211,10 +1211,11 @@ let mk_nary_eq l = vrai let mk_distinct ~iff args = - (* This fix makes sure that the smart constructor agrees with + (* This hot fix makes sure that the smart constructor agrees with the SMT-LIB specification when used with at least 3 arguments. To prevent a soundness bug, we translate the expected expression into a - conjonction of binary disequations. *) + conjonction of binary disequations. + See issue: https://github.com/OCamlPro/alt-ergo/issues/889 *) let args = Array.of_list args in let acc = ref vrai in for i = 0 to Array.length args - 1 do