APRONXX  0.9.12
Protected Member Functions | Protected Attributes | Static Protected Attributes | List of all members
apron::abstract1 Class Reference

Level 1 abstract value (ap_abstract1_t wrapper). More...

#include <apxx_abstract1.hh>

Inherits apron::use_malloc.

Public Member Functions

Constructors
 abstract1 (manager &m, const environment &e, top x)
 Creates an abstract element representing the whole space. More...
 
 abstract1 (manager &m, const environment &e, bottom x)
 Creates an abstract element representing the empty set. More...
 
 abstract1 (manager &m, const abstract1 &t)
 Creates a (deep) copy of the abstract element. More...
 
 abstract1 (manager &m, const environment &e, const abstract0 &t)
 Creates a (deep) copy of the abstract element and associates an environment (reference count incremented). More...
 
 abstract1 (manager &m, const environment &e, const var v[], const interval_array &x)
 Creates an abstract element from a box. More...
 
 abstract1 (manager &m, const environment &e, const std::vector< var > &v, const interval_array &x)
 Creates an abstract element from a box. More...
 
 abstract1 (manager &m, const lincons1_array &x)
 Creates an abstract element from a conjunction of linear constraints. More...
 
 abstract1 (manager &m, const tcons1_array &x)
 Creates an abstract element from a conjunction of arbitrary constraints. More...
 
 abstract1 (const abstract1 &t)
 Creates a (deep) copy of the abstract element. More...
 
Destructors
 ~abstract1 ()
 Destroys the abstract element. More...
 
void free (manager &m)
 Destroys the abstract element using the given manager. More...
 
Copies and conversions to abstract elements
abstract1operator= (const abstract1 &t)
 Assigns a copy of t to *this. More...
 
abstract1operator= (top t)
 Assigns the full space to *this. More...
 
abstract1operator= (bottom t)
 Assigns the empty set to *this. More...
 
abstract1operator= (const interval_array &x)
 Assigns a box to *this. More...
 
abstract1operator= (const lincons1_array &x)
 Assigns a conjunction of linear constraints to *this. More...
 
abstract1operator= (const tcons1_array &x)
 Assigns a conjunction of arbitrary constraints to *this. More...
 
abstract1set (manager &m, const abstract1 &x)
 Replaces *this with a copy of x. More...
 
abstract1set (manager &m, top t)
 Replaces *this with the full space. More...
 
abstract1set (manager &m, const environment &e, top t)
 Replaces *this with the full space. More...
 
abstract1set (manager &m, bottom t)
 Replaces *this with the empty set. More...
 
abstract1set (manager &m, const environment &e, bottom t)
 Replaces *this with the empty set. More...
 
abstract1set (manager &m, const interval_array &x)
 Replaces *this with a box. More...
 
abstract1set (manager &m, const environment &e, const var v[], const interval_array &x)
 Replaces *this with a box. More...
 
abstract1set (manager &m, const environment &e, const std::vector< var > &v, const interval_array &x)
 Replaces *this with a box. More...
 
abstract1set (manager &m, const lincons1_array &x)
 Replaces *this with a conjunction of linear constraints. More...
 
abstract1set (manager &m, const tcons1_array &x)
 Replaces *this with a conjunction of arbitrary constraints. More...
 
Control of internal representation
abstract1minimize (manager &m)
 Minimizes the size of the representation, to save memory. More...
 
abstract1canonicalize (manager &m)
 Puts the abstract element in canonical form (if such a notion exists). More...
 
abstract1approximate (manager &m, int algorithm)
 Simplifies the abstract element, potentially loosing precision. More...
 
Access
manager get_manager () const
 Returns the manager the abstract element was created with (with reference count incremented). More...
 
environment get_environment () const
 Returns the environment of the abstract element (with reference count incremented). More...
 
abstract0get_abstract0 ()
 Returns a (modifiable) reference to the underlying abstract0. More...
 
const abstract0get_abstract0 () const
 Returns a reference to the underlying abstract0. More...
 
size_t size (manager &m) const
 Returns the (abstract) size of the abstract element. More...
 
Property extraction
interval bound (manager &m, const linexpr1 &l) const
 Returns some bounds for a linear expression evaluated in all points in the abstract element. More...
 
interval bound (manager &m, const texpr1 &l) const
 Returns some bounds for an arbitrary expression evaluated in all points in the abstract element. More...
 
interval bound (manager &m, const var &v) const
 Returns some bounds for the given variable on all points in the abstract element. More...
 
interval_array to_box (manager &m) const
 Returns a bounding box for the set represented by the abstract element. More...
 
generator1_array to_generator_array (manager &m) const
 Returns a generator representation of (an over-approximation of) the set represented by the abstract element. More...
 
lincons1_array to_lincons_array (manager &m) const
 Returns a linear constraint representation of (an over-approximation of) the set represented by the abstract element. More...
 
tcons1_array to_tcons_array (manager &m) const
 Returns a constraint representation of (an over-approximation of) the set represented by the abstract element. More...
 
C API compatibility
ap_abstract1_t * get_ap_abstract1_t ()
 Returns a pointer to the internal APRON object stored in *this. More...
 
const ap_abstract1_t * get_ap_abstract1_t () const
 Returns a pointer to the internal APRON object stored in *this. More...
 
- Public Member Functions inherited from apron::use_malloc
void * operator new (size_t sz)
 
void * operator new[] (size_t sz)
 
void operator delete (void *p)
 
void operator delete[] (void *p)
 

Protected Member Functions

 abstract1 (ap_abstract1_t x)
 Internal use only. Shallow copy of structure. More...
 

Protected Attributes

ap_abstract1_t a
 Structure managed by APRON. More...
 

Static Protected Attributes

static const abstract1 null
 NULL abstract element, to be used only as default argument in assign and substitute. More...
 

Printing

void print (manager &m, FILE *stream=stdout) const
 Pretty-printing to a C stream. More...
 
void dump (manager &m, FILE *stream=stdout) const
 Raw printing to a C stream (mainly for debug purposes). More...
 

Serialisation

std::string * serialize (manager &m) const
 Serializes an abstract element. More...
 

Predicates

bool is_bottom (manager &m) const
 Whether *this represents the empty set. More...
 
bool is_top (manager &m) const
 Whether *this represents the full space. More...
 
bool is_eq (manager &m, const abstract1 &x) const
 Whether *this and x represent the same set. More...
 
bool is_leq (manager &m, const abstract1 &x) const
 Whether *this is included in x (set-wise). More...
 
bool sat (manager &m, const lincons1 &l) const
 Whether all points in *this satisfy a linear constraint. More...
 
bool sat (manager &m, const tcons1 &l) const
 Whether all points in *this satisfy an arbitrary constraint. More...
 
bool sat (manager &m, const var &v, const interval &i) const
 Whether the component v of all points in *this is included in the given interval. More...
 
bool is_variable_unconstrained (manager &m, const var &v) const
 Whether the points in *this are unbounded in the given variable. More...
 

Meet and unification

abstract1meet (manager &m, const abstract1 &y)
 Replaces *this with the meet of *this and the abstract element y. More...
 
abstract1unify (manager &m, const abstract1 &y)
 Replaces *this with the meet of *this and the abstract element y. More...
 
abstract1meet (manager &m, const lincons1_array &y)
 Adds some linear constraints to *this (modified in-place). More...
 
abstract1meet (manager &m, const tcons1_array &y)
 Adds some arbitrary constraints to *this (modified in-place). More...
 
abstract1operator*= (const abstract1 &y)
 Replaces *this with the meet of *this and the abstract element y. More...
 
abstract1operator*= (const lincons1_array &y)
 Adds some linear constraints to *this (modified in-place). More...
 
abstract1operator*= (const tcons1_array &y)
 Adds some arbitrary constraints to *this (modified in-place). More...
 

Join

abstract1join (manager &m, const abstract1 &y)
 Replaces *this with the join of *this and the abstract element y. More...
 
abstract1add_rays (manager &m, const generator1_array &y)
 Adds some rays to *this (modified in-place). More...
 
abstract1operator+= (const abstract1 &y)
 Replaces *this with the join of *this and the abstract element y. More...
 
abstract1operator+= (const generator1_array &y)
 Adds some rays to *this (modified in-place). More...
 

Assignment

abstract1assign (manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
 In-place assignment of linear expression. More...
 
abstract1assign (manager &m, size_t size, const var v[], const linexpr1 *const l[], const abstract1 &inter=null)
 In-place parallel assignment of linear expressions. More...
 
abstract1assign (manager &m, const std::vector< var > &v, const std::vector< const linexpr1 * > &l, const abstract1 &inter=null)
 In-place parallel assignment of linear expressions. More...
 
abstract1assign (manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
 In-place assignment of arbitrary expression. More...
 
abstract1assign (manager &m, size_t size, const var v[], const texpr1 *const l[], const abstract1 &inter=null)
 In-place parallel assignment of arbitrary expressions. More...
 
abstract1assign (manager &m, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter=null)
 In-place parallel assignment of arbitrary expressions. More...
 

Substitution

abstract1substitute (manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
 In-place substitution (backward assignment) of linear expression. More...
 
abstract1substitute (manager &m, size_t size, const var v[], const linexpr1 *const l[], const abstract1 &inter=null)
 In-place parallel substitution (backward assignment) of linear expressions. More...
 
abstract1substitute (manager &m, const std::vector< var > &v, const std::vector< const linexpr1 * > &l, const abstract1 &inter=null)
 In-place parallel substitution (backward assignment) of linear expressions. More...
 
abstract1substitute (manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
 In-place substitution (backward assignment) of arbitrary expression. More...
 
abstract1substitute (manager &m, size_t size, const var v[], const texpr1 *const l[], const abstract1 &inter=null)
 In-place parallel substitution (backward assignment) of arbitrary expressions. More...
 
abstract1substitute (manager &m, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter=null)
 In-place parallel substitution (backward assignment) of arbitrary expressions. More...
 

Projection, forget

abstract1forget (manager &m, const var &v, bool project=false)
 Forgets about the value of variable v in *this. More...
 
abstract1forget (manager &m, size_t size, const var v[], bool project=false)
 Forgets about the value of variables v[0] to v[size-1] in *this. More...
 
abstract1forget (manager &m, const std::vector< var > &v, bool project=false)
 Forgets about the value of all the variables in v in *this. More...
 

Change of environment

abstract1change_environment (manager &m, const environment &e, bool project=false)
 Modifies the environment of *this. More...
 
abstract1minimize_environment (manager &m)
 Removes from *this the variables that are unconstrained. More...
 
abstract1rename (manager &m, size_t size, const var oldv[], const var newv[])
 Renames oldv[i] into newv[i] in *this. More...
 
abstract1rename (manager &m, const std::vector< var > &oldv, const std::vector< var > &newv)
 Renames oldv[i] into newv[i] in *this. More...
 

Expansion and folding

abstract1expand (manager &m, const var &v, size_t size, const var vv[])
 Duplicates variable v into size copies in *this (modified in-place). More...
 
abstract1expand (manager &m, const var &v, const std::vector< var > &vv)
 Duplicates variable v in *this (modified in-place). More...
 
abstract1fold (manager &m, size_t size, const var v[])
 Folds variables v[0] to v[size-1] in *this (modified in-place). More...
 
abstract1fold (manager &m, const std::vector< var > &v)
 Folds all variables v in *this (modified in-place). More...
 

Closure

abstract1closure (manager &m)
 Replaces *this with its topological closure. More...
 

Detailed Description

Level 1 abstract value (ap_abstract1_t wrapper).

Level 1 version of abstract values. Variable names (var) are used in place of dimensions (ap_dim_t). Internally, an abstract1 wraps together an abstract0 (memory managed) and an environment (holding a reference count).

Constructor & Destructor Documentation

◆ abstract1() [1/10]

abstract1::abstract1 ( ap_abstract1_t  x)
inlineprotected

Internal use only. Shallow copy of structure.

◆ abstract1() [2/10]

abstract1::abstract1 ( manager m,
const environment e,
top  x 
)
inline

Creates an abstract element representing the whole space.

◆ abstract1() [3/10]

abstract1::abstract1 ( manager m,
const environment e,
bottom  x 
)
inline

Creates an abstract element representing the empty set.

◆ abstract1() [4/10]

abstract1::abstract1 ( manager m,
const abstract1 t 
)
inline

Creates a (deep) copy of the abstract element.

◆ abstract1() [5/10]

abstract1::abstract1 ( manager m,
const environment e,
const abstract0 t 
)
inline

Creates a (deep) copy of the abstract element and associates an environment (reference count incremented).

◆ abstract1() [6/10]

abstract1::abstract1 ( manager m,
const environment e,
const var  v[],
const interval_array x 
)
inline

Creates an abstract element from a box.

x[i] is the bound for the variable v[i]. Variables not in v have unconstrained bounds.

◆ abstract1() [7/10]

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

Creates an abstract element from a box.

x[i] is the bound for all the variables in v. Variables not in v have unconstrained bounds.

◆ abstract1() [8/10]

abstract1::abstract1 ( manager m,
const lincons1_array x 
)
inline

Creates an abstract element from a conjunction of linear constraints.

◆ abstract1() [9/10]

abstract1::abstract1 ( manager m,
const tcons1_array x 
)
inline

Creates an abstract element from a conjunction of arbitrary constraints.

◆ abstract1() [10/10]

abstract1::abstract1 ( const abstract1 t)
inline

Creates a (deep) copy of the abstract element.

Implicitly uses the manager used to create *this.

◆ ~abstract1()

abstract1::~abstract1 ( )
inline

Destroys the abstract element.

Implicitly uses the manager used to create *this.

Member Function Documentation

◆ add_rays()

abstract1 & abstract1::add_rays ( manager m,
const generator1_array y 
)
inline

Adds some rays to *this (modified in-place).

  • y can only contain rays and lines, not vertexes.
Returns
a reference to *this.

◆ approximate()

abstract1 & abstract1::approximate ( manager m,
int  algorithm 
)
inline

Simplifies the abstract element, potentially loosing precision.

Returns
a reference to *this.

◆ assign() [1/6]

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

In-place parallel assignment of linear expressions.

*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.

Returns
a reference to *this.
Exceptions
std::invalid_argumentif the vectors have different size.

◆ assign() [2/6]

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

In-place parallel assignment of arbitrary expressions.

*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.

Returns
a reference to *this.
Exceptions
std::invalid_argumentif the vectors have different size.

◆ assign() [3/6]

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

In-place assignment of linear expression.

*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.

Returns
a reference to *this.

◆ assign() [4/6]

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

In-place assignment of arbitrary expression.

*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.

Returns
a reference to *this.

◆ assign() [5/6]

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

In-place parallel assignment of linear expressions.

*this is modified in-place to reflect the effect of assigning l[i] to variable v[i], for i from 0 to size-1. Assignments are performed in parallel. If inter is specified, *this is then intersected with it.

Returns
a reference to *this.

◆ assign() [6/6]

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

In-place parallel assignment of arbitrary expressions.

*this is modified in-place to reflect the effect of assigning l[i] to variable v[i], for i from 0 to size-1. Assignments are performed in parallel. If inter is specified, *this is then intersected with it.

Returns
a reference to *this.

◆ bound() [1/3]

interval abstract1::bound ( manager m,
const linexpr1 l 
) const
inline

Returns some bounds for a linear expression evaluated in all points in the abstract element.

◆ bound() [2/3]

interval abstract1::bound ( manager m,
const texpr1 l 
) const
inline

Returns some bounds for an arbitrary expression evaluated in all points in the abstract element.

◆ bound() [3/3]

interval apron::abstract1::bound ( manager m,
const var v 
) const

Returns some bounds for the given variable on all points in the abstract element.

◆ canonicalize()

abstract1 & abstract1::canonicalize ( manager m)
inline

Puts the abstract element in canonical form (if such a notion exists).

Returns
a reference to *this.

◆ change_environment()

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

Modifies the environment of *this.

  • project whether new variables are initialized to 0 (if true), or undefined (if false).
Returns
a reference to *this.

◆ closure()

abstract1 & abstract1::closure ( manager m)
inline

Replaces *this with its topological closure.

Returns
a reference to *this.

◆ dump()

void abstract1::dump ( manager m,
FILE *  stream = stdout 
) const
inline

Raw printing to a C stream (mainly for debug purposes).

◆ expand() [1/2]

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

Duplicates variable v in *this (modified in-place).

The i-th new variable is named vv[i].

Returns
a reference to *this.

◆ expand() [2/2]

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

Duplicates variable v into size copies in *this (modified in-place).

New variables are named vv[0] to vv[size-1].

Returns
a reference to *this.

◆ fold() [1/2]

abstract1& apron::abstract1::fold ( manager m,
const std::vector< var > &  v 
)

Folds all variables v in *this (modified in-place).

After folding, only v[0] is kept and other variables are removed.

Returns
a reference to *this.

◆ fold() [2/2]

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

Folds variables v[0] to v[size-1] in *this (modified in-place).

After folding, only v[0] is kept and other variables are removed.

Returns
a reference to *this.

◆ forget() [1/3]

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

Forgets about the value of all the variables in v in *this.

  • project whether to reset the variables to 0 (if true), or leave them undefined (if false).
Returns
a reference to *this.

◆ forget() [2/3]

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

Forgets about the value of variable v in *this.

  • project whether to reset the variable to 0 (if true), or leave it undefined (if false).
Returns
a reference to *this.

◆ forget() [3/3]

abstract1& apron::abstract1::forget ( manager m,
size_t  size,
const var  v[],
bool  project = false 
)

Forgets about the value of variables v[0] to v[size-1] in *this.

  • project whether to reset the variables to 0 (if true), or it them undefined (if false).
Returns
a reference to *this.

◆ free()

void abstract1::free ( manager m)
inline

Destroys the abstract element using the given manager.

The abstract element cannot be used after being freed. However, the standard destructor can be safely be called (resulting in a no-op).

◆ get_abstract0() [1/2]

abstract0 & abstract1::get_abstract0 ( )
inline

Returns a (modifiable) reference to the underlying abstract0.

◆ get_abstract0() [2/2]

const abstract0 & abstract1::get_abstract0 ( ) const
inline

Returns a reference to the underlying abstract0.

◆ get_ap_abstract1_t() [1/2]

ap_abstract1_t * abstract1::get_ap_abstract1_t ( )
inline

Returns a pointer to the internal APRON object stored in *this.

◆ get_ap_abstract1_t() [2/2]

const ap_abstract1_t * abstract1::get_ap_abstract1_t ( ) const
inline

Returns a pointer to the internal APRON object stored in *this.

◆ get_environment()

environment abstract1::get_environment ( ) const
inline

Returns the environment of the abstract element (with reference count incremented).

◆ get_manager()

manager abstract1::get_manager ( ) const
inline

Returns the manager the abstract element was created with (with reference count incremented).

◆ is_bottom()

bool abstract1::is_bottom ( manager m) const
inline

Whether *this represents the empty set.

◆ is_eq()

bool abstract1::is_eq ( manager m,
const abstract1 x 
) const
inline

Whether *this and x represent the same set.

◆ is_leq()

bool abstract1::is_leq ( manager m,
const abstract1 x 
) const
inline

Whether *this is included in x (set-wise).

◆ is_top()

bool abstract1::is_top ( manager m) const
inline

Whether *this represents the full space.

◆ is_variable_unconstrained()

bool abstract1::is_variable_unconstrained ( manager m,
const var v 
) const
inline

Whether the points in *this are unbounded in the given variable.

◆ join()

abstract1 & abstract1::join ( manager m,
const abstract1 y 
)
inline

Replaces *this with the join of *this and the abstract element y.

Returns
a reference to *this.

◆ meet() [1/3]

abstract1 & abstract1::meet ( manager m,
const abstract1 y 
)
inline

Replaces *this with the meet of *this and the abstract element y.

Returns
a reference to *this.

◆ meet() [2/3]

abstract1 & abstract1::meet ( manager m,
const lincons1_array y 
)
inline

Adds some linear constraints to *this (modified in-place).

Returns
a reference to *this.

◆ meet() [3/3]

abstract1 & abstract1::meet ( manager m,
const tcons1_array y 
)
inline

Adds some arbitrary constraints to *this (modified in-place).

Returns
a reference to *this.

◆ minimize()

abstract1 & abstract1::minimize ( manager m)
inline

Minimizes the size of the representation, to save memory.

Returns
a reference to *this.

◆ minimize_environment()

abstract1 & abstract1::minimize_environment ( manager m)
inline

Removes from *this the variables that are unconstrained.

Returns
a reference to *this.

◆ operator*=() [1/3]

abstract1 & abstract1::operator*= ( const abstract1 y)
inline

Replaces *this with the meet of *this and the abstract element y.

Implicitly uses the manager used to create *this.

Returns
a reference to *this.

◆ operator*=() [2/3]

abstract1 & abstract1::operator*= ( const lincons1_array y)
inline

Adds some linear constraints to *this (modified in-place).

Implicitly uses the manager used to create *this.

Returns
a reference to *this.

◆ operator*=() [3/3]

abstract1 & abstract1::operator*= ( const tcons1_array y)
inline

Adds some arbitrary constraints to *this (modified in-place).

Implicitly uses the manager used to create *this.

Returns
a reference to *this.

◆ operator+=() [1/2]

abstract1 & abstract1::operator+= ( const abstract1 y)
inline

Replaces *this with the join of *this and the abstract element y.

Implicitly uses the manager used to create *this.

Returns
a reference to *this.

◆ operator+=() [2/2]

abstract1 & abstract1::operator+= ( const generator1_array y)
inline

Adds some rays to *this (modified in-place).

Implicitly uses the manager used to create *this.

  • y can only contain rays and lines, not vertexes.
Returns
a reference to *this.

◆ operator=() [1/6]

abstract1 & abstract1::operator= ( bottom  t)
inline

Assigns the empty set to *this.

Implicitly uses the manager used to create *this. Does not change the environment.

◆ operator=() [2/6]

abstract1 & abstract1::operator= ( const abstract1 t)
inline

Assigns a copy of t to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [3/6]

abstract1 & abstract1::operator= ( const interval_array x)
inline

Assigns a box to *this.

Implicitly uses the manager used to create *this. Does not change the environment.

Exceptions
std::invalid_argumentif the array has insufficient size.

◆ operator=() [4/6]

abstract1 & abstract1::operator= ( const lincons1_array x)
inline

Assigns a conjunction of linear constraints to *this.

Implicitly uses the manager used to create *this. Does not change the environment.

◆ operator=() [5/6]

abstract1 & abstract1::operator= ( const tcons1_array x)
inline

Assigns a conjunction of arbitrary constraints to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [6/6]

abstract1 & abstract1::operator= ( top  t)
inline

Assigns the full space to *this.

Implicitly uses the manager used to create *this.

◆ print()

void abstract1::print ( manager m,
FILE *  stream = stdout 
) const
inline

Pretty-printing to a C stream.

◆ rename() [1/2]

abstract1 & abstract1::rename ( manager m,
const std::vector< var > &  oldv,
const std::vector< var > &  newv 
)
inline

Renames oldv[i] into newv[i] in *this.

Returns
a reference to *this.

◆ rename() [2/2]

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

Renames oldv[i] into newv[i] in *this.

Returns
a reference to *this.

◆ sat() [1/3]

bool abstract1::sat ( manager m,
const lincons1 l 
) const
inline

Whether all points in *this satisfy a linear constraint.

◆ sat() [2/3]

bool abstract1::sat ( manager m,
const tcons1 l 
) const
inline

Whether all points in *this satisfy an arbitrary constraint.

◆ sat() [3/3]

bool abstract1::sat ( manager m,
const var v,
const interval i 
) const
inline

Whether the component v of all points in *this is included in the given interval.

◆ serialize()

std::string * abstract1::serialize ( manager m) const
inline

Serializes an abstract element.

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.

Returns
a newly allocated string that the caller should delete it after use.

◆ set() [1/10]

abstract1 & abstract1::set ( manager m,
bottom  t 
)
inline

Replaces *this with the empty set.

Does not change the environment.

Returns
a reference to *this.

◆ set() [2/10]

abstract1 & abstract1::set ( manager m,
const abstract1 x 
)
inline

Replaces *this with a copy of x.

Returns
a reference to *this.

◆ set() [3/10]

abstract1 & abstract1::set ( manager m,
const environment e,
bottom  t 
)
inline

Replaces *this with the empty set.

Returns
a reference to *this.

◆ set() [4/10]

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

Replaces *this with a box.

Returns
a reference to *this.

◆ set() [5/10]

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

Replaces *this with a box.

Returns
a reference to *this.

◆ set() [6/10]

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

Replaces *this with the full space.

Returns
a reference to *this.

◆ set() [7/10]

abstract1 & abstract1::set ( manager m,
const interval_array x 
)
inline

Replaces *this with a box.

Does not change the environment.

Returns
a reference to *this.

◆ set() [8/10]

abstract1 & abstract1::set ( manager m,
const lincons1_array x 
)
inline

Replaces *this with a conjunction of linear constraints.

Returns
a reference to *this.

◆ set() [9/10]

abstract1 & abstract1::set ( manager m,
const tcons1_array x 
)
inline

Replaces *this with a conjunction of arbitrary constraints.

Returns
a reference to *this.

◆ set() [10/10]

abstract1 & abstract1::set ( manager m,
top  t 
)
inline

Replaces *this with the full space.

Does not change the environment.

Returns
a reference to *this.

◆ size()

size_t abstract1::size ( manager m) const
inline

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 max_object_size field of the ap_funopt_t structure.

◆ substitute() [1/6]

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

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.

Returns
a reference to *this.
Exceptions
std::invalid_argumentif the vectors have different size.

◆ substitute() [2/6]

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

In-place parallel substitution (backward assignment) of arbitrary 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.

Returns
a reference to *this.
Exceptions
std::invalid_argumentif the vectors have different size.

◆ substitute() [3/6]

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

In-place substitution (backward assignment) of linear expression.

*this is modified in-place to reflect the effect of substituting l to variable v. If inter is specified, *this is then intersected with it.

Returns
a reference to *this.

◆ substitute() [4/6]

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

In-place substitution (backward assignment) of arbitrary expression.

*this is modified in-place to reflect the effect of substituting l to variable v. If inter is specified, *this is then intersected with it.

Returns
a reference to *this.

◆ substitute() [5/6]

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

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], for i from 0 to size-1. Substitutions are performed in parallel. If inter is specified, *this is then intersected with it.

Returns
a reference to *this.

◆ substitute() [6/6]

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

In-place parallel substitution (backward assignment) of arbitrary expressions.

*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.

Returns
a reference to *this.

◆ to_box()

interval_array abstract1::to_box ( manager m) const
inline

Returns a bounding box for the set represented by the abstract element.

◆ to_generator_array()

generator1_array abstract1::to_generator_array ( manager m) const
inline

Returns a generator representation of (an over-approximation of) the set represented by the abstract element.

◆ to_lincons_array()

lincons1_array abstract1::to_lincons_array ( manager m) const
inline

Returns a linear constraint representation of (an over-approximation of) the set represented by the abstract element.

◆ to_tcons_array()

tcons1_array abstract1::to_tcons_array ( manager m) const
inline

Returns a constraint representation of (an over-approximation of) the set represented by the abstract element.

◆ unify()

abstract1 & abstract1::unify ( manager m,
const abstract1 y 
)
inline

Replaces *this with the meet of *this and the abstract element y.

*this and y can have different environment. They are first embedded into the least common environment before the meet is computed.

Returns
a reference to *this.

Member Data Documentation

◆ a

ap_abstract1_t apron::abstract1::a
protected

Structure managed by APRON.

◆ null

const abstract1 apron::abstract1::null
staticprotected

NULL abstract element, to be used only as default argument in assign and substitute.


The documentation for this class was generated from the following files: