27 inline lincons1::lincons1(ap_lincons1_t p) : l(p)
32 l = ap_lincons1_of_lincons0(const_cast<ap_environment_t*>(e.get_ap_environment_t()),
33 ap_lincons0_copy(const_cast<ap_lincons0_t*>(x.get_ap_lincons0_t())));
39 ap_linexpr1_make(const_cast<ap_environment_t*>(e.get_ap_environment_t()), AP_LINEXPR_SPARSE, 0);
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);
49 inline lincons1::lincons1(ap_constyp_t constyp,
const linexpr1& lin,
const scalar& modulo)
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);
58 l = ap_lincons1_make_unsat(const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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),
73 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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);
108 get_lincons0().set_modulo(c);
113 get_lincons0().set_linexpr(c.get_linexpr0());
123 throw std::invalid_argument(
"apron::lincons1::extend_environment(const environment&) empty expression");
125 ap_lincons1_extend_environment_with(&l,
126 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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));
152 return get_lincons0().size();
157 return get_lincons0().get_constyp();
162 return get_lincons0().get_constyp();
167 return get_lincons0().has_modulo();
172 return get_lincons0().has_linexpr();
178 throw std::invalid_argument(
"apron::lincons1::get_modulo() empty scalar");
179 return get_lincons0().get_modulo();
185 throw std::invalid_argument(
"apron::lincons1::get_modulo() empty scalar");
186 return get_lincons0().get_modulo();
192 throw std::invalid_argument(
"apron::lincons1::get_linexpr() empty expression");
193 linexpr0 ll = get_lincons0().get_linexpr();
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,
216 const_cast<ap_var_t>(var.get_ap_var_t()));
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));
266 return get_lincons0().is_linear();
271 return get_lincons0().is_quasilinear();
305 size_t sz = x.size();
306 a = ap_lincons1_array_make(const_cast<ap_environment_t*>(e.get_ap_environment_t()), sz);
307 for (
size_t i=0; i<sz; i++)
308 a.lincons0_array.p[i] = ap_lincons0_copy(&x.a.p[i]);
313 a = ap_lincons1_array_make(const_cast<ap_environment_t*>(e.get_ap_environment_t()), size);
318 size_t sz = x.size();
319 a = ap_lincons1_array_make(x.get_environment().get_ap_environment_t(), sz);
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),
329 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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);
370 a = ap_lincons1_array_make(x.get_environment().get_ap_environment_t(), sz);
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);
398 a = ap_lincons1_array_make(x[0].
get_environment().get_ap_environment_t(), size);
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,
418 const_cast<ap_environment_t*>(e.get_ap_environment_t()));
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));
443 return reinterpret_cast<lincons0_array&
>(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*>
458 (x.get_lincons0().get_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);
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));
lincons1(ap_lincons1_t p)
Internal use only. Shallow copy (no copy of lincons0 or environment).
Definition: apxx_lincons1.hh:28
coeff & get_cst()
Returns a (modifiable) reference to the constant coefficient.
Definition: apxx_lincons1.hh:198
void extend_environment(const environment &e)
Extends the environment of all expressions in array.
Definition: apxx_lincons1.hh:415
bool has_linexpr() const
Whether the constraint has a valid linear expression.
Definition: apxx_lincons1.hh:171
lincons1 get(size_t i) const
Returns a copy of the constraint at index i.
Definition: apxx_lincons1.hh:447
void resize(size_t size)
Resizes the array.
Definition: apxx_lincons1.hh:410
void set_modulo(const scalar &c)
Sets the auxiliary scalar modulo to c (copied).
Definition: apxx_lincons1.hh:107
lincons1 & operator=(const lincons1 &x)
Makes a (deep) copy.
Definition: apxx_lincons1.hh:91
friend std::ostream & operator<<(std::ostream &os, const lincons1_array &s)
Printing.
Definition: apxx_lincons1.hh:482
bool is_quasilinear() const
Whether the underlying linear expression has only scalar coefficients, except maybe for the constant ...
Definition: apxx_lincons1.hh:270
bool is_unsat() const
Whether the constraint is unsatisfiable.
Definition: apxx_lincons1.hh:260
const lincons0_array & get_lincons0_array() const
Returns a reference to the underlying lincons0_array.
Definition: apxx_lincons1.hh:437
ap_lincons1_array_t a
Structure managed by APRON.
Definition: apxx_lincons1.hh:335
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_lincons1.hh:156
void set_linexpr(const linexpr1 &c)
Sets the underlying linear expression to c (copied).
Definition: apxx_lincons1.hh:112
size_t size() const
Returns the size of the array.
Definition: apxx_lincons1.hh:427
size_t size() const
Returns the size of the underlying linear expression.
Definition: apxx_lincons1.hh:151
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons1.hh:491
~lincons1()
Frees all space for the expression and coefficients, and decrements the reference count of the enviro...
Definition: apxx_lincons1.hh:82
coeff & operator[](const var &v)
Returns a (modifiable) reference to the coefficient corresponding to the given variable name...
Definition: apxx_lincons1.hh:212
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.hh:500
void print(FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons1.hh:251
lincons1_array & operator=(const lincons1_array &x)
(Deep) copy.
Definition: apxx_lincons1.hh:366
scalar & get_modulo()
Returns a (modifiable) reference to the auxiliary scalar.
Definition: apxx_lincons1.hh:176
~lincons1_array()
Frees the space used by the array and all its constraints, and decrements the reference count of the ...
Definition: apxx_lincons1.hh:357
bool has_modulo() const
Whether the constraint has a valid auxiliary scalar (used in modulo constraints). ...
Definition: apxx_lincons1.hh:166
lincons1_array(ap_lincons1_array_t &a)
Internal use only. Shallow copy (no copy of lincons0_array or environment).
Definition: apxx_lincons1.hh:301
linexpr1 get_linexpr() const
Returns a copy of the underlying linear expression.
Definition: apxx_lincons1.hh:190
void set(size_t i, const lincons1 &x)
Changes the constraint at index i.
Definition: apxx_lincons1.hh:454
environment get_environment() const
Returns the environment of the constraint (with incremented reference count).
Definition: apxx_lincons1.hh:136
const lincons0 & get_lincons0() const
Returns a reference to the underlying lincons0.
Definition: apxx_lincons1.hh:141
environment get_environment() const
Returns the environment shared by all constraints (with incremented reference count).
Definition: apxx_lincons1.hh:432
bool is_linear() const
Whether the underlying linear expression has only scalar coefficients.
Definition: apxx_lincons1.hh:265
void extend_environment(const environment &e)
Extends the environment of the expression.
Definition: apxx_lincons1.hh:121
const ap_lincons1_t * get_ap_lincons1_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons1.hh:279