From d10b5e22d9b7643c56408423d6b879d80ccd3e52 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Thu, 8 Dec 2022 11:14:57 +0100
Subject: [PATCH] [Array] Added the diff graph
---
colibri2/core/colibri2_core.mli | 1 +
colibri2/stdlib/debug.ml | 1 +
colibri2/stdlib/debug.mli | 1 +
colibri2/theories/array/array.ml | 224 ++++++++++++++++++++++++-
colibri2/theories/array/foreign_dom.ml | 9 +-
colibri2/theories/array/id_dom.ml | 70 ++++++++
colibri2/theories/array/id_dom.mli | 23 +++
7 files changed, 315 insertions(+), 14 deletions(-)
create mode 100644 colibri2/theories/array/id_dom.ml
create mode 100644 colibri2/theories/array/id_dom.mli
diff --git a/colibri2/core/colibri2_core.mli b/colibri2/core/colibri2_core.mli
index fc5121fe9..615b8ad57 100644
--- a/colibri2/core/colibri2_core.mli
+++ b/colibri2/core/colibri2_core.mli
@@ -1597,6 +1597,7 @@ module Debug : sig
val add_time_during : float stat -> (unit -> 'a) -> 'a
val incr : int stat -> unit
val decr : int stat -> unit
+ val get_stats : int stat -> int
val real_dprintf :
?nobox:unit -> ?ct:unit -> ('a, Format.formatter, unit) format -> 'a
diff --git a/colibri2/stdlib/debug.ml b/colibri2/stdlib/debug.ml
index 8ad188f34..48d750282 100644
--- a/colibri2/stdlib/debug.ml
+++ b/colibri2/stdlib/debug.ml
@@ -334,6 +334,7 @@ let register_stats_time name =
let incr r = if test_flag stats then incr r
let decr r = if test_flag stats then decr r
+let get_stats r : int = !r
let add_time_during r f =
let gettime () = (Unix.times ()).tms_utime in
diff --git a/colibri2/stdlib/debug.mli b/colibri2/stdlib/debug.mli
index cbbb37ee8..8bde3f1ca 100644
--- a/colibri2/stdlib/debug.mli
+++ b/colibri2/stdlib/debug.mli
@@ -468,5 +468,6 @@ val register_stats_int : string -> int stat
val register_stats_time : string -> float stat
val incr : int stat -> unit
val decr : int stat -> unit
+val get_stats : int stat -> int
val add_time_during : float stat -> (unit -> 'a) -> 'a
val print_stats : unit -> unit
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 71c3be7db..1cf77e893 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -21,6 +21,7 @@
open Colibri2_core
open Colibri2_popop_lib
+open Popop_stdlib
let restrict_ext =
Options.register ~pp:Fmt.bool "Array.res-ext"
@@ -38,13 +39,19 @@ let extended_comb =
Cmdliner.Arg.(
value & flag & info [ "array-ext-comb" ] ~doc:"Extended combinators")
-let extended_comb =
- Options.register ~pp:Fmt.bool "Array.res-ext"
+let blast_rule =
+ Options.register ~pp:Fmt.bool "Array.blast-rule"
Cmdliner.Arg.(
value & flag
& info [ "array-blast-rule" ]
~doc:"Use the array blast rule when it is suitable")
+let diff_graph =
+ Options.register ~pp:Fmt.bool "Array.diff-graph"
+ Cmdliner.Arg.(
+ value & flag
+ & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
+
let default_values =
Options.register ~pp:Fmt.bool "Array.def-values"
Cmdliner.Arg.(
@@ -56,6 +63,7 @@ let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
let stats = Debug.register_stats_int "Array.rule"
module NHT = Datastructure.Hashtbl (Node)
+module IHT = Datastructure.Hashtbl (DInt)
module GHT = Datastructure.Hashtbl (Ground)
module GTHT = Datastructure.Hashtbl (Ground.Ty)
@@ -128,6 +136,11 @@ let array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t = function
let node_tyl env n = Ground.Ty.S.elements (Ground.tys env n)
+let get_array_gty : Ground.Ty.t list -> Ground.Ty.t =
+ List.find (function
+ | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } -> true
+ | _ -> false)
+
module Builtin = struct
(** Additional array Builtins *)
type _ Expr.t +=
@@ -154,9 +167,9 @@ module Builtin = struct
(Expr.Ty.arrow [ b_ty ] (Expr.Ty.array ind_ty b_ty)))
let array_map : int -> Dolmen_std.Expr.term_cst =
- let cache = Popop_stdlib.DInt.H.create 13 in
+ let cache = DInt.H.create 13 in
let get_ty i =
- match Popop_stdlib.DInt.H.find cache i with
+ match DInt.H.find cache i with
| ty -> ty
| exception Not_found ->
let ty =
@@ -164,7 +177,7 @@ module Builtin = struct
(Expr.Ty.arrow (replicate i b_ty) c_ty :: replicate i array_ty_ab)
array_ty_ac
in
- Popop_stdlib.DInt.H.add cache i ty;
+ DInt.H.add cache i ty;
ty
in
fun i ->
@@ -415,7 +428,7 @@ module Theory = struct
| h :: t -> (
let tyl = node_tyl env h in
if not (tyl = []) then
- match List.hd tyl with
+ match get_array_gty tyl with
(* TODO: fix *)
| { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ] }
->
@@ -451,7 +464,7 @@ module Theory = struct
let apply_res_ext_2 env =
let apply_ext env a b =
- let gtya, gtyb = array_gty_args (List.hd (node_tyl env a)) in
+ let gtya, gtyb = array_gty_args (get_array_gty (node_tyl env a)) in
let n =
convert
~subst:
@@ -673,7 +686,7 @@ module Theory = struct
(map_pattern, map_run)
let new_map =
- let module NM = Datastructure.Memo2 (Popop_stdlib.DInt) in
+ let module NM = Datastructure.Memo2 (DInt) in
let mk_tlist l n ty =
let rec aux l n =
if n <= 0 then List.rev l
@@ -745,6 +758,197 @@ module Theory = struct
in
Egraph.register env n;
Boolean.set_true env n
+
+ module NPHT = struct
+ module NP = struct
+ module T = struct
+ type t = { id : DInt.t; node : Node.t } [@@deriving eq, ord, hash, show]
+
+ let compare { id = i1; _ } { id = i2; _ } = DInt.compare i1 i2
+ let equal { id = i1; _ } { id = i2; _ } = DInt.equal i1 i2
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let name = "Array.diff_graph.value"
+ end
+
+ open NP
+
+ module DG = struct
+ module HT = Datastructure.Hashtbl (DInt)
+
+ let diff_graph = HT.create (NP.M.pp Node.pp) "diff_graph_db"
+ let set = HT.set diff_graph
+ let find = HT.find_opt diff_graph
+ let change ~f env n = HT.change f diff_graph env n
+ let remove = HT.remove diff_graph
+ end
+
+ let get_neighbours env a = DG.find env a
+
+ let mk_eq env a b gty =
+ convert
+ ~subst:(mk_subst [ (vi, a); (vj, b) ] [ (ind_ty_var, gty) ])
+ env (Expr.Term.eq ti tj)
+
+ let rm_edge env { id; node } knp rnp k =
+ DG.change env id ~f:(function
+ | None ->
+ failwith
+ (Format.asprintf
+ "%a is supposed to be a neighbour of %a or %a, it's neighbour \
+ map mustn't be empty"
+ Node.pp node Node.pp knp.node Node.pp rnp.node)
+ | Some m -> (
+ match NP.M.find_opt rnp m with
+ | None ->
+ failwith
+ (Format.asprintf "There is no edge from %a to the node %a."
+ Node.pp node Node.pp rnp.node)
+ | Some k' ->
+ assert (Egraph.is_equal env k k');
+ Some (NP.M.remove rnp m)))
+
+ let add_edge env { id; node } knp k =
+ DG.change env id ~f:(function
+ | None -> Some (NP.M.singleton knp k)
+ | Some m -> (
+ match NP.M.find_opt knp m with
+ | None -> Some (NP.M.add knp k m)
+ | Some k' ->
+ assert (Egraph.is_equal env k k');
+ failwith
+ (Format.asprintf "%a is already a neighbour of %a." Node.pp
+ knp.node Node.pp node)))
+
+ let eq_arrays_norm env (a : t) (b : t) =
+ Egraph.merge env a.node b.node;
+ let nid = Id_dom.get_id env a.node in
+ (* find which (node, id) pair to keep and which to remove *)
+ let knp, rnp = if nid = a.id then (a, b) else (b, a) in
+ (* get all the neighbours of a and of b *)
+ let knm, rnm =
+ match (get_neighbours env knp.id, get_neighbours env rnp.id) with
+ | Some knm, Some rnm -> (M.remove rnp knm, M.remove knp rnm)
+ | _, _ ->
+ failwith
+ (Format.asprintf
+ "Empty neighbour sets for nodes of the diffgraph which are \
+ eachother's neighbours (%a, %a)"
+ Node.pp a.node Node.pp b.node)
+ in
+ (* iterate over all the neighbours *)
+ let abns =
+ NP.M.fold2_union
+ (fun { id; node } kk_opt kr_opt acc ->
+ match (kk_opt, kr_opt) with
+ | Some k1, Some k2 ->
+ (* if a node x is a neighbour or both a un b through the edges
+ k1 and k2 (resp.) then (k1 = k2) must be set to true, and
+ only the k1 edge should be kept. It's not added to the new
+ neighbours map and it is removed from X's neighbours map. *)
+ if not (Egraph.is_equal env k1 k2) then (
+ let eqn = mk_eq env k1 k2 (List.hd (node_tyl env k1)) in
+ Egraph.register env eqn;
+ Boolean.set_true env eqn);
+ rm_edge env { id; node } knp rnp k2;
+ NP.M.add knp k1 acc
+ | None, Some k ->
+ rm_edge env { id; node } knp rnp k;
+ add_edge env { id; node } knp k;
+ NP.M.add knp k acc
+ | Some k, None -> NP.M.add knp k acc
+ | None, None ->
+ failwith
+ (Format.asprintf
+ "%a is supposed to be a neighbour of %a or %a, at least \
+ one of them must appear in its neighbours map"
+ Node.pp node Node.pp knp.node Node.pp rnp.node))
+ knm rnm NP.M.empty
+ in
+ DG.remove env rnp.id;
+ DG.change env knp.id ~f:(function
+ | None ->
+ failwith
+ (Format.asprintf "%a is not part of the diff_graph" Node.pp
+ knp.node)
+ | Some _ -> Some abns)
+
+ let insert_new_diff env a b k v =
+ let ind_gty, val_gty =
+ array_gty_args (get_array_gty (node_tyl env a.node))
+ in
+ let f idn = function
+ | None -> Some (NP.M.singleton idn k)
+ | Some m -> (
+ match NP.M.find_opt idn m with
+ | Some k' ->
+ if Egraph.is_equal env k k' then Some m
+ else
+ let kk'_eq =
+ convert
+ ~subst:
+ (mk_subst
+ [ (vi, k); (vj, k') ]
+ [ (ind_ty_var, ind_gty) ])
+ env (Expr.Term.eq ti tj)
+ in
+ Egraph.register env kk'_eq;
+ Boolean.set_true env kk'_eq;
+ Some (NP.M.add idn k m)
+ (* is this necessary or is the equality enough? *)
+ | None -> Some (NP.M.add idn k m))
+ in
+ DG.change env a.id ~f:(f b);
+ DG.change env b.id ~f:(f a);
+ let bkv_eq =
+ convert
+ ~subst:
+ (mk_subst
+ [ (va, a.node); (vk, k); (vv, v) ]
+ [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ])
+ env
+ (Expr.Term.eq (Expr.Term.Array.select ta tk) tv)
+ in
+ Egraph.register env bkv_eq;
+ Choice.register_global env
+ {
+ Choice.print_cho = "Decision on the equality of array values.";
+ Choice.prio = 1;
+ choice =
+ (fun env ->
+ match Boolean.is env bkv_eq with
+ | Some true ->
+ eq_arrays_norm env a b;
+ Choice.DecNo
+ | Some false -> Choice.DecNo
+ | None ->
+ Choice.DecTodo
+ [
+ (fun env -> Boolean.set_true env bkv_eq);
+ (fun env -> Boolean.set_false env bkv_eq);
+ ]);
+ }
+
+ let update_np_dp env a b k v =
+ let aid = Id_dom.get_id env a in
+ let bid = Id_dom.get_id env b in
+ let ind_gty, val_gty = array_gty_args (get_array_gty (node_tyl env a)) in
+ let bk =
+ convert
+ ~subst:
+ (mk_subst
+ [ (va, b); (vk, k) ]
+ [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ])
+ env
+ (Expr.Term.Array.select ta tk)
+ in
+ let ap, bp = ({ node = a; id = aid }, { node = b; id = bid }) in
+ Egraph.register env bk;
+ insert_new_diff env ap bp k v
+ end
end
let converter env (f : Ground.t) =
@@ -753,6 +957,7 @@ let converter env (f : Ground.t) =
match s.ty with
| { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ]; _ } ->
Theory.new_array env ind_gty val_gty f;
+ if Options.get env diff_graph then Id_dom.set_id env (Ground.node f);
true
| _ -> false
in
@@ -834,6 +1039,9 @@ let converter env (f : Ground.t) =
Egraph.register env a;
Egraph.register env k;
Egraph.register env v;
+ if Options.get env diff_graph then (
+ Id_dom.set_id env a;
+ Theory.NPHT.update_np_dp env (Ground.node f) a k v);
(* update of the Linearity domain *)
if Options.get env restrict_aup then
Linearity_dom.upd_dom env (Ground.node f) (Linear a);
diff --git a/colibri2/theories/array/foreign_dom.ml b/colibri2/theories/array/foreign_dom.ml
index 777dce3c6..625063d5a 100644
--- a/colibri2/theories/array/foreign_dom.ml
+++ b/colibri2/theories/array/foreign_dom.ml
@@ -25,9 +25,7 @@ open Popop_stdlib
module FVal = struct
module T = struct
- type t = IsForeign [@@deriving eq, ord, hash]
-
- let pp fmt IsForeign = Fmt.pf fmt "IsForeign"
+ type t = IsForeign [@@deriving eq, ord, hash, show]
end
include T
@@ -39,7 +37,7 @@ end
module D = struct
module Value = Value.Register (FVal)
- type t = FVal.t = IsForeign [@@deriving eq]
+ type t = FVal.t = IsForeign [@@deriving eq, show]
let is_singleton _ _ = None
@@ -51,8 +49,7 @@ module D = struct
let name = "Array.foreign"
end)
- let inter _ IsForeign IsForeign = Some IsForeign
- let pp = FVal.pp
+ let inter _ _ _ = Some IsForeign
end
include D
diff --git a/colibri2/theories/array/id_dom.ml b/colibri2/theories/array/id_dom.ml
new file mode 100644
index 000000000..da916fd06
--- /dev/null
+++ b/colibri2/theories/array/id_dom.ml
@@ -0,0 +1,70 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
+open Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+
+module IVal = struct
+ module T = struct
+ type t = DInt.t [@@deriving eq, ord, hash, show]
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let name = "Array.id.value"
+end
+
+module D = struct
+ module Value = Value.Register (IVal)
+
+ type t = DInt.t [@@deriving eq, show]
+
+ let is_singleton _ _ = None
+
+ let key =
+ Dom.Kind.create
+ (module struct
+ type nonrec t = t
+
+ let name = "Array.id"
+ end)
+
+ let inter _ v _ = Some v
+end
+
+include D
+include Dom.Lattice (D)
+
+let set_id =
+ let id_counter = Debug.register_stats_int "Array.id_counter" in
+ fun env n ->
+ match Egraph.get_dom env D.key n with
+ | Some _ -> ()
+ | None ->
+ Debug.incr id_counter;
+ set_dom env n (Debug.get_stats id_counter)
+
+let get_id env n =
+ match Egraph.get_dom env D.key n with
+ | Some id -> id
+ | None -> failwith (Format.asprintf "Array node %a has no id!" Node.pp n)
diff --git a/colibri2/theories/array/id_dom.mli b/colibri2/theories/array/id_dom.mli
new file mode 100644
index 000000000..540b97c9c
--- /dev/null
+++ b/colibri2/theories/array/id_dom.mli
@@ -0,0 +1,23 @@
+(*************************************************************************)
+(* 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 get_id : 'a Egraph.t -> Node.t -> int
+val set_id : Egraph.wt -> Node.t -> unit
--
GitLab