SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
VariableBounds.tpp
Go to the documentation of this file.
1 /**
2  * @file VariableBounds.h
3  * @author Florian Corzilius
4  * @since 2012-10-04
5  * @version 2013-02-05
6  */
7 
8 namespace smtrat
9 {
10  namespace vb
11  {
12  template<typename T>
13  Bound<T>::Bound( Rational* const _limit, Variable<T>* const _variable, Type _type ):
14  mType( _type ),
15  mpLimit( _limit ),
16  mpVariable( _variable ),
17  mpOrigins( new std::set<T,carl::less<T,false>>() )
18  {
19  if( _limit == NULL )
20  mpOrigins->insert( T() );
21  }
22 
23  template<typename T>
24  Bound<T>::~Bound()
25  {
26  delete mpOrigins;
27  delete mpLimit;
28  }
29 
30 
31  template<typename T>
32  bool Bound<T>::operator<( const Bound<T>& _bound ) const
33  {
34  if( isUpperBound() && _bound.isUpperBound() )
35  {
36  if( isInfinite() )
37  return false;
38  else
39  {
40  if( _bound.isInfinite() )
41  return true;
42  else
43  {
44  if( *mpLimit < _bound.limit() )
45  return true;
46  else if( *mpLimit == _bound.limit() )
47  {
48  if( mType == STRICT_UPPER_BOUND )
49  return (_bound.type() != STRICT_UPPER_BOUND);
50  else if( mType == EQUAL_BOUND )
51  return (_bound.type() == WEAK_UPPER_BOUND);
52  }
53  return false;
54  }
55  }
56  }
57  else
58  {
59  assert( isLowerBound() && _bound.isLowerBound() );
60  if( _bound.isInfinite() )
61  return false;
62  else
63  {
64  if( isInfinite() )
65  return true;
66  else
67  {
68  if( *mpLimit < _bound.limit() )
69  return true;
70  else if( *mpLimit == _bound.limit() )
71  {
72  if( mType == WEAK_LOWER_BOUND )
73  return (_bound.type() != WEAK_LOWER_BOUND);
74  else if( mType == EQUAL_BOUND )
75  return (_bound.type() == STRICT_LOWER_BOUND);
76  }
77  return false;
78  }
79  }
80  }
81  }
82 
83 
84  template<typename T>
85  std::ostream& operator<<( std::ostream& _out, const Bound<T>& _bound )
86  {
87  if( _bound.isInfinite() )
88  {
89  if( _bound.type() == Bound<T>::STRICT_LOWER_BOUND )
90  _out << "-inf";
91  else
92  _out << "inf";
93  }
94  else
95  _out << _bound.limit();
96  return _out;
97  }
98 
99 
100  template<typename T>
101  void Bound<T>::print( std::ostream& _out, bool _withRelation ) const
102  {
103  if( _withRelation )
104  {
105  switch( mType )
106  {
107  case STRICT_LOWER_BOUND:
108  _out << ">";
109  break;
110  case WEAK_LOWER_BOUND:
111  _out << ">=";
112  break;
113  case EQUAL_BOUND:
114  _out << "=";
115  break;
116  case WEAK_UPPER_BOUND:
117  _out << "<=";
118  break;
119  case STRICT_UPPER_BOUND:
120  _out << "<";
121  break;
122  default:
123  assert( false );
124  _out << "~";
125  break;
126  }
127  }
128  _out << *this;
129  }
130 
131 
132  template<typename T>
133  Variable<T>::Variable():
134  mUpdatedExactInterval( true ),
135  mUpdatedDoubleInterval( true ),
136  mUpperbounds( Variable<T>::BoundSet() ),
137  mLowerbounds( Variable<T>::BoundSet() )
138  {
139  mUpperbounds.insert( new Bound<T>( nullptr, this, Bound<T>::STRICT_UPPER_BOUND ) );
140  mpSupremum = *mUpperbounds.begin();
141  mLowerbounds.insert( new Bound<T>( nullptr, this, Bound<T>::STRICT_LOWER_BOUND ) );
142  mpInfimum = *mLowerbounds.begin();
143  }
144 
145 
146  template<typename T>
147  Variable<T>::~Variable()
148  {
149  while( !mLowerbounds.empty() )
150  {
151  const Bound<T>* toDelete = *mLowerbounds.begin();
152  mLowerbounds.erase( mLowerbounds.begin() );
153  if( toDelete->type() != Bound<T>::EQUAL_BOUND )
154  delete toDelete;
155  }
156  while( !mUpperbounds.empty() )
157  {
158  const Bound<T>* toDelete = *mUpperbounds.begin();
159  mUpperbounds.erase( mUpperbounds.begin() );
160  delete toDelete;
161  }
162  }
163 
164 
165  template<typename T>
166  bool Variable<T>::conflicting() const
167  {
168  if( mpSupremum->isInfinite() || mpInfimum->isInfinite() )
169  return false;
170  else
171  {
172  if( mpSupremum->limit() < mpInfimum->limit() )
173  return true;
174  else if( mpInfimum->limit() == mpSupremum->limit() )
175  return ( mpInfimum->type() == Bound<T>::STRICT_LOWER_BOUND || mpSupremum->type() == Bound<T>::STRICT_UPPER_BOUND );
176  return false;
177  }
178  }
179 
180 
181  template<typename T>
182  const Bound<T>* Variable<T>::addBound( const ConstraintT& _constraint, const carl::Variable& _var, const T& _origin )
183  {
184  assert( _constraint.variables().size() == 1 );
185  if( _constraint.maxDegree( _var ) == 1 )
186  {
187  const Rational coeff = _constraint.lhs().lterm().coeff();
188  carl::Relation rel = _constraint.relation();
189  Rational* limit = new Rational( -_constraint.lhs().constant_part()/coeff );
190  std::pair< typename Variable<T>::BoundSet::iterator, bool> result;
191  if( rel == carl::Relation::EQ )
192  {
193  Bound<T>* newBound = new Bound<T>( limit, this, Bound<T>::EQUAL_BOUND );
194  result = mUpperbounds.insert( newBound );
195  if( !result.second )
196  delete newBound;
197  else
198  mLowerbounds.insert( newBound );
199  }
200  else if( ( rel == carl::Relation::GEQ && coeff < 0 ) || ( rel == carl::Relation::LEQ && coeff > 0 ) )
201  {
202  Bound<T>* newBound = new Bound<T>( limit, this, Bound<T>::WEAK_UPPER_BOUND );
203  result = mUpperbounds.insert( newBound );
204  if( !result.second )
205  delete newBound;
206  }
207  else if( ( rel == carl::Relation::LEQ && coeff < 0 ) || ( rel == carl::Relation::GEQ && coeff > 0 ) )
208  {
209  Bound<T>* newBound = new Bound<T>( limit, this, Bound<T>::WEAK_LOWER_BOUND );
210  result = mLowerbounds.insert( newBound );
211  if( !result.second )
212  delete newBound;
213  }
214  else if( ( rel == carl::Relation::GREATER && coeff < 0 ) || ( rel == carl::Relation::LESS && coeff > 0 ) )
215  {
216  Bound<T>* newBound = new Bound<T>( limit, this, Bound<T>::STRICT_UPPER_BOUND );
217  result = mUpperbounds.insert( newBound );
218  if( !result.second )
219  delete newBound;
220  }
221  else if( ( rel == carl::Relation::LESS && coeff < 0 ) || ( rel == carl::Relation::GREATER && coeff > 0 ) )
222  {
223  Bound<T>* newBound = new Bound<T>( limit, this, Bound<T>::STRICT_LOWER_BOUND );
224  result = mLowerbounds.insert( newBound );
225  if( !result.second )
226  delete newBound;
227  }
228  else
229  assert( false );
230  (*result.first)->activate( _origin );
231  return *result.first;
232  }
233 // else if( _constraint.lhs().nr_terms() == 1 || (_constraint.lhs().nr_terms() == 2 && _constraint.lhs().has_constant_term()) )
234 // {
235 // // TODO: Retrieve bounds from constraints of the form x^n+b~0
236 // }
237  assert( false );
238  return NULL;
239  }
240 
241 
242  template<typename T>
243  bool Variable<T>::updateBounds( const Bound<T>& _changedBound )
244  {
245  mUpdatedExactInterval = true;
246  mUpdatedDoubleInterval = true;
247  if( _changedBound.isUpperBound() )
248  {
249  // Update the supremum.
250  typename Variable<T>::BoundSet::iterator newBound = mUpperbounds.begin();
251  while( newBound != mUpperbounds.end() )
252  {
253  if( (*newBound)->isActive() )
254  {
255  mpSupremum = *newBound;
256  break;
257  }
258  ++newBound;
259  }
260  }
261  if( _changedBound.isLowerBound() )
262  {
263  // Update the infimum.
264  typename Variable<T>::BoundSet::reverse_iterator newBound = mLowerbounds.rbegin();
265  while( newBound != mLowerbounds.rend() )
266  {
267  if( (*newBound)->isActive() )
268  {
269  mpInfimum = *newBound;
270  break;
271  }
272  ++newBound;
273  }
274  }
275  return conflicting();
276  }
277 
278 
279  template<typename T>
280  VariableBounds<T>::VariableBounds():
281  mpConflictingVariable( NULL ),
282  mpVariableMap( new VariableMap() ),
283  mpConstraintBoundMap( new ConstraintBoundMap() ),
284  mEvalIntervalMap(),
285  mDoubleIntervalMap(),
286  mBoundDeductions()
287  {}
288 
289 
290  template<typename T>
291  VariableBounds<T>::~VariableBounds()
292  {
293  delete mpConstraintBoundMap;
294  while( !mpVariableMap->empty() )
295  {
296  Variable<T>* toDelete = mpVariableMap->begin()->second;
297  mpVariableMap->erase( mpVariableMap->begin() );
298  delete toDelete;
299  }
300  delete mpVariableMap;
301  }
302 
303  template<typename T>
304  void VariableBounds<T>::clear()
305  {
306  mpConflictingVariable = NULL;
307  mpConstraintBoundMap->clear();
308  while( !mpVariableMap->empty() )
309  {
310  Variable<T>* toDelete = mpVariableMap->begin()->second;
311  mpVariableMap->erase( mpVariableMap->begin() );
312  delete toDelete;
313  }
314  mBoundDeductions.clear();
315  mDoubleIntervalMap.clear();
316  mEvalIntervalMap.clear();
317  }
318 
319  template<typename T>
320  bool VariableBounds<T>::addBound( const ConstraintT& _constraint, const T& _origin )
321  {
322  if( _constraint.relation() != carl::Relation::NEQ )
323  {
324  auto vars = carl::variables(_constraint);
325  carl::Variable var = *vars.begin();
326  if( vars.size() == 1 && _constraint.maxDegree( var ) == 1 )
327  {
328  typename VariableBounds<T>::ConstraintBoundMap::iterator cbPair = mpConstraintBoundMap->find( _constraint );
329  if( cbPair != mpConstraintBoundMap->end() )
330  {
331  const Bound<T>& bound = *cbPair->second;
332  if( bound.activate( _origin ) )
333  {
334  if( bound.pVariable()->updateBounds( bound ) )
335  mpConflictingVariable = bound.pVariable();
336  }
337  }
338  else
339  {
340  Variable<T>* variable;
341  const Bound<T>* bound;
342  typename VariableBounds<T>::VariableMap::iterator evPair = mpVariableMap->find( var );
343  if( evPair != mpVariableMap->end() )
344  {
345  variable = evPair->second;
346  bound = variable->addBound( _constraint, evPair->first, _origin );
347  }
348  else
349  {
350  variable = new Variable<T>();
351  (*mpVariableMap)[var] = variable;
352  bound = variable->addBound( _constraint, var, _origin );
353  }
354  mpConstraintBoundMap->insert( std::pair< ConstraintT, const Bound<T>* >( _constraint, bound ) );
355  if( variable->updateBounds( *bound ) )
356  mpConflictingVariable = bound->pVariable();
357  }
358  return true;
359  }
360  else // No bound.
361  {
362  if( mNonBoundConstraints.insert( _constraint ).second )
363  {
364  for (auto sym: carl::variables(_constraint))
365  {
366  Variable<T>* variable = new Variable<T>();
367  if( !mpVariableMap->insert( std::pair< const carl::Variable, Variable<T>* >( sym, variable ) ).second )
368  delete variable;
369  }
370  }
371  }
372  }
373  else
374  {
375  for (auto sym: carl::variables(_constraint))
376  {
377  Variable<T>* variable = new Variable<T>();
378  if( !mpVariableMap->insert( std::pair< const carl::Variable, Variable<T>* >( sym, variable ) ).second )
379  delete variable;
380  }
381  }
382  return false;
383  }
384 
385  template<typename T>
386  bool VariableBounds<T>::addBound( const FormulaT& _formula, const T& _origin ) {
387  switch (_formula.type()) {
388  case carl::FormulaType::CONSTRAINT:
389  return addBound(_formula.constraint(), _origin);
390  case carl::FormulaType::NOT: {
391  if (_formula.subformula().type() == carl::FormulaType::CONSTRAINT) {
392  const ConstraintT& c = _formula.subformula().constraint();
393  return addBound(ConstraintT(c.lhs(), carl::inverse(c.relation())), _origin);
394  }
395  break;
396  }
397  case carl::FormulaType::AND: {
398  bool res = false;
399  for (const auto& f: _formula.subformulas()) {
400  res = res || addBound(f, _origin);
401  }
402  return res;
403  }
404  default: break;
405  }
406  return false;
407  }
408 
409  template<typename T>
410  unsigned VariableBounds<T>::removeBound( const ConstraintT& _constraint, const T& _origin )
411  {
412  if( _constraint.relation() != carl::Relation::NEQ )
413  {
414  auto vars = carl::variables(_constraint);
415  carl::Variable var = *vars.begin();
416  if( vars.size() == 1 && _constraint.maxDegree( var ) == 1 )
417  {
418  assert( mpConstraintBoundMap->find( _constraint ) != mpConstraintBoundMap->end() );
419  const Bound<T>& bound = *(*mpConstraintBoundMap)[_constraint];
420  if( bound.deactivate( _origin ) )
421  {
422  if( bound.pVariable()->updateBounds( bound ) )
423  mpConflictingVariable = bound.pVariable();
424  else
425  mpConflictingVariable = NULL;
426  return 2;
427  }
428  return 1;
429  }
430  else
431  {
432  mNonBoundConstraints.erase( _constraint );
433  }
434  }
435  return 0;
436  }
437 
438  template<typename T>
439  unsigned VariableBounds<T>::removeBound( const ConstraintT& _constraint, const T& _origin, carl::Variable*& _changedVariable )
440  {
441  if( _constraint.relation() != carl::Relation::NEQ )
442  {
443  auto vars = carl::variables(_constraint);
444  carl::Variable var = *vars.begin();
445  if( vars.size() == 1 && _constraint.maxDegree( var ) == 1 )
446  {
447  assert( mpConstraintBoundMap->find( _constraint ) != mpConstraintBoundMap->end() );
448  const Bound<T>& bound = *(*mpConstraintBoundMap)[_constraint];
449  if( bound.deactivate( _origin ) )
450  {
451  if( bound.pVariable()->updateBounds( bound ) )
452  mpConflictingVariable = bound.pVariable();
453  else
454  mpConflictingVariable = NULL;
455  _changedVariable = new carl::Variable( var );
456  return 2;
457  }
458  return 1;
459  }
460  else
461  {
462  mNonBoundConstraints.erase( _constraint );
463  }
464  }
465  return 0;
466  }
467 
468  template<typename T>
469  unsigned VariableBounds<T>::removeBound(const FormulaT& _formula, const T& _origin) {
470  switch (_formula.type()) {
471  case carl::FormulaType::CONSTRAINT:
472  return removeBound(_formula.constraint(), _origin);
473  case carl::FormulaType::NOT: {
474  if (_formula.subformula().type() == carl::FormulaType::CONSTRAINT) {
475  const ConstraintT& c = _formula.subformula().constraint();
476  return removeBound(ConstraintT(c.lhs(), carl::inverse(c.relation())), _origin);
477  }
478  break;
479  }
480  case carl::FormulaType::AND: {
481  unsigned res = 0;
482  for (const auto& f: _formula.subformulas()) {
483  res = std::max(res, removeBound(f, _origin));
484  }
485  return res;
486  }
487  default: break;
488  }
489  return 0;
490  }
491 
492  #define CONVERT_BOUND(type, namesp) (type != Bound<T>::WEAK_UPPER_BOUND && type != Bound<T>::WEAK_LOWER_BOUND && type != Bound<T>::EQUAL_BOUND ) ? namesp::STRICT : namesp::WEAK
493 
494  template<typename T>
495  const smtrat::EvalRationalIntervalMap& VariableBounds<T>::getEvalIntervalMap() const
496  {
497  assert( mpConflictingVariable == NULL );
498  for( auto varVarPair = mpVariableMap->begin(); varVarPair != mpVariableMap->end(); ++varVarPair )
499  {
500  Variable<T>& var = *varVarPair->second;
501  if( var.updatedExactInterval() )
502  {
503  carl::BoundType lowerBoundType;
504  Rational lowerBoundValue;
505  carl::BoundType upperBoundType;
506  Rational upperBoundValue;
507  if( var.infimum().isInfinite() )
508  {
509  lowerBoundType = carl::BoundType::INFTY;
510  lowerBoundValue = 0;
511  }
512  else
513  {
514  lowerBoundType = CONVERT_BOUND( var.infimum().type(), carl::BoundType );
515  lowerBoundValue = var.infimum().limit();
516  }
517  if( var.supremum().isInfinite() )
518  {
519  upperBoundType = carl::BoundType::INFTY;
520  upperBoundValue = 0;
521  }
522  else
523  {
524  upperBoundType = CONVERT_BOUND( var.supremum().type(), carl::BoundType );
525  upperBoundValue = var.supremum().limit();
526  }
527  mEvalIntervalMap[varVarPair->first] = RationalInterval( lowerBoundValue, lowerBoundType, upperBoundValue, upperBoundType );
528  var.exactIntervalHasBeenUpdated();
529  }
530  }
531  return mEvalIntervalMap;
532  }
533 
534 
535  template<typename T>
536  const RationalInterval& VariableBounds<T>::getInterval( const carl::Variable& _var ) const
537  {
538  assert( mpConflictingVariable == NULL );
539  typename VariableMap::iterator varVarPair = mpVariableMap->find( _var );
540  if( varVarPair == mpVariableMap->end() )
541  {
542  Variable<T>* var = new Variable<T>();
543  mpVariableMap->emplace( _var, var );
544  auto ret = mEvalIntervalMap.emplace( _var, RationalInterval::unbounded_interval() );
545  var->exactIntervalHasBeenUpdated();
546  mDoubleIntervalMap.emplace( _var, carl::Interval<double>::unbounded_interval() );
547  var->doubleIntervalHasBeenUpdated();
548  return ret.first->second;
549  }
550  else
551  {
552  Variable<T>& var = *varVarPair->second;
553  if( var.updatedExactInterval() )
554  {
555  carl::BoundType lowerBoundType;
556  Rational lowerBoundValue;
557  carl::BoundType upperBoundType;
558  Rational upperBoundValue;
559  if( var.infimum().isInfinite() )
560  {
561  lowerBoundType = carl::BoundType::INFTY;
562  lowerBoundValue = 0;
563  }
564  else
565  {
566  lowerBoundType = CONVERT_BOUND( var.infimum().type(), carl::BoundType );
567  lowerBoundValue = var.infimum().limit();
568  }
569  if( var.supremum().isInfinite() )
570  {
571  upperBoundType = carl::BoundType::INFTY;
572  upperBoundValue = 0;
573  }
574  else
575  {
576  upperBoundType = CONVERT_BOUND( var.supremum().type(), carl::BoundType );
577  upperBoundValue = var.supremum().limit();
578  }
579  mEvalIntervalMap[_var] = RationalInterval( lowerBoundValue, lowerBoundType, upperBoundValue, upperBoundType );
580  var.exactIntervalHasBeenUpdated();
581  }
582  }
583  return mEvalIntervalMap[_var];
584  }
585 
586  template<typename T>
587  RationalInterval VariableBounds<T>::getInterval( carl::Monomial::Arg _mon ) const
588  {
589  RationalInterval res(1);
590  for (const auto& vexp: *_mon) {
591  const RationalInterval& i = getInterval(vexp.first);
592  res *= carl::pow(i, vexp.second);
593  }
594  return res;
595  }
596 
597  template<typename T>
598  RationalInterval VariableBounds<T>::getInterval( const TermT& _term ) const
599  {
600  if (_term.is_constant()) return RationalInterval(_term.coeff());
601  return getInterval(_term.monomial()) * _term.coeff();
602  }
603 
604  template<typename T>
605  const smtrat::EvalDoubleIntervalMap& VariableBounds<T>::getIntervalMap() const
606  {
607  assert( mpConflictingVariable == NULL );
608  for( auto varVarPair = mpVariableMap->begin(); varVarPair != mpVariableMap->end(); ++varVarPair )
609  {
610  Variable<T>& var = *varVarPair->second;
611  if( var.updatedDoubleInterval() )
612  {
613  carl::BoundType lowerBoundType;
614  Rational lowerBoundValue;
615  carl::BoundType upperBoundType;
616  Rational upperBoundValue;
617  if( var.infimum().isInfinite() )
618  {
619  lowerBoundType = carl::BoundType::INFTY;
620  lowerBoundValue = 0;
621  }
622  else
623  {
624  lowerBoundType = CONVERT_BOUND( var.infimum().type(), carl::BoundType );
625  lowerBoundValue = var.infimum().limit();
626  }
627  if( var.supremum().isInfinite() )
628  {
629  upperBoundType = carl::BoundType::INFTY;
630  upperBoundValue = 0;
631  }
632  else
633  {
634  upperBoundType = CONVERT_BOUND( var.supremum().type(), carl::BoundType );
635  upperBoundValue = var.supremum().limit();
636  }
637  mDoubleIntervalMap[varVarPair->first] = carl::Interval<double>( lowerBoundValue, lowerBoundType, upperBoundValue, upperBoundType );
638  var.doubleIntervalHasBeenUpdated();
639  }
640  }
641  return mDoubleIntervalMap;
642  }
643 
644 
645  template<typename T>
646  const carl::Interval<double>& VariableBounds<T>::getDoubleInterval( const carl::Variable& _var ) const
647  {
648  assert( mpConflictingVariable == NULL );
649  typename VariableMap::iterator varVarPair = mpVariableMap->find( _var );
650 
651  if( varVarPair == mpVariableMap->end() )
652  {
653  Variable<T>* var = new Variable<T>();
654  mpVariableMap->emplace( _var, var );
655  mEvalIntervalMap.emplace( _var, RationalInterval::unbounded_interval() );
656  var->exactIntervalHasBeenUpdated();
657  auto ret = mDoubleIntervalMap.emplace( _var, carl::Interval<double>::unbounded_interval() );
658  var->doubleIntervalHasBeenUpdated();
659  return ret.first->second;
660  }
661  else
662  {
663  Variable<T>& var = *varVarPair->second;
664  if( var.updatedDoubleInterval() )
665  {
666  carl::BoundType lowerBoundType;
667  Rational lowerBoundValue;
668  carl::BoundType upperBoundType;
669  Rational upperBoundValue;
670  if( var.infimum().isInfinite() )
671  {
672  lowerBoundType = carl::BoundType::INFTY;
673  lowerBoundValue = 0;
674  }
675  else
676  {
677  lowerBoundType = CONVERT_BOUND( var.infimum().type(), carl::BoundType );
678  lowerBoundValue = var.infimum().limit();
679  }
680  if( var.supremum().isInfinite() )
681  {
682  upperBoundType = carl::BoundType::INFTY;
683  upperBoundValue = 0;
684  }
685  else
686  {
687  upperBoundType = CONVERT_BOUND( var.supremum().type(), carl::BoundType );
688  upperBoundValue = var.supremum().limit();
689  }
690  mDoubleIntervalMap[_var] = carl::Interval<double>( lowerBoundValue, lowerBoundType, upperBoundValue, upperBoundType );
691  var.doubleIntervalHasBeenUpdated();
692  }
693  }
694  return mDoubleIntervalMap[_var];
695  }
696 
697  template<typename T>
698  std::vector<T> VariableBounds<T>::getOriginsOfBounds( const carl::Variable& _var ) const
699  {
700  std::vector<T> originsOfBounds;
701  auto varVarPair = mpVariableMap->find( _var );
702  if( varVarPair != mpVariableMap->end() )
703  {
704  if( !varVarPair->second->infimum().isInfinite() ) originsOfBounds.push_back( *varVarPair->second->infimum().origins().begin() );
705  if( !varVarPair->second->supremum().isInfinite() ) originsOfBounds.push_back( *varVarPair->second->supremum().origins().begin() );
706  }
707  return originsOfBounds;
708  }
709 
710  template<typename T>
711  std::vector<T> VariableBounds<T>::getOriginsOfBounds( const carl::Variables& _variables ) const
712  {
713  std::vector<T> originsOfBounds;
714  for( auto var = _variables.begin(); var != _variables.end(); ++var )
715  {
716  auto varVarPair = mpVariableMap->find( *var );
717  if( varVarPair != mpVariableMap->end() )
718  {
719  if( !varVarPair->second->infimum().isInfinite() ) originsOfBounds.push_back( *varVarPair->second->infimum().origins().begin() );
720  if( !varVarPair->second->supremum().isInfinite() ) originsOfBounds.push_back( *varVarPair->second->supremum().origins().begin() );
721  }
722  }
723  return originsOfBounds;
724  }
725 
726  template<typename T>
727  std::vector<T> VariableBounds<T>::getOriginsOfBounds() const
728  {
729  std::vector<T> originsOfBounds;
730  for( auto varVarPair = mpVariableMap->begin(); varVarPair != mpVariableMap->end(); ++varVarPair )
731  {
732  const Variable<T>& var = *varVarPair->second;
733  if( !var.infimum().isInfinite() ) originsOfBounds.push_back( *var.infimum().origins().begin() );
734  if( !var.supremum().isInfinite() ) originsOfBounds.push_back( *var.supremum().origins().begin() );
735  }
736  return originsOfBounds;
737  }
738 
739  template<typename T>
740  std::set<T> VariableBounds<T>::getOriginSetOfBounds() const
741  {
742  std::set<T> originsOfBounds;
743  for( auto varVarPair = mpVariableMap->begin(); varVarPair != mpVariableMap->end(); ++varVarPair )
744  {
745  const Variable<T>& var = *varVarPair->second;
746  if( !var.infimum().isInfinite() ) originsOfBounds.insert( *var.infimum().origins().begin() );
747  if( !var.supremum().isInfinite() ) originsOfBounds.insert( *var.supremum().origins().begin() );
748  }
749  return originsOfBounds;
750  }
751 
752  template<typename T>
753  std::set<T> VariableBounds<T>::getOriginSetOfBounds( const carl::Variable& _var ) const
754  {
755  std::set<T> originsOfBounds;
756  auto varVarPair = mpVariableMap->find( _var );
757  if( varVarPair != mpVariableMap->end() )
758  {
759  if( !varVarPair->second->infimum().isInfinite() ) originsOfBounds.insert( *varVarPair->second->infimum().origins().begin() );
760  if( !varVarPair->second->supremum().isInfinite() ) originsOfBounds.insert( *varVarPair->second->supremum().origins().begin() );
761  }
762  return originsOfBounds;
763  }
764 
765  template<typename T>
766  std::set<T> VariableBounds<T>::getOriginSetOfBounds( const carl::Variables& _variables ) const
767  {
768  std::set<T> originsOfBounds;
769  for( auto var = _variables.begin(); var != _variables.end(); ++var )
770  {
771  auto varVarPair = mpVariableMap->find( *var );
772  if( varVarPair != mpVariableMap->end() )
773  {
774  if( !varVarPair->second->infimum().isInfinite() ) originsOfBounds.insert( *varVarPair->second->infimum().origins().begin() );
775  if( !varVarPair->second->supremum().isInfinite() ) originsOfBounds.insert( *varVarPair->second->supremum().origins().begin() );
776  }
777  }
778  return originsOfBounds;
779  }
780 
781  template<typename T>
782  std::vector<std::pair<std::vector<ConstraintT>, ConstraintT>> VariableBounds<T>::getBoundDeductions() const
783  {
784  std::vector<std::pair<std::vector<ConstraintT>, ConstraintT>> result;;
785  for( auto cons = mNonBoundConstraints.begin(); cons != mNonBoundConstraints.end(); ++cons )
786  {
787  assert( cons->relation() != carl::Relation::NEQ );
788  std::vector<ConstraintT> boundConstraints;
789  carl::Variables boundedVars;
790  carl::Variables notBoundedVars;
791  for( auto carlVar: cons->variables() )
792  {
793  const Variable<T>& var = *(mpVariableMap->find( carlVar )->second);
794  if( !var.infimum().isInfinite() || !var.supremum().isInfinite() )
795  {
796  boundedVars.insert( carlVar );
797  if( !var.infimum().isInfinite() )
798  {
799  boundConstraints.push_back( (*var.infimum().origins().begin())->constraint() );
800  }
801  if( !var.supremum().isInfinite() )
802  {
803  boundConstraints.push_back( (*var.supremum().origins().begin())->constraint() );
804  }
805  }
806  else
807  {
808  notBoundedVars.insert( carlVar );
809  if( notBoundedVars.size() > 1 )
810  break;
811  }
812  }
813  if( boundedVars.size() == 0 || notBoundedVars.size() > 1 || cons->maxDegree( *notBoundedVars.begin() ) > 1 )
814  continue;
815  EvalRationalIntervalMap bounds = getEvalIntervalMap();
816  boundConstraints.push_back( *cons );
817  if( mBoundDeductions.find( boundConstraints ) == mBoundDeductions.end() )
818  {
819 // std::cout << std::endl << (*cons) << std::endl;
820 // std::cout << "find variable" << std::endl;
821  // Check whether all variables in the constraint but one are bounded (upper, lower or both)
822  if( notBoundedVars.size() == 1 )
823  {
824  carl::Variable var = *notBoundedVars.begin();
825 // std::cout << "var = " << var << std::endl;
826 // std::cout << "with the bounds: " << std::endl;
827 // for( auto bcons = boundConstraints.begin(); bcons != boundConstraints.end(); ++bcons )
828 // std::cout << (*bcons) << std::endl;
829  Poly varCoeff = cons->coefficient( var, 1 );
830  assert( !carl::is_zero(varCoeff) );
831  RationalInterval varCoeffEvaluated = carl::evaluate( varCoeff, bounds );
832  Poly remainder = carl::substitute(cons->lhs(), var, Poly(0) );
833  RationalInterval remainderEvaluated = carl::evaluate( remainder, bounds ).inverse();
834 
835  RationalInterval newBoundsA;
836  RationalInterval newBoundsB;
837  if( remainderEvaluated.div_ext( varCoeffEvaluated, newBoundsA, newBoundsB ) )
838  {
839 // std::cout << "case a: " << newBoundsA << " and " << newBoundsB << std::endl;
840  carl::BoundType lt = carl::BoundType::INFTY;
841  carl::BoundType rt = carl::BoundType::INFTY;
842  Rational lb;
843  Rational rb;
844  if( newBoundsA <= newBoundsB )
845  {
846  lt = newBoundsA.lower_bound_type();
847  rt = newBoundsB.upper_bound_type();
848  if( lt != carl::BoundType::INFTY ) lb = newBoundsA.lower();
849  if( rt != carl::BoundType::INFTY ) rb = newBoundsB.upper();
850  }
851  else
852  {
853  assert( newBoundsA >= newBoundsB );
854  lt = newBoundsB.lower_bound_type();
855  rt = newBoundsA.upper_bound_type();
856  if( lt != carl::BoundType::INFTY ) lb = newBoundsB.lower();
857  if( rt != carl::BoundType::INFTY ) rb = newBoundsA.upper();
858  }
859  if( cons->relation() == carl::Relation::EQ )
860  {
861  if( newBoundsA.lower_bound_type() != carl::BoundType::INFTY )
862  {
863  typename Poly::PolyType boundLhs = typename Poly::PolyType( var ) - newBoundsA.lower();
864  carl::Relation boundRel = newBoundsA.lower_bound_type() == carl::BoundType::STRICT ? carl::Relation::LEQ : carl::Relation::LESS;
865  ConstraintT newBoundConstraint = ConstraintT( boundLhs, boundRel );
866  result.push_back( std::pair<std::vector<ConstraintT>, ConstraintT >( boundConstraints, newBoundConstraint ) );
867  }
868  if( newBoundsB.upper_bound_type() != carl::BoundType::INFTY )
869  {
870  typename Poly::PolyType boundLhs = typename Poly::PolyType( var ) - newBoundsB.upper();
871  carl::Relation boundRel = newBoundsA.upper_bound_type() == carl::BoundType::STRICT ? carl::Relation::LEQ : carl::Relation::LESS;
872  ConstraintT newBoundConstraint = ConstraintT( boundLhs, boundRel );
873  result.push_back( std::pair<std::vector< ConstraintT >, ConstraintT >( boundConstraints, newBoundConstraint ) );
874  }
875  }
876  }
877  else
878  {
879  if( !varCoeffEvaluated.contains( Rational(0) ) || cons->relation() == carl::Relation::EQ )
880  {
881  carl::Relation rel = cons->relation();
882  if( varCoeffEvaluated.sgn() == carl::Sign::NEGATIVE )
883  {
884  switch( rel )
885  {
886  case carl::Relation::LEQ:
887  rel = carl::Relation::GEQ;
888  break;
889  case carl::Relation::GEQ:
890  rel = carl::Relation::LEQ;
891  break;
892  case carl::Relation::LESS:
893  rel = carl::Relation::GREATER;
894  break;
895  case carl::Relation::GREATER:
896  rel = carl::Relation::LESS;
897  break;
898  default:
899  break;
900  }
901  }
902  if( newBoundsA.lower_bound_type() != carl::BoundType::INFTY )
903  {
904  if( rel == carl::Relation::EQ || rel == carl::Relation::GEQ || rel == carl::Relation::GREATER )
905  {
906  typename Poly::PolyType boundLhs = typename Poly::PolyType( var ) - newBoundsA.lower();
907  carl::Relation boundRel = carl::Relation::GEQ;
908  if( newBoundsA.lower_bound_type() == carl::BoundType::STRICT || rel == carl::Relation::GREATER )
909  boundRel = carl::Relation::GREATER;
910  ConstraintT newBoundConstraint = ConstraintT( boundLhs, boundRel );
911  result.push_back( std::pair<std::vector< ConstraintT >, ConstraintT >( boundConstraints, newBoundConstraint ) );
912  }
913  }
914  if( newBoundsA.upper_bound_type() != carl::BoundType::INFTY )
915  {
916  if( rel == carl::Relation::EQ || rel == carl::Relation::LEQ || rel == carl::Relation::LESS )
917  {
918  typename Poly::PolyType boundLhs = typename Poly::PolyType( var ) - newBoundsA.upper();
919  carl::Relation boundRel = carl::Relation::LEQ;
920  if( newBoundsA.upper_bound_type() == carl::BoundType::STRICT || rel == carl::Relation::LESS )
921  boundRel = carl::Relation::LESS;
922  ConstraintT newBoundConstraint = ConstraintT( boundLhs, boundRel );
923  result.push_back( std::pair<std::vector< ConstraintT >, ConstraintT >( boundConstraints, newBoundConstraint ) );
924  }
925  }
926  }
927  }
928  }
929  mBoundDeductions.insert( boundConstraints );
930  }
931  boundConstraints.pop_back();
932  }
933  return result;
934  }
935 
936 
937  template<typename T>
938  void VariableBounds<T>::print( std::ostream& _out, const std::string _init, bool _printAllBounds ) const
939  {
940  for( auto varVarPair = mpVariableMap->begin(); varVarPair != mpVariableMap->end(); ++varVarPair )
941  {
942  _out << _init;
943  std::stringstream outA;
944  outA << varVarPair->first;
945  _out << std::setw( 15 ) << outA.str();
946  _out << " in ";
947  if( varVarPair->second->infimum().type() == Bound<T>::STRICT_LOWER_BOUND )
948  _out << "] ";
949  else
950  _out << "[ ";
951  std::stringstream outB;
952  outB << varVarPair->second->infimum();
953  _out << std::setw( 12 ) << outB.str();
954  _out << ", ";
955  std::stringstream outC;
956  outC << varVarPair->second->supremum();
957  _out << std::setw( 12 ) << outC.str();
958  if( varVarPair->second->supremum().type() == Bound<T>::STRICT_UPPER_BOUND )
959  _out << " [";
960  else
961  _out << " ]";
962  _out << std::endl;
963  if( _printAllBounds )
964  {
965  _out << _init << " Upper bounds:" << std::endl;
966  for( auto _uBound = varVarPair->second->upperbounds().begin(); _uBound != varVarPair->second->upperbounds().end(); ++_uBound )
967  {
968  _out << _init << " ";
969  (*_uBound)->print( _out, true );
970  _out << " {";
971  for( auto origin = (*_uBound)->origins().begin(); origin != (*_uBound)->origins().end(); ++origin )
972  _out << " " << *origin;
973  _out << " }" << std::endl;
974  }
975  _out << _init << " Lower bounds:" << std::endl;
976  for( auto _lBound = varVarPair->second->lowerbounds().rbegin(); _lBound != varVarPair->second->lowerbounds().rend(); ++_lBound )
977  {
978  _out << _init << " ";
979  (*_lBound)->print( _out, true );
980  _out << " {";
981  for( auto origin = (*_lBound)->origins().begin(); origin != (*_lBound)->origins().end(); ++origin )
982  _out << " " << *origin;
983  _out << " }" << std::endl;
984  }
985  }
986  }
987  }
988  } // namespace vb
989 } // namespace smtrat