carl  24.04
Computer ARithmetic Library
ConstraintBounds.h
Go to the documentation of this file.
1 #pragma once
2 
3 namespace carl {
4 
5 /// A map from formula pointers to a map of rationals to a pair of a constraint relation and a formula pointer. (internally used)
6 template<typename Pol>
7 using ConstraintBounds = FastMap<Pol, std::map<typename Pol::NumberType, std::pair<Relation,Formula<Pol>>>> ;
8 
9 // #define CONSTRAINT_BOUND_DEBUG
10 
11 /**
12  * Adds the bound to the bounds of the polynomial specified by this constraint. E.g., if the constraint is p+b~0, where p is a sum
13  * of terms, being a rational (actually integer) coefficient times a non-trivial (!=1) monomial( product of variables to the power
14  * of an exponent), b is a rational and ~ is any constraint relation. Furthermore, the leading coefficient of p is 1. Then we add
15  * the bound -b to the bounds of p (means that p ~ -b) stored in the given constraint bounds.
16  * @param _constraintBounds An object collecting bounds of polynomials.
17  * @param _constraint The constraint to find a bound for a polynomial for.
18  * @param _inConjunction true, if the constraint is part of a conjunction.
19  * false, if the constraint is part of a disjunction.
20  * @return Formula<Pol>( FALSE ), if the yet determined bounds imply that the conjunction (_inConjunction == true) or disjunction
21  * (_inConjunction == false) of which we got the given constraint is invalid resp. valid;
22  * false, the added constraint.
23  */
24 template<typename Pol>
25 Formula<Pol> addConstraintBound( ConstraintBounds<Pol>& _constraintBounds, const Formula<Pol>& _constraint, bool _inConjunction )
26 {
27  #ifdef CONSTRAINT_BOUND_DEBUG
28  std::cout << "add from a " << (_inConjunction ? "conjunction" : "disjunction") << " to " << &_constraintBounds << ": " << _constraint << std::endl;
29  #endif
30  bool negated = _constraint.type() == FormulaType::NOT;
31  assert( _constraint.type() == FormulaType::CONSTRAINT || (negated && _constraint.subformula().type() == FormulaType::CONSTRAINT ) );
32  const Constraint<Pol>& constraint = negated ? _constraint.subformula().constraint() : _constraint.constraint();
33  assert( constraint.is_consistent() == 2 );
34  typename Pol::NumberType boundValue;
35  Relation relation = negated ? carl::inverse( constraint.relation() ) : constraint.relation();
36  const Pol& lhs = constraint.lhs();
37  Pol poly;
38  bool multipliedByMinusOne = lhs.lterm().coeff() < typename Pol::NumberType( 0 );
39  if( multipliedByMinusOne )
40  {
41  boundValue = constraint.lhs().constant_part();
42  relation = carl::turn_around( relation );
43  poly = Pol( -lhs + boundValue );
44  }
45  else
46  {
47  boundValue = -constraint.lhs().constant_part();
48  poly = Pol( lhs + boundValue );
49  }
50  typename Pol::NumberType cf( poly.coprime_factor() );
51  assert( cf > 0 );
52  boundValue *= cf;
53  poly *= cf;
54  #ifdef CONSTRAINT_BOUND_DEBUG
55  std::cout << "try to add the bound " << relation << boundValue << " for the polynomial " << poly << std::endl;
56  #endif
57  auto resA = _constraintBounds.insert( std::make_pair( std::move(poly), std::move( std::map<typename Pol::NumberType, std::pair<Relation, Formula<Pol>>>() ) ) );
58  auto resB = resA.first->second.insert( std::make_pair( boundValue, std::make_pair( relation, _constraint ) ) );
59  if( resB.second || resB.first->second.first == relation )
60  return resB.first->second.second;
61  switch( relation )
62  {
63  case Relation::EQ:
64  if( _inConjunction )
65  {
66  if( resB.first->second.first == Relation::LEQ || resB.first->second.first == Relation::GEQ )
67  {
68  resB.first->second.first = Relation::EQ;
69  resB.first->second.second = _constraint;
70  return resB.first->second.second;
71  }
72  else
73  return Formula<Pol>( FormulaType::FALSE );
74  }
75  else
76  {
77  switch( resB.first->second.first )
78  {
79  case Relation::LEQ:
80  return resB.first->second.second;
81  case Relation::GEQ:
82  return resB.first->second.second;
83  case Relation::LESS:
84  resB.first->second.first = Relation::LEQ;
85  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::GEQ : Relation::LEQ );
86  return resB.first->second.second;
87  case Relation::GREATER:
88  resB.first->second.first = Relation::GEQ;
89  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::LEQ : Relation::GEQ );
90  return resB.first->second.second;
91  default:
92  assert( resB.first->second.first == Relation::NEQ );
93  return Formula<Pol>( FormulaType::FALSE );
94  }
95  }
96  case Relation::LEQ:
97  if( _inConjunction )
98  {
99  switch( resB.first->second.first )
100  {
101  case Relation::EQ:
102  return resB.first->second.second;
103  case Relation::GEQ:
104  resB.first->second.first = Relation::EQ;
105  resB.first->second.second = Formula<Pol>( lhs, Relation::EQ );
106  return resB.first->second.second;
107  case Relation::LESS:
108  return resB.first->second.second;
109  case Relation::GREATER:
110  return Formula<Pol>( FormulaType::FALSE );
111  default:
112  assert( resB.first->second.first == Relation::NEQ );
113  resB.first->second.first = Relation::LESS;
114  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::GREATER : Relation::LESS );
115  return resB.first->second.second;
116  }
117  }
118  else
119  {
120  switch( resB.first->second.first )
121  {
122  case Relation::EQ:
123  resB.first->second.first = Relation::LEQ;
124  resB.first->second.second = _constraint;
125  return resB.first->second.second;
126  case Relation::GEQ:
127  return Formula<Pol>( FormulaType::FALSE );
128  case Relation::LESS:
129  resB.first->second.first = Relation::LEQ;
130  resB.first->second.second = _constraint;
131  return resB.first->second.second;
132  case Relation::GREATER:
133  return Formula<Pol>( FormulaType::FALSE );
134  default:
135  assert( resB.first->second.first == Relation::NEQ );
136  return Formula<Pol>( FormulaType::FALSE );
137  }
138  }
139  case Relation::GEQ:
140  if( _inConjunction )
141  {
142  switch( resB.first->second.first )
143  {
144  case Relation::EQ:
145  return resB.first->second.second;
146  case Relation::LEQ:
147  resB.first->second.first = Relation::EQ;
148  resB.first->second.second = Formula<Pol>( lhs, Relation::EQ );
149  return resB.first->second.second;
150  case Relation::LESS:
151  return Formula<Pol>( FormulaType::FALSE );
152  case Relation::GREATER:
153  return resB.first->second.second;
154  default:
155  assert( resB.first->second.first == Relation::NEQ );
156  resB.first->second.first = Relation::GREATER;
157  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::LESS : Relation::GREATER );
158  return resB.first->second.second;
159  }
160  }
161  else
162  {
163  switch( resB.first->second.first )
164  {
165  case Relation::EQ:
166  resB.first->second.first = Relation::GEQ;
167  resB.first->second.second = _constraint;
168  return resB.first->second.second;
169  case Relation::LEQ:
170  return Formula<Pol>( FormulaType::FALSE );
171  case Relation::LESS:
172  return Formula<Pol>( FormulaType::FALSE );
173  case Relation::GREATER:
174  resB.first->second.first = Relation::GEQ;
175  resB.first->second.second = _constraint;
176  return Formula<Pol>( FormulaType::FALSE );
177  default:
178  assert( resB.first->second.first == Relation::NEQ );
179  return Formula<Pol>( FormulaType::FALSE );
180  }
181  }
182  case Relation::LESS:
183  if( _inConjunction )
184  {
185  switch( resB.first->second.first )
186  {
187  case Relation::EQ:
188  return Formula<Pol>( FormulaType::FALSE );
189  case Relation::LEQ:
190  resB.first->second.first = Relation::LESS;
191  resB.first->second.second = _constraint;
192  return resB.first->second.second;
193  case Relation::GEQ:
194  return Formula<Pol>( FormulaType::FALSE );
195  case Relation::GREATER:
196  return Formula<Pol>( FormulaType::FALSE );
197  default:
198  assert( resB.first->second.first == Relation::NEQ );
199  resB.first->second.first = Relation::LESS;
200  resB.first->second.second = _constraint;
201  return resB.first->second.second;
202  }
203  }
204  else
205  {
206  switch( resB.first->second.first )
207  {
208  case Relation::EQ:
209  resB.first->second.first = Relation::LEQ;
210  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::GEQ : Relation::LEQ );
211  return resB.first->second.second;
212  case Relation::LEQ:
213  return resB.first->second.second;
214  case Relation::GEQ:
215  return Formula<Pol>( FormulaType::FALSE );
216  case Relation::GREATER:
217  resB.first->second.first = Relation::NEQ;
218  resB.first->second.second = Formula<Pol>( lhs, Relation::NEQ );
219  return resB.first->second.second;
220  default:
221  assert( resB.first->second.first == Relation::NEQ );
222  return resB.first->second.second;
223  }
224  }
225  case Relation::GREATER:
226  if( _inConjunction )
227  {
228  switch( resB.first->second.first )
229  {
230  case Relation::EQ:
231  return Formula<Pol>( FormulaType::FALSE );
232  case Relation::LEQ:
233  return Formula<Pol>( FormulaType::FALSE );
234  case Relation::GEQ:
235  resB.first->second.first = Relation::GREATER;
236  resB.first->second.second = _constraint;
237  return resB.first->second.second;
238  case Relation::LESS:
239  return Formula<Pol>( FormulaType::FALSE );
240  default:
241  assert( resB.first->second.first == Relation::NEQ );
242  resB.first->second.first = Relation::GREATER;
243  resB.first->second.second = _constraint;
244  return resB.first->second.second;
245  }
246  }
247  else
248  {
249  switch( resB.first->second.first )
250  {
251  case Relation::EQ:
252  resB.first->second.first = Relation::GEQ;
253  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::LEQ : Relation::GEQ );
254  return resB.first->second.second;
255  case Relation::LEQ:
256  return Formula<Pol>( FormulaType::FALSE );
257  case Relation::GEQ:
258  return resB.first->second.second;
259  case Relation::LESS:
260  resB.first->second.first = Relation::NEQ;
261  resB.first->second.second = Formula<Pol>( lhs, Relation::NEQ );
262  return resB.first->second.second;
263  default:
264  assert( resB.first->second.first == Relation::NEQ );
265  return resB.first->second.second;
266  }
267  }
268  default:
269  assert( relation == Relation::NEQ );
270  if( _inConjunction )
271  {
272  switch( resB.first->second.first )
273  {
274  case Relation::EQ:
275  return Formula<Pol>( FormulaType::FALSE );
276  case Relation::LEQ:
277  resB.first->second.first = Relation::LESS;
278  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::GREATER : Relation::LESS );
279  return resB.first->second.second;
280  case Relation::GEQ:
281  resB.first->second.first = Relation::GREATER;
282  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::LESS : Relation::GREATER );
283  return resB.first->second.second;
284  case Relation::LESS:
285  resB.first->second.first = Relation::LESS;
286  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::GREATER : Relation::LESS );
287  return resB.first->second.second;
288  default:
289  assert( resB.first->second.first == Relation::GREATER );
290  resB.first->second.first = Relation::GREATER;
291  resB.first->second.second = Formula<Pol>( lhs, multipliedByMinusOne ? Relation::LESS : Relation::GREATER );
292  return resB.first->second.second;
293  }
294  }
295  else
296  {
297  switch( resB.first->second.first )
298  {
299  case Relation::EQ:
300  return Formula<Pol>( FormulaType::FALSE );
301  case Relation::LEQ:
302  return Formula<Pol>( FormulaType::FALSE );
303  case Relation::GEQ:
304  return Formula<Pol>( FormulaType::FALSE );
305  case Relation::LESS:
306  return resB.first->second.second;
307  default:
308  assert( resB.first->second.first == Relation::GREATER );
309  return resB.first->second.second;
310  }
311  }
312  }
313 }
314 
315 /**
316  * Stores for every polynomial for which we determined bounds for given constraints a minimal set of constraints
317  * representing these bounds into the given set of sub-formulas of a conjunction (_inConjunction == true) or disjunction
318  * (_inConjunction == false) to construct.
319  * @param _constraintBounds An object collecting bounds of polynomials.
320  * @param _intoAsts A set of sub-formulas of a conjunction (_inConjunction == true) or disjunction (_inConjunction == false) to construct.
321  * @param _inConjunction true, if constraints representing the polynomial's bounds are going to be part of a conjunction.
322  * false, if constraints representing the polynomial's bounds are going to be part of a disjunction.
323  * @return true, if the yet added bounds imply that the conjunction (_inConjunction == true) or disjunction
324  * (_inConjunction == false) to which the bounds are added is invalid resp. valid;
325  * false, otherwise.
326  */
327 template<typename Pol>
328 bool swapConstraintBounds( ConstraintBounds<Pol>& _constraintBounds, Formulas<Pol>& _intoFormulas, bool _inConjunction )
329 {
330  #ifdef CONSTRAINT_BOUND_DEBUG
331  std::cout << "swap from " << &_constraintBounds << " to a " << (_inConjunction ? "conjunction" : "disjunction") << std::endl;
332  #endif
333  while( !_constraintBounds.empty() )
334  {
335  #ifdef CONSTRAINT_BOUND_DEBUG
336  std::cout << "for the bounds of " << _constraintBounds.begin()->first << std::endl;
337  #endif
338  const std::map<typename Pol::NumberType, std::pair<Relation, Formula<Pol>>>& bounds = _constraintBounds.begin()->second;
339  assert( !bounds.empty() );
340  if( bounds.size() == 1 )
341  {
342  _intoFormulas.push_back( bounds.begin()->second.second );
343  #ifdef CONSTRAINT_BOUND_DEBUG
344  std::cout << " just add the only bound" << std::endl;
345  #endif
346  }
347  else
348  {
349  auto mostSignificantLowerBound = bounds.end();
350  auto mostSignificantUpperBound = bounds.end();
351  auto moreSignificantCase = bounds.end();
352  Formulas<Pol> lessSignificantCases;
353  auto iter = bounds.begin();
354  for( ; iter != bounds.end(); ++iter )
355  {
356  #ifdef CONSTRAINT_BOUND_DEBUG
357  std::cout << " bound is " << iter->second.first << iter->first << std::endl;
358  #endif
359  if( (_inConjunction && iter->second.first == Relation::NEQ)
360  || (!_inConjunction && iter->second.first == Relation::EQ) )
361  {
362  if( moreSignificantCase == bounds.end() )
363  {
364  if( (_inConjunction && mostSignificantUpperBound == bounds.end())
365  || (!_inConjunction && mostSignificantLowerBound == bounds.end()) )
366  {
367  if( (_inConjunction && mostSignificantLowerBound != bounds.end())
368  || (!_inConjunction && mostSignificantUpperBound != bounds.end()) )
369  {
370  #ifdef CONSTRAINT_BOUND_DEBUG
371  std::cout << " case: " << __LINE__ << std::endl;
372  #endif
373  _intoFormulas.push_back( iter->second.second );
374  }
375  else
376  {
377  #ifdef CONSTRAINT_BOUND_DEBUG
378  std::cout << " case: " << __LINE__ << std::endl;
379  #endif
380  lessSignificantCases.push_back( iter->second.second );
381  }
382  }
383  }
384  }
385  else if( (_inConjunction && (iter->second.first == Relation::GEQ || iter->second.first == Relation::GREATER)) // found a lower bound
386  || (!_inConjunction && (iter->second.first == Relation::LEQ || iter->second.first == Relation::LESS)) ) // found an upper bound
387  {
388  if( (_inConjunction && mostSignificantUpperBound != bounds.end()) // found already an upper bound -> conjunction is invalid!
389  || (!_inConjunction && mostSignificantLowerBound != bounds.end()) // found already a lower bound -> disjunction is valid!
390  || moreSignificantCase != bounds.end() )
391  {
392  #ifdef CONSTRAINT_BOUND_DEBUG
393  std::cout << " case: " << __LINE__ << std::endl;
394  #endif
395  break;
396  }
397  else
398  {
399  #ifdef CONSTRAINT_BOUND_DEBUG
400  std::cout << " case: " << __LINE__ << std::endl;
401  #endif
402  if( _inConjunction ) // update the strongest upper bound
403  mostSignificantLowerBound = iter;
404  else // update the weakest upper bound
405  mostSignificantUpperBound = iter;
406  lessSignificantCases.clear();
407  }
408  }
409  else if( (_inConjunction && iter->second.first == Relation::EQ)
410  || (!_inConjunction && iter->second.first == Relation::NEQ) )
411  {
412  // _inConjunction == true: found already another equality or an upper bound -> conjunction is invalid!
413  // _inConjunction == false: found already another bound with != as relation or a lower bound -> disjunction is valid!
414  if( moreSignificantCase != bounds.end() || (_inConjunction ? mostSignificantUpperBound : mostSignificantLowerBound) != bounds.end() )
415  {
416  #ifdef CONSTRAINT_BOUND_DEBUG
417  std::cout << " case: " << __LINE__ << std::endl;
418  #endif
419  break;
420  }
421  // _inConjunction == true: found first equality
422  // _inConjunction == false: found first bound with !=
423  else
424  {
425  #ifdef CONSTRAINT_BOUND_DEBUG
426  std::cout << " case: " << __LINE__ << std::endl;
427  #endif
428  moreSignificantCase = iter;
429  }
430  }
431  // _inConjunction == true: found an upper bound
432  // _inConjunction == false: found a lower bound
433  else
434  {
435  #ifdef CONSTRAINT_BOUND_DEBUG
436  std::cout << " case: " << __LINE__ << std::endl;
437  #endif
438  assert( !_inConjunction || iter->second.first == Relation::LEQ || iter->second.first == Relation::LESS );
439  assert( _inConjunction || iter->second.first == Relation::GEQ || iter->second.first == Relation::GREATER );
440  if( _inConjunction && mostSignificantUpperBound == bounds.end() ) // first upper bound found = strongest upper bound
441  {
442  #ifdef CONSTRAINT_BOUND_DEBUG
443  std::cout << " case: " << __LINE__ << std::endl;
444  #endif
445  mostSignificantUpperBound = iter;
446  }
447  else if( !_inConjunction && mostSignificantLowerBound == bounds.end() ) // first lower bound found = weakest lower bound
448  {
449  #ifdef CONSTRAINT_BOUND_DEBUG
450  std::cout << " case: " << __LINE__ << std::endl;
451  #endif
452  mostSignificantLowerBound = iter;
453  }
454  }
455  }
456  if( iter != bounds.end() )
457  break;
458  if( moreSignificantCase != bounds.end() )
459  {
460  _intoFormulas.push_back( moreSignificantCase->second.second );
461  }
462  else
463  {
464  #ifdef CONSTRAINT_BOUND_DEBUG
465  if( !(_inConjunction || mostSignificantUpperBound == bounds.end() || mostSignificantLowerBound == bounds.end()
466  || mostSignificantUpperBound->first > mostSignificantLowerBound->first)
467  || !( !_inConjunction || mostSignificantUpperBound == bounds.end() || mostSignificantLowerBound == bounds.end()
468  || mostSignificantLowerBound->first > mostSignificantUpperBound->first ) )
469  {
470  std::cout << "mostSignificantUpperBound: " << mostSignificantUpperBound->first << " [" << mostSignificantUpperBound->second.second << "]" << std::endl;
471  std::cout << "mostSignificantLowerBound: " << mostSignificantLowerBound->first << " [" << mostSignificantLowerBound->second.second << "]" << std::endl;
472  }
473  #endif
474  assert( !_inConjunction || mostSignificantUpperBound == bounds.end() || mostSignificantLowerBound == bounds.end()
475  || mostSignificantUpperBound->first > mostSignificantLowerBound->first );
476  assert( _inConjunction || mostSignificantUpperBound == bounds.end() || mostSignificantLowerBound == bounds.end()
477  || mostSignificantLowerBound->first > mostSignificantUpperBound->first );
478  if( mostSignificantUpperBound != bounds.end() )
479  _intoFormulas.push_back( mostSignificantUpperBound->second.second );
480  if( mostSignificantLowerBound != bounds.end() )
481  _intoFormulas.push_back( mostSignificantLowerBound->second.second );
482  _intoFormulas.insert(_intoFormulas.end(), lessSignificantCases.begin(), lessSignificantCases.end() );
483  }
484  }
485  _constraintBounds.erase( _constraintBounds.begin() );
486  }
487  if( _constraintBounds.empty() )
488  {
489  #ifdef CONSTRAINT_BOUND_DEBUG
490  std::cout << std::endl;
491  #endif
492  return false;
493  }
494  else
495  {
496  _constraintBounds.clear();
497  #ifdef CONSTRAINT_BOUND_DEBUG
498  std::cout << "is " << (_inConjunction ? "invalid" : "valid") << std::endl << std::endl;
499  #endif
500  return true;
501  }
502 }
503 
504 }
Pol
MultivariatePolynomial< Rational > Pol
Definition: HornerTest.cpp:17
carl
carl is the main namespace for the library.
carl::swapConstraintBounds
bool swapConstraintBounds(ConstraintBounds< Pol > &_constraintBounds, Formulas< Pol > &_intoFormulas, bool _inConjunction)
Stores for every polynomial for which we determined bounds for given constraints a minimal set of con...
Definition: ConstraintBounds.h:328
carl::CONSTRAINT
@ CONSTRAINT
Definition: FormulaContent.h:46
carl::addConstraintBound
Formula< Pol > addConstraintBound(ConstraintBounds< Pol > &_constraintBounds, const Formula< Pol > &_constraint, bool _inConjunction)
Adds the bound to the bounds of the polynomial specified by this constraint.
Definition: ConstraintBounds.h:25
carl::Formulas
std::vector< Formula< Poly > > Formulas
Definition: FormulaContent.h:18
carl::inverse
Relation inverse(Relation r)
Inverts the given relation symbol.
Definition: Relation.h:40
carl::ConstraintBounds
FastMap< Pol, std::map< typename Pol::NumberType, std::pair< Relation, Formula< Pol > >> > ConstraintBounds
A map from formula pointers to a map of rationals to a pair of a constraint relation and a formula po...
Definition: ConstraintBounds.h:7
carl::turn_around
Relation turn_around(Relation r)
Turns around the given relation symbol, in the sense that LESS (LEQ) and GREATER (GEQ) are swapped.
Definition: Relation.h:58
carl::GREATER
@ GREATER
Definition: SignCondition.h:15
carl::Relation
Relation
Definition: Relation.h:20
carl::FastMap
std::unordered_map< T1, T2, std::hash< T1 > > FastMap
Definition: container_types.h:67
carl::Constraint
Represent a polynomial (in)equality against zero.
Definition: Constraint.h:62
carl::Constraint::is_consistent
unsigned is_consistent() const
Checks, whether the constraint is consistent.
Definition: Constraint.h:194
carl::Constraint::relation
Relation relation() const
Definition: Constraint.h:116
carl::Constraint::lhs
const Pol & lhs() const
Definition: Constraint.h:109
carl::Formula
Represent an SMT formula, which can be an atom for some background theory or a boolean combination of...
Definition: Formula.h:47
carl::Formula::subformula
const Formula & subformula() const
Definition: Formula.h:327
carl::Formula::constraint
const Constraint< Pol > & constraint() const
Definition: Formula.h:410
carl::Formula::type
FormulaType type() const
Definition: Formula.h:254