16#ifndef __APXX_ABSTRACT0_HH
17#define __APXX_ABSTRACT0_HH
20#include "ap_abstract0.h"
286 void print(
manager& m,
char** name_of_dim=NULL, FILE* stream=stdout)
const;
Level 0 abstract value (ap_abstract0_t* wrapper).
Definition apxx_abstract0.hh:78
friend bool operator==(const abstract0 &x, const abstract0 &y)
Whether x and y represent the same set.
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition apxx_abstract0_inline.hh:475
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const tcons0_array &y)
Replaces dst with the meet of x and some arbitrary constraints.
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const lincons0_array &y)
Replaces dst with the meet of x and some linear constraints.
abstract0 & operator+=(const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition apxx_abstract0_inline.hh:664
abstract0 & set(manager &m, const abstract0 &x)
Replaces *this with a copy of x.
friend 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.
friend 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.
friend abstract0 & add_rays(manager &m, abstract0 &dst, const abstract0 &x, const generator0_array &y)
Replaces dst with x with some rays added.
lincons0_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition apxx_abstract0_inline.hh:483
friend 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.
friend 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.
friend 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.
void free(manager &m)
Destroys the abstract element using the given manager.
Definition apxx_abstract0_inline.hh:89
friend 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.
friend bool operator<=(const abstract0 &x, const abstract0 &y)
Whether x is included within y (set-wise).
friend abstract0 & remove_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d)
Copies src into dst and removes some dimensions.
friend bool operator>(const abstract0 &x, const abstract0 &y)
Whether x strictly contains y (set-wise).
friend 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.
friend abstract0 & join(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the join of x and y.
friend bool operator<(const abstract0 &x, const abstract0 &y)
Whether x is strictly included within y (set-wise).
friend 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.
friend 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.
static const abstract0 null
NULL abstract element, to be used only as default argument in assign and substitute.
Definition apxx_abstract0.hh:88
abstract0(ap_abstract0_t *x)
Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object.
Definition apxx_abstract0_inline.hh:27
friend 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.
friend abstract0 & join(manager &m, abstract0 &dst, const std::vector< const abstract0 * > &x)
Replaces dst with the join of all abstract elements in x.
friend 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.
tcons0_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition apxx_abstract0_inline.hh:491
friend 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.
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the meet of x and y.
friend abstract0 & add_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d, bool project)
Copies src into dst and adds some dimensions.
abstract0 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition apxx_abstract0_inline.hh:263
ap_abstract0_t * a
Pointer managed by APRON.
Definition apxx_abstract0.hh:82
bool is_eq(manager &m, const abstract0 &x) const
Whether *this and x represent the same set.
Definition apxx_abstract0_inline.hh:366
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition apxx_abstract0_inline.hh:328
friend 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.
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_abstract0_inline.hh:1172
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition apxx_abstract0_inline.hh:286
abstract0 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition apxx_abstract0_inline.hh:256
abstract0 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition apxx_abstract0_inline.hh:249
bool is_leq(manager &m, const abstract0 &x) const
Whether *this is included in x (set-wise).
Definition apxx_abstract0_inline.hh:373
abstract0 & operator=(const abstract0 &t)
Assigns a copy of t to *this.
Definition apxx_abstract0_inline.hh:99
friend 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].
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const texpr0 &l, const abstract0 &inter)
Assignment of arbitrary expression.
friend abstract0 & closure(manager &m, abstract0 &dst, const abstract0 &src)
Stores in dst the topological closure of src.
friend bool operator>=(const abstract0 &x, const abstract0 &y)
Whether x contains y (set-wise).
friend 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.
generator0_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition apxx_abstract0_inline.hh:499
friend bool operator!=(const abstract0 &x, const abstract0 &y)
Whether x and y represent different sets.
friend 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.
friend std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Prints in constraint form.
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition apxx_abstract0_inline.hh:304
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition apxx_abstract0_inline.hh:340
friend abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Stores in dst the result of x widened with y.
bool sat(manager &m, const lincons0 &l) const
Whether all points in *this satisfy a linear constraint.
Definition apxx_abstract0_inline.hh:380
bool is_top(manager &m) const
Whether *this represents the full space.
Definition apxx_abstract0_inline.hh:359
friend 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.
interval bound(manager &m, const linexpr0 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element.
Definition apxx_abstract0_inline.hh:447
friend abstract0 & meet(manager &m, abstract0 &dst, const std::vector< const abstract0 * > &x)
Replaces dst with the meet of all abstract elements in x.
friend 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.
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
Assignment of linear expression.
bool is_dimension_unconstrained(manager &m, ap_dim_t dim) const
Whether the points in *this are unbounded in the given dimension.
Definition apxx_abstract0_inline.hh:401
void print(manager &m, char **name_of_dim=NULL, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition apxx_abstract0_inline.hh:274
friend abstract0 & permute_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimperm &d)
Copies src into dst and permute some dimensions.
friend 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.
~abstract0()
Destroys the abstract element.
Definition apxx_abstract0_inline.hh:83
abstract0 & operator*=(const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition apxx_abstract0_inline.hh:657
ap_dimension_t get_dimension(manager &m) const
Returns the number of integer and real dimensions in the abstract element.
Definition apxx_abstract0_inline.hh:333
friend 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.
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition apxx_abstract0_inline.hh:352
friend 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.
Represents a dimension (i.e., variable by index) in an expression tree.
Definition apxx_texpr0.hh:33
Dimension change object (ap_dimchange_t wrapper).
Definition apxx_dimension.hh:102
Dimension permutation object (ap_dimperm_t wrapper).
Definition apxx_dimension.hh:292
Array of generators (ap_generator0_array_t wrapper).
Definition apxx_generator0.hh:214
array of interval(s).
Definition apxx_interval.hh:302
Interval (ap_interval_t wrapper).
Definition apxx_interval.hh:47
Array of linear constraints (ap_lincons0_array_t wrapper).
Definition apxx_lincons0.hh:341
Level 0 linear constraint (ap_lincons0_t wrapper).
Definition apxx_lincons0.hh:43
Level 0 linear expression (ap_linexpr0_t wrapper).
Definition apxx_linexpr0.hh:44
Library manager (ap_manager_t wrapper).
Definition apxx_manager.hh:137
Array of arbitrary constraints (ap_tcons0_array_t wrapper).
Definition apxx_tcons0.hh:350
Level 0 arbitrary constraint (ap_tcons0_t wrapper).
Definition apxx_tcons0.hh:47
Level 0 arbitrary expression tree (ap_texpr0_t wrapper).
Definition apxx_texpr0.hh:92
Definition apxx_abstract0.hh:27
Empty interval or domain, to simplify initialisations and assignments.
Definition apxx_interval.hh:33
Full interval (]-oo,+oo[) or domain, to simplify initialisations and assignments.
Definition apxx_interval.hh:27
Inherited by most wrappers to map new and delete to malloc and free.
Definition apxx_scalar.hh:69