SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
VSModule.tpp
Go to the documentation of this file.
1 /**
2  * File: VSModule.cpp
3  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
4  * @since 2010-05-11
5  * @version 2014-11-27
6  */
7 
8 
9 #include "VSModule.h"
10 
11 #include <carl-arith/vs/Substitution.h>
12 #include <carl-arith/vs/Evaluation.h>
13 
14 #ifdef VS_STATE_DEBUG_METHODS
15 //#define VS_DEBUG_METHODS
16 #endif
17 //#define VS_DEBUG
18 //#define VS_MODULE_VERBOSE_INTEGERS
19 
20 namespace smtrat
21 {
22 
23  using namespace vs;
24  template<class Settings>
25  VSModule<Settings>::VSModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* const _manager ):
26  Module( _formula, _conditionals, _manager ),
27  mConditionsChanged( false ),
28  mInconsistentConstraintAdded( false ),
29  mLazyMode( false ),
30  mIDCounter( 0 ),
31  mLazyCheckThreshold( Settings::lazy_check_threshold ),
32  mpConditionIdAllocator(new carl::IDPool() ),
33  mpStateTree( new State( mpConditionIdAllocator, Settings::use_variable_bounds ) ),
34  mAllVariables(),
35  mFormulaConditionMap(),
36  mRanking(),
37  mVariableVector()
38  {
39  #ifdef SMTRAT_DEVOPTION_Statistics
40  mpStateTree->setStatistics( &mStatistics );
41  #endif
42  }
43 
44  template<class Settings>
45  VSModule<Settings>::~VSModule()
46  {
47  while( !mFormulaConditionMap.empty() )
48  {
49  const vs::Condition* pRecCond = mFormulaConditionMap.begin()->second;
50  mFormulaConditionMap.erase( mFormulaConditionMap.begin() );
51  mpConditionIdAllocator->free( pRecCond->id() );
52  delete pRecCond;
53  pRecCond = NULL;
54  }
55  delete mpStateTree;
56  delete mpConditionIdAllocator;
57  }
58 
59  template<class Settings>
60  bool VSModule<Settings>::addCore( ModuleInput::const_iterator _subformula )
61  {
62  mLazyMode = false;
63  bool negated = false;
64  FormulaT constraintF = _subformula->formula();
65  if( constraintF.type() == carl::FormulaType::NOT && constraintF.subformula().type() == carl::FormulaType::CONSTRAINT )
66  {
67  constraintF = _subformula->formula().subformula();
68  negated = true;
69  }
70  if( constraintF.type() == carl::FormulaType::CONSTRAINT )
71  {
72  const ConstraintT& constraint = negated ? ConstraintT( constraintF.constraint().lhs(), carl::inverse( constraintF.constraint().relation() ) ) : constraintF.constraint();
73  const vs::Condition* condition = new vs::Condition( constraint, mpConditionIdAllocator->get() );
74  mFormulaConditionMap[constraintF] = condition;
75  assert( constraint.is_consistent() == 2 );
76  for( auto var: constraint.variables() )
77  mAllVariables.insert( var );
78  if( Settings::incremental_solving )
79  {
80  removeStatesFromRanking( *mpStateTree );
81  mIDCounter = 0;
82  carl::PointerSet<vs::Condition> oConds;
83  oConds.insert( condition );
84  std::vector<DisjunctionOfConditionConjunctions> subResults;
85  DisjunctionOfConditionConjunctions subResult;
86 
87  if( Settings::split_neq_constraints && constraint.hasIntegerValuedVariable() && !constraint.hasRealValuedVariable() && constraint.relation() == carl::Relation::NEQ )
88  {
89  ConditionList condVectorA;
90  condVectorA.push_back( new vs::Condition( ConstraintT( constraint.lhs(), carl::Relation::LESS ), mpConditionIdAllocator->get(), 0, false, oConds ) );
91  subResult.push_back( std::move(condVectorA) );
92  ConditionList condVectorB;
93  condVectorB.push_back( new vs::Condition( ConstraintT( constraint.lhs(), carl::Relation::GREATER ), mpConditionIdAllocator->get(), 0, false, oConds ) );
94  subResult.push_back( std::move(condVectorB) );
95  }
96  else
97  {
98  ConditionList condVector;
99  condVector.push_back( new vs::Condition( constraint, mpConditionIdAllocator->get(), 0, false, oConds ) );
100  subResult.push_back( std::move(condVector) );
101  }
102  subResults.push_back( std::move(subResult) );
103  mpStateTree->addSubstitutionResults( std::move(subResults) );
104  addStateToRanking( mpStateTree );
105  insertTooHighDegreeStatesInRanking( mpStateTree );
106  }
107  mConditionsChanged = true;
108  }
109  else if( _subformula->formula().type() == carl::FormulaType::FALSE )
110  {
111  removeStatesFromRanking( *mpStateTree );
112  mIDCounter = 0;
113  mInfeasibleSubsets.clear();
114  mInfeasibleSubsets.emplace_back();
115  mInfeasibleSubsets.back().insert( _subformula->formula() );
116  #ifdef SMTRAT_DEVOPTION_Statistics
117  mStatistics.addConflict( rReceivedFormula(), mInfeasibleSubsets );
118  #endif
119  mInconsistentConstraintAdded = true;
120  assert( checkRanking() );
121  return false;
122  }
123  assert( checkRanking() );
124  return true;
125  }
126 
127  template<class Settings>
128  void VSModule<Settings>::removeCore( ModuleInput::const_iterator _subformula )
129  {
130  mLazyMode = false;
131  FormulaT constraintF = _subformula->formula();
132  if( constraintF.type() == carl::FormulaType::NOT && constraintF.subformula().type() == carl::FormulaType::CONSTRAINT )
133  constraintF = _subformula->formula().subformula();
134  if( constraintF.type() == carl::FormulaType::CONSTRAINT )
135  {
136  mInconsistentConstraintAdded = false;
137  auto formulaConditionPair = mFormulaConditionMap.find( constraintF );
138  assert( formulaConditionPair != mFormulaConditionMap.end() );
139  const vs::Condition* condToDelete = formulaConditionPair->second;
140  if( Settings::incremental_solving )
141  {
142  removeStatesFromRanking( *mpStateTree );
143  mpStateTree->rSubResultsSimplified() = false;
144  carl::PointerSet<vs::Condition> condsToDelete;
145  condsToDelete.insert( condToDelete );
146  mpStateTree->deleteOrigins( condsToDelete, mRanking );
147  mpStateTree->rType() = State::COMBINE_SUBRESULTS;
148  if( mpStateTree->hasSubResultsCombination() )
149  mpStateTree->rTakeSubResultCombAgain() = true;
150  else
151  mpStateTree->rTakeSubResultCombAgain() = false;
152  addStateToRanking( mpStateTree );
153  insertTooHighDegreeStatesInRanking( mpStateTree );
154  }
155  mFormulaConditionMap.erase( formulaConditionPair );
156  mpConditionIdAllocator->free( condToDelete->id() );
157  delete condToDelete;
158  condToDelete = NULL;
159  mConditionsChanged = true;
160  }
161  }
162 
163  template<class Settings>
164  Answer VSModule<Settings>::checkCore()
165  {
166  SMTRAT_LOG_DEBUG("smtrat.vs", "Starting checkCore()");
167  #ifdef SMTRAT_DEVOPTION_Statistics
168  mStatistics.check();
169  #endif
170  if( !Settings::incremental_solving )
171  {
172  SMTRAT_LOG_DEBUG("smtrat.vs", "Do not solve incrementally");
173  removeStatesFromRanking( *mpStateTree );
174  delete mpStateTree;
175  mpStateTree = new State( mpConditionIdAllocator, Settings::use_variable_bounds );
176  #ifdef SMTRAT_DEVOPTION_Statistics
177  mpStateTree->setStatistics( &mStatistics );
178  #endif
179  for( auto iter = mFormulaConditionMap.begin(); iter != mFormulaConditionMap.end(); ++iter )
180  {
181  carl::PointerSet<vs::Condition> oConds;
182  oConds.insert( iter->second );
183  std::vector<DisjunctionOfConditionConjunctions> subResults;
184  subResults.emplace_back();
185  subResults.back().emplace_back();
186  subResults.back().back().push_back( new vs::Condition( iter->first.constraint(), mpConditionIdAllocator->get(), 0, false, oConds ) );
187  mpStateTree->addSubstitutionResults( std::move(subResults) );
188  }
189  addStateToRanking( mpStateTree );
190  }
191  if( !rReceivedFormula().isConstraintLiteralConjunction() ) {
192  SMTRAT_LOG_DEBUG("smtrat.vs", "Is not a conjunction of literals, return unknown.");
193  return UNKNOWN;
194  }
195  if( !(rReceivedFormula().isIntegerConstraintLiteralConjunction() || rReceivedFormula().isRealConstraintLiteralConjunction()) ) {
196  SMTRAT_LOG_DEBUG("smtrat.vs", "Is not purely real or integer, return unknown.");
197  return UNKNOWN;
198  }
199  if( !mFinalCheck && !mConditionsChanged && (!mFullCheck || mLastCheckFull) )
200  {
201  SMTRAT_LOG_DEBUG("smtrat.vs", "Do not perform a proper check, exit quickly");
202  if( mInfeasibleSubsets.empty() )
203  {
204  if( solverState() == SAT )
205  {
206  if( !solutionInDomain() )
207  {
208  return UNKNOWN;
209  }
210  else
211  {
212  return consistencyTrue();
213  }
214  }
215  else
216  {
217  return (mFormulaConditionMap.empty() ? consistencyTrue() : UNKNOWN );
218  }
219  }
220  else
221  return UNSAT;
222  }
223  mConditionsChanged = false;
224  mLastCheckFull = mFullCheck;
225  if( rReceivedFormula().empty() )
226  {
227  SMTRAT_LOG_DEBUG("smtrat.vs", "Received formula is empty");
228  if( !solutionInDomain() )
229  {
230  return UNKNOWN;
231  }
232  else
233  {
234  return consistencyTrue();
235  }
236  }
237  if( mInconsistentConstraintAdded )
238  {
239  SMTRAT_LOG_DEBUG("smtrat.vs", "Inconsistent constraint was found");
240  assert( !mInfeasibleSubsets.empty() );
241  assert( !mInfeasibleSubsets.back().empty() );
242  return UNSAT;
243  }
244  if( Settings::use_variable_bounds )
245  {
246  SMTRAT_LOG_DEBUG("smtrat.vs", "Trying to employ variable bounds");
247  if( !mpStateTree->variableBounds().isConflicting() )
248  {
249  std::vector<std::pair<std::vector<ConstraintT>, ConstraintT>> bDeds = mpStateTree->variableBounds().getBoundDeductions();
250  for( auto bDed = bDeds.begin(); bDed != bDeds.end(); ++bDed )
251  {
252  FormulasT subformulas;
253  for( auto cons = bDed->first.begin(); cons != bDed->first.end(); ++cons )
254  {
255  subformulas.emplace_back( carl::FormulaType::NOT, FormulaT( *cons ) ); // @todo store formulas and do not generate a formula here
256  }
257  subformulas.emplace_back( bDed->second );
258  addLemma( FormulaT( carl::FormulaType::OR, std::move( subformulas ) ) );
259  }
260  }
261  }
262  mLazyMode = !mFullCheck || Settings::try_first_lazy;
263  if( Settings::try_first_lazy && mFullCheck )
264  {
265  mLazyCheckThreshold = 1;
266  }
267  else if( !mFullCheck )
268  {
269  mLazyCheckThreshold = Settings::lazy_check_threshold;
270  }
271  while( !mRanking.empty() )
272  {
273  SMTRAT_LOG_DEBUG("smtrat.vs", "Ranking is not empty yet");
274  assert( checkRanking() );
275 // std::this_thread::sleep_for(std::chrono::milliseconds(1000));
276  if( anAnswerFound() )
277  return ABORTED;
278 // else
279 // std::cout << "VSModule iteration" << std::endl;
280  #ifdef SMTRAT_DEVOPTION_Statistics
281  mStatistics.considerState();
282  #endif
283  State* currentState = mRanking.begin()->second;
284  #ifdef VS_DEBUG
285  std::cout << "Ranking:" << std::endl;
286  for( auto valDTPair = mRanking.begin(); valDTPair != mRanking.end(); ++valDTPair )
287  {
288  std::stringstream stream;
289  stream << "(" << valDTPair->first.first << ", " << valDTPair->first.second.first << ", " << valDTPair->first.second.second << ")";
290  std::cout << std::setw(15) << stream.str();
291  std::cout << ": " << valDTPair->second << std::endl;
292  }
293  std::cout << "*** Considered state:" << std::endl;
294  currentState->printAlone( "*** ", std::cout );
295  #endif
296  currentState->simplify( mRanking );
297  #ifdef VS_DEBUG
298  std::cout << "Simplifing results in " << std::endl;
299  currentState->printAlone( "*** ", std::cout );
300  #endif
301 // if( !Settings::split_neq_constraints && !currentState->isInconsistent() && !currentState->takeSubResultCombAgain() )
302 // {
303 // for( auto cond = currentState->conditions().begin(); cond != currentState->conditions().end(); ++cond )
304 // {
305 // if( (*cond)->constraint().hasIntegerValuedVariable() && !(*cond)->constraint().hasRealValuedVariable()
306 // && (*cond)->constraint().relation() == carl::Relation::NEQ )
307 // {
308 // // Split the neq-constraint in a preceeding sat module (make sure that it is there in your strategy when choosing this vssetting)
309 // splitUnequalConstraint( FormulaT( (*cond)->constraint() ) );
310 // assert( currentState->isRoot() );
311 // return UNKNOWN;
312 // }
313 // }
314 // }
315  if( currentState->hasChildrenToInsert() )
316  {
317  SMTRAT_LOG_DEBUG("smtrat.vs", "Children to insert");
318  currentState->rHasChildrenToInsert() = false;
319  addStatesToRanking( currentState );
320  }
321  else
322  {
323  SMTRAT_LOG_DEBUG("smtrat.vs", "No children to insert");
324  if( currentState->isInconsistent() )
325  {
326  SMTRAT_LOG_DEBUG("smtrat.vs", "Current state is inconsistent");
327  #ifdef VS_LOG_INTERMEDIATE_STEPS
328  logConditions( *currentState, false, "Intermediate_conflict_of_VSModule" );
329  #endif
330  removeStatesFromRanking( *currentState );
331  if( currentState->isRoot() )
332  {
333  updateInfeasibleSubset();
334  return UNSAT;
335  }
336  else
337  {
338  currentState->passConflictToFather( Settings::check_conflict_for_side_conditions );
339  removeStateFromRanking( currentState->rFather() );
340  addStateToRanking( currentState->pFather() );
341  }
342  }
343  else if( currentState->takeSubResultCombAgain() && currentState->type() == State::COMBINE_SUBRESULTS )
344  {
345  SMTRAT_LOG_DEBUG("smtrat.vs", "Case 2");
346  #ifdef VS_DEBUG
347  std::cout << "*** Refresh conditons:" << std::endl;
348  #endif
349  if( currentState->refreshConditions( mRanking ) )
350  addStateToRanking( currentState );
351  else
352  addStatesToRanking( currentState );
353  currentState->rTakeSubResultCombAgain() = false;
354  #ifdef VS_DEBUG
355  currentState->printAlone( " ", std::cout );
356  std::cout << "*** Conditions refreshed." << std::endl;
357  #endif
358  }
359  else if( currentState->hasRecentlyAddedConditions() )//&& !(currentState->takeSubResultCombAgain() && currentState->isRoot() ) )
360  {
361  SMTRAT_LOG_DEBUG("smtrat.vs", "Current state has new conditions");
362  #ifdef VS_DEBUG
363  std::cout << "*** Propagate new conditions :" << std::endl;
364  #endif
365  propagateNewConditions(currentState);
366  #ifdef VS_DEBUG
367  std::cout << "*** Propagate new conditions ready." << std::endl;
368  #endif
369  }
370  else
371  {
372  SMTRAT_LOG_DEBUG("smtrat.vs", "Case 4");
373  if( Settings::use_variable_bounds && !currentState->checkTestCandidatesForBounds() )
374  {
375  SMTRAT_LOG_DEBUG("smtrat.vs", "Test candidates invalidates bounds");
376  currentState->rInconsistent() = true;
377  removeStatesFromRanking( *currentState );
378  }
379  else
380  {
381  if( mLazyMode && currentState->getNumberOfCurrentSubresultCombination() > mLazyCheckThreshold )
382  {
383  SMTRAT_LOG_DEBUG("smtrat.vs", "LazyMode case");
384  if( mFullCheck )
385  {
386  if( currentState->cannotBeSolved( true ) )
387  {
388  removeStatesFromRanking( *mpStateTree );
389  mLazyMode = false;
390  mpStateTree->resetCannotBeSolvedLazyFlags();
391  addStatesToRanking( mpStateTree );
392  continue;
393  }
394  if( currentState->initIndex( mAllVariables, VariableValuationStrategy::OPTIMIZE_BEST, Settings::prefer_equation_over_all, true, Settings::use_fixed_variable_order ) )
395  {
396  currentState->initConditionFlags();
397  currentState->resetConflictSets();
398  while( !currentState->children().empty() )
399  {
400  State* toDelete = currentState->rChildren().back();
401  removeStatesFromRanking( *toDelete );
402  currentState->rChildren().pop_back();
403  currentState->resetInfinityChild( toDelete );
404  delete toDelete; // DELETE STATE
405  }
406  currentState->updateIntTestCandidates();
407  }
408  else
409  {
410  removeStatesFromRanking( *currentState );
411  currentState->rCannotBeSolvedLazy() = true;
412  addStateToRanking( currentState );
413  }
414  }
415  else
416  {
417  if( currentState->cannotBeSolved( true ) )
418  {
419  return UNKNOWN;
420  }
421  removeStatesFromRanking( *currentState );
422  currentState->rCannotBeSolvedLazy() = true;
423  addStateToRanking( currentState );
424  }
425  }
426  switch( currentState->type() )
427  {
428  case State::SUBSTITUTION_TO_APPLY:
429  {
430  SMTRAT_LOG_DEBUG("smtrat.vs", "Applying substitution");
431  #ifdef VS_DEBUG
432  std::cout << "*** SubstituteAll changes it to:" << std::endl;
433  #else
434  #ifdef VS_MODULE_VERBOSE_INTEGERS
435  bool minf = currentState->substitution().type() == Substitution::MINUS_INFINITY;
436  if( !minf )
437  {
438  std::cout << std::string( currentState->treeDepth()*3, ' ') << "Test candidate " << std::endl;
439  currentState->substitution().print( true, false, std::cout, std::string( currentState->treeDepth()*3, ' '));
440  }
441  #endif
442  #endif
443  if( !substituteAll( currentState, currentState->rFather().rConditions() ) )
444  {
445  // Delete the currently considered state.
446  assert( currentState->rInconsistent() );
447  removeStateFromRanking( *currentState );
448  }
449  #ifndef VS_DEBUG
450  #ifdef VS_MODULE_VERBOSE_INTEGERS
451  if( minf )
452  {
453  std::cout << std::string( currentState->treeDepth()*3, ' ') << "Test candidate [from -inf]" << std::endl;
454  currentState->substitution().print( true, false, std::cout, std::string( currentState->treeDepth()*3, ' '));
455  }
456  #endif
457  #endif
458  #ifdef VS_DEBUG
459  std::cout << "*** SubstituteAll ready." << std::endl;
460  #endif
461  break;
462  }
463  case State::COMBINE_SUBRESULTS:
464  {
465  SMTRAT_LOG_DEBUG("smtrat.vs", "Combining subresults");
466  #ifdef VS_DEBUG
467  std::cout << "*** Refresh conditons:" << std::endl;
468  #endif
469  if( currentState->nextSubResultCombination() )
470  {
471  if( currentState->refreshConditions( mRanking ) )
472  {
473  #ifdef SMTRAT_DEVOPTION_Statistics
474  mStatistics.considerCase();
475  #endif
476  addStateToRanking( currentState );
477  }
478  else
479  addStatesToRanking( currentState );
480  #ifdef VS_DEBUG
481  currentState->printAlone( " ", std::cout );
482  #endif
483  }
484  else
485  {
486  // If it was the last combination, delete the state.
487  currentState->rInconsistent() = true;
488  removeStatesFromRanking( *currentState );
489  currentState->rFather().rMarkedAsDeleted() = false;
490  addStateToRanking( currentState->pFather() );
491 
492  }
493  #ifdef VS_DEBUG
494  std::cout << "*** Conditions refreshed." << std::endl;
495  #endif
496  break;
497  }
498  case State::TEST_CANDIDATE_TO_GENERATE:
499  {
500  SMTRAT_LOG_DEBUG("smtrat.vs", "Generating test candidate");
501  // Set the index, if not already done, to the best variable to eliminate next.
502  if( currentState->index() == carl::Variable::NO_VARIABLE )
503  currentState->initIndex( mAllVariables, VariableValuationStrategy::OPTIMIZE_BEST, Settings::prefer_equation_over_all, false, Settings::use_fixed_variable_order );
504  else if( currentState->tryToRefreshIndex() )
505  {
506  if( currentState->initIndex( mAllVariables, VariableValuationStrategy::OPTIMIZE_BEST, Settings::prefer_equation_over_all, false, Settings::use_fixed_variable_order ) )
507  {
508  currentState->initConditionFlags();
509  currentState->resetConflictSets();
510  while( !currentState->children().empty() )
511  {
512  State* toDelete = currentState->rChildren().back();
513  removeStatesFromRanking( *toDelete );
514  currentState->rChildren().pop_back();
515  currentState->resetInfinityChild( toDelete );
516  delete toDelete; // DELETE STATE
517  }
518  currentState->updateIntTestCandidates();
519  }
520  }
521  // Find the most adequate conditions to continue.
522  const vs::Condition* currentCondition;
523  if( !currentState->bestCondition( currentCondition, mAllVariables.size(), Settings::prefer_equation_over_all ) )
524  {
525  SMTRAT_LOG_DEBUG("smtrat.vs", "Not the best condition");
526  if( !(*currentState).cannotBeSolved( mLazyMode ) && currentState->tooHighDegreeConditions().empty() )
527  {
528  if( currentState->conditions().empty() )
529  {
530  SMTRAT_LOG_DEBUG("smtrat.vs", "No conditions");
531  #ifdef VS_DEBUG
532  std::cout << "*** Check ancestors!" << std::endl;
533  #endif
534  // Check if there are still conditions in any ancestor, which have not been considered.
535  State * unfinishedAncestor;
536  if( currentState->unfinishedAncestor( unfinishedAncestor ) )
537  {
538  SMTRAT_LOG_DEBUG("smtrat.vs", "Has unfinished ancestor");
539  // Go back to this ancestor and refine.
540  removeStatesFromRanking( *unfinishedAncestor );
541  unfinishedAncestor->extendSubResultCombination();
542  unfinishedAncestor->rType() = State::COMBINE_SUBRESULTS;
543  if( unfinishedAncestor->refreshConditions( mRanking ) )
544  addStateToRanking( unfinishedAncestor );
545  else
546  addStatesToRanking( unfinishedAncestor );
547  #ifdef VS_DEBUG
548  std::cout << "*** Found an unfinished ancestor:" << std::endl;
549  unfinishedAncestor->printAlone();
550  #endif
551  }
552  else // Solution.
553  {
554  SMTRAT_LOG_DEBUG("smtrat.vs", "Has a solution");
555  if( !solutionInDomain() )
556  {
557  bool cannotBeSolved = false;
558  State* cur = currentState;
559  while (!cannotBeSolved && cur != nullptr) {
560  cannotBeSolved = cannotBeSolved || cur->cannotBeSolved(mLazyMode);
561  cur = cur->pFather();
562  }
563  SMTRAT_LOG_DEBUG("smtrat.vs", "Checking for solvability " << mLazyMode << " -> " << currentState->cannotBeSolved(mLazyMode));
564  if (!cannotBeSolved) {
565  SMTRAT_LOG_DEBUG("smtrat.vs", "Solution is not in domain");
566  return UNKNOWN;
567  } else {
568  SMTRAT_LOG_DEBUG("smtrat.vs", "Found infeasibility of this state");
569  }
570  }
571  else
572  {
573  SMTRAT_LOG_DEBUG("smtrat.vs", "Checking the consistency");
574  return consistencyTrue();
575  }
576  }
577  }
578  // It is a state, where all conditions have been used for test candidate generation.
579  else
580  {
581  // Check whether there are still test candidates in form of children left.
582  bool currentStateHasChildrenToConsider = false;
583  bool currentStateHasChildrenWithToHighDegree = false;
584  auto child = currentState->rChildren().begin();
585  while( child != currentState->children().end() )
586  {
587  if( !(**child).isInconsistent() )
588  {
589  if( !(**child).markedAsDeleted() )
590  addStateToRanking( *child );
591  if( !(**child).cannotBeSolved( mLazyMode ) && !(**child).markedAsDeleted() )
592  currentStateHasChildrenToConsider = true;
593  else
594  currentStateHasChildrenWithToHighDegree = true;
595  }
596  child++;
597  }
598 
599  if( !currentStateHasChildrenToConsider )
600  {
601  if( !currentStateHasChildrenWithToHighDegree )
602  {
603  currentState->rInconsistent() = true;
604  #ifdef VS_LOG_INTERMEDIATE_STEPS
605  logConditions( *currentState, false, "Intermediate_conflict_of_VSModule" );
606  #endif
607  removeStatesFromRanking( *currentState );
608  if( currentState->isRoot() )
609  updateInfeasibleSubset();
610  else
611  {
612  currentState->passConflictToFather( Settings::check_conflict_for_side_conditions );
613  removeStateFromRanking( currentState->rFather() );
614  addStateToRanking( currentState->pFather() );
615  }
616  }
617  else
618  {
619  currentState->rMarkedAsDeleted() = true;
620  removeStateFromRanking( *currentState );
621  }
622  }
623  }
624  }
625  else
626  {
627  if( (*currentState).cannotBeSolved( mLazyMode ) )
628  {
629  // If we need to involve another approach.
630  Answer result = runBackendSolvers( currentState );
631  switch( result )
632  {
633  case SAT:
634  {
635  currentState->rCannotBeSolved() = true;
636  State * unfinishedAncestor;
637  if( currentState->unfinishedAncestor( unfinishedAncestor ) )
638  {
639  // Go back to this ancestor and refine.
640  removeStatesFromRanking( *unfinishedAncestor );
641  unfinishedAncestor->extendSubResultCombination();
642  unfinishedAncestor->rType() = State::COMBINE_SUBRESULTS;
643  if( unfinishedAncestor->refreshConditions( mRanking ) )
644  addStateToRanking( unfinishedAncestor );
645  else
646  addStatesToRanking( unfinishedAncestor );
647  }
648  else // Solution.
649  {
650  if( !solutionInDomain() )
651  {
652  return UNKNOWN;
653  }
654  else
655  {
656  return consistencyTrue();
657  }
658  }
659  break;
660  }
661  case UNSAT:
662  {
663  break;
664  }
665  case UNKNOWN:
666  {
667  return UNKNOWN;
668  }
669  case ABORTED:
670  {
671  return ABORTED;
672  }
673  default:
674  {
675  std::cout << "Error: UNKNOWN answer in method " << __func__ << " line " << __LINE__ << std::endl;
676  return UNKNOWN;
677  }
678  }
679  }
680  else
681  {
682  currentState->rCannotBeSolved() = true;
683  addStateToRanking( currentState );
684  }
685  }
686  }
687  // Generate test candidates for the chosen variable and the chosen condition.
688  else
689  {
690  if( Settings::local_conflict_search && currentState->index().type() == carl::VariableType::VT_REAL && currentState->hasLocalConflict() )
691  {
692  removeStatesFromRanking( *currentState );
693  addStateToRanking( currentState );
694  }
695  else
696  {
697  #ifdef VS_DEBUG
698  std::cout << "*** Eliminate " << currentState->index() << " in ";
699  std::cout << currentCondition->constraint();
700  std::cout << " creates:" << std::endl;
701  #endif
702  eliminate( currentState, currentState->index(), currentCondition );
703  #ifdef VS_DEBUG
704  std::cout << "*** Eliminate ready." << std::endl;
705  #endif
706  }
707  }
708  break;
709  }
710  default:
711  SMTRAT_LOG_DEBUG("smtrat.vs", "Fallthrough case.");
712  assert( false );
713  }
714  }
715  }
716  }
717  }
718  if( mpStateTree->markedAsDeleted() )
719  {
720  SMTRAT_LOG_DEBUG("smtrat.vs", "State tree is to be deleted");
721  #ifdef VS_DEBUG
722  printAll();
723  #endif
724  return UNKNOWN;
725  }
726  SMTRAT_LOG_DEBUG("smtrat.vs", "Nothing was found, return UNSAT");
727  #ifdef VS_LOG_INTERMEDIATE_STEPS
728  if( mpStateTree->conflictSets().empty() ) logConditions( *mpStateTree, false, "Intermediate_conflict_of_VSModule" );
729  #endif
730  assert( !mpStateTree->conflictSets().empty() );
731  updateInfeasibleSubset();
732  #ifdef VS_DEBUG
733  printAll();
734  #endif
735  return UNSAT;
736  }
737 
738  template<class Settings>
739  void VSModule<Settings>::updateModel() const
740  {
741  clearModel();
742  if( solverState() == SAT )
743  {
744  if( mFormulaConditionMap.empty() )
745  return;
746  for( size_t i = mVariableVector.size(); i<=mRanking.begin()->second->treeDepth(); ++i )
747  {
748  std::stringstream outA;
749  outA << "m_inf_" << id() << "_" << i;
750  carl::Variable minfVar( carl::fresh_real_variable( outA.str() ) );
751  std::stringstream outB;
752  outB << "eps_" << id() << "_" << i;
753  carl::Variable epsVar( carl::fresh_real_variable( outB.str() ) );
754  mVariableVector.push_back( std::pair<carl::Variable,carl::Variable>( minfVar, epsVar ) );
755  }
756  assert( !mRanking.empty() );
757  carl::Variables allVarsInRoot;
758  mpStateTree->variables( allVarsInRoot );
759  RationalAssignment rationalAssignments;
760  const State* state = mRanking.begin()->second;
761  while( !state->isRoot() )
762  {
763  const Substitution& sub = state->substitution();
764  ModelValue ass;
765  if( sub.type() == Substitution::MINUS_INFINITY )
766  ass = SqrtEx( mVariableVector.at( state->treeDepth()-1 ).first );
767  else
768  {
769  assert( sub.type() != Substitution::PLUS_INFINITY );
770  SqrtEx substitutedTerm = substitute(sub.term(), rationalAssignments );
771  if( sub.type() == Substitution::PLUS_EPSILON )
772  {
773  assert( state->substitution().variable().type() != carl::VariableType::VT_INT );
774  ass = substitutedTerm + SqrtEx( mVariableVector.at( state->treeDepth()-1 ).second );
775  }
776  else
777  {
778  if( substitutedTerm.isRational() )
779  ass = substitutedTerm.asRational();
780  if( substitutedTerm.is_polynomial() )
781  ass = carl::createSubstitution<Rational,Poly,ModelPolynomialSubstitution>( substitutedTerm.as_polynomial() );
782  else
783  ass = substitutedTerm;
784  }
785  }
786  mModel.insert(std::make_pair(state->substitution().variable(), ass));
787  state = state->pFather();
788  }
789  if( mRanking.begin()->second->cannotBeSolved( mLazyMode ) )
790  Module::getBackendsModel();
791  // All variables which occur in the root of the constructed state tree but were incidentally eliminated
792  // (during the elimination of another variable) can have an arbitrary assignment. If the variable has the
793  // real domain, we leave at as a parameter, and, if it has the integer domain we assign 0 to it.
794  for( auto var = allVarsInRoot.begin(); var != allVarsInRoot.end(); ++var )
795  {
796  mModel.insert(std::make_pair(*var, carl::createSubstitution<Rational,Poly,ModelPolynomialSubstitution>( Poly(0) )));
797  }
798  }
799  }
800 
801  template<class Settings>
802  Answer VSModule<Settings>::consistencyTrue()
803  {
804  #ifdef VS_LOG_INTERMEDIATE_STEPS
805  checkAnswer();
806  #endif
807  #ifdef VS_PRINT_ANSWERS
808  printAnswer();
809  #endif
810  #ifdef VS_DEBUG
811  printAll();
812  #endif
813  return SAT;
814  }
815 
816  template<class Settings>
817  void VSModule<Settings>::eliminate( State* _currentState, const carl::Variable& _eliminationVar, const vs::Condition* _condition )
818  {
819  // Get the constraint of this condition.
820  const ConstraintT& constraint = (*_condition).constraint();
821  assert( _condition->constraint().variables().has( _eliminationVar ) );
822  bool generatedTestCandidateBeingASolution = false;
823  unsigned numberOfAddedChildren = 0;
824  carl::PointerSet<vs::Condition> oConditions;
825  oConditions.insert( _condition );
826  if( !Settings::use_variable_bounds || _currentState->hasRootsInVariableBounds( _condition, Settings::sturm_sequence_for_root_check ) )
827  {
828  carl::Relation relation = (*_condition).constraint().relation();
829  if( !Settings::use_strict_inequalities_for_test_candidate_generation )
830  {
831  if( relation == carl::Relation::LESS || relation == carl::Relation::GREATER || relation == carl::Relation::NEQ )
832  {
833  _currentState->rTooHighDegreeConditions().insert( _condition );
834  _condition->rFlag() = true;
835  return;
836  }
837  }
838  // Determine the substitution type: normal or +epsilon
839  bool weakConstraint = (relation == carl::Relation::EQ || relation == carl::Relation::LEQ || relation == carl::Relation::GEQ);
840  Substitution::Type subType = weakConstraint ? Substitution::NORMAL : Substitution::PLUS_EPSILON;
841  std::vector< Poly > factors = std::vector< Poly >();
842  ConstraintsT sideConditions;
843  if( Settings::elimination_with_factorization && !carl::is_trivial(constraint.lhs_factorization()))
844  {
845  auto& factorization = constraint.lhs_factorization();
846  for( auto iter = factorization.begin(); iter != factorization.end(); ++iter )
847  {
848  if( carl::variables(iter->first).has( _eliminationVar ) )
849  factors.push_back( iter->first );
850  else
851  {
852  ConstraintT cons = ConstraintT( iter->first, carl::Relation::NEQ );
853  if( cons != ConstraintT( true ) )
854  {
855  assert( cons != ConstraintT( false ) );
856  sideConditions.insert( cons );
857  }
858  }
859  }
860  }
861  else
862  factors.push_back( constraint.lhs() );
863  for( auto factor = factors.begin(); factor != factors.end(); ++factor )
864  {
865  #ifdef VS_DEBUG
866  std::cout << "Eliminate for " << *factor << std::endl;
867  #endif
868  auto varInfo = carl::var_info(*factor, _eliminationVar, true);
869  const auto& coeffs = varInfo.coeffs();
870  assert( !coeffs.empty() );
871  // Generate test candidates for the chosen variable considering the chosen constraint.
872  switch( coeffs.rbegin()->first )
873  {
874  case 0:
875  {
876  assert( false );
877  break;
878  }
879  //degree = 1
880  case 1:
881  {
882  Poly constantCoeff;
883  auto iter = coeffs.find( 0 );
884  if( iter != coeffs.end() ) constantCoeff = iter->second;
885  // Create state ({b!=0} + oldConditions, [x -> -c/b]):
886  ConstraintT cons = ConstraintT( coeffs.rbegin()->second, carl::Relation::NEQ );
887  if( cons == ConstraintT( false ) )
888  {
889  if( relation == carl::Relation::EQ )
890  generatedTestCandidateBeingASolution = sideConditions.empty();
891  }
892  else
893  {
894  ConstraintsT sideCond = sideConditions;
895  if( cons != ConstraintT( true ) )
896  sideCond.insert( cons );
897  SqrtEx sqEx = SqrtEx( -constantCoeff, Poly(0), coeffs.rbegin()->second, Poly(0) );
898  Substitution sub = Substitution( _eliminationVar, sqEx, subType, carl::PointerSet<vs::Condition>(oConditions), std::move(sideCond) );
899  std::vector<State*> addedChildren = _currentState->addChild( sub );
900  if( !addedChildren.empty() )
901  {
902  if( relation == carl::Relation::EQ && !_currentState->children().back()->hasSubstitutionResults() )
903  {
904  _currentState->rChildren().back()->setOriginalCondition( _condition );
905  generatedTestCandidateBeingASolution = true;
906  }
907  // Add its valuation to the current ranking.
908  while( !addedChildren.empty() )
909  {
910  addStatesToRanking( addedChildren.back() );
911  addedChildren.pop_back();
912  }
913  ++numberOfAddedChildren;
914  #ifdef VS_DEBUG
915  (*(*_currentState).rChildren().back()).print( " ", std::cout );
916  #endif
917  }
918  }
919  break;
920  }
921  //degree = 2
922  case 2:
923  {
924  Poly constantCoeff;
925  auto iter = coeffs.find( 0 );
926  if( iter != coeffs.end() ) constantCoeff = iter->second;
927  Poly linearCoeff;
928  iter = coeffs.find( 1 );
929  if( iter != coeffs.end() ) linearCoeff = iter->second;
930  Poly radicand = carl::pow(linearCoeff, 2) - Rational( 4 ) * coeffs.rbegin()->second * constantCoeff;
931  bool constraintHasZeros = false;
932  ConstraintT cons11 = ConstraintT( coeffs.rbegin()->second, carl::Relation::EQ );
933  if( cons11 != ConstraintT( false ) )
934  {
935  // Create state ({a==0, b!=0} + oldConditions, [x -> -c/b]):
936  ConstraintT cons12 = ConstraintT( linearCoeff, carl::Relation::NEQ );
937  if( cons12 != ConstraintT( false ) )
938  {
939  ConstraintsT sideCond = sideConditions;
940  if( cons11 != ConstraintT( true ) )
941  sideCond.insert( cons11 );
942  if( cons12 != ConstraintT( true ) )
943  sideCond.insert( cons12 );
944  SqrtEx sqEx = SqrtEx( -constantCoeff, Poly(0), linearCoeff, Poly(0) );
945  Substitution sub = Substitution( _eliminationVar, sqEx, subType, carl::PointerSet<vs::Condition>(oConditions), std::move(sideCond) );
946  std::vector<State*> addedChildren = _currentState->addChild( sub );
947  if( !addedChildren.empty() )
948  {
949  if( relation == carl::Relation::EQ && !_currentState->children().back()->hasSubstitutionResults() )
950  {
951  _currentState->rChildren().back()->setOriginalCondition( _condition );
952  generatedTestCandidateBeingASolution = true;
953  }
954  // Add its valuation to the current ranking.
955  while( !addedChildren.empty() )
956  {
957  addStatesToRanking( addedChildren.back() );
958  addedChildren.pop_back();
959  }
960  ++numberOfAddedChildren;
961  #ifdef VS_DEBUG
962  (*(*_currentState).rChildren().back()).print( " ", std::cout );
963  #endif
964  }
965  constraintHasZeros = true;
966  }
967  }
968  ConstraintT cons21 = ConstraintT( radicand, carl::Relation::GEQ );
969  if( cons21 != ConstraintT( false ) )
970  {
971  ConstraintT cons22 = ConstraintT( coeffs.rbegin()->second, carl::Relation::NEQ );
972  if( cons22 != ConstraintT( false ) )
973  {
974  ConstraintsT sideCond = sideConditions;
975  if( cons21 != ConstraintT( true ) )
976  sideCond.insert( cons21 );
977  if( cons22 != ConstraintT( true ) )
978  sideCond.insert( cons22 );
979  // Create state ({a!=0, b^2-4ac>=0} + oldConditions, [x -> (-b-sqrt(b^2-4ac))/2a]):
980  SqrtEx sqExA = SqrtEx( -linearCoeff, Poly(-1), Rational( 2 ) * coeffs.rbegin()->second, radicand );
981  Substitution subA = Substitution( _eliminationVar, sqExA, subType, carl::PointerSet<vs::Condition>(oConditions), ConstraintsT(sideCond) );
982  std::vector<State*> addedChildrenA = _currentState->addChild( subA );
983  if( !addedChildrenA.empty() )
984  {
985  if( relation == carl::Relation::EQ && !_currentState->children().back()->hasSubstitutionResults() )
986  {
987  _currentState->rChildren().back()->setOriginalCondition( _condition );
988  generatedTestCandidateBeingASolution = true;
989  }
990  // Add its valuation to the current ranking.
991  while( !addedChildrenA.empty() )
992  {
993  addStatesToRanking( addedChildrenA.back() );
994  addedChildrenA.pop_back();
995  }
996  ++numberOfAddedChildren;
997  #ifdef VS_DEBUG
998  (*(*_currentState).rChildren().back()).print( " ", std::cout );
999  #endif
1000  }
1001  // Create state ({a!=0, b^2-4ac>=0} + oldConditions, [x -> (-b+sqrt(b^2-4ac))/2a]):
1002  SqrtEx sqExB = SqrtEx( -linearCoeff, Poly(1), Rational( 2 ) * coeffs.rbegin()->second, radicand );
1003  Substitution subB = Substitution( _eliminationVar, sqExB, subType, carl::PointerSet<vs::Condition>(oConditions), std::move(sideCond) );
1004  std::vector<State*> addedChildrenB = _currentState->addChild( subB );
1005  if( !addedChildrenB.empty() )
1006  {
1007  if( relation == carl::Relation::EQ && !_currentState->children().back()->hasSubstitutionResults() )
1008  {
1009  _currentState->rChildren().back()->setOriginalCondition( _condition );
1010  generatedTestCandidateBeingASolution = true;
1011  }
1012  // Add its valuation to the current ranking.
1013  while( !addedChildrenB.empty() )
1014  {
1015  addStatesToRanking( addedChildrenB.back() );
1016  addedChildrenB.pop_back();
1017  }
1018  ++numberOfAddedChildren;
1019  #ifdef VS_DEBUG
1020  (*(*_currentState).rChildren().back()).print( " ", std::cout );
1021  #endif
1022  }
1023  constraintHasZeros = true;
1024  }
1025  }
1026  if( !constraintHasZeros && relation == carl::Relation::EQ )
1027  generatedTestCandidateBeingASolution = sideConditions.empty();
1028  break;
1029  }
1030  //degree > 2 (> 3)
1031  default:
1032  {
1033  _currentState->rTooHighDegreeConditions().insert( _condition );
1034  break;
1035  }
1036  }
1037  }
1038  }
1039  if( !generatedTestCandidateBeingASolution && !_currentState->isInconsistent() )
1040 // if( _eliminationVar.type() != carl::VariableType::VT_INT && !generatedTestCandidateBeingASolution && !_currentState->isInconsistent() )
1041  {
1042  // Create state ( Conditions, [x -> -infinity]):
1043  Substitution sub = Substitution( _eliminationVar, Substitution::MINUS_INFINITY, carl::PointerSet<vs::Condition>(oConditions) );
1044  std::vector<State*> addedChildren = _currentState->addChild( sub );
1045  if( !addedChildren.empty() )
1046  {
1047  // Add its valuation to the current ranking.
1048  while( !addedChildren.empty() )
1049  {
1050  addStatesToRanking( addedChildren.back() );
1051  addedChildren.pop_back();
1052  }
1053  numberOfAddedChildren++;
1054  #ifdef VS_DEBUG
1055  (*(*_currentState).rChildren().back()).print( " ", std::cout );
1056  #endif
1057  }
1058  }
1059 // if( _eliminationVar.type() == carl::VariableType::VT_INT )
1060 // {
1061 // if( !generatedTestCandidateBeingASolution && !_currentState->isInconsistent() )
1062 // {
1063 // // Create state ( Conditions, [x -> -infinity]):
1064 // Substitution sub = Substitution( _eliminationVar, Substitution::PLUS_INFINITY, carl::PointerSet<vs::Condition>(oConditions) );
1065 // std::vector<State*> addedChildren = _currentState->addChild( sub );
1066 // if( !addedChildren.empty() )
1067 // {
1068 // // Add its valuation to the current ranking.
1069 // while( !addedChildren.empty() )
1070 // {
1071 // addStatesToRanking( addedChildren.back() );
1072 // addedChildren.pop_back();
1073 // }
1074 // numberOfAddedChildren++;
1075 // #ifdef VS_DEBUG
1076 // (*(*_currentState).rChildren().back()).print( " ", std::cout );
1077 // #endif
1078 // }
1079 // }
1080 // }
1081  if( generatedTestCandidateBeingASolution )
1082  {
1083  _currentState->rTooHighDegreeConditions().clear();
1084  for( auto cond = _currentState->rConditions().begin(); cond != _currentState->conditions().end(); ++cond )
1085  (**cond).rFlag() = true;
1086  assert( numberOfAddedChildren <= _currentState->children().size() );
1087  while( _currentState->children().size() > numberOfAddedChildren )
1088  {
1089  State* toDelete = *_currentState->rChildren().begin();
1090  removeStatesFromRanking( *toDelete );
1091  _currentState->resetConflictSets();
1092  _currentState->rChildren().erase( _currentState->rChildren().begin() );
1093  _currentState->resetInfinityChild( toDelete );
1094  delete toDelete; // DELETE STATE
1095  }
1096  _currentState->updateIntTestCandidates();
1097  if( numberOfAddedChildren == 0 )
1098  {
1099  ConditionSetSet conflictSet;
1100  carl::PointerSet<vs::Condition> condSet;
1101  condSet.insert( _condition );
1102  conflictSet.insert( condSet );
1103  _currentState->addConflicts( NULL, std::move(conflictSet) );
1104  _currentState->rInconsistent() = true;
1105  }
1106  }
1107  else
1108  (*_condition).rFlag() = true;
1109  addStateToRanking( _currentState );
1110  }
1111 
1112  template<class Settings>
1113  bool VSModule<Settings>::substituteAll( State* _currentState, ConditionList& _conditions )
1114  {
1115  /*
1116  * Create a vector to store the results of each single substitution. Each entry corresponds to
1117  * the results of a single substitution. These results can be considered as a disjunction of
1118  * conjunctions of constraints.
1119  */
1120  std::vector<DisjunctionOfConditionConjunctions> allSubResults;
1121  // The substitution to apply.
1122  assert( !_currentState->isRoot() );
1123  const Substitution& currentSubs = _currentState->substitution();
1124  // The variable to substitute.
1125  const carl::Variable& substitutionVariable = currentSubs.variable();
1126  // The conditions of the currently considered state, without the one getting just eliminated.
1127  ConditionList oldConditions;
1128  bool anySubstitutionFailed = false;
1129  bool allSubstitutionsApplied = true;
1130  ConditionSetSet conflictSet;
1131  EvalDoubleIntervalMap solBox = Settings::use_variable_bounds ? _currentState->father().variableBounds().getIntervalMap() : EvalDoubleIntervalMap();
1132  // Apply the substitution to the given conditions.
1133  for( auto cond = _conditions.begin(); cond != _conditions.end(); ++cond )
1134  {
1135  // The constraint to substitute in.
1136  const ConstraintT& currentConstraint = (**cond).constraint();
1137  // Does the condition contain the variable to substitute.
1138  //auto var = currentConstraint.variables().find( substitutionVariable );
1139  if( !currentConstraint.variables().has( substitutionVariable ) )
1140  {
1141  if( !anySubstitutionFailed )
1142  {
1143  oldConditions.push_back( new vs::Condition( currentConstraint, mpConditionIdAllocator->get(), (**cond).valuation() ) );
1144  oldConditions.back()->pOriginalConditions()->insert( *cond );
1145  }
1146  }
1147  else
1148  {
1149  DisjunctionOfConstraintConjunctions subResult;
1150  carl::Variables conflVars;
1151  bool substitutionCouldBeApplied = substitute( currentConstraint, currentSubs, subResult, Settings::virtual_substitution_according_paper, conflVars, solBox );
1152  allSubstitutionsApplied &= substitutionCouldBeApplied;
1153  // Create the the conditions according to the just created constraint prototypes.
1154  if( substitutionCouldBeApplied && subResult.empty() )
1155  {
1156  anySubstitutionFailed = true;
1157  carl::PointerSet<vs::Condition> condSet;
1158  condSet.insert( *cond );
1159  if( _currentState->pOriginalCondition() != NULL )
1160  condSet.insert( _currentState->pOriginalCondition() );
1161  if( Settings::use_variable_bounds )
1162  {
1163  auto conflictingBounds = _currentState->father().variableBounds().getOriginsOfBounds( conflVars );
1164  condSet.insert( conflictingBounds.begin(), conflictingBounds.end() );
1165  }
1166  conflictSet.insert( condSet );
1167  }
1168  else
1169  {
1170  if( allSubstitutionsApplied && !anySubstitutionFailed )
1171  {
1172  allSubResults.emplace_back();
1173  DisjunctionOfConditionConjunctions& currentDisjunction = allSubResults.back();
1174  for( auto consConj = subResult.begin(); consConj != subResult.end(); ++consConj )
1175  {
1176  currentDisjunction.emplace_back();
1177  ConditionList& currentConjunction = currentDisjunction.back();
1178  for( auto cons = consConj->begin(); cons != consConj->end(); ++cons )
1179  {
1180  currentConjunction.push_back( new vs::Condition( *cons, mpConditionIdAllocator->get(), _currentState->treeDepth() ) );
1181  currentConjunction.back()->pOriginalConditions()->insert( *cond );
1182  }
1183  }
1184  }
1185  }
1186  }
1187  }
1188  bool cleanResultsOfThisMethod = false;
1189  if( anySubstitutionFailed )
1190  {
1191  _currentState->rFather().addConflicts( _currentState->pSubstitution(), std::move(conflictSet) );
1192  _currentState->rInconsistent() = true;
1193  while( !_currentState->rConflictSets().empty() )
1194  {
1195  const Substitution* sub = _currentState->rConflictSets().begin()->first;
1196  _currentState->rConflictSets().erase( _currentState->rConflictSets().begin() );
1197  if( sub != NULL && sub->type() == Substitution::Type::INVALID )
1198  {
1199  delete sub;
1200  }
1201  }
1202  while( !_currentState->children().empty() )
1203  {
1204  State* toDelete = _currentState->rChildren().back();
1205  removeStatesFromRanking( *toDelete );
1206  _currentState->rChildren().pop_back();
1207  _currentState->resetInfinityChild( toDelete );
1208  delete toDelete; // DELETE STATE
1209  }
1210  _currentState->updateIntTestCandidates();
1211  while( !_currentState->conditions().empty() )
1212  {
1213  const vs::Condition* pCond = _currentState->rConditions().back();
1214  _currentState->rConditions().pop_back();
1215  if( Settings::use_variable_bounds )
1216  _currentState->rVariableBounds().removeBound( pCond->constraint(), pCond );
1217  mpConditionIdAllocator->free( pCond->id() );
1218  delete pCond;
1219  pCond = NULL;
1220  }
1221  cleanResultsOfThisMethod = true;
1222  }
1223  else
1224  {
1225  if( !_currentState->isInconsistent() )
1226  {
1227  if( allSubstitutionsApplied )
1228  {
1229  removeStatesFromRanking( *_currentState );
1230  allSubResults.emplace_back();
1231  allSubResults.back().push_back( oldConditions );
1232  _currentState->addSubstitutionResults( std::move(allSubResults) );
1233  #ifdef VS_MODULE_VERBOSE_INTEGERS
1234  _currentState->printSubstitutionResults( std::string( _currentState->treeDepth()*3, ' '), std::cout );
1235  #endif
1236  addStatesToRanking( _currentState );
1237  }
1238  else
1239  {
1240  removeStatesFromRanking( _currentState->rFather() );
1241  _currentState->resetConflictSets();
1242  while( !_currentState->children().empty() )
1243  {
1244  State* toDelete = _currentState->rChildren().back();
1245  _currentState->rChildren().pop_back();
1246  _currentState->resetInfinityChild( toDelete );
1247  delete toDelete; // DELETE STATE
1248  }
1249  _currentState->updateIntTestCandidates();
1250  while( !_currentState->conditions().empty() )
1251  {
1252  const vs::Condition* pCond = _currentState->rConditions().back();
1253  _currentState->rConditions().pop_back();
1254  if( Settings::use_variable_bounds )
1255  _currentState->rVariableBounds().removeBound( pCond->constraint(), pCond );
1256  mpConditionIdAllocator->free( pCond->id() );
1257  delete pCond;
1258  pCond = NULL;
1259  }
1260  _currentState->rMarkedAsDeleted() = true;
1261  _currentState->rFather().rCannotBeSolved() = true;
1262  addStatesToRanking( _currentState->pFather() );
1263  cleanResultsOfThisMethod = true;
1264  }
1265  }
1266  #ifdef VS_DEBUG
1267  _currentState->print( " ", std::cout );
1268  #endif
1269  }
1270  if( cleanResultsOfThisMethod )
1271  {
1272  while( !oldConditions.empty() )
1273  {
1274  const vs::Condition* rpCond = oldConditions.back();
1275  oldConditions.pop_back();
1276  mpConditionIdAllocator->free( rpCond->id() );
1277  delete rpCond;
1278  rpCond = NULL;
1279  }
1280  while( !allSubResults.empty() )
1281  {
1282  while( !allSubResults.back().empty() )
1283  {
1284  while( !allSubResults.back().back().empty() )
1285  {
1286  const vs::Condition* rpCond = allSubResults.back().back().back();
1287  allSubResults.back().back().pop_back();
1288  mpConditionIdAllocator->free( rpCond->id() );
1289  delete rpCond;
1290  rpCond = NULL;
1291  }
1292  allSubResults.back().pop_back();
1293  }
1294  allSubResults.pop_back();
1295  }
1296  }
1297  return !anySubstitutionFailed;
1298  }
1299 
1300  namespace vsmodulehelper {
1301  /**
1302  * @param _var The variable to check the size of its solution set for.
1303  * @return true, if it is easy to decide whether this constraint has a finite solution set
1304  * in the given variable;
1305  * false, otherwise.
1306  */
1307  bool hasFinitelyManySolutionsIn(const ConstraintT& constr, const carl::Variable& _var) {
1308  if (constr.variables().has(_var))
1309  return true;
1310  if (constr.relation() == carl::Relation::EQ) {
1311  if (constr.variables().size() == 1)
1312  return true;
1313  }
1314  return false;
1315  }
1316  }
1317 
1318  template<class Settings>
1319  void VSModule<Settings>::propagateNewConditions( State* _currentState )
1320  {
1321 
1322  removeStatesFromRanking( *_currentState );
1323  // Collect the recently added conditions and mark them as not recently added.
1324  bool deleteExistingTestCandidates = false;
1325  ConditionList recentlyAddedConditions;
1326  for( auto cond = _currentState->rConditions().begin(); cond != _currentState->conditions().end(); ++cond )
1327  {
1328  if( (**cond).recentlyAdded() )
1329  {
1330  (**cond).rRecentlyAdded() = false;
1331  recentlyAddedConditions.push_back( *cond );
1332  if( _currentState->pOriginalCondition() == NULL )
1333  {
1334  bool onlyTestCandidateToConsider = false;
1335  if( _currentState->index() != carl::Variable::NO_VARIABLE ) // TODO: Maybe only if the degree is not to high
1336  onlyTestCandidateToConsider = vsmodulehelper::hasFinitelyManySolutionsIn((**cond).constraint(), _currentState->index() );
1337  if( onlyTestCandidateToConsider )
1338  deleteExistingTestCandidates = true;
1339  }
1340  }
1341  }
1342  addStateToRanking( _currentState );
1343  if( !_currentState->children().empty() )
1344  {
1345  if( deleteExistingTestCandidates || _currentState->initIndex( mAllVariables, VariableValuationStrategy::OPTIMIZE_BEST, Settings::prefer_equation_over_all, false, Settings::use_fixed_variable_order ) )
1346  {
1347  _currentState->initConditionFlags();
1348  // If the recently added conditions make another variable being the best to eliminate next delete all children.
1349  _currentState->resetConflictSets();
1350  while( !_currentState->children().empty() )
1351  {
1352  State* toDelete = _currentState->rChildren().back();
1353  _currentState->rChildren().pop_back();
1354  _currentState->resetInfinityChild( toDelete );
1355  delete toDelete; // DELETE STATE
1356  }
1357  _currentState->updateIntTestCandidates();
1358  }
1359  else
1360  {
1361  bool newTestCandidatesGenerated = false;
1362  if( _currentState->pOriginalCondition() == NULL )
1363  {
1364  /*
1365  * Check if there are new conditions in this state, which would have been better choices
1366  * to generate test candidates than those conditions of the already generated test
1367  * candidates. If so, generate the test candidates of the better conditions.
1368  */
1369  for( auto cond = recentlyAddedConditions.begin(); cond != recentlyAddedConditions.end(); ++cond )
1370  {
1371  if( _currentState->index() != carl::Variable::NO_VARIABLE && (**cond).constraint().variables().has( _currentState->index() ) )
1372  {
1373  bool worseConditionFound = false;
1374  auto child = _currentState->rChildren().begin();
1375  while( child != _currentState->children().end() )
1376  {
1377  if( (**child).substitution().type() != Substitution::MINUS_INFINITY || (**child).substitution().type() != Substitution::PLUS_INFINITY)
1378  {
1379  auto oCond = (**child).rSubstitution().rOriginalConditions().begin();
1380  while( !worseConditionFound && oCond != (**child).substitution().originalConditions().end() )
1381  {
1382  if( (**cond).valuate( _currentState->index(), mAllVariables.size(), Settings::prefer_equation_over_all ) > (**oCond).valuate( _currentState->index(), mAllVariables.size(), Settings::prefer_equation_over_all ) )
1383  {
1384  newTestCandidatesGenerated = true;
1385  #ifdef VS_DEBUG
1386  std::cout << "*** Eliminate " << _currentState->index() << " in ";
1387  std::cout << (**cond).constraint();
1388  std::cout << " creates:" << std::endl;
1389  #endif
1390  eliminate( _currentState, _currentState->index(), *cond );
1391  #ifdef VS_DEBUG
1392  std::cout << "*** Eliminate ready." << std::endl;
1393  #endif
1394  worseConditionFound = true;
1395  break;
1396  }
1397  ++oCond;
1398  }
1399  if( worseConditionFound )
1400  break;
1401  }
1402  ++child;
1403  }
1404  }
1405  }
1406  }
1407  // Otherwise, add the recently added conditions to each child of the considered state to
1408  // which a substitution must be or already has been applied.
1409  for( auto child = _currentState->rChildren().begin(); child != _currentState->children().end(); ++child )
1410  {
1411  if( (**child).type() != State::SUBSTITUTION_TO_APPLY || (**child).isInconsistent() )
1412  {
1413  // Apply substitution to new conditions and add the result to the substitution result vector.
1414  if( !substituteAll( *child, recentlyAddedConditions ) )
1415  {
1416  // Delete the currently considered state.
1417  assert( (*child)->rInconsistent() );
1418  assert( (**child).conflictSets().empty() );
1419  removeStateFromRanking( **child );
1420  }
1421  else if( (**child).isInconsistent() && !(**child).subResultsSimplified() && !(**child).conflictSets().empty() )
1422  {
1423  addStateToRanking( *child );
1424  }
1425  }
1426  else
1427  {
1428  if( newTestCandidatesGenerated )
1429  {
1430  if( !(**child).children().empty() )
1431  {
1432  (**child).rHasChildrenToInsert() = true;
1433  }
1434  }
1435  else
1436  {
1437  addStatesToRanking( *child );
1438  }
1439  }
1440  }
1441  }
1442  }
1443  _currentState->rHasRecentlyAddedConditions() = false;
1444  }
1445 
1446  template<class Settings>
1447  void VSModule<Settings>::addStateToRanking( State* _state )
1448  {
1449  if( !_state->markedAsDeleted()
1450  && !(_state->isInconsistent() && _state->conflictSets().empty() && _state->conditionsSimplified()))
1451  {
1452  if( _state->id() != 0 )
1453  {
1454  size_t id = _state->id();
1455  removeStateFromRanking( *_state );
1456  _state->rID()= id;
1457  }
1458  else
1459  {
1460  increaseIDCounter();
1461  _state->rID() = mIDCounter;
1462  }
1463  _state->updateValuation( mLazyMode );
1464  UnsignedTriple key = UnsignedTriple( _state->valuation(), std::pair< size_t, size_t> ( _state->id(), _state->backendCallValuation() ) );
1465  if( (mRanking.insert( ValStatePair( key, _state ) )).second == false )
1466  {
1467  std::cout << "Warning: Could not insert. Entry already exists.";
1468  std::cout << std::endl;
1469  }
1470  }
1471  }
1472 
1473  template<class Settings>
1474  void VSModule<Settings>::addStatesToRanking( State* _state )
1475  {
1476  addStateToRanking( _state );
1477  if( _state->conditionsSimplified() && _state->subResultsSimplified() && !_state->takeSubResultCombAgain() && !_state->hasRecentlyAddedConditions() )
1478  for( auto dt = (*_state).rChildren().begin(); dt != (*_state).children().end(); ++dt )
1479  addStatesToRanking( *dt );
1480  }
1481 
1482  template<class Settings>
1483  void VSModule<Settings>::insertTooHighDegreeStatesInRanking( State* _state )
1484  {
1485  if( _state->cannotBeSolved( mLazyMode ) )
1486  addStateToRanking( _state );
1487  else
1488  for( auto dt = (*_state).rChildren().begin(); dt != (*_state).children().end(); ++dt )
1489  insertTooHighDegreeStatesInRanking( *dt );
1490  }
1491 
1492  template<class Settings>
1493  bool VSModule<Settings>::removeStateFromRanking( State& _state )
1494  {
1495  UnsignedTriple key = UnsignedTriple( _state.valuation(), std::pair< unsigned, unsigned> ( _state.id(), _state.backendCallValuation() ) );
1496  auto valDTPair = mRanking.find( key );
1497  if( valDTPair != mRanking.end() )
1498  {
1499  mRanking.erase( valDTPair );
1500  _state.rID() = 0;
1501  return true;
1502  }
1503  else
1504  return false;
1505  }
1506 
1507  template<class Settings>
1508  void VSModule<Settings>::removeStatesFromRanking( State& _state )
1509  {
1510  removeStateFromRanking( _state );
1511  for( auto dt = _state.rChildren().begin(); dt != _state.children().end(); ++dt )
1512  removeStatesFromRanking( **dt );
1513  }
1514 
1515  template<class Settings>
1516  bool VSModule<Settings>::checkRanking() const
1517  {
1518  for( auto valDTPair = mRanking.begin(); valDTPair != mRanking.end(); ++valDTPair )
1519  {
1520  if( !mpStateTree->containsState( valDTPair->second ) )
1521  return false;
1522  }
1523  return true;
1524  }
1525 
1526  template<class Settings>
1527  FormulaSetT VSModule<Settings>::getReasons( const carl::PointerSet<vs::Condition>& _conditions ) const
1528  {
1529  FormulaSetT result;
1530  if( _conditions.empty() ) return result;
1531  // Get the original conditions of the root of the root state leading to the given set of conditions.
1532  carl::PointerSet<vs::Condition> conds = _conditions;
1533  carl::PointerSet<vs::Condition> oConds;
1534  while( !(*conds.begin())->originalConditions().empty() )
1535  {
1536  for( auto cond = conds.begin(); cond != conds.end(); ++cond )
1537  {
1538  assert( !(*cond)->originalConditions().empty() );
1539  oConds.insert( (*cond)->originalConditions().begin(), (*cond)->originalConditions().end() );
1540  }
1541  conds.clear();
1542  conds.swap( oConds );
1543  }
1544  // Get the sub-formulas in the received formula corresponding to these original conditions.
1545  for( auto oCond = conds.begin(); oCond != conds.end(); ++oCond )
1546  {
1547  assert( (*oCond)->originalConditions().empty() );
1548  auto receivedConstraint = rReceivedFormula().begin();
1549  while( receivedConstraint != rReceivedFormula().end() )
1550  {
1551  if( receivedConstraint->formula().type() == carl::FormulaType::CONSTRAINT )
1552  {
1553  if( (**oCond).constraint() == receivedConstraint->formula().constraint() )
1554  break;
1555  }
1556  else if( receivedConstraint->formula().type() == carl::FormulaType::NOT && receivedConstraint->formula().subformula().type() == carl::FormulaType::CONSTRAINT )
1557  {
1558  ConstraintT recConstraint = receivedConstraint->formula().subformula().constraint();
1559  if( (**oCond).constraint() == ConstraintT( recConstraint.lhs(), carl::inverse( recConstraint.relation() ) ) )
1560  break;
1561  }
1562  ++receivedConstraint;
1563  }
1564  assert( receivedConstraint != rReceivedFormula().end() );
1565  result.insert( receivedConstraint->formula() );
1566  }
1567  return result;
1568  }
1569 
1570  template<class Settings>
1571  std::vector<FormulaT> VSModule<Settings>::getReasonsAsVector( const carl::PointerSet<vs::Condition>& _conditions ) const
1572  {
1573  std::vector<FormulaT> result;
1574  if( _conditions.empty() ) return result;
1575  // Get the original conditions of the root of the root state leading to the given set of conditions.
1576  carl::PointerSet<vs::Condition> conds = _conditions;
1577  carl::PointerSet<vs::Condition> oConds;
1578  while( !(*conds.begin())->originalConditions().empty() )
1579  {
1580  for( auto cond = conds.begin(); cond != conds.end(); ++cond )
1581  {
1582  assert( !(*cond)->originalConditions().empty() );
1583  oConds.insert( (*cond)->originalConditions().begin(), (*cond)->originalConditions().end() );
1584  }
1585  conds.clear();
1586  conds.swap( oConds );
1587  }
1588  // Get the sub-formulas in the received formula corresponding to these original conditions.
1589  for( auto oCond = conds.begin(); oCond != conds.end(); ++oCond )
1590  {
1591  assert( (*oCond)->originalConditions().empty() );
1592  auto receivedConstraint = rReceivedFormula().begin();
1593  while( receivedConstraint != rReceivedFormula().end() )
1594  {
1595  if( receivedConstraint->formula().type() == carl::FormulaType::CONSTRAINT )
1596  {
1597  if( (**oCond).constraint() == receivedConstraint->formula().constraint() )
1598  break;
1599  }
1600  else if( receivedConstraint->formula().type() == carl::FormulaType::NOT && receivedConstraint->formula().subformula().type() == carl::FormulaType::CONSTRAINT )
1601  {
1602  ConstraintT recConstraint = receivedConstraint->formula().subformula().constraint();
1603  if( (**oCond).constraint() == ConstraintT( recConstraint.lhs(), carl::inverse( recConstraint.relation() ) ) )
1604  break;
1605  }
1606  ++receivedConstraint;
1607  }
1608  assert( receivedConstraint != rReceivedFormula().end() );
1609  result.push_back( receivedConstraint->formula() );
1610  }
1611  return result;
1612  }
1613 
1614  template<class Settings>
1615  void VSModule<Settings>::updateInfeasibleSubset( bool _includeInconsistentTestCandidates )
1616  {
1617  if( !Settings::infeasible_subset_generation )
1618  {
1619  // Set the infeasible subset to the set of all received constraints.
1620  mInfeasibleSubsets.emplace_back();
1621  for( auto cons = rReceivedFormula().begin(); cons != rReceivedFormula().end(); ++cons )
1622  mInfeasibleSubsets.back().insert( cons->formula() );
1623  #ifdef SMTRAT_DEVOPTION_Statistics
1624  mStatistics.addConflict( rReceivedFormula(), mInfeasibleSubsets );
1625  #endif
1626  return;
1627  }
1628  // Determine the minimum covering sets of the conflict sets, i.e. the infeasible subsets of the root.
1629  ConditionSetSet minCoverSets;
1630  ConditionSetSetSet confSets;
1631  State::ConflictSets::iterator nullConfSet = mpStateTree->rConflictSets().find( NULL );
1632  if( nullConfSet != mpStateTree->rConflictSets().end() && !_includeInconsistentTestCandidates )
1633  confSets.insert( nullConfSet->second.begin(), nullConfSet->second.end() );
1634  else
1635  for( auto confSet = mpStateTree->rConflictSets().begin(); confSet != mpStateTree->rConflictSets().end(); ++confSet )
1636  confSets.insert( confSet->second.begin(), confSet->second.end() );
1637  allMinimumCoveringSets( confSets, minCoverSets );
1638  assert( !minCoverSets.empty() );
1639  // Change the globally stored infeasible subset to the smaller one.
1640  mInfeasibleSubsets.clear();
1641  for( auto minCoverSet = minCoverSets.begin(); minCoverSet != minCoverSets.end(); ++minCoverSet )
1642  {
1643  assert( !minCoverSet->empty() );
1644  mInfeasibleSubsets.push_back( getReasons( *minCoverSet ) );
1645  // TODO: Avoid adding multiple identical infeasible subsets.
1646  // The following input triggers the creation of seven identical infeasible subsets.
1647  // (x <= 0) and !(x < 0) and !(x = 0)
1648  break;
1649  }
1650  assert( !mInfeasibleSubsets.empty() );
1651  assert( !mInfeasibleSubsets.back().empty() );
1652  #ifdef SMTRAT_DEVOPTION_Statistics
1653  mStatistics.addConflict( rReceivedFormula(), mInfeasibleSubsets );
1654  #endif
1655  }
1656 
1657  template<class Settings>
1658  bool VSModule<Settings>::solutionInDomain()
1659  {
1660  bool trySplitting = Settings::use_branch_and_bound && (!Settings::only_split_in_final_call || mFinalCheck);
1661  SMTRAT_LOG_DEBUG("smtrat.vs", "Try splitting? " << trySplitting << " (from " << Settings::use_branch_and_bound << " " << Settings::only_split_in_final_call << " " << mFinalCheck << ")");
1662  if( rReceivedFormula().isRealConstraintLiteralConjunction() ) {
1663  SMTRAT_LOG_DEBUG("smtrat.vs", "Everything is real anyway");
1664  return true;
1665  }
1666  assert( solverState() != UNSAT );
1667  if( !mRanking.empty() )
1668  {
1669  SMTRAT_LOG_DEBUG("smtrat.vs", "Ranking is not empty");
1670  std::vector<carl::Variable> varOrder;
1671  State* currentState = mRanking.begin()->second;
1672  RationalAssignment varSolutions;
1673  if( currentState->cannotBeSolved( mLazyMode ) )
1674  {
1675  Model bmodel = backendsModel();
1676  for( auto& ass : bmodel )
1677  {
1678  if( ass.second.isSqrtEx() )
1679  {
1680  assert( ass.second.asSqrtEx().is_constant() && carl::is_integer( ass.second.asSqrtEx().constant_part().constant_part() ) );
1681  varSolutions[ass.first.asVariable()] = ass.second.asSqrtEx().constant_part().constant_part();
1682  }
1683  else if( ass.second.isRAN() )
1684  {
1685  assert( ass.second.asRAN().is_numeric() && carl::is_integer( ass.second.asRAN().value() ) );
1686  varSolutions[ass.first.asVariable()] = ass.second.asRAN().value();
1687  }
1688  }
1689  }
1690  while( !currentState->isRoot() )
1691  {
1692  SMTRAT_LOG_DEBUG("smtrat.vs", "State is not the root");
1693  const carl::Variables& tVars = currentState->substitution().termVariables();
1694  if( currentState->substitution().variable().type() == carl::VariableType::VT_INT )
1695  {
1696  SMTRAT_LOG_DEBUG("smtrat.vs", "This variable is integer");
1697  for( carl::Variable::Arg v : tVars )
1698  varSolutions.insert( std::make_pair( v, Rational(0) ) );
1699 // assert( currentState->substitution().type() != Substitution::MINUS_INFINITY );
1700 // assert( currentState->substitution().type() != Substitution::PLUS_INFINITY );
1701  if( currentState->substitution().type() == Substitution::MINUS_INFINITY || currentState->substitution().type() == Substitution::PLUS_INFINITY )
1702  {
1703  SMTRAT_LOG_DEBUG("smtrat.vs", "substitution is infty");
1704  Rational nextIntTCinRange;
1705  if( currentState->getNextIntTestCandidate( nextIntTCinRange, Settings::int_max_range ) )
1706  {
1707  SMTRAT_LOG_DEBUG("smtrat.vs", "Get next int test candidate");
1708  if( trySplitting )
1709  {
1710  SMTRAT_LOG_DEBUG("smtrat.vs", "Try splitting");
1711  #ifdef SMTRAT_DEVOPTION_Statistics
1712  mStatistics.branch();
1713  #endif
1714  branchAt( currentState->substitution().variable(), nextIntTCinRange, std::move(getReasonsAsVector( currentState->substitution().originalConditions() )) );
1715  }
1716  }
1717  else
1718  {
1719  SMTRAT_LOG_DEBUG("smtrat.vs", "Some else case");
1720  removeStatesFromRanking( *currentState );
1721  currentState->rCannotBeSolved() = true;
1722  addStateToRanking( currentState );
1723  }
1724  return false;
1725  }
1726  else
1727  {
1728  SMTRAT_LOG_DEBUG("smtrat.vs", "substitution is not infty");
1729  assert( currentState->substitution().type() != Substitution::PLUS_EPSILON );
1730  if( trySplitting && Settings::branch_and_bound_at_origin )
1731  {
1732  SMTRAT_LOG_DEBUG("smtrat.vs", "Try splitting for B&B");
1733  RationalAssignment partialVarSolutions;
1734  const Poly& substitutionPoly = (*currentState->substitution().originalConditions().begin())->constraint().lhs();
1735  for( auto var = varOrder.rbegin(); var != varOrder.rend(); ++var )
1736  {
1737  assert( varSolutions.find( *var ) != varSolutions.end() );
1738  partialVarSolutions[*var] = varSolutions[*var];
1739  Poly subPolyPartiallySubstituted = carl::substitute(substitutionPoly, partialVarSolutions );
1740  if( !carl::is_zero(subPolyPartiallySubstituted) )
1741  {
1742  Rational cp = subPolyPartiallySubstituted.coprime_factor_without_constant();
1743  assert( carl::get_num( cp ) == Rational(1) || carl::get_num( cp ) == Rational(-1) );
1744  Rational g = carl::get_denom( cp );
1745  if( g > Rational(0) && carl::mod( carl::to_int<Integer>( subPolyPartiallySubstituted.constant_part() ), carl::to_int<Integer>( g ) ) != 0 )
1746  {
1747  Poly branchEx = (subPolyPartiallySubstituted - subPolyPartiallySubstituted.constant_part()) * cp;
1748  Rational branchValue = subPolyPartiallySubstituted.constant_part() * cp;
1749  if( branchAt( branchEx, true, branchValue, std::move(getReasonsAsVector( currentState->substitution().originalConditions() )) ) )
1750  {
1751  #ifdef SMTRAT_DEVOPTION_Statistics
1752  mStatistics.branch();
1753  #endif
1754  return false;
1755  }
1756  }
1757  }
1758  }
1759  }
1760  // Insert the (integer!) assignments of the other variables.
1761  const SqrtEx& subTerm = currentState->substitution().term();
1762  if( carl::is_zero(carl::substitute(subTerm.denominator(), varSolutions )) )
1763  {
1764  SMTRAT_LOG_DEBUG("smtrat.vs", "Something is zero");
1765  if( mFinalCheck )
1766  splitUnequalConstraint( FormulaT( subTerm.denominator(), carl::Relation::NEQ ) );
1767  return false;
1768  }
1769  auto result = evaluate( subTerm, varSolutions, -1 );
1770  Rational evaluatedSubTerm = result.first;
1771  bool assIsInteger = result.second;
1772  assIsInteger &= carl::is_integer( evaluatedSubTerm );
1773  if( !assIsInteger )
1774  {
1775  SMTRAT_LOG_DEBUG("smtrat.vs", "Assignment is not integer");
1776  if( trySplitting )
1777  {
1778  SMTRAT_LOG_DEBUG("smtrat.vs", "Try to split");
1779  #ifdef SMTRAT_DEVOPTION_Statistics
1780  mStatistics.branch();
1781  #endif
1782  branchAt( currentState->substitution().variable(), evaluatedSubTerm, std::move(getReasonsAsVector( currentState->substitution().originalConditions() )) );
1783  }
1784  return false;
1785  }
1786  assert( varSolutions.find( currentState->substitution().variable() ) == varSolutions.end() );
1787  varSolutions.insert( std::make_pair( currentState->substitution().variable(), evaluatedSubTerm ) );
1788  }
1789  }
1790  varOrder.push_back( currentState->substitution().variable() );
1791  currentState = currentState->pFather();
1792  }
1793  }
1794  return true;
1795  }
1796 
1797  template<class Settings>
1798  void VSModule<Settings>::allMinimumCoveringSets( const ConditionSetSetSet& _conflictSets, ConditionSetSet& _minCovSets )
1799  {
1800  if( !_conflictSets.empty() )
1801  {
1802  // First we construct all possible combinations of combining all single sets of each set of sets.
1803  // Store for each set an iterator.
1804  std::vector<ConditionSetSet::iterator> conditionSetSetIters = std::vector<ConditionSetSet::iterator>();
1805  for( auto conflictSet = _conflictSets.begin(); conflictSet != _conflictSets.end(); ++conflictSet )
1806  {
1807  conditionSetSetIters.push_back( (*conflictSet).begin() );
1808  // Assure, that the set is not empty.
1809  assert( conditionSetSetIters.back() != (*conflictSet).end() );
1810  }
1811  ConditionSetSetSet::iterator conflictSet;
1812  std::vector<ConditionSetSet::iterator>::iterator conditionSet;
1813  // Find all covering sets by forming the union of all combinations.
1814  bool lastCombinationReached = false;
1815  while( !lastCombinationReached )
1816  {
1817  // Create a new combination of vectors.
1818  carl::PointerSet<vs::Condition> coveringSet;
1819  bool previousIteratorIncreased = false;
1820  // For each set of sets in the vector of sets of sets, choose a set in it. We combine
1821  // these sets by forming their union and store it as a covering set.
1822  conditionSet = conditionSetSetIters.begin();
1823  conflictSet = _conflictSets.begin();
1824  while( conditionSet != conditionSetSetIters.end() )
1825  {
1826  if( (*conflictSet).empty() )
1827  {
1828  conflictSet++;
1829  conditionSet++;
1830  }
1831  else
1832  {
1833  coveringSet.insert( (**conditionSet).begin(), (**conditionSet).end() );
1834  // Set the iterator.
1835  if( !previousIteratorIncreased )
1836  {
1837  (*conditionSet)++;
1838  if( *conditionSet != (*conflictSet).end() )
1839  previousIteratorIncreased = true;
1840  else
1841  *conditionSet = (*conflictSet).begin();
1842  }
1843  conflictSet++;
1844  conditionSet++;
1845  if( !previousIteratorIncreased && conditionSet == conditionSetSetIters.end() )
1846  lastCombinationReached = true;
1847  }
1848  }
1849  _minCovSets.insert( coveringSet );
1850  }
1851  /*
1852  * Delete all covering sets, which are not minimal. We benefit of the set of sets property,
1853  * which sorts its sets according to the elements they contain. If a set M is a subset of
1854  * another set M', the position of M in the set of sets is before M'.
1855  */
1856  auto minCoverSet = _minCovSets.begin();
1857  auto coverSet = _minCovSets.begin();
1858  coverSet++;
1859  while( coverSet != _minCovSets.end() )
1860  {
1861  auto cond1 = (*minCoverSet).begin();
1862  auto cond2 = (*coverSet).begin();
1863  while( cond1 != (*minCoverSet).end() && cond2 != (*coverSet).end() )
1864  {
1865  if( *cond1 != *cond2 )
1866  break;
1867  cond1++;
1868  cond2++;
1869  }
1870  if( cond1 == (*minCoverSet).end() )
1871  _minCovSets.erase( coverSet++ );
1872  else
1873  {
1874  minCoverSet = coverSet;
1875  coverSet++;
1876  }
1877  }
1878  }
1879  }
1880 
1881  template<class Settings>
1882  bool VSModule<Settings>::adaptPassedFormula( const State& _state, FormulaConditionMap& _formulaCondMap )
1883  {
1884  if( _state.conditions().empty() ) return false;
1885  bool changedPassedFormula = false;
1886  // Collect the constraints to check.
1887  std::map<ConstraintT,const vs::Condition*> constraintsToCheck;
1888  for( auto cond = _state.conditions().begin(); cond != _state.conditions().end(); ++cond )
1889  {
1890  // Optimization: If the zeros of the polynomial in a weak inequality have already been checked pass the strict version.
1891  if( Settings::make_constraints_strict_for_backend && _state.allTestCandidatesInvalidated( *cond ) )
1892  {
1893  const ConstraintT& constraint = (*cond)->constraint();
1894  switch( constraint.relation() )
1895  {
1896  case carl::Relation::GEQ:
1897  {
1898  ConstraintT strictVersion = ConstraintT( constraint.lhs(), carl::Relation::GREATER );
1899  constraintsToCheck.insert( std::pair< ConstraintT, const vs::Condition*>( strictVersion, *cond ) );
1900  break;
1901  }
1902  case carl::Relation::LEQ:
1903  {
1904  ConstraintT strictVersion = ConstraintT( constraint.lhs(), carl::Relation::LESS );
1905  constraintsToCheck.insert( std::pair< ConstraintT, const vs::Condition*>( strictVersion, *cond ) );
1906  break;
1907  }
1908  default:
1909  {
1910  constraintsToCheck.insert( std::pair< ConstraintT, const vs::Condition*>( constraint, *cond ) );
1911  }
1912  }
1913  }
1914  else
1915  constraintsToCheck.insert( std::pair< ConstraintT, const vs::Condition*>( (*cond)->constraint(), *cond ) );
1916  }
1917  /*
1918  * Remove the constraints from the constraints to check, which are already in the passed formula
1919  * and remove the sub formulas (constraints) in the passed formula, which do not occur in the
1920  * constraints to add.
1921  */
1922  auto subformula = passedFormulaBegin();
1923  while( subformula != rPassedFormula().end() )
1924  {
1925  auto iter = constraintsToCheck.find( subformula->formula().constraint() );
1926  if( iter != constraintsToCheck.end() )
1927  {
1928  _formulaCondMap[subformula->formula()] = iter->second;
1929  constraintsToCheck.erase( iter );
1930  ++subformula;
1931  }
1932  else
1933  {
1934  subformula = eraseSubformulaFromPassedFormula( subformula );
1935  changedPassedFormula = true;
1936  }
1937  }
1938  // Add the the remaining constraints to add to the passed formula.
1939  for( auto iter = constraintsToCheck.begin(); iter != constraintsToCheck.end(); ++iter )
1940  {
1941  changedPassedFormula = true;
1942  // @todo store formula and do not generate a new formula every time
1943  FormulaT formula = FormulaT( iter->first );
1944  _formulaCondMap[formula] = iter->second;
1945  addConstraintToInform( formula );
1946  addSubformulaToPassedFormula( formula );
1947  }
1948  return changedPassedFormula;
1949  }
1950 
1951  template<class Settings>
1952  Answer VSModule<Settings>::runBackendSolvers( State* _state )
1953  {
1954  // Run the backends on the constraint of the state.
1955  FormulaConditionMap formulaToConditions;
1956  adaptPassedFormula( *_state, formulaToConditions );
1957  Answer result = runBackends();
1958  #ifdef VS_DEBUG
1959  std::cout << "Ask backend : ";
1960  printPassedFormula();
1961  std::cout << std::endl;
1962  std::cout << "Answer : " << result << std::endl;
1963  #endif
1964  switch( result )
1965  {
1966  case SAT:
1967  {
1968  return SAT;
1969  }
1970  case UNSAT:
1971  {
1972  /*
1973  * Get the conflict sets formed by the infeasible subsets in the backend.
1974  */
1975  ConditionSetSet conflictSet;
1976  std::vector<Module*>::const_iterator backend = usedBackends().begin();
1977  while( backend != usedBackends().end() )
1978  {
1979  if( !(*backend)->infeasibleSubsets().empty() )
1980  {
1981  for( auto infsubset = (*backend)->infeasibleSubsets().begin(); infsubset != (*backend)->infeasibleSubsets().end(); ++infsubset )
1982  {
1983  carl::PointerSet<vs::Condition> conflict;
1984  #ifdef VS_DEBUG
1985  std::cout << "Infeasible Subset: {";
1986  #endif
1987  for( auto subformula = infsubset->begin(); subformula != infsubset->end(); ++subformula )
1988  {
1989  #ifdef VS_DEBUG
1990  std::cout << " " << *subformula;
1991  #endif
1992  auto fcPair = formulaToConditions.find( *subformula );
1993  assert( fcPair != formulaToConditions.end() );
1994  conflict.insert( fcPair->second );
1995  }
1996  #ifdef VS_DEBUG
1997  std::cout << " }" << std::endl;
1998  #endif
1999  #ifdef SMTRAT_DEVOPTION_Validation
2000  smtrat::ConstraintsT constraints;
2001  for( auto cond = conflict.begin(); cond != conflict.end(); ++cond )
2002  constraints.insert( (**cond).constraint() );
2003  SMTRAT_VALIDATION_ADD("smtrat.modules.vs",(*backend)->moduleName() + "_infeasible_subset",constraints,false);
2004  #endif
2005  assert( conflict.size() == infsubset->size() );
2006  assert( !conflict.empty() );
2007  conflictSet.insert( conflict );
2008  }
2009  break;
2010  }
2011  }
2012  assert( !conflictSet.empty() );
2013  _state->addConflictSet( NULL, std::move(conflictSet) );
2014  removeStatesFromRanking( *_state );
2015 
2016  #ifdef VS_LOG_INTERMEDIATE_STEPS
2017  logConditions( *_state, false, "Intermediate_conflict_of_VSModule" );
2018  #endif
2019  // If the considered state is the root, update the found infeasible subset as infeasible subset.
2020  if( _state->isRoot() )
2021  updateInfeasibleSubset();
2022  // If the considered state is not the root, pass the infeasible subset to the father.
2023  else
2024  {
2025  removeStatesFromRanking( *_state );
2026  _state->passConflictToFather( Settings::check_conflict_for_side_conditions );
2027  removeStateFromRanking( _state->rFather() );
2028  addStateToRanking( _state->pFather() );
2029  }
2030  return UNSAT;
2031  }
2032  case UNKNOWN:
2033  {
2034  return UNKNOWN;
2035  }
2036  case ABORTED:
2037  {
2038  return ABORTED;
2039  }
2040  default:
2041  {
2042  std::cerr << "UNKNOWN answer type!" << std::endl;
2043  assert( false );
2044  return UNKNOWN;
2045  }
2046  }
2047  }
2048 
2049  /**
2050  * Checks the correctness of the symbolic assignment given by the path from the root
2051  * state to the satisfying state.
2052  */
2053  template<class Settings>
2054  void VSModule<Settings>::checkAnswer() const
2055  {
2056  if( !mRanking.empty() )
2057  {
2058  const State* currentState = mRanking.begin()->second;
2059  while( !(*currentState).isRoot() )
2060  {
2061  logConditions( *currentState, true, "Intermediate_result_of_VSModule" );
2062  currentState = currentState->pFather();
2063  }
2064  }
2065  }
2066 
2067  template<class Settings>
2068  void VSModule<Settings>::logConditions( const State& _state, [[maybe_unused]] bool _assumption, const std::string& _description, bool _logAsDeduction ) const
2069  {
2070  if( !_state.conditions().empty() )
2071  {
2072  smtrat::ConstraintsT constraints;
2073  for( auto cond = _state.conditions().begin(); cond != _state.conditions().end(); ++cond )
2074  constraints.insert( (**cond).constraint() );
2075  if( _logAsDeduction ) {
2076  SMTRAT_VALIDATION_ADD("smtrat.modules.vs",_description,constraints,_assumption);
2077  }
2078  else
2079  {
2080  std::cout << "(assert (and";
2081  for( auto constraint = constraints.begin(); constraint != constraints.end(); ++constraint )
2082  std::cout << " " << *constraint;
2083  std::cout << " " << _description;
2084  std::cout << "))" << std::endl;
2085  }
2086  }
2087  }
2088 
2089  #ifdef VS_DEBUG_METHODS
2090 
2091  template<class Settings>
2092  void VSModule<Settings>::printAll( const std::string& _init, std::ostream& _out ) const
2093  {
2094  _out << _init << " Current solver status, where the constraints" << std::endl;
2095  printFormulaConditionMap( _init, _out );
2096  _out << _init << " have been added:" << std::endl;
2097  _out << _init << " mInconsistentConstraintAdded: " << mInconsistentConstraintAdded << std::endl;
2098  _out << _init << " mIDCounter: " << mIDCounter << std::endl;
2099  _out << _init << " Current ranking:" << std::endl;
2100  printRanking( _init, std::cout );
2101  _out << _init << " State tree:" << std::endl;
2102  mpStateTree->print( _init + " ", _out );
2103  }
2104 
2105  template<class Settings>
2106  void VSModule<Settings>::printFormulaConditionMap( const std::string& _init, std::ostream& _out ) const
2107  {
2108  for( auto cond = mFormulaConditionMap.begin(); cond != mFormulaConditionMap.end(); ++cond )
2109  {
2110  _out << _init << " ";
2111  _out << cond->first;
2112  _out << " <-> ";
2113  cond->second->print( _out );
2114  _out << std::endl;
2115  }
2116  }
2117 
2118  template<class Settings>
2119  void VSModule<Settings>::printRanking( const std::string& _init, std::ostream& _out ) const
2120  {
2121  for( auto valDTPair = mRanking.begin(); valDTPair != mRanking.end(); ++valDTPair )
2122  (*(*valDTPair).second).printAlone( _init + " ", _out );
2123  }
2124 
2125  template<class Settings>
2126  void VSModule<Settings>::printAnswer( const std::string& _init, std::ostream& _out ) const
2127  {
2128  _out << _init << " Answer:" << std::endl;
2129  if( mRanking.empty() )
2130  _out << _init << " UNSAT." << std::endl;
2131  else
2132  {
2133  _out << _init << " SAT:" << std::endl;
2134  const State* currentState = mRanking.begin()->second;
2135  while( !(*currentState).isRoot() )
2136  {
2137  _out << _init << " " << (*currentState).substitution() << std::endl;
2138  currentState = (*currentState).pFather();
2139  }
2140  }
2141  _out << std::endl;
2142  }
2143  #endif
2144 } // end namespace smtrat
2145 
2146