28 inline tcons1::tcons1(ap_tcons1_t l) : l(l)
31 inline tcons1::tcons1(
const environment& env, ap_constyp_t constyp)
33 l.tcons0 = ap_tcons0_make(constyp, NULL, NULL);
34 l.env = ap_environment_copy(const_cast<ap_environment_t*>(env.get_ap_environment_t()));
37 inline tcons1::tcons1(ap_constyp_t constyp,
const texpr1::builder& t)
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);
44 inline tcons1::tcons1(ap_constyp_t constyp,
const texpr1::builder& t,
const scalar& modulo)
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),
63 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
65 throw std::invalid_argument(
"apron::tcons1::tcons1(const tcons1&, const enviroment&) not a super-environment");
70 l.tcons0 = ap_tcons0_make_unsat();
71 l.env = ap_environment_copy(const_cast<ap_environment_t*>(e.get_ap_environment_t()));
75 : l(ap_tcons1_from_lincons1(const_cast<ap_lincons1_t*>(x.get_ap_lincons1_t())))
91 inline 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);
98 inline 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);
105 inline 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);
112 inline 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);
119 inline 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);
126 inline 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();
156 l = ap_tcons1_from_lincons1(const_cast<ap_lincons1_t*>(x.get_ap_lincons1_t()));
162 get_tcons0().set_modulo(c);
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,
183 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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);
209 return get_tcons0().get_constyp();
214 return get_tcons0().get_constyp();
219 return get_tcons0().has_modulo();
224 return get_tcons0().has_texpr();
229 if (!get_tcons0().has_modulo())
throw std::invalid_argument(
"apron::tcons1::get_modulo() empty scalar");
230 return get_tcons0().get_modulo();
235 if (!get_tcons0().has_modulo())
throw std::invalid_argument(
"apron::tcons1::get_modulo() empty scalar");
236 return get_tcons0().get_modulo();
241 if (!l.tcons0.texpr0)
throw std::invalid_argument(
"apron::tcons1::get_texpr() empty expression");
242 return texpr1::iterator(l.tcons0.texpr0,l.env);
247 if (!l.tcons0.texpr0)
throw std::invalid_argument(
"apron::tcons1::get_texpr() empty expression");
248 return texpr1::const_iterator(l.tcons0.texpr0,l.env);
256 inline 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));
280 return get_texpr().is_interval_cst();
285 return get_texpr().is_interval_linear();
290 return get_texpr().is_interval_polynomial();
295 return get_texpr().is_interval_polyfrac();
300 return get_texpr().is_scalar();
335 size_t sz = x.size();
336 a = ap_tcons1_array_make(const_cast<ap_environment_t*>(e.get_ap_environment_t()), sz);
337 for (
size_t i=0; i<sz; i++)
338 a.tcons0_array.p[i] = ap_tcons0_copy(&x.a.p[i]);
343 a = ap_tcons1_array_make(const_cast<ap_environment_t*>(e.get_ap_environment_t()), size);
348 size_t sz = x.size();
349 a = ap_tcons1_array_make(x.get_environment().get_ap_environment_t(), sz);
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),
359 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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);
400 a = ap_tcons1_array_make(x.get_environment().get_ap_environment_t(), sz);
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);
428 a = ap_tcons1_array_make(x[0].
get_environment().get_ap_environment_t(), size);
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,
448 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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));
473 return reinterpret_cast<tcons0_array&
>(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*>
489 (x.get_tcons0().get_ap_tcons0_t()));
496 inline 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);
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 is_interval_polynomial() const
Whether the expression is polynomial and there is no rounding.
Definition: apxx_tcons1.hh:289
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition: apxx_tcons1.hh:462
void set_modulo(const scalar &c)
Sets the extra scalar modulo to c (copied).
Definition: apxx_tcons1.hh:161
void set(size_t i, const tcons1 &x)
Changes the constraint at index i.
Definition: apxx_tcons1.hh:485
void extend_environment(const environment &e)
Extends the environment of the expression.
Definition: apxx_tcons1.hh:180
scalar & get_modulo()
Returns a (modifiable) reference to the extra scalar.
Definition: apxx_tcons1.hh:228
bool is_interval_cst() const
Whether the expression is constant (i.e., has no dimension leaves).
Definition: apxx_tcons1.hh:279
bool has_texpr() const
Whether the constraint contains a valid expression tree.
Definition: apxx_tcons1.hh:223
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_tcons1.hh:522
const ap_tcons1_t * get_ap_tcons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_tcons1.hh:308
const tcons0_array & get_tcons0_array() const
Returns a reference to the underlying tcons0_array.
Definition: apxx_tcons1.hh:467
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_tcons1.hh:208
bool operator==(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:410
bool is_interval_polyfrac() const
Whether the expression is a polynomial fraction and there is no rounding.
Definition: apxx_tcons1.hh:294
const tcons0 & get_tcons0() const
Returns a reference to the underlying tcons0.
Definition: apxx_tcons1.hh:198
bool operator>(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:434
~tcons1()
Frees the constraint, including the embedded expression tree and optional modulo scalar.
Definition: apxx_tcons1.hh:83
environment get_environment() const
Returns the environment of the expression (with incremented reference count).
Definition: apxx_tcons1.hh:193
tcons1 get(size_t i) const
Returns a copy of the constraint at index i.
Definition: apxx_tcons1.hh:477
friend std::ostream & operator<<(std::ostream &os, const tcons1_array &s)
Printing.
Definition: apxx_tcons1.hh:513
size_t size() const
Returns the size of the array.
Definition: apxx_tcons1.hh:457
void extend_environment(const environment &e)
Extends the environment of all expressions in array.
Definition: apxx_tcons1.hh:445
bool operator>=(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:429
bool is_scalar() const
Whether all occurring constants are scalar.
Definition: apxx_tcons1.hh:299
bool operator!=(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:417
bool has_modulo() const
Returns whether the constraint has a valid extra scalar (used in modulo constraints).
Definition: apxx_tcons1.hh:218
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.hh:531
tcons1(ap_tcons1_t l)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_tcons1.hh:29
void resize(size_t size)
Resizes the array.
Definition: apxx_tcons1.hh:440
tcons1_array & operator=(const tcons1_array &x)
(Deep) copy.
Definition: apxx_tcons1.hh:396
tcons1 & operator=(const tcons1 &x)
(Deep) copy.
Definition: apxx_tcons1.hh:138
void set_texpr(const texpr1::builder &c)
Sets the underlying expression tree to c (copied).
Definition: apxx_tcons1.hh:166
ap_tcons1_array_t a
Structure managed by APRON.
Definition: apxx_tcons1.hh:341
tcons1_array(ap_tcons1_array_t &a)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_tcons1.hh:331
bool operator<=(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:422
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_tcons1.hh:270
bool is_interval_linear() const
Whether the expression is linear and there is no rounding.
Definition: apxx_tcons1.hh:284
~tcons1_array()
Frees the space used by the array and all its constraints.
Definition: apxx_tcons1.hh:387
texpr1::iterator get_texpr()
Returns an iterator to the root of the underlying expression tree.
Definition: apxx_tcons1.hh:240
bool operator<(const abstract0 &x, const abstract0 &y)
Definition: apxx_abstract0.hh:439