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

#include <apxx_abstract1.hh>

Public Member Functions
Constructors
	abstract1 (manager &m, const environment &e, top x)
	Creates an abstract element representing the whole space.

	abstract1 (manager &m, const environment &e, bottom x)
	Creates an abstract element representing the empty set.

	abstract1 (manager &m, const abstract1 &t)
	Creates a (deep) copy of the abstract element.

	abstract1 (manager &m, const environment &e, const abstract0 &t)
	Creates a (deep) copy of the abstract element and associates an environment (reference count incremented).

	abstract1 (manager &m, const environment &e, const var v[], const interval_array &x)
	Creates an abstract element from a box.

	abstract1 (manager &m, const environment &e, const std::vector< var > &v, const interval_array &x)
	Creates an abstract element from a box.

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

	abstract1 (manager &m, const tcons1_array &x)
	Creates an abstract element from a conjunction of arbitrary constraints.

	abstract1 (const abstract1 &t)
	Creates a (deep) copy of the abstract element.

Destructors
	~abstract1 ()
	Destroys the abstract element.

void	free (manager &m)
	Destroys the abstract element using the given manager.

Copies and conversions to abstract elements
abstract1 &	operator= (const abstract1 &t)
	Assigns a copy of t to *this.

abstract1 &	operator= (top t)
	Assigns the full space to *this.

abstract1 &	operator= (bottom t)
	Assigns the empty set to *this.

abstract1 &	operator= (const interval_array &x)
	Assigns a box to *this.

abstract1 &	operator= (const lincons1_array &x)
	Assigns a conjunction of linear constraints to *this.

abstract1 &	operator= (const tcons1_array &x)
	Assigns a conjunction of arbitrary constraints to *this.

abstract1 &	set (manager &m, const abstract1 &x)
	Replaces *this with a copy of x.

abstract1 &	set (manager &m, top t)
	Replaces *this with the full space.

abstract1 &	set (manager &m, const environment &e, top t)
	Replaces *this with the full space.

abstract1 &	set (manager &m, bottom t)
	Replaces *this with the empty set.

abstract1 &	set (manager &m, const environment &e, bottom t)
	Replaces *this with the empty set.

abstract1 &	set (manager &m, const interval_array &x)
	Replaces *this with a box.

abstract1 &	set (manager &m, const environment &e, const var v[], const interval_array &x)
	Replaces *this with a box.

abstract1 &	set (manager &m, const environment &e, const std::vector< var > &v, const interval_array &x)
	Replaces *this with a box.

abstract1 &	set (manager &m, const lincons1_array &x)
	Replaces *this with a conjunction of linear constraints.

abstract1 &	set (manager &m, const tcons1_array &x)
	Replaces *this with a conjunction of arbitrary constraints.

Control of internal representation
abstract1 &	minimize (manager &m)
	Minimizes the size of the representation, to save memory.

abstract1 &	canonicalize (manager &m)
	Puts the abstract element in canonical form (if such a notion exists).

abstract1 &	approximate (manager &m, int algorithm)
	Simplifies the abstract element, potentially loosing precision.

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

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

abstract0 &	get_abstract0 ()
	Returns a (modifiable) reference to the underlying abstract0.

const abstract0 &	get_abstract0 () const
	Returns a reference to the underlying abstract0.

size_t	size (manager &m) const
	Returns the (abstract) size of the abstract element.

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.

interval	bound (manager &m, const texpr1 &l) const
	Returns some bounds for an arbitrary expression evaluated in all points in the abstract element.

interval	bound (manager &m, const var &v) const
	Returns some bounds for the given variable on all points in the abstract element.

interval_array	to_box (manager &m) const
	Returns a bounding box for the set represented by the abstract element.

generator1_array	to_generator_array (manager &m) const
	Returns a generator representation of (an over-approximation of) the set represented by the abstract element.

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.

tcons1_array	to_tcons_array (manager &m) const
	Returns a constraint representation of (an over-approximation of) the set represented by the abstract element.

C API compatibility
ap_abstract1_t *	get_ap_abstract1_t ()
	Returns a pointer to the internal APRON object stored in *this.

const ap_abstract1_t *	get_ap_abstract1_t () const
	Returns a pointer to the internal APRON object stored in *this.

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.

Protected Attributes
ap_abstract1_t	a
	Structure managed by APRON.

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

Printing
void	print (manager &m, FILE *stream=stdout) const
	Pretty-printing to a C stream.

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

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

Predicates
bool	is_bottom (manager &m) const
	Whether *this represents the empty set.

bool	is_top (manager &m) const
	Whether *this represents the full space.

bool	is_eq (manager &m, const abstract1 &x) const
	Whether *this and x represent the same set.

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

bool	sat (manager &m, const lincons1 &l) const
	Whether all points in *this satisfy a linear constraint.

bool	sat (manager &m, const tcons1 &l) const
	Whether all points in *this satisfy an arbitrary constraint.

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.

bool	is_variable_unconstrained (manager &m, const var &v) const
	Whether the points in *this are unbounded in the given variable.

Meet and unification
abstract1 &	meet (manager &m, const abstract1 &y)
	Replaces this with the meet of this and the abstract element y.

abstract1 &	unify (manager &m, const abstract1 &y)
	Replaces this with the meet of this and the abstract element y.

abstract1 &	meet (manager &m, const lincons1_array &y)
	Adds some linear constraints to *this (modified in-place).

abstract1 &	meet (manager &m, const tcons1_array &y)
	Adds some arbitrary constraints to *this (modified in-place).

abstract1 &	operator*= (const abstract1 &y)
	Replaces this with the meet of this and the abstract element y.

abstract1 &	operator*= (const lincons1_array &y)
	Adds some linear constraints to *this (modified in-place).

abstract1 &	operator*= (const tcons1_array &y)
	Adds some arbitrary constraints to *this (modified in-place).

Join
abstract1 &	join (manager &m, const abstract1 &y)
	Replaces this with the join of this and the abstract element y.

abstract1 &	add_rays (manager &m, const generator1_array &y)
	Adds some rays to *this (modified in-place).

abstract1 &	operator+= (const abstract1 &y)
	Replaces this with the join of this and the abstract element y.

abstract1 &	operator+= (const generator1_array &y)
	Adds some rays to *this (modified in-place).

Assignment
abstract1 &	assign (manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
	In-place assignment of linear expression.

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.

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.

abstract1 &	assign (manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
	In-place assignment of arbitrary expression.

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.

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.

Substitution
abstract1 &	substitute (manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
	In-place substitution (backward assignment) of linear expression.

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.

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.

abstract1 &	substitute (manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
	In-place substitution (backward assignment) of arbitrary expression.

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.

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.

Projection, forget
abstract1 &	forget (manager &m, const var &v, bool project=false)
	Forgets about the value of variable v in *this.

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.

abstract1 &	forget (manager &m, const std::vector< var > &v, bool project=false)
	Forgets about the value of all the variables in v in *this.

Change of environment
abstract1 &	change_environment (manager &m, const environment &e, bool project=false)
	Modifies the environment of *this.

abstract1 &	minimize_environment (manager &m)
	Removes from *this the variables that are unconstrained.

abstract1 &	rename (manager &m, size_t size, const var oldv[], const var newv[])
	Renames oldv[i] into newv[i] in *this.

abstract1 &	rename (manager &m, const std::vector< var > &oldv, const std::vector< var > &newv)
	Renames oldv[i] into newv[i] in *this.

Expansion and folding
abstract1 &	expand (manager &m, const var &v, size_t size, const var vv[])
	Duplicates variable v into size copies in *this (modified in-place).

abstract1 &	expand (manager &m, const var &v, const std::vector< var > &vv)
	Duplicates variable v in *this (modified in-place).

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

abstract1 &	fold (manager &m, const std::vector< var > &v)
	Folds all variables v in *this (modified in-place).

Closure
abstract1 &	closure (manager &m)
	Replaces *this with its topological closure.

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 & abstract1::assign	(	manager &	m,
		const std::vector< var > &	v,
		const std::vector< const linexpr1 * > &	l,
		const abstract1 &	inter = null )

inline

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_argument if the vectors have different size.

◆ assign() [2/6]

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

inline

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_argument if the vectors have different size.

◆ assign() [3/6]

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

inline

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 & abstract1::assign	(	manager &	m,
		const var &	v,
		const texpr1 &	l,
		const abstract1 &	inter = null )

inline

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 & abstract1::assign	(	manager &	m,
		size_t	size,
		const var	v[],
		const linexpr1 *const	l[],
		const abstract1 &	inter = null )

inline

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 & abstract1::assign	(	manager &	m,
		size_t	size,
		const var	v[],
		const texpr1 *const	l[],
		const abstract1 &	inter = null )

inline

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

inline

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 & abstract1::change_environment	(	manager &	m,
		const environment &	e,
		bool	project = false )

inline

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 )

inline

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

inline

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 & abstract1::forget	(	manager &	m,
		const std::vector< var > &	v,
		bool	project = false )

inline

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 & abstract1::forget	(	manager &	m,
		const var &	v,
		bool	project = false )

inline

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 & abstract1::forget	(	manager &	m,
		size_t	size,
		const var	v[],
		bool	project = false )

inline

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_argument if 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 & abstract1::substitute	(	manager &	m,
		const std::vector< var > &	v,
		const std::vector< const linexpr1 * > &	l,
		const abstract1 &	inter = null )

inline

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_argument if the vectors have different size.

◆ substitute() [2/6]

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

inline

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_argument if the vectors have different size.

◆ substitute() [3/6]

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

inline

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 & abstract1::substitute	(	manager &	m,
		const var &	v,
		const texpr1 &	l,
		const abstract1 &	inter = null )

inline

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

inline

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 & abstract1::substitute	(	manager &	m,
		size_t	size,
		const var	v[],
		const texpr1 *const	l[],
		const abstract1 &	inter = null )

inline

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:

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

Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Printing

Serialisation

Predicates

Meet and unification

Join

Assignment

Substitution

Projection, forget

Change of environment

Expansion and folding

Closure

Detailed Description

Constructor & Destructor Documentation

◆ abstract1() [1/10]

◆ abstract1() [2/10]

◆ abstract1() [3/10]

◆ abstract1() [4/10]

◆ abstract1() [5/10]

◆ abstract1() [6/10]

◆ abstract1() [7/10]

◆ abstract1() [8/10]

◆ abstract1() [9/10]

◆ abstract1() [10/10]

◆ ~abstract1()

Member Function Documentation

◆ add_rays()

◆ approximate()

◆ assign() [1/6]

◆ assign() [2/6]

◆ assign() [3/6]

◆ assign() [4/6]

◆ assign() [5/6]

◆ assign() [6/6]

◆ bound() [1/3]

◆ bound() [2/3]

◆ bound() [3/3]

◆ canonicalize()

◆ change_environment()

◆ closure()

◆ dump()

◆ expand() [1/2]

◆ expand() [2/2]

◆ fold() [1/2]

◆ fold() [2/2]

◆ forget() [1/3]

◆ forget() [2/3]

◆ forget() [3/3]

◆ free()

◆ get_abstract0() [1/2]

◆ get_abstract0() [2/2]

◆ get_ap_abstract1_t() [1/2]

◆ get_ap_abstract1_t() [2/2]

◆ get_environment()

◆ get_manager()

◆ is_bottom()

◆ is_eq()

◆ is_leq()

◆ is_top()

◆ is_variable_unconstrained()

◆ join()

◆ meet() [1/3]

◆ meet() [2/3]

◆ meet() [3/3]

◆ minimize()

◆ minimize_environment()

◆ operator*=() [1/3]

◆ operator*=() [2/3]

◆ operator*=() [3/3]

◆ operator+=() [1/2]

◆ operator+=() [2/2]

◆ operator=() [1/6]

◆ operator=() [2/6]

◆ operator=() [3/6]

◆ operator=() [4/6]

◆ operator=() [5/6]

◆ operator=() [6/6]