#include "isl_sample.h"
#include <isl_mat_private.h>
#include <isl_aff_private.h>
+#include <isl_options_private.h>
#include <isl_config.h>
/*
if (tab->empty && !sol->add_empty)
return;
+ if (sol->context->op->is_empty(sol->context))
+ return;
bset = sol_domain(sol);
return ineq;
}
+/* Normalize a div expression of the form
+ *
+ * [(g*f(x) + c)/(g * m)]
+ *
+ * with c the constant term and f(x) the remaining coefficients, to
+ *
+ * [(f(x) + [c/g])/m]
+ */
+static void normalize_div(__isl_keep isl_vec *div)
+{
+ isl_ctx *ctx = isl_vec_get_ctx(div);
+ int len = div->size - 2;
+
+ isl_seq_gcd(div->el + 2, len, &ctx->normalize_gcd);
+ isl_int_gcd(ctx->normalize_gcd, ctx->normalize_gcd, div->el[0]);
+
+ if (isl_int_is_one(ctx->normalize_gcd))
+ return;
+
+ isl_int_divexact(div->el[0], div->el[0], ctx->normalize_gcd);
+ isl_int_fdiv_q(div->el[1], div->el[1], ctx->normalize_gcd);
+ isl_seq_scale_down(div->el + 2, div->el + 2, ctx->normalize_gcd, len);
+}
+
/* Return a integer division for use in a parametric cut based on the given row.
* In particular, let the parametric constant of the row be
*
isl_int_set(div->el[0], tab->mat->row[row][0]);
get_row_parameter_line(tab, row, div->el + 1);
- div = isl_vec_normalize(div);
+ normalize_div(div);
isl_seq_neg(div->el + 1, div->el + 1, div->size - 1);
isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
isl_int_set(div->el[0], tab->mat->row[row][0]);
get_row_parameter_line(tab, row, div->el + 1);
- div = isl_vec_normalize(div);
+ normalize_div(div);
isl_seq_fdiv_r(div->el + 1, div->el + 1, div->el[0], div->size - 1);
return div;
return tab->con[r].index;
}
+#define CUT_ALL 1
+#define CUT_ONE 0
+
/* Given a non-parametric tableau, add cuts until an integer
* sample point is obtained or until the tableau is determined
* to be integer infeasible.
* combination of variables/constraints plus a non-integral constant,
* then there is no way to obtain an integer point and we return
* a tableau that is marked empty.
+ * The parameter cutting_strategy controls the strategy used when adding cuts
+ * to remove non-integer points. CUT_ALL adds all possible cuts
+ * before continuing the search. CUT_ONE adds only one cut at a time.
*/
-static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab)
+static struct isl_tab *cut_to_integer_lexmin(struct isl_tab *tab,
+ int cutting_strategy)
{
int var;
int row;
row = add_cut(tab, row);
if (row < 0)
goto error;
+ if (cutting_strategy == CUT_ONE)
+ break;
} while ((var = next_non_integer_var(tab, var, &flags)) != -1);
if (restore_lexmin(tab) < 0)
goto error;
if (isl_tab_push_basis(tab) < 0)
goto error;
- tab = cut_to_integer_lexmin(tab);
+ tab = cut_to_integer_lexmin(tab, CUT_ALL);
if (!tab)
goto error;
{
struct isl_tab *tab;
- bset = isl_basic_set_cow(bset);
if (!bset)
return NULL;
tab = tab_for_lexmin((struct isl_basic_map *)bset, NULL, 1, 0);
}
}
- cgbr->shifted = isl_tab_from_basic_set(bset);
+ cgbr->shifted = isl_tab_from_basic_set(bset, 0);
for (i = 0; i < bset->n_ineq; ++i)
isl_int_set(bset->ineq[i][0], cst->el[i]);
cgbr->cone = isl_tab_from_recession_cone(bset, 0);
if (!cgbr->cone)
return NULL;
- if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
+ if (isl_tab_track_bset(cgbr->cone,
+ isl_basic_set_copy(bset)) < 0)
return NULL;
}
if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
cgbr->cone = isl_tab_from_recession_cone(bset, 0);
if (!cgbr->cone)
goto error;
- if (isl_tab_track_bset(cgbr->cone, isl_basic_set_dup(bset)) < 0)
+ if (isl_tab_track_bset(cgbr->cone,
+ isl_basic_set_copy(bset)) < 0)
goto error;
}
if (isl_tab_detect_implicit_equalities(cgbr->cone) < 0)
cgbr->shifted = NULL;
cgbr->cone = NULL;
- cgbr->tab = isl_tab_from_basic_set(dom);
+ cgbr->tab = isl_tab_from_basic_set(dom, 1);
cgbr->tab = isl_tab_init_samples(cgbr->tab);
if (!cgbr->tab)
goto error;
- if (isl_tab_track_bset(cgbr->tab,
- isl_basic_set_cow(isl_basic_set_copy(dom))) < 0)
- goto error;
check_gbr_integer_feasible(cgbr);
return &cgbr->context;
isl_int_set(aff->v->el[0], M->row[0][0]);
isl_seq_cpy(aff->v->el + 1, M->row[i], M->n_col);
}
+ aff = isl_aff_normalize(aff);
list = isl_aff_list_add(list, aff);
}
isl_local_space_free(ls);
int side, base;
if (init) {
- tab = cut_to_integer_lexmin(tab);
+ tab = cut_to_integer_lexmin(tab, CUT_ONE);
if (!tab)
goto error;
if (tab->empty)
isl_local_space_free(ls);
isl_mat_free(M);
dom = isl_basic_set_simplify(dom);
+ dom = isl_basic_set_finalize(dom);
pma = isl_pw_multi_aff_alloc(isl_set_from_basic_set(dom), maff);
sol->pma = isl_pw_multi_aff_add_disjoint(sol->pma, pma);
if (!sol->pma)