Linear_System_defs.hh

Go to the documentation of this file.

/* Linear_System 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_Linear_System_defs_hh
#define PPL_Linear_System_defs_hh 1

#include "Linear_System_types.hh"

#include "Swapping_Vector_defs.hh"
#include "globals_defs.hh"
#include "Variable_defs.hh"
#include "Variables_Set_defs.hh"

#include "Polyhedron_types.hh"
#include "Bit_Row_types.hh"
#include "Bit_Matrix_types.hh"
#include "Generator_System_types.hh"
#include "Topology_types.hh"

// TODO: Check how much of this description is still true.
#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename Row>
class Parma_Polyhedra_Library::Linear_System {
public:

  // NOTE: `iterator' is actually a const_iterator.
  typedef typename Swapping_Vector<Row>::const_iterator iterator;
  typedef typename Swapping_Vector<Row>::const_iterator const_iterator;


  Linear_System(Topology topol, Representation r);


  Linear_System(Topology topol, dimension_type space_dim, Representation r);

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
  struct With_Pending {
  };

  Linear_System(const Linear_System& y);

  Linear_System(const Linear_System& y, Representation r);

  Linear_System(const Linear_System& y, With_Pending);

  Linear_System(const Linear_System& y, Representation r, With_Pending);

  Linear_System& operator=(const Linear_System& y);

  void assign_with_pending(const Linear_System& y);

  void m_swap(Linear_System& y);

  Representation representation() const;

  void set_representation(Representation r);

  static dimension_type max_space_dimension();


  dimension_type space_dimension() const;

  void set_space_dimension(dimension_type space_dim);

  void remove_trailing_rows(dimension_type n);


  void remove_row(dimension_type i, bool keep_sorted = false);


  void remove_rows(dimension_type first, dimension_type last,
                  bool keep_sorted = false);

  // TODO: Consider removing this.

  void remove_rows(const std::vector<dimension_type>& indexes);

  // TODO: Consider making this private.

  void remove_space_dimensions(const Variables_Set& vars);

  void shift_space_dimensions(Variable v, dimension_type n);

  // TODO: Consider making this private.
  /*
    \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 swap_space_dimensions(Variable v1, Variable v2);


  const Row& operator[](dimension_type k) const;

  iterator begin();
  iterator end();
  const_iterator begin() const;
  const_iterator end() const;

  bool has_no_rows() const;
  dimension_type num_rows() const;

  void strong_normalize();

  void sign_normalize();


  Topology topology() const;

  bool is_sorted() const;

  bool is_necessarily_closed() const;

  dimension_type num_lines_or_equalities() const;

  dimension_type first_pending_row() const;

  dimension_type num_pending_rows() const;

  bool check_sorted() const;

  void set_topology(Topology t);

  void set_necessarily_closed();

  void set_not_necessarily_closed();

  // TODO: Consider removing this, or making it private.

  void mark_as_necessarily_closed();

  // TODO: Consider removing this, or making it private.

  void mark_as_not_necessarily_closed();

  void unset_pending_rows();

  void set_index_first_pending_row(dimension_type i);

  void set_sorted(bool b);


  void add_universe_rows_and_space_dimensions(dimension_type n);

  void insert(const Row& r);

  void insert_pending(const Row& r);

  void insert(Row& r, Recycle_Input);

  void insert_pending(Row& r, Recycle_Input);


  void insert(const Linear_System& y);

  void insert_pending(const Linear_System& r);


  void insert(Linear_System& r, Recycle_Input);

  void insert_pending(Linear_System& r, Recycle_Input);

  void sort_rows();

  void sort_rows(dimension_type first_row, dimension_type last_row);

  void merge_rows_assign(const Linear_System& y);

  void sort_pending_and_remove_duplicates();

  void sort_and_remove_with_sat(Bit_Matrix& sat);


  dimension_type gauss(dimension_type n_lines_or_equalities);

  void back_substitute(dimension_type n_lines_or_equalities);

  void simplify();

  void clear();

  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;


  Swapping_Vector<Row> rows;

  bool OK() const;

private:

  void remove_row_no_ok(dimension_type i, bool keep_sorted = false);

  void insert_pending_no_ok(Row& r, Recycle_Input);

  void insert_no_ok(Row& r, Recycle_Input);


  void set_space_dimension_no_ok(dimension_type space_dim);


  void swap_row_intervals(dimension_type first, dimension_type last,
                          dimension_type offset);

  dimension_type space_dimension_;

  Topology row_topology;

  dimension_type index_first_pending;

  bool sorted;

  Representation representation_;

  struct Row_Less_Than {
    bool operator()(const Row& x, const Row& y) const;
  };

  struct Unique_Compare {
    Unique_Compare(const Swapping_Vector<Row>& cont,
                   dimension_type base = 0);

    bool operator()(dimension_type i, dimension_type j) const;

    const Swapping_Vector<Row>& container;
    const dimension_type base_index;
  };

  friend class Polyhedron;
  friend class Generator_System;
};

namespace Parma_Polyhedra_Library {

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename Row>
void swap(Parma_Polyhedra_Library::Linear_System<Row>& x,
          Parma_Polyhedra_Library::Linear_System<Row>& y);

} // namespace std

namespace Parma_Polyhedra_Library {

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename Row>
bool operator==(const Linear_System<Row>& x, const Linear_System<Row>& y);

#ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS

#endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
template <typename Row>
bool operator!=(const Linear_System<Row>& x, const Linear_System<Row>& y);

} // namespace Parma_Polyhedra_Library

#include "Linear_System_inlines.hh"
#include "Linear_System_templates.hh"

#endif // !defined(PPL_Linear_System_defs_hh)