From: Sven Verdoolaege <skimo@kotnet.org>
Date: Wed, 5 Jan 2011 09:26:32 +0000 (+0100)
Subject: Merge commit 'isl-0.05.1'
X-Git-Tag: isl-0.06~116
X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=b6f4dc516a5f5f3d83132a3dd77e6d574768af89;hp=-c;p=platform%2Fupstream%2Fisl.git

Merge commit 'isl-0.05.1'

Signed-off-by: Sven Verdoolaege <skimo@kotnet.org>
---

b6f4dc516a5f5f3d83132a3dd77e6d574768af89
diff --combined isl_map.c
index 57c9d11,89be7b2..c8b15aa
--- a/isl_map.c
+++ b/isl_map.c
@@@ -1721,8 -1721,7 +1721,8 @@@ static void dump(struct isl_basic_map *
  	}
  }
  
 -void isl_basic_set_dump(struct isl_basic_set *bset, FILE *out, int indent)
 +void isl_basic_set_print_internal(struct isl_basic_set *bset,
 +	FILE *out, int indent)
  {
  	if (!bset) {
  		fprintf(out, "null basic set\n");
@@@ -1736,8 -1735,7 +1736,8 @@@
  	dump((struct isl_basic_map *)bset, out, indent);
  }
  
 -void isl_basic_map_dump(struct isl_basic_map *bmap, FILE *out, int indent)
 +void isl_basic_map_print_internal(struct isl_basic_map *bmap,
 +	FILE *out, int indent)
  {
  	if (!bmap) {
  		fprintf(out, "null basic map\n");
@@@ -1913,7 -1911,7 +1913,7 @@@ void isl_set_free(struct isl_set *set
  	free(set);
  }
  
 -void isl_set_dump(struct isl_set *set, FILE *out, int indent)
 +void isl_set_print_internal(struct isl_set *set, FILE *out, int indent)
  {
  	int i;
  
@@@ -1929,11 -1927,11 +1929,11 @@@
  	for (i = 0; i < set->n; ++i) {
  		fprintf(out, "%*s", indent, "");
  		fprintf(out, "basic set %d:\n", i);
 -		isl_basic_set_dump(set->p[i], out, indent+4);
 +		isl_basic_set_print_internal(set->p[i], out, indent+4);
  	}
  }
  
 -void isl_map_dump(struct isl_map *map, FILE *out, int indent)
 +void isl_map_print_internal(struct isl_map *map, FILE *out, int indent)
  {
  	int i;
  
@@@ -1950,7 -1948,7 +1950,7 @@@
  	for (i = 0; i < map->n; ++i) {
  		fprintf(out, "%*s", indent, "");
  		fprintf(out, "basic map %d:\n", i);
 -		isl_basic_map_dump(map->p[i], out, indent+4);
 +		isl_basic_map_print_internal(map->p[i], out, indent+4);
  	}
  }
  
@@@ -4083,6 -4081,7 +4083,7 @@@ struct isl_basic_map *isl_basic_map_uni
  {
  	struct isl_basic_map *bmap;
  	bmap = isl_basic_map_alloc_dim(dim, 0, 0, 0);
+ 	bmap = isl_basic_map_finalize(bmap);
  	return bmap;
  }
  
@@@ -4090,6 -4089,7 +4091,7 @@@ struct isl_basic_set *isl_basic_set_uni
  {
  	struct isl_basic_set *bset;
  	bset = isl_basic_set_alloc_dim(dim, 0, 0, 0);
+ 	bset = isl_basic_set_finalize(bset);
  	return bset;
  }
  
@@@ -4592,7 -4592,7 +4594,7 @@@ struct isl_set *isl_basic_set_partial_l
  			dom, empty);
  }
  
 -/* Given a basic map "bmap", compute the lexicograhically minimal
 +/* Given a basic map "bmap", compute the lexicographically minimal
   * (or maximal) image element for each domain element in dom.
   * Set *empty to those elements in dom that do not have an image element.
   *
@@@ -4644,7 -4644,7 +4646,7 @@@ error
  	return NULL;
  }
  
 -/* Given a map "map", compute the lexicograhically minimal
 +/* Given a map "map", compute the lexicographically minimal
   * (or maximal) image element for each domain element in dom.
   * Set *empty to those elements in dom that do not have an image element.
   *
@@@ -4656,46 -4656,16 +4658,46 @@@
   *
   * Let res^k and todo^k be the results after k steps and let i = k + 1.
   * Assume we are computing the lexicographical maximum.
 - * We first intersect basic map i with a relation that maps elements
 - * to elements that are lexicographically larger than the image elements
 - * in res^k and the compute the maximum image element of this intersection.
 - * The result ("better") corresponds to those image elements in basic map i
 - * that are better than what we had before.  The remainder ("keep") are the
 - * domain elements for which the image element in res_k was better.
 - * We also compute the lexicographical maximum of basic map i in todo^k.
 - * res^i is the result of the operation + better + those elements in
 - *		res^k that we should keep
 - * todo^i is the remainder of the maximum operation on todo^k.
 + * We first compute the lexicographically maximal element in basic map i.
 + * This results in a partial solution res_i and a subset todo_i.
 + * Then we combine these results with those obtain for the first k basic maps
 + * to obtain a result that is valid for the first k+1 basic maps.
 + * In particular, the set where there is no solution is the set where
 + * there is no solution for the first k basic maps and also no solution
 + * for the ith basic map, i.e.,
 + *
 + *	todo^i = todo^k * todo_i
 + *
 + * On dom(res^k) * dom(res_i), we need to pick the larger of the two
 + * solutions, arbitrarily breaking ties in favor of res^k.
 + * That is, when res^k(a) >= res_i(a), we pick res^k and
 + * when res^k(a) < res_i(a), we pick res_i.  (Here, ">=" and "<" denote
 + * the lexicographic order.)
 + * In practice, we compute
 + *
 + *	res^k * (res_i . "<=")
 + *
 + * and
 + *
 + *	res_i * (res^k . "<")
 + *
 + * Finally, we consider the symmetric difference of dom(res^k) and dom(res_i),
 + * where only one of res^k and res_i provides a solution and we simply pick
 + * that one, i.e.,
 + *
 + *	res^k * todo_i
 + * and
 + *	res_i * todo^k
 + *
 + * Note that we only compute these intersections when dom(res^k) intersects
 + * dom(res_i).  Otherwise, the only effect of these intersections is to
 + * potentially break up res^k and res_i into smaller pieces.
 + * We want to avoid such splintering as much as possible.
 + * In fact, an earlier implementation of this function would look for
 + * better results in the domain of res^k and for extra results in todo^k,
 + * but this would always result in a splintering according to todo^k,
 + * even when the domain of basic map i is disjoint from the domains of
 + * the previous basic maps.
   */
  static __isl_give isl_map *isl_map_partial_lexopt(
  		__isl_take isl_map *map, __isl_take isl_set *dom,
@@@ -4720,38 -4690,32 +4722,38 @@@
  					isl_set_copy(dom), &todo, max);
  
  	for (i = 1; i < map->n; ++i) {
 -		struct isl_map *lt;
 -		struct isl_map *better;
 -		struct isl_set *keep;
 -		struct isl_map *res_i;
 -		struct isl_set *todo_i;
 -		struct isl_dim *dim = isl_map_get_dim(res);
 -
 -		dim = isl_dim_range(dim);
 -		if (max)
 -			lt = isl_map_lex_lt(dim);
 -		else
 -			lt = isl_map_lex_gt(dim);
 -		lt = isl_map_apply_range(isl_map_copy(res), lt);
 -		lt = isl_map_intersect(lt,
 -			isl_map_from_basic_map(isl_basic_map_copy(map->p[i])));
 -		better = isl_map_partial_lexopt(lt,
 -			isl_map_domain(isl_map_copy(res)),
 -			&keep, max);
 +		isl_map *lt, *le;
 +		isl_map *res_i;
 +		isl_set *todo_i;
 +		isl_dim *dim = isl_dim_range(isl_map_get_dim(res));
  
  		res_i = basic_map_partial_lexopt(isl_basic_map_copy(map->p[i]),
 -						todo, &todo_i, max);
 +					isl_set_copy(dom), &todo_i, max);
 +
 +		if (max) {
 +			lt = isl_map_lex_lt(isl_dim_copy(dim));
 +			le = isl_map_lex_le(dim);
 +		} else {
 +			lt = isl_map_lex_gt(isl_dim_copy(dim));
 +			le = isl_map_lex_ge(dim);
 +		}
 +		lt = isl_map_apply_range(isl_map_copy(res), lt);
 +		lt = isl_map_intersect(lt, isl_map_copy(res_i));
 +		le = isl_map_apply_range(isl_map_copy(res_i), le);
 +		le = isl_map_intersect(le, isl_map_copy(res));
 +
 +		if (!isl_map_is_empty(lt) || !isl_map_is_empty(le)) {
 +			res = isl_map_intersect_domain(res,
 +							isl_set_copy(todo_i));
 +			res_i = isl_map_intersect_domain(res_i,
 +							isl_set_copy(todo));
 +		}
  
 -		res = isl_map_intersect_domain(res, keep);
  		res = isl_map_union_disjoint(res, res_i);
 -		res = isl_map_union_disjoint(res, better);
 -		todo = todo_i;
 +		res = isl_map_union_disjoint(res, lt);
 +		res = isl_map_union_disjoint(res, le);
 +
 +		todo = isl_set_intersect(todo, todo_i);
  	}
  
  	isl_set_free(dom);
diff --combined isl_test.c
index 2a0594b,af517f1..8af787d
--- a/isl_test.c
+++ b/isl_test.c
@@@ -1115,7 -1115,7 +1115,7 @@@ void test_lex(struct isl_ctx *ctx
  void test_lexmin(struct isl_ctx *ctx)
  {
  	const char *str;
 -	isl_map *map;
 +	isl_map *map, *map2;
  	isl_set *set;
  	isl_set *set2;
  
@@@ -1144,36 -1144,6 +1144,36 @@@
  	set = isl_set_intersect(set, set2);
  	assert(!isl_set_is_empty(set));
  	isl_set_free(set);
 +
 +	str = "{ [x] -> [y] : x <= y <= 10; [x] -> [5] : -8 <= x <= 8 }";
 +	map = isl_map_read_from_str(ctx, str, -1);
 +	map = isl_map_lexmin(map);
 +	str = "{ [x] -> [5] : 6 <= x <= 8; "
 +		"[x] -> [x] : x <= 5 or (9 <= x <= 10) }";
 +	map2 = isl_map_read_from_str(ctx, str, -1);
 +	assert(isl_map_is_equal(map, map2));
 +	isl_map_free(map);
 +	isl_map_free(map2);
 +
 +	str = "{ [x] -> [y] : 4y = x or 4y = -1 + x or 4y = -2 + x }";
 +	map = isl_map_read_from_str(ctx, str, -1);
 +	map2 = isl_map_copy(map);
 +	map = isl_map_lexmin(map);
 +	assert(isl_map_is_equal(map, map2));
 +	isl_map_free(map);
 +	isl_map_free(map2);
 +
 +	str = "{ [x] -> [y] : x = 4y; [x] -> [y] : x = 2y }";
 +	map = isl_map_read_from_str(ctx, str, -1);
 +	map = isl_map_lexmin(map);
 +	str = "{ [x] -> [y] : (4y = x and x >= 0) or "
 +		"(exists (e0 = [(x)/4], e1 = [(-2 + x)/4]: 2y = x and "
 +		"4e1 = -2 + x and 4e0 <= -1 + x and 4e0 >= -3 + x)) or "
 +		"(exists (e0 = [(x)/4]: 2y = x and 4e0 = x and x <= -4)) }";
 +	map2 = isl_map_read_from_str(ctx, str, -1);
 +	assert(isl_map_is_equal(map, map2));
 +	isl_map_free(map);
 +	isl_map_free(map2);
  }
  
  struct must_may {
@@@ -1607,6 -1577,22 +1607,22 @@@ void test_lift(isl_ctx *ctx
  	isl_basic_set_free(bset);
  }
  
+ void test_subset(isl_ctx *ctx)
+ {
+ 	const char *str;
+ 	isl_set *set1, *set2;
+ 
+ 	str = "{ [112, 0] }";
+ 	set1 = isl_set_read_from_str(ctx, str, 0);
+ 	str = "{ [i0, i1] : exists (e0 = [(i0 - i1)/16], e1: "
+ 		"16e0 <= i0 - i1 and 16e0 >= -15 + i0 - i1 and "
+ 		"16e1 <= i1 and 16e0 >= -i1 and 16e1 >= -i0 + i1) }";
+ 	set2 = isl_set_read_from_str(ctx, str, 0);
+ 	assert(isl_set_is_subset(set1, set2));
+ 	isl_set_free(set1);
+ 	isl_set_free(set2);
+ }
+ 
  int main()
  {
  	struct isl_ctx *ctx;
@@@ -1615,6 -1601,7 +1631,7 @@@
  	assert(srcdir);
  
  	ctx = isl_ctx_alloc();
+ 	test_subset(ctx);
  	test_lift(ctx);
  	test_bound(ctx);
  	test_union(ctx);