carl  24.04
Computer ARithmetic Library
IntervalEvaluation.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include <carl-arith/core/Common.h>
4 #include "BasicConstraint.h"
5 #include <carl-arith/interval/Interval.h>
6 #include <carl-arith/poly/umvpoly/functions/IntervalEvaluation.h>
7 #include <boost/logic/tribool_io.hpp>
8 
9 namespace carl {
10 
11 template<typename Number, typename Poly>
12 inline boost::tribool evaluate(const BasicConstraint<Poly>& c, const Assignment<Interval<Number>>& map) {
13  return evaluate(evaluate(c.lhs(), map), c.relation());
14 }
15 
16 /**
17  * Checks whether this constraint is consistent with the given assignment from
18  * the its variables to interval domains.
19  * @param _solutionInterval The interval domains of the variables.
20  * @return 1, if this constraint is consistent with the given intervals;
21  * 0, if this constraint is not consistent with the given intervals;
22  * 2, if it cannot be decided whether this constraint is consistent with the given intervals.
23  */
24 template<typename Pol>
25 static unsigned consistent_with(const BasicConstraint<Pol>& c, const Assignment<Interval<double>>& _solutionInterval) {
26  auto vars = variables(c);
27  if (vars.empty())
28  return carl::evaluate(c.lhs().constant_part(), c.relation()) ? 1 : 0;
29  else {
30  auto varIter = vars.begin();
31  auto varIntervalIter = _solutionInterval.begin();
32  while (varIter != vars.end() && varIntervalIter != _solutionInterval.end()) {
33  if (*varIter < varIntervalIter->first) {
34  return 2;
35  } else if (*varIter > varIntervalIter->first) {
36  ++varIntervalIter;
37  } else {
38  ++varIter;
39  ++varIntervalIter;
40  }
41  }
42  if (varIter != vars.end())
43  return 2;
44  Interval<double> solutionSpace = carl::evaluate(c.lhs(), _solutionInterval);
45  if (solutionSpace.is_empty())
46  return 2;
47  switch (c.relation()) {
48  case Relation::EQ: {
49  if (solutionSpace.is_zero())
50  return 1;
51  else if (!solutionSpace.contains(0))
52  return 0;
53  break;
54  }
55  case Relation::NEQ: {
56  if (!solutionSpace.contains(0))
57  return 1;
58  break;
59  }
60  case Relation::LESS: {
61  if (solutionSpace.upper_bound_type() != BoundType::INFTY) {
62  if (solutionSpace.upper() < 0)
63  return 1;
64  else if (solutionSpace.upper() == 0 && solutionSpace.upper_bound_type() == BoundType::STRICT)
65  return 1;
66  }
67  if (solutionSpace.lower_bound_type() != BoundType::INFTY && solutionSpace.lower() >= 0)
68  return 0;
69  break;
70  }
71  case Relation::GREATER: {
72  if (solutionSpace.lower_bound_type() != BoundType::INFTY) {
73  if (solutionSpace.lower() > 0)
74  return 1;
75  else if (solutionSpace.lower() == 0 && solutionSpace.lower_bound_type() == BoundType::STRICT)
76  return 1;
77  }
78  if (solutionSpace.upper_bound_type() != BoundType::INFTY && solutionSpace.upper() <= 0)
79  return 0;
80  break;
81  }
82  case Relation::LEQ: {
83  if (solutionSpace.upper_bound_type() != BoundType::INFTY && solutionSpace.upper() <= 0)
84  return 1;
85  if (solutionSpace.lower_bound_type() != BoundType::INFTY) {
86  if (solutionSpace.lower() > 0)
87  return 0;
88  else if (solutionSpace.lower() == 0 && solutionSpace.lower_bound_type() == BoundType::STRICT)
89  return 0;
90  }
91  break;
92  }
93  case Relation::GEQ: {
94  if (solutionSpace.lower_bound_type() != BoundType::INFTY && solutionSpace.lower() >= 0)
95  return 1;
96  if (solutionSpace.upper_bound_type() != BoundType::INFTY) {
97  if (solutionSpace.upper() < 0)
98  return 0;
99  else if (solutionSpace.upper() == 0 && solutionSpace.upper_bound_type() == BoundType::STRICT)
100  return 0;
101  }
102  break;
103  }
104  default: {
105  std::cout << "Error in isConsistent: unexpected relation symbol." << std::endl;
106  return 0;
107  }
108  }
109  return 2;
110  }
111 }
112 
113 /**
114  * Checks whether this constraint is consistent with the given assignment from
115  * the its variables to interval domains.
116  * @param _solutionInterval The interval domains of the variables.
117  * @param _stricterRelation This relation is set to a relation R such that this constraint and the given variable bounds
118  * imply the constraint formed by R, comparing this constraint's left-hand side to zero.
119  * @return 1, if this constraint is consistent with the given intervals;
120  * 0, if this constraint is not consistent with the given intervals;
121  * 2, if it cannot be decided whether this constraint is consistent with the given intervals.
122  */
123 template<typename Pol>
124 static unsigned consistent_with(const BasicConstraint<Pol>& c, const Assignment<Interval<double>>& _solutionInterval, Relation& _stricterRelation) {
125  _stricterRelation = c.relation();
126  auto vars = variables(c);
127  if (vars.empty())
128  return carl::evaluate(c.lhs().constant_part(), c.relation()) ? 1 : 0;
129  else {
130  auto varIter = vars.begin();
131  auto varIntervalIter = _solutionInterval.begin();
132  while (varIter != vars.end() && varIntervalIter != _solutionInterval.end()) {
133  if (*varIter < varIntervalIter->first) {
134  return 2;
135  } else if (*varIter > varIntervalIter->first) {
136  ++varIntervalIter;
137  } else {
138  ++varIter;
139  ++varIntervalIter;
140  }
141  }
142  if (varIter != vars.end())
143  return 2;
144  Interval<double> solutionSpace = carl::evaluate(c.lhs(), _solutionInterval);
145  if (solutionSpace.is_empty())
146  return 2;
147  switch (c.relation()) {
148  case Relation::EQ: {
149  if (solutionSpace.is_zero())
150  return 1;
151  else if (!solutionSpace.contains(0))
152  return 0;
153  break;
154  }
155  case Relation::NEQ: {
156  if (!solutionSpace.contains(0))
157  return 1;
158  if (solutionSpace.upper_bound_type() == BoundType::WEAK && solutionSpace.upper() == 0) {
159  _stricterRelation = Relation::LESS;
160  } else if (solutionSpace.lower_bound_type() == BoundType::WEAK && solutionSpace.lower() == 0) {
161  _stricterRelation = Relation::GREATER;
162  }
163  break;
164  }
165  case Relation::LESS: {
166  if (solutionSpace.upper_bound_type() != BoundType::INFTY) {
167  if (solutionSpace.upper() < 0)
168  return 1;
169  else if (solutionSpace.upper() == 0 && solutionSpace.upper_bound_type() == BoundType::STRICT)
170  return 1;
171  }
172  if (solutionSpace.lower_bound_type() != BoundType::INFTY && solutionSpace.lower() >= 0)
173  return 0;
174  break;
175  }
176  case Relation::GREATER: {
177  if (solutionSpace.lower_bound_type() != BoundType::INFTY) {
178  if (solutionSpace.lower() > 0)
179  return 1;
180  else if (solutionSpace.lower() == 0 && solutionSpace.lower_bound_type() == BoundType::STRICT)
181  return 1;
182  }
183  if (solutionSpace.upper_bound_type() != BoundType::INFTY && solutionSpace.upper() <= 0)
184  return 0;
185  break;
186  }
187  case Relation::LEQ: {
188  if (solutionSpace.upper_bound_type() != BoundType::INFTY) {
189  if (solutionSpace.upper() <= 0) {
190  return 1;
191  }
192  }
193  if (solutionSpace.lower_bound_type() != BoundType::INFTY) {
194  if (solutionSpace.lower() > 0) {
195  return 0;
196  } else if (solutionSpace.lower() == 0) {
197  if (solutionSpace.lower_bound_type() == BoundType::STRICT) {
198  return 0;
199  } else {
200  _stricterRelation = Relation::EQ;
201  }
202  }
203  }
204  break;
205  }
206  case Relation::GEQ: {
207  if (solutionSpace.lower_bound_type() != BoundType::INFTY) {
208  if (solutionSpace.lower() >= 0)
209  return 1;
210  }
211  if (solutionSpace.upper_bound_type() != BoundType::INFTY) {
212  if (solutionSpace.upper() < 0)
213  return 0;
214  else if (solutionSpace.upper() == 0) {
215  if (solutionSpace.upper_bound_type() == BoundType::STRICT)
216  return 0;
217  else
218  _stricterRelation = Relation::EQ;
219  }
220  }
221  break;
222  }
223  default: {
224  std::cout << "Error in isConsistent: unexpected relation symbol." << std::endl;
225  return 0;
226  }
227  }
228  return 2;
229  }
230 }
231 
232 }
carl
carl is the main namespace for the library.
carl::evaluate
bool evaluate(const BasicConstraint< Poly > &c, const Assignment< Number > &m)
Definition: Evaluation.h:10
carl::consistent_with
static unsigned consistent_with(const BasicConstraint< Pol > &c, const Assignment< Interval< double >> &_solutionInterval)
Checks whether this constraint is consistent with the given assignment from the its variables to inte...
Definition: IntervalEvaluation.h:25
carl::GREATER
@ GREATER
Definition: SignCondition.h:15
carl::BoundType::WEAK
@ WEAK
the given bound is compared by a weak ordering relation
carl::BoundType::STRICT
@ STRICT
the given bound is compared by a strict ordering relation
carl::BoundType::INFTY
@ INFTY
the given bound is interpreted as minus or plus infinity depending on whether it is the left or the r...
carl::Assignment
std::map< Variable, T > Assignment
Definition: Common.h:13
carl::Relation
Relation
Definition: Relation.h:20
carl::variables
void variables(const BasicConstraint< Pol > &c, carlVariables &vars)
Definition: BasicConstraint.h:139
carl::BasicConstraint
Represent a polynomial (in)equality against zero.
Definition: BasicConstraint.h:15
carl::BasicConstraint::lhs
const Pol & lhs() const
Definition: BasicConstraint.h:33
carl::BasicConstraint::relation
Relation relation() const
Definition: BasicConstraint.h:48
carl::Interval
The class which contains the interval arithmetic including trigonometric functions.
Definition: Interval.h:134
carl::Interval::is_empty
bool is_empty() const
Function which determines, if the interval is empty.
Definition: Interval.h:1056
carl::Interval::lower_bound_type
BoundType lower_bound_type() const
The getter for the lower bound type of the interval.
Definition: Interval.h:883
carl::Interval::upper
const Number & upper() const
The getter for the upper boundary of the interval.
Definition: Interval.h:849
carl::Interval::contains
bool contains(const Number &val) const
Checks if the interval contains the given value.
carl::Interval::lower
const Number & lower() const
The getter for the lower boundary of the interval.
Definition: Interval.h:840
carl::Interval::upper_bound_type
BoundType upper_bound_type() const
The getter for the upper bound type of the interval.
Definition: Interval.h:892
carl::Interval::is_zero
bool is_zero() const
Function which determines, if the interval is the zero interval.
Definition: Interval.h:1101