feat: initial support for is-a/select

src/cc/Sidekick_cc.ml

@@ -279,8 +279,9 @@ module Make (A: CC_ARG)
   and ev_on_propagate = t -> lit -> (unit -> lit list) -> unit
 
   let[@inline] size_ (r:repr) = r.n_size
-  let[@inline] true_ cc = Lazy.force cc.true_
+  let[@inline] n_true cc = Lazy.force cc.true_
-  let[@inline] false_ cc = Lazy.force cc.false_
+  let[@inline] n_false cc = Lazy.force cc.false_
+  let n_bool cc b = if b then n_true cc else n_false cc
   let[@inline] term_state cc = cc.tst
   let allocate_bitfield ~descr cc =
     Log.debugf 5 (fun k->k "(@[cc.allocate-bit-field@ :descr %s@])" descr);
@@ -557,7 +558,7 @@ module Make (A: CC_ARG)
       n.n_as_lit <- Some lit
 
   let n_is_bool (self:t) n : bool =
-    N.equal n (true_ self) || N.equal n (false_ self)
+    N.equal n (n_true self) || N.equal n (n_false self)
 
   (* main CC algo: add terms from [pending] to the signature table,
      check for collisions *)
@@ -581,17 +582,17 @@ module Make (A: CC_ARG)
           let expl = Expl.mk_merge a b in
           Log.debugf 5 
             (fun k->k "(pending.eq@ %a@ :r1 %a@ :r2 %a@])" N.pp n N.pp a N.pp b);
-          merge_classes cc n (true_ cc) expl
+          merge_classes cc n (n_true cc) expl
         )
       | Some (Not u) ->
         (* [u = bool ==> not u = not bool] *)
         let r_u = find_ u in
-        if N.equal r_u (true_ cc) then (
+        if N.equal r_u (n_true cc) then (
-          let expl = Expl.mk_merge u (true_ cc) in
+          let expl = Expl.mk_merge u (n_true cc) in
-          merge_classes cc n (false_ cc) expl
+          merge_classes cc n (n_false cc) expl
-        ) else if N.equal r_u (false_ cc) then (
+        ) else if N.equal r_u (n_false cc) then (
-          let expl = Expl.mk_merge u (false_ cc) in
+          let expl = Expl.mk_merge u (n_false cc) in
-          merge_classes cc n (true_ cc) expl
+          merge_classes cc n (n_true cc) expl
         )
       | Some s0 ->
         (* update the signature by using [find] on each sub-node *)
@@ -622,8 +623,8 @@ module Make (A: CC_ARG)
       assert (N.is_root rb);
       Stat.incr cc.count_merge;
       (* check we're not merging [true] and [false] *)
-      if (N.equal ra (true_ cc) && N.equal rb (false_ cc)) ||
+      if (N.equal ra (n_true cc) && N.equal rb (n_false cc)) ||
-         (N.equal rb (true_ cc) && N.equal ra (false_ cc)) then (
+         (N.equal rb (n_true cc) && N.equal ra (n_false cc)) then (
         Log.debugf 5
           (fun k->k "(@[<hv>cc.merge.true_false_conflict@ \
                      @[:r1 %a@ :t1 %a@]@ @[:r2 %a@ :t2 %a@]@ :e_ab %a@])"
@@ -644,9 +645,9 @@ module Make (A: CC_ARG)
       in
       (* when merging terms with [true] or [false], possibly propagate them to SAT *)
       let merge_bool r1 t1 r2 t2 =
-        if N.equal r1 (true_ cc) then (
+        if N.equal r1 (n_true cc) then (
           propagate_bools cc acts r2 t2 r1 t1 e_ab true
-        ) else if N.equal r1 (false_ cc) then (
+        ) else if N.equal r1 (n_false cc) then (
           propagate_bools cc acts r2 t2 r1 t1 e_ab false
         )
       in
@@ -788,7 +789,7 @@ module Make (A: CC_ARG)
         merge_classes cc a b (Expl.mk_lit lit)
       | _ ->
         (* equate t and true/false *)
-        let rhs = if sign then true_ cc else false_ cc in
+        let rhs = if sign then n_true cc else n_false cc in
         let n = add_term cc t in
         (* TODO: ensure that this is O(1).
            basically, just have [n] point to true/false and thus acquire

src/core/Sidekick_core.ml

@@ -282,6 +282,10 @@ module type CC_S = sig
       it must be a theory tautology that [expl ==> absurd].
       To be used in theories. *)
 
+  val n_true : t -> N.t
+  val n_false : t -> N.t
+  val n_bool : t -> bool -> N.t
+
   val merge : t -> N.t -> N.t -> Expl.t -> unit
   (** Merge these two nodes given this explanation.
       It must be a theory tautology that [expl ==> n1 = n2].
@@ -715,7 +719,10 @@ end = struct
     assert (if res then N_tbl.mem self.values n else true);
     res
 
-  let get self n = N_tbl.get self.values n
+  let get self n =
+    if N.get_field self.field_has_value n
+    then N_tbl.get self.values n
+    else None
 
   let on_new_term self cc n (t:T.t) : unit =
     let maybe_m, l = M.of_term n t in

src/main/sidekick_version.ml

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

src/th-data/Sidekick_th_data.ml

@@ -313,15 +313,78 @@ module Make(A : ARG) : S with module A = A = struct
       )
     | _ -> ()
 
-  let on_new_term self _solver n t =
+  let on_new_term (self:t) cc (n:N.t) (t:T.t) : unit =
-    on_new_term_look_at_ty self n t;
+    on_new_term_look_at_ty self n t; (* might have to decide [t] *)
-    ()
+    match A.view_as_data t with
+    | T_is_a (c_t, u) ->
+      let n_u = SI.CC.add_term cc u in
+      let repr_u = SI.CC.find cc n_u in
+      begin match ST_cstors.get self.cstors repr_u with
+        | None -> ()
+        | Some cstor ->
+          let is_true = A.Cstor.equal cstor.c_cstor c_t in
+          Log.debugf 5
+            (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])"
+                name is_true N.pp n Monoid_cstor.pp cstor);
+          SI.CC.merge cc n (SI.CC.n_bool cc is_true) (Expl.mk_merge n_u repr_u)
+      end
+    | T_select (c_t, i, u) ->
+      let n_u = SI.CC.add_term cc u in
+      let repr_u = SI.CC.find cc n_u in
+      begin match ST_cstors.get self.cstors repr_u with
+        | Some cstor when A.Cstor.equal cstor.c_cstor c_t ->
+          Log.debugf 5
+            (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])"
+                name N.pp n i A.Cstor.pp c_t);
+          assert (i < IArray.length cstor.c_args);
+          let u_i = IArray.get cstor.c_args i in
+          let n_u_i = SI.CC.add_term cc u_i in
+          SI.CC.merge cc n n_u_i (Expl.mk_merge n_u repr_u)
+        | _ -> ()
+      end
+    | T_cstor _ | T_other _ -> ()
 
   let cstors_of_ty (ty:Ty.t) : A.Cstor.t Iter.t =
     match A.as_datatype ty with
     | Ty_data {cstors} -> cstors
     | _ -> assert false
 
+  let on_pre_merge (self:t) (cc:SI.CC.t) acts n1 n2 expl : unit =
+    let merge_is_a n1 (c1:Monoid_cstor.t) n2 (is_a2:Monoid_parents.is_a) =
+      let is_true = A.Cstor.equal c1.c_cstor is_a2.is_a_cstor in
+      Log.debugf 50
+        (fun k->k "(@[%s.on-new-term.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])"
+            name is_true N.pp n2 Monoid_cstor.pp c1);
+      SI.CC.merge cc n2 (SI.CC.n_bool cc is_true)
+        Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 is_a2.is_a_n])
+    in
+    let merge_select n1 (c1:Monoid_cstor.t) n2 (sel2:Monoid_parents.select) =
+      if A.Cstor.equal c1.c_cstor sel2.sel_cstor then (
+        Log.debugf 5
+          (fun k->k "(@[%s.on-new-term.select.reduce@ :n %a@ :sel get[%d]-%a@])"
+              name N.pp n2 sel2.sel_idx Monoid_cstor.pp c1);
+        assert (sel2.sel_idx < IArray.length c1.c_args);
+        let u_i = IArray.get c1.c_args sel2.sel_idx in
+        let n_u_i = SI.CC.add_term cc u_i in
+        SI.CC.merge cc n2 n_u_i
+          Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n2 sel2.sel_n]);
+      )
+    in
+    let merge_c_p n1 n2 =
+      match ST_cstors.get self.cstors n1, ST_parents.get self.parents n2 with
+      | None, _
+      | _, None -> ()
+      | Some c1, Some p2 ->
+        Log.debugf 50
+          (fun k->k "(@[%s.pre-merge@ @[:n1 %a@ :c1 %a@]@ @[:n2 %a@ :p2 %a@]@])"
+              name N.pp n1 Monoid_cstor.pp c1 N.pp n2 Monoid_parents.pp p2);
+        List.iter (fun is_a2 -> merge_is_a n1 c1 n2 is_a2) p2.parent_is_a;
+        List.iter (fun s2 -> merge_select n1 c1 n2 s2) p2.parent_select;
+    in
+    merge_c_p n1 n2;
+    merge_c_p n2 n1;
+    ()
+
   module Acyclicity_ = struct
     type st = {
       n: N.t;
@@ -462,6 +525,7 @@ module Make(A : ARG) : S with module A = A = struct
     } in
     Log.debugf 1 (fun k->k "(setup :%s)" name);
     SI.on_cc_new_term solver (on_new_term self);
+    SI.on_cc_pre_merge solver (on_pre_merge self);
     SI.on_final_check solver (on_final_check self);
     self