/home/mine/apron/apronxx/apxx_abstract0.hh

Go to the documentation of this file.

/* -*- C++ -*-
 * apxx_abstract0.hh
 *
 * APRON Library / C++ class wrappers
 *
 * Copyright (C) Antoine Mine' 2007
 *
 */
/* This file is part of the APRON Library, released under LGPL license
   with an exception allowing the redistribution of statically linked
   executables.
 
   Please read the COPYING file packaged in the distribution.
*/
 
#ifndef __APXX_ABSTRACT0_HH
#define __APXX_ABSTRACT0_HH
 
#include <string>
#include "ap_abstract0.h"
#include "apxx_linexpr0.hh"
#include "apxx_lincons0.hh"
#include "apxx_generator0.hh"
#include "apxx_manager.hh"
 
 
namespace apron {
 
 
/* ================================= */
/* abstract0                         */
/* ================================= */


 * real-valued dimensions.
 *
 * \warning all the abstract operators are guaranteed to be sound, but not complete, that is:
 * - returned abstract elements and intervals are over-approximations of the actual result on sets,
 * - returned constraint conjunction may satisfy more points than the original abstract element,
 * - returned generators may span more points than the original abstract element,
 * - predicates return \c true if the predicate is definitively true,
 * and \c false if either the predicate is false (flag_exact is then true), or
 * due to abstraction, the domain cannot conclude (flag_exact is then false).
 *
 * An abstract0 is always created with a manager that indicates the underlying library. This
 * defines its internal representation and algorithms, which in turns defines the expressiveness and
 * cost vs. precision trade-off.
 * Most operations to manipulate an abstract0 also take a manager as first argument.
 * This must be a manager compatible with the one of all abstract0 arguments (including this),
 * that is, a manger created by the same library (e.g., NewPolka polyhedra) and using the same
 * parameter values, if any (e.g., strictness).
 * It need not be the very same manager the abstract0 was created with.
 *
 * Overloaded arithmetic, assignment and copy operators that cannot take an extra manager
 * argument will implicitly use the manager used to create the first argument.
 *
 * Additionally, for binary or n-aray operators, all abstract0 must have the same number of
 * integer and real dimensions.
 *
 * Many operations exist in two kinds:
 * - an imperative class function that modifies the this abstract0,
 * - a more "functional" global function that takes as argument both one or several constant
 * source abstract0 and one destination abstract0 that will be overridden with the result.
 *
 * Both kinds will return a reference to the abstract0 that holds the result.
 *
 * Most functions can throw a variety of exceptions:
 * - std::invalid_argument, when arguments have incompatible managers, types, or dimensions,
 * - std::length_error, when running out of memory or exceeding the \c max_object_size
 * value set by the user in the manager,
 * - std::overflow_error, when a numerical overflow occurs,
 * - not_implemented, when some function is not available,
 * - timeout, when exceeding the \c timout value set by the user in the manager.
 */
class abstract0 : public use_malloc {
 
protected:
 
  ap_abstract0_t* a; 

  //! Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object.
  abstract0(ap_abstract0_t* x);

  static const abstract0 null;
 
  friend class manager;
 
public:
 
 
  /* constructors */
  /* ============ */


  abstract0(manager &m, size_t intdim, size_t realdim, top x);

  abstract0(manager &m, size_t intdim, size_t realdim, bottom x);

  abstract0(manager &m, const abstract0& t);


   *
   * \throw std::invalid_argument if x has less than intdim+realdim dimensions.
   */
  abstract0(manager &m, size_t intdim, size_t realdim, const interval_array& x);

  abstract0(manager &m, size_t intdim, size_t realdim, const lincons0_array& x);

  abstract0(manager &m, size_t intdim, size_t realdim, const tcons0_array& x);

  abstract0(const abstract0& t);

 
 
  /* destructor */
  /* ========== */


  ~abstract0();


   *
   * The abstract element cannot be used after being freed.
   * However, the standard destructor can be safely be called (resulting in a no-op).
   */
  void free(manager& m);

 
 
  /* assignments */
  /* =========== */

  /** @name Copies and conversions to abstract elements */

  abstract0& operator=(const abstract0& t);


   */
  abstract0& operator=(top t);

  abstract0& operator=(bottom t);


   * Implicitly uses the manager used to create *this.
   *
   * \throw std::invalid_argument if the array has insufficient size.
   */
  abstract0& operator=(const interval_array& x);

  abstract0& operator=(const lincons0_array& x);

  /*! \brief Assigns a conjunction of arbitrary constraints to *this.
   *
   * Implicitly uses the manager used to create *this.
   */
  abstract0& operator=(const tcons0_array& x);

  abstract0& set(manager& m, const abstract0& x);

  /*! \brief Replaces *this with the full space.
   *
   * You can either specify new intdim and realdim values or keep those of *this
   * (if unspecified, i.e., left to \c AP_DIM_MAX).
   *
   * \return a reference to *this.
   */
  abstract0& set(manager& m, top t, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);


   */
  abstract0& set(manager& m, bottom t, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);

  abstract0& set(manager& m, const interval_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);


   * You can either specify new intdim and realdim values or keep those of *this
   * (if unspecified, i.e., left to \c AP_DIM_MAX).
   *
   * \return a reference to *this.
   */
  abstract0& set(manager& m, const lincons0_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);


  abstract0& set(manager& m, const tcons0_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
 

 
 
  /* representation */
  /* ============== */



  abstract0& minimize(manager& m);

  /*! \brief Puts the abstract element in canonical form (if such a notion exists).
   *
   * \return a reference to *this.
   */
  abstract0& canonicalize(manager& m);


  abstract0& approximate(manager& m, int algorithm);

 
 
  /* printing */
  /* ======== */


  void print(manager& m, char** name_of_dim=NULL, FILE* stream=stdout) const;

  friend void printdiff(manager& m, const abstract0& x, const abstract0& y, char** name_of_dim, FILE* stream);

  void dump(manager& m, FILE* stream=stdout) const;

  friend std::ostream& operator<< (std::ostream& os, const abstract0& s);

 
 
  /* serialisation */
  /* ============= */


  std::string* serialize(manager& m) const;

  friend abstract0& deserialize(manager& m, abstract0& dst, const std::string& s, size_t* eaten);

 
 
  /* access */
  /* ====== */



  manager get_manager() const;

  ap_dimension_t get_dimension(manager& m) const;

  /*! \brief Returns the (abstract) size of the abstract element.
   *
   * The unit in which size is computed is library-specific.
   * It is guaranteed to be the same as the unit for the \c max_object_size field of
   * the ap_funopt_t structure.
   */
  size_t size(manager& m) const;

 
 
  /* predicates */
  /* ========== */


  bool is_bottom(manager& m) const;

  bool is_top(manager& m) const;

  bool is_eq(manager& m, const abstract0& x) const;

  //! Whether *this is included in x (set-wise).
  bool is_leq(manager& m, const abstract0& x) const;

  bool sat(manager& m, const lincons0& l) const;


  bool sat(manager& m, const tcons0& l) const;

  bool sat(manager& m, ap_dim_t dim, const interval& i) const;

  //! \brief Whether the points in *this are unbounded in the given dimension.
  bool is_dimension_unconstrained(manager& m, ap_dim_t dim) const;


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

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

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

  /*! \brief Whether x contains y (set-wise).
   *
   * The manager for the left argument is used implicitly.
   */
  friend bool operator>= (const abstract0& x, const abstract0& y);


   * The manager for the left argument is used implicitly.
   */
  friend bool operator> (const abstract0& x, const abstract0& y);


   */
  friend bool operator< (const abstract0& x, const abstract0& y);
 
 
 
  /* Properties */
  /* ========== */



  interval bound(manager& m, const linexpr0& l) const;

  interval bound(manager& m, const texpr0& l) const;

  //! Returns some bounds for the given coordinate on all points in the abstract element.
  interval bound(manager& m, ap_dim_t d) const;

  interval_array to_box(manager& m) const;

  generator0_array to_generator_array(manager& m) const;

  lincons0_array to_lincons_array(manager& m) const;

  tcons0_array to_tcons_array(manager& m) const;

 
 
  /* Meet */
  /* ==== */



  abstract0& meet(manager& m, const abstract0& y);

  friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);

  /*! \brief Replaces dst with the meet of all abstract elements in x.
   *
   * \return a reference to dst.
   */
  friend abstract0& meet(manager& m, abstract0& dst, const std::vector<const abstract0*>& x);


   * \return a reference to dst.
   */
  friend abstract0& meet(manager& m, abstract0& dst, size_t size, const abstract0 * const x[]);


  abstract0& meet(manager& m, const lincons0_array& y);

  friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const lincons0_array& y);

  /*! \brief Adds some arbitrary constraints to *this (modified in-place).
   *
   * \return a reference to *this.
   */
  abstract0& meet(manager& m, const tcons0_array& y);


  friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const tcons0_array& y);
 


  abstract0& operator*=(const abstract0& y);
 


  abstract0& operator*=(const lincons0_array& y);

  abstract0& operator*=(const tcons0_array& y);

 
 
 
 
  /* Join */
  /* ==== */


  abstract0& join(manager& m, const abstract0& y);

  friend abstract0& join(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);

  /*! \brief Replaces dst with the join of all abstract elements in x.
   *
   * \return a reference to dst.
   */
  friend abstract0& join(manager& m, abstract0& dst, const std::vector<const abstract0*>& x);


   */
  friend abstract0& join(manager& m, abstract0& dst, size_t size, const abstract0 * const x[]);

  abstract0& add_rays(manager& m, const generator0_array& y);


   * \arg \c y can only contain rays and lines, not vertexes.
   *
   * \return a reference to *this.
   */
  friend abstract0& add_rays(manager& m, abstract0& dst, const abstract0& x, const generator0_array& y);

  abstract0& operator+=(const abstract0& y);


   */
  abstract0& operator+=(const generator0_array& y);

 
 
  /* Assignments */
  /* =========== */



  /*! \brief In-place assignment of linear expression.
   *
   * *this is modified in-place to reflect the effect of assigning l to dimension dim.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract0& assign(manager& m, ap_dim_t dim, const linexpr0& l, const abstract0& inter = null);

  abstract0& assign(manager& m,  size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter = null);
 

  /*! \brief In-place parallel assignment of linear expressions.
   *
   * *this is modified in-place to reflect the effect of assigning l[i] to dimension dim[i].
   * Assignments are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  abstract0& assign(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter = null);


  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const linexpr0& l, const abstract0& inter);

  /*! \brief Parallel assignment of linear expressions.
   *
   * dst is replaced with the effect of assigning l[i] to dimension dim[i] in src,
   * for i from 0 to size-1.
   * Assignments are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src,  size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter);


   * Assignments are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter);
 
 
 


   *
   * \return a reference to *this.
   */
  abstract0& assign(manager& m, ap_dim_t dim, const texpr0& l, const abstract0& inter = null);


   * \return a reference to *this.
   */
  abstract0& assign(manager& m, size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter = null);
 


   *
   * *this is modified in-place to reflect the effect of assigning l[i] to dimension dim[i].
   * Assignments are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  abstract0& assign(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter = null);

  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const texpr0& l, const abstract0& inter);


   * for i from 0 to size-1.
   * Assignments are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter);

  friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter);

 
 
  /* Substitutions */
  /* ============== */



  abstract0& substitute(manager& m, ap_dim_t dim, const linexpr0& l, const abstract0& inter = null);


   * Substitutions are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract0& substitute(manager& m, size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter = null);
 


   * *this is modified in-place to reflect the effect of substituting l[i] to dimension dim[i].
   * Substitutions are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  abstract0& substitute(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter = null);


   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const linexpr0& l, const abstract0& inter);

  /*! \brief Parallel substitution (backward assignment) of linear expressions.
   *
   * dst is replaced with the effect of substituting l[i] to dimension dim[i] in src,
   * for i from 0 to size-1.
   * Substitutions are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src,  size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter);


   * dst is replaced with the effect of substituting l[i] to dimension dim[i] in src.
   * Substitutions are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter);
 
 
 

   * \return a reference to *this.
   */
  abstract0& substitute(manager& m, ap_dim_t dim, const texpr0& l, const abstract0& inter = null);


   * *this is modified in-place to reflect the effect of substituting l[i] to dimension dim[i], for
   * i from 0 to size-1.
   * Substitutions are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract0& substitute(manager& m,  size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter = null);
 

  /*! \brief In-place parallel substitution (backward assignment) of arbitrary expressions.
   *
   * *this is modified in-place to reflect the effect of substituting l[i] to dimension dim[i].
   * Substitutions are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  abstract0& substitute(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter = null);


   *
   * dst is replaced with the effect of substituting l to dimension dim in src.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const texpr0& l, const abstract0& inter);

  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src,  size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter);

  /*! \brief Parallel substitution (backward assignment) of arbitrary expressions.
   *
   * dst is replaced with the effect of substituting l[i] to dimension dim[i] in src.
   * Substitutions are performed in parallel.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter);


 
 
 
  /* Projection */
  /* ========== */



   *
   * \arg \c project whether to reset the dimension to 0 (if true), or leave it undefined (if false).
   *
   * \return a reference to *this.
   */
  abstract0& forget(manager& m, ap_dim_t dim, bool project = false);


   *
   * \return a reference to *this.
   */
  abstract0& forget(manager& m, size_t size, const ap_dim_t dim[], bool project = false);

  abstract0& forget(manager& m, const std::vector<ap_dim_t> dim, bool project = false);

  /*! \brief Stores in dst the result of forgetting the value of dimension dim in src.
   *
   * \arg \c project if true, resets the dimension to 0 (if true).
   *
   * \return a reference to dst.
   */
  friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, bool project);

  friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, size_t size, const ap_dim_t dim[], bool project);


   * \arg \c project whether to reset the dimensions to 0 (if true), or leave them undefined (if false).
   *
   * \return a reference to dst.
   */
  friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t> dim, bool project);

 
 
  /* Change of dimension */
  /* =================== */


 

   *
   * \return a reference to *this.
   */
  abstract0& add_dimensions(manager& m, const dimchange& d, bool project = false);

  /*! \brief Removes some dimensions from *this.
   *
   * \return a reference to *this.
   */
  abstract0& remove_dimensions(manager& m, const dimchange& d);


   */
  abstract0& permute_dimensions(manager& m, const dimperm& d);
 


   *
   * \return a reference to dst.
   */
  friend abstract0& add_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimchange& d, bool project);

  /*! \brief Copies src into dst and removes some dimensions.
   *
   * \return a reference to dst.
   */
  friend abstract0& remove_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimchange& d);

  friend abstract0& permute_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimperm& d);

  //@}
 
 
  /* Expansion and folding */
  /* ===================== */



   * New dimensions are appended after the last integer or real dimension of *this.
   *
   * \return a reference to *this.
   */
  abstract0& expand(manager& m, ap_dim_t dim, size_t n = 1);


   * \return a reference to dst.
   */
  friend abstract0& expand(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, size_t n);


   *
   * \return a reference to *this.
   */
  abstract0& fold(manager& m,  size_t size, const ap_dim_t dim[]);


   * After folding, only dim[0] is kept and other dimensions are removed.
   *
   * \return a reference to *this.
   */
  abstract0& fold(manager& m, const std::vector<ap_dim_t>& dim);


   */
  friend abstract0& fold(manager& m, abstract0& dst, const abstract0& src,  size_t size, const ap_dim_t dim[]);

  friend abstract0& fold(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim);

 
 
  /* Widenings */
  /* ========= */



  friend abstract0& widening(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);


   */
  friend abstract0& widening(manager& m, abstract0& dst, const abstract0& x, const abstract0& y, const lincons0_array& l);

 
 
  /* Closure */
  /* ======= */

  /** @name Closure */
 


   */
  abstract0& closure(manager& m);


  friend abstract0& closure(manager& m, abstract0& dst, const abstract0& src);

 
 
 
  /* C-level compatibility */
  /* ===================== */


  //@{

  ap_abstract0_t* get_ap_abstract0_t();

  const ap_abstract0_t* get_ap_abstract0_t() const;

 
};
 
#include "apxx_abstract0_inline.hh"
 
}
 
#endif /* __APXX_ABSTRACT0_HH */