APRONXX 0.9.14
/builddir/build/BUILD/apron-0.9.15-build/apron-0.9.15/apronxx/apxx_abstract0.hh
Go to the documentation of this file.
1/* -*- C++ -*-
2 * apxx_abstract0.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_ABSTRACT0_HH
17#define __APXX_ABSTRACT0_HH
18
19#include <string>
20#include "ap_abstract0.h"
21#include "apxx_linexpr0.hh"
22#include "apxx_lincons0.hh"
23#include "apxx_generator0.hh"
24#include "apxx_manager.hh"
25
26
27namespace apron {
29
30/* ================================= */
31/* abstract0 */
32/* ================================= */
33
78class abstract0 : public use_malloc {
79
80protected:
81
82 ap_abstract0_t* a;
83
85 abstract0(ap_abstract0_t* x);
86
88 static const abstract0 null;
89
90 friend class manager;
91
92public:
93
94
95 /* constructors */
96 /* ============ */
97
102 abstract0(manager &m, size_t intdim, size_t realdim, top x);
103
105 abstract0(manager &m, size_t intdim, size_t realdim, bottom x);
106
108 abstract0(manager &m, const abstract0& t);
109
114 abstract0(manager &m, size_t intdim, size_t realdim, const interval_array& x);
115
117 abstract0(manager &m, size_t intdim, size_t realdim, const lincons0_array& x);
118
120 abstract0(manager &m, size_t intdim, size_t realdim, const tcons0_array& x);
126 abstract0(const abstract0& t);
127
129
130
131 /* destructor */
132 /* ========== */
133
136
141 ~abstract0();
142
148 void free(manager& m);
149
151
152
153 /* assignments */
154 /* =========== */
155
158
163 abstract0& operator=(const abstract0& t);
164
170
176
184
190
196
201 abstract0& set(manager& m, const abstract0& x);
202
210 abstract0& set(manager& m, top t, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
211
219 abstract0& set(manager& m, bottom t, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
220
228 abstract0& set(manager& m, const interval_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
229
237 abstract0& set(manager& m, const lincons0_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
238
246 abstract0& set(manager& m, const tcons0_array& x, size_t intdim = AP_DIM_MAX, size_t realdim = AP_DIM_MAX);
247
248
251
252 /* representation */
253 /* ============== */
254
263
269
274 abstract0& approximate(manager& m, int algorithm);
277
278
279 /* printing */
280 /* ======== */
284
286 void print(manager& m, char** name_of_dim=NULL, FILE* stream=stdout) const;
289 friend void printdiff(manager& m, const abstract0& x, const abstract0& y, char** name_of_dim, FILE* stream);
290
292 void dump(manager& m, FILE* stream=stdout) const;
295 friend std::ostream& operator<< (std::ostream& os, const abstract0& s);
296
298
299
300 /* serialisation */
301 /* ============= */
302
313 std::string* serialize(manager& m) const;
324 friend abstract0& deserialize(manager& m, abstract0& dst, const std::string& s, size_t* eaten);
325
327
328
329 /* access */
330 /* ====== */
331
336 manager get_manager() const;
337
339 ap_dimension_t get_dimension(manager& m) const;
340
347 size_t size(manager& m) const;
348
350
351
352 /* predicates */
353 /* ========== */
354
357
359 bool is_bottom(manager& m) const;
362 bool is_top(manager& m) const;
363
365 bool is_eq(manager& m, const abstract0& x) const;
366
368 bool is_leq(manager& m, const abstract0& x) const;
369
371 bool sat(manager& m, const lincons0& l) const;
372
374 bool sat(manager& m, const tcons0& l) const;
375
379 bool sat(manager& m, ap_dim_t dim, const interval& i) const;
380
382 bool is_dimension_unconstrained(manager& m, ap_dim_t dim) const;
383
388 friend bool operator== (const abstract0& x, const abstract0& y);
389
394 friend bool operator!= (const abstract0& x, const abstract0& y);
400 friend bool operator<= (const abstract0& x, const abstract0& y);
401
406 friend bool operator>= (const abstract0& x, const abstract0& y);
407
412 friend bool operator> (const abstract0& x, const abstract0& y);
413
418 friend bool operator< (const abstract0& x, const abstract0& y);
419
420
421
422 /* Properties */
423 /* ========== */
424
427
429 interval bound(manager& m, const linexpr0& l) const;
430
432 interval bound(manager& m, const texpr0& l) const;
433
435 interval bound(manager& m, ap_dim_t d) const;
436
438 interval_array to_box(manager& m) const;
444
457
458 /* Meet */
459 /* ==== */
460
463
469
474 friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);
475
480 friend abstract0& meet(manager& m, abstract0& dst, const std::vector<const abstract0*>& x);
481
486 friend abstract0& meet(manager& m, abstract0& dst, size_t size, const abstract0 * const x[]);
487
493
498 friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const lincons0_array& y);
499
504 abstract0& meet(manager& m, const tcons0_array& y);
505
510 friend abstract0& meet(manager& m, abstract0& dst, const abstract0& x, const tcons0_array& y);
511
520
521
529
537
539
540
542
543 /* Join */
544 /* ==== */
545
548
553 abstract0& join(manager& m, const abstract0& y);
559 friend abstract0& join(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);
560
565 friend abstract0& join(manager& m, abstract0& dst, const std::vector<const abstract0*>& x);
566
571 friend abstract0& join(manager& m, abstract0& dst, size_t size, const abstract0 * const x[]);
572
580
587 friend abstract0& add_rays(manager& m, abstract0& dst, const abstract0& x, const generator0_array& y);
588
595 abstract0& operator+=(const abstract0& y);
606
608
609
610 /* Assignments */
611 /* =========== */
612
615
623 abstract0& assign(manager& m, ap_dim_t dim, const linexpr0& l, const abstract0& inter = null);
634 abstract0& assign(manager& m, size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter = null);
635
636
647 abstract0& assign(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter = null);
648
656 friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const linexpr0& l, const abstract0& inter);
657
667 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);
668
679 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);
681
682
683
691 abstract0& assign(manager& m, ap_dim_t dim, const texpr0& l, const abstract0& inter = null);
692
702 abstract0& assign(manager& m, size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter = null);
703
704
715 abstract0& assign(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter = null);
724 friend abstract0& assign(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const texpr0& l, const abstract0& inter);
725
735 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);
736
747 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);
750
751
752 /* Substitutions */
753 /* ============== */
754
757
765 abstract0& substitute(manager& m, ap_dim_t dim, const linexpr0& l, const abstract0& inter = null);
766
776 abstract0& substitute(manager& m, size_t size, const ap_dim_t dim[], const linexpr0 * const l[], const abstract0& inter = null);
777
778
789 abstract0& substitute(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const linexpr0*>& l, const abstract0& inter = null);
790
798 friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const linexpr0& l, const abstract0& inter);
799
809 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);
810
821 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);
822
823
824
825
833 abstract0& substitute(manager& m, ap_dim_t dim, const texpr0& l, const abstract0& inter = null);
834
844 abstract0& substitute(manager& m, size_t size, const ap_dim_t dim[], const texpr0 * const l[], const abstract0& inter = null);
845
846
857 abstract0& substitute(manager& m, const std::vector<ap_dim_t>& dim, const std::vector<const texpr0*>& l, const abstract0& inter = null);
858
866 friend abstract0& substitute(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, const texpr0& l, const abstract0& inter);
867
877 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);
878
889 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);
890
892
893
894
895 /* Projection */
896 /* ========== */
897
900
907 abstract0& forget(manager& m, ap_dim_t dim, bool project = false);
908
915 abstract0& forget(manager& m, size_t size, const ap_dim_t dim[], bool project = false);
916
923 abstract0& forget(manager& m, const std::vector<ap_dim_t> dim, bool project = false);
924
931 friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, bool project);
932
940 friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, size_t size, const ap_dim_t dim[], bool project);
941
948 friend abstract0& forget(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t> dim, bool project);
949
951
952
953 /* Change of dimension */
954 /* =================== */
955
958
959
966 abstract0& add_dimensions(manager& m, const dimchange& d, bool project = false);
967
973
979
980
987 friend abstract0& add_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimchange& d, bool project);
988
993 friend abstract0& remove_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimchange& d);
994
999 friend abstract0& permute_dimensions(manager& m, abstract0& dst, const abstract0& src, const dimperm& d);
1000
1002
1003
1004 /* Expansion and folding */
1005 /* ===================== */
1006
1009
1016 abstract0& expand(manager& m, ap_dim_t dim, size_t n = 1);
1017
1024 friend abstract0& expand(manager& m, abstract0& dst, const abstract0& src, ap_dim_t dim, size_t n);
1025
1033 abstract0& fold(manager& m, size_t size, const ap_dim_t dim[]);
1034
1042 abstract0& fold(manager& m, const std::vector<ap_dim_t>& dim);
1043
1051 friend abstract0& fold(manager& m, abstract0& dst, const abstract0& src, size_t size, const ap_dim_t dim[]);
1052
1060 friend abstract0& fold(manager& m, abstract0& dst, const abstract0& src, const std::vector<ap_dim_t>& dim);
1063
1064
1065 /* Widenings */
1066 /* ========= */
1067
1070
1077 friend abstract0& widening(manager& m, abstract0& dst, const abstract0& x, const abstract0& y);
1078
1085 friend abstract0& widening(manager& m, abstract0& dst, const abstract0& x, const abstract0& y, const lincons0_array& l);
1086
1088
1089
1090 /* Closure */
1091 /* ======= */
1092
1095
1096
1102
1107 friend abstract0& closure(manager& m, abstract0& dst, const abstract0& src);
1108
1110
1111
1112
1113 /* C-level compatibility */
1114 /* ===================== */
1115
1118
1120 ap_abstract0_t* get_ap_abstract0_t();
1121
1123 const ap_abstract0_t* get_ap_abstract0_t() const;
1124
1126
1127};
1129#include "apxx_abstract0_inline.hh"
1130
1131}
1132
1133#endif /* __APXX_ABSTRACT0_HH */
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.
Definition apxx_abstract0.hh:410
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition apxx_abstract0.hh:476
abstract0 & operator+=(const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition apxx_abstract0.hh:665
abstract0 & set(manager &m, const abstract0 &x)
Replaces *this with a copy of x.
Definition apxx_abstract0.hh:168
friend abstract0 & add_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d, bool project)
Copies src into dst and adds some dimensions.
Definition apxx_abstract0.hh:1038
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.
Definition apxx_abstract0.hh:281
friend abstract0 & add_rays(manager &m, abstract0 &dst, const abstract0 &x, const generator0_array &y)
Replaces dst with x with some rays added.
Definition apxx_abstract0.hh:645
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.hh:484
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.
Definition apxx_abstract0.hh:984
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.
Definition apxx_abstract0.hh:1084
void free(manager &m)
Destroys the abstract element using the given manager.
Definition apxx_abstract0.hh:90
abstract0 & operator=(const interval_array &x)
Assigns a box to *this.
Definition apxx_abstract0.hh:131
friend bool operator<=(const abstract0 &x, const abstract0 &y)
Whether x is included within y (set-wise).
Definition apxx_abstract0.hh:422
friend abstract0 & remove_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d)
Copies src into dst and removes some dimensions.
Definition apxx_abstract0.hh:1050
friend bool operator>(const abstract0 &x, const abstract0 &y)
Whether x strictly contains y (set-wise).
Definition apxx_abstract0.hh:434
friend abstract0 & join(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the join of x and y.
Definition apxx_abstract0.hh:561
friend bool operator<(const abstract0 &x, const abstract0 &y)
Whether x is strictly included within y (set-wise).
Definition apxx_abstract0.hh:439
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.
Definition apxx_abstract0.hh:860
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.hh:28
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.hh:492
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the meet of x and y.
Definition apxx_abstract0.hh:519
abstract0 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition apxx_abstract0.hh:264
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.hh:367
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition apxx_abstract0.hh:329
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_abstract0.hh:1173
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
Assignment of linear expression.
Definition apxx_abstract0.hh:729
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition apxx_abstract0.hh:287
abstract0 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition apxx_abstract0.hh:257
abstract0 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition apxx_abstract0.hh:250
bool is_leq(manager &m, const abstract0 &x) const
Whether *this is included in x (set-wise).
Definition apxx_abstract0.hh:374
abstract0 & operator=(const abstract0 &t)
Assigns a copy of t to *this.
Definition apxx_abstract0.hh:100
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].
Definition apxx_abstract0.hh:1107
friend abstract0 & closure(manager &m, abstract0 &dst, const abstract0 &src)
Stores in dst the topological closure of src.
Definition apxx_abstract0.hh:1159
friend bool operator>=(const abstract0 &x, const abstract0 &y)
Whether x contains y (set-wise).
Definition apxx_abstract0.hh:429
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.
Definition apxx_abstract0.hh:314
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.hh:500
friend bool operator!=(const abstract0 &x, const abstract0 &y)
Whether x and y represent different sets.
Definition apxx_abstract0.hh:417
friend std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Prints in constraint form.
Definition apxx_abstract0.hh:293
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition apxx_abstract0.hh:305
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition apxx_abstract0.hh:341
friend abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Stores in dst the result of x widened with y.
Definition apxx_abstract0.hh:1128
bool sat(manager &m, const lincons0 &l) const
Whether all points in *this satisfy a linear constraint.
Definition apxx_abstract0.hh:381
bool is_top(manager &m) const
Whether *this represents the full space.
Definition apxx_abstract0.hh:360
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.hh:448
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.hh:402
void print(manager &m, char **name_of_dim=NULL, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition apxx_abstract0.hh:275
friend abstract0 & permute_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimperm &d)
Copies src into dst and permute some dimensions.
Definition apxx_abstract0.hh:1061
~abstract0()
Destroys the abstract element.
Definition apxx_abstract0.hh:84
abstract0 & operator*=(const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition apxx_abstract0.hh:658
ap_dimension_t get_dimension(manager &m) const
Returns the number of integer and real dimensions in the abstract element.
Definition apxx_abstract0.hh:334
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition apxx_abstract0.hh:353
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