27 inline abstract1::abstract1(ap_abstract1_t x) : a(x)
34 m.
raise(
"apron::abstract1::abstract1(manager &, const environment&, top)",
a);
41 m.
raise(
"apron::abstract1::abstract1(manager &, const environment&, bottom)",
a);
47 m.
raise(
"apron::abstract1::abstract1(manager &, const abstract1&)",
a);
55 m.
raise(
"apron::abstract1::abstract1(manager &, const abstract1&)",
a);
62 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(v)),
65 m.
raise(
"apron::abstract1::abstract1(manager &, const environment&, const var[], const interval_array&)",
a);
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();
79 m.
raise(
"apron::abstract1::abstract1(manager &, const environment&, const std::vector<var>&, const interval_array&)",
a);
87 m.
raise(
"apron::abstract1::abstract1(manager &, const lincons1_array&)",
a);
95 m.
raise(
"apron::abstract1::abstract1(manager &, const tcons1_array&)",
a);
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);
110 if (
a.abstract0) ap_abstract1_clear(
a.abstract0->man, &
a);
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);
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);
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);
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,
161 manager::raise(
a.abstract0->man,
"apron::abstract1::operator=(const interval_array&)",r);
162 ap_abstract0_free(
a.abstract0->man,
a.abstract0);
170 ap_abstract1_of_lincons_array(
a.abstract0->man,
173 manager::raise(
a.abstract0->man,
"apron::abstract1::operator=(const lincons1_array&)",r);
174 ap_abstract1_clear(
a.abstract0->man, &
a);
182 ap_abstract1_of_tcons_array(
a.abstract0->man,
185 manager::raise(
a.abstract0->man,
"apron::abstract1::operator=(const tcons1_array&)",r);
186 ap_abstract1_clear(
a.abstract0->man, &
a);
196 const_cast<ap_abstract1_t*
>(&x.
a));
197 m.
raise(
"apron::abstract1::set(manager&, abstract1&)",r);
208 m.
raise(
"apron::abstract1::set(manager&, top)",r);
218 m.
raise(
"apron::abstract1::set(manager&, const environment&, top)",r);
227 m.
raise(
"apron::abstract1::set(manager&, bottom)",r);
237 m.
raise(
"apron::abstract1::set(manager&, const environment&, bottom)",r);
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,
250 m.
raise(
"apron::abstract1::operator=(const interval_array&)",r);
262 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(v)),
265 m.
raise(
"apron::abstract1::set(manager &, const environment&, const var[], const interval_array&)",r);
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();
283 m.
raise(
"apron::abstract1::set(manager &, const environment&, const std::vector<var>&, const interval_array&)",r);
295 m.
raise(
"apron::abstract1::set(manager &, const lincons1_array&)",r);
307 m.
raise(
"apron::abstract1::set(manager &, const tcons1_array&)",r);
320 m.
raise(
"apron::abstract1::minimize(manager &)");
327 m.
raise(
"apron::abstract1::canonicalize(manager &)");
334 m.
raise(
"apron::abstract1::approximate(manager &, int)");
344 ap_abstract1_fprint(stream, m.
get_ap_manager_t(),
const_cast<ap_abstract1_t*
>(&
a));
345 m.
raise(
"apron::abstract1::print(manager&, FILE*)");
348 inline void printdiff(manager& m,
const abstract1& x,
const abstract1& y, FILE* stream = stdout)
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*)");
358 ap_abstract1_fdump(stream, m.
get_ap_manager_t(),
const_cast<ap_abstract1_t*
>(&
a));
359 m.
raise(
"apron::abstract1::dump(manager&, FILE*)");
362 inline std::ostream&
operator<< (std::ostream& os,
const abstract1& s)
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);
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);
384 inline abstract1&
deserialize(manager& m, abstract1& dst,
const std::string& s,
size_t* eaten = NULL)
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);
392 if (eaten) *eaten = x;
402 return ap_manager_copy(ap_abstract0_manager(
const_cast<ap_abstract0_t*
>(
a.abstract0)));
407 return ap_environment_copy(
const_cast<ap_environment_t*
>(
a.env));
412 return reinterpret_cast<abstract0&
>(
a.abstract0);
417 return reinterpret_cast<const abstract0&
>(
a.abstract0);
423 const_cast<ap_abstract1_t*
>(&
a));
424 m.
raise(
"apron::abstract1::get_size(manager&)");
437 const_cast<ap_abstract1_t*
>(&
a));
438 m.
raise(
"apron::abstract1::is_bottom(manager&)");
445 const_cast<ap_abstract1_t*
>(&
a));
446 m.
raise(
"apron::abstract1::is_top(manager&)");
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&)");
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&)");
471 const_cast<ap_abstract1_t*
>(&
a),
473 m.
raise(
"apron::abstract1::sat(manager&, const lincons1&)");
480 const_cast<ap_abstract1_t*
>(&
a),
482 m.
raise(
"apron::abstract1::sat(manager&, const tcons1&)");
489 const_cast<ap_abstract1_t*
>(&
a),
492 m.
raise(
"apron::abstract1::sat(manager&, const var&, const interval&)");
499 const_cast<ap_abstract1_t*
>(&
a),
501 m.
raise(
"apron::abstract1::is_variable_unconstrained(manager&, const var&)");
506 inline bool operator== (
const abstract1& x,
const abstract1& y)
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&)");
515 inline bool operator!= (
const abstract1& x,
const abstract1& y)
520 inline bool operator<= (
const abstract1& x,
const abstract1& y)
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&)");
529 inline bool operator>= (
const abstract1& x,
const abstract1& y)
534 inline bool operator> (
const abstract1& x,
const abstract1& y)
539 inline bool operator< (
const abstract1& x,
const abstract1& y)
553 const_cast<ap_abstract1_t*
>(&
a),
555 m.
raise(
"apron::abstract1::bound(manager&, const linexpr1&)");
563 const_cast<ap_abstract1_t*
>(&
a),
566 m.
raise(
"apron::abstract1::bound(manager&, const texpr1&)");
574 const_cast<ap_abstract1_t*
>(&
a),
577 m.
raise(
"apron::abstract1::bound(manager&, ap_dim_t)");
585 const_cast<ap_abstract1_t*
>(&
a));
587 m.
raise(
"apron::abstract1::to_box(manager&)");
588 size_t sz = r.env->intdim + r.env->realdim;
589 ap_environment_free(r.env);
595 ap_lincons1_array_t r =
597 const_cast<ap_abstract1_t*
>(&
a));
599 m.
raise(
"apron::abstract1::to_lincons_array(manager&)");
605 ap_tcons1_array_t r =
607 const_cast<ap_abstract1_t*
>(&
a));
609 m.
raise(
"apron::abstract1::to_tcons_array(manager&)");
615 ap_generator1_array_t r =
617 const_cast<ap_abstract1_t*
>(&
a));
619 m.
raise(
"apron::abstract1::to_generator_array(manager&)");
630 const_cast<ap_abstract1_t*
>(&
a),
631 const_cast<ap_abstract1_t*
>(&y.
a));
632 m.
raise(
"apron::abstract1::unify(manager&, const abstract1&)");
636 inline abstract1&
unify(manager& m, abstract1& dst,
const abstract1& x,
const abstract1& y)
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);
651 const_cast<ap_abstract1_t*
>(&
a),
652 const_cast<ap_abstract1_t*
>(&y.
a));
653 m.
raise(
"apron::abstract1::meet(manager&, const abstract1&)");
657 inline abstract1&
meet(manager& m, abstract1& dst,
const abstract1& x,
const abstract1& y)
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);
669 inline abstract1&
meet(manager& m, abstract1& dst,
const std::vector<const abstract1*>& x)
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());
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);
682 inline abstract1&
meet(manager& m, abstract1& dst,
size_t sz,
const abstract1 *
const x[])
684 ap_abstract1_t xx[sz];
685 for (
size_t i=0;i<sz;i++)
686 xx[i] = *(x[i]->get_ap_abstract1_t());
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);
698 const_cast<ap_abstract1_t*
>(&
a),
699 const_cast<ap_abstract1_t*
>(&y.
a));
700 m.
raise(
"apron::abstract1::join(manager&, const abstract1&)");
704 inline abstract1&
join(manager& m, abstract1& dst,
const abstract1& x,
const abstract1& y)
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);
716 inline abstract1&
join(manager& m, abstract1& dst,
size_t sz,
const abstract1 *
const x[])
718 ap_abstract1_t xx[sz];
719 for (
size_t i=0;i<sz;i++)
720 xx[i] = *(x[i]->get_ap_abstract1_t());
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);
729 inline abstract1&
join(manager& m, abstract1& dst,
const std::vector<const abstract1*>& x)
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());
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);
746 const_cast<ap_abstract1_t*
>(&
a),
748 m.
raise(
"apron::abstract1::meet(manager&, const lincons1_array&)");
752 inline abstract1&
meet(manager& m, abstract1& dst,
const abstract1& x,
const lincons1_array& y)
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);
768 const_cast<ap_abstract1_t*
>(&
a),
770 m.
raise(
"apron::abstract1::meet(manager&, const tcons1_array&)");
774 inline abstract1&
meet(manager& m, abstract1& dst,
const abstract1& x,
const tcons1_array& y)
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);
792 const_cast<ap_abstract1_t*
>(&
a),
794 m.
raise(
"apron::abstract1::add_rays(manager&, const generator1_array&)");
798 inline abstract1&
add_rays(manager& m, abstract1& dst,
const abstract1& x,
const generator1_array& y)
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);
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&)");
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&)");
835 ap_abstract1_meet_lincons_array(
a.abstract0->man,
true,
836 const_cast<ap_abstract1_t*
>(&
a),
838 manager::raise(
a.abstract0->man,
"apron::abstract1::operator*=(const lincons1_array&)");
845 ap_abstract1_meet_tcons_array(
a.abstract0->man,
true,
846 const_cast<ap_abstract1_t*
>(&
a),
848 manager::raise(
a.abstract0->man,
"apron::abstract1::operator*=(const tcons1_array&)");
855 ap_abstract1_add_ray_array(
a.abstract0->man,
true,
856 const_cast<ap_abstract1_t*
>(&
a),
858 manager::raise(
a.abstract0->man,
"apron::abstract1::operator+=(const generator1_array&)");
869 ap_abstract1_t* r =
const_cast<ap_abstract1_t*
>(i.get_ap_abstract1_t());
870 if (r->abstract0)
return r;
874 inline abstract1&
abstract1::assign(manager& m,
const var& v,
const linexpr1& l,
const abstract1& inter)
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()),
881 m.raise(
"apron::abstract1::assign(manager&, size_t size, const var&, const linexpr1&, const abstract1&)");
885 inline abstract1&
abstract1::assign(manager& m,
size_t size,
const var v[],
const linexpr1 *
const l[],
const abstract1& inter)
887 ap_linexpr1_t ll[
size];
888 for (
size_t i=0;i<
size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
890 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(),
true, &
a,
891 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(v)),
894 m.raise(
"apron::abstract1::assign(manager&, size_t size, const var[], const linexpr1 * const [], const abstract1&)");
899 inline abstract1&
abstract1::assign(manager& m,
const std::vector<var>& v,
const std::vector<const linexpr1*>& l,
const abstract1& inter)
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();
910 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(),
true, &
a,
913 m.raise(
"apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)");
918 inline abstract1&
assign(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
const linexpr1& l,
const abstract1& inter =
abstract1::null)
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()),
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);
933 inline abstract1&
assign(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var v[],
const linexpr1 *
const l[],
const abstract1& inter =
abstract1::null)
935 ap_linexpr1_t ll[size];
936 for (
size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
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)),
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);
949 inline 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)
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();
960 ap_abstract1_assign_linexpr_array(m.get_ap_manager_t(),
false,
961 const_cast<ap_abstract1_t*
>(&src.a),
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);
974 inline abstract1&
abstract1::assign(manager& m,
const var& v,
const texpr1& l,
const abstract1& inter)
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()),
981 m.raise(
"apron::abstract1::assign(manager&, size_t size, const var&, const texpr1&, const abstract1&)");
985 inline abstract1&
abstract1::assign(manager& m,
size_t size,
const var v[],
const texpr1 *
const l[],
const abstract1& inter)
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)),
993 m.raise(
"apron::abstract1::assign(manager&, size_t size, const var[], const texpr1 * const [], const abstract1&)");
997 inline abstract1&
abstract1::assign(manager& m,
const std::vector<var>& v,
const std::vector<const texpr1*>& l,
const abstract1& inter)
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();
1007 a = ap_abstract1_assign_texpr_array(m.get_ap_manager_t(),
true, &
a,
1010 m.raise(
"apron::abstract1::assign(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1014 inline abstract1&
assign(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
const texpr1& l,
const abstract1& inter =
abstract1::null)
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()),
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);
1029 inline abstract1&
assign(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var v[],
const texpr1 *
const l[],
const abstract1& inter =
abstract1::null)
1031 ap_texpr1_t ll[size];
1032 for (
size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
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)),
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);
1045 inline 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)
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();
1056 ap_abstract1_assign_texpr_array(m.get_ap_manager_t(),
false,
1057 const_cast<ap_abstract1_t*
>(&src.a),
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);
1072 inline abstract1&
abstract1::substitute(manager& m,
const var& v,
const linexpr1& l,
const abstract1& inter)
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()),
1079 m.raise(
"apron::abstract1::substitute(manager&, size_t size, const var&, const linexpr1&, const abstract1&)");
1083 inline abstract1&
abstract1::substitute(manager& m,
size_t size,
const var v[],
const linexpr1 *
const l[],
const abstract1& inter)
1085 ap_linexpr1_t ll[
size];
1086 for (
size_t i=0;i<
size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
1088 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(),
true, &
a,
1089 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(v)),
1092 m.raise(
"apron::abstract1::substitute(manager&, size_t size, const var[], const linexpr1 * const [], const abstract1&)");
1097 inline abstract1&
abstract1::substitute(manager& m,
const std::vector<var>& v,
const std::vector<const linexpr1*>& l,
const abstract1& inter)
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();
1108 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(),
true, &
a,
1111 m.raise(
"apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const linexpr1*>&, const abstract1&)");
1116 inline abstract1&
substitute(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
const linexpr1& l,
const abstract1& inter =
abstract1::null)
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()),
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);
1131 inline abstract1&
substitute(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var v[],
const linexpr1 *
const l[],
const abstract1& inter =
abstract1::null)
1133 ap_linexpr1_t ll[size];
1134 for (
size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_linexpr1_t());
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)),
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);
1147 inline 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)
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();
1158 ap_abstract1_substitute_linexpr_array(m.get_ap_manager_t(),
false,
1159 const_cast<ap_abstract1_t*
>(&src.a),
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);
1172 inline abstract1&
abstract1::substitute(manager& m,
const var& v,
const texpr1& l,
const abstract1& inter)
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()),
1179 m.raise(
"apron::abstract1::substitute(manager&, size_t size, const var&, const texpr1&, const abstract1&)");
1183 inline abstract1&
abstract1::substitute(manager& m,
size_t size,
const var v[],
const texpr1 *
const l[],
const abstract1& inter)
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)),
1191 m.raise(
"apron::abstract1::substitute(manager&, size_t size, const var[], const texpr1 * const [], const abstract1&)");
1195 inline abstract1&
abstract1::substitute(manager& m,
const std::vector<var>& v,
const std::vector<const texpr1*>& l,
const abstract1& inter)
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();
1205 a = ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(),
true, &
a,
1208 m.raise(
"apron::abstract1::substitute(manager&, const std::vector<var>&, const std::vector<const texpr1*>&, const abstract1&) vectors have different size");
1212 inline abstract1&
substitute(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
const texpr1& l,
const abstract1& inter =
abstract1::null)
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()),
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);
1227 inline abstract1&
substitute(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var v[],
const texpr1 *
const l[],
const abstract1& inter =
abstract1::null)
1229 ap_texpr1_t ll[size];
1230 for (
size_t i=0;i<size;i++) ll[i] = *(l[i]->get_ap_texpr1_t());
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)),
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);
1243 inline 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)
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();
1254 ap_abstract1_substitute_texpr_array(m.get_ap_manager_t(),
false,
1255 const_cast<ap_abstract1_t*
>(&src.a),
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);
1273 return forget(m,1,&v,project);
1276 inline abstract1&
abstract1::forget(manager& m,
size_t size,
const var v[],
bool project)
1278 a = ap_abstract1_forget_array(m.get_ap_manager_t(),
true, &
a,
1279 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(v)),
1281 m.raise(
"apron::abstract1::forget(manager&, size_t, const var[], bool)");
1285 inline abstract1&
abstract1::forget(manager& m,
const std::vector<var>& v,
bool project)
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)");
1294 inline abstract1&
forget(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
bool project =
false)
1296 return forget(m,dst,src,1,&v,project);
1299 inline abstract1&
forget(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var v[],
bool project =
false)
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)),
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);
1311 inline abstract1&
forget(manager& m, abstract1& dst,
const abstract1& src,
const std::vector<var>& v,
bool project =
false)
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);
1331 a = ap_abstract1_change_environment(m.get_ap_manager_t(),
true, &
a,
1332 const_cast<ap_environment_t*
>(e.get_ap_environment_t()),
1334 m.raise(
"apron::abstract1::change_environment(manager&, const environment&, bool)");
1338 inline abstract1&
change_environment(manager& m, abstract1& dst,
const abstract1& src,
const environment& e,
bool project =
false)
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()),
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);
1354 m.
raise(
"apron::abstract1::minimize_environment(manager&)");
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);
1372 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(oldv)),
1373 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(newv)),
1375 m.
raise(
"apron::abstract1::rename(manager&, size_t, const var[], const var[])");
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();
1390 oldvv, newvv, oldv.size());
1391 m.
raise(
"apron::abstract1::rename(manager&, const std::vector<var>&, const std::vector<var>&)");
1395 inline abstract1&
rename(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var oldv[],
const var newv[])
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)),
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);
1409 inline abstract1&
rename(manager& m, abstract1& dst,
const abstract1& src,
const std::vector<var>& oldv,
const std::vector<var>& newv)
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();
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);
1438 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(vv)),
1440 m.
raise(
"apron::abstract1::expand(manager&, const var&, size_t, const var[])");
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();
1451 m.
raise(
"apron::abstract1::expand(manager&, const var&, const std::vector<var>&)");
1455 inline abstract1&
expand(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
size_t size,
const var vv[])
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)),
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);
1469 inline abstract1&
expand(manager& m, abstract1& dst,
const abstract1& src,
const var& v,
const std::vector<var>& vv)
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();
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()),
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);
1486 inline abstract1&
abstract1::fold(manager& m,
size_t size,
const var vv[])
1488 a = ap_abstract1_fold(m.get_ap_manager_t(),
true, &
a,
1489 reinterpret_cast<ap_var_t*
>(
const_cast<var*
>(vv)),
1491 m.raise(
"apron::abstract1::fold(manager&, const var&, size_t, const var[])");
1495 inline abstract1&
abstract1::fold(manager& m,
const std::vector<var>& vv)
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>&)");
1504 inline abstract1&
fold(manager& m, abstract1& dst,
const abstract1& src,
size_t size,
const var vv[])
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)),
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);
1517 inline abstract1&
fold(manager& m, abstract1& dst,
const abstract1& src,
const std::vector<var>& vv)
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();
1522 ap_abstract1_fold(m.get_ap_manager_t(),
false,
1523 const_cast<ap_abstract1_t*
>(&src.a),
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);
1535 inline abstract1&
widening(manager& m, abstract1& dst,
const abstract1& x,
const abstract1& y)
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);
1547 inline abstract1&
widening(manager& m, abstract1& dst,
const abstract1& x,
const abstract1& y,
const lincons1_array& l)
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);
1568 m.
raise(
"apron::abstract1::closured(manager&)");
1572 inline abstract1&
closure(manager& m, abstract1& dst,
const abstract1& src)
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);
std::ostream & operator<<(std::ostream &os, const abstract1 &s)
Definition: apxx_abstract1_inline.hh:362
abstract1 & change_environment(manager &m, abstract1 &dst, const abstract1 &src, const environment &e, bool project=false)
Definition: apxx_abstract1_inline.hh:1338
abstract1 & closure(manager &m, abstract1 &dst, const abstract1 &src)
Definition: apxx_abstract1_inline.hh:1572
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
bool operator!=(const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:515
abstract1 & unify(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:636
abstract1 & widening(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:1535
static ap_abstract1_t * ap_abstract1_t_or_null(const abstract1 &i)
Definition: apxx_abstract1_inline.hh:867
bool operator<(const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:539
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 & 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 & forget(manager &m, abstract1 &dst, const abstract1 &src, const var &v, bool project=false)
Definition: apxx_abstract1_inline.hh:1294
bool operator<=(const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:520
abstract1 & add_rays(manager &m, abstract1 &dst, const abstract1 &x, const generator1_array &y)
Definition: apxx_abstract1_inline.hh:798
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:529
bool operator>(const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:534
abstract1 & join(manager &m, abstract1 &dst, const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:704
abstract1 & minimize_environment(manager &m, abstract1 &dst, const abstract1 &src)
Definition: apxx_abstract1_inline.hh:1358
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 & deserialize(manager &m, abstract1 &dst, const std::string &s, size_t *eaten=NULL)
Definition: apxx_abstract1_inline.hh:384
abstract1 & rename(manager &m, abstract1 &dst, const abstract1 &src, size_t size, const var oldv[], const var newv[])
Definition: apxx_abstract1_inline.hh:1395
bool operator==(const abstract1 &x, const abstract1 &y)
Definition: apxx_abstract1_inline.hh:506
Level 0 abstract value (ap_abstract0_t* wrapper).
Definition: apxx_abstract0.hh:78
ap_abstract0_t * get_ap_abstract0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_abstract0_inline.hh:1172
Level 1 abstract value (ap_abstract1_t wrapper).
Definition: apxx_abstract1.hh:42
size_t size(manager &m) const
Returns the (abstract) size of the abstract element.
Definition: apxx_abstract1_inline.hh:420
environment get_environment() const
Returns the environment of the abstract element (with reference count incremented).
Definition: apxx_abstract1_inline.hh:405
abstract1 & substitute(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place substitution (backward assignment) of linear expression.
abstract1 & assign(manager &m, const var &v, const linexpr1 &l, const abstract1 &inter=null)
In-place assignment of linear expression.
abstract1 & fold(manager &m, size_t size, const var v[])
Folds variables v[0] to v[size-1] in *this (modified in-place).
interval bound(manager &m, const linexpr1 &l) const
Returns some bounds for a linear expression evaluated in all points in the abstract element.
Definition: apxx_abstract1_inline.hh:549
static const abstract1 null
NULL abstract element, to be used only as default argument in assign and substitute.
Definition: apxx_abstract1.hh:49
abstract1 & canonicalize(manager &m)
Puts the abstract element in canonical form (if such a notion exists).
Definition: apxx_abstract1_inline.hh:324
abstract1 & add_rays(manager &m, const generator1_array &y)
Adds some rays to *this (modified in-place).
Definition: apxx_abstract1_inline.hh:788
~abstract1()
Destroys the abstract element.
Definition: apxx_abstract1_inline.hh:108
interval_array to_box(manager &m) const
Returns a bounding box for the set represented by the abstract element.
Definition: apxx_abstract1_inline.hh:581
generator1_array to_generator_array(manager &m) const
Returns a generator representation of (an over-approximation of) the set represented by the abstract ...
Definition: apxx_abstract1_inline.hh:613
abstract1 & join(manager &m, const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:695
bool is_bottom(manager &m) const
Whether *this represents the empty set.
Definition: apxx_abstract1_inline.hh:434
bool sat(manager &m, const lincons1 &l) const
Whether all points in *this satisfy a linear constraint.
Definition: apxx_abstract1_inline.hh:468
manager get_manager() const
Returns the manager the abstract element was created with (with reference count incremented).
Definition: apxx_abstract1_inline.hh:400
bool is_eq(manager &m, const abstract1 &x) const
Whether *this and x represent the same set.
Definition: apxx_abstract1_inline.hh:450
abstract1 & unify(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:627
bool is_leq(manager &m, const abstract1 &x) const
Whether *this is included in x (set-wise).
Definition: apxx_abstract1_inline.hh:459
abstract1 & rename(manager &m, size_t size, const var oldv[], const var newv[])
Renames oldv[i] into newv[i] in *this.
Definition: apxx_abstract1_inline.hh:1369
abstract1 & operator*=(const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:812
void print(manager &m, FILE *stream=stdout) const
Pretty-printing to a C stream.
Definition: apxx_abstract1_inline.hh:342
abstract1 & set(manager &m, const abstract1 &x)
Replaces *this with a copy of x.
Definition: apxx_abstract1_inline.hh:192
abstract1 & operator+=(const abstract1 &y)
Replaces *this with the join of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:822
abstract1 & approximate(manager &m, int algorithm)
Simplifies the abstract element, potentially loosing precision.
Definition: apxx_abstract1_inline.hh:331
abstract0 & get_abstract0()
Returns a (modifiable) reference to the underlying abstract0.
Definition: apxx_abstract1_inline.hh:410
std::string * serialize(manager &m) const
Serializes an abstract element.
Definition: apxx_abstract1_inline.hh:374
ap_abstract1_t * get_ap_abstract1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_abstract1_inline.hh:1586
abstract1 & forget(manager &m, const var &v, bool project=false)
Forgets about the value of variable v in *this.
abstract1 & change_environment(manager &m, const environment &e, bool project=false)
Modifies the environment of *this.
abstract1 & operator=(const abstract1 &t)
Assigns a copy of t to *this.
Definition: apxx_abstract1_inline.hh:124
abstract1 & closure(manager &m)
Replaces *this with its topological closure.
Definition: apxx_abstract1_inline.hh:1565
abstract1 & minimize_environment(manager &m)
Removes from *this the variables that are unconstrained.
Definition: apxx_abstract1_inline.hh:1351
abstract1 & expand(manager &m, const var &v, size_t size, const var vv[])
Duplicates variable v into size copies in *this (modified in-place).
Definition: apxx_abstract1_inline.hh:1434
bool is_variable_unconstrained(manager &m, const var &v) const
Whether the points in *this are unbounded in the given variable.
Definition: apxx_abstract1_inline.hh:496
tcons1_array to_tcons_array(manager &m) const
Returns a constraint representation of (an over-approximation of) the set represented by the abstract...
Definition: apxx_abstract1_inline.hh:603
void dump(manager &m, FILE *stream=stdout) const
Raw printing to a C stream (mainly for debug purposes).
Definition: apxx_abstract1_inline.hh:356
ap_abstract1_t a
Structure managed by APRON.
Definition: apxx_abstract1.hh:46
abstract1 & meet(manager &m, const abstract1 &y)
Replaces *this with the meet of *this and the abstract element y.
Definition: apxx_abstract1_inline.hh:648
abstract1 & minimize(manager &m)
Minimizes the size of the representation, to save memory.
Definition: apxx_abstract1_inline.hh:317
bool is_top(manager &m) const
Whether *this represents the full space.
Definition: apxx_abstract1_inline.hh:442
abstract1(ap_abstract1_t x)
Internal use only. Shallow copy of structure.
Definition: apxx_abstract1_inline.hh:27
void free(manager &m)
Destroys the abstract element using the given manager.
Definition: apxx_abstract1_inline.hh:114
lincons1_array to_lincons_array(manager &m) const
Returns a linear constraint representation of (an over-approximation of) the set represented by the a...
Definition: apxx_abstract1_inline.hh:593
Level 1 environment (ap_environment_t wrapper).
Definition: apxx_environment.hh:51
const ap_environment_t * get_ap_environment_t() const
Returns a pointer to the internal APRON object pointed by *this.
Definition: apxx_environment_inline.hh:425
Array of generators (ap_generator1_array_t wrapper).
Definition: apxx_generator1.hh:272
const ap_generator1_array_t * get_ap_generator1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_generator1_inline.hh:436
array of interval(s).
Definition: apxx_interval.hh:302
const ap_interval_t *const * get_ap_interval_t_array() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_interval_inline.hh:505
size_t size() const
Returns the array size.
Definition: apxx_interval_inline.hh:473
Interval (ap_interval_t wrapper).
Definition: apxx_interval.hh:47
const ap_interval_t * get_ap_interval_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_interval_inline.hh:336
Array of linear constraints (ap_lincons1_array_t wrapper).
Definition: apxx_lincons1.hh:331
const ap_lincons1_array_t * get_ap_lincons1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons1_inline.hh:499
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition: apxx_lincons1_inline.hh:431
Level 1 linear constraint (ap_lincons1_t wrapper).
Definition: apxx_lincons1.hh:40
const ap_lincons1_t * get_ap_lincons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons1_inline.hh:278
Level 1 linear expression (ap_linexpr1_t wrapper).
Definition: apxx_linexpr1.hh:39
const ap_linexpr1_t * get_ap_linexpr1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_linexpr1_inline.hh:321
Library manager (ap_manager_t wrapper).
Definition: apxx_manager.hh:137
bool exception_raised()
Internal use only. Whether APRON has raised an exception.
Definition: apxx_manager_inline.hh:82
ap_manager_t * get_ap_manager_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_manager_inline.hh:206
static void raise(ap_manager_t *m, const char *msg, ap_abstract0_t *a=NULL)
Internal use only. Translates APRON exceptions to C++ ones.
Array of arbitrary constraints (ap_tcons1_array_t wrapper).
Definition: apxx_tcons1.hh:337
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition: apxx_tcons1_inline.hh:461
const ap_tcons1_array_t * get_ap_tcons1_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_tcons1_inline.hh:530
Level 1 arbitrary constraint (ap_tcons1_t wrapper).
Definition: apxx_tcons1.hh:39
const ap_tcons1_t * get_ap_tcons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_tcons1_inline.hh:307
Level 1 arbitrary expression tree (ap_texpr1_t wrapper).
Definition: apxx_texpr1.hh:42
ap_texpr1_t * get_ap_texpr1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_texpr1_inline.hh:271
Variable name (ap_var_t wrapper).
Definition: apxx_var.hh:39
const ap_var_t & get_ap_var_t() const
Returns a reference to the APRON object wrapped (no copy).
Definition: apxx_var_inline.hh:156
Empty interval or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:33
Full interval (]-oo,+oo[) or domain, to simplify initialisations and assignments.
Definition: apxx_interval.hh:27