[PPL-devel] [GIT] ppl/ppl(master): Drafted the implementation of methods drop_some_non_integer_points().
Roberto Bagnara
bagnara at cs.unipr.it
Wed Mar 24 18:40:52 CET 2010
Module: ppl/ppl
Branch: master
Commit: ce7681699c3e6056ce77eb9492ae8a051bb00dc3
URL: http://www.cs.unipr.it/git/gitweb.cgi?p=ppl/ppl.git;a=commit;h=ce7681699c3e6056ce77eb9492ae8a051bb00dc3
Author: Roberto Bagnara <bagnara at cs.unipr.it>
Date: Wed Mar 24 21:37:52 2010 +0400
Drafted the implementation of methods drop_some_non_integer_points().
---
src/Polyhedron.defs.hh | 18 ++++++
src/Polyhedron.inlines.hh | 13 ++++
src/Polyhedron_nonpublic.cc | 135 +++++++++++++++++++++++++++++++++++++++++++
3 files changed, 166 insertions(+), 0 deletions(-)
diff --git a/src/Polyhedron.defs.hh b/src/Polyhedron.defs.hh
index 3a1f563..0a3c86b 100644
--- a/src/Polyhedron.defs.hh
+++ b/src/Polyhedron.defs.hh
@@ -2698,6 +2698,24 @@ protected:
//@} // Exception Throwers
#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
+ /*! \brief
+ Possibly tightens \p *this by dropping some points with non-integer
+ coordinates for the space dimensions corresponding to \p *pvars.
+
+ \param pvars
+ When nonzero, points with non-integer coordinates for the
+ variables/space-dimensions contained in \p *pvars can be discarded.
+
+ \param complexity
+ The maximal complexity of any algorithms used.
+
+ \note
+ Currently there is no optimality guarantee, not even if
+ \p complexity is <CODE>ANY_COMPLEXITY</CODE>.
+ */
+ void drop_some_non_integer_points(const Variables_Set* pvars,
+ Complexity_Class complexity);
+
//! Helper function that overapproximates an interval linear form.
/*!
\param lf
diff --git a/src/Polyhedron.inlines.hh b/src/Polyhedron.inlines.hh
index 8f3aeef..2909057 100644
--- a/src/Polyhedron.inlines.hh
+++ b/src/Polyhedron.inlines.hh
@@ -431,6 +431,19 @@ Polyhedron::strictly_contains(const Polyhedron& y) const {
return x.contains(y) && !y.contains(x);
}
+inline void
+Polyhedron::drop_some_non_integer_points(Complexity_Class complexity) {
+ drop_some_non_integer_points(static_cast<const Variables_Set*>(0),
+ complexity);
+}
+
+inline void
+Polyhedron::drop_some_non_integer_points(const Variables_Set& vars,
+ Complexity_Class complexity) {
+ drop_some_non_integer_points(&vars, complexity);
+}
+
+
namespace Interfaces {
inline bool
diff --git a/src/Polyhedron_nonpublic.cc b/src/Polyhedron_nonpublic.cc
index 1cd9fb2..a54c639 100644
--- a/src/Polyhedron_nonpublic.cc
+++ b/src/Polyhedron_nonpublic.cc
@@ -2075,6 +2075,141 @@ PPL::Polyhedron::BFT00_poly_hull_assign_if_exact(const Polyhedron& y) {
}
void
+PPL::Polyhedron::drop_some_non_integer_points(const Variables_Set* pvars,
+ Complexity_Class complexity) {
+ // There is nothing to do for an empty set of variables.
+ if (pvars != 0 && pvars->empty())
+ return;
+
+ // Any empty polyhedron does not contain integer points.
+ if (marked_empty())
+ return;
+
+ // A zero-dimensional, universe polyhedron has, by convention, an
+ // integer point.
+ if (space_dim == 0)
+ set_empty();
+
+ // The constraints (possibly with pending rows) are required.
+ if (has_pending_generators()) {
+ // Processing of pending generators is exponential in the worst case.
+ if (complexity != ANY_COMPLEXITY)
+ return;
+ else
+ process_pending_generators();
+ }
+ if (!constraints_are_up_to_date()) {
+ // Constraints update is exponential in the worst case.
+ if (complexity != ANY_COMPLEXITY)
+ return;
+ else
+ update_constraints();
+ }
+
+ PPL_ASSERT(!has_pending_generators() && constraints_are_up_to_date());
+
+ bool changed = false;
+ const dimension_type eps_index = space_dim + 1;
+ PPL_DIRTY_TEMP_COEFFICIENT(gcd);
+
+ for (dimension_type j = con_sys.num_rows(); j-- > 0; ) {
+ Constraint& c = con_sys[j];
+ if (c.is_tautological())
+ goto next_constraint;
+
+ if (pvars != 0) {
+ for (dimension_type i = space_dim; i-- > 0; )
+ if (c[i+1] != 0 && pvars->find(i) == pvars->end())
+ goto next_constraint;
+ }
+
+ if (!is_necessarily_closed()) {
+ // Transform all strict inequalities into non-strict ones,
+ // with the inhomogeneous term incremented by 1.
+ if (c[eps_index] < 0 && !c.is_tautological()) {
+ c[eps_index] = 0;
+ ++c[0];
+ changed = true;
+ }
+ }
+
+ {
+ // Compute the GCD of all the homogeneous terms.
+ dimension_type i = space_dim+1;
+ while (i > 1) {
+ const Coefficient& c_i = c[--i];
+ if (const int c_i_sign = sgn(c_i)) {
+ gcd = c_i;
+ if (c_i_sign < 0)
+ neg_assign(gcd);
+ goto compute_gcd;
+ }
+ }
+ // We reach this point only if all the coefficients were zero.
+ goto maybe_normalize;
+
+ compute_gcd:
+ if (gcd == 1)
+ goto maybe_normalize;
+ while (i > 1) {
+ const Coefficient& c_i = c[--i];
+ if (c_i != 0) {
+ // See the comment in Row::normalize().
+ gcd_assign(gcd, c_i, gcd);
+ if (gcd == 1)
+ goto maybe_normalize;
+ }
+ }
+ PPL_ASSERT(gcd != 1);
+ PPL_ASSERT(c[0] % gcd != 0);
+
+ // If we have an equality, the polyhedron becomes empty.
+ if (c.is_equality()) {
+ set_empty();
+ return;
+ }
+
+ // Divide the inhomogeneous coefficients by the GCD.
+ for (dimension_type i = space_dim+1; --i > 0; ) {
+ Coefficient& c_i = c[i];
+ exact_div_assign(c_i, c_i, gcd);
+ }
+ Coefficient& c_0 = c[0];
+ const int c_0_sign = sgn(c_0);
+ c_0 /= gcd;
+ if (c_0_sign < 0)
+ --c_0;
+ changed = true;
+ }
+
+ maybe_normalize:
+ if (changed)
+ // Enforce normalization.
+ //c.normalize();
+ ;
+
+ next_constraint:
+ ;
+ }
+
+ if (changed) {
+ if (!is_necessarily_closed()) {
+ con_sys.insert(Constraint::epsilon_leq_one());
+ // FIXME: make sure that the following line really can stay here
+ // and should not be moved below the brace.
+ con_sys.set_sorted(false);
+ }
+
+ // After changing the system of constraints, the generators
+ // are no longer up-to-date and the constraints are no longer
+ // minimized.
+ clear_generators_up_to_date();
+ clear_constraints_minimized();
+ }
+ PPL_ASSERT_HEAVY(OK());
+}
+
+void
PPL::Polyhedron::throw_runtime_error(const char* method) const {
std::ostringstream s;
s << "PPL::";
More information about the PPL-devel
mailing list