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

[Array] Add nomalization of the memoization data structures

parent 99a6aaa7
No related branches found
No related tags found
1 merge request!32Update ocplib-simplex, some fixes
Pipeline #55286 passed
Stage: test
    Hide whitespace changes
    Inline Side-by-side
    Showing
    with 344 additions and 181 deletions
    colibri2/theories/array/RWRules.ml
    + 262
    − 161
    View file @ 5ee49bdc
    ...@@ -62,7 +62,49 @@ module D2db = ...@@ -62,7 +62,49 @@ module D2db =
    let pp = Pp.unit let pp = Pp.unit
    end) end)
    let get_ss_nodes env (subst : Ground.Subst.t) = (** (a,b,i,j):
    a -> (true,b,i,j) | b -> (false,a,i,j) |
    i -> (true,a,b,j) | j -> (false,a,b,i) *)
    module D1ids = struct
    include MkIHT (struct
    include I3.S
    let name = "D1Ids"
    end)
    let add env (id1, id2, id3, id4, ty1, ty2) =
    let aux env id v =
    change
    ~f:(function
    | Some s -> Some (I3.S.add v s) | None -> Some (I3.S.singleton v))
    env id
    in
    aux env id1 (true, id2, id3, id4, ty1, ty2);
    aux env id2 (false, id1, id3, id4, ty1, ty2);
    aux env id3 (true, id1, id2, id4, ty1, ty2);
    aux env id4 (false, id1, id2, id3, ty1, ty2)
    end
    (** (a,b): a -> (true,b) | b -> (false,a) *)
    module D2ids = struct
    include MkIHT (struct
    include I1.S
    let name = "D2Ids"
    end)
    let add env (id1, id2, ty1, ty2) =
    let aux env id v =
    change
    ~f:(function
    | Some s -> Some (I1.S.add v s) | None -> Some (I1.S.singleton v))
    env id
    in
    aux env id1 (true, id2, ty1, ty2);
    aux env id2 (false, id1, ty1, ty2)
    end
    let get_disj1_nodes env (subst : Ground.Subst.t) =
    let b_n = Expr.Term.Var.M.find STV.vb subst.term in 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 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 j_n = Expr.Term.Var.M.find STV.vj subst.term in
    ...@@ -77,12 +119,212 @@ let get_ss_nodes env (subst : Ground.Subst.t) = ...@@ -77,12 +119,212 @@ let get_ss_nodes env (subst : Ground.Subst.t) =
    in in
    (a_n, b_n, i_n, j_n, ind_gty, val_gty) (a_n, b_n, i_n, j_n, ind_gty, val_gty)
    (* let get_ext_nodes (subst : Ground.Subst.t) = let new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty =
    let a_n = Expr.Term.Var.M.find STV.va subst.term in match
    let b_n = Expr.Term.Var.M.find STV.vb subst.term in let a_id = Id.Array.get_id env a_n in
    let ind_gty = Expr.Ty.Var.M.find STV.ind_ty_var subst.ty in let b_id = Id.Array.get_id env b_n in
    let val_gty = Expr.Ty.Var.M.find STV.val_ty_var subst.ty in let i_id = Id.Index.get_id env i_n in
    (a_n, b_n, ind_gty, val_gty) *) 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 (mk_store_term STV.tb STV.ti STV.tv) 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) ();
    D1ids.add env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
    let new_disj1 env subst =
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_disj1_nodes env subst in
    new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty
    let new_disj1_raup2 env subst =
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_disj1_nodes env subst in
    match Egraph.get_dom env Linearity_dom.key b_n with
    | Some NonLinear ->
    Debug.dprintf2 debug "Apply raup2 with %a" Ground.Subst.pp subst;
    new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty
    | _ ->
    Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear" Node.pp
    b_n
    let new_dist_arrays env (a_n, a_id) (b_n, b_id) ind_gty val_gty =
    match D2db.find_opt env (a_id, b_id, ind_gty, val_gty) with
    | Some () -> ()
    | None ->
    let diseq = mk_distinct_arrays env a_n b_n ind_gty val_gty in
    Egraph.register env diseq;
    Boolean.set_true env diseq;
    D2db.set env (a_id, b_id, ind_gty, val_gty) ();
    D2ids.add env (a_id, b_id, ind_gty, val_gty)
    let new_disj2 env (a, a_id) (b, b_id) ind_gty val_gty =
    match D2db.find_opt env (a_id, b_id, 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 (a_id, b_id, ind_gty, val_gty) ();
    D2ids.add env (a_id, b_id, ind_gty, val_gty)
    let eq_arrays_norm env (_, kid) (_, rid) _ =
    (match D1ids.find_opt env rid with
    | None -> ()
    | Some s ->
    let ns =
    I3.S.fold
    (fun (b, oid, iid, jid, ty1, ty2) s ->
    let ns, (ofst, osnd, nfst, nsnd) =
    if oid = rid then
    ( I3.S.add
    (b, kid, iid, jid, ty1, ty2)
    (I3.S.remove (b, oid, iid, jid, ty1, ty2) s),
    if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
    else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
    in
    D1db.remove env (ofst, osnd, iid, jid, ty1, ty2);
    D1db.set env (nfst, nsnd, iid, jid, ty1, ty2) ();
    D1ids.change env iid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (true, nfst, nsnd, jid, ty1, ty2)
    (I3.S.remove (true, ofst, osnd, jid, ty1, ty2) s)));
    D1ids.change env jid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (false, nfst, nsnd, iid, ty1, ty2)
    (I3.S.remove (false, ofst, osnd, iid, ty1, ty2) s)));
    D1ids.change env oid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (not b, kid, iid, jid, ty1, ty2)
    (I3.S.remove (not b, rid, iid, jid, ty1, ty2) s)));
    ns)
    s s
    in
    D1ids.change env kid ~f:(function
    | None -> Some ns
    | Some s' -> Some (I3.S.union ns s')));
    (match D2ids.find_opt env rid with
    | None -> ()
    | Some s ->
    let ns =
    I1.S.fold
    (fun (b, oid, ty1, ty2) s ->
    let ns, (ofst, osnd, nfst, nsnd) =
    if oid = rid then
    ( I1.S.add (b, kid, ty1, ty2) (I1.S.remove (b, oid, ty1, ty2) s),
    if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
    else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
    in
    D2db.remove env (ofst, osnd, ty1, ty2);
    D2db.set env (nfst, nsnd, ty1, ty2) ();
    D2ids.change env oid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I1.S.add (not b, kid, ty1, ty2)
    (I1.S.remove (not b, rid, ty1, ty2) s)));
    ns)
    s s
    in
    D2ids.change env kid ~f:(function
    | None -> Some ns
    | Some s' -> Some (I1.S.union ns s')));
    D2ids.remove env rid;
    D1ids.remove env rid
    let eq_indices_norm env (_, kid) (_, rid) _ =
    (match D1ids.find_opt env rid with
    | None -> ()
    | Some s ->
    let ns =
    I3.S.fold
    (fun (b, aid, bid, oid, ty1, ty2) s ->
    let ns, (ofst, osnd, nfst, nsnd) =
    if oid = rid then
    ( I3.S.add
    (b, aid, bid, kid, ty1, ty2)
    (I3.S.remove (b, aid, bid, oid, ty1, ty2) s),
    if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
    else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
    in
    D1db.remove env (aid, bid, ofst, osnd, ty1, ty2);
    D1db.set env (aid, bid, nfst, nsnd, ty1, ty2) ();
    D1ids.change env aid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (true, bid, nfst, nsnd, ty1, ty2)
    (I3.S.remove (true, bid, ofst, osnd, ty1, ty2) s)));
    D1ids.change env bid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (false, aid, nfst, nsnd, ty1, ty2)
    (I3.S.remove (false, aid, ofst, osnd, ty1, ty2) s)));
    D1ids.change env oid ~f:(function
    | None -> assert false
    | Some s ->
    Some
    (I3.S.add
    (not b, aid, bid, kid, ty1, ty2)
    (I3.S.remove (not b, aid, bid, rid, ty1, ty2) s)));
    ();
    ns)
    s s
    in
    D1ids.change env kid ~f:(function
    | None -> Some ns
    | Some s' -> Some (I3.S.union ns s')));
    D1ids.remove env rid
    type size = Inf | Finite of { num : int; size : int } [@@deriving show] type size = Inf | Finite of { num : int; size : int } [@@deriving show]
    ...@@ -115,34 +357,7 @@ let adown_pattern, adown_run = ...@@ -115,34 +357,7 @@ let adown_pattern, adown_run =
    let adown_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in let adown_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
    let adown_run env subst = let adown_run env subst =
    Debug.dprintf2 debug "Found adown with %a" Ground.Subst.pp subst; Debug.dprintf2 debug "Found adown with %a" Ground.Subst.pp subst;
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in new_disj1 env subst
    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 in
    (adown_pattern, adown_run) (adown_pattern, adown_run)
    ...@@ -160,34 +375,7 @@ let aup_pattern, aup_run = ...@@ -160,34 +375,7 @@ let aup_pattern, aup_run =
    let subst = Ground.Subst.distinct_union subst_bis subst in let subst = Ground.Subst.distinct_union subst_bis subst in
    (* (a,b,i,j) *) (* (a,b,i,j) *)
    Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst; Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst;
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in new_disj1 env subst
    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 in
    InvertedPath.add_callback env aup_pattern_bis aup_run_bis InvertedPath.add_callback env aup_pattern_bis aup_run_bis
    in in
    ...@@ -207,41 +395,7 @@ let raup_pattern, raup_run = ...@@ -207,41 +395,7 @@ let raup_pattern, raup_run =
    let raup_run_bis env subst_bis = let raup_run_bis env subst_bis =
    let subst = Ground.Subst.distinct_union subst_bis subst in let subst = Ground.Subst.distinct_union subst_bis subst in
    Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst; Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
    let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in new_disj1_raup2 env subst
    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 in
    InvertedPath.add_callback env raup_pattern_bis raup_run_bis InvertedPath.add_callback env raup_pattern_bis raup_run_bis
    in in
    ...@@ -267,18 +421,12 @@ let apply_res_ext_1_1_aux env ind_gty val_gty l = ...@@ -267,18 +421,12 @@ let apply_res_ext_1_1_aux env ind_gty val_gty l =
    match l with match l with
    | [] -> () | [] -> ()
    | n1 :: t -> | n1 :: t ->
    let id1 = Id.Array.get_id env n1 in
    List.iter List.iter
    (fun n2 -> (fun n2 ->
    (* (a,b) *) (* (a,b) *)
    let id1 = Id.Array.get_id env n1 in
    let id2 = Id.Array.get_id env n2 in let id2 = Id.Array.get_id env n2 in
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty)
    | 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; t;
    aux t aux t
    in in
    ...@@ -299,15 +447,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l = ...@@ -299,15 +447,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l =
    (fun (n2, id2) -> (fun (n2, id2) ->
    if DInt.M.mem id2 m then if DInt.M.mem id2 m then
    (* (a,b) *) (* (a,b) *)
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty)
    | 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) t)
    in in
    let rec aux1 l = let rec aux1 l =
    ...@@ -321,17 +461,9 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l = ...@@ -321,17 +461,9 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l =
    List.rev_map List.rev_map
    (fun n2 -> (fun n2 ->
    let id2 = Id.Array.get_id env n2 in let id2 = Id.Array.get_id env n2 in
    (if DInt.M.mem id2 m then if DInt.M.mem id2 m then
    (* (a,b) *) (* (a,b) *)
    match D2db.find_opt env (id1, id2, ind_gty, val_gty) with new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty;
    | 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)) (n2, id2))
    t t
    in in
    ...@@ -364,39 +496,6 @@ let get_foreign_neighbours env a arr_set = ...@@ -364,39 +496,6 @@ let get_foreign_neighbours env a arr_set =
    else acc) else acc)
    arr_set Node.S.empty arr_set Node.S.empty
    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]) *) (* a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
    let apply_res_ext_2_1, apply_res_ext_2_2 = let apply_res_ext_2_1, apply_res_ext_2_2 =
    let foreign_array_db = GTHT.create Node.S.pp "foreign_array_db" in let foreign_array_db = GTHT.create Node.S.pp "foreign_array_db" in
    ...@@ -426,7 +525,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 = ...@@ -426,7 +525,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
    Node.S.iter Node.S.iter
    (fun b -> (fun b ->
    let id2 = Id.Array.get_id env b in let id2 = Id.Array.get_id env b in
    apply_ext env (a, id1) (b, id2) ind_gty val_gty) (* (a, b) *)
    new_disj2 env (a, id1) (b, id2) ind_gty val_gty)
    fa_set) fa_set)
    env aty a env aty a
    in in
    ...@@ -439,7 +539,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 = ...@@ -439,7 +539,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
    Node.S.iter Node.S.iter
    (fun b -> (fun b ->
    let id2 = Id.Array.get_id env b in let id2 = Id.Array.get_id env b in
    apply_ext env (a, id1) (b, id2) ind_gty val_gty) (* (a, b) *)
    new_disj2 env (a, id1) (b, id2) ind_gty val_gty)
    (get_foreign_neighbours env a fa_set)) (get_foreign_neighbours env a fa_set))
    env aty a env aty a
    in in
    ......
    colibri2/theories/array/RWRules.mli
    + 2
    − 0
    View file @ 5ee49bdc
    ...@@ -50,3 +50,5 @@ val add_array_map_hook : ...@@ -50,3 +50,5 @@ val add_array_map_hook :
    val new_map : Egraph.rw Egraph.t -> Ground.t -> unit val new_map : Egraph.rw Egraph.t -> Ground.t -> unit
    val apply_blast_rule : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit val apply_blast_rule : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit
    val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
    val eq_indices_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
    colibri2/theories/array/WEGraph.ml
    + 12
    − 12
    View file @ 5ee49bdc
    ...@@ -1209,11 +1209,11 @@ let eq_indices_norm env (_kn, kid) (rn, rid) b = ...@@ -1209,11 +1209,11 @@ let eq_indices_norm env (_kn, kid) (rn, rid) b =
    ~msg:(Fmt.str "_eq_indices_norm %a %a" (pp_nid env) kid (pp_nid env) rid) ~msg:(Fmt.str "_eq_indices_norm %a %a" (pp_nid env) kid (pp_nid env) rid)
    env () env ()
    let eq_values_norm env (_, kid) (_, rid) _b = let eq_values_norm env (_, kid) (_, rid) b =
    Debug.dprintf4 debug "WEGraph: eq_values_norm_ %a %a" (pp_nid env) kid Debug.dprintf4 debug "WEGraph: eq_values_norm_ %a %a" (pp_nid env) kid
    (pp_nid env) rid; (pp_nid env) rid;
    Values.eq_values_norm env kid rid; Values.eq_values_norm env kid rid;
    if not _b then ITN.set env kid (ITN.find env rid); if not b then ITN.set env kid (ITN.find env rid);
    ITN.remove env rid ITN.remove env rid
    let ineq_indices_norm env s = let ineq_indices_norm env s =
    ...@@ -1259,6 +1259,16 @@ let new_select env r a i = ...@@ -1259,6 +1259,16 @@ let new_select env r a i =
    | None -> () | None -> ()
    | Some v -> do_mk_eq_if_neq env v r) | Some v -> do_mk_eq_if_neq env v r)
    let new_id_hook env id n =
    WEG.set env id (DInt.M.empty, DInt.M.empty);
    ITN.set env id n
    let new_index_id_hook env id n =
    Vertices.set env id Vertex.S.empty;
    ITN.set env id n
    let new_value_id_hook env id n = ITN.set env id n
    let get_neighbours env nid = let get_neighbours env nid =
    let rec aux (k : DInt.t) inp acc = let rec aux (k : DInt.t) inp acc =
    if DInt.S.mem inp acc then acc if DInt.S.mem inp acc then acc
    ...@@ -1275,14 +1285,6 @@ let get_neighbours env nid = ...@@ -1275,14 +1285,6 @@ let get_neighbours env nid =
    | None -> DInt.S.empty | None -> DInt.S.empty
    | Some (m, _) -> DInt.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty | Some (m, _) -> DInt.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty
    let new_id_hook env id n =
    WEG.set env id (DInt.M.empty, DInt.M.empty);
    ITN.set env id n
    let new_index_id_hook env id n =
    Vertices.set env id Vertex.S.empty;
    ITN.set env id n
    let get_array_kvs env n = let get_array_kvs env n =
    match KnownValues.HT.find_opt env (Id.Array.get_id env n) with match KnownValues.HT.find_opt env (Id.Array.get_id env n) with
    | Some kv -> | Some kv ->
    ...@@ -1292,5 +1294,3 @@ let get_array_kvs env n = ...@@ -1292,5 +1294,3 @@ let get_array_kvs env n =
    Node.M.add indn v acc) Node.M.add indn v acc)
    kv Node.M.empty kv Node.M.empty
    | None -> Node.M.empty | None -> Node.M.empty
    let new_value_id_hook env id n = ITN.set env id n
    colibri2/theories/array/array.ml
    + 4
    − 4
    View file @ 5ee49bdc
    ...@@ -219,12 +219,12 @@ let init env = ...@@ -219,12 +219,12 @@ let init env =
    Ground.register_converter env converter; Ground.register_converter env converter;
    if not (Options.get env no_wegraph) then ( if not (Options.get env no_wegraph) then (
    Id.Array.register_new_id_hook env WEGraph.new_id_hook; Id.Array.register_new_id_hook env WEGraph.new_id_hook;
    Id.Array.register_merge_hook env WEGraph.eq_arrays_norm;
    Id.Index.register_new_id_hook env WEGraph.new_index_id_hook; Id.Index.register_new_id_hook env WEGraph.new_index_id_hook;
    Id.Index.register_merge_hook env WEGraph.eq_indices_norm;
    Id.Value.register_new_id_hook env WEGraph.new_value_id_hook; Id.Value.register_new_id_hook env WEGraph.new_value_id_hook;
    Id.Value.register_merge_hook env WEGraph.eq_values_norm; Id.Array.register_merge_hook env Normalization.eq_arrays_norm;
    Equality.register_hook_new_disequality env WEGraph.ineq_indices_norm); Id.Index.register_merge_hook env Normalization.eq_indices_norm;
    Id.Value.register_merge_hook env Normalization.eq_values_norm;
    Equality.register_hook_new_disequality env Normalization.ineq_indices_norm);
    (* extᵣ (restricted extensionality): (* extᵣ (restricted extensionality):
    - (a = b) ≡ false |> (a[k] ≠ b[k]) - (a = b) ≡ false |> (a[k] ≠ b[k])
    - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *) - a, b, {a,b} ⊆ foreign |> (a = b) ⋁ (a[k] ≠ b[k]) *)
    ......
    colibri2/theories/array/common.ml
    + 3
    − 2
    View file @ 5ee49bdc
    ...@@ -543,7 +543,7 @@ end ...@@ -543,7 +543,7 @@ end
    module I3 = struct module I3 = struct
    module T = struct module T = struct
    type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t type t = DBool.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    [@@deriving eq, ord, hash, show] [@@deriving eq, ord, hash, show]
    end end
    ...@@ -563,7 +563,8 @@ end ...@@ -563,7 +563,8 @@ end
    module I1 = struct module I1 = struct
    module T = struct module T = struct
    type t = DInt.t * Ground.Ty.t * Ground.Ty.t [@@deriving eq, ord, hash, show] type t = DBool.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    [@@deriving eq, ord, hash, show]
    end end
    include T include T
    ......
    colibri2/theories/array/common.mli
    + 3
    − 2
    View file @ 5ee49bdc
    ...@@ -197,7 +197,8 @@ module I4 : ...@@ -197,7 +197,8 @@ module I4 :
    with type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t with type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    module I3 : module I3 :
    Datatype with type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t Datatype
    with type t = DBool.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 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 module I1 : Datatype with type t = DBool.t * DInt.t * Ground.Ty.t * Ground.Ty.t
    colibri2/theories/array/normalization.ml 0 → 100644
    + 33
    − 0
    View file @ 5ee49bdc
    (*************************************************************************)
    (* This file is part of Colibri2. *)
    (* *)
    (* Copyright (C) 2014-2021 *)
    (* CEA (Commissariat à l'énergie atomique et aux énergies *)
    (* alternatives) *)
    (* OCamlPro *)
    (* *)
    (* you can redistribute it and/or modify it under the terms of the GNU *)
    (* Lesser General Public License as published by the Free Software *)
    (* Foundation, version 2.1. *)
    (* *)
    (* It is distributed in the hope that it will be useful, *)
    (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
    (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
    (* GNU Lesser General Public License for more details. *)
    (* *)
    (* See the GNU Lesser General Public License version 2.1 *)
    (* for more details (enclosed in the file licenses/LGPLv2.1). *)
    (*************************************************************************)
    let eq_arrays_norm env (kn, kid) (rn, rid) b =
    (* RWRules.eq_arrays_norm env (kn, kid) (rn, rid) b; *)
    WEGraph.eq_arrays_norm env (kn, kid) (rn, rid) b
    let eq_indices_norm env (kn, kid) (rn, rid) b =
    (* RWRules.eq_indices_norm env (kn, kid) (rn, rid) b; *)
    WEGraph.eq_indices_norm env (kn, kid) (rn, rid) b
    let eq_values_norm env (kn, kid) (rn, rid) b =
    WEGraph.eq_values_norm env (kn, kid) (rn, rid) b
    let ineq_indices_norm env s = WEGraph.ineq_indices_norm env s
    colibri2/theories/array/normalization.mli 0 → 100644
    + 25
    − 0
    View file @ 5ee49bdc
    (*************************************************************************)
    (* This file is part of Colibri2. *)
    (* *)
    (* Copyright (C) 2014-2021 *)
    (* CEA (Commissariat à l'énergie atomique et aux énergies *)
    (* alternatives) *)
    (* OCamlPro *)
    (* *)
    (* you can redistribute it and/or modify it under the terms of the GNU *)
    (* Lesser General Public License as published by the Free Software *)
    (* Foundation, version 2.1. *)
    (* *)
    (* It is distributed in the hope that it will be useful, *)
    (* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
    (* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
    (* GNU Lesser General Public License for more details. *)
    (* *)
    (* See the GNU Lesser General Public License version 2.1 *)
    (* for more details (enclosed in the file licenses/LGPLv2.1). *)
    (*************************************************************************)
    val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
    val eq_indices_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
    val ineq_indices_norm : Egraph.wt -> Node.S.t -> unit
    val eq_values_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
    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