feat(data): store is-a/select parents in a monoid

src/cc/Sidekick_cc.ml

@@ -282,7 +282,9 @@ module Make (A: CC_ARG)
   let[@inline] true_ cc = Lazy.force cc.true_
   let[@inline] false_ cc = Lazy.force cc.false_
   let[@inline] term_state cc = cc.tst
-  let[@inline] allocate_bitfield cc = Bits.mk_field cc.bitgen
+  let allocate_bitfield ~descr cc =
+    Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr);
+    Bits.mk_field cc.bitgen
 
   let[@inline] on_backtrack cc f : unit =
     Backtrack_stack.push_if_nonzero_level cc.undo f

src/core/Sidekick_core.ml

@@ -231,7 +231,7 @@ module type CC_S = sig
     t
   (** Create a new congruence closure. *)
 
-  val allocate_bitfield : t -> N.bitfield
+  val allocate_bitfield : descr:string -> t -> N.bitfield
   (** Allocate a new bitfield for the nodes.
       See {!N.bitfield}. *)
 
@@ -668,11 +668,24 @@ module type MONOID_ARG = sig
   module SI : SOLVER_INTERNAL
   type t
   val pp : t Fmt.printer
-  val name : string (* name of the monoid's value (short) *)
-  val of_term : SI.CC.N.t -> SI.T.Term.t -> t option
+  val name : string
+  (** name of the monoid's value (short) *)
+
+  val of_term :
+    SI.CC.N.t -> SI.T.Term.t ->
+    (t option * (SI.T.Term.t * t) list)
+  (** [of_term n t], where [t] is the term annotating node [n],
+      returns [maybe_m, l], where:
+      - [maybe_m = Some m] if [t] has monoid value [m];
+        otherwise [maybe_m=None]
+      - [l] is a list of [(u, m_u)] where each [u] is a direct subterm of [t]
+        and [m_u] is the monoid value attached to [u].
+      *)
+
   val merge : SI.CC.t -> SI.CC.N.t -> t -> SI.CC.N.t -> t -> (t, SI.CC.Expl.t) result
 end
 
+(** Keep track of monoid state per equivalence class *)
 module Monoid_of_repr(M : MONOID_ARG) : sig
   type t
   val create_and_setup : ?size:int -> M.SI.t -> t
@@ -680,7 +693,7 @@ module Monoid_of_repr(M : MONOID_ARG) : sig
   val pop_levels : t -> int -> unit
   val mem : t -> M.SI.CC.N.t -> bool
   val get : t -> M.SI.CC.N.t -> M.t option
-  val iter_all : t -> (M.SI.CC.N.t * M.t) Iter.t
+  val iter_all : t -> (M.SI.CC.repr * M.t) Iter.t
 end = struct
   module SI = M.SI
   module T = SI.T.Term
@@ -704,15 +717,52 @@ end = struct
 
   let get self n = N_tbl.get self.values n
 
-  let on_new_term self cc n (t:T.t) =
-    match M.of_term n t with
-    | Some v ->
-      Log.debugf 20
-        (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])"
-            M.name N.pp n M.pp v);
-      SI.CC.set_bitfield cc self.field_has_value true n;
-      N_tbl.add self.values n v
-    | None -> ()
+  let on_new_term self cc n (t:T.t) : unit =
+    let maybe_m, l = M.of_term n t in
+    begin match maybe_m with
+      | Some v ->
+        Log.debugf 20
+          (fun k->k "(@[monoid[%s].on-new-term@ :n %a@ :value %a@])"
+              M.name N.pp n M.pp v);
+        SI.CC.set_bitfield cc self.field_has_value true n;
+        N_tbl.add self.values n v
+      | None -> ()
+    end;
+    List.iter
+      (fun (u,m_u) ->
+        Log.debugf 20
+          (fun k->k "(@[monoid[%s].on-new-term.sub@ :n %a@ :sub-t %a@ :value %a@])"
+              M.name N.pp n T.pp u M.pp m_u);
+        let n_u =
+          try CC.find_t cc u
+          with Not_found -> Error.errorf "subterm %a does not have a repr" T.pp u
+        in
+        if N.get_field self.field_has_value n_u then (
+          let m_u' =
+            try N_tbl.find self.values n_u
+            with Not_found ->
+              Error.errorf "node %a has bitfield but no value" N.pp n_u
+          in
+          match M.merge cc n_u m_u n_u m_u' with
+          | Error expl ->
+            Error.errorf
+              "when merging@ @[for node %a@],@ \
+               values %a and %a:@ conflict %a"
+              N.pp n_u M.pp m_u M.pp m_u' CC.Expl.pp expl
+          | Ok m_u_merged ->
+            Log.debugf 20
+              (fun k->k "(@[monoid[%s].on-new-term.sub.merged@ \
+                         :n %a@ :sub-t %a@ :value %a@])"
+                  M.name N.pp n T.pp u M.pp m_u_merged);
+            N_tbl.add self.values n_u m_u_merged;
+        ) else (
+          (* just add to [n_u] *)
+          SI.CC.set_bitfield cc self.field_has_value true n_u;
+          N_tbl.add self.values n_u m_u;
+        )
+      )
+      l;
+    ()
 
   let iter_all (self:t) : _ Iter.t =
     N_tbl.to_iter self.values
@@ -756,7 +806,9 @@ end = struct
     end
 
   let create_and_setup ?size (solver:SI.t) : t =
-    let field_has_value = SI.CC.allocate_bitfield (SI.cc solver) in
+    let field_has_value =
+      SI.CC.allocate_bitfield ~descr:("monoid."^M.name^".has-value")
+        (SI.cc solver) in
     let self = { values=N_tbl.create ?size (); field_has_value; } in
     SI.on_cc_new_term solver (on_new_term self);
     SI.on_cc_pre_merge solver (on_pre_merge self);

src/main/sidekick_version.ml

@@ -1,2 +1,2 @@
-let version = {git|ef77e1e729f176c3db680de25df9f2f820795e47
+let version = {git|858ffb6f2587ca5593417be1c9f95fe727390e9e
 |git}

src/th-cstor/Sidekick_th_cstor.ml

@@ -40,10 +40,10 @@ module Make(A : ARG) : S with module A = A = struct
       Fmt.fprintf out "(@[cstor %a@ :term %a@])" Fun.pp v.cstor T.pp v.t
 
     (* attach data to constructor terms *)
-    let of_term n (t:T.t) : _ option =
+    let of_term n (t:T.t) : _ option * _ =
       match A.view_as_cstor t with
-      | T_cstor (cstor,args) -> Some {n; t; cstor; args}
-      | _ -> None
+      | T_cstor (cstor,args) -> Some {n; t; cstor; args}, []
+      | _ -> None, []
 
     let merge cc n1 v1 n2 v2 : _ result =
       Log.debugf 5

src/th-data/Sidekick_th_data.ml

@@ -138,77 +138,139 @@ module Make(A : ARG) : S with module A = A = struct
 
   module Card = Compute_card(A)
 
+  (** Monoid mapping each class to the (unique) constructor it contains,
+      if any *)
   module Monoid_cstor = struct
     module SI = SI
+    let name = "th-data.cstor"
 
     (* associate to each class a unique constructor term in the class (if any) *)
     type t = {
-      t: T.t;
-      n: N.t;
-      cstor: A.Cstor.t;
-      args: T.t IArray.t;
+      c_n: N.t;
+      c_cstor: A.Cstor.t;
+      c_args: T.t IArray.t;
     }
 
-    let name = "th-data.cstor"
     let pp out (v:t) =
-      Fmt.fprintf out "(@[cstor %a@ :term %a@])" A.Cstor.pp v.cstor T.pp v.t
+      Fmt.fprintf out "(@[%s@ :cstor %a@])" name A.Cstor.pp v.c_cstor
 
     (* attach data to constructor terms *)
-    let of_term n (t:T.t) : _ option =
+    let of_term n (t:T.t) : _ option * _ list =
       match A.view_as_data t with
-      | T_cstor (cstor,args) -> Some {n; t; cstor; args}
-      | _ -> None
+      | T_cstor (cstor,args) ->
+        Some {c_n=n;c_cstor=cstor; c_args=args}, []
+      | _ -> None, []
 
-    let merge cc n1 v1 n2 v2 : _ result =
+    let merge cc n1 c1 n2 c2 : _ result =
       Log.debugf 5
-        (fun k->k "(@[%s.merge@ @[:c1 %a (t %a)@]@ @[:c2 %a (t %a)@]@])"
-            name N.pp n1 T.pp v1.t N.pp n2 T.pp v2.t); 
+        (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])"
+            name N.pp n1 pp c1 N.pp n2 pp c2); 
       (* build full explanation of why the constructor terms are equal *)
       let expl =
         Expl.mk_list [
-          Expl.mk_merge n1 v1.n;
-          Expl.mk_merge n2 v2.n;
+          Expl.mk_merge n1 c1.c_n;
+          Expl.mk_merge n2 c2.c_n;
           Expl.mk_merge n1 n2;
         ]
       in
-      if A.Cstor.equal v1.cstor v2.cstor then (
+      if A.Cstor.equal c1.c_cstor c2.c_cstor then (
         (* same function: injectivity *)
-        assert (IArray.length v1.args = IArray.length v2.args);
+        assert (IArray.length c1.c_args = IArray.length c2.c_args);
         IArray.iter2
           (fun u1 u2 -> SI.CC.merge_t cc u1 u2 expl)
-          v1.args v2.args;
-        Ok v1
+          c1.c_args c2.c_args;
+        Ok c1
       ) else (
         (* different function: disjointness *)
         Error expl
       )
   end
 
+  (** Monoid mapping each class to the set of is-a/select of which it
+      is the argument *)
+  module Monoid_parents = struct
+    module SI = SI
+    let name = "th-data.parents"
+
+    type select = {
+      sel_n: N.t;
+      sel_cstor: A.Cstor.t;
+      sel_idx: int;
+    }
+
+    type is_a = {
+      is_a_n: N.t;
+      is_a_cstor: A.Cstor.t;
+    }
+
+    (* associate to each class a unique constructor term in the class (if any) *)
+    type t = {
+      parent_is_a: is_a list;(* parents that are [is-a] *)
+      parent_select: select list; (* parents that are [select] *)
+    }
+
+    let pp_select out s = Fmt.fprintf out "sel[%d]-%a" s.sel_idx A.Cstor.pp s.sel_cstor
+    let pp_is_a out s = Fmt.fprintf out "is-%a" A.Cstor.pp s.is_a_cstor
+    let pp out (v:t) =
+      Fmt.fprintf out
+        "(@[%s@ @[:sel [@[%a@]]@]@ @[:is-a [@[%a@]]@]@])"
+        name
+        (Util.pp_list pp_select) v.parent_select
+        (Util.pp_list pp_is_a) v.parent_is_a
+
+    (* attach data to constructor terms *)
+    let of_term n (t:T.t) : _ option * _ list =
+      match A.view_as_data t with
+      | T_select (c, i, u) ->
+        let m_sel = {
+          parent_select=[{sel_n=n; sel_idx=i; sel_cstor=c}];
+          parent_is_a=[];
+        } in
+        None, [u, m_sel]
+      | T_is_a (c, u) ->
+        let m_sel = {
+          parent_is_a=[{is_a_n=n; is_a_cstor=c}];
+          parent_select=[];
+        } in
+        None, [u, m_sel]
+      | T_cstor _ | T_other _ -> None, []
+
+    let merge cc n1 v1 n2 v2 : _ result =
+      Log.debugf 5
+        (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])"
+            name N.pp n1 pp v1 N.pp n2 pp v2); 
+      let parent_is_a = v1.parent_is_a @ v2.parent_is_a in
+      let parent_select = v1.parent_select @ v2.parent_select in
+      Ok {parent_is_a; parent_select;}
+  end
+
   module ST_cstors = Sidekick_core.Monoid_of_repr(Monoid_cstor)
+  module ST_parents = Sidekick_core.Monoid_of_repr(Monoid_parents)
   module N_tbl = Backtrackable_tbl.Make(N)
 
   type t = {
     tst: T.state;
     cstors: ST_cstors.t; (* repr -> cstor for the class *)
+    parents: ST_parents.t; (* repr -> parents for the class *)
     cards: Card.t; (* remember finiteness *)
     to_decide: unit N_tbl.t; (* set of terms to decide. *)
     case_split_done: unit T.Tbl.t; (* set of terms for which case split is done *)
-    (* TODO: also allocate a bit in CC to filter out quickly classes without cstors? *)
     (* TODO: bitfield for types with less than 62 cstors, to quickly detect conflict? *)
   }
 
   let push_level self =
     ST_cstors.push_level self.cstors;
+    ST_parents.push_level self.parents;
     N_tbl.push_level self.to_decide;
     ()
 
   let pop_levels self n =
     ST_cstors.pop_levels self.cstors n;
+    ST_parents.pop_levels self.parents n;
     N_tbl.pop_levels self.to_decide n;
     ()
 
   (* TODO: select/is-a *)
-  (* TODO: acyclicity *)
 
   (* TODO: remove
   (* attach data to constructor terms *)
@@ -310,12 +372,12 @@ module Make(A : ARG) : S with module A = A = struct
             Log.debugf 100
               (fun k->k "(@[data.acycl.mk-path %a %a@])" N.pp n pp_parent parent);
             let acc = Expl.mk_merge_t (N.term n) parent.t_eq_n :: acc in
-            let acc = Expl.mk_merge parent.parent.n parent.parent.cstor.n :: acc in
+            let acc = Expl.mk_merge parent.parent.n parent.parent.n :: acc in
             match parent.parent.flag with
             | Current (Some p') -> mk_path acc parent.parent.n p'
             | _ -> acc
           in
-          let c0 = [Expl.mk_merge n st.cstor.n;] in
+          let c0 = [Expl.mk_merge n st.n;] in
           let c = match parent with
             | None -> c0
             | Some parent -> mk_path c0 n parent
@@ -331,7 +393,7 @@ module Make(A : ARG) : S with module A = A = struct
              | Some st' ->
                let parent = {parent=st; t_eq_n=sub_t} in
                traverse ~parent sub st')
-          st.cstor.args;
+          st.cstor.Monoid_cstor.c_args;
       in
       begin
         (* populate tbl with [repr->cstor] *)
@@ -393,6 +455,7 @@ module Make(A : ARG) : S with module A = A = struct
     let self = {
       tst=SI.tst solver;
       cstors=ST_cstors.create_and_setup ~size:32 solver;
+      parents=ST_parents.create_and_setup ~size:32 solver;
       to_decide=N_tbl.create ~size:16 ();
       case_split_done=T.Tbl.create 16;
       cards=Card.create();