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. 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
abstract1 &	operator= (const abstract1 &t)
	Assigns a copy of t to *this. More...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

abstract1 &	approximate (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...

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

const abstract0 &	get_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...

Friends
Widening
abstract1 &	widening (manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
	Stores in dst the result of x widened with y. More...

abstract1 &	widening (manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y, const lincons1_array &l)
	Stores in dst the result of x widened with y, using some widening thresholds. More...

Printing
void	printdiff (manager &m, const abstract1 &x, const abstract1 &y, FILE *stream)
	Pretty-printing the difference between x and y to a C stream. More...

std::ostream &	operator<< (std::ostream &os, const abstract1 &s)
	Prints in constraint form. More...

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

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

Predicates
bool	operator== (const abstract1 &x, const abstract1 &y)
	Whether x and y represent the same set. More...

bool	operator!= (const abstract1 &x, const abstract1 &y)
	Whether x and y represent different sets. More...

bool	operator<= (const abstract1 &x, const abstract1 &y)
	Whether x is included within y (set-wise). More...

bool	operator>= (const abstract1 &x, const abstract1 &y)
	Whether x contains y (set-wise). More...

bool	operator> (const abstract1 &x, const abstract1 &y)
	Whether x strictly contains y (set-wise). More...

bool	operator< (const abstract1 &x, const abstract1 &y)
	Whether x is strictly included within y (set-wise). More...

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
abstract1 &	meet (manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
	Replaces dst with the meet of x and y. More...

abstract1 &	unify (manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
	Replaces dst with the meet of x and y. More...

abstract1 &	meet (manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
	Replaces dst with the meet of all abstract elements in x. More...

abstract1 &	meet (manager &m, abstract1 &dst, size_t size, const abstract1 *const x[])
	Replaces dst with the meet of all size abstract elements in x. More...

abstract1 &	meet (manager &m, abstract1 &dst, const abstract1 &x, const lincons1_array &y)
	Replaces dst with the meet of x and some linear constraints. More...

abstract1 &	meet (manager &m, abstract1 &dst, const abstract1 &x, const tcons1_array &y)
	Replaces dst with the meet of x and some arbitrary constraints. More...

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

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

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

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

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

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

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

Join
abstract1 &	join (manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
	Replaces dst with the join of x and y. More...

abstract1 &	join (manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
	Replaces dst with the join of all abstract elements in x. More...

abstract1 &	join (manager &m, abstract1 &dst, size_t size, const abstract1 *const x[])
	Replaces dst with the join of all size abstract elements in x. More...

abstract1 &	add_rays (manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
	Replaces dst with x with some rays added. More...

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

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

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

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

Assignment
abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter)
	Assignment of linear expression. More...

abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[], const linexpr1 *const l[], const abstract1 &inter)
	Parallel assignment of linear expressions. More...

abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v, const std::vector< const linexpr1 * > &l, const abstract1 &inter)
	Parallel assignment of linear expressions. More...

abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, const var &v, const texpr1 &l, const abstract1 &inter)
	Assignment of arbitrary expression. More...

abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[], const texpr1 *const l[], const abstract1 &inter)
	Parallel assignment of arbitrary expressions. More...

abstract1 &	assign (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter)
	Parallel assignment of arbitrary expressions. More...

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

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

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

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

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

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

Substitution
abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter)
	Substitution (backward assignment) of linear expression. More...

abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[], const linexpr1 *const l[], const abstract1 &inter)
	Parallel substitution (backward assignment) of linear expressions. More...

abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v, const std::vector< const linexpr1 * > &l, const abstract1 &inter)
	Parallel substitution (backward assignment) of linear expressions. More...

abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, const var &v, const texpr1 &l, const abstract1 &inter)
	Substitution (backward assignment) of arbitrary expression. More...

abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[], const texpr1 *const l[], const abstract1 &inter)
	Parallel substitution (backward assignment) of arbitrary expressions. More...

abstract1 &	substitute (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter)
	Parallel substitution (backward assignment) of arbitrary expressions. More...

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

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

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

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

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

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

Projection, forget
abstract1 &	forget (manager &m, abstract1 &dst, const abstract1 &src, const var &v, bool project)
	Stores in dst the result of forgetting the value of variable v in src. More...

abstract1 &	forget (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[], bool project)
	Stores in dst the result of forgetting the value of variables v[0] to v[size-1] in src. More...

abstract1 &	forget (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v, bool project)
	Stores in dst the result of forgetting the value of all the variables in v in src. More...

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

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

abstract1 &	forget (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
abstract1 &	change_environment (manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project)
	Replaces dst with src and changes its environment. More...

abstract1 &	minimize_environment (manager &m, abstract1 &dst, const abstract1 &src)
	Replaces dst with src and removes the variables that are unconstrained. More...

abstract1 &	rename (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var oldv[], const var newv[])
	Replaces dst with src and renames oldv[i] into newv[i]. More...

abstract1 &	rename (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &oldv, const std::vector< var > &newv)
	Replaces dst with src and renames oldv[i] into newv[i]. More...

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

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

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

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

Expansion and folding
abstract1 &	expand (manager &m, abstract1 &dst, const abstract1 &src, const var &v, size_t size, const var vv[])
	Replaces dst with a copy of src and duplicates variable v into size copies. More...

abstract1 &	expand (manager &m, abstract1 &dst, const abstract1 &src, const var &v, const std::vector< var > &vv)
	Replaces dst with a copy of src and duplicates variable v. More...

abstract1 &	fold (manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var v[])
	Replaces dst with a copy of src and folds variables v[0] to v[size-1]. More...

abstract1 &	fold (manager &m, abstract1 &dst, const abstract1 &src, const std::vector< var > &v)
	Replaces dst with a copy of src and folds all variables in v. More...

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

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

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

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

Closure
abstract1 &	closure (manager &m, abstract1 &dst, const abstract1 &src)
	Stores in dst the topological closure of src. More...

abstract1 &	closure (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 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() [2/6]

abstract1 & apron::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() [3/6]

abstract1 & apron::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() [4/6]

abstract1 & apron::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 & apron::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.

◆ assign() [6/6]

abstract1 & apron::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.

◆ 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 & apron::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,
		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.

◆ expand() [2/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.

◆ fold() [1/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.

◆ fold() [2/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.

◆ forget() [1/3]

abstract1 & apron::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() [2/3]

abstract1 & apron::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.

◆ forget() [3/3]

abstract1 & apron::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.

◆ 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= ( const abstract1 & t )

inline

Assigns a copy of t to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [2/6]

abstract1 & abstract1::operator= ( top t )

inline

Assigns the full space to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [3/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=() [4/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=() [5/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=() [6/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.

◆ 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,
		size_t	size,
		const var	oldv[],
		const var	newv[]
	)

inline

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

Returns: a reference to *this.

◆ rename() [2/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.

◆ 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,
		const abstract1 &	x
	)

inline

Replaces *this with a copy of x.

Returns: a reference to *this.

◆ set() [2/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.

◆ set() [3/10]

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

inline

Replaces *this with the full space.

Returns: a reference to *this.

◆ set() [4/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() [5/10]

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

inline

Replaces *this with the empty set.

Returns: a reference to *this.

◆ set() [6/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() [7/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() [8/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() [9/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() [10/10]

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

inline

Replaces *this with a conjunction of arbitrary constraints.

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 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() [2/6]

abstract1 & apron::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() [3/6]

abstract1 & apron::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() [4/6]

abstract1 & apron::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 & apron::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.

◆ substitute() [6/6]

abstract1 & apron::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.

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

Friends And Related Function Documentation

◆ add_rays

abstract1& add_rays	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	x,
		const generator1_array &	y
	)

friend

Replaces dst with x with some rays added.

y can only contain rays and lines, not vertexes.

Returns: a reference to *this.

◆ assign [1/6]

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

friend

Assignment of linear expression.

dst is replaced with the effect of assigning l to variable v in src. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ assign [2/6]

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

friend

Parallel assignment of linear expressions.

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

Returns: a reference to dst.

◆ assign [3/6]

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

friend

Parallel assignment of linear expressions.

dst is replaced with the effect of assigning l[i] to variable v[i] in src. Assignments are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

Exceptions

std::invalid_argument if the vectors have different size.

◆ assign [4/6]

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

friend

Assignment of arbitrary expression.

dst is replaced with the effect of assigning l to variable v in src. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ assign [5/6]

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

friend

Parallel assignment of arbitrary expressions.

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

Returns: a reference to dst.

◆ assign [6/6]

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

friend

Parallel assignment of arbitrary expressions.

dst is replaced with the effect of assigning l[i] to variable v[i] in src. Assignments are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

Exceptions

std::invalid_argument if the vectors have different size.

◆ change_environment

abstract1& change_environment	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	src,
		const environment &	e,
		bool	project = `false`
	)

friend

Replaces dst with src and changes its environment.

project whether new variables are initialized to 0 (if true), or undefined (if false).

Returns: a reference to dst.

◆ closure

abstract1& closure	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	src
	)

friend

Stores in dst the topological closure of src.

Returns: a reference to dst.

◆ deserialize

abstract1& deserialize	(	manager &	m,
		abstract1 &	dst,
		const std::string &	s,
		size_t *	eaten = `NULL`
	)

friend

Reconstruct an abstract element form a serialized byte-stream and put it into dst.

The managers used to serialized and deserialize need not be the same, but they must have been created using the same library and with the same arguments.

eaten, if not NULL, will be set to the actual number of bytes consumed from the string.
Returns
a reference to dst.

◆ expand [1/2]

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

friend

Replaces dst with a copy of src and duplicates variable v into size copies.

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

Returns: a reference to dst.

◆ expand [2/2]

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

friend

Replaces dst with a copy of src and duplicates variable v.

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

Returns: a reference to dst.

◆ fold [1/2]

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

friend

Replaces dst with a copy of src and folds variables v[0] to v[size-1].

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

Returns: a reference to dst.

◆ fold [2/2]

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

friend

Replaces dst with a copy of src and folds all variables in v.

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

Returns: a reference to dst.

◆ forget [1/3]

abstract1& forget	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	src,
		const var &	v,
		bool	project = `false`
	)

friend

Stores in dst the result of forgetting the value of variable v in src.

project if true, resets the variable to 0 (if true).

Returns: a reference to dst.

◆ forget [2/3]

abstract1& forget	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	src,
		size_t	size,
		const var	v[],
		bool	project = `false`
	)

friend

Stores in dst the result of forgetting the value of variables v[0] to v[size-1] in src.

project whether to reset the variables to 0 (if true), or leave them undefined (if false).

Returns: a reference to dst.

◆ forget [3/3]

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

friend

Stores in dst the result of forgetting the value of all the variables in v in src.

project whether to reset the variables to 0 (if true), or leave them undefined (if false).

Returns: a reference to dst.

◆ join [1/3]

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

friend

Replaces dst with the join of x and y.

Returns: a reference to dst.

◆ join [2/3]

abstract1& join	(	manager &	m,
		abstract1 &	dst,
		const std::vector< const abstract1 * > &	x
	)

friend

Replaces dst with the join of all abstract elements in x.

Returns: a reference to dst.

◆ join [3/3]

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

friend

Replaces dst with the join of all size abstract elements in x.

Returns: a reference to dst.

◆ meet [1/5]

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

friend

Replaces dst with the meet of x and y.

Returns: a reference to dst.

◆ meet [2/5]

abstract1& meet	(	manager &	m,
		abstract1 &	dst,
		const std::vector< const abstract1 * > &	x
	)

friend

Replaces dst with the meet of all abstract elements in x.

Returns: a reference to dst.

◆ meet [3/5]

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

friend

Replaces dst with the meet of all size abstract elements in x.

Returns: a reference to dst.

◆ meet [4/5]

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

friend

Replaces dst with the meet of x and some linear constraints.

Returns: a reference to dst.

◆ meet [5/5]

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

friend

Replaces dst with the meet of x and some arbitrary constraints.

Returns: a reference to dst.

◆ minimize_environment

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

friend

Replaces dst with src and removes the variables that are unconstrained.

Returns: a reference to dst.

◆ operator!=

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

friend

Whether x and y represent different sets.

The manager for the left argument is used implicitly.

◆ operator<

bool operator<	(	const abstract1 &	x,
		const abstract1 &	y
	)

friend

Whether x is strictly included within y (set-wise).

The manager for the left argument is used implicitly.

◆ operator<<

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

friend

Prints in constraint form.

◆ operator<=

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

friend

Whether x is included within y (set-wise).

The manager for the left argument is used implicitly.

◆ operator==

bool operator==	(	const abstract1 &	x,
		const abstract1 &	y
	)

friend

Whether x and y represent the same set.

The manager for the left argument is used implicitly.

◆ operator>

bool operator>	(	const abstract1 &	x,
		const abstract1 &	y
	)

friend

Whether x strictly contains y (set-wise).

The manager for the left argument is used implicitly.

◆ operator>=

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

friend

Whether x contains y (set-wise).

The manager for the left argument is used implicitly.

◆ printdiff

void printdiff	(	manager &	m,
		const abstract1 &	x,
		const abstract1 &	y,
		FILE *	stream = `stdout`
	)

friend

Pretty-printing the difference between x and y to a C stream.

◆ rename [1/2]

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

friend

Replaces dst with src and renames oldv[i] into newv[i].

Returns: a reference to dst.

◆ rename [2/2]

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

friend

Replaces dst with src and renames oldv[i] into newv[i].

Returns: a reference to dst.

◆ substitute [1/6]

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

friend

Substitution (backward assignment) of linear expression.

dst is replaced with the effect of substituting l to variable v in src. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ substitute [2/6]

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

friend

Parallel substitution (backward assignment) of linear expressions.

dst is replaced with the effect of substituting l[i] to variable v[i] in src, for i from 0 to size-1. Substitutions are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ substitute [3/6]

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

friend

Parallel substitution (backward assignment) of linear expressions.

dst is replaced with the effect of substituting l[i] to variable v[i] in src. Substitutions are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

Exceptions

std::invalid_argument if the vectors have different size.

◆ substitute [4/6]

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

friend

Substitution (backward assignment) of arbitrary expression.

dst is replaced with the effect of substituting l to variable v in src. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ substitute [5/6]

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

friend

Parallel substitution (backward assignment) of arbitrary expressions.

dst is replaced with the effect of substituting l[i] to variable v[i] in src, for i from 0 to size-1. Substitutions are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

◆ substitute [6/6]

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

friend

Parallel substitution (backward assignment) of arbitrary expressions.

dst is replaced with the effect of substituting l[i] to variable v[i] in src. Substitutions are performed in parallel. If inter is specified, dst is then intersected with it.

Returns: a reference to dst.

Exceptions

std::invalid_argument if the vectors have different size.

◆ unify

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

friend

Replaces dst with the meet of x and y.

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

Returns: a reference to dst.

◆ widening [1/2]

abstract1& widening	(	manager &	m,
		abstract1 &	dst,
		const abstract1 &	x,
		const abstract1 &	y
	)

friend

Stores in dst the result of x widened with y.

Warning: y must be a superset of x.

Returns: a reference to dst.

◆ widening [2/2]

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

friend

Stores in dst the result of x widened with y, using some widening thresholds.

Warning: y must be a superset of x.

Returns: a reference to dst.

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

Friends

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]