[Quant] try to only do eager instantiation for already know terms

But loose some regression tests, and it is still too often for real examples

src_colibri2/core/ground.ml

@@ -175,6 +175,15 @@ let rec convert ?(subst=Subst.empty) (t : Expr.Term.t) =
     assert false (* TODO convert to one multitest like
                     the match of why3  and projection *)
 
+let apply (f:Expr.Term.Const.t) tyargs args =
+  let subst =
+    List.fold_left2
+      (fun acc v ty -> Expr.Ty.Var.M.add v ty acc)
+      Expr.Ty.Var.M.empty f.ty.fun_vars tyargs
+  in
+  let ty = Ty.convert subst f.ty.fun_ret in
+  { Term.app = f; tyargs; args; ty }
+
 (** Definitions *)
 module Defs = struct
 

src_colibri2/core/ground.mli

@@ -86,6 +86,8 @@ include RegisteredThTerm with type s := Term.t
 
 val convert : ?subst:Subst.t -> Expr.Term.t -> Node.t
 
+val apply : Expr.Term.Const.t -> Ty.t list -> Node.t list -> Term.t
+
 val init: Egraph.t -> unit
 
 val register_converter:

src_colibri2/core/structures/expr.ml

@@ -33,6 +33,15 @@ module Ty = struct
     | Var v -> Var.S.add v acc
     | App (_, l) -> List.fold_left free_vars acc l
 
+  let rec subst_ty subst (p : t) : t  =
+    match p.descr with
+    | Var v -> (
+        match Var.M.find v subst with
+        | exception Not_found -> p
+        | ty -> ty)
+    | App (cst, tyl) ->
+      apply cst (List.map (subst_ty subst) tyl)
+
   module Const = struct
     include Dolmen_std.Expr.Ty.Const
     let pp fmt (t:t) = Dolmen_std.Expr.Id.print fmt t

src_colibri2/theories/quantifier/quantifier.ml

@@ -208,6 +208,100 @@ module Pattern = struct
             Ground.Subst.S.union substs acc)
           Ground.Subst.S.empty s
 
+  let rec check_ty subst (ty : Ground.Ty.t) (p : Expr.Ty.t) : bool =
+    match p.descr with
+    | Var v -> (
+        match Expr.Ty.Var.M.find v subst.Ground.Subst.ty with
+        | exception Not_found -> false
+        | ty' -> Ground.Ty.equal ty ty' )
+    | App (cst', tyl') ->
+        Expr.Ty.Const.equal ty.app cst'
+        && List.for_all2 (check_ty subst) ty.args tyl'
+
+  let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
+    Debug.dprintf4 debug "[Quant] check %a %a" pp p Node.pp n;
+    match p with
+    | Var v -> (
+        match Datastructure.HNode.find_opt Info.env d n with
+        | None -> false
+        | Some info -> (
+            Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty) info.tys
+            &&
+            match Expr.Term.Var.M.find v subst.term with
+            | exception Not_found -> false
+            | n' -> Egraph.is_equal d n n' ) )
+    | App (pf, ptyl, pargs) ->
+        let s =
+          Opt.get_def Ground.S.empty
+          @@
+          let open Option in
+          let* info =
+            Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n)
+          in
+          F.M.find_opt pf info.apps
+        in
+        Ground.S.exists
+          (fun n ->
+            let { Ground.Term.app = f; tyargs = tyl; args; _ } = Ground.sem n in
+            assert (Term.Const.equal f pf);
+            List.for_all2 (check_ty subst) tyl ptyl
+            && List.for_all2 (check_term d subst) args pargs)
+          s
+
+  let _ = check_term
+
+  exception IncompleteSubstitution
+
+  let rec check_term_exists d (subst : Ground.Subst.t) (p : t) : Node.S.t =
+    match p with
+    | Var v -> (
+        match Expr.Term.Var.M.find v subst.term with
+        | exception Not_found -> raise IncompleteSubstitution
+        | n -> (
+            match Datastructure.HNode.find_opt Info.env d n with
+            | None -> raise Not_found
+            | Some info ->
+                if
+                  (Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty))
+                    info.tys
+                then Node.S.singleton (Egraph.find_def d n)
+                else raise Not_found ) )
+    | App (pf, ptyl, []) ->
+        let g =
+          Ground.apply pf (List.map (Ground.Ty.convert subst.ty) ptyl) []
+          |> Ground.index |> Ground.node
+        in
+        if Egraph.is_registered d g then Node.S.singleton (Egraph.find d g)
+        else raise Not_found
+    | App (pf, _, parg :: pargs) ->
+        let find_app pos n =
+          Opt.get_def Ground.S.empty
+          @@
+          let open Option in
+          let* info =
+            Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n)
+          in
+          F_Pos.M.find_opt { f = pf; pos } info.parents
+        in
+        let get_parents pos parg =
+          let nodes = check_term_exists d subst parg in
+          let nodes =
+            Node.S.fold_left
+              (fun acc n ->
+                Ground.S.fold_left
+                  (fun acc g -> Node.S.add (Ground.node g) acc)
+                  acc (find_app pos n))
+              Node.S.empty nodes
+          in
+          nodes
+        in
+        let nodes =
+          Lists.fold_lefti
+            (fun acc i parg -> Node.S.inter acc (get_parents (i + 1) parg))
+            (get_parents 0 parg) pargs
+        in
+        if Node.S.is_empty nodes then raise Not_found else nodes
+
   let get_pps pattern =
     let rec aux acc fp p =
       match p with
@@ -241,6 +335,7 @@ module Trigger = struct
 
     type t = {
       pat : Pattern.t;
+      checks : Pattern.t list;
       (* list *) form : Ground.ThClosedQuantifier.t;
       eager : bool;
     }
@@ -254,6 +349,59 @@ module Trigger = struct
   include T
   include Popop_stdlib.MkDatatype (T)
 
+  let compute_top_triggers (cq : Ground.ThClosedQuantifier.t) =
+    let cq' = Ground.ThClosedQuantifier.sem cq in
+    let tyvs = cq'.ty_vars in
+    let tvs = cq'.term_vars in
+    let t = cq'.body in
+    let rec aux pats (t : Expr.Term.t) =
+      match t.descr with
+      | Expr.Binder (_, _) -> pats (* todo *)
+      | Expr.Match (_, _) -> pats (* todo *)
+      | Expr.App
+          ( {
+              builtin =
+                ( Expr.And | Expr.Equal | Expr.Equiv | Expr.Or | Expr.Xor
+                | Expr.Imply );
+              _;
+            },
+            _,
+            tl ) ->
+          List.fold_left aux pats tl
+      | _ -> t :: pats
+    in
+    let pats = aux [] t in
+    let tyvs = Expr.Ty.Var.S.of_list tyvs in
+    let tvs = Expr.Term.Var.S.of_list tvs in
+    let pats_full, pats_partial =
+      Base.List.partition_tf
+        ~f:(fun pat ->
+          let sty, st =
+            Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) pat
+          in
+          Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs)
+        pats
+    in
+    let pats_full = List.map Pattern.of_term pats_full in
+    let pats_partial = List.map Pattern.of_term pats_partial in
+    let multi_pats =
+      let rec aux acc other = function
+        | [] -> acc
+        | a :: l ->
+            aux
+              ( {
+                  pat = a;
+                  checks = other @ pats_partial;
+                  form = cq;
+                  eager = true;
+                }
+              :: acc )
+              (a :: other) l
+      in
+      aux [] [] pats_full
+    in
+    multi_pats
+
   let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
     let cq' = Ground.ThClosedQuantifier.sem cq in
     let tyvs = cq'.ty_vars in
@@ -294,28 +442,40 @@ module Trigger = struct
       List.filter_map
         (fun (c, (sty, st)) ->
           if Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs then
-            Some { pat = Pattern.of_term c; form = cq; eager = true }
+            Some
+              { pat = Pattern.of_term c; form = cq; eager = true; checks = [] }
           else None)
         pats
     in
     pats
 
+  let _ = compute_all_triggers
+
+  let _ = compute_top_triggers
+
   let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
 
   module EnvApps = Datastructure.Memo (F)
 
-  let env_apps =
+  let env_tri_by_apps =
     EnvApps.create
       (Context.Queue.pp ~sep:Fmt.semi pp)
-      "Quantifier.Trigger.apps" Context.Queue.create
+      "Quantifier.Trigger.tri_by_apps" Context.Queue.create
 
   let add_trigger d t =
     match t.pat with
     | Var _ -> Datastructure.Queue.push env_vars d t
-    | App (f, _, _) -> Context.Queue.push (EnvApps.find env_apps d f) t
+    | App (f, _, _) -> Context.Queue.push (EnvApps.find env_tri_by_apps d f) t
 
   let instantiate d tri subst =
-    if tri.eager then (
+    if
+      tri.eager
+      && List.for_all
+           (fun pat ->
+             try not (Node.S.is_empty (Pattern.check_term_exists d subst pat))
+             with Not_found -> false)
+           tri.checks
+    then (
       let form = Ground.ThClosedQuantifier.sem tri.form in
       Debug.dprintf4 debug "[Quant] %a instantiation found %a" Ground.Subst.pp
         subst Expr.Term.pp form.body;
@@ -669,7 +829,7 @@ let add_info_on_ground_terms d thg =
       tys = Ground.Ty.S.singleton g.ty;
     };
   (* Try pattern from the start *)
-  let trgs = Trigger.EnvApps.find Trigger.env_apps d g.app in
+  let trgs = Trigger.EnvApps.find Trigger.env_tri_by_apps d g.app in
   Context.Queue.iter (fun trg -> Trigger.match_ d trg res) trgs
 
 let init d =