1 #include "isl_basis_reduction.h"
6 /* Call callback->add with the current sample value of the tableau "tab".
8 static int add_solution(struct isl_tab
*tab
, struct isl_scan_callback
*callback
)
10 struct isl_vec
*sample
;
14 sample
= isl_tab_get_sample_value(tab
);
18 return callback
->add(callback
, sample
);
21 static int scan_0D(struct isl_basic_set
*bset
,
22 struct isl_scan_callback
*callback
)
24 struct isl_vec
*sample
;
26 sample
= isl_vec_alloc(bset
->ctx
, 1);
27 isl_basic_set_free(bset
);
32 isl_int_set_si(sample
->el
[0], 1);
34 return callback
->add(callback
, sample
);
37 /* Look for all integer points in "bset", which is assumed to be unbounded,
38 * and call callback->add on each of them.
40 * We first compute a reduced basis for the set and then scan
41 * the set in the directions of this basis.
42 * We basically perform a depth first search, where in each level i
43 * we compute the range in the i-th basis vector direction, given
44 * fixed values in the directions of the previous basis vector.
45 * We then add an equality to the tableau fixing the value in the
46 * direction of the current basis vector to each value in the range
47 * in turn and then continue to the next level.
49 * The search is implemented iteratively. "level" identifies the current
50 * basis vector. "init" is true if we want the first value at the current
51 * level and false if we want the next value.
52 * Solutions are added in the leaves of the search tree, i.e., after
53 * we have fixed a value in each direction of the basis.
55 int isl_basic_set_scan(struct isl_basic_set
*bset
,
56 struct isl_scan_callback
*callback
)
59 struct isl_mat
*B
= NULL
;
60 struct isl_tab
*tab
= NULL
;
63 struct isl_tab_undo
**snap
;
66 enum isl_lp_result res
;
71 dim
= isl_basic_set_total_dim(bset
);
73 return scan_0D(bset
, callback
);
75 min
= isl_vec_alloc(bset
->ctx
, dim
);
76 max
= isl_vec_alloc(bset
->ctx
, dim
);
77 snap
= isl_alloc_array(bset
->ctx
, struct isl_tab_undo
*, dim
);
79 if (!min
|| !max
|| !snap
)
82 tab
= isl_tab_from_basic_set(bset
);
86 tab
->basis
= isl_mat_identity(bset
->ctx
, 1 + dim
);
88 tab
= isl_tab_compute_reduced_basis(tab
);
91 B
= isl_mat_copy(tab
->basis
);
101 res
= isl_tab_min(tab
, B
->row
[1 + level
],
102 bset
->ctx
->one
, &min
->el
[level
], NULL
, 0);
103 if (res
== isl_lp_empty
)
105 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
107 isl_seq_neg(B
->row
[1 + level
] + 1,
108 B
->row
[1 + level
] + 1, dim
);
109 res
= isl_tab_min(tab
, B
->row
[1 + level
],
110 bset
->ctx
->one
, &max
->el
[level
], NULL
, 0);
111 isl_seq_neg(B
->row
[1 + level
] + 1,
112 B
->row
[1 + level
] + 1, dim
);
113 isl_int_neg(max
->el
[level
], max
->el
[level
]);
114 if (res
== isl_lp_empty
)
116 if (res
== isl_lp_error
|| res
== isl_lp_unbounded
)
118 snap
[level
] = isl_tab_snap(tab
);
120 isl_int_add_ui(min
->el
[level
], min
->el
[level
], 1);
122 if (empty
|| isl_int_gt(min
->el
[level
], max
->el
[level
])) {
126 if (isl_tab_rollback(tab
, snap
[level
]) < 0)
130 isl_int_neg(B
->row
[1 + level
][0], min
->el
[level
]);
131 tab
= isl_tab_add_valid_eq(tab
, B
->row
[1 + level
]);
132 isl_int_set_si(B
->row
[1 + level
][0], 0);
133 if (level
< dim
- 1) {
138 if (add_solution(tab
, callback
) < 0)
141 if (isl_tab_rollback(tab
, snap
[level
]) < 0)
149 isl_basic_set_free(bset
);
157 isl_basic_set_free(bset
);