3 #include <poly/variable_list.h>
10 LPPolynomial::LPPolynomial(
const LPPolynomial& rhs)
11 : m_internal(lp_polynomial_new_copy(rhs.m_internal)), m_context(rhs.m_context) {
12 assert(lp_polynomial_check_order(get_internal()));
15 LPPolynomial::LPPolynomial(LPPolynomial&& rhs)
16 : m_internal(rhs.m_internal), m_context(std::move(rhs.m_context)) {
17 assert(lp_polynomial_check_order(get_internal()));
20 LPPolynomial& LPPolynomial::operator=(
const LPPolynomial& rhs) {
21 m_internal = lp_polynomial_new_copy(rhs.m_internal);
22 m_context = rhs.m_context;
23 assert(lp_polynomial_check_order(get_internal()));
27 LPPolynomial& LPPolynomial::operator=(LPPolynomial&& rhs) {
28 m_internal = rhs.m_internal;
29 m_context = std::move(rhs.m_context);
30 assert(lp_polynomial_check_order(get_internal()));
34 LPPolynomial::LPPolynomial(
const LPContext& context)
35 : m_internal(lp_polynomial_new(context.lp_context())), m_context(context) {
37 assert(lp_polynomial_check_order(get_internal()));
40 LPPolynomial::LPPolynomial(lp_polynomial_t* p,
const LPContext& context)
41 : m_internal(p), m_context(context) {
43 assert(lp_polynomial_check_order(get_internal()));
44 assert(context.lp_context() == lp_polynomial_get_context(get_internal()));
47 LPPolynomial::LPPolynomial(
const LPContext& context,
long val)
48 : m_internal(lp_polynomial_alloc()), m_context(context) {
49 lp_polynomial_construct_simple(get_internal(), context.lp_context(), mpz_class(val).get_mpz_t(), 0, 0);
51 assert(lp_polynomial_check_order(get_internal()));
54 LPPolynomial::LPPolynomial(
const LPContext& context,
const mpz_class& val)
55 : m_internal(lp_polynomial_alloc()), m_context(context) {
56 lp_polynomial_construct_simple(get_internal(), context.lp_context(), val.get_mpz_t(), lp_variable_null, 0) ;
58 assert(lp_polynomial_check_order(get_internal()));
61 LPPolynomial::LPPolynomial(
const LPContext& context,
const mpq_class& val) : LPPolynomial(context,
carl::
get_num(val)) {}
63 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& var,
const mpz_class& coeff,
unsigned int degree)
64 : m_internal(lp_polynomial_alloc()), m_context(context) {
65 lp_polynomial_construct_simple(get_internal(), context.lp_context(), mpz_class(coeff).get_mpz_t(), context.lp_variable(var), degree);
67 assert(lp_polynomial_check_order(get_internal()));
70 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& var)
71 : m_internal(lp_polynomial_alloc()), m_context(context) {
72 lp_polynomial_construct_simple(get_internal(), context.lp_context(), mpz_class(1).get_mpz_t(), context.lp_variable(var), 1);
74 assert(lp_polynomial_check_order(get_internal()));
77 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& mainVar,
const std::initializer_list<mpz_class>& coefficients)
78 : LPPolynomial(context) {
80 auto var = context.lp_variable(mainVar);
81 auto pow = coefficients.size();
83 for (
const mpz_class& coeff : coefficients) {
87 lp_monomial_construct(context.lp_context(), &t);
88 lp_monomial_set_coefficient(context.lp_context(), &t, mpz_class(coeff).get_mpz_t());
90 lp_monomial_push(&t, var, (
unsigned int)
pow);
91 lp_polynomial_add_monomial(get_internal(), &t);
92 lp_monomial_destruct(&t);
97 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& mainVar,
const std::vector<mpz_class>& coefficients)
98 : LPPolynomial(context) {
100 auto var = context.lp_variable(mainVar);
101 auto pow = coefficients.size();
103 for (
const mpz_class& coeff : coefficients) {
107 lp_monomial_construct(context.lp_context(), &t);
108 lp_monomial_set_coefficient(context.lp_context(), &t, mpz_class(coeff).get_mpz_t());
110 lp_monomial_push(&t, var, (
unsigned int)
pow);
111 lp_polynomial_add_monomial(get_internal(), &t);
112 lp_monomial_destruct(&t);
117 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& mainVar, std::vector<mpz_class>&& coefficients)
118 : LPPolynomial(context) {
120 auto var = context.lp_variable(mainVar);
121 auto pow = coefficients.size();
123 for (
const mpz_class& coeff : coefficients) {
127 lp_monomial_construct(context.lp_context(), &t);
128 lp_monomial_set_coefficient(context.lp_context(), &t, mpz_class(coeff).get_mpz_t());
130 lp_monomial_push(&t, var, (
unsigned int)
pow);
131 lp_polynomial_add_monomial(get_internal(), &t);
132 lp_monomial_destruct(&t);
137 LPPolynomial::LPPolynomial(
const LPContext& context,
const Variable& mainVar,
const std::map<unsigned int, mpz_class>& coefficients)
138 : LPPolynomial(context) {
140 auto var = context.lp_variable(mainVar);
142 for (
const auto& coeff : coefficients) {
143 if (
is_zero(coeff.second))
continue;
145 lp_monomial_construct(context.lp_context(), &t);
146 lp_monomial_set_coefficient(context.lp_context(), &t, mpz_class(coeff.second).get_mpz_t());
148 lp_monomial_push(&t, var, (
unsigned int)coeff.first);
149 lp_polynomial_add_monomial(get_internal(), &t);
150 lp_monomial_destruct(&t);
155 bool LPPolynomial::has(
const Variable& var)
const {
156 lp_variable_list_t varList;
157 lp_variable_list_construct(&varList);
158 lp_polynomial_get_variables(get_internal(), &varList);
159 auto lp_variable = context().lp_variable_opt(var);
160 if (!lp_variable)
return false;
161 bool contains = lp_variable_list_contains(&varList, *lp_variable);
162 lp_variable_list_destruct(&varList);
166 bool operator==(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
167 return lp_polynomial_eq(lhs.get_internal(), rhs.get_internal());
169 bool operator==(
const LPPolynomial& lhs,
const mpz_class& rhs) {
173 return lhs.constant_part() == rhs;
175 bool operator==(
const mpz_class& lhs,
const LPPolynomial& rhs) {
179 bool operator!=(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
180 return !(lhs == rhs);
182 bool operator!=(
const LPPolynomial& lhs,
const mpz_class& rhs) {
183 return !(lhs == rhs);
185 bool operator!=(
const mpz_class& lhs,
const LPPolynomial& rhs) {
186 return !(lhs == rhs);
189 inline auto cmp_util(
const LPPolynomial& lhs,
const mpz_class& rhs) {
191 auto res = lp_polynomial_cmp(lhs.get_internal(), tmp);
192 lp_polynomial_delete(tmp);
196 bool operator<(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
197 return lp_polynomial_cmp(lhs.get_internal(), rhs.get_internal()) < 0;
199 bool operator<(
const LPPolynomial& lhs,
const mpz_class& rhs) {
200 return cmp_util(lhs,rhs) < 0;
202 bool operator<(
const mpz_class& lhs,
const LPPolynomial& rhs) {
203 return cmp_util(rhs,lhs) > 0;
206 bool operator<=(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
207 return lp_polynomial_cmp(lhs.get_internal(), rhs.get_internal()) <= 0;
209 bool operator<=(
const LPPolynomial& lhs,
const mpz_class& rhs) {
210 return cmp_util(lhs,rhs) <= 0;
212 bool operator<=(
const mpz_class& lhs,
const LPPolynomial& rhs) {
213 return cmp_util(rhs,lhs) >= 0;
216 bool operator>(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
217 return lp_polynomial_cmp(lhs.get_internal(), rhs.get_internal()) > 0;
219 bool operator>(
const LPPolynomial& lhs,
const mpz_class& rhs) {
220 return cmp_util(lhs,rhs) > 0;
222 bool operator>(
const mpz_class& lhs,
const LPPolynomial& rhs) {
223 return cmp_util(rhs,lhs) < 0;
226 bool operator>=(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
227 return lp_polynomial_cmp(lhs.get_internal(), rhs.get_internal()) >= 0;
229 bool operator>=(
const LPPolynomial& lhs,
const mpz_class& rhs) {
230 return cmp_util(lhs,rhs) >= 0;
232 bool operator>=(
const mpz_class& lhs,
const LPPolynomial& rhs) {
233 return cmp_util(rhs,lhs) <= 0;
236 LPPolynomial
operator+(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
237 assert(rhs.context() == lhs.context());
238 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
239 LPPolynomial result(lhs.context());
240 lp_polynomial_add(result.get_internal(), lhs.get_internal(), rhs.get_internal());
243 LPPolynomial
operator+(
const LPPolynomial& lhs,
const mpz_class& rhs) {
244 return lhs + LPPolynomial(lhs.context(), rhs);
246 LPPolynomial
operator+(
const mpz_class& lhs,
const LPPolynomial& rhs) {
250 LPPolynomial
operator-(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
251 assert(rhs.context() == lhs.context());
252 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
253 LPPolynomial result(lhs.context());
254 lp_polynomial_sub(result.get_internal(), lhs.get_internal(), rhs.get_internal());
257 LPPolynomial
operator-(
const LPPolynomial& lhs,
const mpz_class& rhs) {
258 return lhs - LPPolynomial(lhs.context(), rhs);
260 LPPolynomial
operator-(
const mpz_class& lhs,
const LPPolynomial& rhs) {
261 return LPPolynomial(rhs.context(), lhs) - rhs;
264 LPPolynomial
operator*(
const LPPolynomial& lhs,
const LPPolynomial& rhs) {
265 assert(lhs.context() == rhs.context());
266 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
267 LPPolynomial result(lhs.context());
268 lp_polynomial_mul(result.get_internal(), lhs.get_internal(), rhs.get_internal());
271 LPPolynomial
operator*(
const LPPolynomial& lhs,
const mpz_class& rhs) {
272 return lhs * LPPolynomial(lhs.context(), rhs);
274 LPPolynomial
operator*(
const mpz_class& lhs,
const LPPolynomial& rhs) {
278 LPPolynomial&
operator+=(LPPolynomial& lhs,
const LPPolynomial& rhs) {
279 assert(rhs.context() == lhs.context());
280 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
281 lp_polynomial_add(lhs.get_internal(), lhs.get_internal(), rhs.get_internal());
284 LPPolynomial&
operator+=(LPPolynomial& lhs,
const mpz_class& rhs) {
286 lp_polynomial_add(lhs.get_internal(), lhs.get_internal(), tmp);
287 lp_polynomial_delete(tmp);
291 LPPolynomial&
operator-=(LPPolynomial& lhs,
const LPPolynomial& rhs) {
292 assert(rhs.context() == lhs.context());
293 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
294 lp_polynomial_sub(lhs.get_internal(), lhs.get_internal(), rhs.get_internal());
297 LPPolynomial&
operator-=(LPPolynomial& lhs,
const mpz_class& rhs) {
299 lp_polynomial_sub(lhs.get_internal(), lhs.get_internal(), tmp);
300 lp_polynomial_delete(tmp);
304 LPPolynomial&
operator*=(LPPolynomial& lhs,
const LPPolynomial& rhs) {
305 assert(rhs.context() == lhs.context());
306 assert(lp_polynomial_context_equal(lp_polynomial_get_context(lhs.get_internal()), lp_polynomial_get_context(rhs.get_internal())));
307 lp_polynomial_mul(lhs.get_internal(), lhs.get_internal(), rhs.get_internal());
310 LPPolynomial&
operator*=(LPPolynomial& lhs,
const mpz_class& rhs) {
312 lp_polynomial_mul(lhs.get_internal(), lhs.get_internal(), tmp);
313 lp_polynomial_delete(tmp);
317 mpz_class LPPolynomial::coprime_factor()
const {
319 struct coprime_factor_travers {
320 std::vector<mpz_class> coefficients;
323 auto getCoeffs = [](
const lp_polynomial_context_t* ,
326 coprime_factor_travers& v = *
static_cast<coprime_factor_travers*
>(d);
327 v.coefficients.push_back(*
reinterpret_cast<mpz_class*
>(&m->a));
331 coprime_factor_travers travers;
332 lp_polynomial_traverse(get_internal(), getCoeffs, &travers);
334 if (travers.coefficients.size() == 0) {
337 mpz_class res = travers.coefficients[0];
338 for (
size_t i = 1; i < travers.coefficients.size(); i++) {
339 res =
gcd(res, travers.coefficients[i]);
345 LPPolynomial LPPolynomial::coprime_coefficients()
const {
346 mpz_class g = coprime_factor();
347 if (g == 1)
return *
this;
349 lp_polynomial_t* res = lp_polynomial_new(context().lp_context());
350 lp_polynomial_div(res, get_internal(), temp);
351 lp_polynomial_delete(temp);
352 return LPPolynomial(res, context());
357 struct degree_travers {
358 std::size_t degree = 0;
361 auto getDegree = [](
const lp_polynomial_context_t* ,
364 degree_travers& v = *
static_cast<degree_travers*
>(d);
366 size_t current_degree = 0;
368 for (
size_t i = 0; i < m->n; i++) {
369 current_degree += m->p[i].d;
371 v.degree = std::max(v.degree, current_degree);
374 degree_travers travers;
375 lp_polynomial_traverse(get_internal(), getDegree, &travers);
377 return travers.degree;
380 std::size_t LPPolynomial::degree(Variable::Arg var)
const {
381 struct degree_travers {
382 std::size_t degree = 0;
386 auto getDegree = [](
const lp_polynomial_context_t* ,
389 degree_travers& v = *
static_cast<degree_travers*
>(d);
391 size_t current_degree = 0;
393 for (
size_t i = 0; i < m->n; i++) {
394 if (m->p[i].x == v.var) {
395 current_degree = m->p[i].d;
399 v.degree = std::max(v.degree, current_degree);
402 degree_travers travers;
403 travers.var = context().lp_variable(var);
404 lp_polynomial_traverse(get_internal(), getDegree, &travers);
406 return travers.degree;
409 std::vector<std::size_t> LPPolynomial::monomial_total_degrees()
const {
410 struct degree_travers {
411 std::vector<std::size_t> degree;
414 auto getDegree = [](
const lp_polynomial_context_t* ,
417 degree_travers& v = *
static_cast<degree_travers*
>(d);
419 size_t current_degree = 0;
421 for (
size_t i = 0; i < m->n; i++) {
422 current_degree += m->p[i].d;
424 v.degree.push_back(current_degree);
427 degree_travers travers;
428 lp_polynomial_traverse(get_internal(), getDegree, &travers);
430 return travers.degree;
433 std::vector<std::size_t> LPPolynomial::monomial_degrees(Variable::Arg var)
const {
434 struct degree_travers {
435 std::vector<std::size_t> degree;
439 auto getDegree = [](
const lp_polynomial_context_t* ,
442 degree_travers& v = *
static_cast<degree_travers*
>(d);
444 size_t current_degree = 0;
446 for (
size_t i = 0; i < m->n; i++) {
447 if (m->p[i].x == v.var) {
448 current_degree = m->p[i].d;
452 v.degree.push_back(current_degree);
455 degree_travers travers;
456 travers.var = context().lp_variable(var);
457 lp_polynomial_traverse(get_internal(), getDegree, &travers);
459 return travers.degree;
462 mpz_class LPPolynomial::unit_part()
const {
469 return lp_polynomial_lc_sgn(get_internal()) ;
472 LPPolynomial LPPolynomial::normalized()
const {
473 auto res = coprime_coefficients();
474 auto unit = res.unit_part() ;
485 LPPolynomial LPPolynomial::coeff(Variable::Arg var, std::size_t
exp)
const {
486 struct coeff_travers {
487 std::vector<lp_monomial_t> coeff;
488 const lp_polynomial_context_t* ctx;
494 auto getCoeff = [](
const lp_polynomial_context_t* ,
497 coeff_travers& v = *
static_cast<coeff_travers*
>(d);
501 for (
size_t i = 0; i < m->n; i++) {
502 if (m->p[i].x == v.var && m->p[i].d == v.exp) {
513 lp_monomial_t new_monomial;
514 lp_monomial_construct(v.ctx, &new_monomial);
515 new_monomial.n = m->n -1 ;
516 new_monomial.capacity = m->capacity ;
517 lp_integer_assign(v.ctx->K, &new_monomial.a ,&m->a);
518 new_monomial.p = (power_t*)realloc(new_monomial.p,
sizeof(power_t) * new_monomial.capacity);
520 size_t current_counter = 0 ;
521 for(
size_t i = 0; i < m->n; i++){
522 if(m->p[i].x == v.var && m->p[i].d == v.exp){
525 new_monomial.p[current_counter].x = m->p[i].x;
526 new_monomial.p[current_counter].d = m->p[i].d;
529 assert(current_counter == new_monomial.n);
530 v.coeff.push_back(std::move(new_monomial));
533 coeff_travers travers;
534 travers.var = context().lp_variable(var);
536 travers.ctx = lp_polynomial_get_context(get_internal());
537 lp_polynomial_traverse(get_internal(), getCoeff, &travers);
539 LPPolynomial res(context());
540 for (
auto m : travers.coeff) {
541 lp_polynomial_add_monomial(res.get_internal(), &m);
545 for(
auto& m : travers.coeff){
546 lp_monomial_destruct(&m);
552 bool LPPolynomial::is_normal()
const {
557 std::ostream&
operator<<(std::ostream& os,
const LPPolynomial& p) {
558 os << lp_polynomial_to_string(p.get_internal());
562 void LPPolynomial::set_context(
const LPContext& c) {
563 for (
auto& v :
variables(*
this)) assert(c.has(v));
564 if (context() == c)
return;
566 bool reorder = !(c.is_extension_of(context()) || context().is_extension_of(c));
568 lp_polynomial_set_context(get_internal(), m_context.lp_context());
570 lp_polynomial_ensure_order(get_internal());
572 assert(lp_polynomial_check_order(get_internal()));
std::ostream & operator<<(std::ostream &os, const GbBenchmark< C, O, P > &b)
carl is the main namespace for the library.
bool operator>(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
Interval< Number > operator+(const Interval< Number > &lhs, const Interval< Number > &rhs)
Operator for the addition of two intervals.
bool operator<(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
cln::cl_I gcd(const cln::cl_I &a, const cln::cl_I &b)
Calculate the greatest common divisor of two integers.
Interval< Number > exp(const Interval< Number > &i)
bool is_zero(const Interval< Number > &i)
Check if this interval is a point-interval containing 0.
Interval< Number > operator*(const Interval< Number > &lhs, const Interval< Number > &rhs)
Operator for the multiplication of two intervals.
cln::cl_I get_num(const cln::cl_RA &n)
Extract the numerator from a fraction.
Interval< Number > & operator*=(Interval< Number > &lhs, const Interval< Number > &rhs)
Operator for the multiplication of an interval and a number with assignment.
Interval< Number > & operator+=(Interval< Number > &lhs, const Interval< Number > &rhs)
Operator for the addition of an interval and a number with assignment.
Interval< Number > operator-(const Interval< Number > &rhs)
Unary minus.
bool operator!=(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
bool operator<=(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
bool operator==(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
bool operator>=(const BasicConstraint< P > &lhs, const BasicConstraint< P > &rhs)
Interval< Number > & operator-=(Interval< Number > &lhs, const Interval< Number > &rhs)
Operator for the subtraction of two intervals with assignment.
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
Interval< Number > pow(const Interval< Number > &i, Integer exp)
auto total_degree(const Monomial &m)
Gives the total degree, i.e.
bool is_one(const Interval< Number > &i)
Check if this interval is a point-interval containing 1.
lp_polynomial_t * construct_lp_poly(const lp_polynomial_context_t *c, lp_variable_t v)