Affine_Space_defs.hh

Go to the documentation of this file.

/* Affine_Space 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_Affine_Space_defs_hh
#define PPL_Affine_Space_defs_hh 1

#include "Affine_Space_types.hh"
#include "Variable_defs.hh"
#include "Variables_Set_types.hh"
#include "Linear_Expression_types.hh"
#include "Constraint_types.hh"
#include "Constraint_System_defs.hh"
#include "Constraint_System_inlines.hh"
#include "Congruence_System_defs.hh"
#include "Congruence_System_inlines.hh"
#include "Poly_Con_Relation_defs.hh"
#include "Poly_Gen_Relation_defs.hh"
#include "Box_types.hh"
#include "Polyhedron_types.hh"
#include "BD_Shape_types.hh"
#include "Octagonal_Shape_types.hh"
#include "Grid_defs.hh"
#include <iosfwd>

namespace Parma_Polyhedra_Library {

namespace IO_Operators {


std::ostream&
operator<<(std::ostream& s, const Affine_Space& gr);

} // namespace IO_Operators


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

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

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

} // namespace Parma_Polyhedra_Library



class Parma_Polyhedra_Library::Affine_Space {
public:
  typedef Coefficient coefficient_type;

  static dimension_type max_space_dimension();

  static bool can_recycle_constraint_systems();

  static bool can_recycle_congruence_systems();


  explicit Affine_Space(dimension_type num_dimensions = 0,
                        Degenerate_Element kind = UNIVERSE);


  explicit Affine_Space(const Constraint_System& cs);


  Affine_Space(Constraint_System& cs, Recycle_Input dummy);


  explicit Affine_Space(const Generator_System& gs);


  Affine_Space(Generator_System& gs, Recycle_Input dummy);


  template <typename Interval>
  explicit Affine_Space(const Box<Interval>& box,
                        Complexity_Class complexity = ANY_COMPLEXITY);


  template <typename U>
  explicit Affine_Space(const BD_Shape<U>& bd,
                        Complexity_Class complexity = ANY_COMPLEXITY);


  template <typename U>
  explicit Affine_Space(const Octagonal_Shape<U>& os,
                        Complexity_Class complexity = ANY_COMPLEXITY);

  explicit Affine_Space(const Polyhedron& ph,
                        Complexity_Class complexity = ANY_COMPLEXITY);


  Affine_Space(const Affine_Space& y,
               Complexity_Class complexity = ANY_COMPLEXITY);

  Affine_Space& operator=(const Affine_Space& y);



  dimension_type space_dimension() const;

  dimension_type affine_dimension() const;

  Constraint_System constraints() const;

  Constraint_System minimized_constraints() const;

  const Congruence_System& congruences() const;

  const Congruence_System& minimized_congruences() const;

  Generator_System generators() const;

  Generator_System minimized_generators() const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and congruence \p cg are dimension-incompatible.
  */
  Poly_Con_Relation relation_with(const Congruence& cg) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and generator \p g are dimension-incompatible.
  */
  Poly_Gen_Relation
  relation_with(const Generator& g) const;

  /*
    \exception std::invalid_argument
    Thrown if \p *this and constraint \p c are dimension-incompatible.
  */
  Poly_Con_Relation relation_with(const Constraint& c) const;

  bool is_empty() const;

  bool is_universe() const;

  bool is_topologically_closed() const;

  bool is_disjoint_from(const Affine_Space& y) const;


  bool is_discrete() const;

  bool is_bounded() const;

  bool contains_integer_point() const;

  bool constrains(Variable var) const;


  bool bounds_from_above(const Linear_Expression& expr) const;


  bool bounds_from_below(const Linear_Expression& expr) const;

  // FIXME: revise all the comment blocks below this one.

  bool maximize(const Linear_Expression& expr,
                Coefficient& sup_n, Coefficient& sup_d, bool& maximum) const;

  bool maximize(const Linear_Expression& expr,
                Coefficient& sup_n, Coefficient& sup_d, bool& maximum,
                Generator& point) const;

  bool minimize(const Linear_Expression& expr,
                Coefficient& inf_n, Coefficient& inf_d, bool& minimum) const;

  bool minimize(const Linear_Expression& expr,
                Coefficient& inf_n, Coefficient& inf_d, bool& minimum,
                Generator& point) const;

  bool frequency(const Linear_Expression& expr,
                 Coefficient& freq_n, Coefficient& freq_d,
                 Coefficient& val_n, Coefficient& val_d) const;


  bool contains(const Affine_Space& y) const;

  bool strictly_contains(const Affine_Space& y) const;


  bool OK(bool check_not_empty = false) const;





  void add_congruence(const Congruence& cg);

  void add_generator(const Generator& g);


  void add_congruences(const Congruence_System& cgs);


  void add_recycled_congruences(Congruence_System& cgs);

  void add_constraint(const Constraint& c);

  void add_constraints(const Constraint_System& cs);

  void add_recycled_constraints(Constraint_System& cs);


  void refine_with_congruence(const Congruence& cg);


  void refine_with_congruences(const Congruence_System& cgs);


  void refine_with_constraint(const Constraint& c);


  void refine_with_constraints(const Constraint_System& cs);

  void add_generators(const Generator_System& gs);

  void add_recycled_generators(Generator_System& gs);

  void unconstrain(Variable var);

  void unconstrain(const Variables_Set& vars);

  void intersection_assign(const Affine_Space& y);

  void upper_bound_assign(const Affine_Space& y);

  bool upper_bound_assign_if_exact(const Affine_Space& y);

  void difference_assign(const Affine_Space& y);

  bool simplify_using_context_assign(const Affine_Space& y);

  void affine_image(Variable var,
                    const Linear_Expression& expr,
                    Coefficient_traits::const_reference denominator
                    = Coefficient_one());

  void affine_preimage(Variable var,
                       const Linear_Expression& expr,
                       Coefficient_traits::const_reference denominator
                         = Coefficient_one());

  void
  generalized_affine_image(Variable var,
                           Relation_Symbol relsym,
                           const Linear_Expression& expr,
                           Coefficient_traits::const_reference denominator
                           = Coefficient_one());

  void
  generalized_affine_preimage(Variable var,
                              Relation_Symbol relsym,
                              const Linear_Expression& expr,
                              Coefficient_traits::const_reference denominator
                              = Coefficient_one());

  void
  generalized_affine_image(const Linear_Expression& lhs,
                           Relation_Symbol relsym,
                           const Linear_Expression& rhs);

  void
  generalized_affine_preimage(const Linear_Expression& lhs,
                              Relation_Symbol relsym,
                              const Linear_Expression& rhs);

  void bounded_affine_image(Variable var,
                            const Linear_Expression& lb_expr,
                            const Linear_Expression& ub_expr,
                            Coefficient_traits::const_reference denominator
                            = Coefficient_one());

  void bounded_affine_preimage(Variable var,
                               const Linear_Expression& lb_expr,
                               const Linear_Expression& ub_expr,
                               Coefficient_traits::const_reference denominator
                               = Coefficient_one());

  void time_elapse_assign(const Affine_Space& y);

  void topological_closure_assign();

  void widening_assign(const Affine_Space& y, unsigned* tp = NULL);

  void limited_extrapolation_assign(const Affine_Space& y,
                                    const Constraint_System& cs,
                                    unsigned* tp = NULL);




  void add_space_dimensions_and_embed(dimension_type m);

  void add_space_dimensions_and_project(dimension_type m);

  void concatenate_assign(const Affine_Space& y);


  void remove_space_dimensions(const Variables_Set& vars);

  void remove_higher_space_dimensions(dimension_type new_dimension);

  template <typename Partial_Function>
  void map_space_dimensions(const Partial_Function& pfunc);


  void expand_space_dimension(Variable var, dimension_type m);


  void fold_space_dimensions(const Variables_Set& to_be_folded, Variable var);


  friend bool operator==(const Affine_Space& x, const Affine_Space& y);



  ~Affine_Space();

  void m_swap(Affine_Space& y);

  PPL_OUTPUT_DECLARATIONS

  bool ascii_load(std::istream& s);

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  int32_t hash_code() const;


private:
  Grid gr;

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
protected:
#if 0
  void throw_invalid_argument(const char* method, const char* reason) const;
#endif
  void throw_dimension_incompatible(const char* method,
                                    const char* other_name,
                                    dimension_type other_dim) const;
  void throw_dimension_incompatible(const char* method,
                                    const char* as_name,
                                    const Affine_Space& as) const;

  // Note: it has to be a static method, because it can be called inside
  // constructors (before actually constructing the grid object).
  static void throw_space_dimension_overflow(const char* method,
                                             const char* reason);

  void throw_invalid_constraint(const char* method,
                                const char* c_name) const;
  void throw_invalid_constraints(const char* method,
                                 const char* cs_name) const;
  void throw_invalid_generator(const char* method,
                               const char* g_name) const;
  void throw_invalid_generators(const char* method,
                                const char* gs_name) const;
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)

};

#include "Affine_Space_inlines.hh"

#endif // !defined(PPL_Affine_Space_defs_hh)