refactor: functorize th-cstor

src/th-cstor/Sidekick_th_cstor.ml

@@ -5,36 +5,25 @@ type ('c,'t) cstor_view =
   | T_cstor of 'c * 't list
   | T_other of 't
 
-module type S = sig
-  type lit
-  type term
-
-  (** Micro theory only *)
-  val cc_th : Sidekick_smt.CC.Theory.t
-end
+let name = "th-cstor"
 
 module type ARG = sig
-  module Fun : sig
-    type t
-    val equal : t -> t -> bool
-end
-  module T : sig
-    type t
-    val pp : t Fmt.printer
-    val equal : t -> t -> bool
-    val view_as_cstor : t -> (Fun.t,t) cstor_view
-  end
+  module S : Sidekick_core.SOLVER
+  val view_as_cstor : S.A.Term.t -> (S.A.Fun.t, S.A.Term.t) cstor_view
 end
 
-module Make(Arg : ARG with type T.t = Sidekick_smt.Term.t)
-(*   : S with type lit = Arg.Lit.t and type term = Arg.T.t *)
-= struct
-  module N = Sidekick_smt.Theory.CC_eq_class
-  module Expl = Sidekick_smt.Theory.CC_expl
-  module CC = Sidekick_smt.CC
+module type S = sig
+  module A : ARG
+  val theory : A.S.theory
+end
 
-  open Arg
-  type term = T.t
+module Make(A : ARG) : S with module A = A = struct
+  module A = A
+  module Solver = A.S.Internal
+  module T = A.S.A.Term
+  module N = Solver.N
+  module Fun = A.S.A.Fun
+  module Expl = Solver.Expl
 
   type data = {
     t: T.t;
@@ -42,54 +31,48 @@ module Make(Arg : ARG with type T.t = Sidekick_smt.Term.t)
   }
   (* associate to each class a unique constructor term in the class (if any) *)
 
-  let pp_data out x = T.pp out x.t
+  module Data = struct
+    type t = data
+    let pp out x = T.pp out x.t
+    (* let equal x y = T.equal x.t y.t *)
+    let merge x _ = x
+  end
 
-  let key : (_,_,data) Sidekick_cc.Key.t = Sidekick_cc.Key.create
-      ~pp:pp_data ~name:"cstor"
-      ~eq:(fun x y -> T.equal x.t y.t)
-      ~merge:(fun x _ -> x) ()
+  type t = {
+    k: data Solver.Key.t;
+  }
 
-  type t = unit
-
-  let on_merge (cc:CC.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
+  let on_merge (solver:Solver.t) n1 tc1 n2 tc2 e_n1_n2 : unit =
     Log.debugf 5
       (fun k->k "(@[th-cstor.on_merge@ @[:c1 %a@ (term %a)@]@ @[:c2 %a@ (term %a)@]@])"
           N.pp n1 T.pp tc1.t N.pp n2 T.pp tc2.t); 
     let expl = Expl.mk_list [e_n1_n2; Expl.mk_merge n1 tc1.n; Expl.mk_merge n2 tc2.n] in
-    match T.view_as_cstor tc1.t, T.view_as_cstor tc2.t with
+    match A.view_as_cstor tc1.t, A.view_as_cstor tc2.t with
     | T_cstor (f1, l1), T_cstor (f2, l2) ->
-      if Arg.Fun.equal f1 f2 then (
+      (* merging two constructor terms: injectivity + disjointness checks *)
+      if Fun.equal f1 f2 then (
         (* same function: injectivity *)
         assert (List.length l1 = List.length l2);
         List.iter2
-          (fun u1 u2 -> CC.Theory.merge cc (CC.add_term cc u1) (CC.add_term cc u2) expl)
+          (fun u1 u2 -> Solver.cc_merge_t solver u1 u2 expl)
           l1 l2
       ) else (
         (* different function: disjointness *)
-        CC.Theory.raise_conflict cc expl
+        Solver.raise_conflict solver expl
       )
     | _ -> assert false
 
+  (* attach data to constructor terms *)
   let on_new_term _ n (t:T.t) =
-    match T.view_as_cstor t with
+    match A.view_as_cstor t with
     | T_cstor _ -> Some {t;n}
     | _ -> None
 
-  let cc_th = Sidekick_smt.CC.Theory.make ~key ~on_new_term ~on_merge ()
+  let create_and_setup (solver:Solver.t) : t =
+    let k = Solver.Key.create solver ~on_merge (module Data) in
+    Solver.on_cc_merge solver ~k on_merge;
+    Solver.on_cc_new_term solver ~k on_new_term;
+    {k}
+
+  let theory = A.S.mk_theory ~name ~create_and_setup ()
 end
-
-
-(* TODO: default building of constructor terms
-include Make(struct
-    module Fun = Sidekick_smt.Cst
-    module T = struct
-      include Sidekick_smt.Term
-      let[@inline] view_as_cstor t = match view t with
-        | App_cst (c, args) when Fun.do_cc
-        | If (a,b,c) -> T_ite (a,b,c)
-        | Bool b -> T_bool b
-        | _ -> T_other t
-      end
-    end)
-   *)
-