28inline tcons1::tcons1(ap_tcons1_t l) : l(l)
33 l.tcons0 = ap_tcons0_make(constyp, NULL, NULL);
39 ap_texpr1_t* x = ap_texpr1_copy(
const_cast<ap_texpr1_t*
>(t.
get_ap_texpr1_t()));
40 l = ap_tcons1_make(constyp, x, NULL);
46 ap_scalar_t* mmodulo = ap_scalar_alloc_set(
const_cast<ap_scalar_t*
>(modulo.
get_ap_scalar_t()));
47 ap_texpr1_t* x = ap_texpr1_copy(
const_cast<ap_texpr1_t*
>(t.
get_ap_texpr1_t()));
48 l = ap_tcons1_make(constyp, x, mmodulo);
53 : l(ap_tcons1_copy(const_cast<ap_tcons1_t*>(&x.l)))
58 if (!x.
l.tcons0.texpr0)
59 throw std::invalid_argument(
"apron::tcons1::tcons1(const tcons1&, const enviroment&) empty expression");
61 ap_tcons1_extend_environment(&
l,
62 const_cast<ap_tcons1_t*
>(&x.
l),
65 throw std::invalid_argument(
"apron::tcons1::tcons1(const tcons1&, const enviroment&) not a super-environment");
70 l.tcons0 = ap_tcons0_make_unsat();
75 : l(ap_tcons1_from_lincons1(const_cast<ap_lincons1_t*>(x.get_ap_lincons1_t())))
91inline tcons1
operator>=(
const texpr1::builder& a,
const texpr1::builder& b)
93 if (b.is_zero())
return tcons1(AP_CONS_SUPEQ,a);
94 else if (a.is_zero())
return tcons1(AP_CONS_SUPEQ,-b);
95 else return tcons1(AP_CONS_SUPEQ,a-b);
98inline tcons1
operator<=(
const texpr1::builder& a,
const texpr1::builder& b)
100 if (b.is_zero())
return tcons1(AP_CONS_SUPEQ,-a);
101 else if (a.is_zero())
return tcons1(AP_CONS_SUPEQ,b);
102 else return tcons1(AP_CONS_SUPEQ,b-a);
105inline tcons1
operator> (
const texpr1::builder& a,
const texpr1::builder& b)
107 if (b.is_zero())
return tcons1(AP_CONS_SUP,a);
108 else if (a.is_zero())
return tcons1(AP_CONS_SUP,-b);
109 else return tcons1(AP_CONS_SUP,a-b);
112inline tcons1
operator< (
const texpr1::builder& a,
const texpr1::builder& b)
114 if (b.is_zero())
return tcons1(AP_CONS_SUP,-a);
115 else if (a.is_zero())
return tcons1(AP_CONS_SUP,b);
116 else return tcons1(AP_CONS_SUP,b-a);
119inline tcons1
operator==(
const texpr1::builder& a,
const texpr1::builder& b)
121 if (b.is_zero())
return tcons1(AP_CONS_EQ,a);
122 else if (a.is_zero())
return tcons1(AP_CONS_EQ,b);
123 else return tcons1(AP_CONS_EQ,a-b);
126inline tcons1
operator!=(
const texpr1::builder& a,
const texpr1::builder& b)
128 if (b.is_zero())
return tcons1(AP_CONS_DISEQ,a);
129 else if (a.is_zero())
return tcons1(AP_CONS_DISEQ,b);
130 else return tcons1(AP_CONS_DISEQ,a-b);
141 l = ap_tcons1_copy(
const_cast<ap_tcons1_t*
>(&x.
l));
148 ap_tcons0_clear(&
l.tcons0);
149 l.tcons0 = ap_tcons0_make_unsat();
167 ap_texpr1_t* cc = ap_texpr1_copy(
const_cast<ap_texpr1_t*
>(c.
get_ap_texpr1_t()));
168 if (
l.tcons0.texpr0) ap_texpr0_free(
l.tcons0.texpr0);
169 ap_environment_free(
l.env);
170 l.tcons0.texpr0 = cc->texpr0;
182 ap_tcons1_extend_environment_with(&
l,
185 throw std::invalid_argument(
"apron::tcons1::extend_environment(const environment&) not a super-environment");
194 return ap_environment_copy(
l.env);
199 return reinterpret_cast<const tcons0&
>(
l.tcons0);
204 return reinterpret_cast<tcons0&
>(
l.tcons0);
229 if (!
get_tcons0().
has_modulo())
throw std::invalid_argument(
"apron::tcons1::get_modulo() empty scalar");
235 if (!
get_tcons0().
has_modulo())
throw std::invalid_argument(
"apron::tcons1::get_modulo() empty scalar");
241 if (!
l.tcons0.texpr0)
throw std::invalid_argument(
"apron::tcons1::get_texpr() empty expression");
247 if (!
l.tcons0.texpr0)
throw std::invalid_argument(
"apron::tcons1::get_texpr() empty expression");
256inline std::ostream&
operator<< (std::ostream& os,
const tcons1& s)
259 switch (s.get_constyp()) {
260 case AP_CONS_EQ:
return os <<
" = 0";
261 case AP_CONS_SUPEQ:
return os <<
" >= 0";
262 case AP_CONS_SUP:
return os <<
" > 0";
263 case AP_CONS_EQMOD:
return os <<
" = 0 mod " << s.get_modulo();
264 case AP_CONS_DISEQ:
return os <<
" != 0";
265 default:
throw std::invalid_argument(
"apron::operator<<(ostream&, const tcons1&) invalid constraint type");
271 ap_tcons1_fprint(stream,
const_cast<ap_tcons1_t*
>(&
l));
335 size_t sz = x.
size();
337 for (
size_t i=0; i<sz; i++)
338 a.tcons0_array.p[i] = ap_tcons0_copy(&x.
a.p[i]);
348 size_t sz = x.
size();
350 for (
size_t i=0; i<sz; i++)
351 a.tcons0_array.p[i] = ap_tcons0_copy(&x.
a.tcons0_array.p[i]);
357 ap_tcons1_array_extend_environment(&
a,
358 const_cast<ap_tcons1_array_t*
>(&x.
a),
360 if (r)
throw std::invalid_argument(
"apron::tcons1_array::tcons1_array(const tcons1_array, const environment&) not a super-environment");
365 if (sz<1)
throw std::invalid_argument(
"apron::tcons1_array::tcons1_array(size_t, const tcons1) null size");
366 a = ap_tcons1_array_make(x[0].
get_environment().get_ap_environment_t(), sz);
367 for (
size_t i=0; i<sz; i++)
368 a.tcons0_array.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>
369 (x[i].get_tcons0().get_ap_tcons0_t()));
374 size_t sz = x.size();
375 if (sz<1)
throw std::invalid_argument(
"apron::tcons1_array::tcons1_array(const vector<tcons1>&) null size");
376 a = ap_tcons1_array_make(x[0].
get_environment().get_ap_environment_t(), sz);
377 for (
size_t i=0; i<sz; i++)
378 a.tcons0_array.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>
379 (x[i].get_tcons0().get_ap_tcons0_t()));
388 ap_tcons1_array_clear(&
a);
398 size_t sz = x.
size();
399 ap_tcons1_array_clear(&
a);
401 for (
size_t i=0; i<sz; i++)
402 a.tcons0_array.p[i] = ap_tcons0_copy(&x.
a.tcons0_array.p[i]);
410 for (
size_t i=0; i<sz; i++) {
411 ap_tcons0_clear(&
a.tcons0_array.p[i]);
412 a.tcons0_array.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>
413 (x[i].get_tcons0().get_ap_tcons0_t()));
420 size_t size = x.size();
422 ap_tcons1_array_t aa = ap_tcons1_array_make(
a.env,0);
423 ap_tcons1_array_clear(&
a);
427 ap_tcons1_array_clear(&
a);
429 for (
size_t i=0; i<
size; i++)
430 a.tcons0_array.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>
431 (x[i].get_tcons0().get_ap_tcons0_t()));
441 ap_tcons0_array_resize(&
a.tcons0_array,
size);
447 ap_tcons1_array_extend_environment_with(&
a,
449 if (r)
throw std::invalid_argument(
"apron::tcons1_array::extend_environment(const environment&) not a super-environment");
458 return ap_tcons1_array_size(
const_cast<ap_tcons1_array_t*
>(&
a));
463 return (ap_environment_copy(ap_tcons1_array_envref(
const_cast<ap_tcons1_array_t*
>(&
a))));
468 return reinterpret_cast<tcons0_array&
>(
const_cast<ap_tcons0_array_t&
>(
a.tcons0_array));
478 if (i>=
size())
throw std::out_of_range(
"apron::tcons1_array::get(size_t)");
479 ap_tcons1_t c = ap_tcons1_array_get(
const_cast<ap_tcons1_array_t*
>(&
a),i);
480 ap_tcons1_t cc = ap_tcons1_copy(&c);
486 if (i>=
size())
throw std::out_of_range(
"apron::tcons1_array::set(size_t, const tcons1&)");
487 ap_tcons0_clear(&
a.tcons0_array.p[i]);
488 a.tcons0_array.p[i] = ap_tcons0_copy(
const_cast<ap_tcons0_t*
>
496inline tcons1_array::operator std::vector<tcons1>()
const
500 std::vector<tcons1> v(sz,dummy);
501 for (
size_t i=0;i<sz;i++) {
502 ap_tcons1_t c = ap_tcons1_array_get(
const_cast<ap_tcons1_array_t*
>(&a),i);
503 v[i] = ap_tcons1_copy(&c);
512inline std::ostream&
operator<< (std::ostream& os,
const tcons1_array& s)
514 size_t sz = s.size();
516 for (
size_t i=0;i<sz;i++)
517 os << s.get(i) <<
"; ";
523 ap_tcons1_array_fprint(stream,
const_cast<ap_tcons1_array_t*
>(&
a));
bool operator==(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:409
bool operator<=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:421
bool operator>(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:433
bool operator<(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:438
bool operator>=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:428
bool operator!=(const abstract0 &x, const abstract0 &y)
Definition apxx_abstract0_inline.hh:416
std::ostream & operator<<(std::ostream &os, const abstract0 &s)
Definition apxx_abstract0_inline.hh:292
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
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
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
ap_tcons0_array_t a
Structure managed by APRON.
Definition apxx_tcons0.hh:354
size_t size() const
Returns the size of the array.
Definition apxx_tcons0_inline.hh:450
Level 0 arbitrary constraint (ap_tcons0_t wrapper).
Definition apxx_tcons0.hh:47
bool has_modulo() const
Returns whether the constraint has a valid extra scalar (used in modulo constraints).
Definition apxx_tcons0_inline.hh:197
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 set_modulo(const scalar &c)
Sets the extra scalar modulo to c (copied).
Definition apxx_tcons0_inline.hh:219
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
scalar & get_modulo()
Returns a (modifiable) reference to the extra scalar.
Definition apxx_tcons0_inline.hh:207
Array of arbitrary constraints (ap_tcons1_array_t wrapper).
Definition apxx_tcons1.hh:337
tcons1_array(ap_tcons1_array_t &a)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition apxx_tcons1_inline.hh:330
ap_tcons1_array_t a
Structure managed by APRON.
Definition apxx_tcons1.hh:341
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition apxx_tcons1_inline.hh:461
tcons1_array & operator=(const tcons1_array &x)
(Deep) copy.
Definition apxx_tcons1_inline.hh:395
size_t size() const
Returns the size of the array.
Definition apxx_tcons1_inline.hh:456
void set(size_t i, const tcons1 &x)
Changes the constraint at index i.
Definition apxx_tcons1_inline.hh:484
const tcons0_array & get_tcons0_array() const
Returns a reference to the underlying tcons0_array.
Definition apxx_tcons1_inline.hh:466
~tcons1_array()
Frees the space used by the array and all its constraints.
Definition apxx_tcons1_inline.hh:386
void resize(size_t size)
Resizes the array.
Definition apxx_tcons1_inline.hh:439
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
tcons1 get(size_t i) const
Returns a copy of the constraint at index i.
Definition apxx_tcons1_inline.hh:476
void extend_environment(const environment &e)
Extends the environment of all expressions in array.
Definition apxx_tcons1_inline.hh:444
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition apxx_tcons1_inline.hh:521
Level 1 arbitrary constraint (ap_tcons1_t wrapper).
Definition apxx_tcons1.hh:39
bool has_modulo() const
Returns whether the constraint has a valid extra scalar (used in modulo constraints).
Definition apxx_tcons1_inline.hh:217
bool has_texpr() const
Whether the constraint contains a valid expression tree.
Definition apxx_tcons1_inline.hh:222
texpr1::iterator get_texpr()
Returns an iterator to the root of the underlying expression tree.
Definition apxx_tcons1_inline.hh:239
bool is_interval_cst() const
Whether the expression is constant (i.e., has no dimension leaves).
Definition apxx_tcons1_inline.hh:278
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition apxx_tcons1_inline.hh:207
void set_texpr(const texpr1::builder &c)
Sets the underlying expression tree to c (copied).
Definition apxx_tcons1_inline.hh:165
~tcons1()
Frees the constraint, including the embedded expression tree and optional modulo scalar.
Definition apxx_tcons1_inline.hh:82
bool is_interval_polynomial() const
Whether the expression is polynomial and there is no rounding.
Definition apxx_tcons1_inline.hh:288
ap_tcons1_t l
Structure managed by APRON.
Definition apxx_tcons1.hh:43
bool is_interval_linear() const
Whether the expression is linear and there is no rounding.
Definition apxx_tcons1_inline.hh:283
void set_modulo(const scalar &c)
Sets the extra scalar modulo to c (copied).
Definition apxx_tcons1_inline.hh:160
tcons1(ap_tcons1_t l)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition apxx_tcons1_inline.hh:28
tcons1 & operator=(const tcons1 &x)
(Deep) copy.
Definition apxx_tcons1_inline.hh:137
void extend_environment(const environment &e)
Extends the environment of the expression.
Definition apxx_tcons1_inline.hh:179
environment get_environment() const
Returns the environment of the expression (with incremented reference count).
Definition apxx_tcons1_inline.hh:192
scalar & get_modulo()
Returns a (modifiable) reference to the extra scalar.
Definition apxx_tcons1_inline.hh:227
bool is_interval_polyfrac() const
Whether the expression is a polynomial fraction and there is no rounding.
Definition apxx_tcons1_inline.hh:293
bool is_scalar() const
Whether all occurring constants are scalar.
Definition apxx_tcons1_inline.hh:298
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition apxx_tcons1_inline.hh:269
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
const tcons0 & get_tcons0() const
Returns a reference to the underlying tcons0.
Definition apxx_tcons1_inline.hh:197
Temporary expression nodes used when constructing a texpr1.
Definition apxx_texpr1.hh:561
ap_texpr1_t * get_ap_texpr1_t()
Returns a pointer to the internal APRON object stored in *this.
Definition apxx_texpr1_inline.hh:988
Iterators to traverse a constant expression tree.
Definition apxx_texpr1.hh:183
bool is_scalar() const
Whether all occurring constants are scalar.
Definition apxx_texpr1_inline.hh:473
bool is_interval_linear() const
Whether the expression is linear and there is no rounding.
Definition apxx_texpr1_inline.hh:458
bool is_interval_cst() const
Whether the expression is constant (i.e., has no dimension leaves).
Definition apxx_texpr1_inline.hh:453
bool is_interval_polynomial() const
Whether the expression is polynomial and there is no rounding.
Definition apxx_texpr1_inline.hh:463
bool is_interval_polyfrac() const
Whether the expression is a polynomial fraction and there is no rounding.
Definition apxx_texpr1_inline.hh:468
Iterators to traverse and mutate an expression tree.
Definition apxx_texpr1.hh:386
Unsatisfiable constraint, to simplify initialisations and assignments.
Definition apxx_lincons0.hh:28