23 inline tcons0::tcons0(ap_tcons0_t& l) : l(l)
28 l = ap_tcons0_make(constyp, NULL, NULL);
33 ap_texpr0_t* lt = ap_texpr0_copy(
const_cast<ap_texpr0_t*
>(t.
get_ap_texpr0_t()));
34 ap_scalar_t* mmodulo = ap_scalar_alloc_set(
const_cast<ap_scalar_t*
>(modulo.
get_ap_scalar_t()));
35 l = ap_tcons0_make(constyp, lt, mmodulo);
40 ap_texpr0_t* lt = ap_texpr0_copy(
const_cast<ap_texpr0_t*
>(t.
get_ap_texpr0_t()));
41 l = ap_tcons0_make(constyp, lt, NULL);
46 l = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(&x.
l));
51 l = ap_tcons0_make_unsat();
56 if (!x.
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::tcons0(const tcons0&, const dimchange&, bool) empty expression");
58 l = ap_tcons0_add_dimensions(
const_cast<ap_tcons0_t*
>(&x.
l),
61 l = ap_tcons0_remove_dimensions(
const_cast<ap_tcons0_t*
>(&x.
l),
67 if (!x.
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::tcons0(const tcons0&, const dimperm&) empty expression");
68 l = ap_tcons0_permute_dimensions(
const_cast<ap_tcons0_t*
>(&x.
l),
83 ap_tcons0_clear(
const_cast<ap_tcons0_t*
>(&
l));
90 inline tcons0
operator>=(
const texpr0::builder& a,
const texpr0::builder& b)
92 if (b.is_zero())
return tcons0(AP_CONS_SUPEQ,a);
93 else if (a.is_zero())
return tcons0(AP_CONS_SUPEQ,-b);
94 else return tcons0(AP_CONS_SUPEQ,a-b);
97 inline tcons0
operator<=(
const texpr0::builder& a,
const texpr0::builder& b)
99 if (b.is_zero())
return tcons0(AP_CONS_SUPEQ,-a);
100 else if (a.is_zero())
return tcons0(AP_CONS_SUPEQ,b);
101 else return tcons0(AP_CONS_SUPEQ,b-a);
104 inline tcons0
operator> (
const texpr0::builder& a,
const texpr0::builder& b)
106 if (b.is_zero())
return tcons0(AP_CONS_SUP,a);
107 else if (a.is_zero())
return tcons0(AP_CONS_SUP,-b);
108 else return tcons0(AP_CONS_SUP,a-b);
111 inline tcons0
operator< (
const texpr0::builder& a,
const texpr0::builder& b)
113 if (b.is_zero())
return tcons0(AP_CONS_SUP,-a);
114 else if (a.is_zero())
return tcons0(AP_CONS_SUP,b);
115 else return tcons0(AP_CONS_SUP,b-a);
118 inline tcons0
operator==(
const texpr0::builder& a,
const texpr0::builder& b)
120 if (b.is_zero())
return tcons0(AP_CONS_EQ,a);
121 else if (a.is_zero())
return tcons0(AP_CONS_EQ,b);
122 else return tcons0(AP_CONS_EQ,a-b);
125 inline tcons0
operator!=(
const texpr0::builder& a,
const texpr0::builder& b)
127 if (b.is_zero())
return tcons0(AP_CONS_DISEQ,a);
128 else if (a.is_zero())
return tcons0(AP_CONS_DISEQ,b);
129 else return tcons0(AP_CONS_DISEQ,a-b);
140 l = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(&x.
l));
148 l = ap_tcons0_make_unsat();
165 if (!
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::add_dimensions(const dimchange&) empty expression");
171 if (!
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::remove_dimensions(const dimchange&) empty expression");
177 if (!
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::permute_dimensions(dimperm&) empty expression");
178 ap_tcons0_permute_dimensions_with(&
l,
const_cast<ap_dimperm_t*
>(d.
get_ap_dimperm_t()));
199 return l.scalar!=NULL;
204 return l.texpr0!=NULL;
209 if (!
l.scalar)
throw std::invalid_argument(
"apron::tcons0::get_modulo() empty scalar");
210 return reinterpret_cast<scalar&
>(*
l.scalar);
215 if (!
l.scalar)
throw std::invalid_argument(
"apron::tcons0::get_modulo() empty scalar");
216 return reinterpret_cast<scalar&
>(*
l.scalar);
221 if (!
l.scalar)
l.scalar = ap_scalar_alloc_set(
const_cast<ap_scalar_t*
>(c.
get_ap_scalar_t()));
222 else ap_scalar_set(
l.scalar,
const_cast<ap_scalar_t*
>(c.
get_ap_scalar_t()));
228 throw std::invalid_argument(
"apron::tcons0::get_texpr() empty expression");
234 if (!
l.texpr0)
throw std::invalid_argument(
"apron::tcons0::get_texpr() empty expression");
240 ap_texpr0_t* cc = ap_texpr0_copy(
const_cast<ap_texpr0_t*
>(c.
get_ap_texpr0_t()));
241 if (
l.texpr0) ap_texpr0_free(
l.texpr0);
249 inline std::ostream&
operator<< (std::ostream& os,
const tcons0& s)
252 switch (s.get_constyp()) {
253 case AP_CONS_EQ:
return os <<
" = 0";
254 case AP_CONS_SUPEQ:
return os <<
" >= 0";
255 case AP_CONS_SUP:
return os <<
" > 0";
256 case AP_CONS_EQMOD:
return os <<
" = 0 mod " << s.get_modulo();
257 case AP_CONS_DISEQ:
return os <<
" != 0";
258 default:
throw std::invalid_argument(
"apron::operator<<(ostream&, const tcons0&) invalid constraint type");
264 ap_tcons0_fprint(stream,
const_cast<ap_tcons0_t*
>(&
l), name_of_dim);
273 return ap_tcons0_is_interval_cst(
const_cast<ap_tcons0_t*
>(&
l));
278 return ap_tcons0_is_interval_linear(
const_cast<ap_tcons0_t*
>(&
l));
283 return ap_tcons0_is_interval_polynomial(
const_cast<ap_tcons0_t*
>(&
l));
288 return ap_tcons0_is_interval_polyfrac(
const_cast<ap_tcons0_t*
>(&
l));
293 return ap_tcons0_is_scalar(
const_cast<ap_tcons0_t*
>(&
l));
321 : a(ap_tcons0_array_make(size))
326 : a(ap_tcons0_array_make(x.a.size))
328 for (
size_t i=0; i<
a.size; i++)
329 a.p[i] = ap_tcons0_copy(&x.
a.p[i]);
333 : a(ap_tcons0_array_make(size))
335 for (
size_t i=0; i<
size; i++)
336 a.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(x[i].get_ap_tcons0_t()));
340 : a(ap_tcons0_array_make(x.size()))
342 for (
size_t i=0; i<
a.size; i++)
343 a.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(x[i].get_ap_tcons0_t()));
349 a = ap_tcons0_array_add_dimensions(
const_cast<ap_tcons0_array_t*
>(&x.
a),
352 a = ap_tcons0_array_remove_dimensions(
const_cast<ap_tcons0_array_t*
>(&x.
a),
358 a = ap_tcons0_array_permute_dimensions(
const_cast<ap_tcons0_array_t*
>(&x.
a),
363 : a(ap_tcons0_array_make(x.size()))
365 for (
size_t i=0; i<
a.size; i++)
366 a.p[i] = ap_tcons0_from_lincons0(
const_cast<ap_lincons0_t*
>(x[i].get_ap_lincons0_t()));
375 ap_tcons0_array_clear(&
a);
385 ap_tcons0_array_clear(&
a);
386 a = ap_tcons0_array_make(x.
a.size);
387 for (
size_t i=0; i<
a.size; i++)
a.p[i] = ap_tcons0_copy(&x.
a.p[i]);
394 size_t size =
a.size;
395 ap_tcons0_array_clear(&
a);
396 a = ap_tcons0_array_make(
size);
397 for (
size_t i=0; i<
size; i++)
398 a.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(x[i].get_ap_tcons0_t()));
404 size_t size = x.size();
405 ap_tcons0_array_clear(&
a);
406 a = ap_tcons0_array_make(
size);
407 for (
size_t i=0; i<
size; i++)
408 a.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>(x[i].get_ap_tcons0_t()));
415 ap_tcons0_array_clear(&
a);
416 a = ap_tcons0_array_make(
size);
417 for (
size_t i=0; i<
size; i++)
418 a.p[i] = ap_tcons0_from_lincons0(
const_cast<ap_lincons0_t*
>(x[i].get_ap_lincons0_t()));
428 ap_tcons0_array_resize(&
a,
size);
433 ap_tcons0_array_add_dimensions_with(&
a,
const_cast<ap_dimchange_t*
>(d.
get_ap_dimchange_t()));
438 ap_tcons0_array_remove_dimensions_with(&
a,
const_cast<ap_dimchange_t*
>(d.
get_ap_dimchange_t()));
443 ap_tcons0_array_permute_dimensions_with(&
a,
const_cast<ap_dimperm_t*
>(d.
get_ap_dimperm_t()));
457 return reinterpret_cast<tcons0*
>(
a.p);
462 return reinterpret_cast<tcons0*
>(
a.p);
467 return reinterpret_cast<tcons0&
>(
a.p[i]);
472 return reinterpret_cast<tcons0&
>(
a.p[i]);
477 if (i >=
a.size)
throw std::out_of_range(
"apron::tcons0_array::get()");
478 return reinterpret_cast<tcons0&
>(
a.p[i]);
483 if (i >=
a.size)
throw std::out_of_range(
"apron::tcons0_array::get()");
484 return reinterpret_cast<tcons0&
>(
a.p[i]);
491 inline tcons0_array::operator std::vector<tcons0>()
const
494 std::vector<tcons0> v = std::vector<tcons0>(sz);
495 for (
size_t i=0;i<sz;i++)
504 inline std::ostream&
operator<< (std::ostream& os,
const tcons0_array& s)
506 size_t size = s.size();
508 for (
size_t i=0;i<size;i++)
515 ap_tcons0_array_fprint(stream,
const_cast<ap_tcons0_array_t*
>(&
a), name_of_dim);
524 return ap_tcons0_array_is_interval_linear(
const_cast<ap_tcons0_array_t*
>(&
a));
tcons0 operator!=(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:125
tcons0 operator>(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:104
tcons0 operator<=(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:97
tcons0 operator>=(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:90
std::ostream & operator<<(std::ostream &os, const tcons0 &s)
Definition: apxx_tcons0_inline.hh:249
tcons0 operator<(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:111
tcons0 operator==(const texpr0::builder &a, const texpr0::builder &b)
Definition: apxx_tcons0_inline.hh:118
texpr0::builder add(const texpr0::builder &a, const texpr0::builder &b, ap_texpr_rtype_t rtype=AP_RTYPE_REAL, ap_texpr_rdir_t rdir=AP_RDIR_NEAREST)
Definition: apxx_texpr0_inline.hh:771
Dimension change object (ap_dimchange_t wrapper).
Definition: apxx_dimension.hh:102
const ap_dimchange_t * get_ap_dimchange_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_dimension_inline.hh:204
Dimension permutation object (ap_dimperm_t wrapper).
Definition: apxx_dimension.hh:292
const ap_dimperm_t * get_ap_dimperm_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_dimension_inline.hh:422
Array of linear constraints (ap_lincons0_array_t wrapper).
Definition: apxx_lincons0.hh:341
size_t size() const
Returns the size of the array.
Definition: apxx_lincons0_inline.hh:375
Level 0 linear constraint (ap_lincons0_t wrapper).
Definition: apxx_lincons0.hh:43
const ap_lincons0_t * get_ap_lincons0_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons0_inline.hh:252
Scalar (ap_scalar_t wrapper).
Definition: apxx_scalar.hh:89
const ap_scalar_t * get_ap_scalar_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_scalar_inline.hh:449
Array of arbitrary constraints (ap_tcons0_array_t wrapper).
Definition: apxx_tcons0.hh:350
tcons0_array & operator=(const tcons0_array &x)
(Deep) copy.
Definition: apxx_tcons0_inline.hh:382
bool is_interval_linear() const
Whether all constraints are linear.
Definition: apxx_tcons0_inline.hh:522
ap_tcons0_array_t a
Structure managed by APRON.
Definition: apxx_tcons0.hh:354
void add_dimensions(const dimchange &d)
Applies add_dimensions to all constraints in the array.
Definition: apxx_tcons0_inline.hh:431
size_t size() const
Returns the size of the array.
Definition: apxx_tcons0_inline.hh:450
void print(char **name_of_dim=NULL, FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_tcons0_inline.hh:513
const ap_tcons0_array_t * get_ap_tcons0_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_tcons0_inline.hh:530
tcons0_array(ap_tcons0_array_t &a)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_tcons0.hh:357
tcons0 & operator[](size_t i)
Returns a (modifiable) reference to an element, no bound checking.
Definition: apxx_tcons0_inline.hh:465
tcons0 & get(size_t i)
Returns a (modifiable) reference to an element (bound-checked).
Definition: apxx_tcons0_inline.hh:475
tcons0 * contents()
Returns a pointer to the start of the internal array holding the constraints.
Definition: apxx_tcons0_inline.hh:455
void permute_dimensions(const dimperm &d)
Applies permute_dimensions to all constraints in the array.
Definition: apxx_tcons0_inline.hh:441
~tcons0_array()
Frees the space used by the array and all its constraints.
Definition: apxx_tcons0_inline.hh:373
void resize(size_t size)
Resizes the array.
Definition: apxx_tcons0_inline.hh:426
void remove_dimensions(const dimchange &d)
Applies remove_dimensions to all constraints in the array.
Definition: apxx_tcons0_inline.hh:436
Level 0 arbitrary constraint (ap_tcons0_t wrapper).
Definition: apxx_tcons0.hh:47
tcons0(ap_tcons0_t &l)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_tcons0_inline.hh:23
bool is_interval_polyfrac() const
Whether the expression is a polynomial fraction and there is no rounding.
Definition: apxx_tcons0_inline.hh:286
ap_tcons0_t l
Structure managed by APRON.
Definition: apxx_tcons0.hh:51
~tcons0()
Frees the constraint, including the embedded expression tree and optional modulo scalar.
Definition: apxx_tcons0_inline.hh:81
bool is_interval_cst() const
Whether the expression is constant (i.e., has no dimension leaves).
Definition: apxx_tcons0_inline.hh:271
bool has_modulo() const
Returns whether the constraint has a valid extra scalar (used in modulo constraints).
Definition: apxx_tcons0_inline.hh:197
bool is_scalar() const
Whether all occurring constants are scalar.
Definition: apxx_tcons0_inline.hh:291
void remove_dimensions(const dimchange &d)
Removes dimensions to the underlying expression tree.
Definition: apxx_tcons0_inline.hh:169
bool is_interval_linear() const
Whether the expression is linear and there is no rounding.
Definition: apxx_tcons0_inline.hh:276
void set_texpr(const texpr0::builder &c)
Sets the underlying expression tree to c (copied).
Definition: apxx_tcons0_inline.hh:238
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_tcons0_inline.hh:187
bool has_texpr() const
Whether the constraint contains a valid expression tree.
Definition: apxx_tcons0_inline.hh:202
void permute_dimensions(const dimperm &d)
Applies a permutation to the underlying expression tree.
Definition: apxx_tcons0_inline.hh:175
void set_modulo(const scalar &c)
Sets the extra scalar modulo to c (copied).
Definition: apxx_tcons0_inline.hh:219
void print(char **name_of_dim=NULL, FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_tcons0_inline.hh:262
texpr0::iterator get_texpr()
Returns an iterator to the root of the underlying expression tree.
Definition: apxx_tcons0_inline.hh:232
void add_dimensions(const dimchange &d)
Adds dimensions to the underlying expression tree.
Definition: apxx_tcons0_inline.hh:163
bool is_interval_polynomial() const
Whether the expression is polynomial and there is no rounding.
Definition: apxx_tcons0_inline.hh:281
const ap_tcons0_t * get_ap_tcons0_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_tcons0_inline.hh:301
tcons0 & operator=(const tcons0 &x)
(Deep) copy.
Definition: apxx_tcons0_inline.hh:136
scalar & get_modulo()
Returns a (modifiable) reference to the extra scalar.
Definition: apxx_tcons0_inline.hh:207
Temporary expression nodes used when constructing a texpr0.
Definition: apxx_texpr0.hh:581
ap_texpr0_t * get_ap_texpr0_t()
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_texpr0_inline.hh:912
Iterators to traverse a constant expression tree.
Definition: apxx_texpr0.hh:211
Iterators to traverse and mutate an expression tree.
Definition: apxx_texpr0.hh:413
Unsatisfiable constraint, to simplify initialisations and assignments.
Definition: apxx_lincons0.hh:28