2
2
* Copyright 2010 INRIA Saclay
4
* Use of this software is governed by the GNU LGPLv2.1 license
4
* Use of this software is governed by the MIT license
6
6
* Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
7
7
* Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
608
609
isl_space *dim = isl_basic_set_get_space(delta);
609
610
delta = isl_basic_set_project_out(delta,
610
611
isl_dim_param, 0, nparam);
611
delta = isl_basic_set_add(delta, isl_dim_param, nparam);
612
delta = isl_basic_set_add_dims(delta, isl_dim_param, nparam);
612
613
delta = isl_basic_set_reset_space(delta, dim);
1723
/* Structure for representing the nodes in the graph being traversed
1724
* using Tarjan's algorithm.
1725
* index represents the order in which nodes are visited.
1726
* min_index is the index of the root of a (sub)component.
1727
* on_stack indicates whether the node is currently on the stack.
1729
struct basic_map_sort_node {
1734
/* Structure for representing the graph being traversed
1735
* using Tarjan's algorithm.
1736
* len is the number of nodes
1737
* node is an array of nodes
1738
* stack contains the nodes on the path from the root to the current node
1739
* sp is the stack pointer
1740
* index is the index of the last node visited
1741
* order contains the elements of the components separated by -1
1742
* op represents the current position in order
1724
/* Structure for representing the nodes of the graph of which
1725
* strongly connected components are being computed.
1727
* list contains the actual nodes
1744
1728
* check_closed is set if we may have used the fact that
1745
1729
* a pair of basic maps can be interchanged
1747
struct basic_map_sort {
1749
struct basic_map_sort_node *node;
1731
struct isl_tc_follows_data {
1732
isl_basic_map **list;
1755
1733
int check_closed;
1758
static void basic_map_sort_free(struct basic_map_sort *s)
1768
static struct basic_map_sort *basic_map_sort_alloc(struct isl_ctx *ctx, int len)
1770
struct basic_map_sort *s;
1773
s = isl_calloc_type(ctx, struct basic_map_sort);
1777
s->node = isl_alloc_array(ctx, struct basic_map_sort_node, len);
1780
for (i = 0; i < len; ++i)
1781
s->node[i].index = -1;
1782
s->stack = isl_alloc_array(ctx, int, len);
1785
s->order = isl_alloc_array(ctx, int, 2 * len);
1793
s->check_closed = 0;
1797
basic_map_sort_free(s);
1801
1736
/* Check whether in the computation of the transitive closure
1802
* "bmap1" (R_1) should follow (or be part of the same component as)
1737
* "list[i]" (R_1) should follow (or be part of the same component as)
1805
1740
* That is check whether
1816
1751
* *check_closed is set if the subset relation holds while
1817
1752
* R_1 \circ R_2 is not empty.
1819
static int basic_map_follows(__isl_keep isl_basic_map *bmap1,
1820
__isl_keep isl_basic_map *bmap2, int *check_closed)
1754
static int basic_map_follows(int i, int j, void *user)
1756
struct isl_tc_follows_data *data = user;
1822
1757
struct isl_map *map12 = NULL;
1823
1758
struct isl_map *map21 = NULL;
1826
if (!isl_space_tuple_match(bmap1->dim, isl_dim_in, bmap2->dim, isl_dim_out))
1761
if (!isl_space_tuple_match(data->list[i]->dim, isl_dim_in,
1762
data->list[j]->dim, isl_dim_out))
1829
1765
map21 = isl_map_from_basic_map(
1830
1766
isl_basic_map_apply_range(
1831
isl_basic_map_copy(bmap2),
1832
isl_basic_map_copy(bmap1)));
1767
isl_basic_map_copy(data->list[j]),
1768
isl_basic_map_copy(data->list[i])));
1833
1769
subset = isl_map_is_empty(map21);
1834
1770
if (subset < 0)
1841
if (!isl_space_tuple_match(bmap1->dim, isl_dim_in, bmap1->dim, isl_dim_out) ||
1842
!isl_space_tuple_match(bmap2->dim, isl_dim_in, bmap2->dim, isl_dim_out)) {
1777
if (!isl_space_tuple_match(data->list[i]->dim, isl_dim_in,
1778
data->list[i]->dim, isl_dim_out) ||
1779
!isl_space_tuple_match(data->list[j]->dim, isl_dim_in,
1780
data->list[j]->dim, isl_dim_out)) {
1843
1781
isl_map_free(map21);
1847
1785
map12 = isl_map_from_basic_map(
1848
1786
isl_basic_map_apply_range(
1849
isl_basic_map_copy(bmap1),
1850
isl_basic_map_copy(bmap2)));
1787
isl_basic_map_copy(data->list[i]),
1788
isl_basic_map_copy(data->list[j])));
1852
1790
subset = isl_map_is_subset(map21, map12);
1866
/* Perform Tarjan's algorithm for computing the strongly connected components
1867
* in the graph with the disjuncts of "map" as vertices and with an
1868
* edge between any pair of disjuncts such that the first has
1869
* to be applied after the second.
1871
static int power_components_tarjan(struct basic_map_sort *s,
1872
__isl_keep isl_basic_map **list, int i)
1876
s->node[i].index = s->index;
1877
s->node[i].min_index = s->index;
1878
s->node[i].on_stack = 1;
1880
s->stack[s->sp++] = i;
1882
for (j = s->len - 1; j >= 0; --j) {
1887
if (s->node[j].index >= 0 &&
1888
(!s->node[j].on_stack ||
1889
s->node[j].index > s->node[i].min_index))
1892
f = basic_map_follows(list[i], list[j], &s->check_closed);
1898
if (s->node[j].index < 0) {
1899
power_components_tarjan(s, list, j);
1900
if (s->node[j].min_index < s->node[i].min_index)
1901
s->node[i].min_index = s->node[j].min_index;
1902
} else if (s->node[j].index < s->node[i].min_index)
1903
s->node[i].min_index = s->node[j].index;
1906
if (s->node[i].index != s->node[i].min_index)
1910
j = s->stack[--s->sp];
1911
s->node[j].on_stack = 0;
1912
s->order[s->op++] = j;
1914
s->order[s->op++] = -1;
1919
/* Decompose the "len" basic relations in "list" into strongly connected
1922
static struct basic_map_sort *basic_map_sort_init(isl_ctx *ctx, int len,
1923
__isl_keep isl_basic_map **list)
1926
struct basic_map_sort *s = NULL;
1928
s = basic_map_sort_alloc(ctx, len);
1931
for (i = len - 1; i >= 0; --i) {
1932
if (s->node[i].index >= 0)
1934
if (power_components_tarjan(s, list, i) < 0)
1940
basic_map_sort_free(s);
1944
1804
/* Given a union of basic maps R = \cup_i R_i \subseteq D \times D
1945
1805
* and a dimension specification (Z^{n+1} -> Z^{n+1}),
1946
1806
* construct a map that is an overapproximation of the map
1988
1849
if (map->n <= 1)
1989
1850
return floyd_warshall(dim, map, exact, project);
1991
s = basic_map_sort_init(map->ctx, map->n, map->p);
1853
data.check_closed = 0;
1854
g = isl_tarjan_graph_init(map->ctx, map->n, &basic_map_follows, &data);
1995
1858
orig_exact = exact;
1996
if (s->check_closed && !exact)
1859
if (data.check_closed && !exact)
1997
1860
exact = &local_exact;
2008
1871
struct isl_map *comp;
2009
1872
isl_map *path_comp, *path_comb;
2010
1873
comp = isl_map_alloc_space(isl_map_get_space(map), n, 0);
2011
while (s->order[i] != -1) {
1874
while (g->order[i] != -1) {
2012
1875
comp = isl_map_add_basic_map(comp,
2013
isl_basic_map_copy(map->p[s->order[i]]));
1876
isl_basic_map_copy(map->p[g->order[i]]));
2029
if (c > 1 && s->check_closed && !*exact) {
1892
if (c > 1 && data.check_closed && !*exact) {
2032
1895
closed = isl_map_is_transitively_closed(path);
2033
1896
if (closed < 0)
2036
basic_map_sort_free(s);
1899
isl_tarjan_graph_free(g);
2037
1900
isl_map_free(path);
2038
1901
return floyd_warshall(dim, map, orig_exact, project);
2042
basic_map_sort_free(s);
1905
isl_tarjan_graph_free(g);
2043
1906
isl_space_free(dim);
2047
basic_map_sort_free(s);
1910
isl_tarjan_graph_free(g);
2048
1911
isl_space_free(dim);
2049
1912
isl_map_free(path);
2908
isl_basic_map **list;
2771
isl_basic_map **list = NULL;
2909
2772
isl_basic_map **next;
2910
2773
isl_union_map *path = NULL;
2911
struct basic_map_sort *s = NULL;
2774
struct isl_tc_follows_data data;
2775
struct isl_tarjan_graph *g = NULL;
2913
2777
int recheck = 0;
2928
2792
if (isl_union_map_foreach_map(umap, collect_basic_map, &next) < 0)
2931
s = basic_map_sort_init(ctx, n, list);
2796
data.check_closed = 0;
2797
g = isl_tarjan_graph_init(ctx, n, &basic_map_follows, &data);
2940
2806
isl_union_map *comp;
2941
2807
isl_union_map *path_comp, *path_comb;
2942
2808
comp = isl_union_map_empty(isl_union_map_get_space(umap));
2943
while (s->order[i] != -1) {
2809
while (g->order[i] != -1) {
2944
2810
comp = isl_union_map_add_map(comp,
2945
2811
isl_map_from_basic_map(
2946
isl_basic_map_copy(list[s->order[i]])));
2812
isl_basic_map_copy(list[g->order[i]])));
added
removed
isl/isl_transitive_closure.c
