Powerset_defs.hh

Go to the documentation of this file.

/* Powerset 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_Powerset_defs_hh
#define PPL_Powerset_defs_hh

#include "Powerset_types.hh"
#include "globals_types.hh"
#include "iterator_to_const_defs.hh"
#include <iosfwd>
#include <iterator>
#include <list>

namespace Parma_Polyhedra_Library {


template <typename D>
void swap(Powerset<D>& x, Powerset<D>& y);


template <typename D>
bool
operator==(const Powerset<D>& x, const Powerset<D>& y);


template <typename D>
bool
operator!=(const Powerset<D>& x, const Powerset<D>& y);

namespace IO_Operators {


template <typename D>
std::ostream&
operator<<(std::ostream& s, const Powerset<D>& x);

} // namespace IO_Operators

} // namespace Parma_Polyhedra_Library



template <typename D>
class Parma_Polyhedra_Library::Powerset {
public:


  Powerset();

  Powerset(const Powerset& y);

  explicit Powerset(const D& d);

  ~Powerset();




  bool definitely_entails(const Powerset& y) const;

  bool is_top() const;

  bool is_bottom() const;

  memory_size_type total_memory_in_bytes() const;

  memory_size_type external_memory_in_bytes() const;

  // FIXME: document and perhaps use an enum instead of a bool.
  bool OK(bool disallow_bottom = false) const;


protected:

  typedef std::list<D> Sequence;

  typedef typename Sequence::iterator Sequence_iterator;

  typedef typename Sequence::const_iterator Sequence_const_iterator;

  Sequence sequence;

  mutable bool reduced;

public:
  // Sequence manipulation types, accessors and modifiers
  typedef typename Sequence::size_type size_type;
  typedef typename Sequence::value_type value_type;

  typedef iterator_to_const<Sequence> iterator;

  typedef const_iterator_to_const<Sequence> const_iterator;

  typedef std::reverse_iterator<iterator> reverse_iterator;

  typedef std::reverse_iterator<const_iterator> const_reverse_iterator;



  void omega_reduce() const;

  size_type size() const;

  bool empty() const;

  iterator begin();

  iterator end();

  const_iterator begin() const;

  const_iterator end() const;

  reverse_iterator rbegin();

  reverse_iterator rend();

  const_reverse_iterator rbegin() const;

  const_reverse_iterator rend() const;

  void add_disjunct(const D& d);

  iterator drop_disjunct(iterator position);

  void drop_disjuncts(iterator first, iterator last);

  void clear();




  Powerset& operator=(const Powerset& y);

  void m_swap(Powerset& y);

  void least_upper_bound_assign(const Powerset& y);


  void upper_bound_assign(const Powerset& y);

  bool upper_bound_assign_if_exact(const Powerset& y);

  void meet_assign(const Powerset& y);

  void collapse();


protected:
  bool is_omega_reduced() const;

  void collapse(unsigned max_disjuncts);

  iterator add_non_bottom_disjunct_preserve_reduction(const D& d,
                                                      iterator first,
                                                      iterator last);

  void add_non_bottom_disjunct_preserve_reduction(const D& d);

  template <typename Binary_Operator_Assign>
  void pairwise_apply_assign(const Powerset& y,
                             Binary_Operator_Assign op_assign);

private:
  bool check_omega_reduced() const;

  void collapse(Sequence_iterator sink);
};

#include "Powerset_inlines.hh"
#include "Powerset_templates.hh"

#endif // !defined(PPL_Powerset_defs_hh)