APRONXX  0.9.12
/builddir/build/BUILD/apron-0.9.13/apronxx/apxx_abstract1.hh
Go to the documentation of this file.
1 /* -*- C++ -*-
2  * apxx_abstract1.hh
3  *
4  * APRON Library / C++ class wrappers
5  *
6  * Copyright (C) Antoine Mine' 2007
7  *
8  */
9 /* This file is part of the APRON Library, released under LGPL license
10  with an exception allowing the redistribution of statically linked
11  executables.
12 
13  Please read the COPYING file packaged in the distribution.
14 */
15 
16 #ifndef __APXX_ABSTRACT1_HH
17 #define __APXX_ABSTRACT1_HH
18 
19 #include "ap_abstract1.h"
20 #include "apxx_abstract0.hh"
21 #include "apxx_linexpr1.hh"
22 #include "apxx_lincons1.hh"
23 #include "apxx_generator1.hh"
24 
25 
26 namespace apron {
27 
28 
29 /* ================================= */
30 /* abstract1 */
31 /* ================================= */
32 
33 
42 class abstract1 : public use_malloc {
43 
44 protected:
45 
46  ap_abstract1_t a;
47 
49  static const abstract1 null;
50 
52  abstract1(ap_abstract1_t x);
53 
54  friend class manager;
55 
56 public:
57 
58 
59  /* constructors */
60  /* ============ */
61 
64 
66  abstract1(manager &m, const environment& e, top x);
67 
69  abstract1(manager &m, const environment& e, bottom x);
70 
72  abstract1(manager &m, const abstract1& t);
73 
75  abstract1(manager &m, const environment& e, const abstract0& t);
76 
82  abstract1(manager &m, const environment& e, const var v[], const interval_array& x);
83 
89  abstract1(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x);
90 
92  abstract1(manager &m, const lincons1_array& x);
93 
95  abstract1(manager &m, const tcons1_array& x);
96 
101  abstract1(const abstract1& t);
102 
104 
105 
106  /* destructor */
107  /* ========== */
108 
111 
116  ~abstract1();
117 
123  void free(manager& m);
124 
126 
127 
128  /* assignments */
129  /* =========== */
130 
133 
138  abstract1& operator=(const abstract1& t);
139 
144  abstract1& operator=(top t);
145 
152 
161 
168 
173  abstract1& operator=(const tcons1_array& x);
174 
179  abstract1& set(manager& m, const abstract1& x);
180 
187  abstract1& set(manager& m, top t);
188 
193  abstract1& set(manager& m, const environment& e, top t);
194 
201  abstract1& set(manager& m, bottom t);
202 
207  abstract1& set(manager& m, const environment& e, bottom t);
208 
215  abstract1& set(manager& m, const interval_array& x);
216 
217 
222  abstract1& set(manager &m, const environment& e, const var v[], const interval_array& x);
223 
228  abstract1& set(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x);
229 
234  abstract1& set(manager& m, const lincons1_array& x);
235 
240  abstract1& set(manager& m, const tcons1_array& x);
241 
242 
244 
245 
246  /* representation */
247  /* ============== */
248 
251 
257 
263 
268  abstract1& approximate(manager& m, int algorithm);
269 
271 
272 
273  /* printing */
274  /* ======== */
275 
278 
280  void print(manager& m, FILE* stream=stdout) const;
281 
283  friend void printdiff(manager& m, const abstract1& x, const abstract1& y, FILE* stream);
284 
286  void dump(manager& m, FILE* stream=stdout) const;
287 
289  friend std::ostream& operator<< (std::ostream& os, const abstract1& s);
290 
292 
293 
294  /* serialisation */
295  /* ============= */
296 
299 
307  std::string* serialize(manager& m) const;
308 
318  friend abstract1& deserialize(manager& m, abstract1& dst, const std::string& s, size_t* eaten);
319 
321 
322 
323  /* access */
324  /* ====== */
325 
328 
330  manager get_manager() const;
331 
334 
337 
339  const abstract0& get_abstract0() const;
340 
347  size_t size(manager& m) const;
348 
350 
351 
352  /* predicates */
353  /* ========== */
354 
357 
359  bool is_bottom(manager& m) const;
360 
362  bool is_top(manager& m) const;
363 
365  bool is_eq(manager& m, const abstract1& x) const;
366 
368  bool is_leq(manager& m, const abstract1& x) const;
369 
371  bool sat(manager& m, const lincons1& l) const;
372 
374  bool sat(manager& m, const tcons1& l) const;
375 
379  bool sat(manager& m, const var& v, const interval& i) const;
380 
382  bool is_variable_unconstrained(manager& m, const var& v) const;
383 
388  friend bool operator== (const abstract1& x, const abstract1& y);
389 
394  friend bool operator!= (const abstract1& x, const abstract1& y);
395 
400  friend bool operator<= (const abstract1& x, const abstract1& y);
401 
406  friend bool operator>= (const abstract1& x, const abstract1& y);
407 
412  friend bool operator> (const abstract1& x, const abstract1& y);
413 
418  friend bool operator< (const abstract1& x, const abstract1& y);
419 
420 
421 
422  /* Properties */
423  /* ========== */
424 
427 
429  interval bound(manager& m, const linexpr1& l) const;
430 
432  interval bound(manager& m, const texpr1& l) const;
433 
435  interval bound(manager& m, const var& v) const;
436 
438  interval_array to_box(manager& m) const;
439 
444 
449 
454 
456 
457 
458  /* Meet and unification */
459  /* ==================== */
460 
463 
468  abstract1& meet(manager& m, const abstract1& y);
469 
474  friend abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);
475 
476 
484  abstract1& unify(manager& m, const abstract1& y);
485 
493  friend abstract1& unify(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);
494 
495 
500  friend abstract1& meet(manager& m, abstract1& dst, const std::vector<const abstract1*>& x);
501 
506  friend abstract1& meet(manager& m, abstract1& dst, size_t size, const abstract1 * const x[]);
507 
512  abstract1& meet(manager& m, const lincons1_array& y);
513 
518  friend abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const lincons1_array& y);
519 
524  abstract1& meet(manager& m, const tcons1_array& y);
525 
530  friend abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const tcons1_array& y);
531 
532 
539  abstract1& operator*=(const abstract1& y);
540 
541 
549 
556  abstract1& operator*=(const tcons1_array& y);
557 
559 
560 
561 
562 
563  /* Join */
564  /* ==== */
565 
568 
573  abstract1& join(manager& m, const abstract1& y);
574 
579  friend abstract1& join(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);
580 
585  friend abstract1& join(manager& m, abstract1& dst, const std::vector<const abstract1*>& x);
586 
591  friend abstract1& join(manager& m, abstract1& dst, size_t size, const abstract1 * const x[]);
592 
600 
607  friend abstract1& add_rays(manager& m, abstract1& dst, const abstract1& x, const generator1_array& y);
608 
615  abstract1& operator+=(const abstract1& y);
616 
626 
628 
629 
630  /* Assignments */
631  /* =========== */
632 
635 
643  abstract1& assign(manager& m, const var& v, const linexpr1& l, const abstract1& inter = null);
644 
654  abstract1& assign(manager& m, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = null);
655 
656 
667  abstract1& assign(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);
668 
676  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter);
677 
687  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter);
688 
699  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter);
700 
701 
702 
703 
711  abstract1& assign(manager& m, const var& v, const texpr1& l, const abstract1& inter = null);
712 
722  abstract1& assign(manager& m, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = null);
723 
724 
735  abstract1& assign(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = null);
736 
744  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter);
745 
755  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter);
756 
767  friend abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter);
768 
770 
771 
772  /* Substitutions */
773  /* ============== */
774 
777 
785  abstract1& substitute(manager& m, const var& v, const linexpr1& l, const abstract1& inter = null);
786 
796  abstract1& substitute(manager& m, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = null);
797 
798 
809  abstract1& substitute(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = null);
810 
818  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter);
819 
829  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter);
830 
841  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter);
842 
843 
844 
845 
853  abstract1& substitute(manager& m, const var& v, const texpr1& l, const abstract1& inter = null);
854 
864  abstract1& substitute(manager& m, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = null);
865 
866 
877  abstract1& substitute(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = null);
878 
886  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter);
887 
897  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter);
898 
909  friend abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter);
910 
912 
913 
914 
915  /* Projection */
916  /* ========== */
917 
920 
927  abstract1& forget(manager& m, const var& v, bool project = false);
928 
935  abstract1& forget(manager& m, size_t size, const var v[], bool project = false);
936 
943  abstract1& forget(manager& m, const std::vector<var>& v, bool project = false);
944 
951  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const var& v, bool project);
952 
960  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], bool project);
961 
968  friend abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, bool project);
969 
971 
972 
973  /* Change of environment */
974  /* ====================== */
975 
978 
985  abstract1& change_environment(manager& m, const environment& e, bool project = false);
986 
993  friend abstract1& change_environment(manager& m, abstract1& dst, const abstract1& src, const environment& e, bool project);
994 
1000 
1006 
1011  abstract1& rename(manager& m, size_t size, const var oldv[], const var newv[]);
1012 
1017  abstract1& rename(manager& m, const std::vector<var>& oldv, const std::vector<var>& newv);
1018 
1023  friend abstract1& rename(manager& m, abstract1& dst, const abstract1& src, size_t size, const var oldv[], const var newv[]);
1024 
1029  friend abstract1& rename(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& oldv, const std::vector<var>& newv);
1030 
1032 
1033 
1034  /* Expansion and folding */
1035  /* ===================== */
1036 
1039 
1046  abstract1& expand(manager& m, const var& v, size_t size, const var vv[]);
1047 
1054  abstract1& expand(manager& m, const var& v, const std::vector<var>& vv);
1055 
1062  friend abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, size_t size, const var vv[]);
1063 
1070  friend abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, const std::vector<var>& vv);
1071 
1078  abstract1& fold(manager& m, size_t size, const var v[]);
1079 
1086  abstract1& fold(manager& m, const std::vector<var>& v);
1087 
1094  friend abstract1& fold(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[]);
1095 
1102  friend abstract1& fold(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v);
1103 
1105 
1106 
1107  /* Widenings */
1108  /* ========= */
1109 
1112 
1119  friend abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y);
1120 
1127  friend abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y, const lincons1_array& l);
1128 
1130 
1131 
1132  /* Closure */
1133  /* ======= */
1134 
1137 
1138 
1143  abstract1& closure(manager& m);
1144 
1149  friend abstract1& closure(manager& m, abstract1& dst, const abstract1& src);
1150 
1152 
1153 
1154 
1155  /* C-level compatibility */
1156  /* ===================== */
1157 
1160 
1162  ap_abstract1_t* get_ap_abstract1_t();
1163 
1165  const ap_abstract1_t* get_ap_abstract1_t() const;
1166 
1168 
1169 };
1170 
1171 #include "apxx_abstract1_inline.hh"
1172 
1173 }
1174 
1175 #endif /* __APXX_ABSTRACT1_HH */
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 & meet(manager &m, abstract1 &dst, const abstract1 &x, const tcons1_array &y)
Replaces dst with the meet of x and some arbitrary constraints.
abstract1 & assign(manager &m, const std::vector< var > &v, const std::vector< const linexpr1 * > &l, const abstract1 &inter=null)
In-place parallel assignment of linear expressions.
abstract1 & substitute(manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
In-place substitution (backward assignment) of arbitrary expression.
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.
friend std::ostream & operator<<(std::ostream &os, const abstract1 &s)
Prints in constraint form.
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.
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition: apxx_abstract1_inline.hh:420
environment get_environment() const
Returns the environment of the abstract element (with reference count incremented).
Definition: apxx_abstract1_inline.hh:405
abstract1 & substitute(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place substitution (backward assignment) of linear expression.
abstract1 & assign(manager &m, const var &v, const texpr1 &l, const abstract1 &inter=null)
In-place assignment of arbitrary expression.
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.
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.
abstract1 & substitute(manager &m, size_t size, const var v[], const linexpr1 *const l[], const abstract1 &inter=null)
In-place parallel substitution (backward assignment) of linear expressions.
abstract1 & assign(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place assignment of linear expression.
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.
abstract1 & forget(manager &m, const std::vector< var > &v, bool project=false)
Forgets about the value of all the variables in v in *this.
friend abstract1 & closure(manager &m, abstract1 &dst, const abstract1 &src)
Stores in dst the topological closure of src.
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.
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 & 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.
abstract1 & fold(manager &m, size_t size, const var v[])
Folds variables v[0] to v[size-1] in *this (modified in-place).
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 & join(manager &m, abstract1 &dst, size_t size, const abstract1 *const x[])
Replaces dst with the join of all size abstract elements in x.
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.
abstract1 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition: apxx_abstract1_inline.hh:324
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.
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.
friend abstract1 & meet(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the meet of x and y.
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.
abstract1 & add_rays(manager &m, const generator1_array &y)
Adds some rays to *this (modified in-place).
Definition: apxx_abstract1_inline.hh:788
friend abstract1 & change_environment(manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project)
Replaces dst with src and changes its environment.
friend bool operator!=(const abstract1 &x, const abstract1 &y)
Whether x and y represent different sets.
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.
friend abstract1 & unify(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the meet of x and y.
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].
~abstract1()
Destroys the abstract element.
Definition: apxx_abstract1_inline.hh:108
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, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter)
Parallel substitution (backward assignment) of arbitrary expressions.
abstract1 & assign(manager &m, const std::vector< var > &v, const std::vector< const texpr1 * > &l, const abstract1 &inter=null)
In-place parallel assignment of arbitrary expressions.
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).
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
abstract1 & join(manager &m, const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:695
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition: apxx_abstract1_inline.hh:434
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.
bool sat(manager &m, const lincons1 &l) const
Whether all points in *this satisfy a linear constraint.
Definition: apxx_abstract1_inline.hh:468
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.
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition: apxx_abstract1_inline.hh:400
friend abstract1 & join(manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
Replaces dst with the join of all abstract elements in x.
bool is_eq(manager &m, const abstract1 &x) const
Whether *this and x represent the same set.
Definition: apxx_abstract1_inline.hh:450
abstract1 & unify(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:627
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 & assign(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const texpr1 &l, const abstract1 &inter)
Assignment of arbitrary expression.
friend bool operator<=(const abstract1 &x, const abstract1 &y)
Whether x is included within y (set-wise).
abstract1 & rename(manager &m, size_t size, const var oldv[], const var newv[])
Renames oldv[i] into newv[i] in *this.
Definition: apxx_abstract1_inline.hh:1369
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
friend abstract1 & assign(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter)
Assignment of linear expression.
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.
friend abstract1 & add_rays(manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
Replaces dst with x with some rays added.
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.
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
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition: apxx_abstract1_inline.hh:374
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 & forget(manager &m, const var &v, bool project=false)
Forgets about the value of variable v in *this.
abstract1 & change_environment(manager &m, const environment &e, bool project=false)
Modifies the environment of *this.
abstract1 & operator=(const abstract1 &t)
Assigns a copy of t to *this.
Definition: apxx_abstract1_inline.hh:124
abstract1 & closure(manager &m)
Replaces *this with its topological closure.
Definition: apxx_abstract1_inline.hh:1565
friend abstract1 & meet(manager &m, abstract1 &dst, const std::vector< const abstract1 * > &x)
Replaces dst with the meet of all abstract elements in x.
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_environment(manager &m)
Removes from *this the variables that are unconstrained.
Definition: apxx_abstract1_inline.hh:1351
abstract1 & expand(manager &m, const var &v, size_t size, const var vv[])
Duplicates variable v into size copies in *this (modified in-place).
Definition: apxx_abstract1_inline.hh:1434
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).
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).
friend abstract1 & join(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the join of x and y.
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.
friend abstract1 & minimize_environment(manager &m, abstract1 &dst, const abstract1 &src)
Replaces dst with src and removes the variables that are unconstrained.
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
abstract1 & meet(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:648
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.
abstract1 & fold(manager &m, const std::vector< var > &v)
Folds all variables v in *this (modified in-place).
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.
abstract1 & assign(manager &m, size_t size, const var v[], const texpr1 *const l[], const abstract1 &inter=null)
In-place parallel assignment of arbitrary expressions.
abstract1 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition: apxx_abstract1_inline.hh:317
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.
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 & 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 & 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].
abstract1(ap_abstract1_t x)
Internal use only. Shallow copy of structure.
Definition: apxx_abstract1_inline.hh:27
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.
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.
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
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.
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