carl  24.04
Computer ARithmetic Library
Comparison.h
Go to the documentation of this file.
1 #pragma once
2 
3 #include "BasicConstraint.h"
4 
5 namespace carl {
6 
7 const signed A_IFF_B = 2;
8 const signed A_IMPLIES_B = 1;
9 const signed B_IMPLIES_A = -1;
10 const signed NOT__A_AND_B = -2;
11 const signed A_AND_B__IFF_C = -3;
12 const signed A_XOR_B = -4;
13 
14 /**
15  * Compares _constraintA with _constraintB.
16  * @return 2, if it is easy to decide that _constraintA and _constraintB have the same solutions. _constraintA = _constraintB
17  * 1, if it is easy to decide that _constraintB includes all solutions of _constraintA; _constraintA -> _constraintB
18  * -1, if it is easy to decide that _constraintA includes all solutions of _constraintB; _constraintB -> _constraintA
19  * -2, if it is easy to decide that _constraintA has no solution common with _constraintB; not(_constraintA and _constraintB)
20  * -3, if it is easy to decide that _constraintA and _constraintB can be intersected; _constraintA and _constraintB = _constraintC
21  * -4, if it is easy to decide that _constraintA is the inverse of _constraintB; _constraintA xor _constraintB
22  * 0, otherwise.
23  */
24 template<typename Pol>
25 signed compare(const BasicConstraint<Pol>& _constraintA, const BasicConstraint<Pol>& _constraintB) {
26  /*
27  * Check whether it holds that
28  *
29  * _constraintA = a_1*m_1+...+a_k*m_k + c ~ 0
30  * and
31  * _constraintB = b_1*m_1+...+b_k*m_k + d ~ 0,
32  *
33  * where a_1,..., a_k, b_1,..., b_k, c, d are rational coefficients,
34  * m_1,..., m_k are non-constant monomials and
35  * exists a rational g such that
36  *
37  * a_i = g * b_i for all 1<=i<=k
38  * or b_i = g * a_i for all 1<=i<=k
39  */
40  typename Pol::NumberType one_divided_by_a = _constraintA.lhs().coprime_factor_without_constant();
41  typename Pol::NumberType one_divided_by_b = _constraintB.lhs().coprime_factor_without_constant();
42  typename Pol::NumberType c = _constraintA.lhs().constant_part();
43  typename Pol::NumberType d = _constraintB.lhs().constant_part();
44  assert(carl::is_one(carl::get_num(carl::abs(one_divided_by_b))));
45  Pol tmpA = (_constraintA.lhs() - c) * one_divided_by_a;
46  Pol tmpB = (_constraintB.lhs() - d) * one_divided_by_b;
47  // std::cout << "tmpA = " << tmpA << std::endl;
48  // std::cout << "tmpB = " << tmpB << std::endl;
49  if (tmpA != tmpB) return 0;
50  bool termACoeffGreater = false;
51  bool signsDiffer = (one_divided_by_a < carl::constant_zero<typename Pol::NumberType>::get()) != (one_divided_by_b < carl::constant_zero<typename Pol::NumberType>::get());
52  typename Pol::NumberType g;
53  if (carl::get_denom(one_divided_by_a) > carl::get_denom(one_divided_by_b)) {
54  g = typename Pol::NumberType(carl::get_denom(one_divided_by_a)) / carl::get_denom(one_divided_by_b);
55  if (signsDiffer)
56  g = -g;
57  termACoeffGreater = true;
58  d *= g;
59  } else {
60  g = typename Pol::NumberType(carl::get_denom(one_divided_by_b)) / carl::get_denom(one_divided_by_a);
61  if (signsDiffer)
62  g = -g;
63  c *= g;
64  }
65  // Apply the multiplication by a negative g to the according relation symbol, which
66  // has to be turned around then.
67  Relation relA = _constraintA.relation();
68  Relation relB = _constraintB.relation();
69  if (g < 0) {
70  if (termACoeffGreater) {
71  switch (relB) {
72  case Relation::LEQ:
73  relB = Relation::GEQ;
74  break;
75  case Relation::GEQ:
76  relB = Relation::LEQ;
77  break;
78  case Relation::LESS:
79  relB = Relation::GREATER;
80  break;
81  case Relation::GREATER:
82  relB = Relation::LESS;
83  break;
84  default:
85  break;
86  }
87  } else {
88  switch (relA) {
89  case Relation::LEQ:
90  relA = Relation::GEQ;
91  break;
92  case Relation::GEQ:
93  relA = Relation::LEQ;
94  break;
95  case Relation::LESS:
96  relA = Relation::GREATER;
97  break;
98  case Relation::GREATER:
99  relA = Relation::LESS;
100  break;
101  default:
102  break;
103  }
104  }
105  }
106  // std::cout << "c = " << c << std::endl;
107  // std::cout << "d = " << d << std::endl;
108  // std::cout << "g = " << g << std::endl;
109  // std::cout << "relA = " << relA << std::endl;
110  // std::cout << "relB = " << relB << std::endl;
111  // Compare the adapted constant parts.
112  switch (relB) {
113  case Relation::EQ:
114  switch (relA) {
115  case Relation::EQ: // p+c=0 and p+d=0
116  if (c == d) return A_IFF_B;
117  return NOT__A_AND_B;
118  case Relation::NEQ: // p+c!=0 and p+d=0
119  if (c == d) return A_XOR_B;
120  return B_IMPLIES_A;
121  case Relation::LESS: // p+c<0 and p+d=0
122  if (c < d) return B_IMPLIES_A;
123  return NOT__A_AND_B;
124  case Relation::GREATER: // p+c>0 and p+d=0
125  if (c > d) return B_IMPLIES_A;
126  return NOT__A_AND_B;
127  case Relation::LEQ: // p+c<=0 and p+d=0
128  if (c <= d) return B_IMPLIES_A;
129  return NOT__A_AND_B;
130  case Relation::GEQ: // p+c>=0 and p+d=0
131  if (c >= d) return B_IMPLIES_A;
132  return NOT__A_AND_B;
133  default:
134  return false;
135  }
136  case Relation::NEQ:
137  switch (relA) {
138  case Relation::EQ: // p+c=0 and p+d!=0
139  if (c == d) return A_XOR_B;
140  return A_IMPLIES_B;
141  case Relation::NEQ: // p+c!=0 and p+d!=0
142  if (c == d) return A_IFF_B;
143  return 0;
144  case Relation::LESS: // p+c<0 and p+d!=0
145  if (c >= d) return A_IMPLIES_B;
146  return 0;
147  case Relation::GREATER: // p+c>0 and p+d!=0
148  if (c <= d) return A_IMPLIES_B;
149  return 0;
150  case Relation::LEQ: // p+c<=0 and p+d!=0
151  if (c > d) return A_IMPLIES_B;
152  if (c == d) return A_AND_B__IFF_C;
153  return 0;
154  case Relation::GEQ: // p+c>=0 and p+d!=0
155  if (c < d) return A_IMPLIES_B;
156  if (c == d) return A_AND_B__IFF_C;
157  return 0;
158  default:
159  return 0;
160  }
161  case Relation::LESS:
162  switch (relA) {
163  case Relation::EQ: // p+c=0 and p+d<0
164  if (c > d) return A_IMPLIES_B;
165  return NOT__A_AND_B;
166  case Relation::NEQ: // p+c!=0 and p+d<0
167  if (c <= d) return B_IMPLIES_A;
168  return 0;
169  case Relation::LESS: // p+c<0 and p+d<0
170  if (c == d) return A_IFF_B;
171  if (c < d) return B_IMPLIES_A;
172  return A_IMPLIES_B;
173  case Relation::GREATER: // p+c>0 and p+d<0
174  if (c <= d) return NOT__A_AND_B;
175  return 0;
176  case Relation::LEQ: // p+c<=0 and p+d<0
177  if (c > d) return A_IMPLIES_B;
178  return B_IMPLIES_A;
179  case Relation::GEQ: // p+c>=0 and p+d<0
180  if (c < d) return NOT__A_AND_B;
181  if (c == d) return A_XOR_B;
182  return 0;
183  default:
184  return 0;
185  }
186  case Relation::GREATER: {
187  switch (relA) {
188  case Relation::EQ: // p+c=0 and p+d>0
189  if (c < d) return A_IMPLIES_B;
190  return NOT__A_AND_B;
191  case Relation::NEQ: // p+c!=0 and p+d>0
192  if (c >= d) return B_IMPLIES_A;
193  return 0;
194  case Relation::LESS: // p+c<0 and p+d>0
195  if (c >= d) return NOT__A_AND_B;
196  return 0;
197  case Relation::GREATER: // p+c>0 and p+d>0
198  if (c == d) return A_IFF_B;
199  if (c > d) return B_IMPLIES_A;
200  return A_IMPLIES_B;
201  case Relation::LEQ: // p+c<=0 and p+d>0
202  if (c > d) return NOT__A_AND_B;
203  if (c == d) return A_XOR_B;
204  return 0;
205  case Relation::GEQ: // p+c>=0 and p+d>0
206  if (c > d) return B_IMPLIES_A;
207  return A_IMPLIES_B;
208  default:
209  return 0;
210  }
211  }
212  case Relation::LEQ: {
213  switch (relA) {
214  case Relation::EQ: // p+c=0 and p+d<=0
215  if (c >= d) return A_IMPLIES_B;
216  return NOT__A_AND_B;
217  case Relation::NEQ: // p+c!=0 and p+d<=0
218  if (c < d) return B_IMPLIES_A;
219  if (c == d) return A_AND_B__IFF_C;
220  return 0;
221  case Relation::LESS: // p+c<0 and p+d<=0
222  if (c < d) return B_IMPLIES_A;
223  return A_IMPLIES_B;
224  case Relation::GREATER: // p+c>0 and p+d<=0
225  if (c < d) return NOT__A_AND_B;
226  if (c == d) return A_XOR_B;
227  return 0;
228  case Relation::LEQ: // p+c<=0 and p+d<=0
229  if (c == d) return A_IFF_B;
230  if (c < d) return B_IMPLIES_A;
231  return A_IMPLIES_B;
232  case Relation::GEQ: // p+c>=0 and p+d<=0
233  if (c < d) return NOT__A_AND_B;
234  if (c == d) return A_AND_B__IFF_C;
235  return 0;
236  default:
237  return 0;
238  }
239  }
240  case Relation::GEQ: {
241  switch (relA) {
242  case Relation::EQ: // p+c=0 and p+d>=0
243  if (c <= d) return A_IMPLIES_B;
244  return NOT__A_AND_B;
245  case Relation::NEQ: // p+c!=0 and p+d>=0
246  if (c > d) return B_IMPLIES_A;
247  if (c == d) return A_AND_B__IFF_C;
248  return 0;
249  case Relation::LESS: // p+c<0 and p+d>=0
250  if (c > d) return NOT__A_AND_B;
251  if (c == d) return A_XOR_B;
252  return 0;
253  case Relation::GREATER: // p+c>0 and p+d>=0
254  if (c < d) return B_IMPLIES_A;
255  return A_IMPLIES_B;
256  case Relation::LEQ: // p+c<=0 and p+d>=0
257  if (c > d) return NOT__A_AND_B;
258  if (c == d) return A_AND_B__IFF_C;
259  return 0;
260  case Relation::GEQ: // p+c>=0 and p+d>=0
261  if (c == d) return A_IFF_B;
262  if (c < d) return A_IMPLIES_B;
263  return B_IMPLIES_A;
264  default:
265  return 0;
266  }
267  }
268  default:
269  return 0;
270  }
271 }
272 
273 }
Pol
MultivariatePolynomial< Rational > Pol
Definition: HornerTest.cpp:17
carl
carl is the main namespace for the library.
carl::A_AND_B__IFF_C
const signed A_AND_B__IFF_C
Definition: Comparison.h:11
carl::abs
Interval< Number > abs(const Interval< Number > &_in)
Method which returns the absolute value of the passed number.
Definition: Interval.h:1511
carl::B_IMPLIES_A
const signed B_IMPLIES_A
Definition: Comparison.h:9
carl::compare
signed compare(const BasicConstraint< Pol > &_constraintA, const BasicConstraint< Pol > &_constraintB)
Compares _constraintA with _constraintB.
Definition: Comparison.h:25
carl::A_XOR_B
const signed A_XOR_B
Definition: Comparison.h:12
carl::get_num
cln::cl_I get_num(const cln::cl_RA &n)
Extract the numerator from a fraction.
Definition: operations.h:60
carl::A_IFF_B
const signed A_IFF_B
Definition: Comparison.h:7
carl::get_denom
cln::cl_I get_denom(const cln::cl_RA &n)
Extract the denominator from a fraction.
Definition: operations.h:69
carl::GREATER
@ GREATER
Definition: SignCondition.h:15
carl::A_IMPLIES_B
const signed A_IMPLIES_B
Definition: Comparison.h:8
carl::Relation
Relation
Definition: Relation.h:20
carl::NOT__A_AND_B
const signed NOT__A_AND_B
Definition: Comparison.h:10
carl::is_one
bool is_one(const Interval< Number > &i)
Check if this interval is a point-interval containing 1.
Definition: Interval.h:1462
carl::statistics::get
auto & get(const std::string &name)
Definition: StatisticsCollector.h:33
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