SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
LRAModule.tpp
Go to the documentation of this file.
1 /**
2  * @file LRAModule.tpp
3  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
4  * @since 2012-04-05
5  * @version 2014-10-01
6  */
7 
8 #include "LRAModule.h"
9 
10 #include <smtrat-common/model.h>
11 #include <carl-formula/model/Assignment.h>
12 
13 #ifdef DEBUG_METHODS_TABLEAU
14 //#define DEBUG_METHODS_LRA_MODULE
15 #endif
16 //#define DEBUG_LRA_MODULE // this way no errors occur
17 
18 using namespace smtrat::lra;
19 
20 namespace smtrat
21 {
22  template<class Settings>
23  LRAModule<Settings>::LRAModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager ):
24  Module( _formula, _conditionals, _manager ),
25  mInitialized( false ),
26  mAssignmentFullfilsNonlinearConstraints( false ),
27  mOptimumComputed( false),
28  mRationalModelComputed( false ),
29  mCheckedWithBackends( false ),
30  mTableau( passedFormulaEnd() ),
31  mLinearConstraints(),
32  mNonlinearConstraints(),
33  mActiveResolvedNEQConstraints(),
34  mActiveUnresolvedNEQConstraints(),
35  mDelta( carl::fresh_real_variable( "delta_" + std::to_string( id() ) ) ),
36  mBoundCandidatesToPass(),
37  mRationalAssignment()
38  {}
39 
40  template<class Settings>
41  LRAModule<Settings>::~LRAModule()
42  {}
43 
44  template<class Settings>
45  bool LRAModule<Settings>::informCore( const FormulaT& _constraint )
46  {
47  #ifdef DEBUG_LRA_MODULE
48  std::cout << "LRAModule::inform " << "inform about " << _constraint << std::endl;
49  #endif
50  if( _constraint.type() == carl::FormulaType::CONSTRAINT )
51  {
52  const ConstraintT& constraint = _constraint.constraint();
53  if( !constraint.lhs().is_constant() && constraint.lhs().is_linear() )
54  {
55  mLinearConstraints.insert( _constraint );
56  setBound( _constraint );
57  }
58  return constraint.is_consistent() != 0;
59  }
60  return true;
61  }
62 
63  template<class Settings>
64  void LRAModule<Settings>::deinformCore( const FormulaT& _constraint )
65  {
66  #ifdef DEBUG_LRA_MODULE
67  std::cout << "LRAModule::deinform " << "deinform about " << _constraint << std::endl;
68  #endif
69  if( _constraint.constraint().lhs().is_linear() )
70  {
71  mLinearConstraints.erase( _constraint );
72  mTableau.removeBound( _constraint );
73  }
74  }
75 
76  template<class Settings>
77  bool LRAModule<Settings>::addCore( ModuleInput::const_iterator _subformula )
78  {
79  #ifdef DEBUG_LRA_MODULE
80  std::cout << "LRAModule::add " << _subformula->formula() << std::endl;
81  #endif
82  mOptimumComputed = false;
83  switch( _subformula->formula().type() )
84  {
85  case carl::FormulaType::FALSE:
86  {
87  FormulaSetT infSubSet;
88  infSubSet.insert( _subformula->formula() );
89  mInfeasibleSubsets.push_back( infSubSet );
90  #ifdef SMTRAT_DEVOPTION_Statistics
91  mStatistics.addConflict( mInfeasibleSubsets );
92  #endif
93  return false;
94  }
95  case carl::FormulaType::TRUE:
96  {
97  return true;
98  }
99  case carl::FormulaType::CONSTRAINT:
100  {
101  const FormulaT& formula = _subformula->formula();
102  const ConstraintT& constraint = formula.constraint();
103  #ifdef SMTRAT_DEVOPTION_Statistics
104  mStatistics.add( constraint );
105  #endif
106  // FormulaT constructor simplifies constraint if is_consistent() != 2
107  assert(constraint.is_consistent() == 2);
108  mAssignmentFullfilsNonlinearConstraints = false;
109  if( constraint.lhs().is_linear() )
110  {
111 // bool elementInserted = mLinearConstraints.insert( formula ).second;
112 // if( elementInserted && mInitialized )
113 // {
114 // mTableau.newBound( formula );
115 // }
116  if( constraint.relation() != carl::Relation::NEQ )
117  {
118  auto constrBoundIter = mTableau.constraintToBound().find( formula );
119  assert( constrBoundIter != mTableau.constraintToBound().end() );
120  const std::vector< const LRABound* >* bounds = constrBoundIter->second;
121  assert( bounds != NULL );
122  activateBound( *bounds->begin(), formula );
123 
124  if( !(*bounds->begin())->neqRepresentation().is_true() )
125  {
126  auto pos = mActiveUnresolvedNEQConstraints.find( (*bounds->begin())->neqRepresentation() );
127  if( pos != mActiveUnresolvedNEQConstraints.end() )
128  {
129  auto entry = mActiveResolvedNEQConstraints.insert( *pos );
130  removeOrigin( pos->second.position, pos->second.origin );
131  entry.first->second.position = passedFormulaEnd();
132  mActiveUnresolvedNEQConstraints.erase( pos );
133  auto constrBoundIter = mTableau.constraintToBound().find( (*bounds->begin())->neqRepresentation() );
134  assert( constrBoundIter != mTableau.constraintToBound().end() );
135  const std::vector< const LRABound* >* boundsOfNeqConstraint = constrBoundIter->second;
136  if( *bounds->begin() == (*boundsOfNeqConstraint)[1] || *bounds->begin() == (*boundsOfNeqConstraint)[2] )
137  {
138  bool leqBoundActive = *bounds->begin() == (*boundsOfNeqConstraint)[1];
139  activateStrictBound( (*bounds->begin())->neqRepresentation(), **bounds->begin(), (*boundsOfNeqConstraint)[leqBoundActive ? 0 : 3] );
140  }
141  }
142  }
143  return mInfeasibleSubsets.empty();
144  }
145  else
146  {
147  auto constrBoundIter = mTableau.constraintToBound().find( formula );
148  if (constrBoundIter == mTableau.constraintToBound().end()) {
149  std::quick_exit(57);
150  }
151  assert( constrBoundIter != mTableau.constraintToBound().end() );
152  const std::vector< const LRABound* >* bounds = constrBoundIter->second;
153 // bool intValued = constraint.integer_valued();
154 // if( (intValued && ((*bounds)[1]->isActive() || (*bounds)[2]->isActive()))
155 // || (!intValued && ((*bounds)[0]->isActive() || (*bounds)[1]->isActive() || (*bounds)[2]->isActive() || (*bounds)[3]->isActive())) )
156  if( (*bounds)[0]->isActive() || (*bounds)[1]->isActive() || (*bounds)[2]->isActive() || (*bounds)[3]->isActive() )
157  {
158  Context context( formula, passedFormulaEnd() );
159  mActiveResolvedNEQConstraints.insert( std::pair< FormulaT, Context >( formula, std::move(context) ) );
160  bool leqBoundActive = (*bounds)[1]->isActive();
161  if( leqBoundActive || (*bounds)[2]->isActive() )
162  {
163  activateStrictBound( formula, *(*bounds)[leqBoundActive ? 1 : 2], (*bounds)[leqBoundActive ? 0 : 3] );
164  }
165  }
166  else
167  {
168  Context context( formula, addSubformulaToPassedFormula( formula, formula ).first );
169  mActiveUnresolvedNEQConstraints.insert( std::pair< FormulaT, Context >( formula, std::move(context) ) );
170  }
171  }
172  return true;
173  }
174  else
175  {
176  addSubformulaToPassedFormula( formula, formula );
177  mNonlinearConstraints.insert( formula );
178  return true;
179  }
180  }
181  default:
182  return true;
183  }
184  return true;
185  }
186 
187  template<class Settings>
188  void LRAModule<Settings>::removeCore( ModuleInput::const_iterator _subformula )
189  {
190  #ifdef DEBUG_LRA_MODULE
191  std::cout << "LRAModule::remove " << _subformula->formula() << std::endl;
192  #endif
193  mOptimumComputed = false;
194  const FormulaT& formula = _subformula->formula();
195  if( formula.type() == carl::FormulaType::CONSTRAINT )
196  {
197  // Remove the mapping of the constraint to the sub-formula in the received formula
198  const ConstraintT& constraint = formula.constraint();
199  const FormulaT& pformula = _subformula->formula();
200  #ifdef SMTRAT_DEVOPTION_Statistics
201  mStatistics.remove( constraint );
202  #endif
203  // FormulaT constructor simplifies constraint if is_consistent() != 2
204  assert(constraint.is_consistent() == 2);
205  if( constraint.lhs().is_linear() )
206  {
207  // Deactivate the bounds regarding the given constraint
208  auto constrBoundIter = mTableau.constraintToBound().find( pformula );
209  assert( constrBoundIter != mTableau.rConstraintToBound().end() );
210  std::vector< const LRABound* >* bounds = constrBoundIter->second;
211  assert( bounds != NULL );
212  auto bound = bounds->begin();
213  int pos = 0;
214  int dontRemoveBeforePos = constraint.relation() == carl::Relation::NEQ ? 4 : 1;
215  while( bound != bounds->end() )
216  {
217  if( !(*bound)->origins().empty() )
218  {
219  auto origin = (*bound)->pOrigins()->begin();
220  bool mainOriginRemains = true;
221  while( origin != (*bound)->origins().end() )
222  {
223  if( origin->type() == carl::FormulaType::AND && origin->contains( pformula ) )
224  {
225  origin = (*bound)->pOrigins()->erase( origin );
226  }
227  else if( mainOriginRemains && *origin == pformula )
228  {
229  assert( origin->type() == carl::FormulaType::CONSTRAINT );
230  origin = (*bound)->pOrigins()->erase( origin );
231  // ensures that only one main origin is removed, in the case that a formula is contained more than once in the module input
232  mainOriginRemains = false;
233  }
234  else
235  {
236  ++origin;
237  }
238  }
239  if( (*bound)->origins().empty() )
240  {
241  if( !(*bound)->neqRepresentation().is_true() )
242  {
243  auto constrBoundIterB = mTableau.constraintToBound().find( (*bound)->neqRepresentation() );
244  assert( constrBoundIterB != mTableau.constraintToBound().end() );
245  const std::vector< const LRABound* >* uebounds = constrBoundIterB->second;
246  assert( uebounds != NULL );
247  assert( uebounds->size() >= 4 );
248 // bool intValued = (*bound)->neqRepresentation().constraint().integer_valued();
249 // if( (intValued && !(*uebounds)[1]->isActive() && !(*uebounds)[2]->isActive()) ||
250 // (!intValued && !(*uebounds)[0]->isActive() && !(*uebounds)[1]->isActive() && !(*uebounds)[2]->isActive() && !(*uebounds)[3]->isActive()) )
251  if( !(*uebounds)[0]->isActive() && !(*uebounds)[1]->isActive() && !(*uebounds)[2]->isActive() && !(*uebounds)[3]->isActive() )
252  {
253  auto pos = mActiveResolvedNEQConstraints.find( (*bound)->neqRepresentation() );
254  if( pos != mActiveResolvedNEQConstraints.end() )
255  {
256  auto entry = mActiveUnresolvedNEQConstraints.insert( *pos );
257  mActiveResolvedNEQConstraints.erase( pos );
258  entry.first->second.position = addSubformulaToPassedFormula( entry.first->first, entry.first->second.origin ).first;
259  }
260  }
261  }
262  LRAVariable& var = *(*bound)->pVariable();
263  if( var.deactivateBound( *bound, passedFormulaEnd() ) && !var.isBasic() )
264  {
265  if( var.supremum() < var.assignment() )
266  {
267  mTableau.updateBasicAssignments( var.position(), LRAValue( var.supremum().limit() - var.assignment() ) );
268  var.rAssignment() = var.supremum().limit();
269  }
270  else if( var.infimum() > var.assignment() )
271  {
272  mTableau.updateBasicAssignments( var.position(), LRAValue( var.infimum().limit() - var.assignment() ) );
273  var.rAssignment() = var.infimum().limit();
274  }
275  if( var.isConflicting() )
276  {
277  FormulaSetT infsubset;
278  collectOrigins( *var.supremum().origins().begin(), infsubset );
279  collectOrigins( *var.infimum().origins().begin(), infsubset );
280  mInfeasibleSubsets.push_back( std::move(infsubset) );
281  }
282  }
283  if( !(*bound)->pVariable()->pSupremum()->isInfinite() )
284  {
285  mBoundCandidatesToPass.push_back( (*bound)->pVariable()->pSupremum() );
286  }
287  if( !(*bound)->pVariable()->pInfimum()->isInfinite() )
288  {
289  mBoundCandidatesToPass.push_back( (*bound)->pVariable()->pInfimum() );
290  }
291 
292  if( !is_minimizing() && !(*bound)->variable().hasBound() && (*bound)->variable().isBasic() && !(*bound)->variable().isOriginal() )
293  {
294  mTableau.deactivateBasicVar( (*bound)->pVariable() );
295  }
296  }
297  }
298  if( (*bound)->origins().empty() && pos >= dontRemoveBeforePos )
299  bound = bounds->erase( bound );
300  else
301  {
302  ++bound;
303  ++pos;
304  }
305  }
306  if( constraint.relation() == carl::Relation::NEQ )
307  {
308  if( mActiveResolvedNEQConstraints.erase( pformula ) == 0 )
309  {
310  auto iter = mActiveUnresolvedNEQConstraints.find( pformula );
311  if( iter != mActiveUnresolvedNEQConstraints.end() )
312  {
313  removeOrigin( iter->second.position, iter->second.origin );
314  mActiveUnresolvedNEQConstraints.erase( iter );
315  }
316  }
317  }
318  }
319  else
320  {
321  mNonlinearConstraints.erase( pformula );
322  }
323  }
324  }
325 
326  template<class Settings>
327  Answer LRAModule<Settings>::checkCore()
328  {
329  #ifdef DEBUG_LRA_MODULE
330  std::cout << "LRAModule::check with is_minimizing() = " << is_minimizing() << std::endl;
331  for( const auto& f : rReceivedFormula() )
332  std::cout << f.formula() << std::endl;
333  #endif
334  bool containsIntegerValuedVariables = true;
335  if( !rReceivedFormula().is_constraint_conjunction() )
336  return processResult( UNKNOWN );
337  if( !mInfeasibleSubsets.empty() )
338  return processResult( UNSAT );
339  if( Settings::simple_theory_propagation )
340  simpleTheoryPropagation();
341  if( rReceivedFormula().is_real_constraint_conjunction() )
342  containsIntegerValuedVariables = false;
343 // if( mTableau.isConflicting() )
344 // exit(77);
345  assert( !mTableau.isConflicting() );
346 
347  mTableau.setBlandsRuleStart( 100 );//(unsigned) mTableau.columns().size() );
348  mTableau.compressRows();
349  mCheckedWithBackends = false;
350 
351  // Nonbasic vars satisfy bound
352 
353  // update and pivot
354  #ifdef DEBUG_LRA_MODULE
355  mTableau.print(); mTableau.printVariables(); std::cout << "True" << std::endl;
356  #endif
357  while(true){
358  #ifdef DEBUG_LRA_MODULE
359  mTableau.print();
360  #endif
361  // Check whether a module which has been called on the same instance in parallel, has found an answer.
362  if( anAnswerFound() )
363  return processResult( UNKNOWN );
364  // Find a pivoting element in the tableau.
365  if(Settings::use_SoI_simplex)
366  mTableau.setInfeasibilityRow();
367  std::pair<EntryID,bool> pivotingElement;
368  if(Settings::use_SoI_simplex)
369  pivotingElement = mTableau.nextPivotingElementInfeasibilities();
370  else
371  pivotingElement = mTableau.nextPivotingElement();
372  #ifdef DEBUG_LRA_MODULE
373  if( pivotingElement.second && pivotingElement.first != LAST_ENTRY_ID )
374  {
375  std::cout << std::endl; mTableau.print( pivotingElement.first, std::cout, " " ); std::cout << std::endl;
376  }
377  #endif
378  // If there is no conflict.
379  if(pivotingElement.second){
380  // If no basic variable violates its bounds (and hence no variable at all).
381  if( pivotingElement.first == lra::LAST_ENTRY_ID){
382  #ifdef DEBUG_LRA_MODULE
383  mTableau.print(); mTableau.printVariables(); std::cout << "True" << std::endl;
384  #endif
385  mTableau.storeAssignment();
386  mRationalModelComputed = false;
387  // If the current assignment also fulfills the nonlinear constraints.
388  if( checkAssignmentForNonlinearConstraint() )
389  {
390  if( containsIntegerValuedVariables )
391  {
392  if( branch_and_bound() ){
393  SMTRAT_LOG_DEBUG("smtrat", "Run in branch and bound");
394  return processResult( UNKNOWN );
395  }
396  }
397  return processResult( SAT );
398  }
399  // Otherwise, check the consistency of the formula consisting of the nonlinear constraints and the tightest bounds with the backends.
400  else
401  {
402  mCheckedWithBackends = true;
403  adaptPassedFormula();
404  Answer a = runBackends();
405  if( a == UNSAT ){
406  getInfeasibleSubsets();
407  }
408  return processResult( a );
409  }
410  }
411  else{
412  // Pivot at the found pivoting entry.
413  #ifdef DEBUG_LRA_MODULE
414  auto oldVioSum = mTableau.violationSum();
415  #endif
416  mTableau.pivot( pivotingElement.first );
417  // update infeasibility row
418  #ifdef SMTRAT_DEVOPTION_Statistics
419  mStatistics.pivotStep();
420  #endif
421  if( Settings::learn_refinements ) // Learn all bounds which have been deduced during the pivoting process.
422  processLearnedBounds();
423  // Maybe an easy conflict occurred with the learned bounds.
424  if( !mInfeasibleSubsets.empty() )
425  return processResult( UNSAT );
426  if(Settings::use_SoI_simplex){
427  #ifdef DEBUG_LRA_MODULE
428  auto newVioSum = mTableau.violationSum();
429  SMTRAT_LOG_DEBUG("smtrat", "newVioSum " << newVioSum << " oldVioSum " << oldVioSum << " dVio " << mTableau.get_dVioSum() );
430  if(!mTableau.usedBlandsRule()){
431  assert(newVioSum <= oldVioSum);
432  assert(newVioSum == oldVioSum + mTableau.get_dVioSum());
433  }
434  #endif
435  }
436  }
437  }
438  // There is a conflict, namely a basic variable violating its bounds without any suitable non-basic variable.
439  else
440  {
441  // Create the infeasible subsets.
442  createInfeasibleSubsets( pivotingElement.first );
443  return processResult( UNSAT );
444  }
445  }
446  assert( false );
447  return UNKNOWN;
448  }
449 
450  template<class Settings>
451  Answer LRAModule<Settings>::processResult( Answer _result )
452  {
453  if( _result == ABORTED )
454  {
455  return _result;
456  }
457  if( Settings::learn_refinements )
458  learnRefinements();
459  #ifdef SMTRAT_DEVOPTION_Statistics
460  if( _result != UNKNOWN )
461  {
462  mStatistics.check( rReceivedFormula() );
463  if( _result == UNSAT )
464  mStatistics.addConflict( mInfeasibleSubsets );
465  mStatistics.setNumberOfTableauxEntries( mTableau.size() );
466  mStatistics.setTableauSize( mTableau.rows().size()*mTableau.columns().size() );
467  }
468  #endif
469  if( is_minimizing() )
470  _result = optimize( _result );
471  if( _result != UNKNOWN )
472  {
473  mTableau.resetNumberOfPivotingSteps();
474  if( _result == SAT && !mCheckedWithBackends )
475  _result = checkNotEqualConstraints( _result );
476  }
477  #ifdef DEBUG_LRA_MODULE
478  std::cout << std::endl; mTableau.print(); std::cout << std::endl; std::cout << _result << std::endl;
479  #endif
480  return _result;
481  }
482 
483  template<class Settings>
484  void LRAModule<Settings>::updateModel() const
485  {
486  if( !mModelComputed && !mOptimumComputed )
487  {
488  clearModel();
489  assert( solverState() != UNSAT );
490  if( mAssignmentFullfilsNonlinearConstraints )
491  {
492  const RationalAssignment& rationalAssignment = getRationalModel();
493  for( auto ratAss = rationalAssignment.begin(); ratAss != rationalAssignment.end(); ++ratAss )
494  mModel.insert(mModel.end(), std::make_pair(ratAss->first, ratAss->second) );
495  }
496  else
497  Module::getBackendsModel();
498  mModelComputed = true;
499  }
500  }
501 
502  template<class Settings>
503  const RationalAssignment& LRAModule<Settings>::getRationalModel() const
504  {
505  if( !mRationalModelComputed )
506  {
507  mRationalAssignment = mTableau.getRationalAssignment();
508  mRationalModelComputed = true;
509  }
510  return mRationalAssignment;
511  }
512 
513  template<class Settings>
514  unsigned LRAModule<Settings>::currentlySatisfied( const FormulaT& _formula ) const
515  {
516  switch( _formula.type() )
517  {
518  case carl::FormulaType::TRUE:
519  return 1;
520  case carl::FormulaType::FALSE:
521  return 0;
522  case carl::FormulaType::CONSTRAINT:
523  {
524  if( mCheckedWithBackends )
525  {
526  auto res = satisfies( model(), _formula );
527  return res;
528  }
529  else
530  {
531  if( _formula.constraint().lhs().is_linear() && _formula.constraint().relation() != carl::Relation::NEQ )
532  {
533  auto constrBoundIter = mTableau.constraintToBound().find( _formula );
534  if( constrBoundIter != mTableau.constraintToBound().end() )
535  {
536  const LRABound& bound = *constrBoundIter->second->front();
537  const LRAVariable& lravar = bound.variable();
538  if( lravar.hasBound() || (lravar.isOriginal() && receivedVariable( lravar.expression().single_variable() )) )
539  {
540  const auto& cd = mTableau.currentDelta();
541  if( bound.isSatisfied( cd ) )
542  {
543  return 1;
544  }
545  else
546  {
547  return 0;
548  }
549  }
550  }
551  }
552  else
553  {
554  const auto& m = getRationalModel();
555  return carl::satisfied_by(_formula, Model(m)); // TODO: Isn't this an unnecessary copy operation, Gereon?
556  }
557  }
558  break;
559  }
560  default:
561  break;
562  }
563  return 2;
564  }
565 
566  template<class Settings>
567  Answer LRAModule<Settings>::optimize( Answer _result )
568  {
569  if( _result == SAT )
570  {
571  Poly objectivePoly(objective());
572  LRAVariable* optVar = mTableau.getObjectiveVariable( objectivePoly );
573  assert( optVar->isBasic() );
574  mTableau.activateBasicVar( optVar );
575  for( ; ; )
576  {
577  std::pair<EntryID,bool> pivotingElement = mTableau.nextPivotingElementForOptimizing( *optVar );
578  if( pivotingElement.second )
579  {
580  if( pivotingElement.first == lra::LAST_ENTRY_ID )
581  {
582  assert( optVar->infimum().isInfinite() );
583  #ifdef DEBUG_LRA_MODULE
584  std::cout << std::endl; mTableau.print(); std::cout << std::endl; std::cout << "Optimum: -oo" << std::endl;
585  #endif
586  clearModel();
587  mModel.insert(mModel.end(), std::make_pair(objective(), InfinityValue()) );
588  mOptimumComputed = true;
589  break;
590  }
591  else
592  {
593  #ifdef DEBUG_LRA_MODULE
594  std::cout << std::endl; mTableau.print( pivotingElement.first, std::cout, " " ); std::cout << std::endl;
595  #endif
596  mTableau.pivot( pivotingElement.first, true );
597  }
598  }
599  else
600  {
601  mModelComputed = false;
602  mOptimumComputed = false;
603  updateModel();
604  const RationalAssignment& ratModel = getRationalModel();
605  Rational opti = carl::evaluate(optVar->expression(), ratModel );
606  #ifdef DEBUG_LRA_MODULE
607  std::cout << std::endl; mTableau.print(); std::cout << std::endl; std::cout << "Optimum: " << opti << std::endl;
608  #endif
609  mModel.insert(mModel.end(), std::make_pair(objective(), opti ) );
610  mOptimumComputed = true;
611  break;
612  }
613  }
614  mTableau.deleteVariable( optVar, true );
615  return OPTIMAL;
616  }
617  // @todo Branch if assignment does not fulfill integer domains.
618  return _result;
619  }
620 
621  template<class Settings>
622  Answer LRAModule<Settings>::checkNotEqualConstraints( Answer _result )
623  {
624  // If there are unresolved notequal-constraints and the found satisfying assignment
625  // conflicts this constraint, resolve it by creating the lemma (p<0 or p>0) <-> p!=0 ) and return UNKNOWN.
626  const RationalAssignment& ass = getRationalModel();
627  for( auto iter = mActiveUnresolvedNEQConstraints.begin(); iter != mActiveUnresolvedNEQConstraints.end(); ++iter )
628  {
629  //unsigned consistency = iter->first.satisfiedBy( ass );
630  unsigned consistency = carl::satisfied_by(iter->first, Model(ass)); // TODO: Isn't this an unnecessary copy operation, Gereon?
631  assert( consistency != 2 );
632  if( consistency == 0 )
633  {
634  if( mFinalCheck )
635  {
636  #ifdef SMTRAT_DEVOPTION_Statistics
637  mStatistics.splitUnequalConstraint();
638  #endif
639  splitUnequalConstraint( iter->first );
640  }
641  return UNKNOWN;
642  }
643  }
644  // TODO: This is a rather unfortunate hack, because I couldn't fix the efficient neq-constraint-handling with integer-valued constraints
645  if(true || (_result != UNKNOWN && !rReceivedFormula().is_real_constraint_conjunction()) )
646  {
647  for( auto iter = mActiveResolvedNEQConstraints.begin(); iter != mActiveResolvedNEQConstraints.end(); ++iter )
648  {
649  //unsigned consistency = iter->first.satisfiedBy( ass );
650  unsigned consistency = carl::satisfied_by(iter->first, Model(ass));
651  assert( consistency != 2 );
652  if( consistency == 0 )
653  {
654  if( mFinalCheck )
655  {
656  #ifdef SMTRAT_DEVOPTION_Statistics
657  mStatistics.splitUnequalConstraint();
658  #endif
659  splitUnequalConstraint( iter->first );
660  }
661  return UNKNOWN;
662  }
663  }
664  }
665  assert( assignmentCorrect() );
666  return SAT;
667  }
668 
669  template<class Settings>
670  void LRAModule<Settings>::processLearnedBounds()
671  {
672  while( !mTableau.rNewLearnedBounds().empty() )
673  {
674  FormulasT originSet;
675  typename LRATableau::LearnedBound& learnedBound = mTableau.rNewLearnedBounds().back()->second;
676  mTableau.rNewLearnedBounds().pop_back();
677  std::vector<const LRABound*>& bounds = learnedBound.premise;
678  for( auto bound = bounds.begin(); bound != bounds.end(); ++bound )
679  {
680  const FormulaT& boundOrigins = *(*bound)->origins().begin();
681  if( boundOrigins.type() == carl::FormulaType::AND )
682  {
683  originSet.insert( originSet.end(), boundOrigins.subformulas().begin(), boundOrigins.subformulas().end() );
684  for( auto origin = boundOrigins.subformulas().begin(); origin != boundOrigins.subformulas().end(); ++origin )
685  {
686  auto constrBoundIter = mTableau.rConstraintToBound().find( *origin );
687  assert( constrBoundIter != mTableau.constraintToBound().end() );
688  std::vector< const LRABound* >* constraintToBounds = constrBoundIter->second;
689  constraintToBounds->push_back( *learnedBound.nextWeakerBound );
690  #ifdef LRA_INTRODUCE_NEW_CONSTRAINTS
691  if( learnedBound.newBound != NULL ) constraintToBounds->push_back( learnedBound.newBound );
692  #endif
693  }
694  }
695  else
696  {
697  assert( boundOrigins.type() == carl::FormulaType::CONSTRAINT );
698  originSet.push_back( boundOrigins );
699  auto constrBoundIter = mTableau.rConstraintToBound().find( boundOrigins );
700  assert( constrBoundIter != mTableau.constraintToBound().end() );
701  std::vector< const LRABound* >* constraintToBounds = constrBoundIter->second;
702  constraintToBounds->push_back( *learnedBound.nextWeakerBound );
703  #ifdef LRA_INTRODUCE_NEW_CONSTRAINTS
704  if( learnedBound.newBound != NULL ) constraintToBounds->push_back( learnedBound.newBound );
705  #endif
706  }
707  }
708  FormulaT origin = FormulaT( carl::FormulaType::AND, std::move(originSet) );
709  activateBound( *learnedBound.nextWeakerBound, origin );
710  #ifdef LRA_INTRODUCE_NEW_CONSTRAINTS
711  if( learnedBound.newBound != NULL )
712  {
713  const FormulaT& newConstraint = learnedBound.newBound->asConstraint();
714  addConstraintToInform( newConstraint );
715  mLinearConstraints.insert( newConstraint );
716  std::vector< const LRABound* >* boundVector = new std::vector< const LRABound* >();
717  boundVector->push_back( learnedBound.newBound );
718  mConstraintToBound[newConstraint] = boundVector;
719  activateBound( learnedBound.newBound, origin );
720  }
721  #endif
722  }
723  }
724 
725  template<class Settings>
726  void LRAModule<Settings>::createInfeasibleSubsets( EntryID _tableauEntry )
727  {
728  std::pair<EntryID,bool> conflictPair = mTableau.hasConflict();
729  if( Settings::one_conflict_reason )
730  {
731  std::vector< const LRABound* > conflict;
732 
733  if(!conflictPair.second){
734  SMTRAT_LOG_DEBUG("smtrat", "In simple creation");
735  conflict = mTableau.getConflict( _tableauEntry );
736  }
737  else{
738  SMTRAT_LOG_DEBUG("smtrat", "In multiline creation");
739  conflict = mTableau.getMultilineConflict();
740  }
741  FormulaSetT infSubSet;
742  for( auto bound = conflict.begin(); bound != conflict.end(); ++bound )
743  {
744  assert( (*bound)->isActive() );
745  collectOrigins( *(*bound)->origins().begin(), infSubSet );
746  }
747  mInfeasibleSubsets.push_back( infSubSet );
748  }
749  else
750  {
751  std::vector< std::vector< const LRABound* > > conflictingBounds;
752  if(!conflictPair.second){
753  SMTRAT_LOG_DEBUG("smtrat", "In simple creation");
754  conflictingBounds = mTableau.getConflictsFrom( _tableauEntry );
755  }
756  else{
757  SMTRAT_LOG_DEBUG("smtrat", "In multiline creation");
758  assert(mTableau.hasMultilineConflict());
759  std::vector< const LRABound* > conflict = mTableau.getMultilineConflict();
760  conflictingBounds.push_back(conflict);
761  }
762  for( auto conflict = conflictingBounds.begin(); conflict != conflictingBounds.end(); ++conflict )
763  {
764  FormulaSetT infSubSet;
765  for( auto bound = conflict->begin(); bound != conflict->end(); ++bound )
766  {
767  assert( (*bound)->isActive() );
768  SMTRAT_LOG_DEBUG("smtrat","collected for " << *(*bound)->origins().begin());
769  collectOrigins( *(*bound)->origins().begin(), infSubSet );
770  }
771  mInfeasibleSubsets.push_back( infSubSet );
772  }
773  assert(!mInfeasibleSubsets.empty());
774  }
775  }
776 
777  template<class Settings>
778  EvalRationalIntervalMap LRAModule<Settings>::getVariableBounds() const
779  {
780  EvalRationalIntervalMap result;
781  for( auto iter = mTableau.originalVars().begin(); iter != mTableau.originalVars().end(); ++iter )
782  {
783  const LRAVariable& var = *iter->second;
784  carl::BoundType lowerBoundType;
785  Rational lowerBoundValue;
786  carl::BoundType upperBoundType;
787  Rational upperBoundValue;
788  if( var.infimum().isInfinite() )
789  {
790  lowerBoundType = carl::BoundType::INFTY;
791  lowerBoundValue = 0;
792  }
793  else
794  {
795  lowerBoundType = var.infimum().isWeak() ? carl::BoundType::WEAK : carl::BoundType::STRICT;
796  lowerBoundValue = Rational(var.infimum().limit().mainPart());
797  }
798  if( var.supremum().isInfinite() )
799  {
800  upperBoundType = carl::BoundType::INFTY;
801  upperBoundValue = 0;
802  }
803  else
804  {
805  upperBoundType = var.supremum().isWeak() ? carl::BoundType::WEAK : carl::BoundType::STRICT;
806  upperBoundValue = Rational(var.supremum().limit().mainPart());
807  }
808  RationalInterval interval = RationalInterval( lowerBoundValue, lowerBoundType, upperBoundValue, upperBoundType );
809  result.insert( std::pair< carl::Variable, RationalInterval >( iter->first, interval ) );
810  }
811  return result;
812  }
813 
814  template<class Settings>
815  void LRAModule<Settings>::learnRefinements()
816  {
817  for( const auto& lbound : mTableau.rLearnedLowerBounds() )
818  learnRefinement( lbound.second, false );
819  mTableau.rLearnedLowerBounds().clear();
820  for( const auto& ubound : mTableau.rLearnedUpperBounds() )
821  learnRefinement( ubound.second, true );
822  mTableau.rLearnedUpperBounds().clear();
823  }
824 
825  template<class Settings>
826  void LRAModule<Settings>::learnRefinement( const typename LRATableau::LearnedBound& _learnedBound, bool _upperBound )
827  {
828  bool premiseOnlyEqualities = true;
829  FormulasT subformulas = createPremise( _learnedBound.premise, premiseOnlyEqualities );
830  auto boundIter = _learnedBound.nextWeakerBound;
831  if( _upperBound )
832  ++boundIter;
833  else
834  --boundIter;
835  while( !(*boundIter)->isActive() )
836  {
837  const LRABound& bound = **boundIter;
838  if( bound.exists() && !bound.isComplementActive() )
839  {
840  if( bound.type() != LRABound::Type::EQUAL )
841  {
842  mTheoryPropagations.emplace_back( std::move(FormulasT(subformulas)), bound.asConstraint() );
843  SMTRAT_LOG_DEBUG("smtrat", "theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
844  }
845  else if( premiseOnlyEqualities )
846  {
847  SMTRAT_LOG_DEBUG("smtrat", _learnedBound.newLimit << " == " << bound.limit() );
848  if( _learnedBound.newLimit == bound.limit() )
849  {
850  mTheoryPropagations.emplace_back( std::move(FormulasT(subformulas)), bound.asConstraint() );
851  SMTRAT_LOG_DEBUG("smtrat", "### theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
852  }
853  else
854  {
855  mTheoryPropagations.emplace_back( std::move(FormulasT(subformulas)), bound.asConstraint().negated() );
856  SMTRAT_LOG_DEBUG("smtrat", "### theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
857  }
858  }
859  }
860  if( _upperBound )
861  ++boundIter;
862  else
863  --boundIter;
864  }
865  const LRABound& nextWeakerBound = **_learnedBound.nextWeakerBound;
866  if( nextWeakerBound.exists() && !nextWeakerBound.isComplementActive() )
867  {
868  if( nextWeakerBound.type() != LRABound::Type::EQUAL )
869  {
870  mTheoryPropagations.emplace_back( std::move(subformulas), nextWeakerBound.asConstraint() );
871  SMTRAT_LOG_DEBUG("smtrat", "theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
872  }
873  else if( premiseOnlyEqualities )
874  {
875  if( _learnedBound.newLimit == nextWeakerBound.limit() )
876  {
877  mTheoryPropagations.emplace_back( std::move(FormulasT(subformulas)), nextWeakerBound.asConstraint() );
878  SMTRAT_LOG_DEBUG("smtrat", "### theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
879  }
880  else
881  {
882  mTheoryPropagations.emplace_back( std::move(FormulasT(subformulas)), nextWeakerBound.asConstraint().negated() );
883  SMTRAT_LOG_DEBUG("smtrat", "### theory propagation [" << (_upperBound ? "upper" : "lower") << "]: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion );
884  }
885  }
886  }
887  #ifdef SMTRAT_DEVOPTION_Statistics
888  mStatistics.addRefinement();
889  mStatistics.propagateTheory();
890  #endif
891  }
892 
893  template<class Settings>
894  FormulasT LRAModule<Settings>::createPremise( const std::vector< const LRABound*>& _premiseBounds, bool& _premiseOnlyEqualities ) const
895  {
896  FormulasT subformulas;
897  _premiseOnlyEqualities = true;
898  for( const LRABound* bound : _premiseBounds )
899  {
900  const FormulaT& origin = *bound->origins().begin();
901  if( origin.type() == carl::FormulaType::AND )
902  {
903  for( auto& subformula : origin.subformulas() )
904  {
905  assert( subformula.type() == carl::FormulaType::CONSTRAINT );
906  subformulas.push_back( subformula );
907  if( subformula.constraint().relation() != carl::Relation::EQ )
908  _premiseOnlyEqualities = false;
909  }
910  }
911  else
912  {
913  assert( origin.type() == carl::FormulaType::CONSTRAINT );
914  subformulas.push_back( origin );
915  if( origin.constraint().relation() != carl::Relation::EQ )
916  _premiseOnlyEqualities = false;
917  }
918  }
919  return subformulas;
920  }
921 
922  template<class Settings>
923  void LRAModule<Settings>::adaptPassedFormula()
924  {
925  for( const LRABound* bound : mBoundCandidatesToPass )
926  {
927  if( bound->pInfo()->updated > 0 )
928  {
929  bound->pInfo()->position = addSubformulaToPassedFormula( bound->asConstraint(), bound->pOrigins() ).first;
930  bound->pInfo()->updated = 0;
931  }
932  else if( bound->pInfo()->updated < 0 )
933  {
934  eraseSubformulaFromPassedFormula( bound->pInfo()->position, true );
935  bound->pInfo()->position = passedFormulaEnd();
936  bound->pInfo()->updated = 0;
937  }
938  }
939  mBoundCandidatesToPass.clear();
940  }
941 
942  template<class Settings>
943  bool LRAModule<Settings>::checkAssignmentForNonlinearConstraint()
944  {
945  if( mNonlinearConstraints.empty() )
946  {
947  mAssignmentFullfilsNonlinearConstraints = true;
948  return true;
949  }
950  else
951  {
952  auto assignments = Model(getRationalModel()); // TODO: Isn't this an unnecessary copy operation, Gereon?
953  // Check whether the assignment satisfies the non linear constraints.
954  for( const auto& constraint : mNonlinearConstraints )
955  {
956  if( carl::satisfied_by(constraint, assignments) != 1 )
957  {
958  return false;
959  }
960  }
961  mAssignmentFullfilsNonlinearConstraints = true;
962  return true;
963  }
964  }
965 
966  template<class Settings>
967  void LRAModule<Settings>::activateBound( const LRABound* _bound, const FormulaT& _formula )
968  {
969  // If the bounds constraint has already been passed to the backend, add the given formulas to it's origins
970  const LRAVariable& var = _bound->variable();
971  const LRABound* psup = var.pSupremum();
972  const LRABound& sup = *psup;
973  const LRABound* pinf = var.pInfimum();
974  const LRABound& inf = *pinf;
975  const LRABound& bound = *_bound;
976  mTableau.activateBound( _bound, _formula );
977  if( bound.isUpperBound() )
978  {
979  auto iter = var.lowerbounds().find( pinf );
980  while( /*(**iter).isActive() &&*/ (**iter) > bound.limit() )
981  {
982  if(!(*iter)->isActive())
983  {
984  --iter;
985  continue;
986  }
987  //FormulaSetT infsubset;
988  //collectOrigins( *bound.origins().begin(), infsubset );
989  //collectOrigins( *(**iter).pOrigins()->begin(), infsubset );
990  //mInfeasibleSubsets.push_back( std::move(infsubset) );
991  for(const auto& o1 : bound.origins())
992  {
993  FormulaSetT infsubset;
994  collectOrigins( o1, infsubset );
995  for (const auto& o2: (*iter)->origins()) {
996  FormulaSetT infsubsetForO1(infsubset);
997  collectOrigins( o2, infsubsetForO1 );
998  mInfeasibleSubsets.push_back( std::move(infsubsetForO1) );
999  }
1000  }
1001  assert( iter != var.lowerbounds().begin() );
1002  --iter;
1003  }
1004  if( sup > bound )
1005  {
1006  if( !sup.isInfinite() )
1007  mBoundCandidatesToPass.push_back( psup );
1008  mBoundCandidatesToPass.push_back( _bound );
1009  }
1010  }
1011  if( bound.isLowerBound() )
1012  {
1013  auto iter = var.upperbounds().find( psup );
1014  while( /*(**iter).isActive() &&*/ (**iter) < bound.limit() )
1015  {
1016  if (!(*iter)->isActive()) {
1017  ++iter;
1018  continue;
1019  }
1020  //FormulaSetT infsubset;
1021  //collectOrigins( *bound.origins().begin(), infsubset );
1022  //collectOrigins( *(**iter).pOrigins()->begin(), infsubset );
1023  //mInfeasibleSubsets.push_back( std::move(infsubset) );
1024  for (const auto& o1 : bound.origins()) {
1025  FormulaSetT infsubset;
1026  collectOrigins( o1, infsubset );
1027  for (const auto& o2: (*iter)->origins()) {
1028  FormulaSetT infsubsetForO1(infsubset);
1029  collectOrigins( o2, infsubsetForO1 );
1030  mInfeasibleSubsets.push_back( std::move(infsubsetForO1) );
1031  }
1032  }
1033  ++iter;
1034  assert( iter != var.upperbounds().end() );
1035  }
1036  if( inf < bound )
1037  {
1038  if( !inf.isInfinite() )
1039  mBoundCandidatesToPass.push_back( pinf );
1040  mBoundCandidatesToPass.push_back( _bound );
1041  }
1042  }
1043  assert( mInfeasibleSubsets.empty() || !mInfeasibleSubsets.begin()->empty() );
1044  #ifdef SMTRAT_DEVOPTION_Statistics
1045  if( !mInfeasibleSubsets.empty() )
1046  mStatistics.addConflict( mInfeasibleSubsets );
1047  #endif
1048  }
1049 
1050  template<class Settings>
1051  void LRAModule<Settings>::activateStrictBound( const FormulaT& _neqOrigin, const LRABound& _weakBound, const LRABound* _strictBound )
1052  {
1053  FormulaSetT involvedConstraints;
1054  FormulasT originSet;
1055  originSet.push_back( _neqOrigin );
1056  auto iter = _weakBound.origins().begin();
1057  assert( iter != _weakBound.origins().end() );
1058  if( iter->type() == carl::FormulaType::AND )
1059  {
1060  originSet.insert( originSet.end(), iter->subformulas().begin(), iter->subformulas().end() );
1061  involvedConstraints.insert( iter->subformulas().begin(), iter->subformulas().end() );
1062  }
1063  else
1064  {
1065  assert( iter->type() == carl::FormulaType::CONSTRAINT );
1066  originSet.push_back( *iter );
1067  involvedConstraints.insert( *iter );
1068  }
1069  FormulaT origin = FormulaT( carl::FormulaType::AND, std::move(originSet) );
1070  activateBound( _strictBound, origin );
1071  ++iter;
1072  while( iter != _weakBound.origins().end() )
1073  {
1074  FormulasT originSetB;
1075  originSetB.push_back( _neqOrigin );
1076  if( iter->type() == carl::FormulaType::AND )
1077  {
1078  originSetB.insert( originSetB.end(), iter->subformulas().begin(), iter->subformulas().end() );
1079  involvedConstraints.insert( iter->subformulas().begin(), iter->subformulas().end() );
1080  }
1081  else
1082  {
1083  assert( iter->type() == carl::FormulaType::CONSTRAINT );
1084  originSetB.push_back( *iter );
1085  involvedConstraints.insert( *iter );
1086  }
1087  FormulaT originB = FormulaT( carl::FormulaType::AND, std::move(originSet) );
1088  _strictBound->pOrigins()->push_back( originB );
1089  ++iter;
1090  }
1091  for( const FormulaT& fconstraint : involvedConstraints )
1092  {
1093  auto constrBoundIter = mTableau.rConstraintToBound().find( fconstraint );
1094  assert( constrBoundIter != mTableau.constraintToBound().end() );
1095  std::vector< const LRABound* >* constraintToBounds = constrBoundIter->second;
1096  constraintToBounds->push_back( _strictBound );
1097  }
1098  }
1099 
1100  template<class Settings>
1101  void LRAModule<Settings>::setBound( const FormulaT& _constraint )
1102  {
1103  mTableau.newBound( _constraint );
1104  }
1105 
1106  template<class Settings>
1107  void LRAModule<Settings>::simpleTheoryPropagation()
1108  {
1109  for( const LRAVariable* rowVar : mTableau.rows() )
1110  {
1111  if( rowVar != NULL )
1112  {
1113  if( !rowVar->infimum().isInfinite() )
1114  simpleTheoryPropagation( rowVar->pInfimum() );
1115  if( !rowVar->supremum().isInfinite() && rowVar->supremum().type() != LRABound::Type::EQUAL )
1116  simpleTheoryPropagation( rowVar->pSupremum() );
1117  }
1118  }
1119  for( const LRAVariable* columnVar : mTableau.columns() )
1120  {
1121  if( !columnVar->infimum().isInfinite() )
1122  simpleTheoryPropagation( columnVar->pInfimum() );
1123  if( !columnVar->supremum().isInfinite() && columnVar->supremum().type() != LRABound::Type::EQUAL )
1124  simpleTheoryPropagation( columnVar->pSupremum() );
1125  }
1126  }
1127 
1128 // #define LRA_DEBUG_SIMPLE_THEORY_PROPAGATION
1129  template<class Settings>
1130  void LRAModule<Settings>::simpleTheoryPropagation( const LRABound* _bound )
1131  {
1132  if( !_bound->exists() || (!_bound->isActive() && !_bound->isComplementActive()) )
1133  {
1134  return;
1135  }
1136  switch( _bound->type() )
1137  {
1138  case LRABound::Type::EQUAL:
1139  propagateEqualBound( _bound );
1140  break;
1141  case LRABound::Type::LOWER:
1142  propagateLowerBound( _bound );
1143  break;
1144  default:
1145  assert( _bound->type() == LRABound::Type::UPPER );
1146  propagateUpperBound( _bound );
1147  break;
1148  }
1149  }
1150 
1151  template<class Settings>
1152  void LRAModule<Settings>::propagate( const LRABound* _premise, const FormulaT& _conclusion )
1153  {
1154  FormulasT premise;
1155  collectOrigins( *_premise->origins().begin(), premise );
1156  mTheoryPropagations.emplace_back( std::move(premise), _conclusion );
1157  #ifdef LRA_DEBUG_SIMPLE_THEORY_PROPAGATION
1158  std::cout << "theory propagation: " << mTheoryPropagations.back().mPremise << " => " << mTheoryPropagations.back().mConclusion << std::endl;
1159  #endif
1160  #ifdef SMTRAT_DEVOPTION_Statistics
1161  mStatistics.propagateTheory();
1162  #endif
1163  }
1164 
1165  template<class Settings>
1166  void LRAModule<Settings>::propagateLowerBound( const LRABound* _bound )
1167  {
1168  const LRAVariable& lraVar = _bound->variable();
1169  auto cbIter = lraVar.upperbounds().begin();
1170  for(; !(*cbIter)->isInfinite() && (*cbIter)->limit() < _bound->limit(); ++cbIter )
1171  {
1172  if( (*cbIter)->isUnassigned() && (*cbIter)->type() != LRABound::Type::EQUAL )
1173  {
1174  // p>b => not(p<c) if b>=c
1175  // p>b => not(p<=c) if b>=c
1176  // p>=b => not(p<c) if b>=c
1177  // p>=b => not(p<=c) if b>c
1178  propagate( _bound, (*cbIter)->asConstraint().negated() );
1179  }
1180  }
1181  cbIter = lraVar.lowerbounds().find( _bound );
1182  assert( cbIter != lraVar.lowerbounds().end() );
1183  assert( cbIter != lraVar.lowerbounds().begin() );
1184  --cbIter;
1185  for(;;)
1186  {
1187  if( (*cbIter)->isUnassigned() )
1188  {
1189  if( (*cbIter)->type() == LRABound::Type::EQUAL )
1190  {
1191  if( mActiveUnresolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveUnresolvedNEQConstraints.end()
1192  && mActiveResolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveResolvedNEQConstraints.end() )
1193  {
1194  // p>b => not(p=c) if b>=c
1195  // p>=b => not(p=c) if b>c
1196  propagate( _bound, (*cbIter)->asConstraint().negated() );
1197  }
1198  }
1199  else
1200  {
1201  // p>b => p>c if b>c
1202  // p>b => p>=c if b>=c
1203  // p>=b => p>c if b>c
1204  // p>=b => p>=c if b>c
1205  propagate( _bound, (*cbIter)->asConstraint() );
1206  }
1207  }
1208  if( cbIter == lraVar.lowerbounds().begin() )
1209  break;
1210  --cbIter;
1211  }
1212  }
1213 
1214  template<class Settings>
1215  void LRAModule<Settings>::propagateUpperBound( const LRABound* _bound )
1216  {
1217  const LRAVariable& lraVar = _bound->variable();
1218  auto cbIter = lraVar.lowerbounds().end();
1219  --cbIter;
1220  for(; !(*cbIter)->isInfinite() && (*cbIter)->limit() > _bound->limit(); --cbIter )
1221  {
1222  if( (*cbIter)->isUnassigned() && (*cbIter)->type() != LRABound::Type::EQUAL )
1223  {
1224  // p<b => not(p>c) if b<=c
1225  // p<b => not(p>=c) if b<=c
1226  // p<=b => not(p>c) if b<=c
1227  // p<=b => not(p>=c) if b<c
1228  propagate( _bound, (*cbIter)->asConstraint().negated() );
1229  }
1230  }
1231  cbIter = lraVar.upperbounds().find( _bound );
1232  assert( cbIter != lraVar.upperbounds().end() );
1233  ++cbIter;
1234  for(; cbIter != lraVar.upperbounds().end(); ++cbIter )
1235  {
1236  if( (*cbIter)->isUnassigned() )
1237  {
1238  if( (*cbIter)->type() == LRABound::Type::EQUAL )
1239  {
1240  if( mActiveUnresolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveUnresolvedNEQConstraints.end()
1241  && mActiveResolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveResolvedNEQConstraints.end() )
1242  {
1243  // p<b => not(p=c) if b<=c
1244  // p<=b => not(p=c) if b<c
1245  propagate( _bound, (*cbIter)->asConstraint().negated() );
1246  }
1247  }
1248  else
1249  {
1250  // p<b => p<c if b<c
1251  // p<b => p<=c if b<=c
1252  // p<=b => p<c if b<c
1253  // p<=b => p<=c if b<c
1254  propagate( _bound, (*cbIter)->asConstraint() );
1255  }
1256  }
1257  }
1258  }
1259 
1260  template<class Settings>
1261  void LRAModule<Settings>::propagateEqualBound( const LRABound* _bound )
1262  {
1263  const LRAVariable& lraVar = _bound->variable();
1264  auto cbIter = lraVar.lowerbounds().begin();
1265  for(; *cbIter != _bound; ++cbIter )
1266  {
1267  if( (*cbIter)->isUnassigned() )
1268  {
1269  if( (*cbIter)->type() == LRABound::Type::EQUAL )
1270  {
1271  if( mActiveUnresolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveUnresolvedNEQConstraints.end()
1272  && mActiveResolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveResolvedNEQConstraints.end() )
1273  {
1274  // p=b => not(p=c) if b>c
1275  propagate( _bound, (*cbIter)->asConstraint().negated() );
1276  }
1277  }
1278  else
1279  {
1280  // p=b => p>c if b>c
1281  // p=b => p>=c if b>=c
1282  propagate( _bound, (*cbIter)->asConstraint() );
1283  }
1284  }
1285  }
1286  ++cbIter;
1287  for(; cbIter != lraVar.lowerbounds().end(); ++cbIter )
1288  {
1289  if( (*cbIter)->isUnassigned() )
1290  {
1291  if( (*cbIter)->type() == LRABound::Type::EQUAL )
1292  {
1293  if( mActiveUnresolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveUnresolvedNEQConstraints.end()
1294  && mActiveResolvedNEQConstraints.find( (*cbIter)->asConstraint().negated() ) == mActiveResolvedNEQConstraints.end() )
1295  {
1296  // p=b => not(p=c) if b<c
1297  propagate( _bound, (*cbIter)->asConstraint().negated() );
1298  }
1299  }
1300  else
1301  {
1302  // p=b => not(p>c) if b<c
1303  // p=b => not(p>=c) if b<c
1304  propagate( _bound, (*cbIter)->asConstraint().negated() );
1305  }
1306  }
1307  }
1308  cbIter = lraVar.upperbounds().begin();
1309  for(; *cbIter != _bound; ++cbIter )
1310  {
1311  if( (*cbIter)->isUnassigned() && (*cbIter)->type() != LRABound::Type::EQUAL )
1312  {
1313  // p=b => not(p<c) if b>c
1314  // [p=b => not(p=c) if b>c] is already covered as p=c us also a lower bound
1315  // p=b => not(p<=c) if b>c
1316  propagate( _bound, (*cbIter)->asConstraint().negated() );
1317  }
1318  }
1319  ++cbIter;
1320  for(; cbIter != lraVar.upperbounds().end(); ++cbIter )
1321  {
1322  if( (*cbIter)->isUnassigned() && (*cbIter)->type() != LRABound::Type::EQUAL )
1323  {
1324  // p=b => p>c if b<c
1325  // [p=b => not(p=c) if b<c] is already covered as p=c us also a lower bound
1326  // p=b => p>=c if b<=c
1327  propagate( _bound, (*cbIter)->asConstraint() );
1328  }
1329  }
1330  }
1331 
1332  template<class Settings>
1333  void LRAModule<Settings>::init()
1334  {
1335  if( !mInitialized )
1336  {
1337  mInitialized = true;
1338  for( const FormulaT& constraint : mLinearConstraints )
1339  {
1340  setBound( constraint );
1341  }
1342 // mTableau.setSize( mTableau.slackVars().size(), mTableau.originalVars().size(), mLinearConstraints.size() );
1343  mTableau.setBlandsRuleStart( 100 );
1344  }
1345  }
1346 
1347  template<class Settings>
1348  bool LRAModule<Settings>::gomoryCut()
1349  {
1350  const RationalAssignment& rMap_ = getRationalModel();
1351  bool all_int = true;
1352  for( LRAVariable* basicVar : mTableau.rows() )
1353  {
1354  auto vars = carl::variables(basicVar->expression());
1355  // TODO JNE why should this hold? Doesn't this correspond to the variables of a tableu row?
1356  assert( !vars.empty() );
1357  auto found_ex = rMap_.find(*vars.begin());
1358  const Rational& ass = found_ex->second;
1359  if( !carl::is_integer( ass ) )
1360  {
1361  all_int = false;
1362  const Poly::PolyType* gomory_poly = mTableau.gomoryCut(ass, basicVar);
1363  if( *gomory_poly != Rational(0) )
1364  {
1365  ConstraintT gomory_constr = ConstraintT( *gomory_poly , carl::Relation::GEQ );
1366  ConstraintT neg_gomory_constr = ConstraintT( *gomory_poly - carl::evaluate(*gomory_poly, rMap_ ), carl::Relation::LESS );
1367  //std::cout << gomory_constr << std::endl;
1368  assert( !carl::satisfied_by( gomory_constr, rMap_ ) );
1369  assert( !carl::satisfied_by( neg_gomory_constr, rMap_ ) );
1370  FormulasT subformulas;
1371  mTableau.collect_premises( basicVar, subformulas );
1372  FormulasT premisesOrigins;
1373  for( const FormulaT& pf : subformulas )
1374  collectOrigins( pf, premisesOrigins );
1375  FormulasT premise;
1376  for( const FormulaT& pre : premisesOrigins )
1377  premise.push_back( pre.negated() );
1378  premise.push_back( FormulaT( gomory_constr ) );
1379  FormulaT lemma( carl::FormulaType::OR, std::move( premise ) );
1380 // std::cout << " >>> found gomory cut: " << lemma << std::endl;
1381  addLemma( lemma );
1382  }
1383  }
1384  }
1385  return !all_int;
1386  }
1387 
1388  template<class Settings>
1389  bool LRAModule<Settings>::branch_and_bound()
1390  {
1391  carl::Variables varsToExclude;
1392  return mostInfeasibleVar( Settings::use_gomory_cuts, varsToExclude );
1393  }
1394 
1395  template<class Settings>
1396  bool LRAModule<Settings>::mostInfeasibleVar( bool _tryGomoryCut, carl::Variables& _varsToExclude )
1397  {
1398  const RationalAssignment& _rMap = getRationalModel();
1399  auto branch_var = mTableau.originalVars().begin();
1400  Rational ass_;
1401  bool result = false;
1402  Rational diff = 1;
1403  for( auto map_iterator = _rMap.begin(); map_iterator != _rMap.end(); ++map_iterator )
1404  {
1405  auto var = mTableau.originalVars().find( map_iterator->first );
1406  if( _varsToExclude.find( var->first ) != _varsToExclude.end() )
1407  continue;
1408  assert( var->first == map_iterator->first );
1409  const Rational& ass = map_iterator->second;
1410  if( (var->first.type() == carl::VariableType::VT_INT || var->first.type() == carl::VariableType::VT_BOOL) && !carl::is_integer( ass ) )
1411  {
1412  if( mFinalCheck )
1413  {
1414  Rational curr_diff = carl::abs( Rational( Rational(ass - carl::floor(ass)) - Rational(1)/Rational(2)) );
1415  if( curr_diff < diff )
1416  {
1417  result = true;
1418  diff = curr_diff;
1419  branch_var = var;
1420  ass_ = ass;
1421  }
1422  }
1423  else
1424  return true;
1425  }
1426  }
1427  if( result )
1428  {
1429 // std::cout << "try to branch at (" << branch_var->second->expression() << ", " << ass_ << ")" << std::endl;
1430  if( probablyLooping( branch_var->second->expression(), ass_ ) )
1431  {
1432 // std::cout << " >>> probably looping!" << std::endl;
1433  if( _tryGomoryCut && gomoryCut() )
1434  return true;
1435  _varsToExclude.insert( branch_var->first );
1436 // std::cout << " >>> exclude variable " << branch_var->first << std::endl;
1437  return mostInfeasibleVar( false, _varsToExclude );
1438  }
1439 // FormulaSetT premises;
1440 // mTableau.collect_premises( branch_var->second , premises );
1441 // FormulaSetT premisesOrigins;
1442 // for( auto& pf : premises )
1443 // {
1444 // collectOrigins( pf, premisesOrigins );
1445 // }
1446  branchAt( branch_var->second->expression(), true, ass_ );
1447  return true;
1448  }
1449  else
1450  return !_varsToExclude.empty();
1451  }
1452 
1453  template<class Settings>
1454  bool LRAModule<Settings>::assignmentConsistentWithTableau( const RationalAssignment& _assignment, const LRABoundType& _delta ) const
1455  {
1456  for( auto slackVar : mTableau.slackVars() )
1457  {
1458  Poly tmp = carl::substitute(*slackVar.first, _assignment );
1459  assert( tmp.is_constant() );
1460  LRABoundType slackVarAssignment = slackVar.second->assignment().mainPart() + slackVar.second->assignment().deltaPart() * _delta;
1461  if( !(tmp == Poly(Rational(slackVarAssignment))) )
1462  {
1463  return false;
1464  }
1465  }
1466  return true;
1467  }
1468 
1469  template<class Settings>
1470  bool LRAModule<Settings>::assignmentCorrect() const
1471  {
1472  if( solverState() == UNSAT ) return true;
1473  if( !mAssignmentFullfilsNonlinearConstraints ) return true;
1474  const RationalAssignment& rmodel = getRationalModel();
1475  carl::carlVariables inputVars(carl::variable_type_filter::arithmetic());
1476  rReceivedFormula().gatherVariables( inputVars );
1477  for( auto ass = rmodel.begin(); ass != rmodel.end(); ++ass )
1478  {
1479  if( ass->first.type() == carl::VariableType::VT_INT && !carl::is_integer( ass->second ) && inputVars.has( ass->first ) )
1480  {
1481  return false;
1482  }
1483 
1484  if ( ass->first.type() == carl::VariableType::VT_BOOL && !(ass->second == Rational(0) || ass->second == Rational(1)) )
1485  {
1486  return false;
1487  }
1488  }
1489  for( auto iter = rReceivedFormula().begin(); iter != rReceivedFormula().end(); ++iter )
1490  {
1491  unsigned sat = carl::satisfied_by(iter->formula(), Model(rmodel));
1492  if (sat != 1) {
1493  assert( sat == 0 );
1494  return false;
1495  }
1496  }
1497  return true;
1498  }
1499 
1500  #ifdef DEBUG_METHODS_LRA_MODULE
1501 
1502  template<class Settings>
1503  void LRAModule<Settings>::printLinearConstraints( std::ostream& _out, const std::string _init ) const
1504  {
1505  _out << _init << "Linear constraints:" << std::endl;
1506  for( auto iter = mLinearConstraints.begin(); iter != mLinearConstraints.end(); ++iter )
1507  {
1508  _out << _init << " " << *iter << std::endl;
1509  }
1510  }
1511 
1512  template<class Settings>
1513  void LRAModule<Settings>::printNonlinearConstraints( std::ostream& _out, const std::string _init ) const
1514  {
1515  _out << _init << "Nonlinear constraints:" << std::endl;
1516  for( auto iter = mNonlinearConstraints.begin(); iter != mNonlinearConstraints.end(); ++iter )
1517  {
1518  _out << _init << " " << *iter << std::endl;
1519  }
1520  }
1521 
1522  template<class Settings>
1523  void LRAModule<Settings>::printConstraintToBound( std::ostream& _out, const std::string _init ) const
1524  {
1525  _out << _init << "Mapping of constraints to bounds:" << std::endl;
1526  for( auto iter = mTableau.constraintToBound().begin(); iter != mTableau.constraintToBound().end(); ++iter )
1527  {
1528  _out << _init << " " << iter->first << std::endl;
1529  for( auto iter2 = iter->second->begin(); iter2 != iter->second->end(); ++iter2 )
1530  {
1531  _out << _init << " ";
1532  (*iter2)->print( true, std::cout, true );
1533  _out << std::endl;
1534  }
1535  }
1536  }
1537 
1538  template<class Settings>
1539  void LRAModule<Settings>::printBoundCandidatesToPass( std::ostream& _out, const std::string _init ) const
1540  {
1541  _out << _init << "Bound candidates to pass:" << std::endl;
1542  for( auto iter = mBoundCandidatesToPass.begin(); iter != mBoundCandidatesToPass.end(); ++iter )
1543  {
1544  _out << _init << " ";
1545  (*iter)->print( true, std::cout, true );
1546  _out << " [" << (*iter)->pInfo()->updated << "]" << std::endl;
1547  }
1548  }
1549 
1550  template<class Settings>
1551  void LRAModule<Settings>::printRationalModel( std::ostream& _out, const std::string _init ) const
1552  {
1553  const RationalAssignment& rmodel = getRationalModel();
1554  _out << _init << "Rational model:" << std::endl;
1555  for( auto assign = rmodel.begin(); assign != rmodel.end(); ++assign )
1556  {
1557  _out << _init;
1558  _out << std::setw(10) << assign->first;
1559  _out << " -> " << assign->second << std::endl;
1560  }
1561  }
1562 
1563  template<class Settings>
1564  void LRAModule<Settings>::printTableau( std::ostream& _out, const std::string _init ) const
1565  {
1566  mTableau.print( LAST_ENTRY_ID, _out, _init );
1567  }
1568 
1569  template<class Settings>
1570  void LRAModule<Settings>::printVariables( std::ostream& _out, const std::string _init ) const
1571  {
1572  mTableau.printVariables( true, _out, _init );
1573  }
1574  #endif
1575 } // namespace smtrat
1576 
1577