* Computerwetenschappen, Celestijnenlaan 200A, B-3001 Leuven, Belgium
*/
-#include "isl_ctx.h"
-#include "isl_seq.h"
-#include "isl_set.h"
-#include "isl_lp.h"
-#include "isl_map.h"
-#include "isl_map_private.h"
+#include <isl_ctx_private.h>
+#include <isl_map_private.h>
+#include <isl/seq.h>
+#include <isl/set.h>
+#include <isl/lp.h>
+#include <isl/map.h>
#include "isl_equalities.h"
#include "isl_sample.h"
#include "isl_tab.h"
if (bmap->n_ineq <= 1)
return bmap;
- tab = isl_tab_from_basic_map(bmap);
+ tab = isl_tab_from_basic_map(bmap, 0);
if (isl_tab_detect_implicit_equalities(tab) < 0)
goto error;
bmap = isl_basic_map_update_from_tab(bmap, tab);
return NULL;
}
+/* Move "sample" to a point that is one up (or down) from the original
+ * point in dimension "pos".
+ */
+static void adjacent_point(__isl_keep isl_vec *sample, int pos, int up)
+{
+ if (up)
+ isl_int_add_ui(sample->el[1 + pos], sample->el[1 + pos], 1);
+ else
+ isl_int_sub_ui(sample->el[1 + pos], sample->el[1 + pos], 1);
+}
+
+/* Check if any points that are adjacent to "sample" also belong to "bset".
+ * If so, add them to "hull" and return the updated hull.
+ *
+ * Before checking whether and adjacent point belongs to "bset", we first
+ * check whether it already belongs to "hull" as this test is typically
+ * much cheaper.
+ */
+static __isl_give isl_basic_set *add_adjacent_points(
+ __isl_take isl_basic_set *hull, __isl_take isl_vec *sample,
+ __isl_keep isl_basic_set *bset)
+{
+ int i, up;
+ int dim;
+
+ if (!sample)
+ goto error;
+
+ dim = isl_basic_set_dim(hull, isl_dim_set);
+
+ for (i = 0; i < dim; ++i) {
+ for (up = 0; up <= 1; ++up) {
+ int contains;
+ isl_basic_set *point;
+
+ adjacent_point(sample, i, up);
+ contains = isl_basic_set_contains(hull, sample);
+ if (contains < 0)
+ goto error;
+ if (contains) {
+ adjacent_point(sample, i, !up);
+ continue;
+ }
+ contains = isl_basic_set_contains(bset, sample);
+ if (contains < 0)
+ goto error;
+ if (contains) {
+ point = isl_basic_set_from_vec(
+ isl_vec_copy(sample));
+ hull = affine_hull(hull, point);
+ }
+ adjacent_point(sample, i, !up);
+ if (contains)
+ break;
+ }
+ }
+
+ isl_vec_free(sample);
+
+ return hull;
+error:
+ isl_vec_free(sample);
+ isl_basic_set_free(hull);
+ return NULL;
+}
+
/* Extend an initial (under-)approximation of the affine hull of basic
* set represented by the tableau "tab"
* by looking for points that do not satisfy one of the equalities
*
* The caller of this function ensures that "tab" is bounded or
* that tab->basis and tab->n_unbounded have been set appropriately.
+ *
+ * "bset" may be either NULL or the basic set represented by "tab".
+ * If "bset" is not NULL, we check for any point we find if any
+ * of its adjacent points also belong to "bset".
*/
-static struct isl_basic_set *extend_affine_hull(struct isl_tab *tab,
- struct isl_basic_set *hull)
+static __isl_give isl_basic_set *extend_affine_hull(struct isl_tab *tab,
+ __isl_take isl_basic_set *hull, __isl_keep isl_basic_set *bset)
{
int i, j;
unsigned dim;
tab = isl_tab_add_sample(tab, isl_vec_copy(sample));
if (!tab)
goto error;
+ if (bset)
+ hull = add_adjacent_points(hull, isl_vec_copy(sample),
+ bset);
point = isl_basic_set_from_vec(sample);
hull = affine_hull(hull, point);
if (!hull)
return bset;
}
+/* Construct an initial underapproximatino of the hull of "bset"
+ * from "sample" and any of its adjacent points that also belong to "bset".
+ */
+static __isl_give isl_basic_set *initialize_hull(__isl_keep isl_basic_set *bset,
+ __isl_take isl_vec *sample)
+{
+ isl_basic_set *hull;
+
+ hull = isl_basic_set_from_vec(isl_vec_copy(sample));
+ hull = add_adjacent_points(hull, sample, bset);
+
+ return hull;
+}
+
/* Look for all equalities satisfied by the integer points in bset,
* which is assumed to be bounded.
*
struct isl_tab *tab = NULL;
unsigned dim;
- if (isl_basic_set_fast_is_empty(bset))
+ if (isl_basic_set_plain_is_empty(bset))
return bset;
dim = isl_basic_set_n_dim(bset);
}
}
- tab = isl_tab_from_basic_set(bset);
+ tab = isl_tab_from_basic_set(bset, 1);
if (!tab)
goto error;
if (tab->empty) {
isl_vec_free(sample);
return isl_basic_set_set_to_empty(bset);
}
- if (isl_tab_track_bset(tab, isl_basic_set_copy(bset)) < 0)
- goto error;
if (!sample) {
struct isl_tab_undo *snap;
return isl_basic_set_set_to_empty(bset);
}
- hull = isl_basic_set_from_vec(sample);
+ hull = initialize_hull(bset, sample);
+ hull = extend_affine_hull(tab, hull, bset);
isl_basic_set_free(bset);
- hull = extend_affine_hull(tab, hull);
isl_tab_free(tab);
return hull;
}
/* Given an unbounded tableau and an integer point satisfying the tableau,
- * construct an intial affine hull containing the recession cone
+ * construct an initial affine hull containing the recession cone
* shifted to the given point.
*
* The unbounded directions are taken from the last rows of the basis,
* isl_tab_set_initial_basis_with_cone will add some additional
* constraints to the tableau that have to be removed again.
* In this case, we therefore rollback to the state before
- * any constraints were added and then add the eqaulities back in.
+ * any constraints were added and then add the equalities back in.
*/
struct isl_tab *isl_tab_detect_equalities(struct isl_tab *tab,
struct isl_tab *tab_cone)
isl_vec_free(sample);
- hull = extend_affine_hull(tab, hull);
+ hull = extend_affine_hull(tab, hull, NULL);
if (!hull)
goto error;
total = isl_basic_set_total_dim(cone);
cone_dim = total - cone->n_eq;
- M = isl_mat_sub_alloc(bset->ctx, cone->eq, 0, cone->n_eq, 1, total);
+ M = isl_mat_sub_alloc6(bset->ctx, cone->eq, 0, cone->n_eq, 1, total);
M = isl_mat_left_hermite(M, 0, &U, &Q);
if (!M)
goto error;
{
struct isl_basic_set *cone;
- if (isl_basic_set_fast_is_empty(bset))
+ if (isl_basic_set_plain_is_empty(bset))
return bset;
cone = isl_basic_set_recession_cone(isl_basic_set_copy(bset));
isl_basic_set_free(hull);
return isl_basic_map_set_to_empty(bmap);
}
- bmap = isl_basic_map_extend_dim(bmap, isl_dim_copy(bmap->dim), 0,
+ bmap = isl_basic_map_extend_space(bmap, isl_space_copy(bmap->dim), 0,
hull->n_eq, 0);
for (i = 0; i < hull->n_eq; ++i) {
j = isl_basic_map_alloc_equality(bmap);
isl_basic_map_detect_equalities((isl_basic_map *)bset);
}
-struct isl_map *isl_map_detect_equalities(struct isl_map *map)
+__isl_give isl_map *isl_map_inline_foreach_basic_map(__isl_take isl_map *map,
+ __isl_give isl_basic_map *(*fn)(__isl_take isl_basic_map *bmap))
{
struct isl_basic_map *bmap;
int i;
for (i = 0; i < map->n; ++i) {
bmap = isl_basic_map_copy(map->p[i]);
- bmap = isl_basic_map_detect_equalities(bmap);
+ bmap = fn(bmap);
if (!bmap)
goto error;
isl_basic_map_free(map->p[i]);
return NULL;
}
+__isl_give isl_map *isl_map_detect_equalities(__isl_take isl_map *map)
+{
+ return isl_map_inline_foreach_basic_map(map,
+ &isl_basic_map_detect_equalities);
+}
+
__isl_give isl_set *isl_set_detect_equalities(__isl_take isl_set *set)
{
return (isl_set *)isl_map_detect_equalities((isl_map *)set);
bmap = isl_basic_map_cow(bmap);
if (bmap)
isl_basic_map_free_inequality(bmap, bmap->n_ineq);
+ bmap = isl_basic_map_finalize(bmap);
return bmap;
}
projects / platform / upstream / isl.git / blobdiff