feat: first working version of th-distinct as a separate theory

src/cc/Congruence_closure.ml

@@ -823,27 +823,6 @@ module Make(A: ARG) = struct
       end;
     )
 
-  (* FIXME: remove
-  and task_distinct_ cc acts (l:node list) tag expl : unit =
-    let l = List.map (fun n -> n, find_ n) l in
-    let coll =
-      Sequence.diagonal_l l
-      |> Sequence.find_pred (fun ((_,r1),(_,r2)) -> N.equal r1 r2)
-    in
-    begin match coll with
-      | Some ((n1,_r1),(n2,_r2)) ->
-        (* two classes are already equal *)
-        Log.debugf 5
-          (fun k->k "(@[cc.distinct.conflict@ %a = %a@ :expl %a@])" N.pp n1 N.pp
-              n2 Expl.pp expl);
-        let lits = explain_unfold cc expl in
-        raise_conflict cc acts lits
-      | None ->
-        (* put a tag on all equivalence classes, that will make their merge fail *)
-        List.iter (fun (_,n) -> add_tag_n cc n tag expl) l
-    end
-     *)
-
   (* we are merging [r1] with [r2==Bool(sign)], so propagate each term [u1]
      in the equiv class of [r1] that is a known literal back to the SAT solver
      and which is not the one initially merged.
@@ -881,10 +860,9 @@ module Make(A: ARG) = struct
     type 'a key = (term,lit,'a) Key.t
 
     (* raise a conflict *)
-    let raise_conflict cc _n1 _n2 expl =
+    let raise_conflict cc expl =
       Log.debugf 5
-        (fun k->k "(@[cc.theory.raise-conflict@ :n1 %a@ :n2 %a@ :expl %a@])"
-            N.pp _n1 N.pp _n2 Expl.pp expl);
+        (fun k->k "(@[cc.theory.raise-conflict@ :expl %a@])" Expl.pp expl);
       merge_classes cc (true_ cc) (false_ cc) expl
 
     let merge cc n1 n2 expl =
@@ -1014,19 +992,6 @@ module Make(A: ARG) = struct
     let n2 = add_term cc t2 in
     merge_classes cc n1 n2 expl
 
-  (* FIXME: remove
-  (* generative tag used to annotate classes that can't be merged *)
-  let distinct_tag_ = ref 0
-
-  let assert_distinct cc (l:term list) ~neq:_ (lit:lit) : unit =
-    assert (match l with[] | [_] -> false | _ -> true);
-    let tag = CCRef.get_then_incr distinct_tag_ in
-    Log.debugf 5
-      (fun k->k "(@[cc.assert_distinct@ (@[%a@])@ :tag %d@])" (Util.pp_list T.pp) l tag);
-    let l = List.map (add_term cc) l in
-    Vec.push cc.combine @@ CT_distinct (l, tag, Expl.mk_lit lit)
-     *)
-
   let add_th (self:t) (th:theory) : unit =
     let (module Th) = th in
     if IM.mem Th.key_id self.theories then (

src/smt/CC.mli

@@ -6,6 +6,7 @@ include Sidekick_cc.S
    and type fun_ = Cst.t
    and type term_state = Term.state
    and type proof = Solver_types.proof
+   and module Key = Sidekick_cc.Key
 
 module Mini_cc : Sidekick_cc.Mini_cc.S
   with type term = Term.t

src/th-distinct/Sidekick_th_distinct.ml

@@ -18,7 +18,7 @@ module type ARG = sig
     val neg : t -> t
     val sign : t -> bool
     val compare : t -> t -> int
-    val atom : T.t -> t
+    val atom : T.state -> ?sign:bool -> T.t -> t
     val pp : t Fmt.printer
   end
 end
@@ -41,6 +41,7 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
   module IM = CCMap.Make(Lit)
 
   type term = T.t
+  type term_state = T.state
   type lit = A.Lit.t
   type data = term IM.t (* "distinct" lit -> term appearing under it*)
 
@@ -96,7 +97,7 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
 
     let on_new_term _ _ = None
 
-    let m_th =
+    let th =
       CC.Theory.make ~key ~on_merge ~on_new_term ()
   end
 
@@ -131,7 +132,7 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
       let l = Sequence.to_list subs in
       let c =
         Sequence.diagonal_l l
-        |> Sequence.map (fun (t,u) -> Lit.atom @@ T.mk_eq st.tst t u)
+        |> Sequence.map (fun (t,u) -> Lit.atom st.tst @@ T.mk_eq st.tst t u)
         |> Sequence.to_rev_list
       in
       let c = Lit.neg lit :: c in
@@ -155,15 +156,9 @@ module Make(A : ARG with type Lit.t = Sidekick_smt.Lit.t
       ~create ()
 end
 
-module T = struct
+module Arg = struct
   open Sidekick_smt
   open Sidekick_smt.Solver_types
-  module T = Term
-
-  type t = Term.t
-  type terms = t IArray.t
-  let compare = Term.compare
-  let to_seq = IArray.to_seq
 
   let id_distinct = ID.make "distinct"
 
@@ -171,11 +166,18 @@ module T = struct
   let get_ty _ _ = Ty.prop
   let abs ~self _a = self, true
 
-  let as_distinct t : _ option =
-    match T.view t with
-    | T.App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
-      Some (IArray.to_seq args)
-    | _ -> None
+  module T = struct
+    include Term
+    let mk_eq = eq
+
+    let as_distinct t : _ option =
+      match view t with
+      | App_cst ({cst_id;_}, args) when ID.equal cst_id id_distinct ->
+        Some (IArray.to_seq args)
+      | _ -> None
+  end
+
+  module Lit = Sidekick_smt.Lit
 
   let eval args =
     let module Value = Sidekick_smt.Value in
@@ -200,7 +202,7 @@ module T = struct
     | xs -> distinct st (IArray.of_list xs)
 end
 
-let distinct = T.distinct
-let distinct_l = T.distinct_l
+let distinct = Arg.distinct
+let distinct_l = Arg.distinct_l
 
-include Make(T)
+include Make(Arg)

src/th-distinct/Sidekick_th_distinct.mli

@@ -23,7 +23,7 @@ module type ARG = sig
     val neg : t -> t
     val sign : t -> bool
     val compare : t -> t -> int
-    val atom : T.t -> t
+    val atom : T.state -> ?sign:bool -> T.t -> t
     val pp : t Fmt.printer
   end
 end