/* * Copyright 2008-2009 Katholieke Universiteit Leuven * * Use of this software is governed by the MIT license * * Written by Sven Verdoolaege, K.U.Leuven, Departement * Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium */ #include <isl_map_private.h> #include <isl_seq.h> #include <isl/set.h> #include <isl/map.h> #include "isl_tab.h" #include <isl_point_private.h> #include <isl_vec_private.h> #include <set_to_map.c> #include <set_from_map.c> /* Expand the constraint "c" into "v". The initial "dim" dimensions * are the same, but "v" may have more divs than "c" and the divs of "c" * may appear in different positions in "v". * The number of divs in "c" is given by "n_div" and the mapping * of divs in "c" to divs in "v" is given by "div_map". * * Although it shouldn't happen in practice, it is theoretically * possible that two or more divs in "c" are mapped to the same div in "v". * These divs are then necessarily the same, so we simply add their * coefficients. */ static void expand_constraint(isl_vec *v, unsigned dim, isl_int *c, int *div_map, unsigned n_div) { … } /* Add all constraints of bmap to tab. The equalities of bmap * are added as a pair of inequalities. */ static isl_stat tab_add_constraints(struct isl_tab *tab, __isl_keep isl_basic_map *bmap, int *div_map) { … } /* Add a specific constraint of bmap (or its opposite) to tab. * The position of the constraint is specified by "c", where * the equalities of bmap are counted twice, once for the inequality * that is equal to the equality, and once for its negation. * * Each of these constraints has been added to "tab" before by * tab_add_constraints (and later removed again), so there should * already be a row available for the constraint. */ static isl_stat tab_add_constraint(struct isl_tab *tab, __isl_keep isl_basic_map *bmap, int *div_map, int c, int oppose) { … } static isl_stat tab_add_divs(struct isl_tab *tab, __isl_keep isl_basic_map *bmap, int **div_map) { … } /* Freeze all constraints of tableau tab. */ static int tab_freeze_constraints(struct isl_tab *tab) { … } /* Check for redundant constraints starting at offset. * Put the indices of the non-redundant constraints in index * and return the number of non-redundant constraints. */ static int n_non_redundant(isl_ctx *ctx, struct isl_tab *tab, int offset, int **index) { … } /* basic_map_collect_diff calls add on each of the pieces of * the set difference between bmap and map until the add method * return a negative value. */ struct isl_diff_collector { … }; /* Compute the set difference between bmap and map and call * dc->add on each of the piece until this function returns * a negative value. * Return 0 on success and -1 on error. dc->add returning * a negative value is treated as an error, but the calling * function can interpret the results based on the state of dc. * * Assumes that map has known divs. * * The difference is computed by a backtracking algorithm. * Each level corresponds to a basic map in "map". * When a node in entered for the first time, we check * if the corresonding basic map intersects the current piece * of "bmap". If not, we move to the next level. * Otherwise, we split the current piece into as many * pieces as there are non-redundant constraints of the current * basic map in the intersection. Each of these pieces is * handled by a child of the current node. * In particular, if there are n non-redundant constraints, * then for each 0 <= i < n, a piece is cut off by adding * constraints 0 <= j < i and adding the opposite of constraint i. * If there are no non-redundant constraints, meaning that the current * piece is a subset of the current basic map, then we simply backtrack. * * In the leaves, we check if the remaining piece has any integer points * and if so, pass it along to dc->add. As a special case, if nothing * has been removed when we end up in a leaf, we simply pass along * the original basic map. */ static isl_stat basic_map_collect_diff(__isl_take isl_basic_map *bmap, __isl_take isl_map *map, struct isl_diff_collector *dc) { … } /* A diff collector that actually collects all parts of the * set difference in the field diff. */ struct isl_subtract_diff_collector { … }; /* isl_subtract_diff_collector callback. */ static isl_stat basic_map_subtract_add(struct isl_diff_collector *dc, __isl_take isl_basic_map *bmap) { … } /* Return the set difference between bmap and map. */ static __isl_give isl_map *basic_map_subtract(__isl_take isl_basic_map *bmap, __isl_take isl_map *map) { … } /* Return an empty map living in the same space as "map1" and "map2". */ static __isl_give isl_map *replace_pair_by_empty( __isl_take isl_map *map1, __isl_take isl_map *map2) { … } /* Return the set difference between map1 and map2. * (U_i A_i) \ (U_j B_j) is computed as U_i (A_i \ (U_j B_j)) * * If "map1" and "map2" are obviously equal to each other, * then return an empty map in the same space. * * If "map1" and "map2" are disjoint, then simply return "map1". */ __isl_give isl_map *isl_map_subtract( __isl_take isl_map *map1, __isl_take isl_map *map2) { … } __isl_give isl_set *isl_set_subtract(__isl_take isl_set *set1, __isl_take isl_set *set2) { … } /* Remove the elements of "dom" from the domain of "map". */ __isl_give isl_map *isl_map_subtract_domain(__isl_take isl_map *map, __isl_take isl_set *dom) { … } /* Remove the elements of "dom" from the range of "map". */ __isl_give isl_map *isl_map_subtract_range(__isl_take isl_map *map, __isl_take isl_set *dom) { … } /* A diff collector that aborts as soon as its add function is called, * setting empty to isl_false. */ struct isl_is_empty_diff_collector { … }; /* isl_is_empty_diff_collector callback. */ static isl_stat basic_map_is_empty_add(struct isl_diff_collector *dc, __isl_take isl_basic_map *bmap) { … } /* Check if bmap \ map is empty by computing this set difference * and breaking off as soon as the difference is known to be non-empty. */ static isl_bool basic_map_diff_is_empty(__isl_keep isl_basic_map *bmap, __isl_keep isl_map *map) { … } /* Check if map1 \ map2 is empty by checking if the set difference is empty * for each of the basic maps in map1. */ static isl_bool map_diff_is_empty(__isl_keep isl_map *map1, __isl_keep isl_map *map2) { … } /* Return true if "bmap" contains a single element. */ isl_bool isl_basic_map_plain_is_singleton(__isl_keep isl_basic_map *bmap) { … } /* Return true if "map" contains a single element. */ isl_bool isl_map_plain_is_singleton(__isl_keep isl_map *map) { … } /* Given a singleton basic map, extract the single element * as an isl_point. */ static __isl_give isl_point *singleton_extract_point( __isl_keep isl_basic_map *bmap) { … } /* Return isl_bool_true if the singleton map "map1" is a subset of "map2", * i.e., if the single element of "map1" is also an element of "map2". * Assumes "map2" has known divs. */ static isl_bool map_is_singleton_subset(__isl_keep isl_map *map1, __isl_keep isl_map *map2) { … } static isl_bool map_is_subset(__isl_keep isl_map *map1, __isl_keep isl_map *map2) { … } isl_bool isl_map_is_subset(__isl_keep isl_map *map1, __isl_keep isl_map *map2) { … } isl_bool isl_set_is_subset(__isl_keep isl_set *set1, __isl_keep isl_set *set2) { … } __isl_give isl_map *isl_map_make_disjoint(__isl_take isl_map *map) { … } __isl_give isl_set *isl_set_make_disjoint(__isl_take isl_set *set) { … } __isl_give isl_map *isl_map_complement(__isl_take isl_map *map) { … } __isl_give isl_set *isl_set_complement(__isl_take isl_set *set) { … }