/* Octagonal_Shape class implementation: inline functions. Copyright (C) 2001-2010 Roberto Bagnara Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com) This file is part of the Parma Polyhedra Library (PPL). The PPL is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. The PPL is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA. For the most up-to-date information see the Parma Polyhedra Library site: http://bugseng.com/products/ppl/ . */ #ifndef PPL_Octagonal_Shape_inlines_hh #define PPL_Octagonal_Shape_inlines_hh 1 #include "Constraint_System_defs.hh" #include "Constraint_System_inlines.hh" #include "C_Polyhedron_defs.hh" #include "Grid_defs.hh" #include "BD_Shape_defs.hh" #include "Poly_Con_Relation_defs.hh" #include "Poly_Gen_Relation_defs.hh" #include "wrap_assign.hh" #include "assertions.hh" #include namespace Parma_Polyhedra_Library { namespace Implementation { namespace Octagonal_Shapes { #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS //! Returns the index coherent to \p i. /*! \relates Parma_Polyhedra_Library::Octagonal_Shape */ #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS) inline dimension_type coherent_index(const dimension_type i) { return (i % 2 != 0) ? (i-1) : (i+1); } } // namespace Octagonal_Shapes } // namespace Implementation template inline dimension_type Octagonal_Shape::max_space_dimension() { return OR_Matrix::max_num_rows()/2; } template inline bool Octagonal_Shape::marked_zero_dim_univ() const { return status.test_zero_dim_univ(); } template inline bool Octagonal_Shape::marked_strongly_closed() const { return status.test_strongly_closed(); } template inline bool Octagonal_Shape::marked_empty() const { return status.test_empty(); } template inline void Octagonal_Shape::set_zero_dim_univ() { status.set_zero_dim_univ(); } template inline void Octagonal_Shape::set_empty() { status.set_empty(); } template inline void Octagonal_Shape::set_strongly_closed() { status.set_strongly_closed(); } template inline void Octagonal_Shape::reset_strongly_closed() { status.reset_strongly_closed(); } template inline Octagonal_Shape::Octagonal_Shape(const dimension_type num_dimensions, const Degenerate_Element kind) : matrix(num_dimensions), space_dim(num_dimensions), status() { if (kind == EMPTY) { set_empty(); } else if (num_dimensions > 0) { // A (non zero-dim) universe octagon is strongly closed. set_strongly_closed(); } PPL_ASSERT(OK()); } template inline Octagonal_Shape::Octagonal_Shape(const Octagonal_Shape& y, Complexity_Class) : matrix(y.matrix), space_dim(y.space_dim), status(y.status) { } template template inline Octagonal_Shape::Octagonal_Shape(const Octagonal_Shape& y, Complexity_Class) // For maximum precision, enforce shortest-path closure // before copying the DB matrix. : matrix((y.strong_closure_assign(), y.matrix)), space_dim(y.space_dim), status() { // TODO: handle flags properly, possibly taking special cases into account. if (y.marked_empty()) { set_empty(); } else if (y.marked_zero_dim_univ()) { set_zero_dim_univ(); } } template inline Octagonal_Shape::Octagonal_Shape(const Constraint_System& cs) : matrix(cs.space_dimension()), space_dim(cs.space_dimension()), status() { if (cs.space_dimension() > 0) { // A (non zero-dim) universe octagon is strongly closed. set_strongly_closed(); } add_constraints(cs); } template inline Octagonal_Shape::Octagonal_Shape(const Congruence_System& cgs) : matrix(cgs.space_dimension()), space_dim(cgs.space_dimension()), status() { if (cgs.space_dimension() > 0) { // A (non zero-dim) universe octagon is strongly closed. set_strongly_closed(); } add_congruences(cgs); } template template inline Octagonal_Shape::Octagonal_Shape(const Box& box, Complexity_Class) : matrix(box.space_dimension()), space_dim(box.space_dimension()), status() { // Check for emptiness for maximum precision. if (box.is_empty()) { set_empty(); } else if (box.space_dimension() > 0) { // A (non zero-dim) universe OS is strongly closed. set_strongly_closed(); refine_with_constraints(box.constraints()); } } template inline Octagonal_Shape::Octagonal_Shape(const Grid& grid, Complexity_Class) : matrix(grid.space_dimension()), space_dim(grid.space_dimension()), status() { if (grid.space_dimension() > 0) { // A (non zero-dim) universe OS is strongly closed. set_strongly_closed(); } // Taking minimized congruences ensures maximum precision. refine_with_congruences(grid.minimized_congruences()); } template template inline Octagonal_Shape::Octagonal_Shape(const BD_Shape& bd, Complexity_Class) : matrix(bd.space_dimension()), space_dim(bd.space_dimension()), status() { // Check for emptiness for maximum precision. if (bd.is_empty()) { set_empty(); } else if (bd.space_dimension() > 0) { // A (non zero-dim) universe OS is strongly closed. set_strongly_closed(); refine_with_constraints(bd.constraints()); } } template inline Congruence_System Octagonal_Shape::congruences() const { return minimized_congruences(); } template inline Octagonal_Shape& Octagonal_Shape::operator=(const Octagonal_Shape& y) { matrix = y.matrix; space_dim = y.space_dim; status = y.status; return *this; } template inline Octagonal_Shape::~Octagonal_Shape() { } template inline void Octagonal_Shape::m_swap(Octagonal_Shape& y) { using std::swap; swap(matrix, y.matrix); swap(space_dim, y.space_dim); swap(status, y.status); } template inline dimension_type Octagonal_Shape::space_dimension() const { return space_dim; } template inline bool Octagonal_Shape::is_discrete() const { return affine_dimension() == 0; } template inline bool Octagonal_Shape::is_empty() const { strong_closure_assign(); return marked_empty(); } template inline bool Octagonal_Shape::bounds_from_above(const Linear_Expression& expr) const { return bounds(expr, true); } template inline bool Octagonal_Shape::bounds_from_below(const Linear_Expression& expr) const { return bounds(expr, false); } template inline bool Octagonal_Shape::maximize(const Linear_Expression& expr, Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const { return max_min(expr, true, sup_n, sup_d, maximum); } template inline bool Octagonal_Shape::maximize(const Linear_Expression& expr, Coefficient& sup_n, Coefficient& sup_d, bool& maximum, Generator& g) const { return max_min(expr, true, sup_n, sup_d, maximum, g); } template inline bool Octagonal_Shape::minimize(const Linear_Expression& expr, Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const { return max_min(expr, false, inf_n, inf_d, minimum); } template inline bool Octagonal_Shape::minimize(const Linear_Expression& expr, Coefficient& inf_n, Coefficient& inf_d, bool& minimum, Generator& g) const { return max_min(expr, false, inf_n, inf_d, minimum, g); } template inline bool Octagonal_Shape::is_topologically_closed() const { return true; } template inline void Octagonal_Shape::topological_closure_assign() { } /*! \relates Octagonal_Shape */ template inline bool operator==(const Octagonal_Shape& x, const Octagonal_Shape& y) { if (x.space_dim != y.space_dim) { // Dimension-incompatible OSs are different. return false; } // Zero-dim OSs are equal if and only if they are both empty or universe. if (x.space_dim == 0) { if (x.marked_empty()) { return y.marked_empty(); } else { return !y.marked_empty(); } } x.strong_closure_assign(); y.strong_closure_assign(); // If one of two octagons is empty, then they are equal if and only if // the other octagon is empty too. if (x.marked_empty()) { return y.marked_empty(); } if (y.marked_empty()) { return false; } // Strong closure is a canonical form. return x.matrix == y.matrix; } /*! \relates Octagonal_Shape */ template inline bool operator!=(const Octagonal_Shape& x, const Octagonal_Shape& y) { return !(x == y); } template inline const typename Octagonal_Shape::coefficient_type& Octagonal_Shape::matrix_at(const dimension_type i, const dimension_type j) const { PPL_ASSERT(i < matrix.num_rows() && j < matrix.num_rows()); using namespace Implementation::Octagonal_Shapes; return (j < matrix.row_size(i)) ? matrix[i][j] : matrix[coherent_index(j)][coherent_index(i)]; } template inline typename Octagonal_Shape::coefficient_type& Octagonal_Shape::matrix_at(const dimension_type i, const dimension_type j) { PPL_ASSERT(i < matrix.num_rows() && j < matrix.num_rows()); using namespace Implementation::Octagonal_Shapes; return (j < matrix.row_size(i)) ? matrix[i][j] : matrix[coherent_index(j)][coherent_index(i)]; } template inline Constraint_System Octagonal_Shape::minimized_constraints() const { strong_reduction_assign(); return constraints(); } template inline void Octagonal_Shape::add_octagonal_constraint(const dimension_type i, const dimension_type j, const N& k) { // Private method: the caller has to ensure the following. #ifndef NDEBUG PPL_ASSERT(i < 2*space_dim && j < 2*space_dim && i != j); typename OR_Matrix::row_iterator m_i = matrix.row_begin() + i; PPL_ASSERT(j < m_i.row_size()); #endif N& r_i_j = matrix[i][j]; if (r_i_j > k) { r_i_j = k; if (marked_strongly_closed()) { reset_strongly_closed(); } } } template inline void Octagonal_Shape ::add_octagonal_constraint(const dimension_type i, const dimension_type j, Coefficient_traits::const_reference numer, Coefficient_traits::const_reference denom) { #ifndef NDEBUG // Private method: the caller has to ensure the following. PPL_ASSERT(i < 2*space_dim && j < 2*space_dim && i != j); typename OR_Matrix::row_iterator m_i = matrix.row_begin() + i; PPL_ASSERT(j < m_i.row_size()); PPL_ASSERT(denom != 0); #endif PPL_DIRTY_TEMP(N, k); div_round_up(k, numer, denom); add_octagonal_constraint(i, j, k); } template inline void Octagonal_Shape::add_constraints(const Constraint_System& cs) { for (Constraint_System::const_iterator i = cs.begin(), i_end = cs.end(); i != i_end; ++i) { add_constraint(*i); } } template inline void Octagonal_Shape::add_recycled_constraints(Constraint_System& cs) { add_constraints(cs); } template inline void Octagonal_Shape::add_recycled_congruences(Congruence_System& cgs) { add_congruences(cgs); } template inline void Octagonal_Shape::add_congruences(const Congruence_System& cgs) { for (Congruence_System::const_iterator i = cgs.begin(), cgs_end = cgs.end(); i != cgs_end; ++i) { add_congruence(*i); } } template inline void Octagonal_Shape::refine_with_constraint(const Constraint& c) { // Dimension-compatibility check. if (c.space_dimension() > space_dimension()) { throw_dimension_incompatible("refine_with_constraint(c)", c); } if (!marked_empty()) { refine_no_check(c); } } template inline void Octagonal_Shape::refine_with_constraints(const Constraint_System& cs) { // Dimension-compatibility check. if (cs.space_dimension() > space_dimension()) { throw_invalid_argument("refine_with_constraints(cs)", "cs and *this are space-dimension incompatible"); } for (Constraint_System::const_iterator i = cs.begin(), cs_end = cs.end(); !marked_empty() && i != cs_end; ++i) { refine_no_check(*i); } } template inline void Octagonal_Shape::refine_with_congruence(const Congruence& cg) { const dimension_type cg_space_dim = cg.space_dimension(); // Dimension-compatibility check. if (cg_space_dim > space_dimension()) { throw_dimension_incompatible("refine_with_congruence(cg)", cg); } if (!marked_empty()) { refine_no_check(cg); } } template void Octagonal_Shape::refine_with_congruences(const Congruence_System& cgs) { // Dimension-compatibility check. if (cgs.space_dimension() > space_dimension()) { throw_invalid_argument("refine_with_congruences(cgs)", "cgs and *this are space-dimension incompatible"); } for (Congruence_System::const_iterator i = cgs.begin(), cgs_end = cgs.end(); !marked_empty() && i != cgs_end; ++i) { refine_no_check(*i); } } template inline void Octagonal_Shape::refine_no_check(const Congruence& cg) { PPL_ASSERT(!marked_empty()); PPL_ASSERT(cg.space_dimension() <= space_dimension()); if (cg.is_proper_congruence()) { if (cg.is_inconsistent()) { set_empty(); } // Other proper congruences are just ignored. return; } PPL_ASSERT(cg.is_equality()); Constraint c(cg); refine_no_check(c); } template inline bool Octagonal_Shape::can_recycle_constraint_systems() { return false; } template inline bool Octagonal_Shape::can_recycle_congruence_systems() { return false; } template inline void Octagonal_Shape ::remove_higher_space_dimensions(const dimension_type new_dimension) { // Dimension-compatibility check. if (new_dimension > space_dim) { throw_dimension_incompatible("remove_higher_space_dimension(nd)", new_dimension); } // The removal of no dimensions from any octagon is a no-op. // Note that this case also captures the only legal removal of // dimensions from an octagon in a 0-dim space. if (new_dimension == space_dim) { PPL_ASSERT(OK()); return; } strong_closure_assign(); matrix.shrink(new_dimension); // When we remove all dimensions from a non-empty octagon, // we obtain the zero-dimensional universe octagon. if (new_dimension == 0 && !marked_empty()) { set_zero_dim_univ(); } space_dim = new_dimension; PPL_ASSERT(OK()); } template void Octagonal_Shape::wrap_assign(const Variables_Set& vars, Bounded_Integer_Type_Width w, Bounded_Integer_Type_Representation r, Bounded_Integer_Type_Overflow o, const Constraint_System* cs_p, unsigned complexity_threshold, bool wrap_individually) { Implementation::wrap_assign(*this, vars, w, r, o, cs_p, complexity_threshold, wrap_individually, "Octagonal_Shape"); } template inline void Octagonal_Shape::widening_assign(const Octagonal_Shape& y, unsigned* tp) { BHMZ05_widening_assign(y, tp); } template inline void Octagonal_Shape::CC76_extrapolation_assign(const Octagonal_Shape& y, unsigned* tp) { static N stop_points[] = { N(-2, ROUND_UP), N(-1, ROUND_UP), N( 0, ROUND_UP), N( 1, ROUND_UP), N( 2, ROUND_UP) }; CC76_extrapolation_assign(y, stop_points, stop_points + sizeof(stop_points)/sizeof(stop_points[0]), tp); } template inline void Octagonal_Shape::time_elapse_assign(const Octagonal_Shape& y) { // Dimension-compatibility check. if (space_dimension() != y.space_dimension()) { throw_dimension_incompatible("time_elapse_assign(y)", y); } // Compute time-elapse on polyhedra. // TODO: provide a direct implementation. C_Polyhedron ph_x(constraints()); C_Polyhedron ph_y(y.constraints()); ph_x.time_elapse_assign(ph_y); Octagonal_Shape x(ph_x); m_swap(x); PPL_ASSERT(OK()); } template inline bool Octagonal_Shape::strictly_contains(const Octagonal_Shape& y) const { const Octagonal_Shape& x = *this; return x.contains(y) && !y.contains(x); } template template inline void Octagonal_Shape::generalized_refine_with_linear_form_inequality( const Linear_Form< Interval >& left, const Linear_Form< Interval >& right, const Relation_Symbol relsym) { switch (relsym) { case EQUAL: // TODO: see if we can handle this case more efficiently. refine_with_linear_form_inequality(left, right); refine_with_linear_form_inequality(right, left); break; case LESS_THAN: case LESS_OR_EQUAL: refine_with_linear_form_inequality(left, right); break; case GREATER_THAN: case GREATER_OR_EQUAL: refine_with_linear_form_inequality(right, left); break; case NOT_EQUAL: break; default: PPL_UNREACHABLE; break; } } template template inline void Octagonal_Shape:: refine_fp_interval_abstract_store( Box< Interval >& store) const { // Check that T is a floating point type. PPL_COMPILE_TIME_CHECK(!std::numeric_limits::is_exact, "Octagonal_Shape::refine_fp_interval_abstract_store:" " T not a floating point type."); typedef Interval FP_Interval_Type; store.intersection_assign(Box(*this)); } /*! \relates Octagonal_Shape */ template inline bool rectilinear_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2) { // Dimension-compatibility check. if (x.space_dim != y.space_dim) { return false; } // Zero-dim OSs are equal if and only if they are both empty or universe. if (x.space_dim == 0) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } // The distance computation requires strong closure. x.strong_closure_assign(); y.strong_closure_assign(); // If one of two OSs is empty, then they are equal if and only if // the other OS is empty too. if (x.marked_empty() || y.marked_empty()) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } return rectilinear_distance_assign(r, x.matrix, y.matrix, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool rectilinear_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { typedef Checked_Number Checked_Temp; PPL_DIRTY_TEMP(Checked_Temp, tmp0); PPL_DIRTY_TEMP(Checked_Temp, tmp1); PPL_DIRTY_TEMP(Checked_Temp, tmp2); return rectilinear_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool rectilinear_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { return rectilinear_distance_assign(r, x, y, dir); } /*! \relates Octagonal_Shape */ template inline bool euclidean_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2) { // Dimension-compatibility check. if (x.space_dim != y.space_dim) { return false; } // Zero-dim OSs are equal if and only if they are both empty or universe. if (x.space_dim == 0) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } // The distance computation requires strong closure. x.strong_closure_assign(); y.strong_closure_assign(); // If one of two OSs is empty, then they are equal if and only if // the other OS is empty too. if (x.marked_empty() || y.marked_empty()) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } return euclidean_distance_assign(r, x.matrix, y.matrix, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool euclidean_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { typedef Checked_Number Checked_Temp; PPL_DIRTY_TEMP(Checked_Temp, tmp0); PPL_DIRTY_TEMP(Checked_Temp, tmp1); PPL_DIRTY_TEMP(Checked_Temp, tmp2); return euclidean_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool euclidean_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { return euclidean_distance_assign(r, x, y, dir); } /*! \relates Octagonal_Shape */ template inline bool l_infinity_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir, Temp& tmp0, Temp& tmp1, Temp& tmp2) { // Dimension-compatibility check. if (x.space_dim != y.space_dim) { return false; } // Zero-dim OSs are equal if and only if they are both empty or universe. if (x.space_dim == 0) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } // The distance computation requires strong closure. x.strong_closure_assign(); y.strong_closure_assign(); // If one of two OSs is empty, then they are equal if and only if // the other OS is empty too. if (x.marked_empty() || y.marked_empty()) { if (x.marked_empty() == y.marked_empty()) { assign_r(r, 0, ROUND_NOT_NEEDED); } else { assign_r(r, PLUS_INFINITY, ROUND_NOT_NEEDED); } return true; } return l_infinity_distance_assign(r, x.matrix, y.matrix, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool l_infinity_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { typedef Checked_Number Checked_Temp; PPL_DIRTY_TEMP(Checked_Temp, tmp0); PPL_DIRTY_TEMP(Checked_Temp, tmp1); PPL_DIRTY_TEMP(Checked_Temp, tmp2); return l_infinity_distance_assign(r, x, y, dir, tmp0, tmp1, tmp2); } /*! \relates Octagonal_Shape */ template inline bool l_infinity_distance_assign(Checked_Number& r, const Octagonal_Shape& x, const Octagonal_Shape& y, const Rounding_Dir dir) { return l_infinity_distance_assign(r, x, y, dir); } template inline memory_size_type Octagonal_Shape::total_memory_in_bytes() const { return sizeof(*this) + external_memory_in_bytes(); } template inline int32_t Octagonal_Shape::hash_code() const { return hash_code_from_dimension(space_dimension()); } template inline void Octagonal_Shape::drop_some_non_integer_points_helper(N& elem) { if (!is_integer(elem)) { #ifndef NDEBUG Result r = #endif floor_assign_r(elem, elem, ROUND_DOWN); PPL_ASSERT(r == V_EQ); reset_strongly_closed(); } } /*! \relates Octagonal_Shape */ template inline void swap(Octagonal_Shape& x, Octagonal_Shape& y) { x.m_swap(y); } } // namespace Parma_Polyhedra_Library #endif // !defined(PPL_Octagonal_Shape_inlines_hh)