api/cxx/apxx__abstract1_8hh_source.html

 /* -*- 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                         */
 /* ================================= */


 class abstract1 : public use_malloc {

 protected:

   ap_abstract1_t a;

   static const abstract1 null;

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

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

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

   abstract1(const abstract1& t);


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


   ~abstract1();

   void free(manager& m);


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


   abstract1& operator=(const abstract1& t);

   abstract1& operator=(top t);

   abstract1& operator=(bottom t);

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

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

   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 */
   /* ============= */


   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;

   environment get_environment() const;

   abstract0& get_abstract0();

   const abstract0& get_abstract0() const;

   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;

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

   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;

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


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

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


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

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

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

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


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


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

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


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


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

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

   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[]);

   abstract1& add_rays(manager& m, const generator1_array& y);

   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 */
   /* =========== */


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

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


   abstract1& assign(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);

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

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

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


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

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


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

   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 */
   /* ============== */


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

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


   abstract1& substitute(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);

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

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

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


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

   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[]);

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

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

   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[]);

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


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


   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 */
apxx_abstract1_inline.hh

apron::abstract1::abstract1
abstract1(ap_abstract1_t x)
Internal use only. Shallow copy of structure.
Definition: apxx_abstract1.hh:28

apxx_linexpr1.hh

apron
Definition: apxx_abstract0.hh:27

apron::abstract1::operator!=
friend bool operator!=(const abstract1 &x, const abstract1 &y)
Whether x and y represent different sets.
Definition: apxx_abstract1.hh:516

apron::lincons1_array
Array of linear constraints (ap_lincons1_array_t wrapper).
Definition: apxx_lincons1.hh:331

apxx_lincons1.hh

apron::abstract1::approximate
abstract1 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition: apxx_abstract1.hh:332

apron::abstract1::operator=
abstract1 & operator=(const abstract1 &t)
Assigns a copy of t to *this.
Definition: apxx_abstract1.hh:125

apron::abstract1::assign
abstract1 & assign(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place assignment of linear expression.
Definition: apxx_abstract1.hh:875

apron::abstract1::get_abstract0
abstract0 & get_abstract0()
Returns a (modifiable) reference to the underlying abstract0.
Definition: apxx_abstract1.hh:411

apron::abstract1::to_lincons_array
lincons1_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition: apxx_abstract1.hh:594

apron::abstract1::free
void free(manager &m)
Destroys the abstract element using the given manager.
Definition: apxx_abstract1.hh:115

apron::tcons1_array
Array of arbitrary constraints (ap_tcons1_array_t wrapper).
Definition: apxx_tcons1.hh:337

apron::var
Variable name (ap_var_t wrapper).
Definition: apxx_var.hh:39

apron::abstract1::operator+=
abstract1 & operator+=(const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract1.hh:823

apron::interval_array
array of interval(s).
Definition: apxx_interval.hh:302

apron::abstract1::minimize
abstract1 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition: apxx_abstract1.hh:318

apxx_abstract0.hh

apron::abstract1::operator>=
friend bool operator>=(const abstract1 &x, const abstract1 &y)
Whether x contains y (set-wise).
Definition: apxx_abstract1.hh:530

apron::abstract1::to_box
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition: apxx_abstract1.hh:582

apron::abstract1::to_tcons_array
tcons1_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition: apxx_abstract1.hh:604

apron::abstract1::to_generator_array
generator1_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition: apxx_abstract1.hh:614

apron::abstract1::is_top
bool is_top(manager &m) const
Whether *this represents the full space.
Definition: apxx_abstract1.hh:443

apron::abstract1::abstract1
abstract1(manager &m, const lincons1_array &x)
Creates an abstract element from a conjunction of linear constraints.
Definition: apxx_abstract1.hh:83

apron::abstract1::fold
abstract1 & fold(manager &m, size_t size, const var v[])
Folds variables v[0] to v[size-1] in *this (modified in-place).
Definition: apxx_abstract1.hh:1487

apron::abstract0
Level 0 abstract value (ap_abstract0_t* wrapper).
Definition: apxx_abstract0.hh:78

apron::abstract1::deserialize
friend abstract1 & deserialize(manager &m, abstract1 &dst, const std::string &s, size_t *eaten)
Reconstruct an abstract element form a serialized byte-stream and put it into dst.
Definition: apxx_abstract1.hh:385

apron::abstract1::is_leq
bool is_leq(manager &m, const abstract1 &x) const
Whether *this is included in x (set-wise).
Definition: apxx_abstract1.hh:460

apron::abstract1::is_bottom
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition: apxx_abstract1.hh:435

apron::manager
Library manager (ap_manager_t wrapper).
Definition: apxx_manager.hh:137

apron::abstract1::join
abstract1 & join(manager &m, const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract1.hh:696

apron::abstract1::meet
abstract1 & meet(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1.hh:649

apron::abstract1::dump
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition: apxx_abstract1.hh:357

apxx_generator1.hh

apron::abstract1::expand
abstract1 & expand(manager &m, const var &v, size_t size, const var vv[])
Duplicates variable v into size copies in *this (modified in-place).
Definition: apxx_abstract1.hh:1435

apron::environment
Level 1 environment (ap_environment_t wrapper).
Definition: apxx_environment.hh:51

apron::abstract1::change_environment
abstract1 & change_environment(manager &m, const environment &e, bool project=false)
Modifies the environment of *this.
Definition: apxx_abstract1.hh:1330

apron::abstract1::add_rays
abstract1 & add_rays(manager &m, const generator1_array &y)
Adds some rays to *this (modified in-place).
Definition: apxx_abstract1.hh:789

apron::abstract1::rename
abstract1 & rename(manager &m, size_t size, const var oldv[], const var newv[])
Renames oldv[i] into newv[i] in *this.
Definition: apxx_abstract1.hh:1370

apron::abstract1::unify
abstract1 & unify(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1.hh:628

apron::abstract1::closure
abstract1 & closure(manager &m)
Replaces *this with its topological closure.
Definition: apxx_abstract1.hh:1566

apron::abstract1::forget
abstract1 & forget(manager &m, const var &v, bool project=false)
Forgets about the value of variable v in *this.
Definition: apxx_abstract1.hh:1272

apron::abstract1::operator>
friend bool operator>(const abstract1 &x, const abstract1 &y)
Whether x strictly contains y (set-wise).
Definition: apxx_abstract1.hh:535

apron::lincons1
Level 1 linear constraint (ap_lincons1_t wrapper).
Definition: apxx_lincons1.hh:40

apron::abstract1::bound
interval bound(manager &m, const linexpr1 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element.
Definition: apxx_abstract1.hh:550

apron::linexpr1
Level 1 linear expression (ap_linexpr1_t wrapper).
Definition: apxx_linexpr1.hh:39

apron::abstract1::operator<<
friend std::ostream & operator<<(std::ostream &os, const abstract1 &s)
Prints in constraint form.
Definition: apxx_abstract1.hh:363

apron::abstract1::canonicalize
abstract1 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition: apxx_abstract1.hh:325

apron::bottom
Empty interval or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:33

apron::abstract1
Level 1 abstract value (ap_abstract1_t wrapper).
Definition: apxx_abstract1.hh:42

apron::top
Full interval (]-oo,+oo[) or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:27

apron::abstract1::serialize
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition: apxx_abstract1.hh:375

apron::abstract1::print
void print(manager &m, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition: apxx_abstract1.hh:343

apron::interval
Interval (ap_interval_t wrapper).
Definition: apxx_interval.hh:47

apron::use_malloc
Inherited by most wrappers to map new and delete to malloc and free.
Definition: apxx_scalar.hh:69

apron::abstract1::a
ap_abstract1_t a
Structure managed by APRON.
Definition: apxx_abstract1.hh:46

apron::abstract1::operator *=
abstract1 & operator *=(const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1.hh:813

apron::abstract1::is_eq
bool is_eq(manager &m, const abstract1 &x) const
Whether *this and x represent the same set.
Definition: apxx_abstract1.hh:451

apron::abstract1::set
abstract1 & set(manager &m, const abstract1 &x)
Replaces *this with a copy of x.
Definition: apxx_abstract1.hh:193

apron::abstract1::minimize_environment
abstract1 & minimize_environment(manager &m)
Removes from *this the variables that are unconstrained.
Definition: apxx_abstract1.hh:1352

apron::abstract1::size
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition: apxx_abstract1.hh:421

apron::abstract1::printdiff
friend void printdiff(manager &m, const abstract1 &x, const abstract1 &y, FILE *stream)
Pretty-printing the difference between x and y to a C stream.
Definition: apxx_abstract1.hh:349

apron::abstract1::operator<
friend bool operator<(const abstract1 &x, const abstract1 &y)
Whether x is strictly included within y (set-wise).
Definition: apxx_abstract1.hh:540

apron::abstract1::substitute
abstract1 & substitute(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place substitution (backward assignment) of linear expression.
Definition: apxx_abstract1.hh:1073

apron::texpr1
Level 1 arbitrary expression tree (ap_texpr1_t wrapper).
Definition: apxx_texpr1.hh:42

apron::tcons1
Level 1 arbitrary constraint (ap_tcons1_t wrapper).
Definition: apxx_tcons1.hh:39

apron::abstract1::get_ap_abstract1_t
ap_abstract1_t * get_ap_abstract1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_abstract1.hh:1587

apron::abstract1::operator==
friend bool operator==(const abstract1 &x, const abstract1 &y)
Whether x and y represent the same set.
Definition: apxx_abstract1.hh:507

apron::generator1_array
Array of generators (ap_generator1_array_t wrapper).
Definition: apxx_generator1.hh:272

apron::abstract1::widening
friend abstract1 & widening(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Stores in dst the result of x widened with y.
Definition: apxx_abstract1.hh:1536

apron::abstract1::get_manager
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition: apxx_abstract1.hh:401

apron::abstract1::get_environment
environment get_environment() const
Returns the environment of the abstract element (with reference count incremented).
Definition: apxx_abstract1.hh:406

apron::abstract1::operator<=
friend bool operator<=(const abstract1 &x, const abstract1 &y)
Whether x is included within y (set-wise).
Definition: apxx_abstract1.hh:521

apron::abstract1::sat
bool sat(manager &m, const lincons1 &l) const
Whether all points in *this satisfy a linear constraint.
Definition: apxx_abstract1.hh:469

apron::abstract1::~abstract1
~abstract1()
Destroys the abstract element.
Definition: apxx_abstract1.hh:109

apron::abstract1::is_variable_unconstrained
bool is_variable_unconstrained(manager &m, const var &v) const
Whether the points in *this are unbounded in the given variable.
Definition: apxx_abstract1.hh:497