module Place:`sig`

..`end`

This module provides operations on place graphs.

**Author(s):** Michele Sevegnani

`type `

bmatrix

The type of boolean matrices.

`type `

pg = {

` ` |
`r : ` |
`(*` |
Number of regions
| `*)` |

` ` |
`n : ` |
`(*` |
Number of nodes
| `*)` |

` ` |
`s : ` |
`(*` |
Number of sites
| `*)` |

` ` |
`rn : ` |
`(*` |
Boolean adjacency matrix regions X nodes
| `*)` |

` ` |
`rs : ` |
`(*` |
Boolean adjacency matrix regions X sites
| `*)` |

` ` |
`nn : ` |
`(*` |
Boolean adjacency matrix nodes X nodes
| `*)` |

` ` |
`ns : ` |
`(*` |
Boolean adjacency matrix nodes X sites
| `*)` |

The type of place graphs.

`val to_string : ``pg -> string`

`to_string p`

returns a string representation of place graph `p`

.`val json_of_place : ``pg -> string`

Return a JSON representation of a place graph. Example:

`"place_graph": {`

"regions": 2,

"nodes": 3,

"sites": 1,

"dag": [

{

"source": 1,

"target": 2

},

{

"source": 0,

"target": 2

}

]

}

`val json_of_place_f : ``pg -> Base.JSON.json_node`

`val edges : ``pg -> int`

Compute the number of edges in the DAG.

`val parse : ``regions:int -> nodes:int -> sites:int -> string list -> pg`

`parse r n s lines`

computes a place graph with `r`

regions, `n`

nodes and `s`

sites. Each element in `lines`

is a string in the same format of the output
of `Place.to_string`

.`Invalid_argument`

if the arguments do not specify a valid place
graph.`val get_dot : ``pg -> string * string * string * string`

`get_dot p`

returns three strings expressing place graph `p`

in dot format.
The first two elements encode regions and sites shapes, the third encodes the
node ranks and the fourth represents the adjacency matrix.`val apply : ``Iso.t -> pg -> pg`

Apply an isomorphism

`val parse_placing : ``int list list -> int -> pg`

`parse_placing l r`

returns the placing with `r`

regions defined by list `l`

in which each element is a site's parent set.`val leaves : ``pg -> IntSet.t`

Compute the set of nodes with no children.

`val orphans : ``pg -> IntSet.t`

Compute the set of nodes with no parents.

`val elementary_id : ``int -> pg`

`elementary_id m`

computes a place graph in the form of an identity of
`m`

.`val id0 : ``pg`

`id0`

is the empty place graph.`val elementary_merge : ``int -> pg`

`elementary_merge m`

computes an elementary place graph formed by one region
containing `m`

sites.`val elementary_split : ``int -> pg`

`elementary_split m`

computes an elementary place graph formed by one site
shared by `m`

regions.`val zero : ``pg`

`zero`

is the place graph formed by an orphaned site.`val one : ``pg`

`one`

is the place graph formed by an idle region.`val elementary_sym : ``int -> int -> pg`

`elementary_sym m n`

computes an place graph consisting of a symmetry
between `m`

and `n`

.`val elementary_ion : ``pg`

An ion.

`val equal_placing : ``pg -> pg -> bool`

`equal_placing a b`

returns `true`

if placings `a`

and `b`

are equal.
Inputs are assumed to be valid placing. No check is performed.`val compare_placing : ``pg -> pg -> int`

`compare_placing a b`

compares placings `a`

and `b`

.`val equal_bmatrix : ``bmatrix -> bmatrix -> bool`

Equality for

`Place.bmatrix`

.`val compare_bmatrix : ``bmatrix -> bmatrix -> int`

Comparison for

`Place.bmatrix`

.`val entries_bmatrix : ``bmatrix -> int`

Return the number of edges in a

`Place.bmatrix`

.`exception COMP_ERROR of ``(int * int)`

Raised when a composition between two incompatible place graphs is
attempted. The two integers are the number of sites and regions involved in
the composition, respectively.

`val tens : ``pg -> pg -> pg`

`tens p0 p1`

returns the tensor product of place graphs `p0`

and `p1`

.`val tens_of_list : ``pg list -> pg`

Same as

`Place.tens`

but on a list of place graphs.`val comp : ``pg -> pg -> pg`

`comp p0 p1`

returns the composition of place graphs `p0`

and `p1`

.`COMP_ERROR`

when mediating interfaces mismatch.`val is_id : ``pg -> bool`

`is_id p`

returns `true`

if place graph `p`

is an identity, `false`

otherwise.`val is_plc : ``pg -> bool`

Test for the absence of nodes.

`val is_ground : ``pg -> bool`

`is_ground p`

is `true`

if place graph `p`

has no sites, `false`

otherwise.`val is_mono : ``pg -> bool`

`is_mono p`

is `true`

if place graph `p`

is monomorphic, `false`

otherwise. A place graph is monomorphic if no two sites are siblings and no
site is an orphan.`val is_epi : ``pg -> bool`

`is_epi p`

is `true`

if place graph `p`

is epimorphic, `false`

otherwise. A
place graph is epimorphic if no root is idle and no two roots are
partners.`val is_guard : ``pg -> bool`

`is_guard p`

is `true`

if place graph `p`

is guarded, `false`

otherwise. A
place graph is guarded if no region has sites as children.`val decomp : ``target:pg ->`

pattern:pg -> Iso.t -> pg * pg * pg * Iso.t * Iso.t

`decomp t p i`

computes the decomposition of target `t`

given pattern `p`

and node isomorphism `i`

from `p`

to `t`

. Pattern `p`

is assumed epi and
mono. The result tuple `(c, id, d, iso_c, iso_d)`

is formed by context `c`

,
identity `id`

, parameter `d`

, and nodes in `c`

and `d`

expressed as rows of
`t`

.`exception NOT_PRIME`

Raised when a place graph cannot be decomposed into prime components. The
first element is a set of shared nodes and the second a set of shared
sites.

`val prime_components : ``pg -> (pg * Iso.t) list`

Compute the prime components (*i.e.* place graphs with one region) of a
place graph. The original node numbering is returned in the form of an
isomorphism.

**Raises**

`NOT_PRIME`

when some region is shared`val decomp_d : ``pg -> int -> pg * pg * Iso.t * Iso.t`

Compute the decomposition

**Raises**

`D = D' X D_id`

.`NOT_PRIME`

when some region is shared`exception NOT_TOTAL`

Raised when a node in the pattern cannot be matched to any node in the
target.

`val match_list : ``target:pg ->`

pattern:pg ->

n_t:Nodes.t ->

n_p:Nodes.t ->

(Cnf.clause * Cnf.b_clause list) list * Cnf.clause list * IntSet.t

`match_list t p n_t n_p`

computes constraints to match edges in pattern `p`

with compatible edges in target `t`

. `n_t`

and `n_p`

are the node sets of
`t`

and `p`

, respectively.`NOT_TOTAL`

when there are nodes in the pattern that cannot be
matched.`val match_leaves : ``target:pg ->`

pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t

`match_leaves t p n_t n_p`

computes constraints to match the leaves
(`p`

with those in `t`

. `n_t`

and `n_p`

are defined as in `Place.match_list`

.`NOT_TOTAL`

when there are leaves in the pattern that cannot be
matched.`val match_orphans : ``target:pg ->`

pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t

Dual of

**Raises**

`Place.match_leaves`

.`NOT_TOTAL`

when there are orphans in the pattern that cannot be matched.`val match_regions : ``target:pg ->`

pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t

Compute constraints to match regions. Arguments are as in

`Place.match_list`

. Only controls and degrees are checked.`val match_sites : ``target:pg ->`

pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t

Dual of

`Place.match_regions`

.`val match_trans : ``target:pg -> pattern:pg -> Cnf.clause list`

Compute constraints to block matches between unconnected pairs of nodes with
sites and nodes with regions.

`val check_match : ``target:pg -> pattern:pg -> bmatrix -> Iso.t -> bool`

`check_match t p trans iso`

checks if `iso`

from `p`

to `t`

is a valid match.`val match_region_nodes : ``pg -> pg -> Nodes.t -> Nodes.t -> Cnf.clause list * IntSet.t`

Compute constraints for equality: regions must have children with the same
controls.

`val match_nodes_sites : ``pg -> pg -> Nodes.t -> Nodes.t -> Cnf.clause list * IntSet.t`

Dual of

`Place.match_region_nodes`

.`val match_list_eq : ``pg ->`

pg ->

Nodes.t ->

Nodes.t -> (Cnf.clause * Cnf.b_clause list) list * Cnf.clause list * IntSet.t

Compute constraints for equality. Similar to

`Place.match_list`

.`val deg_regions : ``pg -> int list`

Compute the outer degree of the regions of a place graph.

`val deg_sites : ``pg -> int list`

Compute the inner degree of the sites of a place graph.

`val trans : ``pg -> bmatrix`

Compute the transitive closure of the nodes X nodes matrix of a place
graph.