/*

 * Copyright 2008-2009 Katholieke Universiteit Leuven

 * Copyright 2010      INRIA Saclay

 * Copyright 2012-2013 Ecole Normale Superieure

 *

 * 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

 * and INRIA Saclay - Ile-de-France, Parc Club Orsay Universite,

 * ZAC des vignes, 4 rue Jacques Monod, 91893 Orsay, France 

 * and Ecole Normale Superieure, 45 rue d’Ulm, 75230 Paris, France

 */

#include <stdlib.h>

#include <string.h>

#include <isl_ctx_private.h>

#include <isl_map_private.h>

#include <isl/set.h>

#include <isl_seq.h>

#include <isl_polynomial_private.h>

#include <isl_printer_private.h>

#include <isl_space_private.h>

#include <isl_mat_private.h>

#include <isl_vec_private.h>

#include <isl/union_set.h>

#include <isl/union_map.h>

#include <isl/constraint.h>

#include <isl_local_space_private.h>

#include <isl_aff_private.h>

#include <isl_val_private.h>

#include <isl_constraint_private.h>

#include <isl/ast_build.h>

#include <isl_sort.h>

#include <isl_output_private.h>

#include <bset_to_bmap.c>

#include <set_to_map.c>

#include <uset_to_umap.c>

static const char *s_to[2] = { " -> ", " \\to " };

static const char *s_and[2] = { " and ", " \\wedge " };

static const char *s_or[2] = { " or ", " \\vee " };

static const char *s_le[2] = { "<=", "\\le" };

static const char *s_ge[2] = { ">=", "\\ge" };

static const char *s_open_set[2] = { "{ ", "\\{\\, " };

static const char *s_close_set[2] = { " }", " \\,\\}" };

static const char *s_open_list[2] = { "[", "(" };

static const char *s_close_list[2] = { "]", ")" };

static const char *s_such_that[2] = { " : ", " \\mid " };

static const char *s_open_exists[2] = { "exists (", "\\exists \\, " };

static const char *s_close_exists[2] = { ")", "" };

static const char *s_div_prefix[2] = { "e", "\\alpha_" };

static const char *s_mod[2] = { "mod", "\\bmod" };

static const char *s_param_prefix[2] = { "p", "p_" };

static const char *s_input_prefix[2] = { "i", "i_" };

static const char *s_output_prefix[2] = { "o", "o_" };

static __isl_give isl_printer *print_constraint_polylib(

  struct isl_basic_map *bmap, int ineq, int n, __isl_take isl_printer *p)

{

  int i;

  unsigned n_in = isl_basic_map_dim(bmap, isl_dim_in);

  unsigned n_out = isl_basic_map_dim(bmap, isl_dim_out);

  unsigned nparam = isl_basic_map_dim(bmap, isl_dim_param);

  isl_int *c = ineq ? bmap->ineq[n] : bmap->eq[n];

  p = isl_printer_start_line(p);

  p = isl_printer_print_int(p, ineq);

  for (i = 0; i < n_out; ++i) {

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_isl_int(p, c[1+nparam+n_in+i]);

  }

  for (i = 0; i < n_in; ++i) {

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_isl_int(p, c[1+nparam+i]);

  }

  for (i = 0; i < bmap->n_div; ++i) {

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_isl_int(p, c[1+nparam+n_in+n_out+i]);

  }

  for (i = 0; i < nparam; ++i) {

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_isl_int(p, c[1+i]);

  }

  p = isl_printer_print_str(p, " ");

  p = isl_printer_print_isl_int(p, c[0]);

  p = isl_printer_end_line(p);

  return p;

}

static __isl_give isl_printer *print_constraints_polylib(

  struct isl_basic_map *bmap, __isl_take isl_printer *p)

{

  int i;

  p = isl_printer_set_isl_int_width(p, 5);

  for (i = 0; i < bmap->n_eq; ++i)

    p = print_constraint_polylib(bmap, 0, i, p);

  for (i = 0; i < bmap->n_ineq; ++i)

    p = print_constraint_polylib(bmap, 1, i, p);

  return p;

}

static __isl_give isl_printer *bset_print_constraints_polylib(

  struct isl_basic_set *bset, __isl_take isl_printer *p)

{

  return print_constraints_polylib(bset_to_bmap(bset), p);

}

static __isl_give isl_printer *isl_basic_map_print_polylib(

  __isl_keep isl_basic_map *bmap, __isl_take isl_printer *p, int ext)

{

  unsigned total = isl_basic_map_total_dim(bmap);

  p = isl_printer_start_line(p);

  p = isl_printer_print_int(p, bmap->n_eq + bmap->n_ineq);

  p = isl_printer_print_str(p, " ");

  p = isl_printer_print_int(p, 1 + total + 1);

  if (ext) {

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_int(p,

            isl_basic_map_dim(bmap, isl_dim_out));

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_int(p,

            isl_basic_map_dim(bmap, isl_dim_in));

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_int(p,

            isl_basic_map_dim(bmap, isl_dim_div));

    p = isl_printer_print_str(p, " ");

    p = isl_printer_print_int(p,

            isl_basic_map_dim(bmap, isl_dim_param));

  }

  p = isl_printer_end_line(p);

  return print_constraints_polylib(bmap, p);

}

static __isl_give isl_printer *isl_basic_set_print_polylib(

  __isl_keep isl_basic_set *bset, __isl_take isl_printer *p, int ext)

{

  return isl_basic_map_print_polylib(bset_to_bmap(bset), p, ext);

}

static __isl_give isl_printer *isl_map_print_polylib(__isl_keep isl_map *map,

  __isl_take isl_printer *p, int ext)

{

  int i;

  p = isl_printer_start_line(p);

  p = isl_printer_print_int(p, map->n);

  p = isl_printer_end_line(p);

  for (i = 0; i < map->n; ++i) {

    p = isl_printer_start_line(p);

    p = isl_printer_end_line(p);

    p = isl_basic_map_print_polylib(map->p[i], p, ext);

  }

  return p;

}

static __isl_give isl_printer *isl_set_print_polylib(__isl_keep isl_set *set,

  __isl_take isl_printer *p, int ext)

{

  return isl_map_print_polylib(set_to_map(set), p, ext);

}

static int count_same_name(__isl_keep isl_space *dim,

  enum isl_dim_type type, unsigned pos, const char *name)

{

  enum isl_dim_type t;

  unsigned p, s;

  int count = 0;

  for (t = isl_dim_param; t <= type && 
t <= isl_dim_out72.3k
; 
++t59.9k
) {

    s = t == type ? 
pos22.2k
 : 
isl_space_dim(dim, t)37.6k
;

    for (p = 0; p < s; 
++p278k
) {

      const char *n = isl_space_get_dim_name(dim, t, p);

      if (n && 
!strcmp(n, name)238k
)

        count++;

    }

  }

  return count;

}

/* Print the name of the variable of type "type" and position "pos"

 * in "space" to "p".

 */

static __isl_give isl_printer *print_name(__isl_keep isl_space *space,

  __isl_take isl_printer *p, enum isl_dim_type type, unsigned pos,

  int latex)

{

  const char *name;

  char buffer[20];

  int primes;

  name = type == isl_dim_div ? NULL

           : 
isl_space_get_dim_name(space, type, pos)34.6k
;

  if (!name) {

    const char *prefix;

    if (type == isl_dim_param)

      prefix = s_param_prefix[latex];

    else if (type == isl_dim_div)

      prefix = s_div_prefix[latex];

    else if (isl_space_is_set(space) || 
type == isl_dim_in10.4k
)

      prefix = s_input_prefix[latex];

    else

      prefix = s_output_prefix[latex];

    snprintf(buffer, sizeof(buffer), "%s%d", prefix, pos);

    name = buffer;

  }

  primes = count_same_name(space, name == buffer ? 
isl_dim_div12.3k
 : 
type22.2k
,

         pos, name);

  p = isl_printer_print_str(p, name);

  while (primes-- > 0)

    p = isl_printer_print_str(p, "'");

  return p;

}

static enum isl_dim_type pos2type(__isl_keep isl_space *dim, unsigned *pos)

{

  enum isl_dim_type type;

  unsigned n_in = isl_space_dim(dim, isl_dim_in);

  unsigned n_out = isl_space_dim(dim, isl_dim_out);

  unsigned nparam = isl_space_dim(dim, isl_dim_param);

  if (*pos < 1 + nparam) {

    type = isl_dim_param;

    *pos -= 1;

  } else if (*pos < 1 + nparam + n_in) {

    type = isl_dim_in;

    *pos -= 1 + nparam;

  } else 
if (1.83k
*pos < 1 + nparam + n_in + n_out1.83k
) {

    type = isl_dim_out;

    *pos -= 1 + nparam + n_in;

  } else {

    type = isl_dim_div;

    *pos -= 1 + nparam + n_in + n_out;

  }

  return type;

}

/* Can the div expression of the integer division at position "row" of "div"

 * be printed?

 * In particular, are the div expressions available and does the selected

 * variable have a known explicit representation?

 * Furthermore, the Omega format does not allow any div expressions

 * to be printed.

 */

static isl_bool can_print_div_expr(__isl_keep isl_printer *p,

  __isl_keep isl_mat *div, int pos)

{

  if (p->output_format == ISL_FORMAT_OMEGA)

    
return isl_bool_false0
;

  if (!div)

    return isl_bool_false;

  return !isl_int_is_zero(div->row[pos][0]);

}

static __isl_give isl_printer *print_div(__isl_keep isl_space *dim,

  __isl_keep isl_mat *div, int pos, __isl_take isl_printer *p);

static __isl_give isl_printer *print_term(__isl_keep isl_space *space,

  __isl_keep isl_mat *div,

  isl_int c, unsigned pos, __isl_take isl_printer *p, int latex)

{

  enum isl_dim_type type;

  int print_div_def;

  if (!p || !space)

    return isl_printer_free(p);

  if (pos == 0)

    return isl_printer_print_isl_int(p, c);

  type = pos2type(space, &pos);

  print_div_def = type == isl_dim_div && 
can_print_div_expr(p, div, pos)125
;

  if (isl_int_is_one(c))

    
;10.4k

  else if (isl_int_is_negone(c))

    
p = isl_printer_print_str(p, "-")232
;

  else {

    p = isl_printer_print_isl_int(p, c);

    if (p->output_format == ISL_FORMAT_C || print_div_def)

      p = isl_printer_print_str(p, "*");

  }

  if (print_div_def)

    p = print_div(space, div, pos, p);

  else

    p = print_name(space, p, type, pos, latex);

  return p;

}

static __isl_give isl_printer *print_affine_of_len(__isl_keep isl_space *dim,

  __isl_keep isl_mat *div,

  __isl_take isl_printer *p, isl_int *c, int len)

{

  int i;

  int first;

  for (i = 0, first = 1; i < len; 
++i102k
) {

    int flip = 0;

    if (isl_int_is_zero(c[i]))

      
continue89.4k
;

    if (!first) {

      if (isl_int_is_neg(c[i])) {

        flip = 1;

        isl_int_neg(c[i], c[i]);

        p = isl_printer_print_str(p, " - ");

      } else 

        p = isl_printer_print_str(p, " + ");

    }

    first = 0;

    p = print_term(dim, div, c[i], i, p, 0);

    if (flip)

      
isl_int_neg485
(c[i], c[i]);

  }

  if (first)

    p = isl_printer_print_str(p, "0");

  return p;

}

/* Print an affine expression "c"

 * to "p", with the variable names taken from "space" and

 * the integer division definitions taken from "div".

 */

static __isl_give isl_printer *print_affine(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, isl_int *c)

{

  unsigned n_div;

  unsigned len;

  if (!space || !div)

    return isl_printer_free(p);

  n_div = isl_mat_rows(div);

  len = 1 + isl_space_dim(space, isl_dim_all) + n_div;

  return print_affine_of_len(space, div, p, c, len);

}

/* offset is the offset of local_dim inside data->type of data->space.

 */

static __isl_give isl_printer *print_nested_var_list(__isl_take isl_printer *p,

  __isl_keep isl_space *local_dim, enum isl_dim_type local_type,

  struct isl_print_space_data *data, int offset)

{

  int i;

  if (data->space != local_dim && 
local_type == isl_dim_out114
)

    offset += local_dim->n_in;

  for (i = 0; i < isl_space_dim(local_dim, local_type); 
++i29.4k
) {

    if (i)

      p = isl_printer_print_str(p, ", ");

    if (data->print_dim)

      p = data->print_dim(p, data, offset + i);

    else

      p = print_name(data->space, p, data->type, offset + i,

          data->latex);

  }

  return p;

}

static __isl_give isl_printer *print_var_list(__isl_take isl_printer *p,

  __isl_keep isl_space *space, enum isl_dim_type type)

{

  struct isl_print_space_data data = { .space = space, .type = type };

  return print_nested_var_list(p, space, type, &data, 0);

}

static __isl_give isl_printer *print_nested_map_dim(__isl_take isl_printer *p,

  __isl_keep isl_space *local_dim,

  struct isl_print_space_data *data, int offset);

static __isl_give isl_printer *print_nested_tuple(__isl_take isl_printer *p,

  __isl_keep isl_space *local_dim, enum isl_dim_type local_type,

  struct isl_print_space_data *data, int offset)

{

  const char *name = NULL;

  unsigned n = isl_space_dim(local_dim, local_type);

  if ((local_type == isl_dim_in || 
local_type == isl_dim_out10.9k
)) {

    name = isl_space_get_tuple_name(local_dim, local_type);

    if (name) {

      if (data->latex)

        p = isl_printer_print_str(p, "\\mathrm{");

      p = isl_printer_print_str(p, name);

      if (data->latex)

        p = isl_printer_print_str(p, "}");

    }

  }

  if (!data->latex || 
n != 10
 || 
name0
)

    p = isl_printer_print_str(p, s_open_list[data->latex]);

  if ((local_type == isl_dim_in || 
local_type == isl_dim_out10.9k
) &&

      
local_dim->nested[local_type - isl_dim_in]10.6k
) {

    if (data->space != local_dim && 
local_type == isl_dim_out0
)

      offset += local_dim->n_in;

    p = print_nested_map_dim(p,

        local_dim->nested[local_type - isl_dim_in],

        data, offset);

  } else

    p = print_nested_var_list(p, local_dim, local_type, data,

            offset);

  if (!data->latex || 
n != 10
 || 
name0
)

    p = isl_printer_print_str(p, s_close_list[data->latex]);

  return p;

}

static __isl_give isl_printer *print_tuple(__isl_keep isl_space *dim,

  __isl_take isl_printer *p, enum isl_dim_type type,

  struct isl_print_space_data *data)

{

  data->space = dim;

  data->type = type;

  return print_nested_tuple(p, dim, type, data, 0);

}

static __isl_give isl_printer *print_nested_map_dim(__isl_take isl_printer *p,

  __isl_keep isl_space *local_dim,

  struct isl_print_space_data *data, int offset)

{

  p = print_nested_tuple(p, local_dim, isl_dim_in, data, offset);

  p = isl_printer_print_str(p, s_to[data->latex]);

  p = print_nested_tuple(p, local_dim, isl_dim_out, data, offset);

  return p;

}

__isl_give isl_printer *isl_print_space(__isl_keep isl_space *space,

  __isl_take isl_printer *p, int rational,

  struct isl_print_space_data *data)

{

  if (rational && 
!data->latex0
)

    p = isl_printer_print_str(p, "rat: ");

  if (isl_space_is_params(space))

    ;

  else if (isl_space_is_set(space))

    p = print_tuple(space, p, isl_dim_set, data);

  else {

    p = print_tuple(space, p, isl_dim_in, data);

    p = isl_printer_print_str(p, s_to[data->latex]);

    p = print_tuple(space, p, isl_dim_out, data);

  }

  return p;

}

static __isl_give isl_printer *print_omega_parameters(__isl_keep isl_space *dim,

  __isl_take isl_printer *p)

{

  if (isl_space_dim(dim, isl_dim_param) == 0)

    return p;

  p = isl_printer_start_line(p);

  p = isl_printer_print_str(p, "symbolic ");

  p = print_var_list(p, dim, isl_dim_param);

  p = isl_printer_print_str(p, ";");

  p = isl_printer_end_line(p);

  return p;

}

/* Does the inequality constraint following "i" in "bmap"

 * have an opposite value for the same last coefficient?

 * "last" is the position of the last coefficient of inequality "i".

 * If the next constraint is a div constraint, then it is ignored

 * since div constraints are not printed.

 */

static int next_is_opposite(__isl_keep isl_basic_map *bmap, int i, int last)

{

  unsigned total = isl_basic_map_total_dim(bmap);

  unsigned o_div = isl_basic_map_offset(bmap, isl_dim_div);

  if (i + 1 >= bmap->n_ineq)

    return 0;

  if (isl_seq_last_non_zero(bmap->ineq[i + 1], 1 + total) != last)

    return 0;

  if (last >= o_div) {

    isl_bool is_div;

    is_div = isl_basic_map_is_div_constraint(bmap,

              bmap->ineq[i + 1], last - o_div);

    if (is_div < 0)

      return -1;

    if (is_div)

      return 0;

  }

  return isl_int_abs_eq(bmap->ineq[i][last], bmap->ineq[i + 1][last]) &&

    
!2.61k
isl_int_eq2.61k
(bmap->ineq[i][last], bmap->ineq[i + 1][last]);

}

/* Return a string representation of the operator used when

 * printing a constraint where the LHS is greater than or equal to the LHS

 * (sign > 0) or smaller than or equal to the LHS (sign < 0).

 * If "strict" is set, then return the strict version of the comparison

 * operator.

 */

static const char *constraint_op(int sign, int strict, int latex)

{

  if (strict)

    return sign < 0 ? 
"<"810
 : 
">"441
;

  if (sign < 0)

    return s_le[latex];

  else

    return s_ge[latex];

}

/* Print one side of a constraint "c" to "p", with

 * the variable names taken from "space" and the integer division definitions

 * taken from "div".

 * "last" is the position of the last non-zero coefficient.

 * Let c' be the result of zeroing out this coefficient, then

 * the partial constraint

 *

 *  c' op

 *

 * is printed.

 */

static __isl_give isl_printer *print_half_constraint(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div,

  isl_int *c, int last, const char *op, int latex)

{

  isl_int_set_si(c[last], 0);

  p = print_affine(p, space, div, c);

  p = isl_printer_print_str(p, " ");

  p = isl_printer_print_str(p, op);

  p = isl_printer_print_str(p, " ");

  return p;

}

/* Print a constraint "c" to "p", with the variable names

 * taken from "space" and the integer division definitions taken from "div".

 * "last" is the position of the last non-zero coefficient, which is

 * moreover assumed to be negative.

 * Let c' be the result of zeroing out this coefficient, then

 * the constraint is printed in the form

 *

 *  -c[last] op c'

 */

static __isl_give isl_printer *print_constraint(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div,

  isl_int *c, int last, const char *op, int latex)

{

  isl_int_abs(c[last], c[last]);

  p = print_term(space, div, c[last], last, p, latex);

  p = isl_printer_print_str(p, " ");

  p = isl_printer_print_str(p, op);

  p = isl_printer_print_str(p, " ");

  isl_int_set_si(c[last], 0);

  p = print_affine(p, space, div, c);

  return p;

}

/* Given an integer division

 *

 *  floor(f/m)

 *

 * at position "pos" in "div", print the corresponding modulo expression

 *

 *  (f) mod m

 *

 * to "p".  The variable names are taken from "space", while any

 * nested integer division definitions are taken from "div".

 */

static __isl_give isl_printer *print_mod(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, int pos,

  int latex)

{

  if (!p || !div)

    return isl_printer_free(p);

  p = isl_printer_print_str(p, "(");

  p = print_affine_of_len(space, div, p,

        div->row[pos] + 1, div->n_col - 1);

  p = isl_printer_print_str(p, ") ");

  p = isl_printer_print_str(p, s_mod[latex]);

  p = isl_printer_print_str(p, " ");

  p = isl_printer_print_isl_int(p, div->row[pos][0]);

  return p;

}

/* Can the equality constraints "c" be printed as a modulo constraint?

 * In particular, is of the form

 *

 *  f - a m floor(g/m) = 0,

 *

 * with c = -a m the coefficient at position "pos"?

 * Return the position of the corresponding integer division if so.

 * Return the number of integer divisions if not.

 * Return -1 on error.

 *

 * Modulo constraints are currently not printed in C format.

 * Other than that, "pos" needs to correspond to an integer division

 * with explicit representation and "c" needs to be a multiple

 * of the denominator of the integer division.

 */

static int print_as_modulo_pos(__isl_keep isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, unsigned pos,

  isl_int c)

{

  isl_bool can_print;

  unsigned n_div;

  enum isl_dim_type type;

  if (!p || !space)

    return -1;

  n_div = isl_mat_rows(div);

  if (p->output_format == ISL_FORMAT_C)

    
return n_div0
;

  type = pos2type(space, &pos);

  if (type != isl_dim_div)

    return n_div;

  can_print = can_print_div_expr(p, div, pos);

  if (can_print < 0)

    return -1;

  if (!can_print)

    return n_div;

  if (!isl_int_is_divisible_by(c, div->row[pos][0]))

    
return n_div2
;

  return pos;

}

/* Print equality constraint "c" to "p" as a modulo constraint,

 * with the variable names taken from "space" and

 * the integer division definitions taken from "div".

 * "last" is the position of the last non-zero coefficient, which is

 * moreover assumed to be negative and a multiple of the denominator

 * of the corresponding integer division.  "div_pos" is the corresponding

 * position in the sequence of integer divisions.

 *

 * The equality is of the form

 *

 *  f - a m floor(g/m) = 0.

 *

 * Print it as

 *

 *  a (g mod m) = -f + a g

 */

static __isl_give isl_printer *print_eq_mod_constraint(

  __isl_take isl_printer *p, __isl_keep isl_space *space,

  __isl_keep isl_mat *div, unsigned div_pos,

  isl_int *c, int last, int latex)

{

  isl_ctx *ctx;

  int multiple;

  ctx = isl_printer_get_ctx(p);

  isl_int_divexact(c[last], c[last], div->row[div_pos][0]);

  isl_int_abs(c[last], c[last]);

  multiple = !isl_int_is_one(c[last]);

  if (multiple) {

    p = isl_printer_print_isl_int(p, c[last]);

    p = isl_printer_print_str(p, "*(");

  }

  p = print_mod(p, space, div, div_pos, latex);

  if (multiple)

    p = isl_printer_print_str(p, ")");

  p = isl_printer_print_str(p, " = ");

  isl_seq_combine(c, ctx->negone, c,

          c[last], div->row[div_pos] + 1, last);

  isl_int_set_si(c[last], 0);

  p = print_affine(p, space, div, c);

  return p;

}

/* Print equality constraint "c" to "p", with the variable names

 * taken from "space" and the integer division definitions taken from "div".

 * "last" is the position of the last non-zero coefficient, which is

 * moreover assumed to be negative.

 *

 * If possible, print the equality constraint as a modulo constraint.

 */

static __isl_give isl_printer *print_eq_constraint(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, isl_int *c,

  int last, int latex)

{

  unsigned n_div;

  int div_pos;

  n_div = isl_mat_rows(div);

  div_pos = print_as_modulo_pos(p, space, div, last, c[last]);

  if (div_pos < 0)

    return isl_printer_free(p);

  if (div_pos < n_div)

    return print_eq_mod_constraint(p, space, div, div_pos,

            c, last, latex);

  return print_constraint(p, space, div, c, last, "=", latex);

}

/* Print the constraints of "bmap" to "p".

 * The names of the variables are taken from "space" and

 * the integer division definitions are taken from "div".

 * Div constraints are only printed in "dump" mode.

 * The constraints are sorted prior to printing (except in "dump" mode).

 *

 * If x is the last variable with a non-zero coefficient,

 * then a lower bound

 *

 *  f - a x >= 0

 *

 * is printed as

 *

 *  a x <= f

 *

 * while an upper bound

 *

 *  f + a x >= 0

 *

 * is printed as

 *

 *  a x >= -f

 *

 * If the next constraint has an opposite sign for the same last coefficient,

 * then it is printed as

 *

 *  f >= a x

 *

 * or

 *

 *  -f <= a x

 *

 * instead.  In fact, the "a x" part is not printed explicitly, but

 * reused from the next constraint, which is therefore treated as

 * a first constraint in the conjunction.

 *

 * If the constant term of "f" is -1, then "f" is replaced by "f + 1" and

 * the comparison operator is replaced by the strict variant.

 * Essentially, ">= 1" is replaced by "> 0".

 */

static __isl_give isl_printer *print_constraints(__isl_keep isl_basic_map *bmap,

  __isl_keep isl_space *space, __isl_keep isl_mat *div,

  __isl_take isl_printer *p, int latex)

{

  int i;

  isl_vec *c = NULL;

  int rational = ISL_F_ISSET(bmap, ISL_BASIC_MAP_RATIONAL);

  unsigned total = isl_basic_map_total_dim(bmap);

  unsigned o_div = isl_basic_map_offset(bmap, isl_dim_div);

  int first = 1;

  int dump;

  if (!p)

    return NULL;

  bmap = isl_basic_map_copy(bmap);

  dump = p->dump;

  if (!dump)

    bmap = isl_basic_map_sort_constraints(bmap);

  if (!bmap)

    goto error;

  c = isl_vec_alloc(bmap->ctx, 1 + total);

  if (!c)

    goto error;

  
for (i = bmap->n_eq - 1; 3.67k
i >= 0; 
--i316
) {

    int l = isl_seq_last_non_zero(bmap->eq[i], 1 + total);

    if (l < 0) {

      if (i != bmap->n_eq - 1)

        p = isl_printer_print_str(p, s_and[latex]);

      p = isl_printer_print_str(p, "0 = 0");

      continue;

    }

    if (!first)

      p = isl_printer_print_str(p, s_and[latex]);

    if (isl_int_is_neg(bmap->eq[i][l]))

      
isl_seq_cpy(c->el, bmap->eq[i], 1 + total)0
;

    else

      isl_seq_neg(c->el, bmap->eq[i], 1 + total);

    p = print_eq_constraint(p, space, div, c->el, l, latex);

    first = 0;

  }

  for (i = 0; i < bmap->n_ineq; 
++i7.79k
) {

    int l = isl_seq_last_non_zero(bmap->ineq[i], 1 + total);

    int strict;

    int s;

    const char *op;

    if (l < 0)

      continue;

    if (!dump && l >= o_div &&

        
can_print_div_expr(p, div, l - o_div)231
) {

      isl_bool is_div;

      is_div = isl_basic_map_is_div_constraint(bmap,

                bmap->ineq[i], l - o_div);

      if (is_div < 0)

        goto error;

      if (is_div)

        continue;

    }

    if (!first)

      p = isl_printer_print_str(p, s_and[latex]);

    s = isl_int_sgn(bmap->ineq[i][l]);

    strict = !rational && isl_int_is_negone(bmap->ineq[i][0]);

    if (s < 0)

      isl_seq_cpy(c->el, bmap->ineq[i], 1 + total);

    else

      isl_seq_neg(c->el, bmap->ineq[i], 1 + total);

    if (strict)

      
isl_int_set_si1.25k
(c->el[0], 0);

    if (!dump && next_is_opposite(bmap, i, l)) {

      op = constraint_op(-s, strict, latex);

      p = print_half_constraint(p, space, div, c->el, l,

            op, latex);

      first = 1;

    } else {

      op = constraint_op(s, strict, latex);

      p = print_constraint(p, space, div, c->el, l,

            op, latex);

      first = 0;

    }

  }

  isl_basic_map_free(bmap);

  isl_vec_free(c);

  return p;

error:

  isl_basic_map_free(bmap);

  isl_vec_free(c);

  isl_printer_free(p);

  return NULL;

}

static __isl_give isl_printer *print_div(__isl_keep isl_space *dim,

  __isl_keep isl_mat *div, int pos, __isl_take isl_printer *p)

{

  int c;

  if (!p || !div)

    return isl_printer_free(p);

  c = p->output_format == ISL_FORMAT_C;

  p = isl_printer_print_str(p, c ? 
"floord("0
 : "floor((");

  p = print_affine_of_len(dim, div, p,

        div->row[pos] + 1, div->n_col - 1);

  p = isl_printer_print_str(p, c ? 
", "0
 : ")/");

  p = isl_printer_print_isl_int(p, div->row[pos][0]);

  p = isl_printer_print_str(p, ")");

  return p;

}

/* Print a comma separated list of div names, except those that have

 * a definition that can be printed.

 * If "print_defined_divs" is set, then those div names are printed

 * as well, along with their definitions.

 */

static __isl_give isl_printer *print_div_list(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, int latex,

  int print_defined_divs)

{

  int i;

  int first = 1;

  unsigned n_div;

  if (!p || !space || !div)

    return isl_printer_free(p);

  n_div = isl_mat_rows(div);

  for (i = 0; i < n_div; 
++i4
) {

    if (!print_defined_divs && can_print_div_expr(p, div, i))

      continue;

    if (!first)

      p = isl_printer_print_str(p, ", ");

    p = print_name(space, p, isl_dim_div, i, latex);

    first = 0;

    if (!can_print_div_expr(p, div, i))

      continue;

    p = isl_printer_print_str(p, " = ");

    p = print_div(space, div, i, p);

  }

  return p;

}

/* Does printing an object with local variables described by "div"

 * require an "exists" clause?

 * That is, are there any local variables without an explicit representation?

 * An exists clause is also needed in "dump" mode because

 * explicit div representations are not printed inline in that case.

 */

static isl_bool need_exists(__isl_keep isl_printer *p, __isl_keep isl_mat *div)

{

  int i, n;

  if (!p || !div)

    return isl_bool_error;

  n = isl_mat_rows(div);

  if (n == 0)

    return isl_bool_false;

  if (p->dump)

    return isl_bool_true;

  
for (i = 0; 161
i < n; 
++i177
)

    if (!can_print_div_expr(p, div, i))

      return isl_bool_true;

  
return isl_bool_false159
;

}

/* Print the start of an exists clause, i.e.,

 *

 *  (exists variables:

 *

 * In dump mode, local variables with an explicit definition are printed

 * as well because they will not be printed inline.

 */

static __isl_give isl_printer *open_exists(__isl_take isl_printer *p,

  __isl_keep isl_space *space, __isl_keep isl_mat *div, int latex)

{

  int dump;

  if (!p)

    return NULL;

  dump = p->dump;

  p = isl_printer_print_str(p, s_open_exists[latex]);

  p = print_div_list(p, space, div, latex, dump);

  p = isl_printer_print_str(p, ": ");

  return p;

}

/* Remove the explicit representations of all local variables in "div".

 */

static __isl_give isl_mat *mark_all_unknown(__isl_take isl_mat *div)

{

  int i, n_div;

  if (!div)

    return NULL;

  n_div = isl_mat_rows(div);

  for (i = 0; i < n_div; ++i)

    div = isl_mat_set_element_si(div, i, 0, 0);

  return div;

}

/* Print the constraints of "bmap" to "p".

 * The names of the variables are taken from "space".

 * "latex" is set if the constraints should be printed in LaTeX format.

 * Do not print inline explicit div representations in "dump" mode.

 */

static __isl_give isl_printer *print_disjunct(__isl_keep isl_basic_map *bmap,

  __isl_keep isl_space *space, __isl_take isl_printer *p, int latex)

{

  int dump;

  isl_mat *div;

  isl_bool exists;

  if (!p)

    return NULL;

  dump = p->dump;

  div = isl_basic_map_get_divs(bmap);

  exists = need_exists(p, div);

  if (exists >= 0 && exists)

    p = open_exists(p, space, div, latex);

  if (dump)

    div = mark_all_unknown(div);

  p = print_constraints(bmap, space, div, p, latex);

  isl_mat_free(div);

  if (exists >= 0 && exists)

    p = isl_printer_print_str(p, s_close_exists[latex]);

  return p;

}

/* Print a colon followed by the constraints of "bmap"

 * to "p", provided there are any constraints.

 * The names of the variables are taken from "space".

 * "latex" is set if the constraints should be printed in LaTeX format.

 */

static __isl_give isl_printer *print_optional_disjunct(

  __isl_keep isl_basic_map *bmap, __isl_keep isl_space *space,

  __isl_take isl_printer *p, int latex)

{

  if (isl_basic_map_plain_is_universe(bmap))

    return p;

  p = isl_printer_print_str(p, ": ");

  p = print_disjunct(bmap, space, p, latex);

  return p;

}

static __isl_give isl_printer *basic_map_print_omega(

  __isl_keep isl_basic_map *bmap, __isl_take isl_printer *p)

{

  p = isl_printer_print_str(p, "{ [");

  p = print_var_list(p, bmap->dim, isl_dim_in);

  p = isl_printer_print_str(p, "] -> [");

  p = print_var_list(p, bmap->dim, isl_dim_out);

  p = isl_printer_print_str(p, "] ");

  p = print_optional_disjunct(bmap, bmap->dim, p, 0);

  p = isl_printer_print_str(p, " }");