http://gcc.gnu.org/bugzilla/show_bug.cgi?id=50439
bagnara at cs dot unipr.it changed:
What|Removed |Added
CC||bagnara at cs dot unipr.it
--- Comment #5 from bagnara at cs dot unipr.it 2012-04-06 13:49:57 UTC ---
Here is a sketch (100% untested) of what can be done without intervening on the
specification of the function, that is, without giving up. The original
implementation was inefficient, by the way: if one element of the powerset was
found not to be empty, all the other elements were tested anyway instead of
immediately returning false. Whether it is best to try the MIP solver or the
PIP solver first is something to be determined experimentally.
bool
ppl_powerset_is_empty (ppl_Pointset_Powerset_C_Polyhedron_t ps)
{
ppl_dimension_type d;
ppl_Constraint_System_const_iterator_t first, last;
ppl_Pointset_Powerset_C_Polyhedron_iterator_t it, end;
bool has_integer_solutions = false;
/* FIXME: the following values should be determined experimentally. */
unsigned weight = 2;
unsigned weight_increment = 5000;
unsigned timeouts;
if (ppl_Pointset_Powerset_C_Polyhedron_is_empty (ps))
return true;
while (true)
{
ppl_Pointset_Powerset_C_Polyhedron_space_dimension (ps, d);
ppl_new_Constraint_System_const_iterator (first);
ppl_new_Constraint_System_const_iterator (last);
ppl_new_Pointset_Powerset_C_Polyhedron_iterator (it);
ppl_new_Pointset_Powerset_C_Polyhedron_iterator (end);
timeouts = 0;
for (ppl_Pointset_Powerset_C_Polyhedron_iterator_begin (ps, it),
ppl_Pointset_Powerset_C_Polyhedron_iterator_end (ps, end);
!ppl_Pointset_Powerset_C_Polyhedron_iterator_equal_test (it, end);
ppl_Pointset_Powerset_C_Polyhedron_iterator_increment (it))
{
ppl_const_Polyhedron_t ph;
ppl_const_Constraint_System_t pcs;
ppl_Linear_Expression_t le;
ppl_MIP_Problem_t mip;
int ppl_result;
ppl_Pointset_Powerset_C_Polyhedron_iterator_dereference (it, ph);
ppl_Polyhedron_get_constraints (ph, pcs);
/* Try with the MIP solver first. */
ppl_new_Linear_Expression (le);
ppl_new_MIP_Problem (mip, d, pcs, le,
PPL_OPTIMIZATION_MODE_MAXIMIZATION);
ppl_set_deterministic_timeout (weight);
ppl_result = ppl_MIP_Problem_is_satisfiable (mip);
ppl_reset_deterministic_timeout ();
ppl_delete_MIP_Problem (mip);
if (ppl_result == PPL_TIMEOUT_EXCEPTION)
{
/* Deterministic timeout expired: try with the PIP solver. */
ppl_PIP_Problem_t pip;
ppl_Constraint_System_begin (pcs, first);
ppl_Constraint_System_end (pcs, last);
ppl_new_PIP_Problem_from_constraints (pip, d, first, last, 0,
NULL);
ppl_set_deterministic_timeout (weight);
ppl_result = ppl_PIP_Problem_is_satisfiable (pip);
ppl_reset_deterministic_timeout ();
ppl_delete_PIP_Problem (pip);
if (ppl_result == PPL_TIMEOUT_EXCEPTION)
++timeouts;
else if (ppl_result 0)
{
has_integer_solutions = true;
break;
}
}
else if (ppl_result 0)
{
has_integer_solutions = true;
break;
}
}
ppl_delete_Constraint_System_const_iterator (first);
ppl_delete_Constraint_System_const_iterator (last);
ppl_delete_Pointset_Powerset_C_Polyhedron_iterator (it);
ppl_delete_Pointset_Powerset_C_Polyhedron_iterator (end);
/* If there were no timeouts, then we have the answer. */
if (timeouts == 0)
return !has_integer_solutions;
if (weight = UINT_MAX - weight_increment)
weight += weight_increment;
}
}
