From fe0928c7dce06cd9244d422d5ff121995362fd0d Mon Sep 17 00:00:00 2001
From: OriginLabs-Iguernlala <mohamed.iguernlala@origin-labs.com>
Date: Wed, 22 Jul 2020 12:25:28 +0200
Subject: [PATCH] fix simplification of distincts

---
 src/lib/structures/expr.ml  | 37 +++++++++++++++++--------------------
 src/lib/structures/typed.ml |  2 ++
 2 files changed, 19 insertions(+), 20 deletions(-)

diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index b3f2425108..3a27f6c9fc 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -990,33 +990,30 @@ let mk_eq ~iff t1 t2 =
     else
       mk_positive_lit (Sy.Lit Sy.L_eq) (Sy.Lit Sy.L_neg_eq) [t1; t2]
 
-let mk_nary_eq ~iff l =
-  let l = List.fast_sort (fun a b -> compare b a) l in (* decreasing *)
-  match l with
-  | [] | [_] | [_;_] -> assert false
-  | _ ->
-    let _, l =
-      List.fold_left
-        (fun ((last, acc) as accu) e ->
-           match last with
-           | Some d -> if equal d e then accu else Some e, e :: acc
-           | None -> Some e, e :: acc
-        )(None, []) l
-    in
+let mk_nary_eq l =
+  try
+    let l = List.fast_sort (fun a b -> compare b a) l in (* decreasing *)
     match l with
-    | [] -> assert false (* not possible *)
-    | [_] -> vrai (* all the elements are physically equal *)
-    | [a; b] -> mk_eq ~iff a b
-    | (e :: r) as l ->
+    | [] | [_] | [_;_] -> assert false
+    | e::r ->
+      let _ =
+        List.fold_left
+          (fun last e ->
+             if equal last e then raise Exit;
+             e
+          ) e r
+      in
       if type_info e == Ty.Tbool then
         List.fold_left (fun x y -> mk_iff x y 0) e  r
       else
         mk_positive_lit (Sy.Lit Sy.L_eq) (Sy.Lit Sy.L_neg_eq) l
+  with Exit ->
+    vrai
 
 let mk_distinct ~iff tl =
   match tl with
   | [a; b] -> neg (mk_eq ~iff a b)
-  | _ -> neg (mk_nary_eq ~iff tl)
+  | _ -> neg (mk_nary_eq tl)
 
 let mk_builtin ~is_pos n l =
   let pos =
@@ -1134,7 +1131,7 @@ let rec apply_subst_aux (s_t, s_ty) t =
         begin match xs' with
           | [] | [_] -> assert false
           | [a; b] ->  mk_eq ~iff:true a b
-          | _ -> mk_nary_eq ~iff:true xs'
+          | _ -> mk_nary_eq xs'
         end
 
       | Sy.Lit Sy.L_neg_eq, _ ->
@@ -2329,7 +2326,7 @@ module Purification = struct
         match l with
         | [] | [_] -> assert false
         | [a; b ] -> mk_eq ~iff:true a b
-        | l -> mk_nary_eq ~iff:true l
+        | l -> mk_nary_eq l
       ) l
 
   and purify_distinct l =
diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml
index 627640be9f..0708369d54 100644
--- a/src/lib/structures/typed.ml
+++ b/src/lib/structures/typed.ml
@@ -312,6 +312,8 @@ and print_atom fmt a =
     else print_term fmt t
   | TTisConstr (t1, s) ->
     fprintf fmt "%a ? %s" print_term t1 (Hstring.view s)
+  | TAdistinct l ->
+    fprintf fmt "distinct(%a)" print_term_list l
   | _ -> assert false
 
 and print_triggers fmt l =