APRONXX 0.9.14
/builddir/build/BUILD/apron-0.9.15-build/apron-0.9.15/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
26namespace apron {
27
28
29/* ================================= */
30/* abstract1 */
31/* ================================= */
32
33
42class abstract1 : public use_malloc {
43
44protected:
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
56public:
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
145
152
161
168
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
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
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 & 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