APRONXX  0.9.12
/builddir/build/BUILD/apron-0.9.13/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 
27 namespace apron {
28 
29 
30 /* ================================= */
31 /* abstract0 */
32 /* ================================= */
33 
78 class abstract0 : public use_malloc {
79 
80 protected:
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 
92 public:
93 
94 
95  /* constructors */
96  /* ============ */
97 
100 
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);
121 
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 
169  abstract0& operator=(top t);
170 
176 
184 
190 
195  abstract0& operator=(const tcons0_array& x);
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 
250 
251 
252  /* representation */
253  /* ============== */
254 
257 
263 
269 
274  abstract0& approximate(manager& m, int algorithm);
275 
277 
278 
279  /* printing */
280  /* ======== */
281 
284 
286  void print(manager& m, char** name_of_dim=NULL, FILE* stream=stdout) const;
287 
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;
293 
295  friend std::ostream& operator<< (std::ostream& os, const abstract0& s);
296 
298 
299 
300  /* serialisation */
301  /* ============= */
302 
305 
313  std::string* serialize(manager& m) const;
314 
324  friend abstract0& deserialize(manager& m, abstract0& dst, const std::string& s, size_t* eaten);
325 
327 
328 
329  /* access */
330  /* ====== */
331 
334 
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;
360 
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);
395 
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;
439 
444 
449 
454 
456 
457 
458  /* Meet */
459  /* ==== */
460 
463 
468  abstract0& meet(manager& m, const abstract0& y);
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 
492  abstract0& meet(manager& m, const lincons0_array& y);
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 
512 
519  abstract0& operator*=(const abstract0& y);
520 
521 
529 
536  abstract0& operator*=(const tcons0_array& y);
537 
539 
540 
541 
542 
543  /* Join */
544  /* ==== */
545 
548 
553  abstract0& join(manager& m, const abstract0& y);
554 
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);
596 
606 
608 
609 
610  /* Assignments */
611  /* =========== */
612 
615 
623  abstract0& assign(manager& m, ap_dim_t dim, const linexpr0& l, const abstract0& inter = null);
624 
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);
680 
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);
716 
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);
748 
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);
1061 
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 
1101  abstract0& closure(manager& m);
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 };
1128 
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 abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y, const lincons0_array &l)
Stores in dst the result of x widened with y, using some widening thresholds.
friend bool operator==(const abstract0 &x, const abstract0 &y)
Whether x and y represent the same set.
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition: apxx_abstract0_inline.hh:475
abstract0 & expand(manager &m, ap_dim_t dim, size_t n=1)
Duplicates dimension dim into n copies in *this (modified in-place).
abstract0 & operator+=(const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract0_inline.hh:664
friend abstract0 & add_rays(manager &m, abstract0 &dst, const abstract0 &x, const generator0_array &y)
Replaces dst with x with some rays added.
friend abstract0 & closure(manager &m, abstract0 &dst, const abstract0 &src)
Stores in dst the topological closure of src.
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const lincons0_array &y)
Replaces dst with the meet of x and some linear constraints.
friend abstract0 & permute_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimperm &d)
Copies src into dst and permute some dimensions.
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter)
Parallel assignment of linear expressions.
friend std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Prints in constraint form.
abstract0 & permute_dimensions(manager &m, const dimperm &d)
Permutes some dimensions in *this.
Definition: apxx_abstract0_inline.hh:1029
friend abstract0 & fold(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim)
Replaces dst with a copy of src and folds all dimensions in dims.
abstract0 & substitute(manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter=null)
In-place parallel substitution (backward assignment) of arbitrary expressions.
abstract0 & assign(manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter=null)
In-place parallel assignment of linear expressions.
friend abstract0 & forget(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, bool project)
Stores in dst the result of forgetting the value of dimension dim in src.
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const texpr0 &l, const abstract0 &inter)
Substitution (backward assignment) of arbitrary expression.
abstract0 & set(manager &m, bottom t, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
Replaces *this with the empty set.
lincons0_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition: apxx_abstract0_inline.hh:483
abstract0 & set(manager &m, top t, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
Replaces *this with the full space.
friend abstract0 & fold(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[])
Replaces dst with a copy of src and folds dimensions dims[0] to dim[size-1].
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter)
Parallel assignment of arbitrary expressions.
void free(manager &m)
Destroys the abstract element using the given manager.
Definition: apxx_abstract0_inline.hh:89
friend abstract0 & remove_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d)
Copies src into dst and removes some dimensions.
friend bool operator<=(const abstract0 &x, const abstract0 &y)
Whether x is included within y (set-wise).
abstract0 & join(manager &m, const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract0_inline.hh:553
friend bool operator>(const abstract0 &x, const abstract0 &y)
Whether x strictly contains y (set-wise).
friend bool operator<(const abstract0 &x, const abstract0 &y)
Whether x is strictly included within y (set-wise).
friend abstract0 & join(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the join of x and y.
abstract0 & substitute(manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
In-place substitution (backward assignment) of linear expression.
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
Substitution (backward assignment) of linear expression.
friend abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Stores in dst the result of x widened with y.
abstract0 & substitute(manager &m, ap_dim_t dim, const texpr0 &l, const abstract0 &inter=null)
In-place substitution (backward assignment) of arbitrary expression.
abstract0(ap_abstract0_t *x)
Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object.
Definition: apxx_abstract0_inline.hh:27
abstract0 & fold(manager &m, size_t size, const ap_dim_t dim[])
Folds dimensions dim[0] to dim[size-1] in *this (modified in-place).
Definition: apxx_abstract0_inline.hh:1092
friend abstract0 & add_dimensions(manager &m, abstract0 &dst, const abstract0 &src, const dimchange &d, bool project)
Copies src into dst and adds some dimensions.
tcons0_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition: apxx_abstract0_inline.hh:491
abstract0 & meet(manager &m, const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract0_inline.hh:511
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter)
Parallel assignment of linear expressions.
abstract0 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition: apxx_abstract0_inline.hh:263
ap_abstract0_t * a
Pointer managed by APRON.
Definition: apxx_abstract0.hh:82
bool is_eq(manager &m, const abstract0 &x) const
Whether *this and x represent the same set.
Definition: apxx_abstract0_inline.hh:366
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition: apxx_abstract0_inline.hh:328
abstract0 & set(manager &m, const abstract0 &x)
Replaces *this with a copy of x.
abstract0 & set(manager &m, const tcons0_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
Replaces *this with a conjunction of arbitrary constraints.
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_abstract0_inline.hh:1172
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition: apxx_abstract0_inline.hh:286
abstract0 & remove_dimensions(manager &m, const dimchange &d)
Removes some dimensions from *this.
Definition: apxx_abstract0_inline.hh:1021
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const tcons0_array &y)
Replaces dst with the meet of x and some arbitrary constraints.
abstract0 & assign(manager &m, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter=null)
In-place parallel assignment of linear expressions.
abstract0 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition: apxx_abstract0_inline.hh:256
friend abstract0 & join(manager &m, abstract0 &dst, size_t size, const abstract0 *const x[])
Replaces dst with the join of all size abstract elements in x.
abstract0 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition: apxx_abstract0_inline.hh:249
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const texpr0 &l, const abstract0 &inter)
Assignment of arbitrary expression.
bool is_leq(manager &m, const abstract0 &x) const
Whether *this is included in x (set-wise).
Definition: apxx_abstract0_inline.hh:373
abstract0 & operator=(const abstract0 &t)
Assigns a copy of t to *this.
Definition: apxx_abstract0_inline.hh:99
abstract0 & substitute(manager &m, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter=null)
In-place parallel substitution (backward assignment) of linear expressions.
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter)
Parallel assignment of arbitrary expressions.
abstract0 & assign(manager &m, ap_dim_t dim, const texpr0 &l, const abstract0 &inter=null)
In-place assignment of arbitrary expression.
abstract0 & closure(manager &m)
Replaces *this with its topological closure.
Definition: apxx_abstract0_inline.hh:1151
friend bool operator>=(const abstract0 &x, const abstract0 &y)
Whether x contains y (set-wise).
abstract0 & assign(manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter=null)
In-place parallel assignment of arbitrary expressions.
abstract0 & forget(manager &m, const std::vector< ap_dim_t > dim, bool project=false)
Forgets about the value of all the dimensions in dim in *this.
generator0_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition: apxx_abstract0_inline.hh:499
friend abstract0 & forget(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], bool project)
Stores in dst the result of forgetting the value of dimensions dim[0] to dim[size-1] in src.
friend bool operator!=(const abstract0 &x, const abstract0 &y)
Whether x and y represent different sets.
abstract0 & forget(manager &m, ap_dim_t dim, bool project=false)
Forgets about the value of dimension dim in *this.
abstract0 & add_rays(manager &m, const generator0_array &y)
Adds some rays to *this (modified in-place).
Definition: apxx_abstract0_inline.hh:636
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter)
Parallel substitution (backward assignment) of linear expressions.
abstract0 & assign(manager &m, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter=null)
In-place parallel assignment of arbitrary expressions.
friend abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter)
Assignment of linear expression.
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter)
Parallel substitution (backward assignment) of arbitrary expressions.
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition: apxx_abstract0_inline.hh:304
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.
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition: apxx_abstract0_inline.hh:340
abstract0 & forget(manager &m, size_t size, const ap_dim_t dim[], bool project=false)
Forgets about the value of dimensions dims[0] to dims[size-1] in *this.
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > &dim, const std::vector< const texpr0 * > &l, const abstract0 &inter)
Parallel substitution (backward assignment) of arbitrary expressions.
bool sat(manager &m, const lincons0 &l) const
Whether all points in *this satisfy a linear constraint.
Definition: apxx_abstract0_inline.hh:380
bool is_top(manager &m) const
Whether *this represents the full space.
Definition: apxx_abstract0_inline.hh:359
friend abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Replaces dst with the meet of x and y.
abstract0 & substitute(manager &m, size_t size, const ap_dim_t dim[], const texpr0 *const l[], const abstract0 &inter=null)
In-place parallel substitution (backward assignment) of arbitrary expressions.
interval bound(manager &m, const linexpr0 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element.
Definition: apxx_abstract0_inline.hh:447
abstract0 & add_dimensions(manager &m, const dimchange &d, bool project=false)
Adds some dimensions to *this.
abstract0 & set(manager &m, const interval_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
Replaces *this with a box.
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.
bool is_dimension_unconstrained(manager &m, ap_dim_t dim) const
Whether the points in *this are unbounded in the given dimension.
Definition: apxx_abstract0_inline.hh:401
friend abstract0 & meet(manager &m, abstract0 &dst, size_t size, const abstract0 *const x[])
Replaces dst with the meet of all size abstract elements in x.
abstract0 & substitute(manager &m, const std::vector< ap_dim_t > &dim, const std::vector< const linexpr0 * > &l, const abstract0 &inter=null)
In-place parallel substitution (backward assignment) of linear expressions.
friend abstract0 & join(manager &m, abstract0 &dst, const std::vector< const abstract0 * > &x)
Replaces dst with the join of all abstract elements in x.
void print(manager &m, char **name_of_dim=NULL, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition: apxx_abstract0_inline.hh:274
friend abstract0 & meet(manager &m, abstract0 &dst, const std::vector< const abstract0 * > &x)
Replaces dst with the meet of all abstract elements in x.
abstract0 & set(manager &m, const lincons0_array &x, size_t intdim=AP_DIM_MAX, size_t realdim=AP_DIM_MAX)
Replaces *this with a conjunction of linear constraints.
~abstract0()
Destroys the abstract element.
Definition: apxx_abstract0_inline.hh:83
friend abstract0 & forget(manager &m, abstract0 &dst, const abstract0 &src, const std::vector< ap_dim_t > dim, bool project)
Stores in dst the result of forgetting the value of all the dimensions in dim in src.
abstract0 & operator*=(const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract0_inline.hh:657
ap_dimension_t get_dimension(manager &m) const
Returns the number of integer and real dimensions in the abstract element.
Definition: apxx_abstract0_inline.hh:333
abstract0 & assign(manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
In-place assignment of linear expression.
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition: apxx_abstract0_inline.hh:352
friend abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[], const linexpr0 *const l[], const abstract0 &inter)
Parallel substitution (backward assignment) of linear expressions.
friend void printdiff(manager &m, const abstract0 &x, const abstract0 &y, char **name_of_dim, FILE *stream)
Pretty-printing the difference between x and y to a C stream.
Represents a dimension (i.e., variable by index) in an expression tree.
Definition: apxx_texpr0.hh:33
Dimension change object (ap_dimchange_t wrapper).
Definition: apxx_dimension.hh:102
Dimension permutation object (ap_dimperm_t wrapper).
Definition: apxx_dimension.hh:292
Array of generators (ap_generator0_array_t wrapper).
Definition: apxx_generator0.hh:214
array of interval(s).
Definition: apxx_interval.hh:302
Interval (ap_interval_t wrapper).
Definition: apxx_interval.hh:47
Array of linear constraints (ap_lincons0_array_t wrapper).
Definition: apxx_lincons0.hh:341
Level 0 linear constraint (ap_lincons0_t wrapper).
Definition: apxx_lincons0.hh:43
Level 0 linear expression (ap_linexpr0_t wrapper).
Definition: apxx_linexpr0.hh:44
Library manager (ap_manager_t wrapper).
Definition: apxx_manager.hh:137
Array of arbitrary constraints (ap_tcons0_array_t wrapper).
Definition: apxx_tcons0.hh:350
Level 0 arbitrary constraint (ap_tcons0_t wrapper).
Definition: apxx_tcons0.hh:47
Level 0 arbitrary expression tree (ap_texpr0_t wrapper).
Definition: apxx_texpr0.hh:92
Definition: apxx_abstract0.hh:27
Empty interval or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:33
Full interval (]-oo,+oo[) or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:27
Inherited by most wrappers to map new and delete to malloc and free.
Definition: apxx_scalar.hh:69