/home/mine/apron/apronxx/apxx_abstract1.hh

Go to the documentation of this file.

/* -*- C++ -*-
 * apxx_abstract1.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_ABSTRACT1_HH
#define __APXX_ABSTRACT1_HH
 
#include "ap_abstract1.h"
#include "apxx_abstract0.hh"
#include "apxx_linexpr1.hh"
#include "apxx_lincons1.hh"
#include "apxx_generator1.hh"
 
 
namespace apron {
 
 
/* ================================= */
/* abstract1                         */
/* ================================= */
 


 * Internally, an abstract1 wraps together an abstract0 (memory managed) and an environment
 * (holding a reference count).
 */
 
class abstract1 : public use_malloc {
 
protected:
 
  ap_abstract1_t a; 

  static const abstract1 null;

  //! Internal use only. Shallow copy of structure.
  abstract1(ap_abstract1_t x);
 
  friend class manager;
 
public:
 
 
  /* constructors */
  /* ============ */


  abstract1(manager &m, const environment& e, top x);


  abstract1(manager &m, const environment& e, bottom x);

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

  abstract1(manager &m, const environment& e, const abstract0& t);

  abstract1(manager &m, const environment& e, const var v[], const interval_array& x);

  abstract1(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x);

  //! Creates an abstract element from a conjunction of linear constraints.
  abstract1(manager &m, const lincons1_array& x);

  abstract1(manager &m, const tcons1_array& x);


   * Implicitly uses the manager used to create *this.
   */
  abstract1(const abstract1& t);

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

  /** @name Destructors */


   */
  ~abstract1();


  void free(manager& m);

  //@}
 
 
  /* assignments */
  /* =========== */



   */
  abstract1& operator=(const abstract1& t);

  abstract1& operator=(top t);

  /*! \brief Assigns the empty set to *this.
   *
   * Implicitly uses the manager used to create *this.
   * Does not change the environment.
   */
  abstract1& operator=(bottom t);


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

  abstract1& operator=(const lincons1_array& x);

  abstract1& operator=(const tcons1_array& x);

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

  abstract1& set(manager& m, top t);


  abstract1& set(manager& m, const environment& e, top t);

  abstract1& set(manager& m, bottom t);


   */
  abstract1& set(manager& m, const environment& e, bottom t);


  abstract1& set(manager& m, const interval_array& x);
 

  abstract1& set(manager &m, const environment& e, const var v[], const interval_array& x);


   *
   * \return a reference to *this.
   */
  abstract1& set(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x);


  abstract1& set(manager& m, const lincons1_array& x);

  abstract1& set(manager& m, const tcons1_array& x);
 


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


  abstract1& minimize(manager& m);

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

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

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


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

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

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

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

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



   * The string can be safely stored to disk and reloaded later or transmitted across a network.
   * The format is library-specific but is generally a machine-readable byte-stream.
   *
   * \return a newly allocated string that the caller should delete it after use.
   */
  std::string* serialize(manager& m) const;


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

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


  manager get_manager() const;

   //! Returns the environment of the abstract element (with reference count incremented).
  environment get_environment() const;

  abstract0& get_abstract0();


  const abstract0& get_abstract0() const;

   * 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 abstract1& x) const;

  bool is_leq(manager& m, const abstract1& x) const;


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

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

  bool sat(manager& m, const var& v, const interval& i) const;

  bool is_variable_unconstrained(manager& m, const var& v) const;


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

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


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


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


   */
  friend bool operator> (const abstract1& x, const abstract1& y);


   * The manager for the left argument is used implicitly.
   */
  friend bool operator< (const abstract1& x, const abstract1& y);
 
 
 
  /* Properties */
  /* ========== */



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

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

  interval bound(manager& m, const var& v) const;

  interval_array to_box(manager& m) const;


  generator1_array to_generator_array(manager& m) const;

  lincons1_array to_lincons_array(manager& m) const;


   * set represented by the abstract element.
   */
  tcons1_array to_tcons_array(manager& m) const;

 
 
  /* Meet and unification */
  /* ==================== */


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

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


   *
   * *this and y can have different environment.
   * They are first embedded into the least common environment before the meet is computed.
   *
   * \return a reference to *this.
   */
  abstract1& unify(manager& m, const abstract1& y);


   *
   * x and y can have different environment.
   * They are first embedded into the least common environment before the meet is computed.
   *
   * \return a reference to dst.
   */
  friend abstract1& unify(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);
 


   *
   * \return a reference to dst.
   */
  friend abstract1& meet(manager& m, abstract1& dst, const std::vector<const abstract1*>& x);


  friend abstract1& meet(manager& m, abstract1& dst, size_t size, const abstract1 * const x[]);

  abstract1& meet(manager& m, const lincons1_array& y);


   * \return a reference to dst.
   */
  friend abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const lincons1_array& y);


   *
   * \return a reference to *this.
   */
  abstract1& meet(manager& m, const tcons1_array& y);


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


   * Implicitly uses the manager used to create *this.
   *
   * \return a reference to *this.
   */
  abstract1& operator*=(const abstract1& y);
 


  abstract1& operator*=(const lincons1_array& y);

  /*! \brief Adds some arbitrary constraints to *this (modified in-place).
   *
   * Implicitly uses the manager used to create *this.
   *
   * \return a reference to *this.
   */
  abstract1& operator*=(const tcons1_array& y);

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



   * \return a reference to *this.
   */
  abstract1& join(manager& m, const abstract1& y);

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


   *
   * \return a reference to dst.
   */
  friend abstract1& join(manager& m, abstract1& dst, const std::vector<const abstract1*>& x);

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


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


   *
   * \return a reference to *this.
   */
  friend abstract1& add_rays(manager& m, abstract1& dst, const abstract1& x, const generator1_array& y);


   */
  abstract1& operator+=(const abstract1& y);


  abstract1& operator+=(const generator1_array& y);

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



   *
   * *this is modified in-place to reflect the effect of assigning l to variable v.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract1& assign(manager& m, const var& v, const linexpr1& l, const abstract1& inter = null);


   * Assignments are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract1& assign(manager& m,  size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = null);
 


   *
   * *this is modified in-place to reflect the effect of assigning l[i] to variable v[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.
   */
  abstract1& assign(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);


   *
   * dst is replaced with the effect of assigning l to variable v in src.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter);


   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src,  size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter);


   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter);
 
 
 


   *
   * *this is modified in-place to reflect the effect of assigning l to variable v.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract1& assign(manager& m, const var& v, const texpr1& l, const abstract1& inter = null);


   * Assignments are performed in parallel.
   * If inter is specified, *this is then intersected with it.
   *
   * \return a reference to *this.
   */
  abstract1& assign(manager& m, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = null);
 


   *
   * \return a reference to *this.
   *
   * \throw std::invalid_argument if the vectors have different size.
   */
  abstract1& assign(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = null);


   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter);


   * \return a reference to dst.
   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter);


   */
  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter);

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

  /** @name Substitution */

  abstract1& substitute(manager& m, const var& v, const linexpr1& l, const abstract1& inter = null);

   * *this is modified in-place to reflect the effect of substituting l[i] to variable v[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.
   */
  abstract1& substitute(manager& m, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = null);
 

  /*! \brief In-place parallel substitution (backward assignment) of linear expressions.
   *
   * *this is modified in-place to reflect the effect of substituting l[i] to variable v[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.
   */
  abstract1& substitute(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);

   * dst is replaced with the effect of substituting l to variable v in src.
   * If inter is specified, dst is then intersected with it.
   *
   * \return a reference to dst.
   */
  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter);


   * 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 abstract1& substitute(manager& m, abstract1& dst, const abstract1& src,  size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter);


   * dst is replaced with the effect of substituting l[i] to variable v[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 abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter);
 
 
 


  abstract1& substitute(manager& m, const var& v, const texpr1& l, const abstract1& inter = null);


  abstract1& substitute(manager& m,  size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = null);
 

   *
   * *this is modified in-place to reflect the effect of substituting l[i] to variable v[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.
   */
  abstract1& substitute(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = null);


  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter);

  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src,  size_t size, const var v[], const texpr1 * const l[], const abstract1& inter);

   *
   * dst is replaced with the effect of substituting l[i] to variable v[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 abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter);

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

  //@{

  abstract1& forget(manager& m, const var& v, bool project = false);


   */
  abstract1& forget(manager& m, size_t size, const var v[], bool project = false);

  abstract1& forget(manager& m, const std::vector<var>& v, bool project = false);


   */
  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const var& v, bool project);

  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], bool project);

  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, bool project);


 
 
  /* Change of environment */
  /* ====================== */


   abstract1& change_environment(manager& m, const environment& e, bool project = false);

  friend abstract1& change_environment(manager& m, abstract1& dst, const abstract1& src, const environment& e, bool project);


   */
  abstract1& minimize_environment(manager& m);

  friend abstract1& minimize_environment(manager& m, abstract1& dst, const abstract1& src);

  abstract1& rename(manager& m, size_t size, const var oldv[], const var newv[]);


   * \return a reference to *this.
   */
  abstract1& rename(manager& m, const std::vector<var>& oldv, const std::vector<var>& newv);

  friend abstract1& rename(manager& m, abstract1& dst, const abstract1& src, size_t size, const var oldv[], const var newv[]);

  friend abstract1& rename(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& oldv, const std::vector<var>& newv);

 
 
  /* Expansion and folding */
  /* ===================== */



  abstract1& expand(manager& m, const var& v, size_t size, const var vv[]);

  abstract1& expand(manager& m, const var& v, const std::vector<var>& vv);

  friend abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, size_t size, const var vv[]);


  friend abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, const std::vector<var>& vv);

   *
   * After folding, only v[0] is kept and other variables are removed.
   *
   * \return a reference to *this.
   */
  abstract1& fold(manager& m,  size_t size, const var v[]);


   * \return a reference to *this.
   */
  abstract1& fold(manager& m, const std::vector<var>& v);

  friend abstract1& fold(manager& m, abstract1& dst, const abstract1& src,  size_t size, const var v[]);


   * After folding, only v[0] is kept and other variables are removed.
   *
   * \return a reference to dst.
   */
  friend abstract1& fold(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v);

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



   * \return a reference to dst.
   */
  friend abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);

  friend abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y, const lincons1_array& l);

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

 

  abstract1& closure(manager& m);


   */
  friend abstract1& closure(manager& m, abstract1& dst, const abstract1& src);

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


  ap_abstract1_t* get_ap_abstract1_t();

  const ap_abstract1_t* get_ap_abstract1_t() const;

 
};
 
#include "apxx_abstract1_inline.hh"
 
}
 
#endif /* __APXX_ABSTRACT1_HH */