27 inline abstract0::abstract0(ap_abstract0_t* x)
33 a = ap_abstract0_top(m.get_ap_manager_t(), intdim, realdim);
34 m.raise(
"apron::abstract0::abstract0(manager&, size_t, size_t, top)",
a);
39 a = ap_abstract0_bottom(m.get_ap_manager_t(), intdim, realdim);
40 m.raise(
"apron::abstract0::abstract0(manager&, size_t, size_t, bottom)",
a);
45 a = ap_abstract0_copy(m.get_ap_manager_t(), t.a);
46 m.raise(
"apron::abstract0::abstract0::(manager&, const abstract0&)",
a);
51 if (x.size()<intdim+realdim)
52 throw std::invalid_argument(
"apron::abstract0::abstract0(manager&, size_t, size_t, const interval_array&) array too short");
53 a = ap_abstract0_of_box(m.get_ap_manager_t(), intdim, realdim,
54 const_cast<ap_interval_t**
>(x.get_ap_interval_t_array()));
55 m.raise(
"apron::abstract0::abstract0(manager&, size_t, size_t, const interval_array&)",
a);
60 a = ap_abstract0_of_lincons_array(m.get_ap_manager_t(), intdim, realdim,
61 const_cast<ap_lincons0_array_t*
>(x.get_ap_lincons0_array_t()));
62 m.raise(
"apron::abstract0::abstract0(manager&, size_t, size_t, const lincons0_array&)",
a);
67 a = ap_abstract0_of_tcons_array(m.get_ap_manager_t(), intdim, realdim,
68 const_cast<ap_tcons0_array_t*
>(x.get_ap_tcons0_array_t()));
69 m.raise(
"apron::abstract0::abstract0(manager&, size_t, size_t, const tcons0_array&)",
a);
74 a = ap_abstract0_copy(t.a->man, t.a);
85 if (
a &&
a->value) ap_abstract0_free(
a->man,
a);
91 if (
a &&
a->value) ap_abstract0_free(m.get_ap_manager_t(),
a);
102 ap_abstract0_t* r = ap_abstract0_copy(
a->man, t.a);
103 manager::raise(
a->man,
"apron::abstract0::operator=(const abstract0&)",r);
104 ap_abstract0_free(
a->man,
a);
112 ap_dimension_t d = ap_abstract0_dimension(
a->man,
a);
113 ap_abstract0_t* r = ap_abstract0_top(
a->man, d.intdim, d.realdim);
115 ap_abstract0_free(
a->man,
a);
122 ap_dimension_t d = ap_abstract0_dimension(
a->man,
a);
123 ap_abstract0_t* r = ap_abstract0_bottom(
a->man, d.intdim, d.realdim);
125 ap_abstract0_free(
a->man,
a);
132 ap_dimension_t d = ap_abstract0_dimension(
a->man,
a);
133 if (x.size()<d.intdim+d.realdim)
134 throw std::invalid_argument(
"apron::abstract0::operator=(const interval_array&) array too short");
135 ap_abstract0_t* r = ap_abstract0_of_box(
a->man, d.intdim, d.realdim,
136 const_cast<ap_interval_t**>(x.get_ap_interval_t_array()));
137 manager::raise(
a->man,
"apron::abstract0::operator=(const interval_array&)",r);
138 ap_abstract0_free(
a->man,
a);
145 ap_dimension_t d = ap_abstract0_dimension(
a->man,
a);
147 ap_abstract0_of_lincons_array(
a->man, d.intdim, d.realdim,
148 const_cast<ap_lincons0_array_t*>(x.get_ap_lincons0_array_t()));
149 manager::raise(
a->man,
"apron::abstract0::operator=(const lincons0_array&)",r);
150 ap_abstract0_free(
a->man,
a);
157 ap_dimension_t d = ap_abstract0_dimension(
a->man,
a);
159 ap_abstract0_of_tcons_array(
a->man, d.intdim, d.realdim,
160 const_cast<ap_tcons0_array_t*>(x.get_ap_tcons0_array_t()));
161 manager::raise(
a->man,
"apron::abstract0::operator=(const tcons0_array&)",r);
162 ap_abstract0_free(
a->man,
a);
170 ap_abstract0_t* r = ap_abstract0_copy(m.get_ap_manager_t(), t.a);
171 m.raise(
"apron::abstract0::set(manager&, abstract0&)",r);
172 ap_abstract0_free(m.get_ap_manager_t(),
a);
180 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
181 if (intdim!=AP_DIM_MAX) d.intdim = intdim;
182 if (realdim!=AP_DIM_MAX) d.realdim = realdim;
183 ap_abstract0_t* r = ap_abstract0_top(m.get_ap_manager_t(), d.intdim, d.realdim);
184 m.raise(
"apron::abstract0::set(manager&, top, size_t, size_t)",r);
185 ap_abstract0_free(m.get_ap_manager_t(),
a);
192 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
193 if (intdim!=AP_DIM_MAX) d.intdim = intdim;
194 if (realdim!=AP_DIM_MAX) d.realdim = realdim;
195 ap_abstract0_t* r = ap_abstract0_bottom(m.get_ap_manager_t(), d.intdim, d.realdim);
196 m.raise(
"apron::abstract0::set(manager&, bottom, size_t, size_t)",r);
197 ap_abstract0_free(m.get_ap_manager_t(),
a);
204 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
205 if (intdim!=AP_DIM_MAX) d.intdim = intdim;
206 if (realdim!=AP_DIM_MAX) d.realdim = realdim;
207 if (x.size()<d.intdim+d.realdim)
208 throw std::invalid_argument(
"apron::abstract0::set(manager&, const interval_array&, size_t, size_t) array too short");
209 ap_abstract0_t* r = ap_abstract0_of_box(m.get_ap_manager_t(), d.intdim, d.realdim,
210 const_cast<ap_interval_t**
>(x.get_ap_interval_t_array()));
211 m.raise(
"apron::abstract0::set(manager&, const interval_array&, size_t, size_t)",r);
212 ap_abstract0_free(m.get_ap_manager_t(),
a);
219 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
220 if (intdim!=AP_DIM_MAX) d.intdim = intdim;
221 if (realdim!=AP_DIM_MAX) d.realdim = realdim;
223 ap_abstract0_of_lincons_array(m.get_ap_manager_t(), d.intdim, d.realdim,
224 const_cast<ap_lincons0_array_t*
>(x.get_ap_lincons0_array_t()));
225 m.raise(
"apron::abstract0::set(manager&, const lincons0_array&, size_t, size_t)",r);
226 ap_abstract0_free(m.get_ap_manager_t(),
a);
233 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
234 if (intdim!=AP_DIM_MAX) d.intdim = intdim;
235 if (realdim!=AP_DIM_MAX) d.realdim = realdim;
237 ap_abstract0_of_tcons_array(m.get_ap_manager_t(), d.intdim, d.realdim,
238 const_cast<ap_tcons0_array_t*
>(x.get_ap_tcons0_array_t()));
239 m.raise(
"apron::abstract0::set(manager&, const tcons0_array&, size_t, size_t)",r);
240 ap_abstract0_free(m.get_ap_manager_t(),
a);
251 ap_abstract0_minimize(m.get_ap_manager_t(),
a);
252 m.raise(
"abstract0::minimize(manager&)");
258 ap_abstract0_canonicalize(m.get_ap_manager_t(),
a);
259 m.raise(
"apron::abstract0::canonicalize(manager&)");
265 ap_abstract0_approximate(m.get_ap_manager_t(),
a, algorithm);
266 m.raise(
"apron::abstract0::approximate(manager&, int)");
276 ap_abstract0_fprint(stream, m.get_ap_manager_t(),
a, name_of_dim);
277 m.raise(
"apron::abstract0::print(manager&, char**, FILE*)");
282 ap_abstract0_fprintdiff(stream, m.get_ap_manager_t(), x.a, y.a, name_of_dim);
283 m.raise(
"apron::printdiff(manager&, const abstract0&, const abstract0&, char**, FILE*)");
288 ap_abstract0_fdump(stream, m.get_ap_manager_t(),
a);
289 m.raise(
"apron::abstract0::dump(manager&, FILE*)");
295 if (s.is_bottom(m))
return os <<
"bottom";
296 if (s.is_top(m))
return os <<
"top";
297 return os << s.to_lincons_array(m);
306 ap_membuf_t x = ap_abstract0_serialize_raw(m.get_ap_manager_t(),
a);
307 m.raise(
"apron::abstract0::serialize_raw(manager&)");
308 std::string* s =
new std::string((
char*)x.ptr, x.size);
316 ap_abstract0_t* r = ap_abstract0_deserialize_raw(m.get_ap_manager_t(),
const_cast<char*
>(s.data()), &x);
317 m.raise(
"apron::deserialize_raw(manager&, abstract0&, const std::string&, size_t*)",r);
318 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
320 if (eaten) *eaten = x;
330 return ap_manager_copy(ap_abstract0_manager(
a));
335 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
336 m.raise(
"apron::abstract0::get_dimension(manager&)");
342 size_t sz = ap_abstract0_size(m.get_ap_manager_t(),
a);
343 m.raise(
"apron::abstract0::get_size(manager&)");
354 bool r = ap_abstract0_is_bottom(m.get_ap_manager_t(),
a);
355 m.raise(
"apron::abstract0::is_bottom(manager&)");
361 bool r = ap_abstract0_is_top(m.get_ap_manager_t(),
a);
362 m.raise(
"apron::abstract0::is_top(manager&)");
368 bool r = ap_abstract0_is_eq(m.get_ap_manager_t(),
a, x.a);
369 m.raise(
"apron::abstract0::is_eq(manager&, const abstract&)");
375 bool r = ap_abstract0_is_leq(m.get_ap_manager_t(),
a, x.a);
376 m.raise(
"apron::abstract0::is_leq(manager&, const abstract&)");
382 bool r = ap_abstract0_sat_lincons(m.get_ap_manager_t(),
a,
const_cast<ap_lincons0_t*
>(l.get_ap_lincons0_t()));
383 m.raise(
"apron::abstract0::sat(manager&, const lincons0&)");
389 bool r = ap_abstract0_sat_tcons(m.get_ap_manager_t(),
a,
const_cast<ap_tcons0_t*
>(l.get_ap_tcons0_t()));
390 m.raise(
"apron::abstract0::sat(manager&, const tcons0&)");
396 bool r = ap_abstract0_sat_interval(m.get_ap_manager_t(),
a, dim,
const_cast<ap_interval_t*
>(i.get_ap_interval_t()));
397 m.raise(
"apron::abstract0::sat(manager&, ap_dim_t, const interval&)");
403 bool r = ap_abstract0_is_dimension_unconstrained(m.get_ap_manager_t(),
a, dim);
404 m.raise(
"apron::abstract0::is_dimension_unconstrained(manager&, ap_dim_t)");
411 bool r = ap_abstract0_is_eq(x.a->man, x.a, y.a);
412 manager::raise(x.a->man,
"apron::operator==(const abstract0&, const abstract0&)");
423 bool r = ap_abstract0_is_leq(x.a->man, x.a, y.a);
424 manager::raise(x.a->man,
"apron::operator<=(const abstract0&, const abstract0&)");
450 ap_abstract0_bound_linexpr(m.get_ap_manager_t(),
a,
451 const_cast<ap_linexpr0_t*
>(l.get_ap_linexpr0_t()));
452 if (m.exception_raised()) ap_interval_free(r);
453 m.raise(
"apron::abstract0::bound(manager&, const linexpr0&)");
460 ap_abstract0_bound_texpr(m.get_ap_manager_t(),
a,
461 const_cast<ap_texpr0_t*
>(l.get_ap_texpr0_t()));
462 if (m.exception_raised()) ap_interval_free(r);
463 m.raise(
"apron::abstract0::bound(manager&, const texpr0&)");
469 ap_interval_t* r = ap_abstract0_bound_dimension(m.get_ap_manager_t(),
a, d);
470 if (m.exception_raised()) ap_interval_free(r);
471 m.raise(
"apron::abstract0::bound(manager&, ap_dim_t)");
477 ap_dimension_t d = ap_abstract0_dimension(m.get_ap_manager_t(),
a);
478 ap_interval_t** r = ap_abstract0_to_box(m.get_ap_manager_t(),
a);
479 m.raise(
"apron::abstract0::to_box(manager&)");
480 return interval_array(d.intdim+d.realdim, r);
485 ap_lincons0_array_t r = ap_abstract0_to_lincons_array(m.get_ap_manager_t(),
a);
486 if (m.exception_raised()) ap_lincons0_array_clear(&r);
487 m.raise(
"apron::abstract0::to_lincons_array(manager&)");
493 ap_tcons0_array_t r = ap_abstract0_to_tcons_array(m.get_ap_manager_t(),
a);
494 if (m.exception_raised()) ap_tcons0_array_clear(&r);
495 m.raise(
"apron::abstract0::to_tcons_array(manager&)");
501 ap_generator0_array_t r = ap_abstract0_to_generator_array(m.get_ap_manager_t(),
a);
502 if (m.exception_raised()) ap_generator0_array_clear(&r);
503 m.raise(
"apron::abstract0::to_generator_array(manager&)");
513 a = ap_abstract0_meet(m.get_ap_manager_t(),
true,
a, y.a);
514 m.raise(
"apron::abstract0::meet(manager&, const abstract0&)");
520 ap_abstract0_t* r = ap_abstract0_meet(m.get_ap_manager_t(),
false, x.a, y.a);
521 m.raise(
"apron::meet(manager&, abstract0&, const abstract0&, const abstract0&)",r);
522 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
529 ap_abstract0_t* xx[x.size()];
530 for (
size_t i=0;i<x.size();i++)
533 ap_abstract0_meet_array(m.get_ap_manager_t(), xx, x.size());
534 m.raise(
"apron::meet(manager&, abstract0&, const std::vector<const abstract0*>&)",r);
535 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
542 ap_abstract0_t* xx[sz];
543 for (
size_t i=0;i<sz;i++)
546 ap_abstract0_meet_array(m.get_ap_manager_t(), xx, sz);
547 m.raise(
"apron::meet(manager&, abstract0&, size_t, const abstract0 * const [])",r);
548 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
555 a = ap_abstract0_join(m.get_ap_manager_t(),
true,
a, y.a);
556 m.raise(
"apron::abstract0::join(manager&, const abstract0&)");
562 ap_abstract0_t* r = ap_abstract0_join(m.get_ap_manager_t(),
false, x.a, y.a);
563 m.raise(
"apron::join(manager&, abstract0&, const abstract0&, const abstract0&)",r);
564 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
571 ap_abstract0_t* xx[sz];
572 for (
size_t i=0;i<sz;i++)
575 ap_abstract0_join_array(m.get_ap_manager_t(), xx, sz);
576 m.raise(
"apron::join(manager&, abstract0&, size_t, const abstract0 * const [])",r);
577 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
584 ap_abstract0_t* xx[x.size()];
585 for (
size_t i=0;i<x.size();i++)
588 ap_abstract0_join_array(m.get_ap_manager_t(), xx, x.size());
589 m.raise(
"apron::join(manager&, abstract0&, const std::vector<const abstract0*>&)",r);
590 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
597 a = ap_abstract0_meet_lincons_array(m.get_ap_manager_t(),
true,
a,
598 const_cast<ap_lincons0_array_t*
>(y.get_ap_lincons0_array_t()));
599 m.raise(
"apron::abstract0::meet(manager&, const lincons0_array&)");
606 ap_abstract0_meet_lincons_array(m.get_ap_manager_t(),
false, x.a,
607 const_cast<ap_lincons0_array_t*
>(y.get_ap_lincons0_array_t()));
608 m.raise(
"apron::meet(manager&, abstract0&, const abstract0&, const lincons0_array&)",r);
609 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
617 a = ap_abstract0_meet_tcons_array(m.get_ap_manager_t(),
true,
a,
618 const_cast<ap_tcons0_array_t*
>(y.get_ap_tcons0_array_t()));
619 m.raise(
"apron::abstract0::meet(manager&, const tcons0_array&)");
626 ap_abstract0_meet_tcons_array(m.get_ap_manager_t(),
false, x.a,
627 const_cast<ap_tcons0_array_t*
>(y.get_ap_tcons0_array_t()));
628 m.raise(
"apron::meet(manager&, abstract0&, const abstract0&, const tcons0_array&)",r);
629 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
638 a = ap_abstract0_add_ray_array(m.get_ap_manager_t(),
true,
a,
639 const_cast<ap_generator0_array_t*
>(y.get_ap_generator0_array_t()));
640 m.raise(
"apron::abstract0::add_rays(manager&, const generator0_array&)");
647 ap_abstract0_add_ray_array(m.get_ap_manager_t(),
false, x.a,
648 const_cast<ap_generator0_array_t*
>(y.get_ap_generator0_array_t()));
649 m.raise(
"apron::add_rays(manager&, abstract0&, const abstract0&, const generator0_array&)",r);
650 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
659 a = ap_abstract0_meet(
a->man,
true,
a, y.a);
660 manager::raise(
a->man,
"apron::abstract0::operator*=(const abstract0&)");
666 a = ap_abstract0_join(
a->man,
true,
a, y.a);
667 manager::raise(
a->man,
"apron::abstract0::operator+=(const abstract0&)");
673 a = ap_abstract0_meet_lincons_array(
a->man,
true,
a,
674 const_cast<ap_lincons0_array_t*>(y.get_ap_lincons0_array_t()));
675 manager::raise(
a->man,
"apron::abstract0::operator*=(const lincons0_array&)");
681 a = ap_abstract0_meet_tcons_array(
a->man,
true,
a,
682 const_cast<ap_tcons0_array_t*>(y.get_ap_tcons0_array_t()));
683 manager::raise(
a->man,
"apron::abstract0::operator*=(const tcons0_array&)");
689 a = ap_abstract0_add_ray_array(
a->man,
true,
a,
690 const_cast<ap_generator0_array_t*>(y.get_ap_generator0_array_t()));
691 manager::raise(
a->man,
"apron::abstract0::operator+=(const generator0_array&)");
701 const linexpr0* ll = &l;
702 return assign(m, 1, &dim, &ll, inter);
707 a = ap_abstract0_assign_linexpr_array(m.get_ap_manager_t(),
true,
a,
708 const_cast<ap_dim_t*
>(dim),
709 reinterpret_cast<ap_linexpr0_t**>(const_cast<linexpr0**>(l)),
711 m.raise(
"apron::abstract0::assign(manager&, size_t size, const ap_dim_t[], const linexpr0 * const [], const abstract0&)");
717 if (l.size()!=dim.size())
718 throw std::invalid_argument(
"apron::abstract0::assign(manager&, const std::vector<ap_dim_t>&, const std::vector<const linexpr0*>&, const abstract0&) vectors have different size");
719 const linexpr0* ll[l.size()];
720 ap_dim_t dd[dim.size()];
721 for (
size_t i=0;i<l.size();i++) {
725 return assign(m, l.size(), dd, ll, inter);
730 const linexpr0* ll = &l;
731 return assign(m, dst, src, 1, &dim, &ll, inter);
737 ap_abstract0_assign_linexpr_array(m.get_ap_manager_t(),
false, src.a,
738 const_cast<ap_dim_t*
>(dim),
739 reinterpret_cast<ap_linexpr0_t**>(const_cast<linexpr0**>(l)),
741 m.raise(
"apron::assign((manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[], const linexpr0 * const [], const abstract0&)",r);
742 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
749 if (l.size()!=dim.size())
750 throw std::invalid_argument(
"apron::assign(manager&, abstract0, const abstract0&, const std::vector<ap_dim_t>&, const std::vector<const linexpr0*>&, const abstract0&) vectors have different size");
751 const linexpr0* ll[l.size()];
752 ap_dim_t dd[dim.size()];
753 for (
size_t i=0;i<l.size();i++) {
757 return assign(m, dst, src, l.size(), dd, ll, inter);
766 const texpr0* ll = &l;
767 return assign(m, 1, &dim, &ll, inter);
772 a = ap_abstract0_assign_texpr_array(m.get_ap_manager_t(),
true,
a,
773 const_cast<ap_dim_t*
>(dim),
774 reinterpret_cast<ap_texpr0_t**>(const_cast<texpr0**>(l)),
776 m.raise(
"apron::abstract0::assign(manager&, size_t size, const ap_dim_t[], const texpr0 * const [], const abstract0&)");
782 if (l.size()!=dim.size())
783 throw std::invalid_argument(
"apron::abstract0::assign(manager&, const std::vector<ap_dim_t>&, const std::vector<const texpr0*>&, const abstract0&) vectors have different size");
784 const texpr0* ll[l.size()];
785 ap_dim_t dd[dim.size()];
786 for (
size_t i=0;i<l.size();i++) {
790 return assign(m, l.size(), dd, ll, inter);
795 const texpr0* ll = &l;
796 return assign(m, dst, src, 1, &dim, &ll, inter);
802 ap_abstract0_assign_texpr_array(m.get_ap_manager_t(),
false, src.a,
803 const_cast<ap_dim_t*
>(dim),
804 reinterpret_cast<ap_texpr0_t**>(const_cast<texpr0**>(l)),
806 m.raise(
"apron::assign((manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[], const texpr0 * const [], const abstract0&)",r);
807 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
814 if (l.size()!=dim.size())
815 throw std::invalid_argument(
"apron::assign(manager&, abstract0, const abstract0&, const std::vector<ap_dim_t>&, const std::vector<const texpr0*>&, const abstract0&) vectors have different size");
816 const texpr0* ll[l.size()];
817 ap_dim_t dd[dim.size()];
818 for (
size_t i=0;i<l.size();i++) {
822 return assign(m, dst, src, l.size(), dd, ll, inter);
832 const linexpr0* ll = &l;
838 a = ap_abstract0_substitute_linexpr_array(m.get_ap_manager_t(),
true,
a,
839 const_cast<ap_dim_t*
>(dim),
840 reinterpret_cast<ap_linexpr0_t**>(const_cast<linexpr0**>(l)),
842 m.raise(
"apron::abstract0::substitute(manager&, size_t size, const ap_dim_t[], const linexpr0 * const [], const abstract0&)");
848 if (l.size()!=dim.size())
849 throw std::invalid_argument(
"apron::abstract0::substitute(manager&, const std::vector<ap_dim_t>&, const std::vector<const linexpr0*>&, const abstract0&) vectors have different size");
850 const linexpr0* ll[l.size()];
851 ap_dim_t dd[dim.size()];
852 for (
size_t i=0;i<l.size();i++) {
856 return substitute(m, l.size(), dd, ll, inter);
861 const linexpr0* ll = &l;
862 return substitute(m, dst, src, 1, &dim, &ll, inter);
868 ap_abstract0_substitute_linexpr_array(m.get_ap_manager_t(),
false, src.a,
869 const_cast<ap_dim_t*
>(dim),
870 reinterpret_cast<ap_linexpr0_t**>(const_cast<linexpr0**>(l)),
872 m.raise(
"apron::substitute((manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[], const linexpr0 *const [], const abstract0&)",r);
873 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
880 if (l.size()!=dim.size())
881 throw std::invalid_argument(
"apron::substitute(manager&, abstract0, const abstract0&, const std::vector<ap_dim_t>&, const std::vector<const linexpr0*>&, const abstract0&) vectors have different size");
882 const linexpr0* ll[l.size()];
883 ap_dim_t dd[dim.size()];
884 for (
size_t i=0;i<l.size();i++) {
888 return substitute(m, dst, src, l.size(), dd, ll, inter);
897 const texpr0* ll = &l;
903 a = ap_abstract0_substitute_texpr_array(m.get_ap_manager_t(),
true,
a,
904 const_cast<ap_dim_t*
>(dim),
905 reinterpret_cast<ap_texpr0_t**>(const_cast<texpr0**>(l)),
907 m.raise(
"apron::abstract0::substitute(manager&, size_t size, const ap_dim_t[], const texpr0 * const [], const abstract0&)");
913 if (l.size()!=dim.size())
914 throw std::invalid_argument(
"apron::abstract0::substitute(manager&, const std::vector<ap_dim_t>&, const std::vector<const texpr0*>&, const abstract0&) vectors have different size");
915 const texpr0* ll[l.size()];
916 ap_dim_t dd[dim.size()];
917 for (
size_t i=0;i<l.size();i++) {
921 return substitute(m, l.size(), dd, ll, inter);
926 const texpr0* ll = &l;
927 return substitute(m, dst, src, 1, &dim, &ll, inter);
933 ap_abstract0_substitute_texpr_array(m.get_ap_manager_t(),
false, src.a,
934 const_cast<ap_dim_t*
>(dim),
935 reinterpret_cast<ap_texpr0_t**>(const_cast<texpr0**>(l)),
937 m.raise(
"apron::substitute((manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[], const texpr0 * const [], const abstract0&)",r);
938 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
945 if (l.size()!=dim.size())
946 throw std::invalid_argument(
"apron::substitute(manager&, abstract0, const abstract0&, const std::vector<ap_dim_t>&, const std::vector<const texpr0*>&, const abstract0&) vectors have different size");
947 const texpr0* ll[l.size()];
948 ap_dim_t dd[dim.size()];
949 for (
size_t i=0;i<l.size();i++) {
953 return substitute(m, dst, src, l.size(), dd, ll, inter);
964 return forget(m, 1, &dim, project);
969 a = ap_abstract0_forget_array(m.get_ap_manager_t(),
true,
a,
970 const_cast<ap_dim_t*
>(dim),
972 m.raise(
"apron::abstract0::substitute(orget(manager&, size_t size, const ap_dim_t[], bool)");
978 ap_dim_t dd[dim.size()];
979 for (
size_t i=0;i<dim.size();i++) dd[i] = dim[i];
980 return forget(m, dim.size(), dd, project);
985 return forget(m, dst, src, 1, &dim, project);
991 ap_abstract0_forget_array(m.get_ap_manager_t(),
false, src.a,
992 const_cast<ap_dim_t*
>(dim),
994 m.raise(
"apron::forget(manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[], bool)",r);
995 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1002 ap_dim_t dd[dim.size()];
1003 for (
size_t i=0;i<dim.size();i++) dd[i] = dim[i];
1004 return forget(m, dst, src, dim.size(), dd, project);
1013 a = ap_abstract0_add_dimensions(m.get_ap_manager_t(),
true,
a,
1014 const_cast<ap_dimchange_t*
>(d.get_ap_dimchange_t()),
1016 m.raise(
"apron::abstract0::add_dimensions(manager&, const dimchange&, bool)");
1023 a = ap_abstract0_remove_dimensions(m.get_ap_manager_t(),
true,
a,
1024 const_cast<ap_dimchange_t*
>(d.get_ap_dimchange_t()));
1025 m.raise(
"apron::abstract0::remove_dimensions(manager&, const dimchange&)");
1031 a = ap_abstract0_permute_dimensions(m.get_ap_manager_t(),
true,
a,
1032 const_cast<ap_dimperm_t*
>(d.get_ap_dimperm_t()));
1033 m.raise(
"apron::abstract0::permute_dimensions(manager&, const dimperm&)");
1040 ap_abstract0_add_dimensions(m.get_ap_manager_t(),
false, src.a,
1041 const_cast<ap_dimchange_t*
>(d.get_ap_dimchange_t()),
1043 m.raise(
"apron::add_dimensions(manager&, abstract0&, const abstract0&, const dimchange&, bool)",r);
1044 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1052 ap_abstract0_remove_dimensions(m.get_ap_manager_t(),
false, src.a,
1053 const_cast<ap_dimchange_t*
>(d.get_ap_dimchange_t()));
1054 m.raise(
"apron::remove_dimensions(manager&, abstract0&, const abstract0&, const dimchange&)",r);
1055 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1063 ap_abstract0_permute_dimensions(m.get_ap_manager_t(),
false, src.a,
1064 const_cast<ap_dimperm_t*
>(d.get_ap_dimperm_t()));
1065 m.raise(
"apron::permute_dimensions(manager&, abstract0&, const abstract0&, const dimperm&)",r);
1066 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1078 a = ap_abstract0_expand(m.get_ap_manager_t(),
true,
a, dim, n);
1079 m.raise(
"apron::abstract0::expand(manager&, ap_dim_t, size_t)");
1085 ap_abstract0_t* r = ap_abstract0_expand(m.get_ap_manager_t(),
false, src.a, dim, n);
1086 m.raise(
"apron::expand(manager&, abstract0&, const abstract0&, ap_dim_t, size_t)",r);
1087 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1094 a = ap_abstract0_fold(m.get_ap_manager_t(),
true,
a,
const_cast<ap_dim_t*
>(dim), size);
1095 m.raise(
"apron::abstract0::fold(manager&, size_t size, const ap_dim_t[])");
1101 ap_dim_t dd[dim.size()];
1102 for (
size_t i=0;i<dim.size();i++) dd[i] = dim[i];
1103 return fold(m, dim.size(), dd);
1109 ap_abstract0_fold(m.get_ap_manager_t(),
false, src.a,
const_cast<ap_dim_t*
>(dim), size);
1110 m.raise(
"apron::fold(manager&, abstract0&, const abstract0&, size_t size, const ap_dim_t[])",r);
1111 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1118 ap_dim_t dd[dim.size()];
1119 for (
size_t i=0;i<dim.size();i++) dd[i] = dim[i];
1120 return fold(m, dst, src, dim.size(), dd);
1129 ap_abstract0_t* r = ap_abstract0_widening(m.get_ap_manager_t(), x.a, y.a);
1130 m.raise(
"apron::wideningg(manager&, abstract0&, const abstract0&, const abstract0&)",r);
1131 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1139 ap_abstract0_widening_threshold(m.get_ap_manager_t(), x.a, y.a,
1140 const_cast<ap_lincons0_array_t*
>(l.get_ap_lincons0_array_t()));
1141 m.raise(
"apron::widening(manager&, abstract0&, const abstract0&, const abstract0&, const lincons0_array&)",r);
1142 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
1153 a = ap_abstract0_closure(m.get_ap_manager_t(),
true,
a);
1154 m.raise(
"apron::abstract0::closured(manager&)");
1160 ap_abstract0_t* r = ap_abstract0_closure(m.get_ap_manager_t(),
false, src.a);
1161 m.raise(
"apron::closure(manager&, abstract0&, const abstract0&)",r);
1162 ap_abstract0_free(m.get_ap_manager_t(), dst.a);
abstract0 & add_rays(manager &m, const generator0_array &y)
Adds some rays to *this (modified in-place).
Definition: apxx_abstract0.hh:637
abstract0 & fold(manager &m, size_t size, const ap_dim_t dim[])
Folds dimensions dim[0] to dim[size-1] in *this (modified in-place).
Definition: apxx_abstract0.hh:1093
friend bool operator<=(const abstract0 &x, const abstract0 &y)
Whether x is included within y (set-wise).
Definition: apxx_abstract0.hh:422
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition: apxx_abstract0.hh:353
abstract0 & set(manager &m, const abstract0 &x)
Replaces *this with a copy of x.
Definition: apxx_abstract0.hh:168
friend std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Prints in constraint form.
Definition: apxx_abstract0.hh:293
abstract0 & assign(manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
In-place assignment of linear expression.
Definition: apxx_abstract0.hh:700
friend bool operator>=(const abstract0 &x, const abstract0 &y)
Whether x contains y (set-wise).
Definition: apxx_abstract0.hh:429
friend bool operator==(const abstract0 &x, const abstract0 &y)
Whether x and y represent the same set.
Definition: apxx_abstract0.hh:410
ap_abstract0_t * a
Pointer managed by APRON.
Definition: apxx_abstract0.hh:82
bool is_dimension_unconstrained(manager &m, ap_dim_t dim) const
Whether the points in *this are unbounded in the given dimension.
Definition: apxx_abstract0.hh:402
bool sat(manager &m, const lincons0 &l) const
Whether all points in *this satisfy a linear constraint.
Definition: apxx_abstract0.hh:381
abstract0 & expand(manager &m, ap_dim_t dim, size_t n=1)
Duplicates dimension dim into n copies in *this (modified in-place).
Definition: apxx_abstract0.hh:1077
generator0_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition: apxx_abstract0.hh:500
friend bool operator<(const abstract0 &x, const abstract0 &y)
Whether x is strictly included within y (set-wise).
Definition: apxx_abstract0.hh:439
abstract0 & operator*=(const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract0.hh:658
abstract0 & forget(manager &m, ap_dim_t dim, bool project=false)
Forgets about the value of dimension dim in *this.
Definition: apxx_abstract0.hh:963
abstract0 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition: apxx_abstract0.hh:257
abstract0 & operator+=(const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract0.hh:665
friend abstract0 & deserialize(manager &m, abstract0 &dst, const std::string &s, size_t *eaten)
Reconstruct an abstract element form a serialized byte-stream and put it into dst.
Definition: apxx_abstract0.hh:314
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition: apxx_abstract0.hh:341
friend bool operator!=(const abstract0 &x, const abstract0 &y)
Whether x and y represent different sets.
Definition: apxx_abstract0.hh:417
abstract0 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition: apxx_abstract0.hh:264
ap_dimension_t get_dimension(manager &m) const
Returns the number of integer and real dimensions in the abstract element.
Definition: apxx_abstract0.hh:334
abstract0 & join(manager &m, const abstract0 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract0.hh:554
abstract0 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition: apxx_abstract0.hh:250
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition: apxx_abstract0.hh:287
abstract0 & remove_dimensions(manager &m, const dimchange &d)
Removes some dimensions from *this.
Definition: apxx_abstract0.hh:1022
friend class manager
Definition: apxx_abstract0.hh:90
interval bound(manager &m, const linexpr0 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element...
Definition: apxx_abstract0.hh:448
abstract0 & substitute(manager &m, ap_dim_t dim, const linexpr0 &l, const abstract0 &inter=null)
In-place substitution (backward assignment) of linear expression.
Definition: apxx_abstract0.hh:831
friend void printdiff(manager &m, const abstract0 &x, const abstract0 &y, char **name_of_dim, FILE *stream)
Pretty-printing the difference between x and y to a C stream.
Definition: apxx_abstract0.hh:281
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_abstract0.hh:1173
bool is_top(manager &m) const
Whether *this represents the full space.
Definition: apxx_abstract0.hh:360
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition: apxx_abstract0.hh:329
void free(manager &m)
Destroys the abstract element using the given manager.
Definition: apxx_abstract0.hh:90
~abstract0()
Destroys the abstract element.
Definition: apxx_abstract0.hh:84
abstract0 & permute_dimensions(manager &m, const dimperm &d)
Permutes some dimensions in *this.
Definition: apxx_abstract0.hh:1030
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition: apxx_abstract0.hh:476
abstract0 & meet(manager &m, const abstract0 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract0.hh:512
abstract0(ap_abstract0_t *x)
Internal use only. Wraps an abstract0 around the pointer x, taking ownership of the object...
Definition: apxx_abstract0.hh:28
friend bool operator>(const abstract0 &x, const abstract0 &y)
Whether x strictly contains y (set-wise).
Definition: apxx_abstract0.hh:434
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.hh:89
abstract0 & add_dimensions(manager &m, const dimchange &d, bool project=false)
Adds some dimensions to *this.
Definition: apxx_abstract0.hh:1012
void print(manager &m, char **name_of_dim=NULL, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition: apxx_abstract0.hh:275
friend abstract0 & widening(manager &m, abstract0 &dst, const abstract0 &x, const abstract0 &y)
Stores in dst the result of x widened with y.
Definition: apxx_abstract0.hh:1128
static const abstract0 null
NULL abstract element, to be used only as default argument in assign and substitute.
Definition: apxx_abstract0.hh:88
bool is_eq(manager &m, const abstract0 &x) const
Whether *this and x represent the same set.
Definition: apxx_abstract0.hh:367
bool is_leq(manager &m, const abstract0 &x) const
Whether *this is included in x (set-wise).
Definition: apxx_abstract0.hh:374
abstract0 & closure(manager &m)
Replaces *this with its topological closure.
Definition: apxx_abstract0.hh:1152
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition: apxx_abstract0.hh:305
abstract0 & operator=(const abstract0 &t)
Assigns a copy of t to *this.
Definition: apxx_abstract0.hh:100
lincons0_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition: apxx_abstract0.hh:484
tcons0_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition: apxx_abstract0.hh:492