Constraint_defs.hh

Go to the documentation of this file.

/* Constraint class declaration.
   Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
   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_Constraint_defs_hh
#define PPL_Constraint_defs_hh 1

#include "Constraint_types.hh"

#include "Congruence_types.hh"
#include "Variables_Set_types.hh"
#include "Polyhedron_types.hh"
#include "termination_types.hh"
#include "Octagonal_Shape_types.hh"
#include "Grid_types.hh"

#include "Linear_Expression_defs.hh"
#include "Variable_defs.hh"
#include "Topology_types.hh"
#include "Expression_Hide_Last_defs.hh"

#include <iosfwd>

namespace Parma_Polyhedra_Library {


Constraint
operator<(const Linear_Expression& e1, const Linear_Expression& e2);


Constraint
operator<(Variable v1, Variable v2);


Constraint
operator<(const Linear_Expression& e, Coefficient_traits::const_reference n);


Constraint
operator<(Coefficient_traits::const_reference n, const Linear_Expression& e);


Constraint
operator>(const Linear_Expression& e1, const Linear_Expression& e2);


Constraint
operator>(Variable v1, Variable v2);


Constraint
operator>(const Linear_Expression& e, Coefficient_traits::const_reference n);


Constraint
operator>(Coefficient_traits::const_reference n, const Linear_Expression& e);


Constraint
operator==(const Linear_Expression& e1, const Linear_Expression& e2);


Constraint
operator==(Variable v1, Variable v2);


Constraint
operator==(const Linear_Expression& e, Coefficient_traits::const_reference n);


Constraint
operator==(Coefficient_traits::const_reference n, const Linear_Expression& e);


Constraint
operator<=(const Linear_Expression& e1, const Linear_Expression& e2);


Constraint
operator<=(Variable v1, Variable v2);


Constraint
operator<=(const Linear_Expression& e, Coefficient_traits::const_reference n);


Constraint
operator<=(Coefficient_traits::const_reference n, const Linear_Expression& e);


Constraint
operator>=(const Linear_Expression& e1, const Linear_Expression& e2);


Constraint
operator>=(Variable v1, Variable v2);


Constraint
operator>=(const Linear_Expression& e, Coefficient_traits::const_reference n);


Constraint
operator>=(Coefficient_traits::const_reference n, const Linear_Expression& e);

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
int compare(const Constraint& x, const Constraint& y);

}


class Parma_Polyhedra_Library::Constraint {
public:

  enum Type {
    EQUALITY,
    NONSTRICT_INEQUALITY,
    STRICT_INEQUALITY
  };


  static const Representation default_representation = SPARSE;

  explicit Constraint(Representation r = default_representation);


  Constraint(const Constraint& c);


  Constraint(const Constraint& c, dimension_type space_dim);

  Constraint(const Constraint& c, Representation r);

  Constraint(const Constraint& c, dimension_type space_dim,
             Representation r);


  explicit Constraint(const Congruence& cg,
                      Representation r = default_representation);

  ~Constraint();

  Representation representation() const;

  void set_representation(Representation r);

  Constraint& operator=(const Constraint& c);

  static dimension_type max_space_dimension();

  dimension_type space_dimension() const;

  void set_space_dimension(dimension_type space_dim);

  void swap_space_dimensions(Variable v1, Variable v2);


  bool remove_space_dimensions(const Variables_Set& vars);

  /*
    \param cycle
    A vector representing a cycle of the permutation according to which the
    space dimensions must be rearranged.

    The \p cycle vector represents a cycle of a permutation of space
    dimensions.
    For example, the permutation
    \f$ \{ x_1 \mapsto x_2, x_2 \mapsto x_3, x_3 \mapsto x_1 \}\f$ can be
    represented by the vector containing \f$ x_1, x_2, x_3 \f$.
  */
  void permute_space_dimensions(const std::vector<Variable>& cycle);

  void shift_space_dimensions(Variable v, dimension_type n);

  Type type() const;

  bool is_equality() const;

  bool is_inequality() const;

  bool is_nonstrict_inequality() const;

  bool is_strict_inequality() const;


  Coefficient_traits::const_reference coefficient(Variable v) const;

  Coefficient_traits::const_reference inhomogeneous_term() const;

  static void initialize();

  static void finalize();

  static const Constraint& zero_dim_false();

  static const Constraint& zero_dim_positivity();

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  bool is_tautological() const;

  bool is_inconsistent() const;

  bool is_equivalent_to(const Constraint& y) const;


  bool is_equal_to(const Constraint& y) const;

  bool OK() const;

  PPL_OUTPUT_DECLARATIONS

  bool ascii_load(std::istream& s);

  void m_swap(Constraint& y);

  static const Constraint& epsilon_geq_zero();

  static const Constraint& epsilon_leq_one();

  typedef Expression_Hide_Last<Linear_Expression> expr_type;
  expr_type expression() const;

private:

  enum Kind {
    LINE_OR_EQUALITY = 0,
    RAY_OR_POINT_OR_INEQUALITY = 1
  };

  Linear_Expression expr;

  Kind kind_;

  Topology topology_;

  static const Constraint* zero_dim_false_p;

  static const Constraint* zero_dim_positivity_p;

  static const Constraint* epsilon_geq_zero_p;

  static const Constraint* epsilon_leq_one_p;

  Constraint(dimension_type space_dim, Kind kind, Topology topology,
             Representation r = default_representation);

  Constraint(Linear_Expression& e, Kind kind, Topology topology);

  Constraint(Linear_Expression& e, Type type, Topology topology);

  bool is_line_or_equality() const;

  bool is_ray_or_point_or_inequality() const;

  void set_is_line_or_equality();

  void set_is_ray_or_point_or_inequality();


  Topology topology() const;

  bool is_not_necessarily_closed() const;

  bool is_necessarily_closed() const;



  // TODO: Consider setting the epsilon dimension in this method.
  void set_topology(Topology x);

  void set_necessarily_closed();

  void set_not_necessarily_closed();


  void set_space_dimension_no_ok(dimension_type space_dim);

  void
  throw_invalid_argument(const char* method, const char* message) const;

  void
  throw_dimension_incompatible(const char* method,
                               const char* name_var,
                               Variable v) const;

  Coefficient_traits::const_reference epsilon_coefficient() const;

  void set_epsilon_coefficient(Coefficient_traits::const_reference n);


  void mark_as_necessarily_closed();


  void mark_as_not_necessarily_closed();

  void set_is_equality();


  void set_is_inequality();


  void linear_combine(const Constraint& y, dimension_type i);

  void sign_normalize();

  void strong_normalize();

  bool check_strong_normalized() const;

  static Constraint construct_epsilon_geq_zero();

  friend int
  compare(const Constraint& x, const Constraint& y);

  friend class Linear_System<Constraint>;
  friend class Constraint_System;
  friend class Polyhedron;
  friend class Scalar_Products;
  friend class Topology_Adjusted_Scalar_Product_Sign;
  friend class Termination_Helpers;
  friend class Grid;
  template <typename T>
  friend class Octagonal_Shape;

  friend Constraint
  operator<(const Linear_Expression& e1, const Linear_Expression& e2);

  friend Constraint
  operator<(Variable v1, Variable v2);

  friend Constraint
  operator<(const Linear_Expression& e, Coefficient_traits::const_reference n);

  friend Constraint
  operator<(Coefficient_traits::const_reference n, const Linear_Expression& e);

  friend Constraint
  operator>(const Linear_Expression& e1, const Linear_Expression& e2);

  friend Constraint
  operator>(Variable v1, Variable v2);

  friend Constraint
  operator>(const Linear_Expression& e, Coefficient_traits::const_reference n);

  friend Constraint
  operator>(Coefficient_traits::const_reference n, const Linear_Expression& e);

  friend Constraint
  operator==(const Linear_Expression& e1, const Linear_Expression& e2);

  friend Constraint
  operator==(Variable v1, Variable v2);

  friend Constraint
  operator==(const Linear_Expression& e, Coefficient_traits::const_reference n);

  friend Constraint
  operator==(Coefficient_traits::const_reference n, const Linear_Expression& e);

  friend Constraint
  operator<=(const Linear_Expression& e1, const Linear_Expression& e2);

  friend Constraint
  operator<=(Variable v1, Variable v2);

  friend Constraint
  operator<=(const Linear_Expression& e, Coefficient_traits::const_reference n);

  friend Constraint
  operator<=(Coefficient_traits::const_reference n, const Linear_Expression& e);

  friend Constraint
  operator>=(const Linear_Expression& e1, const Linear_Expression& e2);

  friend Constraint
  operator>=(Variable v1, Variable v2);

  friend Constraint
  operator>=(const Linear_Expression& e, Coefficient_traits::const_reference n);

  friend Constraint
  operator>=(Coefficient_traits::const_reference n, const Linear_Expression& e);
};

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


std::ostream& operator<<(std::ostream& s, const Constraint& c);


std::ostream& operator<<(std::ostream& s, const Constraint::Type& t);

} // namespace IO_Operators


bool
operator==(const Constraint& x, const Constraint& y);


bool
operator!=(const Constraint& x, const Constraint& y);

void swap(Constraint& x, Constraint& y);

} // namespace Parma_Polyhedra_Library

#include "Constraint_inlines.hh"

#endif // !defined(PPL_Constraint_defs_hh)