updated HGraph

This commit is contained in:
Simon Cruanes 2013-12-01 22:49:05 +01:00
parent 396a1779bf
commit aeaedd049a
2 changed files with 168 additions and 198 deletions

283
hGraph.ml
View file

@ -36,68 +36,52 @@ module type S = sig
(** Constants. Those are what can annotate hyperedges or make single, (** Constants. Those are what can annotate hyperedges or make single,
leaf, nodes. *) leaf, nodes. *)
type data
(** Additional data carried by the hypergraph elements *)
type t type t
(** An element of the hypergraph. It can be parametrized by a ['a option] (** An hypergraph. It stores a set of edges, and possibly inherits from
additional data (use 'a = unit if you don't care). *) another graph. *)
val eq : t -> t -> bool type edge
(** Structural equality of the two edges *) (** A single edge of the hypergraph. *)
val hash : t -> int val self : t -> edge
(** Hash, used for hashtables *) (** The edge that represents (reifies) the hypergraph itself *)
val id : t -> int val eq : edge -> edge -> bool
(** Same as {!hash}, but guarantees that the int is actually unique. *) (** Equality of the two edges. *)
val cmp : t -> t -> int val arity : edge -> int
(** Arbitrary total order *) (** Number of sub-elements of the edge (how many other edges it connects
together) *)
val data : t -> data option val nth : edge -> int -> edge
(** Data contained in this edge, if any *)
val const : t -> const
(** Constant that annotates this hyperedge. *)
val arity : t -> int
(** Number of sub-elements *)
val nth : t -> int -> t
(** [nth x i] accesses the [i]-th sub-node of [x]. (** [nth x i] accesses the [i]-th sub-node of [x].
@raise Invalid_argument if [i >= arity x]. *) @raise Invalid_argument if [i >= arity x]. *)
val sub : t -> t array val make_graph : ?parent:t -> unit -> t
(** Access the sub-nodes as an array. This array {b MUST NOT} be modified (** New graph, possibly inheriting from another graph. *)
by the caller. *)
val make : ?data:data -> const -> t array -> t val make_edge : t -> edge array -> edge
(** Create a new hyperedge from a constant that annotates it, and (** Create a new hyperedge from an ordered tuple of sub-edges.
an ordered tuple of sub-edges. The edge belongs to the given graph.
@param data optional data to decorate the edge. *) The array must not be used afterwards and must not be empty.
@raise Invalid_argument if the array is empty *)
val make_l : ?data:data -> const -> t list -> t val make_const : t -> const -> edge
(** From a list, same as {!make} otherwise *) (** Constant edge, without sub-edges *)
val const : ?data:data -> const -> t val fresh : t -> edge
(** Constant node *) (** Fresh edge, without constant. It is equal to no other edge. *)
val update : ?data:data -> t -> t array -> t module EdgeTbl : Hashtbl.S with type key = edge
(** [update e sub] creates an hyperedge equivalent to [e] in all ways,
but with the given sub-nodes as sub-edges. The array's ownership
is lost by the caller.
@param data optional data that annotates the new edge. val pp : ?printed:unit EdgeTbl.t ->
*) Buffer.t -> edge -> unit
(** Print the edge on the buffer. @param printed: sub-edges already
val pp : Buffer.t -> t -> unit printed. *)
(** Print itself (non-recursively) on the buffer *)
end end
module type PARAM = sig module type PARAM = sig
type const type const
type data
val eq : const -> const -> bool val eq : const -> const -> bool
val hash : const -> int val hash : const -> int
@ -106,124 +90,129 @@ end
module Make(P : PARAM) = struct module Make(P : PARAM) = struct
type const = P.const type const = P.const
type data = P.data
type t = { type edge =
head : const; | Fresh of int
data : data option; | Const of const
sub : t array; | Edge of edge array
mutable id : int;
mutable backref : t Weak.t;
}
type edge = t let rec eq e1 e2 = match e1, e2 with
| Fresh _, Fresh _ -> e1 == e2
| Const c1, Const c2 -> P.eq c1 c2
| Edge a1, Edge a2 ->
Array.length a1 = Array.length a2 &&
begin try
for i = 0 to Array.length a1 - 1 do
if not (eq (Array.unsafe_get a1 i) (Array.unsafe_get a2 i))
then raise Exit;
done; true
with Exit -> false
end
| _ -> false
let eq t1 t2 = t1.id = t2.id let rec hash e = match e with
| Fresh i -> i
let hash t = t.id | Const c -> P.hash c
| Edge a ->
let id t = t.id let h = ref 0 in
for i = 0 to Array.length a - 1 do
let cmp t1 t2 = t1.id - t2.id h := max_int land (!h * 65599 + (hash (Array.unsafe_get a i)))
let data t = t.data
let const t = t.head
let arity t = Array.length t.sub
let nth t i = t.sub.(i)
let sub t = t.sub
(* add a backref from [a] to [b]. *)
let _add_backref a b =
let n = Weak.length a.backref in
let arr = a.backref in
try
for i = 0 to n-1 do
if not (Weak.check arr i)
then begin (* insert here *)
Weak.set arr i (Some b);
raise Exit;
end
done; done;
(* no insertion possible: resize *) !h
a.backref <- Weak.create (2 * n);
Weak.blit arr 0 a.backref 0 n;
Weak.set a.backref n (Some b)
with Exit -> ()
(* structural equality on top-level *) (* hashtable on edges *)
let _eq_top t1 t2 = module EdgeTbl = Hashtbl.Make(struct
Array.length t1.sub = Array.length t2.sub &&
P.eq t1.head t2.head &&
try
for i = 0 to Array.length t1.sub - 1 do
if not (eq (Array.unsafe_get t1.sub i) (Array.unsafe_get t2.sub i)) then raise Exit;
done; true
with Exit -> false
(* top-level hashing *)
let _hash_top t =
let h = ref (P.hash t.head) in
for i = 0 to Array.length t.sub - 1 do
h := max_int land (!h * 65599 + (hash (Array.unsafe_get t.sub i)))
done;
!h
(* hashconsing weak table *)
module H = Weak.Make(struct
type t = edge type t = edge
let equal = _eq_top let equal = eq
let hash = _hash_top let hash = hash
end) end)
let __count = ref 0 (* hashtable on edges * int *)
let __table = H.create 2045 module BackTbl = Hashtbl.Make(struct
type t = edge * int
let equal (e1, i1) (e2, i2) = i1 = i2 && eq e1 e2
let hash (e, i) = i * 65599 + hash e
end)
let make ?data head sub = (** Hypergraph: set of edges. We map each edge to other edges that point
let my_t = { to it (knowing which ones it points to is trivial) *)
head; type t = {
data; edges : unit EdgeTbl.t;
sub; backref : edge BackTbl.t;
id = ~-1; parent : t option;
backref = Weak.create 0; mutable count : int; (* used for Fresh nodes *)
self : edge;
}
let arity e = match e with
| Fresh _
| Const _ -> 0
| Edge a -> Array.length a
let nth e i = match e with
| Fresh _
| Const _ -> raise (Invalid_argument"HGraph.nth")
| Edge a -> a.(i)
let self g = g.self
let make_graph ?parent () =
let g = {
parent;
edges = EdgeTbl.create 15;
backref = BackTbl.create 15;
count = 1;
self = Fresh 0;
} in } in
let t = H.merge __table my_t in g
if t == my_t then begin
(* hashconsing tag *)
assert (t.id = ~-1);
t.id <- !__count;
incr __count;
(* make a proper backref array *)
t.backref <- Weak.create 5;
(* add oneself to sub-nodes' backref arrays *)
Array.iter (fun t' -> _add_backref t' t) sub
end;
t
let make_l ?data head sub = make ?data head (Array.of_list sub) (* add a backref from [e]'s sub-edges to [e] *)
let _add_backrefs g e = match e with
| Fresh _
| Const _ -> assert false
| Edge a ->
for i = 0 to Array.length a - 1 do
BackTbl.add g.backref (Array.unsafe_get a i, i) e
done
let const ?data head = make ?data head [| |] let make_edge g sub =
if Array.length sub = 0 then raise (Invalid_argument "HGraph.make_edge");
let e = Edge sub in
(* add edge if not already present *)
if not (EdgeTbl.mem g.edges e) then begin
EdgeTbl.add g.edges e ();
_add_backrefs g e
end;
e
let update ?data t sub' = make ?data t.head sub' let make_const g c =
let e = Const c in
if not (EdgeTbl.mem g.edges e) then
EdgeTbl.add g.edges e ();
e
let pp buf e = let fresh g =
Buffer.add_string buf (string_of_int e.id); let e = Fresh g.count in
Buffer.add_char buf ':'; g.count <- g.count + 1;
if arity e = 0 (* always new! *)
then Buffer.add_string buf (P.to_string e.head) EdgeTbl.add g.edges e ();
else begin e
Buffer.add_char buf '(';
Buffer.add_string buf (P.to_string e.head); let pp ?(printed=EdgeTbl.create 7) buf e =
Array.iteri let rec pp buf e = match e with
(fun i sub -> | Fresh i -> Printf.bprintf buf "_e%d" i
if i > 0 then Buffer.add_char buf ' '; | Const c -> Buffer.add_string buf (P.to_string c)
Buffer.add_string buf (string_of_int sub.id)) | Edge a ->
e.sub; if not (EdgeTbl.mem printed e) then begin
Buffer.add_char buf ')' EdgeTbl.add printed e ();
Buffer.add_char buf '[';
for i = 0 to Array.length a - 1 do
if i > 0 then Buffer.add_char buf ' ';
pp buf a.(i)
done
end end
in
pp buf e
end end
(** {2 Useful default} *) (** {2 Useful default} *)

View file

@ -27,8 +27,7 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
(** {2 Hypergraph Representation} (** {2 Hypergraph Representation}
Generalized Hypergraphs. Objects are either constants, or hyperedges that Generalized Hypergraphs. Objects are either constants, or hyperedges that
connect [n] other objets together (a [n]-tuple). Each hyperedge can contain connect [n] other objets together (a [n]-tuple).
additional data.
Hashconsing is used to ensure that structural equality implies physical Hashconsing is used to ensure that structural equality implies physical
equality. This makes this module non thread safe. equality. This makes this module non thread safe.
@ -39,75 +38,59 @@ module type S = sig
(** Constants. Those are what can annotate hyperedges or make single, (** Constants. Those are what can annotate hyperedges or make single,
leaf, nodes. *) leaf, nodes. *)
type data
(** Additional data carried by the hypergraph elements *)
type t type t
(** An element of the hypergraph. It can be parametrized by a ['a option] (** An hypergraph. It stores a set of edges, and possibly inherits from
additional data (use 'a = unit if you don't care). *) another graph. *)
val eq : t -> t -> bool type edge
(** Structural equality of the two edges *) (** A single edge of the hypergraph. *)
val hash : t -> int val self : t -> edge
(** Hash, used for hashtables *) (** The edge that represents (reifies) the hypergraph itself *)
val id : t -> int val eq : edge -> edge -> bool
(** Same as {!hash}, but guarantees that the int is actually unique. *) (** Equality of the two edges. *)
val cmp : t -> t -> int val arity : edge -> int
(** Arbitrary total order *) (** Number of sub-elements of the edge (how many other edges it connects
together) *)
val data : t -> data option val nth : edge -> int -> edge
(** Data contained in this edge, if any *)
val const : t -> const
(** Constant that annotates this hyperedge. *)
val arity : t -> int
(** Number of sub-elements *)
val nth : t -> int -> t
(** [nth x i] accesses the [i]-th sub-node of [x]. (** [nth x i] accesses the [i]-th sub-node of [x].
@raise Invalid_argument if [i >= arity x]. *) @raise Invalid_argument if [i >= arity x]. *)
val sub : t -> t array val make_graph : ?parent:t -> unit -> t
(** Access the sub-nodes as an array. This array {b MUST NOT} be modified (** New graph, possibly inheriting from another graph. *)
by the caller. *)
val make : ?data:data -> const -> t array -> t val make_edge : t -> edge array -> edge
(** Create a new hyperedge from a constant that annotates it, and (** Create a new hyperedge from an ordered tuple of sub-edges.
an ordered tuple of sub-edges. The edge belongs to the given graph.
@param data optional data to decorate the edge. *) The array must not be used afterwards and must not be empty.
@raise Invalid_argument if the array is empty *)
val make_l : ?data:data -> const -> t list -> t val make_const : t -> const -> edge
(** From a list, same as {!make} otherwise *) (** Constant edge, without sub-edges *)
val const : ?data:data -> const -> t val fresh : t -> edge
(** Constant node *) (** Fresh edge, without constant. It is equal to no other edge. *)
val update : ?data:data -> t -> t array -> t module EdgeTbl : Hashtbl.S with type key = edge
(** [update e sub] creates an hyperedge equivalent to [e] in all ways,
but with the given sub-nodes as sub-edges. The array's ownership
is lost by the caller.
@param data optional data that annotates the new edge. val pp : ?printed:unit EdgeTbl.t ->
*) Buffer.t -> edge -> unit
(** Print the edge on the buffer. @param printed: sub-edges already
val pp : Buffer.t -> t -> unit printed. *)
(** Print itself (non-recursively) on the buffer *)
end end
module type PARAM = sig module type PARAM = sig
type const type const
type data
val eq : const -> const -> bool val eq : const -> const -> bool
val hash : const -> int val hash : const -> int
val to_string : const -> string (* for printing *) val to_string : const -> string (* for printing *)
end end
module Make(P : PARAM) : S with type const = P.const and type data = P.data module Make(P : PARAM) : S with type const = P.const
(** {2 Useful default} *) (** {2 Useful default} *)
@ -116,12 +99,10 @@ module DefaultParam : sig
| S of string | S of string
| I of int | I of int
type data = unit include PARAM with type const := const
include PARAM with type const := const and type data := data
val i : int -> const val i : int -> const
val s : string -> const val s : string -> const
end end
module Default : S with type const = DefaultParam.const and type data = DefaultParam.data module Default : S with type const = DefaultParam.const