APRONXX 0.9.14
/builddir/build/BUILD/apron-0.9.15-build/apron-0.9.15/apronxx/apxx_abstract1_inline.hh
Go to the documentation of this file.
1/* -*- C++ -*-
2 * apxx_abstract1_inline.hh
3 *
4 * APRON Library / C++ inline functions
5 *
6 * DO NOT INCLUDE THIS FILE DIRECTLY
7 *
8 * Copyright (C) Antoine Mine' 2007
9 *
10 */
11/* This file is part of the APRON Library, released under LGPL license
12 with an exception allowing the redistribution of statically linked
13 executables.
14
15 Please read the COPYING file packaged in the distribution.
16*/
17
18
19/* ================================= */
20/* abstract1 */
21/* ================================= */
22
23
24/* constructors */
25/* ============ */
26
27inline abstract1::abstract1(ap_abstract1_t x) : a(x)
28{}
29
31{
32 a = ap_abstract1_top(m.get_ap_manager_t(),
33 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
34 m.raise("apron::abstract1::abstract1(manager &, const environment&, top)",a);
35}
36
38{
39 a = ap_abstract1_bottom(m.get_ap_manager_t(),
40 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
41 m.raise("apron::abstract1::abstract1(manager &, const environment&, bottom)",a);
42}
43
45{
46 a = ap_abstract1_copy(m.get_ap_manager_t(), const_cast<ap_abstract1_t*>(&t.a));
47 m.raise("apron::abstract1::abstract1(manager &, const abstract1&)",a);
48}
49
50inline abstract1::abstract1(manager &m, const environment& e, const abstract0& t)
51{
52 a.env = ap_environment_copy(const_cast<ap_environment_t*>(e.get_ap_environment_t()));
53 a.abstract0 = ap_abstract0_copy(m.get_ap_manager_t(),
54 const_cast<ap_abstract0_t*>(t.get_ap_abstract0_t()));
55 m.raise("apron::abstract1::abstract1(manager &, const abstract1&)",a);
56}
57
58inline abstract1::abstract1(manager &m, const environment& e, const var v[], const interval_array& x)
59{
60 a = ap_abstract1_of_box(m.get_ap_manager_t(),
61 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
62 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
63 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()),
64 x.size());
65 m.raise("apron::abstract1::abstract1(manager &, const environment&, const var[], const interval_array&)",a);
66}
67
68inline abstract1::abstract1(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x)
69{
70 if (v.size()!=x.size())
71 throw std::invalid_argument("apron::abstract1::abstract1(manager &, const environment&, const std::vector<var>&, const interval_array&): different array sizes");
72 ap_var_t vv[v.size()];
73 for (size_t i=0;i<v.size();i++) vv[i] = v[i].get_ap_var_t();
74 a = ap_abstract1_of_box(m.get_ap_manager_t(),
75 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
76 vv,
77 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()),
78 v.size());
79 m.raise("apron::abstract1::abstract1(manager &, const environment&, const std::vector<var>&, const interval_array&)",a);
80}
81
83{
84 a = ap_abstract1_of_lincons_array(m.get_ap_manager_t(),
85 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
86 const_cast<ap_lincons1_array_t*>(x.get_ap_lincons1_array_t()));
87 m.raise("apron::abstract1::abstract1(manager &, const lincons1_array&)",a);
88}
89
91{
92 a = ap_abstract1_of_tcons_array(m.get_ap_manager_t(),
93 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
94 const_cast<ap_tcons1_array_t*>(x.get_ap_tcons1_array_t()));
95 m.raise("apron::abstract1::abstract1(manager &, const tcons1_array&)",a);
96}
97
99{
100 a = ap_abstract1_copy(t.a.abstract0->man, const_cast<ap_abstract1_t*>(&t.a));
101 manager::raise(a.abstract0->man, "apron::abstract1::abstract1(abstract1&)",a);
102}
103
104
105/* destructor */
106/* ========== */
107
109{
110 if (a.abstract0) ap_abstract1_clear(a.abstract0->man, &a);
111}
112
113
115{
116 if (a.abstract0) ap_abstract1_clear(m.get_ap_manager_t(), &a);
117}
118
119
120
121/* assignments */
122/* =========== */
123
125{
126 if (&t!=this) {
127 ap_abstract1_t r = ap_abstract1_copy(a.abstract0->man,
128 const_cast<ap_abstract1_t*>(&t.a));
129 manager::raise(a.abstract0->man, "apron::abstract1::operator=(const abstract1&)",r);
130 ap_abstract1_clear(a.abstract0->man, &a);
131 a = r;
132 }
133 return *this;
134}
135
137{
138 ap_abstract1_t r = ap_abstract1_top(a.abstract0->man, a.env);
139 manager::raise(a.abstract0->man, "apron::abstract1::operator=(top)",r);
140 ap_abstract1_clear(a.abstract0->man, &a);
141 a = r;
142 return *this;
143}
144
146{
147 ap_abstract1_t r = ap_abstract1_bottom(a.abstract0->man, a.env);
148 manager::raise(a.abstract0->man, "apron::abstract1::operator=(bottom)",r);
149 ap_abstract1_clear(a.abstract0->man, &a);
150 a = r;
151 return *this;
152}
153
155{
156 ap_dimension_t d = ap_abstract0_dimension(a.abstract0->man, a.abstract0);
157 if (x.size()<d.intdim+d.realdim)
158 throw std::invalid_argument("apron::abstract1::operator=(const interval_array&) array too short");
159 ap_abstract0_t* r = ap_abstract0_of_box(a.abstract0->man, d.intdim, d.realdim,
160 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()));
161 manager::raise(a.abstract0->man, "apron::abstract1::operator=(const interval_array&)",r);
162 ap_abstract0_free(a.abstract0->man, a.abstract0);
163 a.abstract0 = r;
164 return *this;
165}
166
168{
169 ap_abstract1_t r =
170 ap_abstract1_of_lincons_array(a.abstract0->man,
171 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
172 const_cast<ap_lincons1_array_t*>(x.get_ap_lincons1_array_t()));
173 manager::raise(a.abstract0->man, "apron::abstract1::operator=(const lincons1_array&)",r);
174 ap_abstract1_clear(a.abstract0->man, &a);
175 a = r;
176 return *this;
177}
178
180{
181 ap_abstract1_t r =
182 ap_abstract1_of_tcons_array(a.abstract0->man,
183 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
184 const_cast<ap_tcons1_array_t*>(x.get_ap_tcons1_array_t()));
185 manager::raise(a.abstract0->man, "apron::abstract1::operator=(const tcons1_array&)",r);
186 ap_abstract1_clear(a.abstract0->man, &a);
187 a = r;
188 return *this;
189}
190
191
193{
194 if (&x!=this) {
195 ap_abstract1_t r = ap_abstract1_copy(m.get_ap_manager_t(),
196 const_cast<ap_abstract1_t*>(&x.a));
197 m.raise("apron::abstract1::set(manager&, abstract1&)",r);
198 ap_abstract1_clear(m.get_ap_manager_t(), &a);
199 a = r;
200
201 }
202 return *this;
203}
204
206{
207 ap_abstract1_t r = ap_abstract1_top(m.get_ap_manager_t(), a.env);
208 m.raise("apron::abstract1::set(manager&, top)",r);
209 ap_abstract1_clear(m.get_ap_manager_t(), &a);
210 a = r;
211 return *this;
212}
213
215{
216 ap_abstract1_t r = ap_abstract1_top(m.get_ap_manager_t(),
217 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
218 m.raise("apron::abstract1::set(manager&, const environment&, top)",r);
219 ap_abstract1_clear(m.get_ap_manager_t(), &a);
220 a = r;
221 return *this;
222}
223
225{
226 ap_abstract1_t r = ap_abstract1_bottom(m.get_ap_manager_t(), a.env);
227 m.raise("apron::abstract1::set(manager&, bottom)",r);
228 ap_abstract1_clear(m.get_ap_manager_t(), &a);
229 a = r;
230 return *this;
231}
232
234{
235 ap_abstract1_t r = ap_abstract1_bottom(m.get_ap_manager_t(),
236 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
237 m.raise("apron::abstract1::set(manager&, const environment&, bottom)",r);
238 ap_abstract1_clear(m.get_ap_manager_t(), &a);
239 a = r;
240 return *this;
241}
242
244{
245 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(), a.abstract0);
246 if (x.size()<d.intdim+d.realdim)
247 throw std::invalid_argument("apron::abstract1::set(manager&, const interval_array&) array too short");
248 ap_abstract0_t* r = ap_abstract0_of_box(m.get_ap_manager_t(), d.intdim, d.realdim,
249 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()));
250 m.raise("apron::abstract1::operator=(const interval_array&)",r);
251 ap_abstract0_free(m.get_ap_manager_t(), a.abstract0);
252 a.abstract0 = r;
253 return *this;
254}
255
256
257inline abstract1& abstract1::set(manager &m, const environment& e, const var v[], const interval_array& x)
258{
259 ap_abstract1_t r =
260 ap_abstract1_of_box(m.get_ap_manager_t(),
261 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
262 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
263 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()),
264 x.size());
265 m.raise("apron::abstract1::set(manager &, const environment&, const var[], const interval_array&)",r);
266 ap_abstract1_clear(m.get_ap_manager_t(),&a);
267 a = r;
268 return *this;
269}
270
271inline abstract1& abstract1::set(manager &m, const environment& e, const std::vector<var>& v, const interval_array& x)
272{
273 if (v.size()!=x.size())
274 throw std::invalid_argument("apron::abstract1::abstract1(manager &, const environment&, const std::vector<var>&, const interval_array&): different array sizes");
275 ap_var_t vv[v.size()];
276 for (size_t i=0;i<v.size();i++) vv[i] = v[i].get_ap_var_t();
277 ap_abstract1_t r =
278 ap_abstract1_of_box(m.get_ap_manager_t(),
279 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
280 vv,
281 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()),
282 v.size());
283 m.raise("apron::abstract1::set(manager &, const environment&, const std::vector<var>&, const interval_array&)",r);
284 ap_abstract1_clear(m.get_ap_manager_t(), &a);
285 a = r;
286 return *this;
287}
288
290{
291 ap_abstract1_t r =
292 ap_abstract1_of_lincons_array(m.get_ap_manager_t(),
293 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
294 const_cast<ap_lincons1_array_t*>(x.get_ap_lincons1_array_t()));
295 m.raise("apron::abstract1::set(manager &, const lincons1_array&)",r);
296 ap_abstract1_clear(m.get_ap_manager_t(), &a);
297 a = r;
298 return *this;
299}
300
302{
303 ap_abstract1_t r =
304 ap_abstract1_of_tcons_array(m.get_ap_manager_t(),
305 const_cast<ap_environment_t*>(x.get_environment().get_ap_environment_t()),
306 const_cast<ap_tcons1_array_t*>(x.get_ap_tcons1_array_t()));
307 m.raise("apron::abstract1::set(manager &, const tcons1_array&)",r);
308 ap_abstract1_clear(m.get_ap_manager_t(), &a);
309 a = r;
310 return *this;
311}
312
313
314/* representation */
315/* ============== */
316
318{
319 ap_abstract1_minimize(m.get_ap_manager_t(), &a);
320 m.raise("apron::abstract1::minimize(manager &)");
321 return *this;
322}
323
325{
326 ap_abstract1_canonicalize(m.get_ap_manager_t(), &a);
327 m.raise("apron::abstract1::canonicalize(manager &)");
328 return *this;
329}
330
331inline abstract1& abstract1::approximate(manager& m, int algorithm)
332{
333 ap_abstract1_approximate(m.get_ap_manager_t(), &a, algorithm);
334 m.raise("apron::abstract1::approximate(manager &, int)");
335 return *this;
336}
337
338
339/* printing */
340/* ======== */
341
342inline void abstract1::print(manager& m, FILE* stream) const
343{
344 ap_abstract1_fprint(stream, m.get_ap_manager_t(), const_cast<ap_abstract1_t*>(&a));
345 m.raise("apron::abstract1::print(manager&, FILE*)");
346}
347
348inline void printdiff(manager& m, const abstract1& x, const abstract1& y, FILE* stream = stdout)
349{
350 ap_abstract1_fprintdiff(stream, m.get_ap_manager_t(),
351 const_cast<ap_abstract1_t*>(&x.a),
352 const_cast<ap_abstract1_t*>(&y.a));
353 m.raise("apron::printdiff(manager&, const abstract1&, const abstract1&, FILE*)");
354}
355
356inline void abstract1::dump(manager& m, FILE* stream) const
357{
358 ap_abstract1_fdump(stream, m.get_ap_manager_t(), const_cast<ap_abstract1_t*>(&a));
359 m.raise("apron::abstract1::dump(manager&, FILE*)");
360}
361
362inline std::ostream& operator<< (std::ostream& os, const abstract1& s)
363{
364 manager m = s.get_manager();
365 if (s.is_bottom(m)) return os << "bottom";
366 if (s.is_top(m)) return os << "top";
367 return os << s.to_lincons_array(m);
368}
369
370
371/* serialisation */
372/* ============= */
373
374inline std::string* abstract1::serialize(manager& m) const
375{
376 ap_membuf_t x = ap_abstract1_serialize_raw(m.get_ap_manager_t(),
377 const_cast<ap_abstract1_t*>(&a));
378 m.raise("apron::abstract1::serialize_raw(manager&)");
379 std::string* s = new std::string((char*)x.ptr, x.size);
380 ::free(x.ptr);
381 return s;
382}
383
384inline abstract1& deserialize(manager& m, abstract1& dst, const std::string& s, size_t* eaten = NULL)
385{
386 size_t x = s.size();
387 ap_abstract1_t r =
388 ap_abstract1_deserialize_raw(m.get_ap_manager_t(), const_cast<char*>(s.data()), &x);
389 m.raise("apron::deserialize_raw(manager&, abstract1&, const std::string&, size_t*)",r);
390 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
391 dst.a = r;
392 if (eaten) *eaten = x;
393 return dst;
394}
395
396
397/* access */
398/* ====== */
399
401{
402 return ap_manager_copy(ap_abstract0_manager(const_cast<ap_abstract0_t*>(a.abstract0)));
403}
404
406{
407 return ap_environment_copy(const_cast<ap_environment_t*>(a.env));
408}
409
411{
412 return reinterpret_cast<abstract0&>(a.abstract0);
413}
414
416{
417 return reinterpret_cast<const abstract0&>(a.abstract0);
418}
419
420inline size_t abstract1::size(manager& m) const
421{
422 size_t sz = ap_abstract1_size(m.get_ap_manager_t(),
423 const_cast<ap_abstract1_t*>(&a));
424 m.raise("apron::abstract1::get_size(manager&)");
425 return sz;
426}
427
428
429/* predicates */
430/* ========== */
431
432
433
434inline bool abstract1::is_bottom(manager& m) const
435{
436 bool r = ap_abstract1_is_bottom(m.get_ap_manager_t(),
437 const_cast<ap_abstract1_t*>(&a));
438 m.raise("apron::abstract1::is_bottom(manager&)");
439 return r;
440}
441
442inline bool abstract1::is_top(manager& m) const
443{
444 bool r = ap_abstract1_is_top(m.get_ap_manager_t(),
445 const_cast<ap_abstract1_t*>(&a));
446 m.raise("apron::abstract1::is_top(manager&)");
447 return r;
448}
449
450inline bool abstract1::is_eq(manager& m, const abstract1& x) const
451{
452 bool r = ap_abstract1_is_eq(m.get_ap_manager_t(),
453 const_cast<ap_abstract1_t*>(&a),
454 const_cast<ap_abstract1_t*>(&x.a));
455 m.raise("apron::abstract1::is_eq(manager&, const abstract&)");
456 return r;
457}
458
459inline bool abstract1::is_leq(manager& m, const abstract1& x) const
460{
461 bool r = ap_abstract1_is_leq(m.get_ap_manager_t(),
462 const_cast<ap_abstract1_t*>(&a),
463 const_cast<ap_abstract1_t*>(&x.a));
464 m.raise("apron::abstract1::is_leq(manager&, const abstract&)");
465 return r;
466}
467
468inline bool abstract1::sat(manager& m, const lincons1& l) const
469{
470 bool r = ap_abstract1_sat_lincons(m.get_ap_manager_t(),
471 const_cast<ap_abstract1_t*>(&a),
472 const_cast<ap_lincons1_t*>(l.get_ap_lincons1_t()));
473 m.raise("apron::abstract1::sat(manager&, const lincons1&)");
474 return r;
475}
476
477inline bool abstract1::sat(manager& m, const tcons1& l) const
478{
479 bool r = ap_abstract1_sat_tcons(m.get_ap_manager_t(),
480 const_cast<ap_abstract1_t*>(&a),
481 const_cast<ap_tcons1_t*>(l.get_ap_tcons1_t()));
482 m.raise("apron::abstract1::sat(manager&, const tcons1&)");
483 return r;
484}
485
486inline bool abstract1::sat(manager& m, const var& v, const interval& i) const
487{
488 bool r = ap_abstract1_sat_interval(m.get_ap_manager_t(),
489 const_cast<ap_abstract1_t*>(&a),
490 v.get_ap_var_t(),
491 const_cast<ap_interval_t*>(i.get_ap_interval_t()));
492 m.raise("apron::abstract1::sat(manager&, const var&, const interval&)");
493 return r;
494}
495
496inline bool abstract1::is_variable_unconstrained(manager& m, const var& v) const
497{
498 bool r = ap_abstract1_is_variable_unconstrained(m.get_ap_manager_t(),
499 const_cast<ap_abstract1_t*>(&a),
500 v.get_ap_var_t());
501 m.raise("apron::abstract1::is_variable_unconstrained(manager&, const var&)");
502 return r;
503}
504
505
506inline bool operator== (const abstract1& x, const abstract1& y)
507{
508 bool r = ap_abstract1_is_eq(x.a.abstract0->man,
509 const_cast<ap_abstract1_t*>(&x.a),
510 const_cast<ap_abstract1_t*>(&y.a));
511 manager::raise(x.a.abstract0->man, "apron::operator==(const abstract1&, const abstract1&)");
512 return r;
513}
514
515inline bool operator!= (const abstract1& x, const abstract1& y)
516{
517 return !(x==y);
518}
519
520inline bool operator<= (const abstract1& x, const abstract1& y)
521{
522 bool r = ap_abstract1_is_leq(x.a.abstract0->man,
523 const_cast<ap_abstract1_t*>(&x.a),
524 const_cast<ap_abstract1_t*>(&y.a));
525 manager::raise(x.a.abstract0->man, "apron::operator<=(const abstract1&, const abstract1&)");
526 return r;
527}
528
529inline bool operator>= (const abstract1& x, const abstract1& y)
530{
531 return y<=x;
532}
533
534inline bool operator> (const abstract1& x, const abstract1& y)
535{
536 return !(x<=y);
537}
538
539inline bool operator< (const abstract1& x, const abstract1& y)
540{
541 return !(y<=x);
542}
543
544
545/* Properties */
546/* ========== */
547
548
549inline interval abstract1::bound(manager& m, const linexpr1& l) const
550{
551 ap_interval_t* r =
552 ap_abstract1_bound_linexpr(m.get_ap_manager_t(),
553 const_cast<ap_abstract1_t*>(&a),
554 const_cast<ap_linexpr1_t*>(l.get_ap_linexpr1_t()));
555 m.raise("apron::abstract1::bound(manager&, const linexpr1&)");
556 return r;
557}
558
559inline interval abstract1::bound(manager& m, const texpr1& l) const
560{
561 ap_interval_t* r =
562 ap_abstract1_bound_texpr(m.get_ap_manager_t(),
563 const_cast<ap_abstract1_t*>(&a),
564 const_cast<ap_texpr1_t*>(l.get_ap_texpr1_t()));
565 if (m.exception_raised()) ap_interval_free(r);
566 m.raise("apron::abstract1::bound(manager&, const texpr1&)");
567 return r;
568}
569
570inline interval abstract1::bound(manager& m, const var& d) const
571{
572 ap_interval_t* r =
573 ap_abstract1_bound_variable(m.get_ap_manager_t(),
574 const_cast<ap_abstract1_t*>(&a),
575 d.get_ap_var_t());
576 if (m.exception_raised()) ap_interval_free(r);
577 m.raise("apron::abstract1::bound(manager&, ap_dim_t)");
578 return r;
579}
580
582{
583 ap_box1_t r =
584 ap_abstract1_to_box(m.get_ap_manager_t(),
585 const_cast<ap_abstract1_t*>(&a));
586 if (m.exception_raised()) ap_box1_clear(&r);
587 m.raise("apron::abstract1::to_box(manager&)");
588 size_t sz = r.env->intdim + r.env->realdim;
589 ap_environment_free(r.env);
590 return interval_array(sz, r.p);
591}
592
594{
595 ap_lincons1_array_t r =
596 ap_abstract1_to_lincons_array(m.get_ap_manager_t(),
597 const_cast<ap_abstract1_t*>(&a));
598 if (m.exception_raised()) ap_lincons1_array_clear(&r);
599 m.raise("apron::abstract1::to_lincons_array(manager&)");
600 return r;
601}
602
604{
605 ap_tcons1_array_t r =
606 ap_abstract1_to_tcons_array(m.get_ap_manager_t(),
607 const_cast<ap_abstract1_t*>(&a));
608 if (m.exception_raised()) ap_tcons1_array_clear(&r);
609 m.raise("apron::abstract1::to_tcons_array(manager&)");
610 return r;
611}
612
614{
615 ap_generator1_array_t r =
616 ap_abstract1_to_generator_array(m.get_ap_manager_t(),
617 const_cast<ap_abstract1_t*>(&a));
618 if (m.exception_raised()) ap_generator1_array_clear(&r);
619 m.raise("apron::abstract1::to_generator_array(manager&)");
620 return r;
621}
622
623
624/* Meet, join, unification */
625/* ======================= */
626
628{
629 a = ap_abstract1_unify(m.get_ap_manager_t(), true,
630 const_cast<ap_abstract1_t*>(&a),
631 const_cast<ap_abstract1_t*>(&y.a));
632 m.raise("apron::abstract1::unify(manager&, const abstract1&)");
633 return *this;
634}
635
636inline abstract1& unify(manager& m, abstract1& dst, const abstract1& x, const abstract1& y)
637{
638 ap_abstract1_t r =
639 ap_abstract1_unify(m.get_ap_manager_t(), false,
640 const_cast<ap_abstract1_t*>(&x.a),
641 const_cast<ap_abstract1_t*>(&y.a));
642 m.raise("apron::unify(manager&, abstract1&, const abstract1&, const abstract1&)",r);
643 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
644 dst.a = r;
645 return dst;
646}
647
649{
650 a = ap_abstract1_meet(m.get_ap_manager_t(), true,
651 const_cast<ap_abstract1_t*>(&a),
652 const_cast<ap_abstract1_t*>(&y.a));
653 m.raise("apron::abstract1::meet(manager&, const abstract1&)");
654 return *this;
655}
656
657inline abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const abstract1& y)
658{
659 ap_abstract1_t r =
660 ap_abstract1_meet(m.get_ap_manager_t(), false,
661 const_cast<ap_abstract1_t*>(&x.a),
662 const_cast<ap_abstract1_t*>(&y.a));
663 m.raise("apron::meet(manager&, abstract1&, const abstract1&, const abstract1&)",r);
664 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
665 dst.a = r;
666 return dst;
667}
668
669inline abstract1& meet(manager& m, abstract1& dst, const std::vector<const abstract1*>& x)
670{
671 ap_abstract1_t xx[x.size()];
672 for (size_t i=0;i<x.size();i++)
673 xx[i] = *(x[i]->get_ap_abstract1_t());
674 ap_abstract1_t r =
675 ap_abstract1_meet_array(m.get_ap_manager_t(), xx, x.size());
676 m.raise("apron::meet(manager&, abstract1&, const std::vector<const abstract1*>&)",r);
677 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
678 dst.a = r;
679 return dst;
680}
681
682inline abstract1& meet(manager& m, abstract1& dst, size_t sz, const abstract1 * const x[])
683{
684 ap_abstract1_t xx[sz];
685 for (size_t i=0;i<sz;i++)
686 xx[i] = *(x[i]->get_ap_abstract1_t());
687 ap_abstract1_t r =
688 ap_abstract1_meet_array(m.get_ap_manager_t(), xx, sz);
689 m.raise("apron::meet(manager&, abstract1&, size_t, const abstract1 * const [])",r);
690 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
691 dst.a = r;
692 return dst;
693}
694
696{
697 a = ap_abstract1_join(m.get_ap_manager_t(), true,
698 const_cast<ap_abstract1_t*>(&a),
699 const_cast<ap_abstract1_t*>(&y.a));
700 m.raise("apron::abstract1::join(manager&, const abstract1&)");
701 return *this;
702}
703
704inline abstract1& join(manager& m, abstract1& dst, const abstract1& x, const abstract1& y)
705{
706 ap_abstract1_t r =
707 ap_abstract1_join(m.get_ap_manager_t(), false,
708 const_cast<ap_abstract1_t*>(&x.a),
709 const_cast<ap_abstract1_t*>(&y.a));
710 m.raise("apron::join(manager&, abstract1&, const abstract1&, const abstract1&)",r);
711 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
712 dst.a = r;
713 return dst;
714}
715
716inline abstract1& join(manager& m, abstract1& dst, size_t sz, const abstract1 * const x[])
717{
718 ap_abstract1_t xx[sz];
719 for (size_t i=0;i<sz;i++)
720 xx[i] = *(x[i]->get_ap_abstract1_t());
721 ap_abstract1_t r =
722 ap_abstract1_join_array(m.get_ap_manager_t(), xx, sz);
723 m.raise("apron::join(manager&, abstract1&, size_t, const abstract1 * const [])",r);
724 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
725 dst.a = r;
726 return dst;
727}
728
729inline abstract1& join(manager& m, abstract1& dst, const std::vector<const abstract1*>& x)
730{
731 ap_abstract1_t xx[x.size()];
732 for (size_t i=0;i<x.size();i++)
733 xx[i] = *(x[i]->get_ap_abstract1_t());
734 ap_abstract1_t r =
735 ap_abstract1_join_array(m.get_ap_manager_t(), xx, x.size());
736 m.raise("apron::join(manager&, abstract1&, const std::vector<const abstract1*>&)",r);
737 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
738 dst.a = r;
739 return dst;
740}
741
743{
744 a =
745 ap_abstract1_meet_lincons_array(m.get_ap_manager_t(), true,
746 const_cast<ap_abstract1_t*>(&a),
747 const_cast<ap_lincons1_array_t*>(y.get_ap_lincons1_array_t()));
748 m.raise("apron::abstract1::meet(manager&, const lincons1_array&)");
749 return *this;
750}
751
752inline abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const lincons1_array& y)
753{
754 ap_abstract1_t r =
755 ap_abstract1_meet_lincons_array(m.get_ap_manager_t(), false,
756 const_cast<ap_abstract1_t*>(&x.a),
757 const_cast<ap_lincons1_array_t*>(y.get_ap_lincons1_array_t()));
758 m.raise("apron::meet(manager&, abstract1&, const abstract1&, const lincons1_array&)",r);
759 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
760 dst.a = r;
761 return dst;
762}
763
764
766{
767 a = ap_abstract1_meet_tcons_array(m.get_ap_manager_t(), true,
768 const_cast<ap_abstract1_t*>(&a),
769 const_cast<ap_tcons1_array_t*>(y.get_ap_tcons1_array_t()));
770 m.raise("apron::abstract1::meet(manager&, const tcons1_array&)");
771 return *this;
772}
773
774inline abstract1& meet(manager& m, abstract1& dst, const abstract1& x, const tcons1_array& y)
775{
776 ap_abstract1_t r =
777 ap_abstract1_meet_tcons_array(m.get_ap_manager_t(), false,
778 const_cast<ap_abstract1_t*>(&x.a),
779 const_cast<ap_tcons1_array_t*>(y.get_ap_tcons1_array_t()));
780 m.raise("apron::meet(manager&, abstract1&, const abstract1&, const tcons1_array&)",r);
781 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
782 dst.a = r;
783 return dst;
784}
785
786
787
789{
790 a =
791 ap_abstract1_add_ray_array(m.get_ap_manager_t(), true,
792 const_cast<ap_abstract1_t*>(&a),
793 const_cast<ap_generator1_array_t*>(y.get_ap_generator1_array_t()));
794 m.raise("apron::abstract1::add_rays(manager&, const generator1_array&)");
795 return *this;
796}
797
798inline abstract1& add_rays(manager& m, abstract1& dst, const abstract1& x, const generator1_array& y)
799{
800 ap_abstract1_t r =
801 ap_abstract1_add_ray_array(m.get_ap_manager_t(), false,
802 const_cast<ap_abstract1_t*>(&x.a),
803 const_cast<ap_generator1_array_t*>(y.get_ap_generator1_array_t()));
804 m.raise("apron::add_rays(manager&, abstract1&, const abstract1&, const generator1_array&)",r);
805 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
806 dst.a = r;
807 return dst;
808}
809
810
811
813{
814 a =
815 ap_abstract1_meet(a.abstract0->man, true,
816 const_cast<ap_abstract1_t*>(&a),
817 const_cast<ap_abstract1_t*>(&y.a));
818 manager::raise(a.abstract0->man, "apron::abstract1::operator*=(const abstract1&)");
819 return *this;
820}
821
823{
824 a =
825 ap_abstract1_join(a.abstract0->man, true,
826 const_cast<ap_abstract1_t*>(&a),
827 const_cast<ap_abstract1_t*>(&y.a));
828 manager::raise(a.abstract0->man, "apron::abstract1::operator+=(const abstract1&)");
829 return *this;
830}
831
833{
834 a =
835 ap_abstract1_meet_lincons_array(a.abstract0->man, true,
836 const_cast<ap_abstract1_t*>(&a),
837 const_cast<ap_lincons1_array_t*>(y.get_ap_lincons1_array_t()));
838 manager::raise(a.abstract0->man, "apron::abstract1::operator*=(const lincons1_array&)");
839 return *this;
840}
841
843{
844 a =
845 ap_abstract1_meet_tcons_array(a.abstract0->man, true,
846 const_cast<ap_abstract1_t*>(&a),
847 const_cast<ap_tcons1_array_t*>(y.get_ap_tcons1_array_t()));
848 manager::raise(a.abstract0->man, "apron::abstract1::operator*=(const tcons1_array&)");
849 return *this;
850}
851
853{
854 a =
855 ap_abstract1_add_ray_array(a.abstract0->man, true,
856 const_cast<ap_abstract1_t*>(&a),
857 const_cast<ap_generator1_array_t*>(y.get_ap_generator1_array_t()));
858 manager::raise(a.abstract0->man, "apron::abstract1::operator+=(const generator1_array&)");
859 return *this;
860}
861
862
863
864/* Assignments */
865/* =========== */
866
867static inline ap_abstract1_t* ap_abstract1_t_or_null(const abstract1& i)
868{
869 ap_abstract1_t* r = const_cast<ap_abstract1_t*>(i.get_ap_abstract1_t());
870 if (r->abstract0) return r;
871 return NULL;
872}
873
874inline abstract1& abstract1::assign(manager& m, const var& v, const linexpr1& l, const abstract1& inter)
875{
876 a = ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), true, &a,
877 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
878 const_cast<ap_linexpr1_t*>(l.get_ap_linexpr1_t()),
879 1,
881 m.raise("apron::abstract1::assign(manager&, size_t size, const var&, const linexpr1&, const abstract1&)");
882 return *this;
883}
884
885inline abstract1& abstract1::assign(manager& m, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter)
886{
887 ap_linexpr1_t ll[size];
888 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
889 a =
890 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), true, &a,
891 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
892 ll, size,
894 m.raise("apron::abstract1::assign(manager&, size_t size, const var[], const linexpr1 * const [], const abstract1&)");
895 return *this;
896}
897
898
899inline abstract1& abstract1::assign(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter)
900{
901 if (l.size()!=v.size())
902 throw std::invalid_argument("apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&) vectors have different size");
903 ap_linexpr1_t ll[l.size()];
904 ap_var_t vv[v.size()];
905 for (size_t i=0;i<l.size();i++) {
906 ll[i] = *(l[i]->get_ap_linexpr1_t());
907 vv[i] = v[i].get_ap_var_t();
908 }
909 a =
910 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), true, &a,
911 vv, ll, l.size(),
913 m.raise("apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)");
914 return *this;
915}
916
917
918inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter = abstract1::null)
919{
920 ap_abstract1_t r =
921 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), false,
922 const_cast<ap_abstract1_t*>(&src.a),
923 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
924 const_cast<ap_linexpr1_t*>(l.get_ap_linexpr1_t()),
925 1,
927 m.raise("apron::assign(manager&, abstract1&, const abstract1&, const var&, const linexpr1&, const abstract1&)",r);
928 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
929 dst.a = r;
930 return dst;
931}
932
933inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = abstract1::null)
934{
935 ap_linexpr1_t ll[size];
936 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
937 ap_abstract1_t r =
938 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), false,
939 const_cast<ap_abstract1_t*>(&src.a),
940 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
941 ll, size,
943 m.raise("apron::assign((manager&, abstract1&, const abstract1&, size_t size, const var[], const linexpr1 * const [], const abstract1&)",r);
944 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
945 dst.a = r;
946 return dst;
947}
948
949inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = abstract1::null)
950{
951 if (l.size()!=v.size())
952 throw std::invalid_argument("apron::assign(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&) vectors have different size");
953 ap_linexpr1_t ll[l.size()];
954 ap_var_t vv[v.size()];
955 for (size_t i=0;i<l.size();i++) {
956 ll[i] = *(l[i]->get_ap_linexpr1_t());
957 vv[i] = v[i].get_ap_var_t();
958 }
959 ap_abstract1_t r =
960 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(), false,
961 const_cast<ap_abstract1_t*>(&src.a),
962 vv, ll, l.size(),
964 m.raise("apron::assign(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)",r);
965 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
966 dst.a = r;
967 return dst;
968}
969
970
971
972
973
974inline abstract1& abstract1::assign(manager& m, const var& v, const texpr1& l, const abstract1& inter)
975{
976 a = ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), true, &a,
977 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
978 const_cast<ap_texpr1_t*>(l.get_ap_texpr1_t()),
979 1,
981 m.raise("apron::abstract1::assign(manager&, size_t size, const var&, const texpr1&, const abstract1&)");
982 return *this;
983}
984
985inline abstract1& abstract1::assign(manager& m, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter)
986{
987 ap_texpr1_t ll[size];
988 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
989 a = ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), true, &a,
990 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
991 ll, size,
993 m.raise("apron::abstract1::assign(manager&, size_t size, const var[], const texpr1 * const [], const abstract1&)");
994 return *this;
995}
996
997inline abstract1& abstract1::assign(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter)
998{
999 if (l.size()!=v.size())
1000 throw std::invalid_argument("apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1001 ap_texpr1_t ll[l.size()];
1002 ap_var_t vv[v.size()];
1003 for (size_t i=0;i<l.size();i++) {
1004 ll[i] = *(l[i]->get_ap_texpr1_t());
1005 vv[i] = v[i].get_ap_var_t();
1006 }
1007 a = ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), true, &a,
1008 vv, ll, l.size(),
1009 ap_abstract1_t_or_null(inter));
1010 m.raise("apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1011 return *this;
1012}
1013
1014inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter = abstract1::null)
1015{
1016 ap_abstract1_t r =
1017 ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), false,
1018 const_cast<ap_abstract1_t*>(&src.a),
1019 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
1020 const_cast<ap_texpr1_t*>(l.get_ap_texpr1_t()),
1021 1,
1022 ap_abstract1_t_or_null(inter));
1023 m.raise("apron::assign(manager&, abstract1&, const abstract1&, const var&, const texpr1&, const abstract1&)",r);
1024 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1025 dst.a = r;
1026 return dst;
1027}
1028
1029inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = abstract1::null)
1030{
1031 ap_texpr1_t ll[size];
1032 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
1033 ap_abstract1_t r =
1034 ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), false,
1035 const_cast<ap_abstract1_t*>(&src.a),
1036 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1037 ll, size,
1038 ap_abstract1_t_or_null(inter));
1039 m.raise("apron::assign((manager&, abstract1&, const abstract1&, size_t size, const var[], const texpr1 * const [], const abstract1&)",r);
1040 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1041 dst.a = r;
1042 return dst;
1043}
1044
1045inline abstract1& assign(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = abstract1::null)
1046{
1047 if (l.size()!=v.size())
1048 throw std::invalid_argument("apron::assign(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1049 ap_texpr1_t ll[l.size()];
1050 ap_var_t vv[v.size()];
1051 for (size_t i=0;i<l.size();i++) {
1052 ll[i] = *(l[i]->get_ap_texpr1_t());
1053 vv[i] = v[i].get_ap_var_t();
1054 }
1055 ap_abstract1_t r =
1056 ap_abstract1_assign_texpr_array(m.get_ap_manager_t(), false,
1057 const_cast<ap_abstract1_t*>(&src.a),
1058 vv, ll, l.size(),
1059 ap_abstract1_t_or_null(inter));
1060 m.raise("apron::assign(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&)",r);
1061 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1062 dst.a = r;
1063 return dst;
1064}
1065
1066
1067
1068/* Substitutions */
1069/* =========== = */
1070
1071
1072inline abstract1& abstract1::substitute(manager& m, const var& v, const linexpr1& l, const abstract1& inter)
1073{
1074 a = ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), true, &a,
1075 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
1076 const_cast<ap_linexpr1_t*>(l.get_ap_linexpr1_t()),
1077 1,
1078 ap_abstract1_t_or_null(inter));
1079 m.raise("apron::abstract1::substitute(manager&, size_t size, const var&, const linexpr1&, const abstract1&)");
1080 return *this;
1081}
1082
1083inline abstract1& abstract1::substitute(manager& m, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter)
1084{
1085 ap_linexpr1_t ll[size];
1086 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
1087 a =
1088 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), true, &a,
1089 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1090 ll, size,
1091 ap_abstract1_t_or_null(inter));
1092 m.raise("apron::abstract1::substitute(manager&, size_t size, const var[], const linexpr1 * const [], const abstract1&)");
1093 return *this;
1094}
1095
1096
1097inline abstract1& abstract1::substitute(manager& m, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter)
1098{
1099 if (l.size()!=v.size())
1100 throw std::invalid_argument("apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&) vectors have different size");
1101 ap_linexpr1_t ll[l.size()];
1102 ap_var_t vv[v.size()];
1103 for (size_t i=0;i<l.size();i++) {
1104 ll[i] = *(l[i]->get_ap_linexpr1_t());
1105 vv[i] = v[i].get_ap_var_t();
1106 }
1107 a =
1108 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), true, &a,
1109 vv, ll, l.size(),
1110 ap_abstract1_t_or_null(inter));
1111 m.raise("apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)");
1112 return *this;
1113}
1114
1115
1116inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const linexpr1& l, const abstract1& inter = abstract1::null)
1117{
1118 ap_abstract1_t r =
1119 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), false,
1120 const_cast<ap_abstract1_t*>(&src.a),
1121 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
1122 const_cast<ap_linexpr1_t*>(l.get_ap_linexpr1_t()),
1123 1,
1124 ap_abstract1_t_or_null(inter));
1125 m.raise("apron::substitute(manager&, abstract1&, const abstract1&, const var&, const linexpr1&, const abstract1&)",r);
1126 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1127 dst.a = r;
1128 return dst;
1129}
1130
1131inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const linexpr1 * const l[], const abstract1& inter = abstract1::null)
1132{
1133 ap_linexpr1_t ll[size];
1134 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
1135 ap_abstract1_t r =
1136 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), false,
1137 const_cast<ap_abstract1_t*>(&src.a),
1138 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1139 ll, size,
1140 ap_abstract1_t_or_null(inter));
1141 m.raise("apron::substitute((manager&, abstract1&, const abstract1&, size_t size, const var[], const linexpr1 * const [], const abstract1&)",r);
1142 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1143 dst.a = r;
1144 return dst;
1145}
1146
1147inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const linexpr1*>& l, const abstract1& inter = abstract1::null)
1148{
1149 if (l.size()!=v.size())
1150 throw std::invalid_argument("apron::substitute(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&) vectors have different size");
1151 ap_linexpr1_t ll[l.size()];
1152 ap_var_t vv[v.size()];
1153 for (size_t i=0;i<l.size();i++) {
1154 ll[i] = *(l[i]->get_ap_linexpr1_t());
1155 vv[i] = v[i].get_ap_var_t();
1156 }
1157 ap_abstract1_t r =
1158 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(), false,
1159 const_cast<ap_abstract1_t*>(&src.a),
1160 vv, ll, l.size(),
1161 ap_abstract1_t_or_null(inter));
1162 m.raise("apron::substitute(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)",r);
1163 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1164 dst.a = r;
1165 return dst;
1166}
1167
1168
1169
1170
1171
1172inline abstract1& abstract1::substitute(manager& m, const var& v, const texpr1& l, const abstract1& inter)
1173{
1174 a = ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), true, &a,
1175 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
1176 const_cast<ap_texpr1_t*>(l.get_ap_texpr1_t()),
1177 1,
1178 ap_abstract1_t_or_null(inter));
1179 m.raise("apron::abstract1::substitute(manager&, size_t size, const var&, const texpr1&, const abstract1&)");
1180 return *this;
1181}
1182
1183inline abstract1& abstract1::substitute(manager& m, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter)
1184{
1185 ap_texpr1_t ll[size];
1186 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
1187 a = ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), true, &a,
1188 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1189 ll, size,
1190 ap_abstract1_t_or_null(inter));
1191 m.raise("apron::abstract1::substitute(manager&, size_t size, const var[], const texpr1 * const [], const abstract1&)");
1192 return *this;
1193}
1194
1195inline abstract1& abstract1::substitute(manager& m, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter)
1196{
1197 if (l.size()!=v.size())
1198 throw std::invalid_argument("apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1199 ap_texpr1_t ll[l.size()];
1200 ap_var_t vv[v.size()];
1201 for (size_t i=0;i<l.size();i++) {
1202 ll[i] = *(l[i]->get_ap_texpr1_t());
1203 vv[i] = v[i].get_ap_var_t();
1204 }
1205 a = ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), true, &a,
1206 vv, ll, l.size(),
1207 ap_abstract1_t_or_null(inter));
1208 m.raise("apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1209 return *this;
1210}
1211
1212inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const var& v, const texpr1& l, const abstract1& inter = abstract1::null)
1213{
1214 ap_abstract1_t r =
1215 ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), false,
1216 const_cast<ap_abstract1_t*>(&src.a),
1217 reinterpret_cast<ap_var_t*>(const_cast<var*>(&v)),
1218 const_cast<ap_texpr1_t*>(l.get_ap_texpr1_t()),
1219 1,
1220 ap_abstract1_t_or_null(inter));
1221 m.raise("apron::substitute(manager&, abstract1&, const abstract1&, const var&, const texpr1&, const abstract1&)",r);
1222 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1223 dst.a = r;
1224 return dst;
1225}
1226
1227inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], const texpr1 * const l[], const abstract1& inter = abstract1::null)
1228{
1229 ap_texpr1_t ll[size];
1230 for (size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
1231 ap_abstract1_t r =
1232 ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), false,
1233 const_cast<ap_abstract1_t*>(&src.a),
1234 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1235 ll, size,
1236 ap_abstract1_t_or_null(inter));
1237 m.raise("apron::substitute((manager&, abstract1&, const abstract1&, size_t size, const var[], const texpr1 * const [], const abstract1&)",r);
1238 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1239 dst.a = r;
1240 return dst;
1241}
1242
1243inline abstract1& substitute(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, const std::vector<const texpr1*>& l, const abstract1& inter = abstract1::null)
1244{
1245 if (l.size()!=v.size())
1246 throw std::invalid_argument("apron::substitute(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1247 ap_texpr1_t ll[l.size()];
1248 ap_var_t vv[v.size()];
1249 for (size_t i=0;i<l.size();i++) {
1250 ll[i] = *(l[i]->get_ap_texpr1_t());
1251 vv[i] = v[i].get_ap_var_t();
1252 }
1253 ap_abstract1_t r =
1254 ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(), false,
1255 const_cast<ap_abstract1_t*>(&src.a),
1256 vv, ll, l.size(),
1257 ap_abstract1_t_or_null(inter));
1258 m.raise("apron::substitute(manager&, abstract1, const abstract1&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&)",r);
1259 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1260 dst.a = r;
1261 return dst;
1262}
1263
1264
1265
1266
1267
1268/* Projection */
1269/* ========== */
1270
1271inline abstract1& abstract1::forget(manager& m, const var& v, bool project)
1272{
1273 return forget(m,1,&v,project);
1274}
1275
1276inline abstract1& abstract1::forget(manager& m, size_t size, const var v[], bool project)
1277{
1278 a = ap_abstract1_forget_array(m.get_ap_manager_t(), true, &a,
1279 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1280 size, project);
1281 m.raise("apron::abstract1::forget(manager&, size_t, const var[], bool)");
1282 return *this;
1283}
1284
1285inline abstract1& abstract1::forget(manager& m, const std::vector<var>& v, bool project)
1286{
1287 ap_var_t vv[v.size()];
1288 for (size_t i=0;i<v.size();i++) vv[i] = v[i].get_ap_var_t();
1289 a = ap_abstract1_forget_array(m.get_ap_manager_t(), true, &a, vv, v.size(), project);
1290 m.raise("apron::abstract1::forget(manager&, const std::vector<var>&, bool)");
1291 return *this;
1292}
1293
1294inline abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const var& v, bool project = false)
1295{
1296 return forget(m,dst,src,1,&v,project);
1297}
1298
1299inline abstract1& forget(manager& m, abstract1& dst, const abstract1& src, size_t size, const var v[], bool project = false)
1300{
1301 ap_abstract1_t r = ap_abstract1_forget_array(m.get_ap_manager_t(), false,
1302 const_cast<ap_abstract1_t*>(&src.a),
1303 reinterpret_cast<ap_var_t*>(const_cast<var*>(v)),
1304 size, project);
1305 m.raise("apron::forget(manager&, abstract1&, const abstract1&, size_t, const var[], bool)",r);
1306 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1307 dst.a = r;
1308 return dst;
1309}
1310
1311inline abstract1& forget(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& v, bool project = false)
1312{
1313 ap_var_t vv[v.size()];
1314 for (size_t i=0;i<v.size();i++) vv[i] = v[i].get_ap_var_t();
1315 ap_abstract1_t r = ap_abstract1_forget_array(m.get_ap_manager_t(), false,
1316 const_cast<ap_abstract1_t*>(&src.a),
1317 vv, v.size(), project);
1318 m.raise("apron::forget(manager&, abstract1&, const abstract1&, const std::vector<var>&, bool)",r);
1319 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1320 dst.a = r;
1321 return dst;
1322}
1323
1324
1325
1326/* Change of environment */
1327/* ====================== */
1328
1330{
1331 a = ap_abstract1_change_environment(m.get_ap_manager_t(), true, &a,
1332 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
1333 project);
1334 m.raise("apron::abstract1::change_environment(manager&, const environment&, bool)");
1335 return *this;
1336}
1337
1338inline abstract1& change_environment(manager& m, abstract1& dst, const abstract1& src, const environment& e, bool project = false)
1339{
1340 ap_abstract1_t r =
1341 ap_abstract1_change_environment(m.get_ap_manager_t(), false,
1342 const_cast<ap_abstract1_t*>(&src.a),
1343 const_cast<ap_environment_t*>(e.get_ap_environment_t()),
1344 project);
1345 m.raise("apron::change_environment(manager&, abstrct1&, const abstract1&, const environment&, bool)",r);
1346 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1347 dst.a = r;
1348 return dst;
1349}
1350
1352{
1353 a = ap_abstract1_minimize_environment(m.get_ap_manager_t(), true, &a);
1354 m.raise("apron::abstract1::minimize_environment(manager&)");
1355 return *this;
1356}
1357
1358inline abstract1& minimize_environment(manager& m, abstract1& dst, const abstract1& src)
1359{
1360 ap_abstract1_t r =
1361 ap_abstract1_minimize_environment(m.get_ap_manager_t(), false,
1362 const_cast<ap_abstract1_t*>(&src.a));
1363 m.raise("apron::minimize_environment(manager&, abstract1&, const abstract1&)",r);
1364 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1365 dst.a = r;
1366 return dst;
1367}
1368
1369inline abstract1& abstract1::rename(manager& m, size_t size, const var oldv[], const var newv[])
1370{
1371 a = ap_abstract1_rename_array(m.get_ap_manager_t(), true, &a,
1372 reinterpret_cast<ap_var_t*>(const_cast<var*>(oldv)),
1373 reinterpret_cast<ap_var_t*>(const_cast<var*>(newv)),
1374 size);
1375 m.raise("apron::abstract1::rename(manager&, size_t, const var[], const var[])");
1376 return *this;
1377}
1378
1379inline abstract1& abstract1::rename(manager& m, const std::vector<var>& oldv, const std::vector<var>& newv)
1380{
1381 if (oldv.size()!=newv.size())
1382 throw std::invalid_argument("apron::abstract1::rename(manager&, const std::vector<var>&, const std::vector<var>&) vector have different size");
1383 ap_var_t oldvv[oldv.size()];
1384 ap_var_t newvv[newv.size()];
1385 for (size_t i=0;i<oldv.size();i++) {
1386 oldvv[i] = oldv[i].get_ap_var_t();
1387 newvv[i] = newv[i].get_ap_var_t();
1388 }
1389 a = ap_abstract1_rename_array(m.get_ap_manager_t(), true, &a,
1390 oldvv, newvv, oldv.size());
1391 m.raise("apron::abstract1::rename(manager&, const std::vector<var>&, const std::vector<var>&)");
1392 return *this;
1393}
1394
1395inline abstract1& rename(manager& m, abstract1& dst, const abstract1& src, size_t size, const var oldv[], const var newv[])
1396{
1397 ap_abstract1_t r =
1398 ap_abstract1_rename_array(m.get_ap_manager_t(), false,
1399 const_cast<ap_abstract1_t*>(&src.a),
1400 reinterpret_cast<ap_var_t*>(const_cast<var*>(oldv)),
1401 reinterpret_cast<ap_var_t*>(const_cast<var*>(newv)),
1402 size);
1403 m.raise("apron::rename(manager&, abstract1&, const abstract1&, size_t, const var[], const var[])",r);
1404 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1405 dst.a = r;
1406 return dst;
1407}
1408
1409inline abstract1& rename(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& oldv, const std::vector<var>& newv)
1410{
1411 if (oldv.size()!=newv.size())
1412 throw std::invalid_argument("apron::abstract1::rename(manager&, abstract1&, const abstract1&, const std::vector<var>&, const std::vector<var>&) vector have different size");
1413 ap_var_t oldvv[oldv.size()];
1414 ap_var_t newvv[newv.size()];
1415 for (size_t i=0;i<oldv.size();i++) {
1416 oldvv[i] = oldv[i].get_ap_var_t();
1417 newvv[i] = newv[i].get_ap_var_t();
1418 }
1419 ap_abstract1_t r =
1420 ap_abstract1_rename_array(m.get_ap_manager_t(), false,
1421 const_cast<ap_abstract1_t*>(&src.a),
1422 oldvv, newvv, oldv.size());
1423 m.raise("apron::rename(manager&, abstract1&, const abstract1&, const std::vector<var>&, const std::vector<var>&)",r);
1424 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1425 dst.a = r;
1426 return dst;
1427}
1428
1429
1430
1431/* Expansion and folding */
1432/* ===================== */
1433
1434inline abstract1& abstract1::expand(manager& m, const var& v, size_t size, const var vv[])
1435{
1436 a = ap_abstract1_expand(m.get_ap_manager_t(), true, &a,
1437 const_cast<ap_var_t>(v.get_ap_var_t()),
1438 reinterpret_cast<ap_var_t*>(const_cast<var*>(vv)),
1439 size);
1440 m.raise("apron::abstract1::expand(manager&, const var&, size_t, const var[])");
1441 return *this;
1442}
1443
1444inline abstract1& abstract1::expand(manager& m, const var& v, const std::vector<var>& vv)
1445{
1446 ap_var_t ww[vv.size()];
1447 for (size_t i=0;i<vv.size();i++) ww[i] = vv[i].get_ap_var_t();
1448 a = ap_abstract1_expand(m.get_ap_manager_t(), true, &a,
1449 const_cast<ap_var_t>(v.get_ap_var_t()),
1450 ww, vv.size());
1451 m.raise("apron::abstract1::expand(manager&, const var&, const std::vector<var>&)");
1452 return *this;
1453}
1454
1455inline abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, size_t size, const var vv[])
1456{
1457 ap_abstract1_t r =
1458 ap_abstract1_expand(m.get_ap_manager_t(), false,
1459 const_cast<ap_abstract1_t*>(&src.a),
1460 const_cast<ap_var_t>(v.get_ap_var_t()),
1461 reinterpret_cast<ap_var_t*>(const_cast<var*>(vv)),
1462 size);
1463 m.raise("apron::expand(manager&, abstract1&, const abstract1&, const var&, size_t, const var[])",r);
1464 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1465 dst.a = r;
1466 return dst;
1467}
1468
1469inline abstract1& expand(manager& m, abstract1& dst, const abstract1& src, const var& v, const std::vector<var>& vv)
1470{
1471 ap_var_t ww[vv.size()];
1472 for (size_t i=0;i<vv.size();i++) ww[i] = vv[i].get_ap_var_t();
1473 ap_abstract1_t r =
1474 ap_abstract1_expand(m.get_ap_manager_t(), false,
1475 const_cast<ap_abstract1_t*>(&src.a),
1476 const_cast<ap_var_t>(v.get_ap_var_t()),
1477 ww, vv.size());
1478 m.raise("apron::expand(manager&, abstract1&, const abstract1&, const var&, const std::vector<var>&)",r);
1479 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1480 dst.a = r;
1481 return dst;
1482}
1483
1484
1485
1486inline abstract1& abstract1::fold(manager& m, size_t size, const var vv[])
1487{
1488 a = ap_abstract1_fold(m.get_ap_manager_t(), true, &a,
1489 reinterpret_cast<ap_var_t*>(const_cast<var*>(vv)),
1490 size);
1491 m.raise("apron::abstract1::fold(manager&, const var&, size_t, const var[])");
1492 return *this;
1493}
1494
1495inline abstract1& abstract1::fold(manager& m, const std::vector<var>& vv)
1496{
1497 ap_var_t ww[vv.size()];
1498 for (size_t i=0;i<vv.size();i++) ww[i] = vv[i].get_ap_var_t();
1499 a = ap_abstract1_fold(m.get_ap_manager_t(), true, &a, ww, vv.size());
1500 m.raise("apron::abstract1::fold(manager&, const std::vector<var>&)");
1501 return *this;
1502}
1503
1504inline abstract1& fold(manager& m, abstract1& dst, const abstract1& src, size_t size, const var vv[])
1505{
1506 ap_abstract1_t r =
1507 ap_abstract1_fold(m.get_ap_manager_t(), false,
1508 const_cast<ap_abstract1_t*>(&src.a),
1509 reinterpret_cast<ap_var_t*>(const_cast<var*>(vv)),
1510 size);
1511 m.raise("apron::fold(manager&, abstract1&, const abstract1&, size_t, const var[])",r);
1512 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1513 dst.a = r;
1514 return dst;
1515}
1516
1517inline abstract1& fold(manager& m, abstract1& dst, const abstract1& src, const std::vector<var>& vv)
1518{
1519 ap_var_t ww[vv.size()];
1520 for (size_t i=0;i<vv.size();i++) ww[i] = vv[i].get_ap_var_t();
1521 ap_abstract1_t r =
1522 ap_abstract1_fold(m.get_ap_manager_t(), false,
1523 const_cast<ap_abstract1_t*>(&src.a),
1524 ww, vv.size());
1525 m.raise("apron::fold(manager&, abstract1&, const abstract1&, const std::vector<var>&)",r);
1526 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1527 dst.a = r;
1528 return dst;
1529}
1530
1531
1532/* Widenings */
1533/* ========= */
1534
1535inline abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y)
1536{
1537 ap_abstract1_t r =
1538 ap_abstract1_widening(m.get_ap_manager_t(),
1539 const_cast<ap_abstract1_t*>(&x.a),
1540 const_cast<ap_abstract1_t*>(&y.a));
1541 m.raise("apron::widening(manager&, abstract1&, const abstract1&, const abstract1&)",r);
1542 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1543 dst.a = r;
1544 return dst;
1545}
1546
1547inline abstract1& widening(manager& m, abstract1& dst, const abstract1& x, const abstract1& y, const lincons1_array& l)
1548{
1549 ap_abstract1_t r =
1550 ap_abstract1_widening_threshold(m.get_ap_manager_t(),
1551 const_cast<ap_abstract1_t*>(&x.a),
1552 const_cast<ap_abstract1_t*>(&y.a),
1553 const_cast<ap_lincons1_array_t*>(l.get_ap_lincons1_array_t()));
1554 m.raise("apron::widening(manager&, abstract1&, const abstract1&, const abstract1&, const lincons1_array&)",r);
1555 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1556 dst.a = r;
1557 return dst;
1558}
1559
1560
1561/* Closure */
1562/* ======= */
1563
1564
1566{
1567 a = ap_abstract1_closure(m.get_ap_manager_t(), true, &a);
1568 m.raise("apron::abstract1::closured(manager&)");
1569 return *this;
1570}
1571
1572inline abstract1& closure(manager& m, abstract1& dst, const abstract1& src)
1573{
1574 ap_abstract1_t r =
1575 ap_abstract1_closure(m.get_ap_manager_t(), false, const_cast<ap_abstract1_t*>(&src.a));
1576 m.raise("apron::closure(manager&, abstract1&, const abstract1&)",r);
1577 ap_abstract1_clear(m.get_ap_manager_t(), &dst.a);
1578 dst.a = r;
1579 return dst;
1580}
1581
1582
1583/* C-level compatibility */
1584/* ===================== */
1585
1586inline ap_abstract1_t* abstract1::get_ap_abstract1_t()
1587{ return &a; }
1588
1589
1590inline const ap_abstract1_t* abstract1::get_ap_abstract1_t() const
1591{ return &a; }
bool operator==(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:409
void printdiff(manager &m, const abstract0 &x, const abstract0 &y, char **name_of_dim=NULL, FILE *stream=stdout)
Definition apxx_abstract0_inline.hh:280
abstract0 & add_rays(manager &m, abstract0 &dst, const abstract0 &x, const generator0_array &y)
Definition apxx_abstract0_inline.hh:644
abstract0 & forget(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, bool project=false)
Definition apxx_abstract0_inline.hh:983
abstract0 & expand(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, size_t n=1)
Definition apxx_abstract0_inline.hh:1083
bool operator<=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:421
bool operator>(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:433
abstract0 & join(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:560
bool operator<(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:438
abstract0 & substitute(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=abstract0::null)
Definition apxx_abstract0_inline.hh:859
abstract0 & meet(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:518
abstract0 & assign(manager &m, abstract0 &dst, const abstract0 &src, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=abstract0::null)
Definition apxx_abstract0_inline.hh:728
abstract0 & fold(manager &m, abstract0 &dst, const abstract0 &src, size_t size, const ap_dim_t dim[])
Definition apxx_abstract0_inline.hh:1106
abstract0 & closure(manager &m, abstract0 &dst, const abstract0 &src)
Definition apxx_abstract0_inline.hh:1158
bool operator>=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:428
abstract0 & deserialize(manager &m, abstract0 &dst, const std::string &s, size_t *eaten=NULL)
Definition apxx_abstract0_inline.hh:313
bool operator!=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:416
std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Definition apxx_abstract0_inline.hh:292
abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:1127
abstract1 & rename(manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var oldv[], const var newv[])
Definition apxx_abstract1_inline.hh:1395
abstract1 & unify(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:636
static ap_abstract1_t * ap_abstract1_t_or_null(const abstract1 &i)
Definition apxx_abstract1_inline.hh:867
abstract1 & change_environment(manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project=false)
Definition apxx_abstract1_inline.hh:1338
abstract1 & minimize_environment(manager &m, abstract1 &dst, const abstract1 &src)
Definition apxx_abstract1_inline.hh:1358
Level 0 abstract value (ap_abstract0_t* wrapper).
Definition apxx_abstract0.hh:78
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_abstract0_inline.hh:1172
Level 1 abstract value (ap_abstract1_t wrapper).
Definition apxx_abstract1.hh:42
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
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.
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 & 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
abstract1 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition apxx_abstract1_inline.hh:324
~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 & join(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Replaces dst with the join of x and y.
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 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
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
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 & 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
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 & add_rays(manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
Replaces dst with x with some rays added.
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
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
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 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition apxx_abstract1_inline.hh:317
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
void free(manager &m)
Destroys the abstract element using the given manager.
Definition apxx_abstract1_inline.hh:114
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
const ap_environment_t * get_ap_environment_t() const
Returns a pointer to the internal APRON object pointed by *this.
Definition apxx_environment_inline.hh:425
Array of generators (ap_generator1_array_t wrapper).
Definition apxx_generator1.hh:272
const ap_generator1_array_t * get_ap_generator1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_generator1_inline.hh:436
array of interval(s).
Definition apxx_interval.hh:302
const ap_interval_t *const * get_ap_interval_t_array() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_interval_inline.hh:505
size_t size() const
Returns the array size.
Definition apxx_interval_inline.hh:473
Interval (ap_interval_t wrapper).
Definition apxx_interval.hh:47
const ap_interval_t * get_ap_interval_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_interval_inline.hh:336
Array of linear constraints (ap_lincons1_array_t wrapper).
Definition apxx_lincons1.hh:331
const ap_lincons1_array_t * get_ap_lincons1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_lincons1_inline.hh:499
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition apxx_lincons1_inline.hh:431
Level 1 linear constraint (ap_lincons1_t wrapper).
Definition apxx_lincons1.hh:40
const ap_lincons1_t * get_ap_lincons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_lincons1_inline.hh:278
Level 1 linear expression (ap_linexpr1_t wrapper).
Definition apxx_linexpr1.hh:39
const ap_linexpr1_t * get_ap_linexpr1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_linexpr1_inline.hh:321
Library manager (ap_manager_t wrapper).
Definition apxx_manager.hh:137
bool exception_raised()
Internal use only. Whether APRON has raised an exception.
Definition apxx_manager_inline.hh:82
ap_manager_t * get_ap_manager_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_manager_inline.hh:206
static void raise(ap_manager_t *m, const char *msg, ap_abstract0_t *a=NULL)
Internal use only. Translates APRON exceptions to C++ ones.
Definition apxx_manager_inline.hh:88
Array of arbitrary constraints (ap_tcons1_array_t wrapper).
Definition apxx_tcons1.hh:337
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition apxx_tcons1_inline.hh:461
const ap_tcons1_array_t * get_ap_tcons1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_tcons1_inline.hh:530
Level 1 arbitrary constraint (ap_tcons1_t wrapper).
Definition apxx_tcons1.hh:39
const ap_tcons1_t * get_ap_tcons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_tcons1_inline.hh:307
Level 1 arbitrary expression tree (ap_texpr1_t wrapper).
Definition apxx_texpr1.hh:42
ap_texpr1_t * get_ap_texpr1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_texpr1_inline.hh:271
Variable name (ap_var_t wrapper).
Definition apxx_var.hh:39
const ap_var_t & get_ap_var_t() const
Returns a reference to the APRON object wrapped (no copy).
Definition apxx_var_inline.hh:156
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