APRONXX 0.9.15
/home/mine/apron/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
30inline abstract1::abstract1(manager &m, const environment& e, top x)
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
37inline abstract1::abstract1(manager &m, const environment& e, bottom x)
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
44inline abstract1::abstract1(manager &m, const abstract1& t)
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
82inline abstract1::abstract1(manager &m, const lincons1_array& x)
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
90inline abstract1::abstract1(manager &m, const tcons1_array& x)
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
98inline abstract1::abstract1(const abstract1& t)
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
108inline abstract1::~abstract1()
109{
110 if (a.abstract0) ap_abstract1_clear(a.abstract0->man, &a);
111}
112
113
114inline void abstract1::free(manager& m)
115{
116 if (a.abstract0) ap_abstract1_clear(m.get_ap_manager_t(), &a);
117}
118
119
120
121/* assignments */
122/* =========== */
123
124inline abstract1& abstract1::operator=(const abstract1& t)
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
136inline abstract1& abstract1::operator=(top t)
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
145inline abstract1& abstract1::operator=(bottom t)
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
154inline abstract1& abstract1::operator=(const interval_array& x)
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
167inline abstract1& abstract1::operator=(const lincons1_array& x)
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
179inline abstract1& abstract1::operator=(const tcons1_array& x)
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
192inline abstract1& abstract1::set(manager& m, const abstract1& x)
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
205inline abstract1& abstract1::set(manager& m, top t)
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
214inline abstract1& abstract1::set(manager& m, const environment& e, top t)
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
224inline abstract1& abstract1::set(manager& m, bottom t)
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
233inline abstract1& abstract1::set(manager& m, const environment& e, bottom t)
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
243inline abstract1& abstract1::set(manager& m, const interval_array& x)
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
289inline abstract1& abstract1::set(manager& m, const lincons1_array& x)
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
301inline abstract1& abstract1::set(manager& m, const tcons1_array& x)
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
317inline abstract1& abstract1::minimize(manager& m)
318{
319 ap_abstract1_minimize(m.get_ap_manager_t(), &a);
320 m.raise("apron::abstract1::minimize(manager &)");
321 return *this;
322}
323
324inline abstract1& abstract1::canonicalize(manager& m)
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
400inline manager abstract1::get_manager() const
401{
402 return ap_manager_copy(ap_abstract0_manager(const_cast<ap_abstract0_t*>(a.abstract0)));
403}
404
405inline environment abstract1::get_environment() const
406{
407 return ap_environment_copy(const_cast<ap_environment_t*>(a.env));
408}
409
410inline abstract0& abstract1::get_abstract0()
411{
412 return reinterpret_cast<abstract0&>(a.abstract0);
413}
414
415inline const abstract0& abstract1::get_abstract0() const
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
581inline interval_array abstract1::to_box(manager& m) const
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
593inline lincons1_array abstract1::to_lincons_array(manager& m) const
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
603inline tcons1_array abstract1::to_tcons_array(manager& m) const
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
613inline generator1_array abstract1::to_generator_array(manager& m) const
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
627inline abstract1& abstract1::unify(manager& m, const abstract1& y)
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
648inline abstract1& abstract1::meet(manager& m, const abstract1& y)
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
695inline abstract1& abstract1::join(manager& m, const abstract1& y)
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
742inline abstract1& abstract1::meet(manager& m, const lincons1_array& y)
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
765inline abstract1& abstract1::meet(manager& m, const tcons1_array& y)
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
788inline abstract1& abstract1::add_rays(manager& m, const generator1_array& y)
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
812inline abstract1& abstract1::operator*=(const abstract1& y)
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
822inline abstract1& abstract1::operator+=(const abstract1& y)
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
832inline abstract1& abstract1::operator*=(const lincons1_array& y)
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
842inline abstract1& abstract1::operator*=(const tcons1_array& y)
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
852inline abstract1& abstract1::operator+=(const generator1_array& y)
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
1329inline abstract1& abstract1::change_environment(manager& m, const environment& e, bool project)
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
1351inline abstract1& abstract1::minimize_environment(manager& m)
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
1565inline abstract1& abstract1::closure(manager& m)
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; }
abstract1 & rename(manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var oldv[], const var newv[])
Definition apxx_abstract1_inline.hh:1395
void printdiff(manager &m, const abstract1 &x, const abstract1 &y, FILE *stream=stdout)
Definition apxx_abstract1_inline.hh:348
abstract1 & meet(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:657
abstract1 & closure(manager &m, abstract1 &dst, const abstract1 &src)
Definition apxx_abstract1_inline.hh:1572
abstract1 & fold(manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var vv[])
Definition apxx_abstract1_inline.hh:1504
bool operator!=(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:515
abstract1 & expand(manager &m, abstract1 &dst, const abstract1 &src, const var &v, size_t size, const var vv[])
Definition apxx_abstract1_inline.hh:1455
abstract1 & join(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:704
bool operator<(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:539
abstract1 & unify(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:636
bool operator<=(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:520
std::ostream & operator<<(std::ostream &os, const abstract1 &s)
Definition apxx_abstract1_inline.hh:362
static ap_abstract1_t * ap_abstract1_t_or_null(const abstract1 &i)
Definition apxx_abstract1_inline.hh:867
abstract1 & assign(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter=abstract1::null)
Definition apxx_abstract1_inline.hh:918
abstract1 & add_rays(manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
Definition apxx_abstract1_inline.hh:798
bool operator>=(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:529
bool operator>(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:534
abstract1 & widening(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:1535
abstract1 & substitute(manager &m, abstract1 &dst, const abstract1 &src, const var &v, const linexpr1 &l, const abstract1 &inter=abstract1::null)
Definition apxx_abstract1_inline.hh:1116
abstract1 & change_environment(manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project=false)
Definition apxx_abstract1_inline.hh:1338
abstract1 & deserialize(manager &m, abstract1 &dst, const std::string &s, size_t *eaten=NULL)
Definition apxx_abstract1_inline.hh:384
abstract1 & minimize_environment(manager &m, abstract1 &dst, const abstract1 &src)
Definition apxx_abstract1_inline.hh:1358
bool operator==(const abstract1 &x, const abstract1 &y)
Definition apxx_abstract1_inline.hh:506
abstract1 & forget(manager &m, abstract1 &dst, const abstract1 &src, const var &v, bool project=false)
Definition apxx_abstract1_inline.hh:1294