From 1fc6c100aa269b09a0ca4119ab9bb3951e2a756e Mon Sep 17 00:00:00 2001
From: Sven Verdoolaege <skimo@kotnet.org>
Date: Fri, 7 Aug 2009 10:07:44 +0200
Subject: [PATCH] isl_tab: add support for keeping track of samples

---
 isl_tab.c | 13 +++++++++++++
 isl_tab.h | 11 +++++++++++
 2 files changed, 24 insertions(+)

diff --git a/isl_tab.c b/isl_tab.c
index bbe0404..e51beb8 100644
--- a/isl_tab.c
+++ b/isl_tab.c
@@ -171,6 +171,7 @@ void isl_tab_free(struct isl_tab *tab)
 	free(tab->row_var);
 	free(tab->col_var);
 	free(tab->row_sign);
+	isl_mat_free(tab->samples);
 	free(tab);
 }
 
@@ -216,6 +217,13 @@ struct isl_tab *isl_tab_dup(struct isl_tab *tab)
 		for (i = 0; i < tab->n_row; ++i)
 			dup->row_sign[i] = tab->row_sign[i];
 	}
+	if (tab->samples) {
+		dup->samples = isl_mat_dup(tab->samples);
+		if (!dup->samples)
+			goto error;
+		dup->n_sample = tab->n_sample;
+		dup->n_outside = tab->n_outside;
+	}
 	dup->n_row = tab->n_row;
 	dup->n_con = tab->n_con;
 	dup->n_eq = tab->n_eq;
@@ -2094,11 +2102,16 @@ static int perform_undo(struct isl_tab *tab, struct isl_tab_undo *undo)
 		break;
 	case isl_tab_undo_bset_div:
 		isl_basic_set_free_div(tab->bset, 1);
+		if (tab->samples)
+			tab->samples->n_col--;
 		break;
 	case isl_tab_undo_saved_basis:
 		if (restore_basis(tab, undo->u.col_var) < 0)
 			return -1;
 		break;
+	case isl_tab_undo_drop_sample:
+		tab->n_outside--;
+		break;
 	default:
 		isl_assert(tab->mat->ctx, 0, return -1);
 	}
diff --git a/isl_tab.h b/isl_tab.h
index 6231d35..9af71b7 100644
--- a/isl_tab.h
+++ b/isl_tab.h
@@ -28,6 +28,7 @@ enum isl_tab_undo_type {
 	isl_tab_undo_bset_eq,
 	isl_tab_undo_bset_div,
 	isl_tab_undo_saved_basis,
+	isl_tab_undo_drop_sample,
 };
 
 union isl_tab_undo_val {
@@ -90,6 +91,12 @@ struct isl_tab_undo {
  * or all redundant rows are detected.
  * isl_tab_detect_equalities and isl_tab_detect_redundant can be used
  * to perform and exhaustive search for dead columns and redundant rows.
+ *
+ * The samples matrix contains "n_sample" integer points that have at some
+ * point been elements satisfying the tableau.  The first "n_outside"
+ * of them no longer satisfy the tableau.  They are kept because they
+ * can be reinstated during rollback when the constraint that cut them
+ * out is removed.
  */
 enum isl_tab_row_sign {
 	isl_tab_row_unknown = 0,
@@ -124,6 +131,10 @@ struct isl_tab {
 	struct isl_vec *dual;
 	struct isl_basic_set *bset;
 
+	unsigned n_sample;
+	unsigned n_outside;
+	struct isl_mat *samples;
+
 	unsigned need_undo : 1;
 	unsigned rational : 1;
 	unsigned empty : 1;
-- 
2.7.4