27 inline lincons1::lincons1(ap_lincons1_t p) : l(p)
40 l = ap_lincons1_make(constyp, &llin, NULL);
45 ap_linexpr1_t llin = ap_linexpr1_copy(
const_cast<ap_linexpr1_t*
>(lin.
get_ap_linexpr1_t()));
46 l = ap_lincons1_make(constyp, &llin, NULL);
51 ap_linexpr1_t llin = ap_linexpr1_copy(
const_cast<ap_linexpr1_t*
>(lin.
get_ap_linexpr1_t()));
52 ap_scalar_t* mmodulo = ap_scalar_alloc_set(
const_cast<ap_scalar_t*
>(modulo.
get_ap_scalar_t()));
53 l = ap_lincons1_make(constyp, &llin, mmodulo);
63 l = ap_lincons1_copy(
const_cast<ap_lincons1_t*
>(&x.
l));
69 throw std::invalid_argument(
"apron::lincons1::lincons1(const lincons1&, const environment&) empty expression");
71 ap_lincons1_extend_environment(&
l,
72 const_cast<ap_lincons1_t*
>(&x.
l),
74 if (r)
throw std::invalid_argument(
"apron::lincons1::lincons1(const lincons1&, const environment&) not a super-environment");
83 ap_lincons1_clear(&
l);
92 ap_lincons1_t ll = ap_lincons1_copy(
const_cast<ap_lincons1_t*
>(&x.
l));
93 ap_lincons1_clear(&
l);
100 ap_lincons1_t ll = ap_lincons1_make_unsat(ap_lincons1_envref(&
l));
101 ap_lincons1_clear(&
l);
123 throw std::invalid_argument(
"apron::lincons1::extend_environment(const environment&) empty expression");
125 ap_lincons1_extend_environment_with(&
l,
127 if (r)
throw std::invalid_argument(
"apron::lincons1::extend_environment(const environment&) not a super-environment");
137 return (ap_environment_copy(ap_lincons1_envref(
const_cast<ap_lincons1_t*
>(&
l))));
142 return reinterpret_cast<lincons0&
>(*ap_lincons1_lincons0ref(
const_cast<ap_lincons1_t*
>(&
l)));
147 return reinterpret_cast<lincons0&
>(*ap_lincons1_lincons0ref(&
l));
178 throw std::invalid_argument(
"apron::lincons1::get_modulo() empty scalar");
185 throw std::invalid_argument(
"apron::lincons1::get_modulo() empty scalar");
192 throw std::invalid_argument(
"apron::lincons1::get_linexpr() empty expression");
200 throw std::invalid_argument(
"apron::lincons1::get_cst() empty expression");
201 return reinterpret_cast<coeff&
>(*ap_lincons1_cstref(&
l));
207 throw std::invalid_argument(
"apron::lincons1::get_cst() empty expression");
208 return reinterpret_cast<coeff&
>(*ap_lincons1_cstref(
const_cast<ap_lincons1_t*
>(&
l)));
214 throw std::invalid_argument(
"apron::lincons1::operator[](const var&) empty expression");
215 ap_coeff_t* x = ap_lincons1_coeffref(&
l,
218 throw std::invalid_argument(
"apron::lincons1::operator[](const var&) variable not in environment");
219 return reinterpret_cast<coeff&
>(*x);
225 throw std::invalid_argument(
"apron::lincons1::operator[](const var&) empty expression");
226 ap_coeff_t* x = ap_lincons1_coeffref(
const_cast<ap_lincons1_t*
>(&
l),
227 const_cast<ap_var_t
>(var.get_ap_var_t()));
229 throw std::invalid_argument(
"apron::lincons1::operator[](const var&) variable not in environment");
230 return reinterpret_cast<coeff&
>(*x);
237 inline std::ostream&
operator<< (std::ostream& os,
const lincons1& s)
239 os << s.get_linexpr();
240 switch (s.get_constyp()) {
241 case AP_CONS_EQ:
return os <<
" = 0";
242 case AP_CONS_SUPEQ:
return os <<
" >= 0";
243 case AP_CONS_SUP:
return os <<
" > 0";
244 case AP_CONS_EQMOD:
return os <<
" = 0 mod " << s.get_modulo();
245 case AP_CONS_DISEQ:
return os <<
" != 0";
246 default:
throw std::invalid_argument(
"apron::operator<<(ostream&, const lincons1&) invalid constraint type");
252 ap_lincons1_fprint(stream,
const_cast<ap_lincons1_t*
>(&
l));
261 return ap_lincons1_is_unsat(
const_cast<ap_lincons1_t*
>(&
l));
305 size_t sz = x.
size();
307 for (
size_t i=0; i<sz; i++)
308 a.lincons0_array.p[i] = ap_lincons0_copy(&x.
a.p[i]);
318 size_t sz = x.
size();
320 for (
size_t i=0; i<sz; i++)
321 a.lincons0_array.p[i] = ap_lincons0_copy(&x.
a.lincons0_array.p[i]);
327 ap_lincons1_array_extend_environment(&
a,
328 const_cast<ap_lincons1_array_t*
>(&x.
a),
330 if (r)
throw std::invalid_argument(
"apron::lincons1_array::lincons1_array(const lincons1_array, const environment&) not a super-environment");
335 if (sz<1)
throw std::invalid_argument(
"apron::lincons1_array::lincons1_array(size_t, const lincons1) null size");
336 a = ap_lincons1_array_make(x[0].
get_environment().get_ap_environment_t(), sz);
337 for (
size_t i=0; i<sz; i++)
338 a.lincons0_array.p[i] = ap_lincons0_copy(
const_cast<ap_lincons0_t*
>
339 (x[i].get_lincons0().get_ap_lincons0_t()));
344 size_t sz = x.size();
345 if (sz<1)
throw std::invalid_argument(
"apron::lincons1_array::lincons1_array(const vector<lincons1>&) null size");
346 a = ap_lincons1_array_make(x[0].
get_environment().get_ap_environment_t(), sz);
347 for (
size_t i=0; i<sz; i++)
348 a.lincons0_array.p[i] = ap_lincons0_copy(
const_cast<ap_lincons0_t*
>
349 (x[i].get_lincons0().get_ap_lincons0_t()));
358 ap_lincons1_array_clear(&
a);
368 size_t sz = x.
size();
369 ap_lincons1_array_clear(&
a);
371 for (
size_t i=0; i<sz; i++)
372 a.lincons0_array.p[i] = ap_lincons0_copy(&x.
a.lincons0_array.p[i]);
380 for (
size_t i=0; i<sz; i++) {
381 ap_lincons0_clear(&
a.lincons0_array.p[i]);
382 a.lincons0_array.p[i] = ap_lincons0_copy(
const_cast<ap_lincons0_t*
>
383 (x[i].get_lincons0().get_ap_lincons0_t()));
390 size_t size = x.size();
392 ap_lincons1_array_t aa = ap_lincons1_array_make(
a.env,0);
393 ap_lincons1_array_clear(&
a);
397 ap_lincons1_array_clear(&
a);
399 for (
size_t i=0; i<
size; i++)
400 a.lincons0_array.p[i] = ap_lincons0_copy(
const_cast<ap_lincons0_t*
>
401 (x[i].get_lincons0().get_ap_lincons0_t()));
411 ap_lincons0_array_resize(&
a.lincons0_array,
size);
417 ap_lincons1_array_extend_environment_with(&
a,
419 if (r)
throw std::invalid_argument(
"apron::lincons1_array::extend_environment(const environment&) not a super-environment");
428 return ap_lincons1_array_size(
const_cast<ap_lincons1_array_t*
>(&
a));
433 return (ap_environment_copy(ap_lincons1_array_envref(
const_cast<ap_lincons1_array_t*
>(&
a))));
438 return reinterpret_cast<lincons0_array&
>(
const_cast<ap_lincons0_array_t&
>(
a.lincons0_array));
448 if (i>=
size())
throw std::out_of_range(
"apron::lincons1_array::get(size_t)");
449 ap_lincons1_t c = ap_lincons1_array_get(
const_cast<ap_lincons1_array_t*
>(&
a),i);
450 return lincons1(ap_lincons1_copy(&c));
455 if (i>=
size())
throw std::out_of_range(
"apron::lincons1_array::set(size_t, const lincons1&)");
456 ap_lincons0_clear(&
a.lincons0_array.p[i]);
457 a.lincons0_array.p[i] = ap_lincons0_copy(
const_cast<ap_lincons0_t*
>
465 inline lincons1_array::operator std::vector<lincons1>()
const
469 std::vector<lincons1> v(sz,dummy);
470 for (
size_t i=0;i<sz;i++) {
471 ap_lincons1_t c = ap_lincons1_array_get(
const_cast<ap_lincons1_array_t*
>(&a),i);
472 v[i] = ap_lincons1_copy(&c);
481 inline std::ostream&
operator<< (std::ostream& os,
const lincons1_array& s)
483 size_t sz = s.size();
485 for (
size_t i=0;i<sz;i++)
486 os << s.get(i) <<
"; ";
492 ap_lincons1_array_fprint(stream,
const_cast<ap_lincons1_array_t*
>(&
a));
std::ostream & operator<<(std::ostream &os, const lincons1 &s)
Definition: apxx_lincons1_inline.hh:237
Coefficient (ap_coeff_t wrapper).
Definition: apxx_coeff.hh:36
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 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
ap_lincons0_array_t a
Structure managed by APRON.
Definition: apxx_lincons0.hh:345
Level 0 linear constraint (ap_lincons0_t wrapper).
Definition: apxx_lincons0.hh:43
bool has_modulo() const
Whether the constraint has a valid auxiliary scalar (used in modulo constraints).
Definition: apxx_lincons0_inline.hh:145
bool has_linexpr() const
Whether the constraint has a valid linear expression.
Definition: apxx_lincons0_inline.hh:150
void set_linexpr(const linexpr0 &c)
Sets the underlying linear expression to c (copied).
Definition: apxx_lincons0_inline.hh:185
bool is_quasilinear() const
Whether the underlying linear expression has only scalar coefficients, except maybe for the constant ...
Definition: apxx_lincons0_inline.hh:241
bool is_linear() const
Whether the underlying linear expression has only scalar coefficients.
Definition: apxx_lincons0_inline.hh:235
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 & get_modulo()
Returns a (modifiable) reference to the auxiliary scalar.
Definition: apxx_lincons0_inline.hh:155
void set_modulo(const scalar &c)
Sets the auxiliary scalar modulo to c (copied).
Definition: apxx_lincons0_inline.hh:167
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_lincons0_inline.hh:135
size_t size() const
Returns the size of the underlying linear expression.
Definition: apxx_lincons0_inline.hh:126
linexpr0 & get_linexpr()
Returns a (modifiable) reference to the underlying linear expression.
Definition: apxx_lincons0_inline.hh:173
Array of linear constraints (ap_lincons1_array_t wrapper).
Definition: apxx_lincons1.hh:331
void set(size_t i, const lincons1 &x)
Changes the constraint at index i.
Definition: apxx_lincons1_inline.hh:453
const lincons0_array & get_lincons0_array() const
Returns a reference to the underlying lincons0_array.
Definition: apxx_lincons1_inline.hh:436
void extend_environment(const environment &e)
Extends the environment of all expressions in array.
Definition: apxx_lincons1_inline.hh:414
ap_lincons1_array_t a
Structure managed by APRON.
Definition: apxx_lincons1.hh:335
void resize(size_t size)
Resizes the array.
Definition: apxx_lincons1_inline.hh:409
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
lincons1_array(ap_lincons1_array_t &a)
Internal use only. Shallow copy (no copy of lincons0_array or environment).
Definition: apxx_lincons1_inline.hh:300
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition: apxx_lincons1_inline.hh:431
~lincons1_array()
Frees the space used by the array and all its constraints, and decrements the reference count of the ...
Definition: apxx_lincons1_inline.hh:356
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons1_inline.hh:490
lincons1_array & operator=(const lincons1_array &x)
(Deep) copy.
Definition: apxx_lincons1_inline.hh:365
size_t size() const
Returns the size of the array.
Definition: apxx_lincons1_inline.hh:426
lincons1 get(size_t i) const
Returns a copy of the constraint at index i.
Definition: apxx_lincons1_inline.hh:446
Level 1 linear constraint (ap_lincons1_t wrapper).
Definition: apxx_lincons1.hh:40
void set_linexpr(const linexpr1 &c)
Sets the underlying linear expression to c (copied).
Definition: apxx_lincons1_inline.hh:111
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
bool is_linear() const
Whether the underlying linear expression has only scalar coefficients.
Definition: apxx_lincons1_inline.hh:264
size_t size() const
Returns the size of the underlying linear expression.
Definition: apxx_lincons1_inline.hh:150
bool has_modulo() const
Whether the constraint has a valid auxiliary scalar (used in modulo constraints).
Definition: apxx_lincons1_inline.hh:165
environment get_environment() const
Returns the environment of the constraint (with incremented reference count).
Definition: apxx_lincons1_inline.hh:135
coeff & operator[](const var &v)
Returns a (modifiable) reference to the coefficient corresponding to the given variable name.
void set_modulo(const scalar &c)
Sets the auxiliary scalar modulo to c (copied).
Definition: apxx_lincons1_inline.hh:106
void extend_environment(const environment &e)
Extends the environment of the expression.
Definition: apxx_lincons1_inline.hh:120
lincons1 & operator=(const lincons1 &x)
Makes a (deep) copy.
Definition: apxx_lincons1_inline.hh:90
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons1_inline.hh:250
ap_lincons1_t l
Structure managed by APRON.
Definition: apxx_lincons1.hh:44
bool is_quasilinear() const
Whether the underlying linear expression has only scalar coefficients, except maybe for the constant ...
Definition: apxx_lincons1_inline.hh:269
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_lincons1_inline.hh:155
lincons1(ap_lincons1_t p)
Internal use only. Shallow copy (no copy of lincons0 or environment).
Definition: apxx_lincons1_inline.hh:27
const lincons0 & get_lincons0() const
Returns a reference to the underlying lincons0.
Definition: apxx_lincons1_inline.hh:140
linexpr1 get_linexpr() const
Returns a copy of the underlying linear expression.
Definition: apxx_lincons1_inline.hh:189
coeff & get_cst()
Returns a (modifiable) reference to the constant coefficient.
Definition: apxx_lincons1_inline.hh:197
scalar & get_modulo()
Returns a (modifiable) reference to the auxiliary scalar.
Definition: apxx_lincons1_inline.hh:175
bool has_linexpr() const
Whether the constraint has a valid linear expression.
Definition: apxx_lincons1_inline.hh:170
~lincons1()
Frees all space for the expression and coefficients, and decrements the reference count of the enviro...
Definition: apxx_lincons1_inline.hh:81
bool is_unsat() const
Whether the constraint is unsatisfiable.
Definition: apxx_lincons1_inline.hh:259
Level 0 linear expression (ap_linexpr0_t wrapper).
Definition: apxx_linexpr0.hh:44
Level 1 linear expression (ap_linexpr1_t wrapper).
Definition: apxx_linexpr1.hh:39
const linexpr0 & get_linexpr0() const
Returns a reference to the underlying linexpr0.
Definition: apxx_linexpr1_inline.hh:102
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
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
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
Unsatisfiable constraint, to simplify initialisations and assignments.
Definition: apxx_lincons0.hh:28