diff --git a/src_colibri2/theories/quantifier/F.ml b/src_colibri2/theories/quantifier/F.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5808c457a971f835439327de691ea08d85f10171
--- /dev/null
+++ b/src_colibri2/theories/quantifier/F.ml
@@ -0,0 +1,2 @@
+include Expr.Term.Const
+module EnvApps = Datastructure.Memo (Expr.Term.Const)
diff --git a/src_colibri2/theories/quantifier/F_Pos.ml b/src_colibri2/theories/quantifier/F_Pos.ml
new file mode 100644
index 0000000000000000000000000000000000000000..129677c36ef3b8d9b3d1814504ae94f3a6be1722
--- /dev/null
+++ b/src_colibri2/theories/quantifier/F_Pos.ml
@@ -0,0 +1,13 @@
+open Colibri2_popop_lib
+(** A position inside a function symbol *)
+
+module T = struct
+ let hash_fold_int = Base.hash_fold_int
+
+ type t = { f : F.t; pos : int } [@@deriving eq, ord, hash]
+
+ let pp fmt { f; pos } = Format.fprintf fmt "%a.%i" F.pp f pos
+end
+
+include T
+include Popop_stdlib.MkDatatype (T)
diff --git a/src_colibri2/theories/quantifier/F_Pos.mli b/src_colibri2/theories/quantifier/F_Pos.mli
new file mode 100644
index 0000000000000000000000000000000000000000..147e5028a5b0f1c5dfa9e808e40a55323364fa3d
--- /dev/null
+++ b/src_colibri2/theories/quantifier/F_Pos.mli
@@ -0,0 +1,5 @@
+(** A position inside a function symbol *)
+
+type t = { f : F.t; pos : int }
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b4c195a3f6b0aac87e4490652cc87a8b7310c626
--- /dev/null
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -0,0 +1,161 @@
+open Colibri2_popop_lib
+open Common
+
+(**
+ 1) match the subterm
+ 2) possible patterns found
+ 3) GoUp and match other arguments
+ 4) goto 2)
+ *)
+
+type t' = {
+ matches : t Pattern.M.t;
+ triggers : Trigger.t list;
+ ups :
+ (Expr.Ty.t list * Pattern.t list * int (* from which argument we come *) * t)
+ list
+ F_Pos.M.t;
+}
+
+and t = t' Context.Ref.t [@@deriving show]
+
+let create creator =
+ Context.Ref.create creator
+ { matches = Pattern.M.empty; triggers = []; ups = F_Pos.M.empty }
+
+let rec exec d acc substs n ip =
+ Debug.dprintf5 debug_full "[Quant] Exec: %a, %a[%i]" Node.pp n
+ Ground.Subst.S.pp substs
+ (Ground.Subst.S.cardinal substs);
+ (* pp ip; *)
+ if Ground.Subst.S.is_empty substs then acc
+ else
+ let ip = Context.Ref.get ip in
+ let acc =
+ List.fold_left
+ (fun acc tr ->
+ Trigger.M.add_change (fun s -> s) Ground.Subst.S.union tr substs acc)
+ acc ip.triggers
+ in
+ let acc =
+ Pattern.M.fold_left
+ (fun acc p ip ->
+ Debug.dprintf2 debug_full "[Quant] Exec match %a" Pattern.pp p;
+ let substs = Pattern.match_term d substs n p in
+ exec d acc substs n ip)
+ acc ip.matches
+ in
+ let acc =
+ let match_one_app (ptyl, pargs, pos, t) acc g =
+ let { Ground.Term.tyargs = tyl; args; _ } = Ground.sem g in
+ let substs = List.fold_left2 Pattern.match_ty substs tyl ptyl in
+ let substs =
+ if Ground.Subst.S.is_empty substs then substs
+ else
+ let i = ref (-1) in
+ Base.List.fold2_exn args pargs ~init:substs
+ ~f:(fun substs args parg ->
+ incr i;
+ if Int.equal !i pos then substs
+ else Pattern.match_term d substs args parg)
+ in
+ exec d acc substs (Ground.node g) t
+ in
+ let info =
+ Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n)
+ in
+ match info with
+ | None -> acc (* a class without term associated, can't be matched *)
+ | Some info ->
+ let forall_triplets parents acc pt =
+ Ground.S.fold_left (match_one_app pt) acc parents
+ in
+ let forall_fpos acc p ptl =
+ Debug.dprintf2 debug_full "[Quant] Exec ups %a@." F_Pos.pp p;
+ let parents = F_Pos.M.find_def Ground.S.empty p info.parents in
+ List.fold_left (forall_triplets parents) acc ptl
+ in
+ F_Pos.M.fold_left forall_fpos acc ip.ups
+ in
+ acc
+
+module HPC = Datastructure.Memo (PC)
+module HPP = Datastructure.Memo (PP)
+module HPT = Datastructure.Memo (F_Pos)
+
+(** parent-child, wait for a subterm with the right application *)
+let pc_ips = HPC.create Fmt.nop "Quantifier.pc" create
+
+(** parent-parent, a variable appears two times *)
+let pp_ips = HPP.create Fmt.nop "Quantifier.pp" create
+
+(** parent-type, wait for a type to match a variable *)
+let pt_ips = HPT.create Fmt.nop "Quantifier.pt" Context.Queue.create
+
+let add_pattern pat ip =
+ Context.Ref.set ip
+ @@
+ let ip = Context.Ref.get ip in
+ { ip with triggers = pat :: ip.triggers }
+
+let add_match pat ipr =
+ let ip = Context.Ref.get ipr in
+ match Pattern.M.find_opt pat ip.matches with
+ | Some ip' -> ip'
+ | None ->
+ let ip' = create (Context.Ref.creator ipr) in
+ Context.Ref.set ipr
+ @@ { ip with matches = Pattern.M.add pat ip' ip.matches };
+ ip'
+
+let add_up f_pos tytl tl ipr =
+ let ip = Context.Ref.get ipr in
+ let ip' = create (Context.Ref.creator ipr) in
+ Context.Ref.set ipr
+ @@ {
+ ip with
+ ups =
+ F_Pos.M.add_change Lists.singleton Lists.add f_pos
+ (tytl, tl, f_pos.pos, ip') ip.ups;
+ };
+ ip'
+
+let insert_pattern d (trigger : Trigger.t) =
+ let rec aux (fp : F_Pos.t) pp_vars p =
+ match p with
+ | Pattern.Var v ->
+ let pairs = Expr.Term.Var.M.find_def [] v pp_vars in
+ let pairs =
+ List.filter
+ (fun pp ->
+ (* possible just parent1 only one path is needed by pairs *)
+ F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
+ pairs
+ in
+ let ips = List.map (fun pp -> HPP.find pp_ips d pp) pairs in
+ let ip = create (Egraph.context d) in
+ Context.Queue.push (HPT.find pt_ips d fp) (v.ty, ip);
+ let ips = ip :: ips in
+ let ips = List.map (add_match p) ips in
+ ips
+ | App (f, tytl, tl) ->
+ let ips = insert_children pp_vars f tytl tl in
+ let ip = HPC.find pc_ips d PC.{ parent = fp; child = f } in
+ let ip = add_match p ip in
+ let ips = ip :: ips in
+ ips
+ and insert_children pp_vars f tytl tl =
+ List.foldi
+ (fun acc pos p ->
+ let f_pos = F_Pos.{ f; pos } in
+ let ips = aux f_pos pp_vars p in
+ let ips = List.map (add_up f_pos tytl tl) ips in
+ ips @ acc)
+ [] tl
+ in
+ let pp_vars = Pattern.get_pps trigger.pat in
+ match trigger.pat with
+ | Var _ -> ()
+ | App (f, tytl, tl) ->
+ let ips = insert_children pp_vars f tytl tl in
+ List.iter (add_pattern trigger) ips
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
new file mode 100644
index 0000000000000000000000000000000000000000..d53db87e94bd983e32e9d9fcb702b0f9e000639f
--- /dev/null
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -0,0 +1,36 @@
+type t
+(** An InvertedPath is a way to go from one subterm of patterns to substitution
+ of triggers. It allows to know which nodes merge can create new substitutions
+ for a pattern and how to find them. Cf Efficient E-matching + modifications *)
+
+val pp : t Fmt.t
+
+val exec :
+ Egraph.t ->
+ Ground.Subst.S.t Trigger.M.t ->
+ Ground.Subst.S.t ->
+ Node.t ->
+ t ->
+ Ground.Subst.S.t Trigger.M.t
+(** [exec d acc substs n ip] adds to [acc] new substitutions to the triggers
+ that are obtained by the execution of the invertedpath *)
+
+val insert_pattern : Egraph.t -> Trigger.t -> unit
+(** [insert_pattern d tri] insert the pattern in the database of inverted path
+ for all its subterms *)
+
+module HPP : Datastructure.Sig3 with type key := PP.t
+
+val pp_ips : t HPP.t
+(** The database of inverted path for each parent-parent pairs *)
+
+module HPC : Datastructure.Sig3 with type key := PC.t
+
+val pc_ips : t HPC.t
+(** The database of inverted path for each parent-child pairs *)
+
+module HPT : Datastructure.Sig3 with type key := F_Pos.t
+
+val pt_ips : (Ty.t * t) Context.Queue.t HPT.t
+(** The database of inverted path for each parent-type, needed for polymorphic
+ variables *)
diff --git a/src_colibri2/theories/quantifier/PC.ml b/src_colibri2/theories/quantifier/PC.ml
new file mode 100644
index 0000000000000000000000000000000000000000..485fa19fa739a844853c088ef1f88068c238b7ae
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PC.ml
@@ -0,0 +1,11 @@
+open Colibri2_popop_lib
+
+module T = struct
+ open! Base
+
+ type t = { parent : F_Pos.t; child : F.t }
+ [@@deriving show, ord, hash, show, eq]
+end
+
+include T
+include Popop_stdlib.MkDatatype (T)
diff --git a/src_colibri2/theories/quantifier/PC.mli b/src_colibri2/theories/quantifier/PC.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f6c39f6f0cd9609dfb88e94812f6be59255c4803
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PC.mli
@@ -0,0 +1,3 @@
+type t = { parent : F_Pos.t; child : F.t }
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/PP.ml b/src_colibri2/theories/quantifier/PP.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1cebebf12219c955ffd0c8db6ce61a86358d9a2e
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PP.ml
@@ -0,0 +1,15 @@
+open Colibri2_popop_lib
+
+module T = struct
+ open! Base
+
+ type t = { parent1 : F_Pos.t; parent2 : F_Pos.t }
+ [@@deriving show, ord, hash, show, eq]
+end
+
+include T
+include Popop_stdlib.MkDatatype (T)
+
+let create p1 p2 =
+ if F_Pos.compare p1 p2 <= 0 then { parent1 = p1; parent2 = p2 }
+ else { parent1 = p1; parent2 = p2 }
diff --git a/src_colibri2/theories/quantifier/PP.mli b/src_colibri2/theories/quantifier/PP.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3302a3c13bfa8ae939ea5f0d7672e103defdf366
--- /dev/null
+++ b/src_colibri2/theories/quantifier/PP.mli
@@ -0,0 +1,5 @@
+type t = private { parent1 : F_Pos.t; parent2 : F_Pos.t }
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+val create : F_Pos.t -> F_Pos.t -> t
diff --git a/src_colibri2/theories/quantifier/common.ml b/src_colibri2/theories/quantifier/common.ml
new file mode 100644
index 0000000000000000000000000000000000000000..694237dad67d2ad624c69dbdda3297947169d63b
--- /dev/null
+++ b/src_colibri2/theories/quantifier/common.ml
@@ -0,0 +1,12 @@
+open Colibri2_popop_lib
+
+let debug =
+ Debug.register_info_flag ~desc:"Handling of quantifiers" "quantifiers"
+
+let debug_full =
+ Debug.register_flag ~desc:"Handling of quantifiers full" "quantifiers.full"
+
+let nb_instantiation = Debug.register_stats_int ~name:"instantiation" ~init:0
+
+let nb_new_instantiation =
+ Debug.register_stats_int ~name:"new_instantiation" ~init:0
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
new file mode 100644
index 0000000000000000000000000000000000000000..60b1d78ec9f4bb26a41bc80f351b02b9ef06024e
--- /dev/null
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -0,0 +1,27 @@
+(** information added on nodes *)
+
+type t = {
+ parents : Ground.S.t F_Pos.M.t; (** parents *)
+ apps : Ground.S.t F.M.t; (** parent parent *)
+ tys : Ground.Ty.S.t;
+}
+[@@deriving show]
+
+let _ = pp
+
+let merge info info' =
+ {
+ parents =
+ F_Pos.M.union
+ (fun _ a b -> Some (Ground.S.union a b))
+ info.parents info'.parents;
+ apps =
+ F.M.union (fun _ a b -> Some (Ground.S.union a b)) info.apps info'.apps;
+ tys = Ground.Ty.S.union info.tys info'.tys;
+ }
+
+let empty =
+ { parents = F_Pos.M.empty; apps = F.M.empty; tys = Ground.Ty.S.empty }
+
+let env =
+ Datastructure.HNode.create (Fmt.nop : t Format.printer) "Quantifier.info"
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
new file mode 100644
index 0000000000000000000000000000000000000000..00bca883795271a5798f5b4c90783a2159c099a1
--- /dev/null
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -0,0 +1,268 @@
+open Colibri2_popop_lib
+open Common
+
+(** Patterns *)
+
+module T = struct
+ open Base
+
+ type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
+ [@@deriving eq, ord, hash]
+
+ let rec pp fmt = function
+ | Var v -> Expr.Term.Var.pp fmt v
+ | App (f, tyl, tl) ->
+ Fmt.pf fmt "%a[%a](%a)" F.pp f
+ Fmt.(list ~sep:comma Expr.Ty.pp)
+ tyl
+ Fmt.(list ~sep:comma pp)
+ tl
+end
+
+include T
+include Popop_stdlib.MkDatatype (T)
+
+let rec of_term (t : Expr.Term.t) =
+ match t.descr with
+ | Var v -> Var v
+ | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term a
+ | App (f, tys, tl) -> App (f, tys, List.map of_term tl)
+ | _ -> (* absurd *) assert false
+
+let init = Ground.Subst.S.singleton Ground.Subst.empty
+
+let rec match_ty substs (ty : Ground.Ty.t) (p : Expr.Ty.t) : Ground.Subst.S.t =
+ match p.descr with
+ | Var v ->
+ Ground.Subst.S.fold_left
+ (fun acc subst ->
+ match Expr.Ty.Var.M.find v subst.ty with
+ | exception Not_found ->
+ Ground.Subst.S.add
+ { subst with ty = Expr.Ty.Var.M.add v ty subst.ty }
+ acc
+ | ty' ->
+ if Ground.Ty.equal ty ty' then Ground.Subst.S.add subst acc
+ else acc)
+ Ground.Subst.S.empty substs
+ | App (cst', tyl') ->
+ if Expr.Ty.Const.equal ty.app cst' then
+ List.fold_left2 match_ty substs ty.args tyl'
+ else Ground.Subst.S.empty
+
+let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
+ Ground.Subst.S.t =
+ Debug.dprintf4 debug "[Quant] matching %a %a" pp p Node.pp n;
+ if Ground.Subst.S.is_empty substs then substs
+ else
+ match p with
+ | Var v ->
+ let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
+ Debug.dprintf4 debug "[Quant] match_ty %a %a" Expr.Ty.pp v.ty
+ Ground.Ty.pp ty;
+ Ground.Subst.S.union (match_ty substs ty v.ty) acc
+ in
+ let substs =
+ match Datastructure.HNode.find_opt Info.env d n with
+ | None -> Ground.Subst.S.empty
+ | Some info ->
+ Ground.Ty.S.fold_left match_ty Ground.Subst.S.empty info.tys
+ in
+ Ground.Subst.S.fold_left
+ (fun acc subst ->
+ match Expr.Term.Var.M.find v subst.term with
+ | exception Not_found ->
+ Ground.Subst.S.add
+ { subst with term = Expr.Term.Var.M.add v n subst.term }
+ acc
+ | n' ->
+ if Egraph.is_equal d n n' then Ground.Subst.S.add subst acc
+ else acc)
+ Ground.Subst.S.empty substs
+ | 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.fold_left
+ (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 substs tyl ptyl in
+ if Ground.Subst.S.is_empty substs then acc
+ else
+ let substs =
+ Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+ in
+ 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, ptyl, 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 ->
+ if List.for_all2 (check_ty subst) (Ground.sem g).tyargs ptyl
+ then Node.S.add (Ground.node g) acc
+ else 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
+ | Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
+ | App (f, _, tl) ->
+ List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
+ in
+ let m =
+ match pattern with
+ | Var _ -> Expr.Term.Var.M.empty
+ | App (f, _, tl) ->
+ List.foldi
+ (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
+ Expr.Term.Var.M.empty tl
+ in
+ Expr.Term.Var.M.map
+ (fun s ->
+ let l = F_Pos.S.elements s in
+ Lists.fold_product
+ (fun acc parents1 parents2 ->
+ if F_Pos.equal parents1 parents2 then acc
+ else PP.create parents1 parents2 :: acc)
+ [] l l)
+ m
+
+let env_ground_by_apps =
+ F.EnvApps.create
+ (Context.Queue.pp ~sep:Fmt.semi Ground.pp)
+ "Quantifier.Trigger.ground_by_apps" Context.Queue.create
+
+module EnvTy = Datastructure.Memo (Ground.Ty)
+
+let env_node_by_ty =
+ EnvTy.create
+ (Context.Queue.pp ~sep:Fmt.semi Node.pp)
+ "Quantifier.Trigger.node_by_ty" Context.Queue.create
+
+let match_any_term d (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
+ if Ground.Subst.S.is_empty substs then acc
+ else
+ Ground.Subst.S.fold_left
+ (fun acc subst ->
+ Context.Queue.fold
+ (fun acc n ->
+ Ground.Subst.S.add
+ { subst with term = Expr.Term.Var.M.add v n subst.term }
+ acc)
+ acc q)
+ acc substs)
+ env_node_by_ty d Ground.Subst.S.empty
+ | App (pf, ptyl, pargs) ->
+ Context.Queue.fold
+ (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 =
+ Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
+ in
+ Ground.Subst.S.union substs acc)
+ Ground.Subst.S.empty
+ (F.EnvApps.find env_ground_by_apps d pf)
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf9565f7df0f2ee5b8a6f2d449fad08836a65bf2
--- /dev/null
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -0,0 +1,46 @@
+(** Pattern *)
+
+type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+val of_term : Expr.Term.t -> t
+
+val init : Ground.Subst.S.t
+(** Singleton set with the empty substitution, can be used as initial value for
+ the following function. [Ground.Subst.empty] should not be used since the
+ functions will do nothing *)
+
+val match_ty : Ground.Subst.S.t -> Ground.Ty.t -> Expr.Ty.t -> Ground.Subst.S.t
+(** [match_ty substs ty pat] match the [ty] on [pat] for each substitution of
+ [substs] *)
+
+val match_term : Egraph.t -> Ground.Subst.S.t -> Node.t -> t -> Ground.Subst.S.t
+(** [match_term d substs n pat] match the node [n] on the pattern [pat] for each
+ substitution. Each return substitution corresponds to one given as input. *)
+
+val check_ty : Ground.Subst.t -> Ground.Ty.t -> Expr.Ty.t -> bool
+(** [check_ty subst ty pat] checks that the pattern [pat] substituted by [subst]
+ is equal to ty *)
+
+val check_term : Egraph.t -> Ground.Subst.t -> Node.t -> t -> bool
+(** [check_term d subst n pat] checks the pattern [pat] subsituted by [subst] is
+ equal by congruence of [d] to [n] *)
+
+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 get_pps : t -> PP.t list Term.Var.M.t
+(** [get_pps pat] return the parent-parent pairs in [pat] for each variables *)
+
+val env_ground_by_apps : Ground.t Context.Queue.t F.EnvApps.t
+(** The set of ground terms sorted by their top function *)
+
+module EnvTy : Datastructure.Sig3 with type key := Ground.Ty.t
+
+val env_node_by_ty : Node.t Context.Queue.t EnvTy.t
+(** The set of nodes sorted by their type. A node can have multiple types *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index fcc771de8d79908cfe7017de6bcff5bc0d03231c..79e651f97b8bd96b6f44bb6b359c468d3fcb03cc 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -2,778 +2,7 @@
open Colibri2_popop_lib
open Colibri2_core
-
-module F = struct
- include Expr.Term.Const
- module EnvApps = Datastructure.Memo (Expr.Term.Const)
-end
-
-let debug =
- Debug.register_info_flag ~desc:"Handling of quantifiers" "quantifiers"
-
-let debug_full =
- Debug.register_flag ~desc:"Handling of quantifiers full" "quantifiers.full"
-
-let nb_instantiation = Debug.register_stats_int ~name:"instantiation" ~init:0
-
-let nb_new_instantiation =
- Debug.register_stats_int ~name:"new_instantiation" ~init:0
-
-(** instantiated function symbol *)
-module FA = struct
- module T = struct
- let hash_fold_list = Base.hash_fold_list
-
- type t = { tc : F.t; ta : Expr.Ty.t list } [@@deriving eq, ord, hash]
-
- let pp fmt { tc; ta } =
- Format.fprintf fmt "%a[%a]" F.pp tc (Pp.list Pp.colon Expr.Ty.pp) ta
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-end
-
-(** A position inside a function symbol *)
-module FA_Pos = struct
- module T = struct
- let hash_fold_int = Base.hash_fold_int
-
- type t = { fa : FA.t; pos : int } [@@deriving eq, ord, hash]
-
- let pp fmt { fa; pos } = Format.fprintf fmt "%a.%i" FA.pp fa pos
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-end
-
-(** A position inside a function symbol *)
-module F_Pos = struct
- module T = struct
- let hash_fold_int = Base.hash_fold_int
-
- type t = { f : F.t; pos : int } [@@deriving eq, ord, hash]
-
- let pp fmt { f; pos } = Format.fprintf fmt "%a.%i" F.pp f pos
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-end
-
-(** information added on nodes *)
-module Info = struct
- type t = {
- parents : Ground.S.t F_Pos.M.t; (** parents *)
- apps : Ground.S.t F.M.t; (** parent parent *)
- tys : Ground.Ty.S.t;
- }
- [@@deriving show]
-
- let _ = pp
-
- let merge info info' =
- {
- parents =
- F_Pos.M.union
- (fun _ a b -> Some (Ground.S.union a b))
- info.parents info'.parents;
- apps =
- F.M.union (fun _ a b -> Some (Ground.S.union a b)) info.apps info'.apps;
- tys = Ground.Ty.S.union info.tys info'.tys;
- }
-
- let empty =
- { parents = F_Pos.M.empty; apps = F.M.empty; tys = Ground.Ty.S.empty }
-
- let env =
- Datastructure.HNode.create (Fmt.nop : t Format.printer) "Quantifier.info"
-end
-
-module PC = struct
- module T = struct
- open! Base
-
- type t = { parent : F_Pos.t; child : F.t }
- [@@deriving show, ord, hash, show, eq]
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-end
-
-module PP = struct
- module T = struct
- open! Base
-
- type t = { parent1 : F_Pos.t; parent2 : F_Pos.t }
- [@@deriving show, ord, hash, show, eq]
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-
- let create p1 p2 =
- if F_Pos.compare p1 p2 <= 0 then { parent1 = p1; parent2 = p2 }
- else { parent1 = p1; parent2 = p2 }
-end
-
-module Pattern = struct
- module T = struct
- open Base
-
- type t = Var of Expr.Term.Var.t | App of F.t * Expr.Ty.t list * t list
- [@@deriving eq, ord, hash]
-
- let rec pp fmt = function
- | Var v -> Expr.Term.Var.pp fmt v
- | App (f, tyl, tl) ->
- Fmt.pf fmt "%a[%a](%a)" F.pp f
- Fmt.(list ~sep:comma Expr.Ty.pp)
- tyl
- Fmt.(list ~sep:comma pp)
- tl
- end
-
- include T
- include Popop_stdlib.MkDatatype (T)
-
- let rec of_term (t : Expr.Term.t) =
- match t.descr with
- | Var v -> Var v
- | App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term a
- | App (f, tys, tl) -> App (f, tys, List.map of_term tl)
- | _ -> (* absurd *) assert false
-
- let init = Ground.Subst.S.singleton Ground.Subst.empty
-
- let rec match_ty substs (ty : Ground.Ty.t) (p : Expr.Ty.t) : Ground.Subst.S.t
- =
- match p.descr with
- | Var v ->
- Ground.Subst.S.fold_left
- (fun acc subst ->
- match Expr.Ty.Var.M.find v subst.ty with
- | exception Not_found ->
- Ground.Subst.S.add
- { subst with ty = Expr.Ty.Var.M.add v ty subst.ty }
- acc
- | ty' ->
- if Ground.Ty.equal ty ty' then Ground.Subst.S.add subst acc
- else acc)
- Ground.Subst.S.empty substs
- | App (cst', tyl') ->
- if Expr.Ty.Const.equal ty.app cst' then
- List.fold_left2 match_ty substs ty.args tyl'
- else Ground.Subst.S.empty
-
- let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
- Ground.Subst.S.t =
- Debug.dprintf4 debug "[Quant] matching %a %a" pp p Node.pp n;
- if Ground.Subst.S.is_empty substs then substs
- else
- match p with
- | Var v ->
- let match_ty (acc : Ground.Subst.S.t) ty : Ground.Subst.S.t =
- Debug.dprintf4 debug "[Quant] match_ty %a %a" Expr.Ty.pp v.ty
- Ground.Ty.pp ty;
- Ground.Subst.S.union (match_ty substs ty v.ty) acc
- in
- let substs =
- match Datastructure.HNode.find_opt Info.env d n with
- | None -> Ground.Subst.S.empty
- | Some info ->
- Ground.Ty.S.fold_left match_ty Ground.Subst.S.empty info.tys
- in
- Ground.Subst.S.fold_left
- (fun acc subst ->
- match Expr.Term.Var.M.find v subst.term with
- | exception Not_found ->
- Ground.Subst.S.add
- { subst with term = Expr.Term.Var.M.add v n subst.term }
- acc
- | n' ->
- if Egraph.is_equal d n n' then Ground.Subst.S.add subst acc
- else acc)
- Ground.Subst.S.empty substs
- | 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.fold_left
- (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 substs tyl ptyl in
- if Ground.Subst.S.is_empty substs then acc
- else
- let substs =
- Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
- in
- 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, ptyl, 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 ->
- if List.for_all2 (check_ty subst) (Ground.sem g).tyargs ptyl
- then Node.S.add (Ground.node g) acc
- else 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
- | Var v ->
- Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
- | App (f, _, tl) ->
- List.foldi (fun acc pos p -> aux acc F_Pos.{ f; pos } p) acc tl
- in
- let m =
- match pattern with
- | Var _ -> Expr.Term.Var.M.empty
- | App (f, _, tl) ->
- List.foldi
- (fun acc pos p -> aux acc F_Pos.{ f; pos } p)
- Expr.Term.Var.M.empty tl
- in
- Expr.Term.Var.M.map
- (fun s ->
- let l = F_Pos.S.elements s in
- Lists.fold_product
- (fun acc parents1 parents2 ->
- if F_Pos.equal parents1 parents2 then acc
- else PP.create parents1 parents2 :: acc)
- [] l l)
- m
-
- let env_ground_by_apps =
- F.EnvApps.create
- (Context.Queue.pp ~sep:Fmt.semi Ground.pp)
- "Quantifier.Trigger.ground_by_apps" Context.Queue.create
-
- module EnvTy = Datastructure.Memo (Ground.Ty)
-
- let env_node_by_ty =
- EnvTy.create
- (Context.Queue.pp ~sep:Fmt.semi Node.pp)
- "Quantifier.Trigger.node_by_ty" Context.Queue.create
-
- let match_any_term d (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
- if Ground.Subst.S.is_empty substs then acc
- else
- Ground.Subst.S.fold_left
- (fun acc subst ->
- Context.Queue.fold
- (fun acc n ->
- Ground.Subst.S.add
- { subst with term = Expr.Term.Var.M.add v n subst.term }
- acc)
- acc q)
- acc substs)
- env_node_by_ty d Ground.Subst.S.empty
- | App (pf, ptyl, pargs) ->
- Context.Queue.fold
- (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 =
- Base.List.fold2_exn args pargs ~init:substs ~f:(match_term d)
- in
- Ground.Subst.S.union substs acc)
- Ground.Subst.S.empty
- (F.EnvApps.find env_ground_by_apps d pf)
-end
-
-module Trigger = struct
- module T = struct
- open! Base
-
- type t = {
- pat : Pattern.t;
- checks : Pattern.t list;
- (* list *) form : Ground.ThClosedQuantifier.t;
- eager : bool;
- }
- [@@deriving eq, ord, hash]
-
- let pp fmt t =
- Fmt.pf fmt "[%a, %a -> %a]" Pattern.pp t.pat
- Fmt.(list ~sep:comma Pattern.pp)
- t.checks Ground.ThClosedQuantifier.pp t.form
- end
-
- 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 = List.sort_uniq ~cmp:Expr.Term.compare (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 @ l @ pats_partial;
- form = cq;
- eager = true;
- }
- :: acc )
- (a :: other) l
- in
- aux [] [] pats_full
- in
- Debug.dprintf6 debug "@[pats_full:%a,@ pats_partial:%a,@ tri:%a@]@."
- Fmt.(list ~sep:comma Pattern.pp)
- pats_full
- Fmt.(list ~sep:comma Pattern.pp)
- pats_partial
- Fmt.(list ~sep:comma pp)
- multi_pats;
- multi_pats
-
- let compute_all_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 union (sty, st) = function
- | None -> None
- | Some (sty', st') ->
- Some (Expr.Ty.Var.S.union sty sty', Expr.Term.Var.S.union st st')
- in
- let add t fv pats = (t, fv) :: pats in
- let rec aux (pats, acc_fv) (t : Expr.Term.t) =
- match t.descr with
- | Var _ ->
- let fv =
- Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) t
- in
- (add t fv pats, union fv acc_fv)
- | Expr.App (_, tyl, tl) -> (
- let pats, fv =
- List.fold_left aux
- (pats, Some (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty))
- tl
- in
- match fv with
- | None -> (pats, None)
- | Some (sty, st) ->
- let fv = (List.fold_left Expr.Ty.free_vars sty tyl, st) in
- (add t fv pats, union fv acc_fv) )
- | Expr.Binder (_, _) -> (pats, None) (* todo *)
- | Expr.Match (_, _) -> (pats, None)
- (* todo *)
- in
- let pats, _ = aux ([], None) t in
- let tyvs = Expr.Ty.Var.S.of_list tyvs in
- let tvs = Expr.Term.Var.S.of_list tvs in
- let pats =
- 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; checks = [] }
- else None)
- pats
- in
- pats
-
- let _ = compute_all_triggers
-
- let _ = compute_top_triggers
-
- let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
-
- let env_tri_by_apps =
- F.EnvApps.create
- (Context.Queue.pp ~sep:Fmt.semi pp)
- "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 (F.EnvApps.find env_tri_by_apps d f) t
-
- let instantiate_aux d tri subst =
- let form = Ground.ThClosedQuantifier.sem tri.form in
- Debug.incr nb_instantiation;
- let n = Ground.convert ~subst form.body in
- if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
- Debug.incr nb_new_instantiation;
- Egraph.register d n;
- Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form)
-
- module Delayed_instantiation = struct
- type event = unit
-
- let print_event = Unit.pp
-
- let enqueue _ _ = assert false
-
- let key =
- Events.Dem.create_key
- ( module struct
- type d = t * Ground.Subst.t
-
- type t = unit
-
- let name = "delayed_instantiation"
- end )
-
- let delay = Events.LastEffort 1
-
- type runable = t * Ground.Subst.t [@@deriving show]
-
- let print_runable = pp_runable
-
- let run d (tri, subst) =
- Debug.dprintf8 debug
- "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
- subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp tri.pat
- Fmt.(list ~sep:comma Pattern.pp)
- tri.checks;
- instantiate_aux d tri subst;
- None
- end
-
- let () = Egraph.Wait.register_dem (module Delayed_instantiation)
-
- let instantiate d tri subst =
- let subst =
- {
- subst with
- Ground.Subst.term =
- Expr.Term.Var.M.map (Egraph.find_def d) subst.Ground.Subst.term;
- }
- in
- Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
- Ground.Subst.pp subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp
- tri.pat
- Fmt.(list ~sep:comma Pattern.pp)
- tri.checks;
- 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 instantiate_aux d tri subst
- else (
- Debug.dprintf0 debug "[Quant] Delayed";
- Egraph.register_delayed_event d Delayed_instantiation.key (tri, subst) )
-
- let match_ d tri n =
- Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
- let mvar = Pattern.match_term d Ground.Subst.S.empty n tri.pat in
- Ground.Subst.S.iter (fun subst -> instantiate d tri subst) mvar
-end
-
-module InvertedPath = struct
- (**
- 1) match the subterm
- 2) possible patterns found
- 3) GoUp and match other arguments
- 4) goto 2)
- *)
-
- type t' = {
- matches : t Pattern.M.t;
- triggers : Trigger.t list;
- ups :
- ( Expr.Ty.t list
- * Pattern.t list
- * int (* from which argument we come *)
- * t )
- list
- F_Pos.M.t;
- }
-
- and t = t' Context.Ref.t [@@deriving show]
-
- let _ = pp
-
- let create creator =
- Context.Ref.create creator
- { matches = Pattern.M.empty; triggers = []; ups = F_Pos.M.empty }
-
- let rec exec d acc substs n ip =
- Debug.dprintf5 debug_full "[Quant] Exec: %a, %a[%i]" Node.pp n
- Ground.Subst.S.pp substs
- (Ground.Subst.S.cardinal substs);
- (* pp ip; *)
- if Ground.Subst.S.is_empty substs then acc
- else
- let ip = Context.Ref.get ip in
- let acc =
- List.fold_left
- (fun acc tr ->
- Trigger.M.add_change (fun s -> s) Ground.Subst.S.union tr substs acc)
- acc ip.triggers
- in
- let acc =
- Pattern.M.fold_left
- (fun acc p ip ->
- Debug.dprintf2 debug_full "[Quant] Exec match %a" Pattern.pp p;
- let substs = Pattern.match_term d substs n p in
- exec d acc substs n ip)
- acc ip.matches
- in
- let acc =
- let match_one_app (ptyl, pargs, pos, t) acc g =
- let { Ground.Term.tyargs = tyl; args; _ } = Ground.sem g in
- let substs = List.fold_left2 Pattern.match_ty substs tyl ptyl in
- let substs =
- if Ground.Subst.S.is_empty substs then substs
- else
- let i = ref (-1) in
- Base.List.fold2_exn args pargs ~init:substs
- ~f:(fun substs args parg ->
- incr i;
- if Int.equal !i pos then substs
- else Pattern.match_term d substs args parg)
- in
- exec d acc substs (Ground.node g) t
- in
- let info =
- Datastructure.HNode.find_opt Info.env d (Egraph.find_def d n)
- in
- match info with
- | None -> acc (* a class without term associated, can't be matched *)
- | Some info ->
- let forall_triplets parents acc pt =
- Ground.S.fold_left (match_one_app pt) acc parents
- in
- let forall_fpos acc p ptl =
- Debug.dprintf2 debug_full "[Quant] Exec ups %a@." F_Pos.pp p;
- let parents = F_Pos.M.find_def Ground.S.empty p info.parents in
- List.fold_left (forall_triplets parents) acc ptl
- in
- F_Pos.M.fold_left forall_fpos acc ip.ups
- in
- acc
-
- module HPC = Datastructure.Memo (PC)
- module HPP = Datastructure.Memo (PP)
- module HPT = Datastructure.Memo (F_Pos)
-
- (** parent-child, wait for a subterm with the right application *)
- let pc_ips = HPC.create Fmt.nop "Quantifier.pc" create
-
- (** parent-parent, a variable appears two times *)
- let pp_ips = HPP.create Fmt.nop "Quantifier.pp" create
-
- (** parent-type, wait for a type to match a variable *)
- let pt_ips = HPT.create Fmt.nop "Quantifier.pt" Context.Queue.create
-
- let add_pattern pat ip =
- Context.Ref.set ip
- @@
- let ip = Context.Ref.get ip in
- { ip with triggers = pat :: ip.triggers }
-
- let add_match pat ipr =
- let ip = Context.Ref.get ipr in
- match Pattern.M.find_opt pat ip.matches with
- | Some ip' -> ip'
- | None ->
- let ip' = create (Context.Ref.creator ipr) in
- Context.Ref.set ipr
- @@ { ip with matches = Pattern.M.add pat ip' ip.matches };
- ip'
-
- let add_up f_pos tytl tl ipr =
- let ip = Context.Ref.get ipr in
- let ip' = create (Context.Ref.creator ipr) in
- Context.Ref.set ipr
- @@ {
- ip with
- ups =
- F_Pos.M.add_change Lists.singleton Lists.add f_pos
- (tytl, tl, f_pos.pos, ip') ip.ups;
- };
- ip'
-
- let insert_pattern d (trigger : Trigger.t) =
- let rec aux (fp : F_Pos.t) pp_vars p =
- match p with
- | Pattern.Var v ->
- let pairs = Expr.Term.Var.M.find_def [] v pp_vars in
- let pairs =
- List.filter
- (fun pp ->
- (* possible just parent1 only one path is needed by pairs *)
- F_Pos.equal fp pp.PP.parent1 || F_Pos.equal fp pp.PP.parent2)
- pairs
- in
- let ips = List.map (fun pp -> HPP.find pp_ips d pp) pairs in
- let ip = create (Egraph.context d) in
- Context.Queue.push (HPT.find pt_ips d fp) (v.ty, ip);
- let ips = ip :: ips in
- let ips = List.map (add_match p) ips in
- ips
- | App (f, tytl, tl) ->
- let ips = insert_children pp_vars f tytl tl in
- let ip = HPC.find pc_ips d PC.{ parent = fp; child = f } in
- let ip = add_match p ip in
- let ips = ip :: ips in
- ips
- and insert_children pp_vars f tytl tl =
- List.foldi
- (fun acc pos p ->
- let f_pos = F_Pos.{ f; pos } in
- let ips = aux f_pos pp_vars p in
- let ips = List.map (add_up f_pos tytl tl) ips in
- ips @ acc)
- [] tl
- in
- let pp_vars = Pattern.get_pps trigger.pat in
- match trigger.pat with
- | Var _ -> ()
- | App (f, tytl, tl) ->
- let ips = insert_children pp_vars f tytl tl in
- List.iter (add_pattern trigger) ips
-end
+open Common
let add_trigger d t =
Trigger.add_trigger d t;
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
new file mode 100644
index 0000000000000000000000000000000000000000..b83779e08e946935f2b7276524f1b29d6d5be736
--- /dev/null
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -0,0 +1,214 @@
+open Colibri2_popop_lib
+open Common
+
+module T = struct
+ open! Base
+
+ type t = {
+ pat : Pattern.t;
+ checks : Pattern.t list;
+ (* list *) form : Ground.ThClosedQuantifier.t;
+ eager : bool;
+ }
+ [@@deriving eq, ord, hash]
+
+ let pp fmt t =
+ Fmt.pf fmt "[%a, %a -> %a]" Pattern.pp t.pat
+ Fmt.(list ~sep:comma Pattern.pp)
+ t.checks Ground.ThClosedQuantifier.pp t.form
+end
+
+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 = List.sort_uniq ~cmp:Expr.Term.compare (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 @ l @ pats_partial;
+ form = cq;
+ eager = true;
+ }
+ :: acc )
+ (a :: other) l
+ in
+ aux [] [] pats_full
+ in
+ Debug.dprintf6 debug "@[pats_full:%a,@ pats_partial:%a,@ tri:%a@]@."
+ Fmt.(list ~sep:comma Pattern.pp)
+ pats_full
+ Fmt.(list ~sep:comma Pattern.pp)
+ pats_partial
+ Fmt.(list ~sep:comma pp)
+ multi_pats;
+ multi_pats
+
+let compute_all_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 union (sty, st) = function
+ | None -> None
+ | Some (sty', st') ->
+ Some (Expr.Ty.Var.S.union sty sty', Expr.Term.Var.S.union st st')
+ in
+ let add t fv pats = (t, fv) :: pats in
+ let rec aux (pats, acc_fv) (t : Expr.Term.t) =
+ match t.descr with
+ | Var _ ->
+ let fv =
+ Expr.Term.free_vars (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty) t
+ in
+ (add t fv pats, union fv acc_fv)
+ | Expr.App (_, tyl, tl) -> (
+ let pats, fv =
+ List.fold_left aux
+ (pats, Some (Expr.Ty.Var.S.empty, Expr.Term.Var.S.empty))
+ tl
+ in
+ match fv with
+ | None -> (pats, None)
+ | Some (sty, st) ->
+ let fv = (List.fold_left Expr.Ty.free_vars sty tyl, st) in
+ (add t fv pats, union fv acc_fv) )
+ | Expr.Binder (_, _) -> (pats, None) (* todo *)
+ | Expr.Match (_, _) -> (pats, None)
+ (* todo *)
+ in
+ let pats, _ = aux ([], None) t in
+ let tyvs = Expr.Ty.Var.S.of_list tyvs in
+ let tvs = Expr.Term.Var.S.of_list tvs in
+ let pats =
+ 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; checks = [] }
+ else None)
+ pats
+ in
+ pats
+
+let env_vars = Datastructure.Queue.create pp "Quantifier.Trigger.vars"
+
+let env_tri_by_apps =
+ F.EnvApps.create
+ (Context.Queue.pp ~sep:Fmt.semi pp)
+ "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 (F.EnvApps.find env_tri_by_apps d f) t
+
+let instantiate_aux d tri subst =
+ let form = Ground.ThClosedQuantifier.sem tri.form in
+ Debug.incr nb_instantiation;
+ let n = Ground.convert ~subst form.body in
+ if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
+ Debug.incr nb_new_instantiation;
+ Egraph.register d n;
+ Egraph.merge d n (Ground.ThClosedQuantifier.node tri.form)
+
+module Delayed_instantiation = struct
+ type event = unit
+
+ let print_event = Unit.pp
+
+ let enqueue _ _ = assert false
+
+ let key =
+ Events.Dem.create_key
+ ( module struct
+ type d = t * Ground.Subst.t
+
+ type t = unit
+
+ let name = "delayed_instantiation"
+ end )
+
+ let delay = Events.LastEffort 1
+
+ type runable = t * Ground.Subst.t [@@deriving show]
+
+ let print_runable = pp_runable
+
+ let run d (tri, subst) =
+ Debug.dprintf8 debug
+ "[Quant] %a delayed instantiation %a, pat %a, checks:%a" Ground.Subst.pp
+ subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp tri.pat
+ Fmt.(list ~sep:comma Pattern.pp)
+ tri.checks;
+ instantiate_aux d tri subst;
+ None
+end
+
+let () = Egraph.Wait.register_dem (module Delayed_instantiation)
+
+let instantiate d tri subst =
+ let subst =
+ {
+ subst with
+ Ground.Subst.term =
+ Expr.Term.Var.M.map (Egraph.find_def d) subst.Ground.Subst.term;
+ }
+ in
+ Debug.dprintf8 debug "[Quant] %a instantiation found %a, pat %a, checks:%a"
+ Ground.Subst.pp subst Ground.ThClosedQuantifier.pp tri.form Pattern.pp
+ tri.pat
+ Fmt.(list ~sep:comma Pattern.pp)
+ tri.checks;
+ 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 instantiate_aux d tri subst
+ else (
+ Debug.dprintf0 debug "[Quant] Delayed";
+ Egraph.register_delayed_event d Delayed_instantiation.key (tri, subst) )
+
+let match_ d tri n =
+ Debug.dprintf4 debug "[Quant] match %a %a" pp tri Node.pp n;
+ let mvar = Pattern.match_term d Ground.Subst.S.empty n tri.pat in
+ Ground.Subst.S.iter (fun subst -> instantiate d tri subst) mvar
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f1cffad60119edd3722a7759d38c383a7174dde6
--- /dev/null
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -0,0 +1,43 @@
+(** Trigger *)
+
+type t = {
+ pat : Pattern.t;
+ (** The main pattern, the one matched to obtain a complete
+ substitution *)
+ checks : Pattern.t list; (** Guards for the existence of terms *)
+ form : Ground.ThClosedQuantifier.t; (** the body of the formula *)
+ eager : bool;
+ (** If it should be eagerly applied, otherwise wait for LastEffort *)
+}
+
+include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
+
+val compute_top_triggers : Ground.ThClosedQuantifier.t -> t list
+(** Compute triggers, that should only add logical connective or equalities are
+ new terms *)
+
+val compute_all_triggers : Ground.ThClosedQuantifier.t -> t list
+(** Compute all the triggers whose patterns contain all the variables of the formula *)
+
+val env_vars : t Datastructure.Queue.t
+(** Triggers that are only variables *)
+
+val env_tri_by_apps : t Context.Queue.t F.EnvApps.t
+(** Triggers sorted by their top symbol *)
+
+val add_trigger : Egraph.t -> t -> unit
+(** Register a new trigger *)
+
+val instantiate : Egraph.t -> t -> Ground.Subst.t -> unit
+(** [instantiate d tri subst] instantiates the trigger [tri] with the
+ substitution [subst]:
+
+ * now if the trigger is eager and the checks of the trigger exists when
+ substituted by [subst]
+
+ * at last effort otherwise
+*)
+
+val match_ : Egraph.t -> t -> Node.t -> unit
+(** [match_ d tri n] match the pattern of [tri] with [n] and instantiate [tri]
+ with the resulting substitutions *)