Ask_Tell_defs.hh

Go to the documentation of this file.

/* Ask_Tell 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_Ask_Tell_defs_hh
#define PPL_Ask_Tell_defs_hh

#include "Ask_Tell_types.hh"
#include "iterator_to_const_defs.hh"
#include "globals_types.hh"
#include <iosfwd>
#include <list>

namespace Parma_Polyhedra_Library {


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


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


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

namespace IO_Operators {


template <typename D>
std::ostream&
operator<<(std::ostream&, const Ask_Tell<D>&);

} // namespace IO_Operators

} // namespace Parma_Polyhedra_Library


template <typename D>
class Parma_Polyhedra_Library::Ask_Tell_Pair {
public:
  Ask_Tell_Pair(const D& ask, const D& tell);

  const D& ask() const;

  D& ask();

  const D& tell() const;

  D& tell();

  bool definitely_entails(const Ask_Tell_Pair& y) const;

private:
  D a;

  D t;
};


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


  Ask_Tell();

  Ask_Tell(const Ask_Tell& y);

  explicit Ask_Tell(const Ask_Tell_Pair<D>& p);

  Ask_Tell(const D& ask, const D& tell);

  ~Ask_Tell();




  bool definitely_entails(const Ask_Tell& 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;

  int32_t hash_code() const;

  bool OK() const;


protected:
  typedef Ask_Tell_Pair<D> Pair;


  typedef std::list<Ask_Tell_Pair<D> > Sequence;

  typedef typename Sequence::iterator Sequence_iterator;

  typedef typename Sequence::const_iterator Sequence_const_iterator;

  Sequence sequence;

  mutable bool normalized;

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 normalize() 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;

  Ask_Tell& add_pair(const Ask_Tell_Pair<D>& p);

  Ask_Tell& add_pair(const D& ask, const D& tell);

  iterator drop_pair(iterator position);

  void drop_pairs(iterator first, iterator last);

  void clear();




  Ask_Tell& operator=(const Ask_Tell& y);

  void m_swap(Ask_Tell& y);

  void upper_bound_assign(const Ask_Tell& y);

  void meet_assign(const Ask_Tell& y);


protected:
  bool is_normalized() const;

  void pair_insert(const D& a, const D& t);
  void pair_insert_good(const D& a, const D& t);

  /*
    Postcondition:
    the map is well formed and there are no two pairs x and y such that
    x.ASK.definitely_entails(y.ASK) && y.TELL.definitely_entails(x.TELL).
  */
  bool reduce();

  // Preconditions:
  //
  //     the map is well formed and the postcondition of reduce() is satisfied.
  //
  // Postconditions:
  //
  //     the map is well formed, the postcondition of reduce() is satisfied,
  //     and...
  //
  bool deduce();

  bool absorb();

  void deabsorb() const;

  bool check_normalized() const;

protected:
  bool probe(const D& tellv, const D& askv) const;
};

#include "Ask_Tell_inlines.hh"
#include "Ask_Tell_templates.hh"

#endif // !defined(PPL_Ask_Tell_defs_hh)