summaryrefslogtreecommitdiff
path: root/cloog-0.17.0/isl/isl_farkas.c
diff options
context:
space:
mode:
Diffstat (limited to 'cloog-0.17.0/isl/isl_farkas.c')
-rw-r--r--cloog-0.17.0/isl/isl_farkas.c385
1 files changed, 0 insertions, 385 deletions
diff --git a/cloog-0.17.0/isl/isl_farkas.c b/cloog-0.17.0/isl/isl_farkas.c
deleted file mode 100644
index 9f6a462..0000000
--- a/cloog-0.17.0/isl/isl_farkas.c
+++ /dev/null
@@ -1,385 +0,0 @@
-/*
- * Copyright 2010 INRIA Saclay
- *
- * Use of this software is governed by the GNU LGPLv2.1 license
- *
- * Written by Sven Verdoolaege, INRIA Saclay - Ile-de-France,
- * Parc Club Orsay Universite, ZAC des vignes, 4 rue Jacques Monod,
- * 91893 Orsay, France
- */
-
-#include <isl_map_private.h>
-#include <isl/set.h>
-#include <isl_space_private.h>
-#include <isl/seq.h>
-
-/*
- * Let C be a cone and define
- *
- * C' := { y | forall x in C : y x >= 0 }
- *
- * C' contains the coefficients of all linear constraints
- * that are valid for C.
- * Furthermore, C'' = C.
- *
- * If C is defined as { x | A x >= 0 }
- * then any element in C' must be a non-negative combination
- * of the rows of A, i.e., y = t A with t >= 0. That is,
- *
- * C' = { y | exists t >= 0 : y = t A }
- *
- * If any of the rows in A actually represents an equality, then
- * also negative combinations of this row are allowed and so the
- * non-negativity constraint on the corresponding element of t
- * can be dropped.
- *
- * A polyhedron P = { x | b + A x >= 0 } can be represented
- * in homogeneous coordinates by the cone
- * C = { [z,x] | b z + A x >= and z >= 0 }
- * The valid linear constraints on C correspond to the valid affine
- * constraints on P.
- * This is essentially Farkas' lemma.
- *
- * Let A' = [b A], then, since
- * [ 1 0 ]
- * [ w y ] = [t_0 t] [ b A ]
- *
- * we have
- *
- * C' = { w, y | exists t_0, t >= 0 : y = t A' and w = t_0 + t b }
- * or
- *
- * C' = { w, y | exists t >= 0 : y = t A' and w - t b >= 0 }
- *
- * In practice, we introduce an extra variable (w), shifting all
- * other variables to the right, and an extra inequality
- * (w - t b >= 0) corresponding to the positivity constraint on
- * the homogeneous coordinate.
- *
- * When going back from coefficients to solutions, we immediately
- * plug in 1 for z, which corresponds to shifting all variables
- * to the left, with the leftmost ending up in the constant position.
- */
-
-/* Add the given prefix to all named isl_dim_set dimensions in "dim".
- */
-static __isl_give isl_space *isl_space_prefix(__isl_take isl_space *dim,
- const char *prefix)
-{
- int i;
- isl_ctx *ctx;
- unsigned nvar;
- size_t prefix_len = strlen(prefix);
-
- if (!dim)
- return NULL;
-
- ctx = isl_space_get_ctx(dim);
- nvar = isl_space_dim(dim, isl_dim_set);
-
- for (i = 0; i < nvar; ++i) {
- const char *name;
- char *prefix_name;
-
- name = isl_space_get_dim_name(dim, isl_dim_set, i);
- if (!name)
- continue;
-
- prefix_name = isl_alloc_array(ctx, char,
- prefix_len + strlen(name) + 1);
- if (!prefix_name)
- goto error;
- memcpy(prefix_name, prefix, prefix_len);
- strcpy(prefix_name + prefix_len, name);
-
- dim = isl_space_set_dim_name(dim, isl_dim_set, i, prefix_name);
- free(prefix_name);
- }
-
- return dim;
-error:
- isl_space_free(dim);
- return NULL;
-}
-
-/* Given a dimension specification of the solutions space, construct
- * a dimension specification for the space of coefficients.
- *
- * In particular transform
- *
- * [params] -> { S }
- *
- * to
- *
- * { coefficients[[cst, params] -> S] }
- *
- * and prefix each dimension name with "c_".
- */
-static __isl_give isl_space *isl_space_coefficients(__isl_take isl_space *dim)
-{
- isl_space *dim_param;
- unsigned nvar;
- unsigned nparam;
-
- nvar = isl_space_dim(dim, isl_dim_set);
- nparam = isl_space_dim(dim, isl_dim_param);
- dim_param = isl_space_copy(dim);
- dim_param = isl_space_drop_dims(dim_param, isl_dim_set, 0, nvar);
- dim_param = isl_space_move_dims(dim_param, isl_dim_set, 0,
- isl_dim_param, 0, nparam);
- dim_param = isl_space_prefix(dim_param, "c_");
- dim_param = isl_space_insert_dims(dim_param, isl_dim_set, 0, 1);
- dim_param = isl_space_set_dim_name(dim_param, isl_dim_set, 0, "c_cst");
- dim = isl_space_drop_dims(dim, isl_dim_param, 0, nparam);
- dim = isl_space_prefix(dim, "c_");
- dim = isl_space_join(isl_space_from_domain(dim_param),
- isl_space_from_range(dim));
- dim = isl_space_wrap(dim);
- dim = isl_space_set_tuple_name(dim, isl_dim_set, "coefficients");
-
- return dim;
-}
-
-/* Drop the given prefix from all named dimensions of type "type" in "dim".
- */
-static __isl_give isl_space *isl_space_unprefix(__isl_take isl_space *dim,
- enum isl_dim_type type, const char *prefix)
-{
- int i;
- unsigned n;
- size_t prefix_len = strlen(prefix);
-
- n = isl_space_dim(dim, type);
-
- for (i = 0; i < n; ++i) {
- const char *name;
-
- name = isl_space_get_dim_name(dim, type, i);
- if (!name)
- continue;
- if (strncmp(name, prefix, prefix_len))
- continue;
-
- dim = isl_space_set_dim_name(dim, type, i, name + prefix_len);
- }
-
- return dim;
-}
-
-/* Given a dimension specification of the space of coefficients, construct
- * a dimension specification for the space of solutions.
- *
- * In particular transform
- *
- * { coefficients[[cst, params] -> S] }
- *
- * to
- *
- * [params] -> { S }
- *
- * and drop the "c_" prefix from the dimension names.
- */
-static __isl_give isl_space *isl_space_solutions(__isl_take isl_space *dim)
-{
- unsigned nparam;
-
- dim = isl_space_unwrap(dim);
- dim = isl_space_drop_dims(dim, isl_dim_in, 0, 1);
- dim = isl_space_unprefix(dim, isl_dim_in, "c_");
- dim = isl_space_unprefix(dim, isl_dim_out, "c_");
- nparam = isl_space_dim(dim, isl_dim_in);
- dim = isl_space_move_dims(dim, isl_dim_param, 0, isl_dim_in, 0, nparam);
- dim = isl_space_range(dim);
-
- return dim;
-}
-
-/* Compute the dual of "bset" by applying Farkas' lemma.
- * As explained above, we add an extra dimension to represent
- * the coefficient of the constant term when going from solutions
- * to coefficients (shift == 1) and we drop the extra dimension when going
- * in the opposite direction (shift == -1). "dim" is the space in which
- * the dual should be created.
- */
-static __isl_give isl_basic_set *farkas(__isl_take isl_space *dim,
- __isl_take isl_basic_set *bset, int shift)
-{
- int i, j, k;
- isl_basic_set *dual = NULL;
- unsigned total;
-
- total = isl_basic_set_total_dim(bset);
-
- dual = isl_basic_set_alloc_space(dim, bset->n_eq + bset->n_ineq,
- total, bset->n_ineq + (shift > 0));
- dual = isl_basic_set_set_rational(dual);
-
- for (i = 0; i < bset->n_eq + bset->n_ineq; ++i) {
- k = isl_basic_set_alloc_div(dual);
- if (k < 0)
- goto error;
- isl_int_set_si(dual->div[k][0], 0);
- }
-
- for (i = 0; i < total; ++i) {
- k = isl_basic_set_alloc_equality(dual);
- if (k < 0)
- goto error;
- isl_seq_clr(dual->eq[k], 1 + shift + total);
- isl_int_set_si(dual->eq[k][1 + shift + i], -1);
- for (j = 0; j < bset->n_eq; ++j)
- isl_int_set(dual->eq[k][1 + shift + total + j],
- bset->eq[j][1 + i]);
- for (j = 0; j < bset->n_ineq; ++j)
- isl_int_set(dual->eq[k][1 + shift + total + bset->n_eq + j],
- bset->ineq[j][1 + i]);
- }
-
- for (i = 0; i < bset->n_ineq; ++i) {
- k = isl_basic_set_alloc_inequality(dual);
- if (k < 0)
- goto error;
- isl_seq_clr(dual->ineq[k],
- 1 + shift + total + bset->n_eq + bset->n_ineq);
- isl_int_set_si(dual->ineq[k][1 + shift + total + bset->n_eq + i], 1);
- }
-
- if (shift > 0) {
- k = isl_basic_set_alloc_inequality(dual);
- if (k < 0)
- goto error;
- isl_seq_clr(dual->ineq[k], 2 + total);
- isl_int_set_si(dual->ineq[k][1], 1);
- for (j = 0; j < bset->n_eq; ++j)
- isl_int_neg(dual->ineq[k][2 + total + j],
- bset->eq[j][0]);
- for (j = 0; j < bset->n_ineq; ++j)
- isl_int_neg(dual->ineq[k][2 + total + bset->n_eq + j],
- bset->ineq[j][0]);
- }
-
- dual = isl_basic_set_remove_divs(dual);
- isl_basic_set_simplify(dual);
- isl_basic_set_finalize(dual);
-
- isl_basic_set_free(bset);
- return dual;
-error:
- isl_basic_set_free(bset);
- isl_basic_set_free(dual);
- return NULL;
-}
-
-/* Construct a basic set containing the tuples of coefficients of all
- * valid affine constraints on the given basic set.
- */
-__isl_give isl_basic_set *isl_basic_set_coefficients(
- __isl_take isl_basic_set *bset)
-{
- isl_space *dim;
-
- if (!bset)
- return NULL;
- if (bset->n_div)
- isl_die(bset->ctx, isl_error_invalid,
- "input set not allowed to have local variables",
- goto error);
-
- dim = isl_basic_set_get_space(bset);
- dim = isl_space_coefficients(dim);
-
- return farkas(dim, bset, 1);
-error:
- isl_basic_set_free(bset);
- return NULL;
-}
-
-/* Construct a basic set containing the elements that satisfy all
- * affine constraints whose coefficient tuples are
- * contained in the given basic set.
- */
-__isl_give isl_basic_set *isl_basic_set_solutions(
- __isl_take isl_basic_set *bset)
-{
- isl_space *dim;
-
- if (!bset)
- return NULL;
- if (bset->n_div)
- isl_die(bset->ctx, isl_error_invalid,
- "input set not allowed to have local variables",
- goto error);
-
- dim = isl_basic_set_get_space(bset);
- dim = isl_space_solutions(dim);
-
- return farkas(dim, bset, -1);
-error:
- isl_basic_set_free(bset);
- return NULL;
-}
-
-/* Construct a basic set containing the tuples of coefficients of all
- * valid affine constraints on the given set.
- */
-__isl_give isl_basic_set *isl_set_coefficients(__isl_take isl_set *set)
-{
- int i;
- isl_basic_set *coeff;
-
- if (!set)
- return NULL;
- if (set->n == 0) {
- isl_space *dim = isl_set_get_space(set);
- dim = isl_space_coefficients(dim);
- coeff = isl_basic_set_universe(dim);
- coeff = isl_basic_set_set_rational(coeff);
- isl_set_free(set);
- return coeff;
- }
-
- coeff = isl_basic_set_coefficients(isl_basic_set_copy(set->p[0]));
-
- for (i = 1; i < set->n; ++i) {
- isl_basic_set *bset, *coeff_i;
- bset = isl_basic_set_copy(set->p[i]);
- coeff_i = isl_basic_set_coefficients(bset);
- coeff = isl_basic_set_intersect(coeff, coeff_i);
- }
-
- isl_set_free(set);
- return coeff;
-}
-
-/* Construct a basic set containing the elements that satisfy all
- * affine constraints whose coefficient tuples are
- * contained in the given set.
- */
-__isl_give isl_basic_set *isl_set_solutions(__isl_take isl_set *set)
-{
- int i;
- isl_basic_set *sol;
-
- if (!set)
- return NULL;
- if (set->n == 0) {
- isl_space *dim = isl_set_get_space(set);
- dim = isl_space_solutions(dim);
- sol = isl_basic_set_universe(dim);
- sol = isl_basic_set_set_rational(sol);
- isl_set_free(set);
- return sol;
- }
-
- sol = isl_basic_set_solutions(isl_basic_set_copy(set->p[0]));
-
- for (i = 1; i < set->n; ++i) {
- isl_basic_set *bset, *sol_i;
- bset = isl_basic_set_copy(set->p[i]);
- sol_i = isl_basic_set_solutions(bset);
- sol = isl_basic_set_intersect(sol, sol_i);
- }
-
- isl_set_free(set);
- return sol;
-}