23 inline lincons0::lincons0(ap_lincons0_t l) : l(l) {}
27 ap_linexpr0_t* llin = ap_linexpr0_alloc(AP_LINEXPR_SPARSE,0);
28 l = ap_lincons0_make(constyp, llin, NULL);
31 inline lincons0::lincons0(ap_constyp_t constyp,
const linexpr0& lin,
const scalar& modulo)
33 ap_linexpr0_t* llin = ap_linexpr0_copy(const_cast<ap_linexpr0_t*>(lin.get_ap_linexpr0_t()));
34 ap_scalar_t* mmodulo = ap_scalar_alloc_set(const_cast<ap_scalar_t*>(modulo.get_ap_scalar_t()));
35 l = ap_lincons0_make(constyp, llin, mmodulo);
40 ap_linexpr0_t* llin = ap_linexpr0_copy(const_cast<ap_linexpr0_t*>(lin.get_ap_linexpr0_t()));
41 l = ap_lincons0_make(constyp, llin, NULL);
46 l = ap_lincons0_copy(const_cast<ap_lincons0_t*>(&x.l));
51 l = ap_lincons0_make_unsat();
56 if (!x.l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::lincons0(const dimchange&) empty expression");
57 l = ap_lincons0_add_dimensions(const_cast<ap_lincons0_t*>(&x.l),
58 const_cast<ap_dimchange_t*>(d.get_ap_dimchange_t()));
63 if (!x.l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::lincons0(const dimperm&) empty expression");
64 l = ap_lincons0_permute_dimensions(const_cast<ap_lincons0_t*>(&x.l),
65 const_cast<ap_dimperm_t*>(d.get_ap_dimperm_t()));
74 ap_lincons0_clear(&l);
84 ap_lincons0_clear(&l);
85 l = ap_lincons0_copy(const_cast<ap_lincons0_t*>(&x.l));
92 ap_lincons0_clear(&l);
93 l = ap_lincons0_make_unsat();
103 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::resize(size_t) empty expression");
104 ap_linexpr0_realloc(l.linexpr0, size);
110 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::add_dimensions(const dimchange&) empty expression");
111 ap_lincons0_add_dimensions_with(&l, const_cast<ap_dimchange_t*>(d.get_ap_dimchange_t()));
116 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::permute_dimensions(const dimperm&) empty expression");
117 ap_lincons0_permute_dimensions_with(&l, const_cast<ap_dimperm_t*>(d.get_ap_dimperm_t()));
128 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::size() empty expression");
129 return ap_linexpr0_size(const_cast<ap_linexpr0_t*>(l.linexpr0));
147 return l.scalar!=NULL;
152 return l.linexpr0!=NULL;
157 if (!l.scalar)
throw std::invalid_argument(
"apron::lincons0::get_modulo() empty scalar");
158 return reinterpret_cast<scalar&
>(*l.scalar);
163 if (!l.scalar)
throw std::invalid_argument(
"apron::lincons0::get_modulo() empty scalar");
164 return reinterpret_cast<scalar&
>(*l.scalar);
169 if (!l.scalar) l.scalar = ap_scalar_alloc_set(const_cast<ap_scalar_t*>(c.get_ap_scalar_t()));
170 else ap_scalar_set(l.scalar, const_cast<ap_scalar_t*>(c.get_ap_scalar_t()));
175 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::get_linexpr() empty expression");
176 return reinterpret_cast<linexpr0&
>(*l.linexpr0);
181 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::get_linexpr() empty expression");
182 return reinterpret_cast<linexpr0&
>(*l.linexpr0);
187 if (l.linexpr0) ap_linexpr0_free(l.linexpr0);
188 l.linexpr0 = ap_linexpr0_copy(const_cast<ap_linexpr0_t*>(c.get_ap_linexpr0_t()));
192 {
return get_linexpr().get_cst(); }
195 {
return get_linexpr().get_cst(); }
198 {
return get_linexpr()[dim]; }
201 {
return get_linexpr()[dim]; }
207 inline std::ostream&
operator<< (std::ostream& os,
const lincons0& s)
209 os << s.get_linexpr();
210 switch (s.get_constyp()) {
211 case AP_CONS_EQ:
return os <<
" = 0";
212 case AP_CONS_SUPEQ:
return os <<
" >= 0";
213 case AP_CONS_SUP:
return os <<
" > 0";
214 case AP_CONS_EQMOD:
return os <<
" = 0 mod " << s.get_modulo();
215 case AP_CONS_DISEQ:
return os <<
" != 0";
216 default:
throw std::invalid_argument(
"apron::operator<<(ostream&, const lincons0&) unknown constraint type");
222 ap_lincons0_fprint(stream, const_cast<ap_lincons0_t*>(&l), name_of_dim);
231 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::is_unsat() empty expression");
232 return ap_lincons0_is_unsat(const_cast<ap_lincons0_t*>(&l));
237 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::is_linear() empty expression");
238 return ap_linexpr0_is_linear(l.linexpr0);
243 if (!l.linexpr0)
throw std::invalid_argument(
"apron::lincons0::is_quasilinear() empty expression");
244 return ap_linexpr0_is_quasilinear(l.linexpr0);
272 :
a(ap_lincons0_array_make(size))
277 :
a(ap_lincons0_array_make(x.a.size))
279 for (
size_t i=0; i<
a.size; i++)
280 a.p[i] = ap_lincons0_copy(&x.a.p[i]);
284 :
a(ap_lincons0_array_make(size))
286 for (
size_t i=0; i<
size; i++)
287 a.p[i] = ap_lincons0_copy(const_cast<ap_lincons0_t*>(x[i].get_ap_lincons0_t()));
291 :
a(ap_lincons0_array_make(x.size()))
293 for (
size_t i=0; i<
a.size; i++)
294 a.p[i] = ap_lincons0_copy(const_cast<ap_lincons0_t*>(x[i].get_ap_lincons0_t()));
299 a = ap_lincons0_array_add_dimensions(const_cast<ap_lincons0_array_t*>(&x.a),
300 const_cast<ap_dimchange_t*>(d.get_ap_dimchange_t()));
305 a = ap_lincons0_array_permute_dimensions(const_cast<ap_lincons0_array_t*>(&x.a),
306 const_cast<ap_dimperm_t*>(d.get_ap_dimperm_t()));
315 ap_lincons0_array_clear(&
a);
325 ap_lincons0_array_clear(&
a);
326 a = ap_lincons0_array_make(x.a.size);
327 for (
size_t i=0; i<
a.size; i++)
a.p[i] = ap_lincons0_copy(&x.a.p[i]);
334 size_t size =
a.size;
335 ap_lincons0_array_clear(&
a);
336 a = ap_lincons0_array_make(size);
337 for (
size_t i=0; i<
size; i++)
338 a.p[i] = ap_lincons0_copy(const_cast<ap_lincons0_t*>(x[i].get_ap_lincons0_t()));
344 size_t size = x.size();
345 ap_lincons0_array_clear(&
a);
346 a = ap_lincons0_array_make(size);
347 for (
size_t i=0; i<
size; i++)
348 a.p[i] = ap_lincons0_copy(const_cast<ap_lincons0_t*>(x[i].get_ap_lincons0_t()));
358 ap_lincons0_array_resize(&
a, size);
363 ap_lincons0_array_add_dimensions_with(&
a, const_cast<ap_dimchange_t*>(d.get_ap_dimchange_t()));
368 ap_lincons0_array_permute_dimensions_with(&
a, const_cast<ap_dimperm_t*>(d.get_ap_dimperm_t()));
382 return reinterpret_cast<lincons0*
>(
a.p);
387 return reinterpret_cast<lincons0*
>(
a.p);
392 return reinterpret_cast<lincons0&
>(
a.p[i]);
397 return reinterpret_cast<lincons0&
>(
a.p[i]);
402 if (i >=
a.size)
throw std::out_of_range(
"apron::lincons0_array::get(size_t)");
403 return reinterpret_cast<lincons0&
>(
a.p[i]);
408 if (i >=
a.size)
throw std::out_of_range(
"apron::lincons0_array::get(size_t)");
409 return reinterpret_cast<lincons0&
>(
a.p[i]);
416 inline lincons0_array::operator std::vector<lincons0>()
const 419 std::vector<lincons0> v = std::vector<lincons0>(sz);
420 for (
size_t i=0;i<sz;i++)
431 size_t sz = s.size();
433 for (
size_t i=0;i<sz;i++)
440 ap_lincons0_array_fprint(stream, const_cast<ap_lincons0_array_t*>(&
a), name_of_dim);
449 return ap_lincons0_array_is_linear(const_cast<ap_lincons0_array_t*>(&
a));
454 return ap_lincons0_array_is_quasilinear(const_cast<ap_lincons0_array_t*>(&
a));
size_t size() const
Returns the size of the array.
Definition: apxx_lincons0.hh:376
lincons0(ap_lincons0_t l)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_lincons0.hh:24
friend std::ostream & operator<<(std::ostream &os, const lincons0_array &s)
Printing.
Definition: apxx_lincons0.hh:430
void set_linexpr(const linexpr0 &c)
Sets the underlying linear expression to c (copied).
Definition: apxx_lincons0.hh:186
bool is_linear() const
Whether the underlying linear expression has only scalar coefficients.
Definition: apxx_lincons0.hh:236
void set_modulo(const scalar &c)
Sets the auxiliary scalar modulo to c (copied).
Definition: apxx_lincons0.hh:168
coeff & get_cst()
Returns a (modifiable) reference to the constant coefficient.
Definition: apxx_lincons0.hh:192
lincons0_array(ap_lincons0_array_t &a)
Internal use only. Performs a shallow copy and takes ownership of the contents.
Definition: apxx_lincons0.hh:348
~lincons0_array()
Frees the space used by the array and all its constraints.
Definition: apxx_lincons0.hh:314
bool has_modulo() const
Whether the constraint has a valid auxiliary scalar (used in modulo constraints). ...
Definition: apxx_lincons0.hh:146
bool is_quasilinear() const
Whether the underlying linear expression has only scalar coefficients, except maybe for the constant ...
Definition: apxx_lincons0.hh:242
void add_dimensions(const dimchange &d)
Applies add_dimensions to all constraints in the array.
Definition: apxx_lincons0.hh:362
void permute_dimensions(const dimperm &d)
Applies permute_dimensions to all constraints in the array.
Definition: apxx_lincons0.hh:367
scalar & get_modulo()
Returns a (modifiable) reference to the auxiliary scalar.
Definition: apxx_lincons0.hh:156
const ap_lincons0_array_t * get_ap_lincons0_array_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons0.hh:463
void print(char **name_of_dim=NULL, FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons0.hh:439
bool is_quasilinear() const
Whether all constraints are quasi-linear.
Definition: apxx_lincons0.hh:453
void resize(size_t size)
Resizes the array.
Definition: apxx_lincons0.hh:357
~lincons0()
Frees the constraint, including the embedded linear expression and optional modulo scalar...
Definition: apxx_lincons0.hh:73
void add_dimensions(const dimchange &d)
Changes the dimension of the underlying linear expression.
Definition: apxx_lincons0.hh:109
const ap_lincons0_t * get_ap_lincons0_t() const
Returns a pointer to the internal APRON object stored in *this.
Definition: apxx_lincons0.hh:253
ap_lincons0_array_t a
Structure managed by APRON.
Definition: apxx_lincons0.hh:345
lincons0_array & operator=(const lincons0_array &x)
(Deep) copy.
Definition: apxx_lincons0.hh:323
linexpr0 & get_linexpr()
Returns a (modifiable) reference to the underlying linear expression.
Definition: apxx_lincons0.hh:174
lincons0 & operator=(const lincons0 &x)
(Deep) copy.
Definition: apxx_lincons0.hh:82
void resize(size_t size)
Resizes the underlying linear expression.
Definition: apxx_lincons0.hh:102
coeff & operator[](ap_dim_t dim)
Returns a (modifiable) reference to the coefficient corresponding to the given dimension.
Definition: apxx_lincons0.hh:198
bool is_unsat() const
Whether the constraint is unsatisfiable.
Definition: apxx_lincons0.hh:230
lincons0 * contents()
Returns a pointer to the start of the internal array holding the constraints.
Definition: apxx_lincons0.hh:381
bool is_linear() const
Whether all constraints are linear.
Definition: apxx_lincons0.hh:448
lincons0 & get(size_t i)
Returns a (modifiable) reference to an element (bound-checked).
Definition: apxx_lincons0.hh:401
bool has_linexpr() const
Whether the constraint has a valid linear expression.
Definition: apxx_lincons0.hh:151
lincons0 & operator[](size_t i)
Returns a (modifiable) reference to an element, no bound checking.
Definition: apxx_lincons0.hh:391
void permute_dimensions(const dimperm &d)
Applies a permutation to the underlying linear expression.
Definition: apxx_lincons0.hh:115
size_t size() const
Returns the size of the underlying linear expression.
Definition: apxx_lincons0.hh:127
ap_constyp_t & get_constyp()
Returns a (modifiable) reference to the constraint type.
Definition: apxx_lincons0.hh:136
void print(char **name_of_dim=NULL, FILE *stream=stdout) const
Prints to a C stream.
Definition: apxx_lincons0.hh:221