Skip to content
Snippets Groups Projects
Commit 99a6aaa7 authored by Hichem R. A.'s avatar Hichem R. A. Committed by Hichem R. A.
Browse files

[Array] Added memoization of some RW rules

parent 228e91d0
1 merge request!32Update ocplib-simplex, some fixes
Pipeline #55261 passed
Stage: test
    Expand all Hide whitespace changes
    Inline Side-by-side
    colibri2/theories/array/Id.ml
    + 3
    − 9
    View file @ 99a6aaa7
    ......@@ -20,19 +20,13 @@
    (*************************************************************************)
    module Array = Common.MkIdDom (struct
    let n1 = "Array.Id.Array.merge_hooks"
    let n2 = "Array.Id"
    let n3 = "Array.Id.Array.new_id_hooks"
    let name = "Array.Id"
    end)
    module Index = Common.MkIdDom (struct
    let n1 = "Array.Id.Index.merge_hooks"
    let n2 = "Array.Index_id"
    let n3 = "Array.Id.Index.new_id_hooks"
    let name = "Array.Index.Id"
    end)
    module Value = Common.MkIdDom (struct
    let n1 = "Array.Id.Value.merge_hooks"
    let n2 = "Array.Value_id"
    let n3 = "Array.Id.Value.new_id_hooks"
    let name = "Array.Value.Id"
    end)
    colibri2/theories/array/RWRules.ml
    + 270
    − 137
    View file @ 99a6aaa7
    ......@@ -27,6 +27,63 @@ open Colibri2_theories_quantifiers
    module GHT = Datastructure.Hashtbl (Ground)
    module GTHT = Datastructure.Hashtbl (Ground.Ty)
    (** disjunction 1: (a,b,i,j) -> (i = j) \/ (a[j] = b[j]) *)
    module D1db =
    SHT
    (struct
    include I4
    let sort (a, b, i, j, ty1, ty2) =
    let a, b = if a <= b then (a, b) else (b, a) in
    let i, j = if i <= j then (i, j) else (j, i) in
    (a, b, i, j, ty1, ty2)
    end)
    (struct
    type t = unit
    let name = "D1db"
    let pp = Pp.unit
    end)
    (** disjunction 2: (a,b) -> (a = b) ⋁ (a[k] ≠ b[k]) *)
    module D2db =
    SHT
    (struct
    include I2
    let sort (a, b, ty1, ty2) =
    let a, b = if a <= b then (a, b) else (b, a) in
    (a, b, ty1, ty2)
    end)
    (struct
    type t = unit
    let name = "D2db"
    let pp = Pp.unit
    end)
    let get_ss_nodes env (subst : Ground.Subst.t) =
    let b_n = Expr.Term.Var.M.find STV.vb subst.term in
    let i_n = Expr.Term.Var.M.find STV.vi subst.term in
    let j_n = Expr.Term.Var.M.find STV.vj subst.term in
    let ind_gty = Expr.Ty.Var.M.find STV.ind_ty_var subst.ty in
    let val_gty = Expr.Ty.Var.M.find STV.val_ty_var subst.ty in
    let a_n =
    try Expr.Term.Var.M.find STV.va subst.term
    with Not_found ->
    let v_n = Expr.Term.Var.M.find STV.vv subst.term in
    ground_apply env Expr.Term.Const.Array.store [ ind_gty; val_gty ]
    [ b_n; i_n; v_n ]
    in
    (a_n, b_n, i_n, j_n, ind_gty, val_gty)
    (* let get_ext_nodes (subst : Ground.Subst.t) =
    let a_n = Expr.Term.Var.M.find STV.va subst.term in
    let b_n = Expr.Term.Var.M.find STV.vb subst.term in
    let ind_gty = Expr.Ty.Var.M.find STV.ind_ty_var subst.ty in
    let val_gty = Expr.Ty.Var.M.find STV.val_ty_var subst.ty in
    (a_n, b_n, ind_gty, val_gty) *)
    type size = Inf | Finite of { num : int; size : int } [@@deriving show]
    let check_gty_num_size =
    ......@@ -52,24 +109,40 @@ let check_gty_num_size =
    (* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
    let adown_pattern, adown_run =
    let a = mk_store_term STV.tb STV.ti STV.tv in
    let term = mk_select_term a STV.tj in
    (* (a,b,i,j) *)
    let a_term = mk_store_term STV.tb STV.ti STV.tv in
    let term = mk_select_term a_term STV.tj in
    let adown_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
    let adown_run env subst =
    Debug.dprintf2 debug "Found adown with %a" Ground.Subst.pp subst;
    let n = convert ~subst env term in
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq (mk_select_term a STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Egraph.register env n;
    Egraph.register env v;
    Boolean.set_true env v
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
    match
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
    with
    | Some () -> ()
    | None | (exception NoIdFound _) ->
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq
    (mk_select_term a_term STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Egraph.register env v;
    Boolean.set_true env v;
    Id.Array.set_id env a_n;
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
    in
    (adown_pattern, adown_run)
    ......@@ -85,19 +158,36 @@ let aup_pattern, aup_run =
    let aup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
    let aup_run_bis env subst_bis =
    let subst = Ground.Subst.distinct_union subst_bis subst in
    (* (a,b,i,j) *)
    Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst;
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq
    (mk_select_term term STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Egraph.register env v;
    Boolean.set_true env v
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
    match
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
    with
    | Some () -> ()
    | None | (exception NoIdFound _) ->
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq
    (mk_select_term term STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Egraph.register env v;
    Boolean.set_true env v;
    Id.Array.set_id env a_n;
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
    in
    InvertedPath.add_callback env aup_pattern_bis aup_run_bis
    in
    ......@@ -105,6 +195,7 @@ let aup_pattern, aup_run =
    (* ⇑ᵣ: a ≡ b[i <- v], b[j], b ∈ non-linear |> (i = j) \/ a[j] = b[j] *)
    let raup_pattern, raup_run =
    (* (a,b,i,j) *)
    let term = mk_store_term STV.tb STV.ti STV.tv in
    let raup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
    let raup_run env subst =
    ......@@ -116,25 +207,41 @@ let raup_pattern, raup_run =
    let raup_run_bis env subst_bis =
    let subst = Ground.Subst.distinct_union subst_bis subst in
    Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
    let bn = convert ~subst env STV.tb in
    match Egraph.get_dom env Linearity_dom.key bn with
    | Some NonLinear ->
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq
    (mk_select_term term STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Debug.dprintf2 debug "Apply raup2: set %a to true" Node.pp v;
    Egraph.register env v;
    Boolean.set_true env v
    | _ ->
    Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear"
    Node.pp bn
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
    match
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
    with
    | Some () -> ()
    | None | (exception NoIdFound _) -> (
    let bn = convert ~subst env STV.tb in
    match Egraph.get_dom env Linearity_dom.key bn with
    | Some NonLinear ->
    let v =
    convert ~subst env
    (Expr.Term._or
    [
    Expr.Term.eq STV.ti STV.tj;
    Expr.Term.eq
    (mk_select_term term STV.tj)
    (mk_select_term STV.tb STV.tj);
    ])
    in
    Debug.dprintf2 debug "Apply raup2: set %a to true" Node.pp v;
    Egraph.register env v;
    Boolean.set_true env v;
    Id.Array.set_id env a_n;
    let a_id = Id.Array.get_id env a_n in
    let b_id = Id.Array.get_id env b_n in
    let i_id = Id.Index.get_id env i_n in
    let j_id = Id.Index.get_id env j_n in
    D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
    | _ ->
    Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear"
    Node.pp bn)
    in
    InvertedPath.add_callback env raup_pattern_bis raup_run_bis
    in
    ......@@ -152,84 +259,93 @@ let const_read_pattern, const_read_run =
    in
    (const_read_pattern, const_read_run)
    let apply_res_ext_1_1_aux _env ind_gty val_gty l tyvt =
    let apply_res_ext_1_1_aux env ind_gty val_gty l =
    Debug.dprintf2 debug "Application of the res-ext-1-1 rule on %a"
    (Fmt.list ~sep:Fmt.comma Node.pp)
    l;
    let rec aux tnl =
    match tnl with
    | (nterm, _) :: t ->
    let nterms =
    List.fold_left
    (fun acc (oterm, _) -> distinct_arrays_term nterm oterm :: acc)
    [] t
    in
    List.rev_append nterms (aux t)
    | [] -> []
    in
    let _, tsubst, tnl =
    List.fold_left
    (fun (cnt, tsubst, tns) node ->
    let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
    let anvt = Expr.Term.of_var anv in
    (cnt + 1, (anv, node) :: tsubst, (anvt, node) :: tns))
    (0, [], []) l
    let rec aux l =
    match l with
    | [] -> ()
    | n1 :: t ->
    List.iter
    (fun n2 ->
    (* (a,b) *)
    let id1 = Id.Array.get_id env n1 in
    let id2 = Id.Array.get_id env n2 in
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
    | Some () -> ()
    | None ->
    let diseq = mk_distinct_arrays env n1 n2 ind_gty val_gty in
    Egraph.register env diseq;
    Boolean.set_true env diseq;
    D2db.set env (id1, id2, ind_gty, val_gty) ())
    t;
    aux t
    in
    let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
    let subst = mk_subst tsubst tysubst in
    (aux tnl, subst)
    aux l
    let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
    let apply_res_ext_1_2_aux env ind_gty val_gty l =
    Debug.dprintf2 debug "Application of the res-ext-1-2 rule on %a"
    (Fmt.list ~sep:Fmt.comma Node.pp)
    l;
    let rec aux (tnl : (Expr.term * int) list) =
    match tnl with
    | (nterm, idn) :: t -> (
    match WEGraph.WEG.find_opt env idn with
    let rec aux2 l =
    match l with
    | [] -> ()
    | (n1, id1) :: t -> (
    match WEGraph.WEG.find_opt env id1 with
    | None -> aux2 t
    | Some (_, m) ->
    let nterms =
    List.fold_left
    (fun acc (oterm, oid) ->
    if DInt.M.mem oid m then
    distinct_arrays_term nterm oterm :: acc
    else acc)
    [] t
    in
    List.rev_append nterms (aux t)
    | None -> aux t)
    | [] -> []
    List.iter
    (fun (n2, id2) ->
    if DInt.M.mem id2 m then
    (* (a,b) *)
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
    | Some () -> ()
    | None ->
    let diseq =
    mk_distinct_arrays env n1 n2 ind_gty val_gty
    in
    Egraph.register env diseq;
    Boolean.set_true env diseq;
    D2db.set env (id1, id2, ind_gty, val_gty) ())
    t)
    in
    let _, tsubst, tnl =
    List.fold_left
    (fun (cnt, tsubst, tns) node ->
    let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
    let anvt = Expr.Term.of_var anv in
    (cnt + 1, (anv, node) :: tsubst, (anvt, Id.Array.get_id env node) :: tns))
    (0, [], []) l
    let rec aux1 l =
    match l with
    | [] -> ()
    | n1 :: t -> (
    let id1 = Id.Array.get_id env n1 in
    match WEGraph.WEG.find_opt env id1 with
    | Some (_, m) ->
    let t' =
    List.rev_map
    (fun n2 ->
    let id2 = Id.Array.get_id env n2 in
    (if DInt.M.mem id2 m then
    (* (a,b) *)
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
    | Some () -> ()
    | None ->
    let diseq =
    mk_distinct_arrays env n1 n2 ind_gty val_gty
    in
    Egraph.register env diseq;
    Boolean.set_true env diseq;
    D2db.set env (id1, id2, ind_gty, val_gty) ());
    (n2, id2))
    t
    in
    aux2 t'
    | None -> aux1 t)
    in
    let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
    let subst = mk_subst tsubst tysubst in
    (aux tnl, subst)
    aux1 l
    (* (a = b) ≡ false |> (a[k] ≠ b[k]) *)
    let apply_res_ext_1_1, apply_res_ext_1_2 =
    let apply_res_ext_1 f env s =
    let l = Node.S.elements s in
    match get_array_gty_args env (List.hd l) with
    | ind_gty, val_gty -> (
    let tyvt = Expr.Ty.array STV.ind_ty STV.val_ty in
    let l, subst = f env ind_gty val_gty l tyvt in
    match l with
    | [] -> ()
    | [ t ] ->
    let n = convert ~subst env t in
    Egraph.register env n;
    Boolean.set_true env n
    | l ->
    let n = convert ~subst env (Expr.Term._and l) in
    Egraph.register env n;
    Boolean.set_true env n)
    | ind_gty, val_gty -> f env ind_gty val_gty l
    | exception Not_An_Array _ -> ()
    in
    let apply_res_ext_1_1 = apply_res_ext_1 apply_res_ext_1_1_aux in
    ......@@ -248,34 +364,38 @@ let get_foreign_neighbours env a arr_set =
    else acc)
    arr_set Node.S.empty
    let apply_ext env a b =
    let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
    let eq = Equality.equality env [ a; b ] in
    let diseq = mk_distinct_arrays env a b ind_gty val_gty in
    Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
    Node.pp a Node.pp b;
    Egraph.register env eq;
    Egraph.register env diseq;
    Choice.register_global env
    {
    print_cho = "Decision from extensionality application.";
    prio = 1;
    choice =
    (fun env ->
    match (Boolean.is env eq, Boolean.is env diseq) with
    | Some true, _ -> DecNo
    | _, Some true -> DecNo
    | _ ->
    DecTodo
    [
    (fun env ->
    Boolean.set_true env eq;
    Boolean.set_false env diseq);
    (fun env ->
    Boolean.set_false env eq;
    Boolean.set_true env diseq);
    ]);
    }
    let apply_ext env (a, id1) (b, id2) ind_gty val_gty =
    (* (a,b) *)
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
    | Some () -> ()
    | None ->
    let eq = Equality.equality env [ a; b ] in
    let diseq = mk_distinct_arrays env a b ind_gty val_gty in
    Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
    Node.pp a Node.pp b;
    Egraph.register env eq;
    Egraph.register env diseq;
    Choice.register_global env
    {
    print_cho = "Decision from extensionality application.";
    prio = 1;
    choice =
    (fun env ->
    match (Boolean.is env eq, Boolean.is env diseq) with
    | Some true, _ -> DecNo
    | _, Some true -> DecNo
    | _ ->
    DecTodo
    [
    (fun env ->
    Boolean.set_true env eq;
    Boolean.set_false env diseq);
    (fun env ->
    Boolean.set_false env eq;
    Boolean.set_true env diseq);
    ]);
    };
    D2db.set env (id1, id2, ind_gty, val_gty) ()
    (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
    let apply_res_ext_2_1, apply_res_ext_2_2 =
    ......@@ -300,14 +420,27 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
    let apply_res_ext_2_1 env aty a =
    Debug.dprintf2 debug "Application of the res-ext-2-1 rule on %a" Node.pp a;
    apply_res_ext_2
    (fun env a fa_set -> Node.S.iter (apply_ext env a) fa_set)
    (fun env a fa_set ->
    let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
    let id1 = Id.Array.get_id env a in
    Node.S.iter
    (fun b ->
    let id2 = Id.Array.get_id env b in
    apply_ext env (a, id1) (b, id2) ind_gty val_gty)
    fa_set)
    env aty a
    in
    let apply_res_ext_2_2 env aty a =
    Debug.dprintf2 debug "Application of the res-ext-2-2 rule on %a" Node.pp a;
    apply_res_ext_2
    (fun env a fa_set ->
    Node.S.iter (apply_ext env a) (get_foreign_neighbours env a fa_set))
    let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
    let id1 = Id.Array.get_id env a in
    Node.S.iter
    (fun b ->
    let id2 = Id.Array.get_id env b in
    apply_ext env (a, id1) (b, id2) ind_gty val_gty)
    (get_foreign_neighbours env a fa_set))
    env aty a
    in
    (apply_res_ext_2_1, apply_res_ext_2_2)
    ......
    colibri2/theories/array/WEGraph.ml
    + 92
    − 116
    View file @ 99a6aaa7
    This diff is collapsed.
    colibri2/theories/array/common.ml
    + 123
    − 42
    View file @ 99a6aaa7
    ......@@ -81,6 +81,29 @@ exception NoIdFound of string * Node.t
    exception Not_a_neighbour of (Node.t * Node.t * Node.t)
    exception Empty_neighbour_set of (Node.t * Node.t * Node.t)
    let () =
    Printexc.register_printer (function
    | Not_An_Array n -> Some (Fmt.str "%a is not an array!" Node.pp n)
    | Not_An_Array_gty gty ->
    Some (Fmt.str "%a is not an array ground type!" Ground.Ty.pp gty)
    | Not_An_Array_ty ty ->
    Some (Fmt.str "%a is not an array type!" Expr.Ty.pp ty)
    | Type_Not_Set n ->
    Some (Fmt.str "the type of the node %a was not set!" Node.pp n)
    | NoIdFound (s, n) ->
    Some (Fmt.str "get_id(%s) of %a: No Id found!" s Node.pp n)
    | Not_a_neighbour (kn, rn, k) ->
    Some
    (Fmt.str "%a was expected to be a neighbour of %a through %a" Node.pp
    rn Node.pp kn Node.pp k)
    | Empty_neighbour_set (kn, rn, k) ->
    Some
    (Fmt.str
    "%a was expected to be a neighbour of %a through %a, but %a's \
    neighbour set is empty"
    Node.pp rn Node.pp kn Node.pp k Node.pp kn)
    | _ -> None)
    module STV = struct
    let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
    let val_ty_var = Expr.Ty.Var.mk "val_ty"
    ......@@ -351,16 +374,16 @@ let do_mk_eq_if_neq env a b =
    if not (Egraph.is_equal env a b) then do_mk_eq env a b
    module type HTS = sig
    type key
    type t
    val set : Egraph.wt -> int -> t -> unit
    val find : Egraph.wt -> int -> t
    val find_opt : Egraph.wt -> int -> t option
    val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
    val remove : Egraph.wt -> int -> unit
    val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
    val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
    val filter_map_inplace : (int -> t -> t option) -> 'a Egraph.t -> unit
    val set : Egraph.wt -> key -> t -> unit
    val find : Egraph.wt -> key -> t
    val find_opt : Egraph.wt -> key -> t option
    val change : f:(t option -> t option) -> Egraph.wt -> key -> unit
    val remove : Egraph.wt -> key -> unit
    val iter : f:(key -> t -> unit) -> Egraph.wt -> unit
    val fold : (key -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
    val pp : Format.formatter -> Egraph.wt -> unit
    end
    ......@@ -369,7 +392,8 @@ module MkIHT (V : sig
    val pp : t Pp.pp
    val name : string
    end) : HTS with type t = V.t = struct
    end) : HTS with type key = int and type t = V.t = struct
    type key = int
    type t = V.t
    let db = HT.create V.pp V.name
    ......@@ -380,7 +404,6 @@ end) : HTS with type t = V.t = struct
    let remove (env : Egraph.wt) i = HT.remove db env i
    let iter = HT.iter db
    let fold f env acc = HT.fold f db env acc
    let filter_map_inplace f env = HT.filter_map_inplace f db env
    let pp fmt env =
    Fmt.pf fmt "%s:[%a]" V.name
    ......@@ -402,35 +425,13 @@ module type IdDomSig = sig
    val get_id : Egraph.wt -> Node.t -> int
    end
    let () =
    Printexc.register_printer (function
    | Not_An_Array n -> Some (Fmt.str "%a is not an array!" Node.pp n)
    | Not_An_Array_gty gty ->
    Some (Fmt.str "%a is not an array ground type!" Ground.Ty.pp gty)
    | Not_An_Array_ty ty ->
    Some (Fmt.str "%a is not an array type!" Expr.Ty.pp ty)
    | Type_Not_Set n ->
    Some (Fmt.str "the type of the node %a was not set!" Node.pp n)
    | NoIdFound (s, n) ->
    Some (Fmt.str "get_id(%s) of %a: No Id found!" s Node.pp n)
    | Not_a_neighbour (kn, rn, k) ->
    Some
    (Fmt.str "%a was expected to be a neighbour of %a through %a" Node.pp
    rn Node.pp kn Node.pp k)
    | Empty_neighbour_set (kn, rn, k) ->
    Some
    (Fmt.str
    "%a was expected to be a neighbour of %a through %a, but %a's \
    neighbour set is empty"
    Node.pp rn Node.pp kn Node.pp k Node.pp kn)
    | _ -> None)
    (** Global Id counter *)
    let id_counter = ref 0
    module MkIdDom (N : sig
    val n1 : string
    val n2 : string
    val n3 : string
    val name : string
    end) : IdDomSig = struct
    let merge_hooks = Datastructure.Push.create Fmt.nop N.n1
    let merge_hooks = Datastructure.Push.create Fmt.nop (N.name ^ ".merge_hooks")
    let register_merge_hook env (f : Egraph.wt -> 'a -> 'a -> bool -> unit) =
    Datastructure.Push.push merge_hooks env f
    ......@@ -448,7 +449,7 @@ end) : IdDomSig = struct
    (module struct
    type nonrec t = t
    let name = N.n2
    let name = N.name ^ ".DOM"
    end)
    let inter _ v _ = Some v
    ......@@ -469,28 +470,108 @@ end) : IdDomSig = struct
    end
    let () = Dom.register (module D)
    let new_id_hooks = Datastructure.Push.create Fmt.nop N.n3
    let new_id_hooks = Datastructure.Push.create Fmt.nop (N.name ^ ".new_id_hooks")
    let register_new_id_hook env (f : Egraph.wt -> int -> Node.t -> unit) =
    Datastructure.Push.push new_id_hooks env f
    let set_id, get_id =
    let id_counter = ref 0 in
    let set_id env n =
    match Egraph.get_dom env D.key n with
    | None ->
    incr id_counter;
    Debug.dprintf4 debug "set_id(%s) of %a: none -> %d" N.n2 Node.pp n
    Debug.dprintf4 debug "set_id(%s) of %a: none -> %d" N.name Node.pp n
    !id_counter;
    D.set_dom env n !id_counter;
    Datastructure.Push.iter new_id_hooks env ~f:(fun new_id_hook ->
    new_id_hook env !id_counter n)
    | Some id -> Debug.dprintf4 debug "set_id(%s) of %a: %d" N.n2 Node.pp n id
    | Some id ->
    Debug.dprintf4 debug "set_id(%s) of %a: %d" N.name Node.pp n id
    in
    let get_id env n =
    match Egraph.get_dom env D.key n with
    | Some id -> id
    | None -> raise (NoIdFound (N.n2, n))
    | None -> raise (NoIdFound (N.name, n))
    in
    (set_id, get_id)
    end
    module SHT (K : sig
    include Datatype
    val sort : t -> t
    val pp : t Pp.pp
    end) (V : sig
    type t
    val name : string
    val pp : t Pp.pp
    end) : HTS with type key = K.t and type t = V.t = struct
    type key = K.t
    type t = V.t
    module HT = Datastructure.Hashtbl (K)
    let db = HT.create V.pp V.name
    let aux f env k = f db env (K.sort k)
    let remove = aux HT.remove
    let set = aux HT.set
    let find = aux HT.find
    let find_opt = aux HT.find_opt
    let mem = aux HT.mem
    let change ~f = aux (HT.change f)
    let iter = HT.iter db
    let fold f env acc = HT.fold f db env acc
    let pp fmt env =
    Fmt.pf fmt "%s:[%a]" V.name
    (fun fmt () ->
    iter env ~f:(fun i v -> Fmt.pf fmt "(%a -> %a);@ " K.pp i V.pp v))
    ()
    end
    module I4 = struct
    module T = struct
    type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    [@@deriving eq, ord, hash, show]
    end
    include T
    include MkDatatype (T)
    end
    module I3 = struct
    module T = struct
    type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    [@@deriving eq, ord, hash, show]
    end
    include T
    include MkDatatype (T)
    end
    module I2 = struct
    module T = struct
    type t = DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    [@@deriving eq, ord, hash, show]
    end
    include T
    include MkDatatype (T)
    end
    module I1 = struct
    module T = struct
    type t = DInt.t * Ground.Ty.t * Ground.Ty.t [@@deriving eq, ord, hash, show]
    end
    include T
    include MkDatatype (T)
    end
    (* (id1,id2,id3,id4,ty1,ty2) *)
    (* (id1,id2,ty1,ty2) *)
    (* id1 -> (id2,id3,id4,ty1,ty2) *)
    (* id1 -> (id2,ty1,ty2) *)
    colibri2/theories/array/common.mli
    + 36
    − 13
    View file @ 99a6aaa7
    ......@@ -19,6 +19,9 @@
    (* for more details (enclosed in the file licenses/LGPLv2.1). *)
    (*************************************************************************)
    open Colibri2_popop_lib
    open Popop_stdlib
    val no_wegraph : bool Options.t
    val no_res_ext : bool Options.t
    val no_res_aup : bool Options.t
    ......@@ -140,25 +143,25 @@ val do_mk_eq : Egraph.wt -> Node.t -> Node.t -> unit
    val do_mk_eq_if_neq : Egraph.wt -> Node.t -> Node.t -> unit
    module type HTS = sig
    type key
    type t
    val set : Egraph.wt -> int -> t -> unit
    val find : Egraph.wt -> int -> t
    val find_opt : Egraph.wt -> int -> t option
    val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
    val remove : Egraph.wt -> int -> unit
    val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
    val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
    val filter_map_inplace : (int -> t -> t option) -> 'a Egraph.t -> unit
    val set : Egraph.wt -> key -> t -> unit
    val find : Egraph.wt -> key -> t
    val find_opt : Egraph.wt -> key -> t option
    val change : f:(t option -> t option) -> Egraph.wt -> key -> unit
    val remove : Egraph.wt -> key -> unit
    val iter : f:(key -> t -> unit) -> Egraph.wt -> unit
    val fold : (key -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
    val pp : Format.formatter -> Egraph.wt -> unit
    end
    module MkIHT (V : sig
    type t
    val pp : t Colibri2_popop_lib.Pp.pp
    val pp : t Pp.pp
    val name : string
    end) : HTS with type t = V.t
    end) : HTS with type key = int and type t = V.t
    module type IdDomSig = sig
    val register_merge_hook :
    ......@@ -174,7 +177,27 @@ module type IdDomSig = sig
    end
    module MkIdDom (_ : sig
    val n1 : string
    val n2 : string
    val n3 : string
    val name : string
    end) : IdDomSig
    module SHT (K : sig
    include Datatype
    val sort : t -> t
    val pp : t Pp.pp
    end) (V : sig
    type t
    val name : string
    val pp : t Pp.pp
    end) : HTS with type key = K.t and type t = V.t
    module I4 :
    Datatype
    with type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    module I3 :
    Datatype with type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    module I2 : Datatype with type t = DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    module I1 : Datatype with type t = DInt.t * Ground.Ty.t * Ground.Ty.t
    0% or .
    You are about to add 0 people to the discussion. Proceed with caution.
    Finish editing this message first!
    Please register or to comment