Level 0 abstract value (ap_abstract0_t* wrapper). More...

#include <apxx_abstract0.hh>

Public Member Functions
Constructors
	abstract0 (manager &m, size_t intdim, size_t realdim, top x)
	Creates an abstract element representing the whole space. More...

	abstract0 (manager &m, size_t intdim, size_t realdim, bottom x)
	Creates an abstract element representing the empty set. More...

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

	abstract0 (manager &m, size_t intdim, size_t realdim, const interval_array &x)
	Creates an abstract element from a box. More...

	abstract0 (manager &m, size_t intdim, size_t realdim, const lincons0_array &x)
	Creates an abstract element from a conjunction of linear constraints. More...

	abstract0 (manager &m, size_t intdim, size_t realdim, const tcons0_array &x)
	Creates an abstract element from a conjunction of arbitrary constraints. More...

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

Destructors
	~abstract0 ()
	Destroys the abstract element. More...

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

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

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

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

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

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

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

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

abstract0 &	set (manager &m, top t, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
	Replaces *this with the full space. More...

abstract0 &	set (manager &m, bottom t, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
	Replaces *this with the empty set. More...

abstract0 &	set (manager &m, const interval_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
	Replaces *this with a box. More...

abstract0 &	set (manager &m, const lincons0_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
	Replaces *this with a conjunction of linear constraints. More...

abstract0 &	set (manager &m, const tcons0_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
	Replaces *this with a conjunction of arbitrary constraints. More...

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

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

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

ap_dimension_t	get_dimension (manager &m) const
	Returns the number of integer and real dimensions in the abstract element. More...

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

Property extraction
interval	bound (manager &m, const linexpr0 &l) const
	Returns some bounds for a linear expression evaluated in all points in the abstract element. More...

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

interval	bound (manager &m, ap_dim_t d) const
	Returns some bounds for the given coordinate 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...

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

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

tcons0_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_abstract0_t *	get_ap_abstract0_t ()
	Returns a pointer to the internal APRON object stored in *this. More...

const ap_abstract0_t *	get_ap_abstract0_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
	abstract0 (ap_abstract0_t *x)
	Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object. More...

Protected Attributes
ap_abstract0_t *	a
	Pointer managed by APRON. More...

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

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

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

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

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

void	print (manager &m, char *name_of_dim=NULL, 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
abstract0 &	deserialize (manager &m, abstract0 &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 abstract0 &x, const abstract0 &y)
	Whether x and y represent the same set. More...

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

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

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

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

bool	operator< (const abstract0 &x, const abstract0 &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 abstract0 &x) const
	Whether *this and x represent the same set. More...

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

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

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

bool	sat (manager &m, ap_dim_t dim, const interval &i) const
	Whether the dimension dim of all points in *this is included in the given interval. More...

bool	is_dimension_unconstrained (manager &m, ap_dim_t dim) const
	Whether the points in *this are unbounded in the given dimension. More...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Assignment
abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
	Assignment of linear expression. More...

abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter)
	Parallel assignment of linear expressions. More...

abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter)
	Parallel assignment of linear expressions. More...

abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const texpr0 &l, const abstract0 &inter)
	Assignment of arbitrary expression. More...

abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter)
	Parallel assignment of arbitrary expressions. More...

abstract0 &	assign (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter)
	Parallel assignment of arbitrary expressions. More...

abstract0 &	assign (manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
	In-place assignment of linear expression. More...

abstract0 &	assign (manager &m, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter=null)
	In-place parallel assignment of linear expressions. More...

abstract0 &	assign (manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter=null)
	In-place parallel assignment of linear expressions. More...

abstract0 &	assign (manager &m, ap_dim_t dim, const texpr0 &l, const abstract0 &inter=null)
	In-place assignment of arbitrary expression. More...

abstract0 &	assign (manager &m, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter=null)
	In-place parallel assignment of arbitrary expressions. More...

abstract0 &	assign (manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter=null)
	In-place parallel assignment of arbitrary expressions. More...

Substitution
abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
	Substitution (backward assignment) of linear expression. More...

abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter)
	Parallel substitution (backward assignment) of linear expressions. More...

abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter)
	Parallel substitution (backward assignment) of linear expressions. More...

abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const texpr0 &l, const abstract0 &inter)
	Substitution (backward assignment) of arbitrary expression. More...

abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter)
	Parallel substitution (backward assignment) of arbitrary expressions. More...

abstract0 &	substitute (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter)
	Parallel substitution (backward assignment) of arbitrary expressions. More...

abstract0 &	substitute (manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
	In-place substitution (backward assignment) of linear expression. More...

abstract0 &	substitute (manager &m, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter=null)
	In-place parallel substitution (backward assignment) of linear expressions. More...

abstract0 &	substitute (manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter=null)
	In-place parallel substitution (backward assignment) of linear expressions. More...

abstract0 &	substitute (manager &m, ap_dim_t dim, const texpr0 &l, const abstract0 &inter=null)
	In-place substitution (backward assignment) of arbitrary expression. More...

abstract0 &	substitute (manager &m, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter=null)
	In-place parallel substitution (backward assignment) of arbitrary expressions. More...

abstract0 &	substitute (manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter=null)
	In-place parallel substitution (backward assignment) of arbitrary expressions. More...

Projection, forget
abstract0 &	forget (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, bool project)
	Stores in dst the result of forgetting the value of dimension dim in src. More...

abstract0 &	forget (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], bool project)
	Stores in dst the result of forgetting the value of dimensions dim[0] to dim[size-1] in src. More...

abstract0 &	forget (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > dim, bool project)
	Stores in dst the result of forgetting the value of all the dimensions in dim in src. More...

abstract0 &	forget (manager &m, ap_dim_t dim, bool project=false)
	Forgets about the value of dimension dim in *this. More...

abstract0 &	forget (manager &m, size_t size, const ap_dim_t dim[], bool project=false)
	Forgets about the value of dimensions dims[0] to dims[size-1] in *this. More...

abstract0 &	forget (manager &m, const std::vector< ap_dim_t > dim, bool project=false)
	Forgets about the value of all the dimensions in dim in *this. More...

Change of dimension
abstract0 &	add_dimensions (manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d, bool project)
	Copies src into dst and adds some dimensions. More...

abstract0 &	remove_dimensions (manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d)
	Copies src into dst and removes some dimensions. More...

abstract0 &	permute_dimensions (manager &m, abstract0 &dst, const abstract0 &src, const dimperm &d)
	Copies src into dst and permute some dimensions. More...

abstract0 &	add_dimensions (manager &m, const dimchange &d, bool project=false)
	Adds some dimensions to *this. More...

abstract0 &	remove_dimensions (manager &m, const dimchange &d)
	Removes some dimensions from *this. More...

abstract0 &	permute_dimensions (manager &m, const dimperm &d)
	Permutes some dimensions in *this. More...

Expansion and folding
abstract0 &	expand (manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, size_t n)
	Replaces dst with a copy of src and duplicates dimension dim into n copies. More...

abstract0 &	fold (manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[])
	Replaces dst with a copy of src and folds dimensions dims[0] to dim[size-1]. More...

abstract0 &	fold (manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim)
	Replaces dst with a copy of src and folds all dimensions in dims. More...

abstract0 &	expand (manager &m, ap_dim_t dim, size_t n=1)
	Duplicates dimension dim into n copies in *this (modified in-place). More...

abstract0 &	fold (manager &m, size_t size, const ap_dim_t dim[])
	Folds dimensions dim[0] to dim[size-1] in *this (modified in-place). More...

abstract0 &	fold (manager &m, const std::vector< ap_dim_t > &dim)
	Folds all dimensions dims in *this (modified in-place). More...

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

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

Detailed Description

Level 0 abstract value (ap_abstract0_t* wrapper).

An abstract0 object stores an abstract value. It represents a set of points in a numerical space with some integer-valued dimensions and some real-valued dimensions.

Warning

all the abstract operators are guaranteed to be sound, but not complete, that is:

returned abstract elements and intervals are over-approximations of the actual result on sets,
returned constraint conjunction may satisfy more points than the original abstract element,
returned generators may span more points than the original abstract element,
predicates return true if the predicate is definitively true, and false if either the predicate is false (flag_exact is then true), or due to abstraction, the domain cannot conclude (flag_exact is then false).

An abstract0 is always created with a manager that indicates the underlying library. This defines its internal representation and algorithms, which in turns defines the expressiveness and cost vs. precision trade-off. Most operations to manipulate an abstract0 also take a manager as first argument. This must be a manager compatible with the one of all abstract0 arguments (including this), that is, a manger created by the same library (e.g., NewPolka polyhedra) and using the same parameter values, if any (e.g., strictness). It need not be the very same manager the abstract0 was created with.

Overloaded arithmetic, assignment and copy operators that cannot take an extra manager argument will implicitly use the manager used to create the first argument.

Additionally, for binary or n-aray operators, all abstract0 must have the same number of integer and real dimensions.

Many operations exist in two kinds:

an imperative class function that modifies the this abstract0,
a more "functional" global function that takes as argument both one or several constant source abstract0 and one destination abstract0 that will be overridden with the result.

Both kinds will return a reference to the abstract0 that holds the result.

Most functions can throw a variety of exceptions:

std::invalid_argument, when arguments have incompatible managers, types, or dimensions,
std::length_error, when running out of memory or exceeding the max_object_size value set by the user in the manager,
std::overflow_error, when a numerical overflow occurs,
not_implemented, when some function is not available,
timeout, when exceeding the timout value set by the user in the manager.

Constructor & Destructor Documentation

◆ abstract0() [1/8]

abstract0::abstract0 ( ap_abstract0_t * x )

inlineprotected

Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object.

◆ abstract0() [2/8]

abstract0::abstract0	(	manager &	m,
		size_t	intdim,
		size_t	realdim,
		top	x
	)

inline

Creates an abstract element representing the whole space.

◆ abstract0() [3/8]

abstract0::abstract0	(	manager &	m,
		size_t	intdim,
		size_t	realdim,
		bottom	x
	)

inline

Creates an abstract element representing the empty set.

◆ abstract0() [4/8]

abstract0::abstract0	(	manager &	m,
		const abstract0 &	t
	)

inline

Creates a (deep) copy of the abstract element.

◆ abstract0() [5/8]

abstract0::abstract0	(	manager &	m,
		size_t	intdim,
		size_t	realdim,
		const interval_array &	x
	)

inline

Creates an abstract element from a box.

Exceptions

std::invalid_argument if x has less than intdim+realdim dimensions.

◆ abstract0() [6/8]

abstract0::abstract0	(	manager &	m,
		size_t	intdim,
		size_t	realdim,
		const lincons0_array &	x
	)

inline

Creates an abstract element from a conjunction of linear constraints.

◆ abstract0() [7/8]

abstract0::abstract0	(	manager &	m,
		size_t	intdim,
		size_t	realdim,
		const tcons0_array &	x
	)

inline

Creates an abstract element from a conjunction of arbitrary constraints.

◆ abstract0() [8/8]

abstract0::abstract0 ( const abstract0 & t )

inline

Creates a (deep) copy of the abstract element.

Implicitly uses the manager used to create *this.

◆ ~abstract0()

abstract0::~abstract0 ( )

inline

Destroys the abstract element.

Implicitly uses the manager used to create *this.

Member Function Documentation

◆ add_dimensions()

abstract0 & apron::abstract0::add_dimensions	(	manager &	m,
		const dimchange &	d,
		bool	project = `false`
	)

inline

Adds some dimensions to *this.

project whether to set the new dimensions to 0 (if true), or leave them undefined (if false).

Returns: a reference to *this.

◆ add_rays()

abstract0 & abstract0::add_rays	(	manager &	m,
		const generator0_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()

abstract0 & abstract0::approximate	(	manager &	m,
		int	algorithm
	)

inline

Simplifies the abstract element, potentially loosing precision.

Returns: a reference to *this.

◆ assign() [1/6]

abstract0 & apron::abstract0::assign	(	manager &	m,
		ap_dim_t	dim,
		const linexpr0 &	l,
		const abstract0 &	inter = `null`
	)

inline

In-place assignment of linear expression.

*this is modified in-place to reflect the effect of assigning l to dimension dim. If inter is specified, *this is then intersected with it.

Returns: a reference to *this.

◆ assign() [2/6]

abstract0 & apron::abstract0::assign	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[],
		const linexpr0 *const	l[],
		const abstract0 &	inter = `null`
	)

inline

In-place parallel assignment of linear expressions.

*this is modified in-place to reflect the effect of assigning l[i] to dimension dim[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]

abstract0 & apron::abstract0::assign	(	manager &	m,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const linexpr0 * > &	l,
		const abstract0 &	inter = `null`
	)

inline

In-place parallel assignment of linear expressions.

*this is modified in-place to reflect the effect of assigning l[i] to dimension dim[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]

abstract0 & apron::abstract0::assign	(	manager &	m,
		ap_dim_t	dim,
		const texpr0 &	l,
		const abstract0 &	inter = `null`
	)

inline

In-place assignment of arbitrary expression.

*this is modified in-place to reflect the effect of assigning l to dimension dim. If inter is specified, *this is then intersected with it.

Returns: a reference to *this.

◆ assign() [5/6]

abstract0 & apron::abstract0::assign	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[],
		const texpr0 *const	l[],
		const abstract0 &	inter = `null`
	)

inline

In-place parallel assignment of arbitrary expressions.

*this is modified in-place to reflect the effect of assigning l[i] to dimension dim[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]

abstract0 & apron::abstract0::assign	(	manager &	m,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const texpr0 * > &	l,
		const abstract0 &	inter = `null`
	)

inline

In-place parallel assignment of arbitrary expressions.

*this is modified in-place to reflect the effect of assigning l[i] to dimension dim[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 abstract0::bound	(	manager &	m,
		const linexpr0 &	l
	)		const

inline

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

◆ bound() [2/3]

interval abstract0::bound	(	manager &	m,
		const texpr0 &	l
	)		const

inline

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

◆ bound() [3/3]

interval abstract0::bound	(	manager &	m,
		ap_dim_t	d
	)		const

inline

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

◆ canonicalize()

abstract0 & abstract0::canonicalize ( manager & m )

inline

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

Returns: a reference to *this.

◆ closure()

abstract0 & abstract0::closure ( manager & m )

inline

Replaces *this with its topological closure.

Returns: a reference to *this.

◆ dump()

void abstract0::dump	(	manager &	m,
		FILE *	stream = `stdout`
	)		const

inline

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

◆ expand()

abstract0 & apron::abstract0::expand	(	manager &	m,
		ap_dim_t	dim,
		size_t	n = `1`
	)

inline

Duplicates dimension dim into n copies in *this (modified in-place).

New dimensions are appended after the last integer or real dimension of *this.

Returns: a reference to *this.

◆ fold() [1/2]

abstract0 & abstract0::fold	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[]
	)

inline

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

dim must be sorted and contain variables of the same type (integer or real). After folding, only dim[0] is kept and other dimensions are removed.

Returns: a reference to *this.

◆ fold() [2/2]

abstract0 & abstract0::fold	(	manager &	m,
		const std::vector< ap_dim_t > &	dim
	)

inline

Folds all dimensions dims in *this (modified in-place).

dim must be sorted and contain variables of the same type (integer or real). After folding, only dim[0] is kept and other dimensions are removed.

Returns: a reference to *this.

◆ forget() [1/3]

abstract0 & apron::abstract0::forget	(	manager &	m,
		ap_dim_t	dim,
		bool	project = `false`
	)

inline

Forgets about the value of dimension dim in *this.

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

Returns: a reference to *this.

◆ forget() [2/3]

abstract0 & apron::abstract0::forget	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[],
		bool	project = `false`
	)

inline

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

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

Returns: a reference to *this.

◆ forget() [3/3]

abstract0 & apron::abstract0::forget	(	manager &	m,
		const std::vector< ap_dim_t >	dim,
		bool	project = `false`
	)

inline

Forgets about the value of all the dimensions in dim in *this.

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

Returns: a reference to *this.

◆ free()

void abstract0::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_ap_abstract0_t() [1/2]

ap_abstract0_t * abstract0::get_ap_abstract0_t ( )

inline

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

◆ get_ap_abstract0_t() [2/2]

const ap_abstract0_t * abstract0::get_ap_abstract0_t ( ) const

inline

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

◆ get_dimension()

ap_dimension_t abstract0::get_dimension ( manager & m ) const

inline

Returns the number of integer and real dimensions in the abstract element.

◆ get_manager()

manager abstract0::get_manager ( ) const

inline

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

◆ is_bottom()

bool abstract0::is_bottom ( manager & m ) const

inline

Whether *this represents the empty set.

◆ is_dimension_unconstrained()

bool abstract0::is_dimension_unconstrained	(	manager &	m,
		ap_dim_t	dim
	)		const

inline

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

◆ is_eq()

bool abstract0::is_eq	(	manager &	m,
		const abstract0 &	x
	)		const

inline

Whether *this and x represent the same set.

◆ is_leq()

bool abstract0::is_leq	(	manager &	m,
		const abstract0 &	x
	)		const

inline

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

◆ is_top()

bool abstract0::is_top ( manager & m ) const

inline

Whether *this represents the full space.

◆ join()

abstract0 & abstract0::join	(	manager &	m,
		const abstract0 &	y
	)

inline

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

Returns: a reference to *this.

◆ meet() [1/3]

abstract0 & abstract0::meet	(	manager &	m,
		const abstract0 &	y
	)

inline

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

Returns: a reference to *this.

◆ meet() [2/3]

abstract0 & abstract0::meet	(	manager &	m,
		const lincons0_array &	y
	)

inline

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

Returns: a reference to *this.

◆ meet() [3/3]

abstract0 & abstract0::meet	(	manager &	m,
		const tcons0_array &	y
	)

inline

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

Returns: a reference to *this.

◆ minimize()

abstract0 & abstract0::minimize ( manager & m )

inline

Minimizes the size of the representation, to save memory.

Returns: a reference to *this.

◆ operator *=() [1/3]

abstract0 & abstract0::operator *= ( const abstract0 & 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]

abstract0 & abstract0::operator *= ( const lincons0_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]

abstract0 & abstract0::operator *= ( const tcons0_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]

abstract0 & abstract0::operator+= ( const abstract0 & 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]

abstract0 & abstract0::operator+= ( const generator0_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]

abstract0 & abstract0::operator= ( const abstract0 & t )

inline

Assigns a copy of t to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [2/6]

abstract0 & abstract0::operator= ( top t )

inline

Assigns the full space to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [3/6]

abstract0 & abstract0::operator= ( bottom t )

inline

Assigns the empty set to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [4/6]

abstract0 & abstract0::operator= ( const interval_array & x )

inline

Assigns a box to *this.

Implicitly uses the manager used to create *this.

Exceptions

std::invalid_argument if the array has insufficient size.

◆ operator=() [5/6]

abstract0 & abstract0::operator= ( const lincons0_array & x )

inline

Assigns a conjunction of linear constraints to *this.

Implicitly uses the manager used to create *this.

◆ operator=() [6/6]

abstract0 & abstract0::operator= ( const tcons0_array & x )

inline

Assigns a conjunction of arbitrary constraints to *this.

Implicitly uses the manager used to create *this.

◆ permute_dimensions()

abstract0 & abstract0::permute_dimensions	(	manager &	m,
		const dimperm &	d
	)

inline

Permutes some dimensions in *this.

Returns: a reference to *this.

◆ print()

void abstract0::print	(	manager &	m,
		char **	name_of_dim = `NULL`,
		FILE *	stream = `stdout`
	)		const

inline

Pretty-printing to a C stream.

◆ remove_dimensions()

abstract0 & abstract0::remove_dimensions	(	manager &	m,
		const dimchange &	d
	)

inline

Removes some dimensions from *this.

Returns: a reference to *this.

◆ sat() [1/3]

bool abstract0::sat	(	manager &	m,
		const lincons0 &	l
	)		const

inline

Whether all points in *this satisfy a linear constraint.

◆ sat() [2/3]

bool abstract0::sat	(	manager &	m,
		const tcons0 &	l
	)		const

inline

Whether all points in *this satisfy an arbitrary constraint.

◆ sat() [3/3]

bool abstract0::sat	(	manager &	m,
		ap_dim_t	dim,
		const interval &	i
	)		const

inline

Whether the dimension dim of all points in *this is included in the given interval.

◆ serialize()

std::string * abstract0::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/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		const abstract0 &	x
	)

inline

Replaces *this with a copy of x.

Returns: a reference to *this.

◆ set() [2/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		top	t,
		size_t	intdim = `AP_DIM_MAX`,
		size_t	realdim = `AP_DIM_MAX`
	)

inline

Replaces *this with the full space.

You can either specify new intdim and realdim values or keep those of *this (if unspecified, i.e., left to AP_DIM_MAX).

Returns: a reference to *this.

◆ set() [3/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		bottom	t,
		size_t	intdim = `AP_DIM_MAX`,
		size_t	realdim = `AP_DIM_MAX`
	)

inline

Replaces *this with the empty set.

You can either specify new intdim and realdim values or keep those of *this (if unspecified, i.e., left to AP_DIM_MAX).

Returns: a reference to *this.

◆ set() [4/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		const interval_array &	x,
		size_t	intdim = `AP_DIM_MAX`,
		size_t	realdim = `AP_DIM_MAX`
	)

inline

Replaces *this with a box.

You can either specify new intdim and realdim values or keep those of *this (if unspecified, i.e., left to AP_DIM_MAX).

Returns: a reference to *this.

◆ set() [5/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		const lincons0_array &	x,
		size_t	intdim = `AP_DIM_MAX`,
		size_t	realdim = `AP_DIM_MAX`
	)

inline

Replaces *this with a conjunction of linear constraints.

You can either specify new intdim and realdim values or keep those of *this (if unspecified, i.e., left to AP_DIM_MAX).

Returns: a reference to *this.

◆ set() [6/6]

abstract0 & apron::abstract0::set	(	manager &	m,
		const tcons0_array &	x,
		size_t	intdim = `AP_DIM_MAX`,
		size_t	realdim = `AP_DIM_MAX`
	)

inline

Replaces *this with a conjunction of arbitrary constraints.

You can either specify new intdim and realdim values or keep those of *this (if unspecified, i.e., left to AP_DIM_MAX).

Returns: a reference to *this.

◆ size()

size_t abstract0::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]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		ap_dim_t	dim,
		const linexpr0 &	l,
		const abstract0 &	inter = `null`
	)

inline

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

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

Returns: a reference to *this.

◆ substitute() [2/6]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[],
		const linexpr0 *const	l[],
		const abstract0 &	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 dimension dim[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]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const linexpr0 * > &	l,
		const abstract0 &	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 dimension dim[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]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		ap_dim_t	dim,
		const texpr0 &	l,
		const abstract0 &	inter = `null`
	)

inline

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

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

Returns: a reference to *this.

◆ substitute() [5/6]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		size_t	size,
		const ap_dim_t	dim[],
		const texpr0 *const	l[],
		const abstract0 &	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 dimension dim[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]

abstract0 & apron::abstract0::substitute	(	manager &	m,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const texpr0 * > &	l,
		const abstract0 &	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 dimension dim[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 abstract0::to_box ( manager & m ) const

inline

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

◆ to_generator_array()

generator0_array abstract0::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()

lincons0_array abstract0::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()

tcons0_array abstract0::to_tcons_array ( manager & m ) const

inline

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

Friends And Related Function Documentation

◆ add_dimensions

abstract0& add_dimensions	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const dimchange &	d,
		bool	project = `false`
	)

friend

Copies src into dst and adds some dimensions.

project whether to set the new dimensions to 0 (if true), or leave them undefined (if false).

Returns: a reference to dst.

◆ add_rays

abstract0& add_rays	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	x,
		const generator0_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]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		const linexpr0 &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Assignment of linear expression.

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

Returns: a reference to dst.

◆ assign [2/6]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[],
		const linexpr0 *const	l[],
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel assignment of linear expressions.

dst is replaced with the effect of assigning l[i] to dimension dim[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]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const linexpr0 * > &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel assignment of linear expressions.

dst is replaced with the effect of assigning l[i] to dimension dim[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]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		const texpr0 &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Assignment of arbitrary expression.

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

Returns: a reference to dst.

◆ assign [5/6]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[],
		const texpr0 *const	l[],
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel assignment of arbitrary expressions.

dst is replaced with the effect of assigning l[i] to dimension dim[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]

abstract0& assign	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const texpr0 * > &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel assignment of arbitrary expressions.

dst is replaced with the effect of assigning l[i] to dimension dim[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.

◆ closure

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

friend

Stores in dst the topological closure of src.

Returns: a reference to dst.

◆ deserialize

abstract0& deserialize	(	manager &	m,
		abstract0 &	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

abstract0& expand	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		size_t	n = `1`
	)

friend

Replaces dst with a copy of src and duplicates dimension dim into n copies.

New dimensions are appended after the last integer or real dimension of dst.

Returns: a reference to dst.

◆ fold [1/2]

abstract0& fold	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[]
	)

friend

Replaces dst with a copy of src and folds dimensions dims[0] to dim[size-1].

dim must be sorted and contain variables of the same type (integer or real). After folding, only dim[0] is kept and other dimensions are removed.

Returns: a reference to dst.

◆ fold [2/2]

abstract0& fold	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t > &	dim
	)

friend

Replaces dst with a copy of src and folds all dimensions in dims.

dim must be sorted and contain variables of the same type (integer or real). After folding, only dim[0] is kept and other dimensions are removed.

Returns: a reference to dst.

◆ forget [1/3]

abstract0& forget	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		bool	project = `false`
	)

friend

Stores in dst the result of forgetting the value of dimension dim in src.

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

Returns: a reference to dst.

◆ forget [2/3]

abstract0& forget	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[],
		bool	project = `false`
	)

friend

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

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

Returns: a reference to dst.

◆ forget [3/3]

abstract0& forget	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t >	dim,
		bool	project = `false`
	)

friend

Stores in dst the result of forgetting the value of all the dimensions in dim in src.

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

Returns: a reference to dst.

◆ join [1/3]

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

friend

Replaces dst with the join of x and y.

Returns: a reference to dst.

◆ join [2/3]

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

friend

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

Returns: a reference to dst.

◆ join [3/3]

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

friend

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

Returns: a reference to dst.

◆ meet [1/5]

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

friend

Replaces dst with the meet of x and y.

Returns: a reference to dst.

◆ meet [2/5]

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

friend

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

Returns: a reference to dst.

◆ meet [3/5]

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

friend

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

Returns: a reference to dst.

◆ meet [4/5]

abstract0& meet	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	x,
		const lincons0_array &	y
	)

friend

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

Returns: a reference to dst.

◆ meet [5/5]

abstract0& meet	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	x,
		const tcons0_array &	y
	)

friend

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

Returns: a reference to dst.

◆ operator!=

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

friend

Whether x and y represent different sets.

The manager for the left argument is used implicitly.

◆ operator<

bool operator<	(	const abstract0 &	x,
		const abstract0 &	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 abstract0 &	s
	)

friend

Prints in constraint form.

◆ operator<=

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

friend

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

The manager for the left argument is used implicitly.

◆ operator==

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

friend

Whether x and y represent the same set.

The manager for the left argument is used implicitly.

◆ operator>

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

friend

Whether x strictly contains y (set-wise).

The manager for the left argument is used implicitly.

◆ operator>=

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

friend

Whether x contains y (set-wise).

The manager for the left argument is used implicitly.

◆ permute_dimensions

abstract0& permute_dimensions	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const dimperm &	d
	)

friend

Copies src into dst and permute some dimensions.

Returns: a reference to dst.

◆ printdiff

void printdiff	(	manager &	m,
		const abstract0 &	x,
		const abstract0 &	y,
		char **	name_of_dim = `NULL`,
		FILE *	stream = `stdout`
	)

friend

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

◆ remove_dimensions

abstract0& remove_dimensions	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const dimchange &	d
	)

friend

Copies src into dst and removes some dimensions.

Returns: a reference to dst.

◆ substitute [1/6]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		const linexpr0 &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Substitution (backward assignment) of linear expression.

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

Returns: a reference to dst.

◆ substitute [2/6]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[],
		const linexpr0 *const	l[],
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel substitution (backward assignment) of linear expressions.

dst is replaced with the effect of substituting l[i] to dimension dim[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]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const linexpr0 * > &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel substitution (backward assignment) of linear expressions.

dst is replaced with the effect of substituting l[i] to dimension dim[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]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		ap_dim_t	dim,
		const texpr0 &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Substitution (backward assignment) of arbitrary expression.

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

Returns: a reference to dst.

◆ substitute [5/6]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		size_t	size,
		const ap_dim_t	dim[],
		const texpr0 *const	l[],
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel substitution (backward assignment) of arbitrary expressions.

dst is replaced with the effect of substituting l[i] to dimension dim[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]

abstract0& substitute	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	src,
		const std::vector< ap_dim_t > &	dim,
		const std::vector< const texpr0 * > &	l,
		const abstract0 &	inter = `abstract0::null`
	)

friend

Parallel substitution (backward assignment) of arbitrary expressions.

dst is replaced with the effect of substituting l[i] to dimension dim[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.

◆ widening [1/2]

abstract0& widening	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	x,
		const abstract0 &	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]

abstract0& widening	(	manager &	m,
		abstract0 &	dst,
		const abstract0 &	x,
		const abstract0 &	y,
		const lincons0_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_abstract0_t* apron::abstract0::a

protected

Pointer managed by APRON.

◆ null

const abstract0 apron::abstract0::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_abstract0.hh
/home/mine/apron/apronxx/apxx_abstract0_inline.hh

Public Member Functions

Protected Member Functions

Protected Attributes

Static Protected Attributes

Friends

Printing

Serialisation

Predicates

Meet

Join

Assignment

Substitution

Projection, forget

Change of dimension

Expansion and folding

Closure

Detailed Description

Constructor & Destructor Documentation

◆ abstract0() [1/8]

◆ abstract0() [2/8]

◆ abstract0() [3/8]

◆ abstract0() [4/8]

◆ abstract0() [5/8]

◆ abstract0() [6/8]

◆ abstract0() [7/8]

◆ abstract0() [8/8]

◆ ~abstract0()

Member Function Documentation

◆ add_dimensions()

◆ 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()

◆ closure()

◆ dump()

◆ expand()

◆ fold() [1/2]

◆ fold() [2/2]

◆ forget() [1/3]

◆ forget() [2/3]

◆ forget() [3/3]

◆ free()

◆ get_ap_abstract0_t() [1/2]

◆ get_ap_abstract0_t() [2/2]

◆ get_dimension()

◆ get_manager()

◆ is_bottom()

◆ is_dimension_unconstrained()

◆ is_eq()

◆ is_leq()

◆ is_top()

◆ join()

◆ meet() [1/3]

◆ meet() [2/3]

◆ meet() [3/3]

◆ minimize()

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

◆ permute_dimensions()

◆ print()

◆ remove_dimensions()

◆ sat() [1/3]

◆ sat() [2/3]