carl  24.04
Computer ARithmetic Library
Evaluation.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "BasicConstraint.h"
5 #include "../poly/umvpoly/functions/Substitution.h"
6 
7 namespace carl {
8 
9 template<typename Number, typename Poly, typename = std::enable_if_t<is_number_type<Number>::value>>
11  auto res = evaluate(c.lhs(), m);
12  return evaluate(res, c.relation());
13 }
14 
15 /**
16  * Checks whether the given assignment satisfies this constraint.
17  * @param _assignment The assignment.
18  * @return 1, if the given assignment satisfies this constraint.
19  * 0, if the given assignment contradicts this constraint.
20  * 2, otherwise (possibly not defined for all variables in the constraint,
21  * even then it could be possible to obtain the first two results.)
22  */
23 template<typename Pol>
25  unsigned result = 2;
26  Pol tmp = carl::substitute(c.lhs(), _assignment);
27  if (tmp.is_constant()) {
28  result = carl::evaluate((is_zero(tmp) ? typename Pol::NumberType(0) : tmp.trailingTerm().coeff()), c.relation()) ? 1 : 0;
29  }
30  return result;
31 }
32 
33 }
MultivariatePolynomial< Rational > Pol
Definition: HornerTest.cpp:17
carl is the main namespace for the library.
unsigned satisfied_by(const BasicConstraint< Pol > &c, const Assignment< typename Pol::NumberType > &_assignment)
Checks whether the given assignment satisfies this constraint.
Definition: Evaluation.h:24
bool is_zero(const Interval< Number > &i)
Check if this interval is a point-interval containing 0.
Definition: Interval.h:1453
bool evaluate(const BasicConstraint< Poly > &c, const Assignment< Number > &m)
Definition: Evaluation.h:10
Coeff substitute(const Monomial &m, const std::map< Variable, Coeff > &substitutions)
Applies the given substitutions to a monomial.
Definition: Substitution.h:19
std::map< Variable, T > Assignment
Definition: Common.h:13
Represent a polynomial (in)equality against zero.
const Pol & lhs() const
Relation relation() const