fixes: add missing expl in monoids; handle is-c t

src/base-term/Base_types.ml

@@ -402,6 +402,7 @@ module Fun : sig
   val as_undefined_exn : t -> t * Ty.Fun.t
   val is_undefined : t -> bool
   val select : select -> t
+  val select_idx : cstor -> int -> t
   val cstor : cstor -> t
   val is_a : cstor -> t
 
@@ -452,6 +453,12 @@ end = struct
   let is_a c : t = make c.cstor_is_a (Fun_is_a c)
   let cstor c : t = make c.cstor_id (Fun_cstor c)
   let select sel : t = make sel.select_id (Fun_select sel)
+  let select_idx c i : t =
+    let lazy l = c.cstor_args in
+    match List.nth l i with
+    | sel -> select sel
+    | exception Not_found ->
+      Error.errorf "invalid selector %d for cstor %a" i ID.pp c.cstor_id
 
   let[@inline] do_cc (c:t) : bool = match view c with
     | Fun_cstor _ | Fun_select _ | Fun_undef _ | Fun_is_a _ -> true

src/cc/Sidekick_cc.ml

@@ -348,10 +348,12 @@ module Make (A: CC_ARG)
     Vec.push cc.pending t
 
   let merge_classes cc t u e : unit =
-    Log.debugf 50
+    if t != u && not (same_class t u) then (
-      (fun k->k "(@[<hv1>cc.push-combine@ %a ~@ %a@ :expl %a@])"
+      Log.debugf 50
-        N.pp t N.pp u Expl.pp e);
+        (fun k->k "(@[<hv1>cc.push-combine@ %a ~@ %a@ :expl %a@])"
-    Vec.push cc.combine @@ CT_merge (t,u,e)
+          N.pp t N.pp u Expl.pp e);
+      Vec.push cc.combine @@ CT_merge (t,u,e)
+    )
 
   (* re-root the explanation tree of the equivalence class of [n]
      so that it points to [n].

src/core/Sidekick_core.ml

@@ -685,7 +685,11 @@ module type MONOID_ARG = sig
         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
+  val merge :
+    SI.CC.t ->
+    SI.CC.N.t -> t -> SI.CC.N.t -> t ->
+    SI.CC.Expl.t ->
+    (t, SI.CC.Expl.t) result
 end
 
 (** Keep track of monoid state per equivalence class *)
@@ -749,7 +753,7 @@ end = struct
             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
+          match M.merge cc n_u m_u n_u m_u' (Expl.mk_list []) with
           | Error expl ->
             Error.errorf
               "when merging@ @[for node %a@],@ \
@@ -773,35 +777,18 @@ end = struct
   let iter_all (self:t) : _ Iter.t =
     N_tbl.to_iter self.values
 
-  (* find cell for [n] *)
-  let get_cell (self:t) (n:N.t) : M.t option =
-    N_tbl.get self.values n
-    (* TODO
-    if N.get_field self.field_has_value n then (
-      try Some (N_tbl.find self.values n)
-      with Not_found ->
-        Error.errorf "repr %a has value-field bit for %s set, but is not in table"
-          N.pp n M.name
-    ) else (
-      None
-    )
-       *)
-
   let on_pre_merge (self:t) cc acts n1 n2 e_n1_n2 : unit =
-    begin match get_cell self n1, get_cell self n2 with
+    begin match get self n1, get self n2 with
       | Some v1, Some v2 ->
         Log.debugf 5
           (fun k->k
-              "(@[monoid[%s].on_pre_merge@ @[:n1 %a@ :val %a@]@ @[:n2 %a@ :val %a@]@])"
+              "(@[monoid[%s].on_pre_merge@ (@[:n1 %a@ :val1 %a@])@ (@[:n2 %a@ :val2 %a@])@])"
               M.name N.pp n1 M.pp v1 N.pp n2 M.pp v2); 
-        begin match M.merge cc n1 v1 n2 v2 with
+        begin match M.merge cc n1 v1 n2 v2 e_n1_n2 with
           | Ok v' ->
             N_tbl.remove self.values n2; (* only keep repr *)
             N_tbl.add self.values n1 v';
-          | Error expl ->
+          | Error expl -> SI.CC.raise_conflict_from_expl cc acts expl
-            (* add [n1=n2] to the conflict *)
-            let expl = Expl.mk_list [ e_n1_n2; expl; ] in
-            SI.CC.raise_conflict_from_expl cc acts expl
         end
       | None, Some cr ->
         SI.CC.set_bitfield cc self.field_has_value true n1;

src/smtlib/Process.ml

@@ -66,7 +66,6 @@ module Check_cc = struct
         (fun k->k "(@[check-cc-prop.ok@ @[%a => %a@]@])" pp_and reason Lit.pp p);
     )
 
-
   let theory =
     Solver.mk_theory ~name:"cc-check"
       ~create_and_setup:(fun si ->
@@ -282,6 +281,7 @@ module Th_data = Sidekick_th_data.Make(struct
       | _ -> T_other t
 
     let mk_cstor tst c args : Term.t = Term.app_fun tst (Fun.cstor c) args
+    let mk_sel tst c i u = Term.app_fun tst (Fun.select_idx c i) (IArray.singleton u)
     let mk_is_a tst c u : Term.t =
       if c.cstor_arity=0 then (
         Term.eq tst u (Term.const tst (Fun.cstor c))

src/th-cstor/Sidekick_th_cstor.ml

@@ -45,13 +45,14 @@ module Make(A : ARG) : S with module A = A = struct
       | T_cstor (cstor,args) -> Some {n; t; cstor; args}, []
       | _ -> None, []
 
-    let merge cc n1 v1 n2 v2 : _ result =
+    let merge cc n1 v1 n2 v2 e_n1_n2 : _ 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); 
       (* build full explanation of why the constructor terms are equal *)
       let expl =
         Expl.mk_list [
+          e_n1_n2;
           Expl.mk_merge n1 v1.n;
           Expl.mk_merge n2 v2.n;
         ]

src/th-data/Sidekick_th_data.ml

@@ -73,6 +73,7 @@ module type ARG = sig
   val view_as_data : S.T.Term.t -> (Cstor.t, S.T.Term.t) data_view
   val mk_cstor : S.T.Term.state -> Cstor.t -> S.T.Term.t IArray.t -> S.T.Term.t
   val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t
+  val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
   val ty_is_finite : S.T.Ty.t -> bool
   val ty_set_is_finite : S.T.Ty.t -> bool -> unit
 end
@@ -152,7 +153,7 @@ module Make(A : ARG) : S with module A = A = struct
     }
 
     let pp out (v:t) =
-      Fmt.fprintf out "(@[%s@ :cstor %a@])" name A.Cstor.pp v.c_cstor
+      Fmt.fprintf out "(@[%s@ :cstor %a@ :n %a@])" name A.Cstor.pp v.c_cstor N.pp v.c_n
 
     (* attach data to constructor terms *)
     let of_term n (t:T.t) : _ option * _ list =
@@ -161,13 +162,15 @@ module Make(A : ARG) : S with module A = A = struct
         Some {c_n=n;c_cstor=cstor; c_args=args}, []
       | _ -> None, []
 
-    let merge cc n1 c1 n2 c2 : _ result =
+    let merge cc n1 c1 n2 c2 e_n1_n2 : _ result =
       Log.debugf 5
-        (fun k->k "(@[%s.merge@ @[:c1 %a %a@]@ @[:c2 %a %a@]@])"
+        (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 *)
+      (* TODO: have a sort of lemma (injectivity) here to justify this in the proof *)
       let expl =
         Expl.mk_list [
+          e_n1_n2;
           Expl.mk_merge n1 c1.c_n;
           Expl.mk_merge n2 c2.c_n;
         ]
@@ -195,11 +198,13 @@ module Make(A : ARG) : S with module A = A = struct
       sel_n: N.t;
       sel_cstor: A.Cstor.t;
       sel_idx: int;
+      sel_arg: T.t;
     }
 
     type is_a = {
       is_a_n: N.t;
       is_a_cstor: A.Cstor.t;
+      is_a_arg: T.t;
     }
 
     (* associate to each class a unique constructor term in the class (if any) *)
@@ -222,19 +227,19 @@ module Make(A : ARG) : S with module A = A = struct
       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_select=[{sel_n=n; sel_idx=i; sel_cstor=c; sel_arg=u}];
           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_is_a=[{is_a_n=n; is_a_cstor=c; is_a_arg=u;}];
           parent_select=[];
         } in
         None, [u, m_sel]
       | T_cstor _ | T_other _ -> None, []
 
-    let merge cc n1 v1 n2 v2 : _ result =
+    let merge cc n1 v1 n2 v2 _e : _ 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); 
@@ -324,8 +329,8 @@ module Make(A : ARG) : S with module A = A = struct
         | 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@])"
+            (fun k->k "(@[%s.on-new-term.is-a.reduce@ :t %a@ :to %B@ :n %a@ :sub-cstor %a@])"
-                name is_true N.pp n Monoid_cstor.pp cstor);
+                name T.pp t 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) ->
@@ -351,27 +356,27 @@ module Make(A : ARG) : S with module A = A = struct
     | Ty_data {cstors} -> cstors
     | _ -> assert false
 
-  (* FIXME: when merging [(is _ C) t] with true, propagate [t=C(sel[1]-c(t),…)] *)
-  (* FIXME: when merging [(is _ C) t] with false, remove [C] from the available list *)
   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-merge.is-a.reduce@ :to %B@ :n %a@ :sub-cstor %a@])"
+        (fun k->k "(@[%s.on-merge.is-a.reduce@ %a@ :to %B@ :n1 %a@ :n2 %a@ :sub-cstor %a@])"
-            name is_true N.pp n2 Monoid_cstor.pp c1);
+            name Monoid_parents.pp_is_a is_a2 is_true N.pp n1 N.pp n2 Monoid_cstor.pp c1);
       SI.CC.merge cc is_a2.is_a_n (SI.CC.n_bool cc is_true)
-        Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2])
+        Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2;
+                       mk_merge_t (N.term n2) is_a2.is_a_arg])
     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-merge.select.reduce@ :n %a@ :sel get[%d]-%a@])"
+          (fun k->k "(@[%s.on-merge.select.reduce@ :n2 %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 sel2.sel_n n_u_i
-          Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2]);
+          Expl.(mk_list [mk_merge n1 c1.c_n; mk_merge n1 n2;
+                         mk_merge_t (N.term n2) sel2.sel_arg]);
       )
     in
     let merge_c_p n1 n2 =
@@ -380,7 +385,7 @@ module Make(A : ARG) : S with module A = A = struct
       | _, None -> ()
       | Some c1, Some p2 ->
         Log.debugf 50
-          (fun k->k "(@[%s.pre-merge@ @[:n1 %a@ :c1 %a@]@ @[:n2 %a@ :p2 %a@]@])"
+          (fun k->k "(@[<hv>%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;
@@ -472,6 +477,29 @@ module Make(A : ARG) : S with module A = A = struct
       end
   end
 
+  (* FIXME: when merging [(is _ C) t] with false, remove [C] from the available list *)
+  let on_partial_check (self:t) (solver:SI.t) (acts:SI.actions) trail =
+    let check_lit lit =
+      let t = SI.Lit.term lit in
+      match A.view_as_data t with
+      | T_is_a (c, u) when SI.Lit.sign lit ->
+        (* add [((_ is C) u) ==> u = C(sel-c-0 u, …, sel-c-k u)] *)
+        let rhs =
+          let args =
+            A.Cstor.ty_args c
+            |> Iter.mapi (fun i _ty -> A.mk_sel self.tst c i u)
+            |> Iter.to_list |> IArray.of_list
+          in
+          A.mk_cstor self.tst c args
+        in
+        Log.debugf 50
+          (fun k->k"(@[%s.assign-is-a@ :lhs %a@ :rhs %a@ :lit %a@])"
+              name T.pp u  T.pp rhs SI.Lit.pp lit);
+        SI.cc_merge_t solver acts u rhs (Expl.mk_lit lit)
+      | _ -> ()
+    in
+    Iter.iter check_lit trail
+
   (* on final check, check acyclicity,
      then make sure we have done case split on all terms that
      need it. *)
@@ -530,6 +558,7 @@ module Make(A : ARG) : S with module A = A = struct
     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_partial_check solver (on_partial_check self);
     SI.on_final_check solver (on_final_check self);
     self
 

src/th-data/Sidekick_th_data.mli

@@ -42,6 +42,9 @@ module type ARG = sig
   val mk_is_a: S.T.Term.state -> Cstor.t -> S.T.Term.t -> S.T.Term.t
   (** Make a [is-a] term *)
 
+  val mk_sel : S.T.Term.state -> Cstor.t -> int -> S.T.Term.t -> S.T.Term.t
+  (** Make a selector term *)
+
   val ty_is_finite : S.T.Ty.t -> bool
   (** Is the given type known to be finite? *)