Allow match_any_term to work with any initial substitution

src_colibri2/theories/quantifier/pattern.ml

@@ -275,13 +275,13 @@ let env_node_by_ty =
   EnvTy.create (Context.Queue.pp ~sep:Fmt.semi Node.pp)
     "Quantifier.Trigger.node_by_ty" (fun c _ -> Context.Queue.create c)
 
-let match_any_term d (p : t) : Ground.Subst.S.t =
+let match_any_term d subst (p : t) : Ground.Subst.S.t =
   Debug.dprintf2 debug "[Quant] matching any for %a" pp p;
   match p with
   | Var v ->
       EnvTy.fold
         (fun ty q acc ->
-          let substs = match_ty init ty v.ty in
+          let substs = match_ty subst ty v.ty in
           if Ground.Subst.S.is_empty substs then acc
           else
             Ground.Subst.S.fold_left
@@ -302,7 +302,7 @@ let match_any_term d (p : t) : Ground.Subst.S.t =
         (fun acc n ->
           let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
           assert (Term.Const.equal f pf);
-          let substs = List.fold_left2 match_ty init tyl ptyl in
+          let substs = List.fold_left2 match_ty subst tyl ptyl in
           let substs =
             IArray.fold2_exn args pargs ~init:substs ~f:(match_term d)
           in

src_colibri2/theories/quantifier/pattern.mli

@@ -56,8 +56,10 @@ val check_term_exists : Egraph.t -> Ground.Subst.t -> t -> Node.S.t
 (** [check_term_exists d subst pat] return nodes that are equal to the pattern
    [pat] substituted by the substitution [subst] *)
 
-val match_any_term : Egraph.t -> t -> Ground.Subst.S.t
-(** [match_any_term d pat] match the pattern [pat] to all the nodes of [d] *)
+val match_any_term : Egraph.t -> Ground.Subst.S.t -> t -> Ground.Subst.S.t
+(** [match_any_term d subst pat] match the pattern [pat] to all the nodes of [d]
+   for each substitution. Each return substitution corresponds to one given as
+   input. *)
 
 val get_pps : t -> PP.t list Term.Var.M.t
 (** [get_pps pat] return the parent-parent pairs in [pat] for each variables *)

src_colibri2/theories/quantifier/quantifier.ml

@@ -27,7 +27,7 @@ open Common
 let add_trigger d t =
   Trigger.add_trigger d t;
   InvertedPath.insert_pattern d t;
-  let substs = Pattern.match_any_term d t.pat in
+  let substs = Pattern.match_any_term d Pattern.init t.pat in
   Ground.Subst.S.iter (Trigger.instantiate d t) substs
 
 let find_new_event d n (info : Info.t) n' (info' : Info.t) =