16#ifndef __APXX_ABSTRACT1_HH
17#define __APXX_ABSTRACT1_HH
19#include "ap_abstract1.h"
Level 0 abstract value (ap_abstract0_t* wrapper).
Definition apxx_abstract0.hh:78
Level 1 abstract value (ap_abstract1_t wrapper).
Definition apxx_abstract1.hh:42
friend 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.
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition apxx_abstract1_inline.hh:420
friend 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.
environment get_environment() const
Returns the environment of the abstract element (with reference count incremented).
Definition apxx_abstract1_inline.hh:405
friend 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].
friend abstract1 & assign(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter)
Assignment of linear expression.
friend 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.
friend abstract1 & substitute(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const texpr1 &l, const abstract1 &inter)
Substitution (backward assignment) of arbitrary expression.
friend 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.
friend 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].
interval bound(manager &m, const linexpr1 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element.
Definition apxx_abstract1_inline.hh:549
friend 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.
friend abstract1 & meet(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the meet of x and y.
friend abstract1 & closure(manager &m, abstract1 &dst, const abstract1 &src)
Stores in dst the topological closure of src.
static const abstract1 null
NULL abstract element, to be used only as default argument in assign and substitute.
Definition apxx_abstract1.hh:49
friend abstract1 & join(manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
Replaces dst with the join of all abstract elements in x.
abstract1 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition apxx_abstract1_inline.hh:324
friend 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.
abstract1 & fold(manager &m, size_t size, const var v[])
Folds variables v[0] to v[size-1] in *this (modified in-place).
friend bool operator!=(const abstract1 &x, const abstract1 &y)
Whether x and y represent different sets.
friend 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.
~abstract1()
Destroys the abstract element.
Definition apxx_abstract1_inline.hh:108
friend 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].
friend 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.
friend 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.
friend abstract1 & join(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the join of x and y.
friend 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.
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition apxx_abstract1_inline.hh:581
friend bool operator<(const abstract1 &x, const abstract1 &y)
Whether x is strictly included within y (set-wise).
friend abstract1 & unify(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the meet of x and y.
generator1_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition apxx_abstract1_inline.hh:613
friend 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.
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition apxx_abstract1_inline.hh:434
friend abstract1 & change_environment(manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project)
Replaces dst with src and changes its environment.
bool sat(manager &m, const lincons1 &l) const
Whether all points in *this satisfy a linear constraint.
Definition apxx_abstract1_inline.hh:468
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition apxx_abstract1_inline.hh:400
bool is_eq(manager &m, const abstract1 &x) const
Whether *this and x represent the same set.
Definition apxx_abstract1_inline.hh:450
friend abstract1 & meet(manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
Replaces dst with the meet of all abstract elements in x.
bool is_leq(manager &m, const abstract1 &x) const
Whether *this is included in x (set-wise).
Definition apxx_abstract1_inline.hh:459
friend abstract1 & meet(manager &m, abstract1 &dst, const abstract1 &x, const tcons1_array &y)
Replaces dst with the meet of x and some arbitrary constraints.
friend bool operator<=(const abstract1 &x, const abstract1 &y)
Whether x is included within y (set-wise).
friend abstract1 & substitute(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter)
Substitution (backward assignment) of linear expression.
abstract1 & operator*=(const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition apxx_abstract1_inline.hh:812
void print(manager &m, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition apxx_abstract1_inline.hh:342
abstract1 & set(manager &m, const abstract1 &x)
Replaces *this with a copy of x.
Definition apxx_abstract1_inline.hh:192
abstract1 & operator+=(const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition apxx_abstract1_inline.hh:822
abstract1 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition apxx_abstract1_inline.hh:331
abstract0 & get_abstract0()
Returns a (modifiable) reference to the underlying abstract0.
Definition apxx_abstract1_inline.hh:410
friend 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.
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition apxx_abstract1_inline.hh:374
friend std::ostream & operator<<(std::ostream &os, const abstract1 &s)
Prints in constraint form.
ap_abstract1_t * get_ap_abstract1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_abstract1_inline.hh:1586
abstract1 & operator=(const abstract1 &t)
Assigns a copy of t to *this.
Definition apxx_abstract1_inline.hh:124
friend 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.
friend 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.
friend abstract1 & add_rays(manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
Replaces dst with x with some rays added.
abstract1 & fold(manager &m, const std::vector< var > &v)
Folds all variables v in *this (modified in-place).
bool is_variable_unconstrained(manager &m, const var &v) const
Whether the points in *this are unbounded in the given variable.
Definition apxx_abstract1_inline.hh:496
friend bool operator>=(const abstract1 &x, const abstract1 &y)
Whether x contains y (set-wise).
friend abstract1 & assign(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const texpr1 &l, const abstract1 &inter)
Assignment of arbitrary expression.
friend abstract1 & meet(manager &m, abstract1 &dst, const abstract1 &x, const lincons1_array &y)
Replaces dst with the meet of x and some linear constraints.
tcons1_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition apxx_abstract1_inline.hh:603
friend bool operator>(const abstract1 &x, const abstract1 &y)
Whether x strictly contains y (set-wise).
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition apxx_abstract1_inline.hh:356
ap_abstract1_t a
Structure managed by APRON.
Definition apxx_abstract1.hh:46
friend abstract1 & widening(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Stores in dst the result of x widened with y.
friend 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.
friend 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.
abstract1 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition apxx_abstract1_inline.hh:317
friend void printdiff(manager &m, const abstract1 &x, const abstract1 &y, FILE *stream)
Pretty-printing the difference between x and y to a C stream.
bool is_top(manager &m) const
Whether *this represents the full space.
Definition apxx_abstract1_inline.hh:442
friend abstract1 & minimize_environment(manager &m, abstract1 &dst, const abstract1 &src)
Replaces dst with src and removes the variables that are unconstrained.
abstract1(ap_abstract1_t x)
Internal use only. Shallow copy of structure.
Definition apxx_abstract1_inline.hh:27
friend 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.
friend 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.
void free(manager &m)
Destroys the abstract element using the given manager.
Definition apxx_abstract1_inline.hh:114
friend bool operator==(const abstract1 &x, const abstract1 &y)
Whether x and y represent the same set.
interval bound(manager &m, const var &v) const
Returns some bounds for the given variable on all points in the abstract element.
lincons1_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition apxx_abstract1_inline.hh:593
Level 1 environment (ap_environment_t wrapper).
Definition apxx_environment.hh:51
Array of generators (ap_generator1_array_t wrapper).
Definition apxx_generator1.hh:272
array of interval(s).
Definition apxx_interval.hh:302
Interval (ap_interval_t wrapper).
Definition apxx_interval.hh:47
Array of linear constraints (ap_lincons1_array_t wrapper).
Definition apxx_lincons1.hh:331
Level 1 linear constraint (ap_lincons1_t wrapper).
Definition apxx_lincons1.hh:40
Level 1 linear expression (ap_linexpr1_t wrapper).
Definition apxx_linexpr1.hh:39
Library manager (ap_manager_t wrapper).
Definition apxx_manager.hh:137
Array of arbitrary constraints (ap_tcons1_array_t wrapper).
Definition apxx_tcons1.hh:337
Level 1 arbitrary constraint (ap_tcons1_t wrapper).
Definition apxx_tcons1.hh:39
Level 1 arbitrary expression tree (ap_texpr1_t wrapper).
Definition apxx_texpr1.hh:42
Variable name (ap_var_t wrapper).
Definition apxx_var.hh:39
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