SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Substitute.cpp
Go to the documentation of this file.
1 /**
2  * Class containing a method applying a virtual substitution.
3  * @author Florian Corzilius
4  * @since 2011-05-23
5  * @version 2013-10-23
6  */
7 
8 #include "Substitute.h"
9 #include <cmath>
10 #include <limits>
11 
12 #include <carl-arith/poly/umvpoly/functions/Derivative.h>
13 #include <carl-arith/poly/umvpoly/functions/SoSDecomposition.h>
14 #include <carl-arith/constraint/IntervalEvaluation.h>
15 #include <carl-arith/vs/Substitution.h>
16 
17 //#define VS_DEBUG_SUBSTITUTION
18 const unsigned MAX_NUM_OF_TERMS = 512;
19 
20 using namespace carl;
21 
22 namespace smtrat {
23 namespace vs
24 {
25  void simplify( DisjunctionOfConstraintConjunctions& _toSimplify )
26  {
27  bool containsEmptyDisjunction = false;
28  auto conj = _toSimplify.begin();
29  while( conj != _toSimplify.end() )
30  {
31  bool conjInconsistent = false;
32  auto cons = (*conj).begin();
33  while( cons != (*conj).end() )
34  {
35  if( *cons == smtrat::ConstraintT( false ) )
36  {
37  conjInconsistent = true;
38  break;
39  }
40  else if( *cons == smtrat::ConstraintT( true ) )
41  cons = (*conj).erase( cons );
42  else
43  cons++;
44  }
45  bool conjEmpty = (*conj).empty();
46  if( conjInconsistent || (containsEmptyDisjunction && conjEmpty) )
47  {
48  // Delete the conjunction.
49  conj->clear();
50  conj = _toSimplify.erase( conj );
51  }
52  else
53  conj++;
54  if( !containsEmptyDisjunction && conjEmpty )
55  containsEmptyDisjunction = true;
56  }
57  }
58 
59  void simplify( DisjunctionOfConstraintConjunctions& _toSimplify, Variables& _conflictingVars, const smtrat::EvalDoubleIntervalMap& _solutionSpace )
60  {
61  bool containsEmptyDisjunction = false;
62  auto conj = _toSimplify.begin();
63  while( conj != _toSimplify.end() )
64  {
65  bool conjInconsistent = false;
66  auto cons = (*conj).begin();
67  while( cons != (*conj).end() )
68  {
69  if( *cons == smtrat::ConstraintT( false ) )
70  {
71  conjInconsistent = true;
72  break;
73  }
74  else if( *cons == smtrat::ConstraintT( true ) )
75  cons = (*conj).erase( cons );
76  else
77  {
78  unsigned conflictingWithSolutionSpace = consistent_with(cons->constr(), _solutionSpace );
79 
80 // std::cout << "Is " << cons << std::endl;
81 // std::cout << std::endl;
82 // std::cout << "consistent with " << std::endl;
83 // for( auto iter = _solutionSpace.begin(); iter != _solutionSpace.end(); ++iter )
84 // std::cout << iter->first << " in " << iter->second << std::endl;
85 // std::cout << " -> " << conflictingWithSolutionSpace << std::endl;
86 
87  if( conflictingWithSolutionSpace == 0 )
88  {
89  auto vars = carl::variables(*cons);
90  _conflictingVars.insert( vars.begin(), vars.end() );
91  conjInconsistent = true;
92  break;
93  }
94  else if( conflictingWithSolutionSpace == 1 )
95  cons = (*conj).erase( cons );
96  else
97  ++cons;
98  }
99  }
100  bool conjEmpty = (*conj).empty();
101  if( conjInconsistent || (containsEmptyDisjunction && conjEmpty) )
102  {
103  // Delete the conjunction.
104  conj->clear();
105  conj = _toSimplify.erase( conj );
106  }
107  else
108  ++conj;
109  if( !containsEmptyDisjunction && conjEmpty )
110  containsEmptyDisjunction = true;
111  }
112  }
113 
114  bool splitProducts( DisjunctionOfConstraintConjunctions& _toSimplify, bool _onlyNeq )
115  {
116  bool result = true;
117  size_t toSimpSize = _toSimplify.size();
118  for( size_t pos = 0; pos < toSimpSize; )
119  {
120  if( !_toSimplify.begin()->empty() )
121  {
122  DisjunctionOfConstraintConjunctions temp;
123  if( !splitProducts( _toSimplify[pos], temp, _onlyNeq ) )
124  result = false;
125  _toSimplify.erase( _toSimplify.begin() );
126  _toSimplify.insert( _toSimplify.end(), temp.begin(), temp.end() );
127  --toSimpSize;
128  }
129  else
130  ++pos;
131  }
132  return result;
133  }
134 
135  bool splitProducts( const ConstraintVector& _toSimplify, DisjunctionOfConstraintConjunctions& _result, bool _onlyNeq )
136  {
137  std::vector<DisjunctionOfConstraintConjunctions> toCombine;
138  for( auto constraint = _toSimplify.begin(); constraint != _toSimplify.end(); ++constraint )
139  {
140  auto& factorization = (*constraint).lhs_factorization();
141  if( !carl::is_trivial(factorization) )
142  {
143  switch( constraint->relation() )
144  {
145  case Relation::EQ:
146  {
147  if( !_onlyNeq )
148  {
149  toCombine.emplace_back();
150  for( auto factor = factorization.begin(); factor != factorization.end(); ++factor )
151  {
152  toCombine.back().emplace_back();
153  toCombine.back().back().push_back( smtrat::ConstraintT( factor->first, Relation::EQ ) );
154  }
155  simplify( toCombine.back() );
156  }
157  else
158  {
159  toCombine.emplace_back();
160  toCombine.back().emplace_back();
161  toCombine.back().back().push_back( *constraint );
162  }
163  break;
164  }
165  case Relation::NEQ:
166  {
167  toCombine.emplace_back();
168  toCombine.back().emplace_back();
169  for( auto factor = factorization.begin(); factor != factorization.end(); ++factor )
170  toCombine.back().back().push_back( smtrat::ConstraintT( factor->first, Relation::NEQ ) );
171  simplify( toCombine.back() );
172  break;
173  }
174  default:
175  {
176  if( !_onlyNeq )
177  {
178  toCombine.push_back( getSignCombinations( *constraint ) );
179  simplify( toCombine.back() );
180  }
181  else
182  {
183  toCombine.emplace_back();
184  toCombine.back().emplace_back();
185  toCombine.back().back().push_back( *constraint );
186  }
187  }
188  }
189  }
190  else
191  {
192  toCombine.emplace_back();
193  toCombine.back().emplace_back();
194  toCombine.back().back().push_back( *constraint );
195  }
196  }
197  bool result = true;
198  if( !combine( toCombine, _result ) )
199  result = false;
200  simplify( _result );
201  return result;
202  }
203 
204  DisjunctionOfConstraintConjunctions splitProducts( const smtrat::ConstraintT& _constraint, bool _onlyNeq )
205  {
206  DisjunctionOfConstraintConjunctions result;
207  auto& factorization = _constraint.lhs_factorization();
208  if( !carl::is_trivial(factorization) )
209  {
210  switch( _constraint.relation() )
211  {
212  case Relation::EQ:
213  {
214  if( !_onlyNeq )
215  {
216  for( auto factor = factorization.begin(); factor != factorization.end(); ++factor )
217  {
218  result.emplace_back();
219  result.back().push_back( smtrat::ConstraintT( factor->first, Relation::EQ ) );
220  }
221  }
222  else
223  {
224  result.emplace_back();
225  result.back().push_back( _constraint );
226  }
227  simplify( result );
228  break;
229  }
230  case Relation::NEQ:
231  {
232  result.emplace_back();
233  for( auto factor = factorization.begin(); factor != factorization.end(); ++factor )
234  result.back().push_back( smtrat::ConstraintT( factor->first, Relation::NEQ ) );
235  simplify( result );
236  break;
237  }
238  default:
239  {
240  if( !_onlyNeq )
241  {
242  result = getSignCombinations( _constraint );
243  simplify( result );
244  }
245  else
246  {
247  result.emplace_back();
248  result.back().push_back( _constraint );
249  }
250  }
251 
252  }
253  }
254  else
255  {
256  result.emplace_back();
257  result.back().push_back( _constraint );
258  }
259  return result;
260  }
261 
262  void splitSosDecompositions( DisjunctionOfConstraintConjunctions& _toSimplify )
263  {
264  // TODO this needs to be reviewed and fixed
265  // It seems that is is assumed that lcoeffNeg * constraint.lhs() is positive if
266  // a SOS decomposition exists. However, we can only follow that it's non-negative
267  // (in the univariate case), for the multivariate case more requirements need to be made
268  // (therefor constraint.lhs().has_constant_term() ???).
269  // This lead to wrong simplifications in very rare cases, for example
270  // -100 + 140*z + -49*y^2 + -49*z^2 is wrongly simplified to true (see McsatVSBug).
271 
272  // Temporarily disabled (what can be followed in the multivariate case?).
273  return;
274 
275  for( size_t i = 0; i < _toSimplify.size(); )
276  {
277  auto& cc = _toSimplify[i];
278  bool foundNoInvalidConstraint = true;
279  size_t pos = 0;
280  while( foundNoInvalidConstraint && pos < cc.size() )
281  {
282  const smtrat::ConstraintT& constraint = cc[pos];
283  std::vector<std::pair<smtrat::Rational,smtrat::Poly>> sosDec;
284  bool lcoeffNeg = carl::is_negative(constraint.lhs().lcoeff());
285  if (lcoeffNeg)
286  sosDec = carl::sos_decomposition(-constraint.lhs());
287  else
288  sosDec = carl::sos_decomposition(constraint.lhs());
289  if( sosDec.size() > 1 )
290  {
291 // std::cout << "Sum-of-squares decomposition of " << constraint.lhs() << " = " << sosDec << std::endl;
292  bool addSquares = true;
293  bool constraintValid = false;
294  switch( constraint.relation() )
295  {
296  case carl::Relation::EQ:
297  {
298  if( constraint.lhs().has_constant_term() )
299  {
300  foundNoInvalidConstraint = false;
301  addSquares = false;
302  }
303  break;
304  }
305  case carl::Relation::NEQ:
306  {
307  addSquares = false;
308  if( constraint.lhs().has_constant_term() )
309  {
310  constraintValid = true;
311  }
312  break;
313  }
314  case carl::Relation::LEQ:
315  {
316  if( lcoeffNeg )
317  {
318  addSquares = false;
319  constraintValid = true;
320  }
321  else if( constraint.lhs().has_constant_term() )
322  {
323  addSquares = false;
324  foundNoInvalidConstraint = false;
325  }
326  break;
327  }
328  case carl::Relation::LESS:
329  {
330  addSquares = false;
331  if( lcoeffNeg )
332  {
333  if( constraint.lhs().has_constant_term() )
334  constraintValid = true;
335  }
336  else
337  foundNoInvalidConstraint = false;
338  break;
339  }
340  case carl::Relation::GEQ:
341  {
342  if( !lcoeffNeg )
343  {
344  addSquares = false;
345  constraintValid = true;
346  }
347  else if( constraint.lhs().has_constant_term() )
348  {
349  addSquares = false;
350  foundNoInvalidConstraint = false;
351  }
352  break;
353  }
354  default:
355  {
356  assert( constraint.relation() == carl::Relation::GREATER );
357  addSquares = false;
358  if( lcoeffNeg )
359  foundNoInvalidConstraint = false;
360  else
361  {
362  if( constraint.lhs().has_constant_term() )
363  constraintValid = true;
364  }
365  }
366  }
367  assert( !(!foundNoInvalidConstraint && constraintValid) );
368  assert( !(!foundNoInvalidConstraint && addSquares) );
369  if( constraintValid || addSquares )
370  {
371  cc[pos] = cc.back();
372  cc.pop_back();
373  }
374  else
375  ++pos;
376  if( addSquares )
377  {
378  for( auto it = sosDec.begin(); it != sosDec.end(); ++it )
379  {
380  cc.emplace_back( it->second, carl::Relation::EQ );
381  }
382  }
383  }
384  else
385  ++pos;
386  }
387  if( foundNoInvalidConstraint )
388  ++i;
389  else
390  {
391  cc = _toSimplify.back();
392  _toSimplify.pop_back();
393  }
394  }
395  }
396 
397  DisjunctionOfConstraintConjunctions getSignCombinations( const smtrat::ConstraintT& _constraint )
398  {
399  DisjunctionOfConstraintConjunctions combinations;
400  auto& factorization = _constraint.lhs_factorization();
401  if( !carl::is_trivial(factorization) && factorization.size() <= MAX_PRODUCT_SPLIT_NUMBER )
402  {
403  assert( _constraint.relation() == Relation::GREATER || _constraint.relation() == Relation::LESS
404  || _constraint.relation() == Relation::GEQ || _constraint.relation() == Relation::LEQ );
405  Relation relPos = Relation::GREATER;
406  Relation relNeg = Relation::LESS;
407  if( _constraint.relation() == Relation::GEQ || _constraint.relation() == Relation::LEQ )
408  {
409  relPos = Relation::GEQ;
410  relNeg = Relation::LEQ;
411  }
412  bool positive = (_constraint.relation() == Relation::GEQ || _constraint.relation() == Relation::GREATER);
413  ConstraintVector positives;
414  ConstraintVector alwayspositives;
415  ConstraintVector negatives;
416  ConstraintVector alwaysnegatives;
417  unsigned numOfAlwaysNegatives = 0;
418  for( auto factor = factorization.begin(); factor != factorization.end(); ++factor )
419  {
420  smtrat::ConstraintT consPos = smtrat::ConstraintT( factor->first, relPos );
421  unsigned posConsistent = consPos.is_consistent();
422  if( posConsistent != 0 )
423  positives.push_back( consPos );
424  smtrat::ConstraintT consNeg = smtrat::ConstraintT( factor->first, relNeg );
425  unsigned negConsistent = consNeg.is_consistent();
426  if( negConsistent == 0 )
427  {
428  if( posConsistent == 0 )
429  {
430  combinations.emplace_back();
431  combinations.back().push_back( consNeg );
432  return combinations;
433  }
434  if( posConsistent != 1 )
435  alwayspositives.push_back( positives.back() );
436  positives.pop_back();
437  }
438  else
439  {
440  if( posConsistent == 0 )
441  {
442  ++numOfAlwaysNegatives;
443  if( negConsistent != 1 )
444  alwaysnegatives.push_back( consNeg );
445  }
446  else negatives.push_back( consNeg );
447  }
448  }
449  assert( positives.size() == negatives.size() );
450  if( positives.size() > 0 )
451  {
452  std::vector< std::bitset<MAX_PRODUCT_SPLIT_NUMBER> > combSelector = std::vector< std::bitset<MAX_PRODUCT_SPLIT_NUMBER> >();
453  if( fmod( numOfAlwaysNegatives, 2.0 ) != 0.0 )
454  {
455  if( positive )
456  getOddBitStrings( positives.size(), combSelector );
457  else
458  getEvenBitStrings( positives.size(), combSelector );
459  }
460  else
461  {
462  if( positive )
463  getEvenBitStrings( positives.size(), combSelector );
464  else
465  getOddBitStrings( positives.size(), combSelector );
466  }
467  for( auto comb = combSelector.begin(); comb != combSelector.end(); ++comb )
468  {
469  combinations.emplace_back( alwaysnegatives );
470  combinations.back().insert( combinations.back().end(), alwayspositives.begin(), alwayspositives.end() );
471  for( unsigned pos = 0; pos < positives.size(); ++pos )
472  {
473  if( (*comb)[pos] )
474  combinations.back().push_back( negatives[pos] );
475  else
476  combinations.back().push_back( positives[pos] );
477  }
478  }
479  }
480  else
481  {
482  combinations.emplace_back( alwaysnegatives );
483  combinations.back().insert( combinations.back().end(), alwayspositives.begin(), alwayspositives.end() );
484  }
485  }
486  else
487  {
488  combinations.emplace_back();
489  combinations.back().push_back( _constraint );
490  }
491  return combinations;
492  }
493 
494  void getOddBitStrings( std::size_t _length, std::vector< std::bitset<MAX_PRODUCT_SPLIT_NUMBER> >& _strings )
495  {
496  assert( _length > 0 );
497  if( _length == 1 ) _strings.push_back( std::bitset<MAX_PRODUCT_SPLIT_NUMBER>( 1 ) );
498  else
499  {
500  std::size_t pos = _strings.size();
501  getEvenBitStrings( _length - 1, _strings );
502  for( ; pos < _strings.size(); ++pos )
503  {
504  _strings[pos] <<= 1;
505  _strings[pos].flip(0);
506  }
507  getOddBitStrings( _length - 1, _strings );
508  for( ; pos < _strings.size(); ++pos ) _strings[pos] <<= 1;
509  }
510  }
511 
512  void getEvenBitStrings( std::size_t _length, std::vector< std::bitset<MAX_PRODUCT_SPLIT_NUMBER> >& _strings )
513  {
514  assert( _length > 0 );
515  if( _length == 1 ) _strings.push_back( std::bitset<MAX_PRODUCT_SPLIT_NUMBER>( 0 ) );
516  else
517  {
518  std::size_t pos = _strings.size();
519  getEvenBitStrings( _length - 1, _strings );
520  for( ; pos < _strings.size(); ++pos ) _strings[pos] <<= 1;
521  getOddBitStrings( _length - 1, _strings );
522  for( ; pos < _strings.size(); ++pos )
523  {
524  _strings[pos] <<= 1;
525  _strings[pos].flip(0);
526  }
527  }
528  }
529 
530  void print( DisjunctionOfConstraintConjunctions& _substitutionResults )
531  {
532  auto conj = _substitutionResults.begin();
533  while( conj != _substitutionResults.end() )
534  {
535  if( conj != _substitutionResults.begin() )
536  std::cout << " or (";
537  else
538  std::cout << " (";
539  auto cons = (*conj).begin();
540  while( cons != (*conj).end() )
541  {
542  if( cons != (*conj).begin() )
543  std::cout << " and ";
544  std::cout << *cons;
545  cons++;
546  }
547  std::cout << ")" << std::endl;
548  conj++;
549  }
550  std::cout << std::endl;
551  }
552 
553  bool substitute( const smtrat::ConstraintT& _cons,
554  const Substitution& _subs,
555  DisjunctionOfConstraintConjunctions& _result,
556  bool _accordingPaper,
557  Variables& _conflictingVariables,
558  const smtrat::EvalDoubleIntervalMap& _solutionSpace )
559  {
560  #ifdef VS_DEBUG_SUBSTITUTION
561  std::cout << "substitute: ( " << _cons << " )" << _subs << std::endl;
562  #endif
563  bool result = true;
564  // Apply the substitution according to its type.
565  switch( _subs.type() )
566  {
567  case Substitution::NORMAL:
568  {
569  result = substituteNormal( _cons, _subs, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
570  break;
571  }
572  case Substitution::PLUS_EPSILON:
573  {
574  result = substitutePlusEps( _cons, _subs, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
575  break;
576  }
577  case Substitution::MINUS_INFINITY:
578  {
579  substituteInf( _cons, _subs, _result, _conflictingVariables, _solutionSpace );
580  break;
581  }
582  case Substitution::PLUS_INFINITY:
583  {
584  substituteInf( _cons, _subs, _result, _conflictingVariables, _solutionSpace );
585  break;
586  }
587  default:
588  {
589  std::cout << "Error in substitute: unexpected type of substitution." << std::endl;
590  }
591  }
592  #ifdef VS_DEBUG_SUBSTITUTION
593  print( _result );
594  #endif
595  bool factorization = true;
596  if( factorization && !splitProducts( _result, true ) )
597  result = false;
598  if( result )
599  {
600  splitSosDecompositions( _result );
601  }
602  #ifdef VS_DEBUG_SUBSTITUTION
603  print( _result );
604  #endif
605  return result;
606  }
607 
608  bool substituteNormal( const smtrat::ConstraintT& _cons,
609  const Substitution& _subs,
610  DisjunctionOfConstraintConjunctions& _result,
611  bool _accordingPaper,
612  Variables& _conflictingVariables,
613  const smtrat::EvalDoubleIntervalMap& _solutionSpace )
614  {
615 
616  bool result = true;
617  if( _cons.variables().has( _subs.variable() ) )
618  {
619  // Collect all necessary left hand sides to create the new conditions of all cases referring to the virtual substitution.
620  if( carl::pow( smtrat::Rational(smtrat::Rational(_subs.term().constant_part().size()) + smtrat::Rational(_subs.term().factor().size()) * smtrat::Rational(_subs.term().radicand().size())), _cons.maxDegree( _subs.variable() )) > (MAX_NUM_OF_TERMS*MAX_NUM_OF_TERMS) )
621  {
622  return false;
623  }
624  smtrat::SqrtEx sub = carl::substitute( _cons.lhs(), _subs.variable(), _subs.term() );
625  #ifdef VS_DEBUG_SUBSTITUTION
626  std::cout << "Result of common substitution:" << sub << std::endl;
627  #endif
628  // The term then looks like: q/s
629  if( !sub.has_sqrt() )
630  {
631  // Create the new decision tuples.
632  if( _cons.relation() == Relation::EQ || _cons.relation() == Relation::NEQ )
633  {
634  // Add conjunction (sub.constant_part() = 0) to the substitution result.
635  _result.emplace_back();
636  _result.back().push_back( smtrat::ConstraintT( sub.constant_part(), _cons.relation() ) );
637  }
638  else
639  {
640  if( !_subs.term().denominator().is_constant() )
641  {
642  // Add conjunction (sub.denominator()>0 and sub.constant_part() </>/<=/>= 0) to the substitution result.
643  _result.emplace_back();
644  _result.back().push_back( smtrat::ConstraintT( sub.denominator(), Relation::GREATER ) );
645  _result.back().push_back( smtrat::ConstraintT( sub.constant_part(), _cons.relation() ) );
646  // Add conjunction (sub.denominator()<0 and sub.constant_part() >/</>=/<= 0) to the substitution result.
647  Relation inverseRelation;
648  switch( _cons.relation() )
649  {
650  case Relation::LESS:
651  inverseRelation = Relation::GREATER;
652  break;
653  case Relation::GREATER:
654  inverseRelation = Relation::LESS;
655  break;
656  case Relation::LEQ:
657  inverseRelation = Relation::GEQ;
658  break;
659  case Relation::GEQ:
660  inverseRelation = Relation::LEQ;
661  break;
662  default:
663  assert( false );
664  inverseRelation = Relation::EQ;
665  }
666  _result.emplace_back();
667  _result.back().push_back( smtrat::ConstraintT( sub.denominator(), Relation::LESS ) );
668  _result.back().push_back( smtrat::ConstraintT( sub.constant_part(), inverseRelation ) );
669  }
670  else
671  {
672  // Add conjunction (f(-c/b)*b^k </>/<=/>= 0) to the substitution result.
673  _result.emplace_back();
674  _result.back().push_back( smtrat::ConstraintT( sub.constant_part(), _cons.relation() ) );
675  }
676  }
677  }
678  // The term then looks like: (q+r*sqrt(b^2-4ac))/s
679  else
680  {
681  smtrat::Poly s = Poly(1);
682  if( !_subs.term().denominator().is_constant() )
683  s = sub.denominator();
684  switch( _cons.relation() )
685  {
686  case Relation::EQ:
687  {
688  result = substituteNormalSqrtEq( sub.radicand(), sub.constant_part(), sub.factor(), _result, _accordingPaper );
689  break;
690  }
691  case Relation::NEQ:
692  {
693  result = substituteNormalSqrtNeq( sub.radicand(), sub.constant_part(), sub.factor(), _result, _accordingPaper );
694  break;
695  }
696  case Relation::LESS:
697  {
698  result = substituteNormalSqrtLess( sub.radicand(), sub.constant_part(), sub.factor(), s, _result, _accordingPaper );
699  break;
700  }
701  case Relation::GREATER:
702  {
703  result = substituteNormalSqrtLess( sub.radicand(), sub.constant_part(), sub.factor(), -s, _result, _accordingPaper );
704  break;
705  }
706  case Relation::LEQ:
707  {
708  result = substituteNormalSqrtLeq( sub.radicand(), sub.constant_part(), sub.factor(), s, _result, _accordingPaper );
709  break;
710  }
711  case Relation::GEQ:
712  {
713  result = substituteNormalSqrtLeq( sub.radicand(), sub.constant_part(), sub.factor(), -s, _result, _accordingPaper );
714  break;
715  }
716  default:
717  std::cout << "Error in substituteNormal: Unexpected relation symbol" << std::endl;
718  assert( false );
719  }
720  }
721  }
722  else
723  {
724  _result.emplace_back();
725  _result.back().push_back( _cons );
726  }
727  simplify( _result, _conflictingVariables, _solutionSpace );
728  return result;
729  }
730 
731  bool substituteNormalSqrtEq( const smtrat::Poly& _radicand,
732  const smtrat::Poly& _q,
733  const smtrat::Poly& _r,
734  DisjunctionOfConstraintConjunctions& _result,
735  bool _accordingPaper )
736  {
737  if( _q.size() > MAX_NUM_OF_TERMS || _r.size() > MAX_NUM_OF_TERMS || _radicand.size() > MAX_NUM_OF_TERMS )
738  return false;
739  smtrat::Poly lhs = carl::pow(_q, 2) - carl::pow(_r, 2) * _radicand;
740  if( _accordingPaper )
741  {
742  smtrat::Poly qr = _q * _r;
743  // Add conjunction (q*r<=0 and q^2-r^2*radicand=0) to the substitution result.
744  _result.emplace_back();
745  _result.back().push_back( smtrat::ConstraintT( qr, Relation::LEQ ) );
746  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::EQ ) );
747  }
748  else
749  {
750  // Add conjunction (q=0 and r=0) to the substitution result.
751  _result.emplace_back();
752  _result.back().push_back( smtrat::ConstraintT( _q, Relation::EQ ) );
753  _result.back().push_back( smtrat::ConstraintT( _r, Relation::EQ ) );
754  // Add conjunction (q=0 and radicand=0) to the substitution result.
755  _result.emplace_back();
756  _result.back().push_back( smtrat::ConstraintT( _q, Relation::EQ ) );
757  _result.back().push_back( smtrat::ConstraintT( _radicand, Relation::EQ ) );
758  // Add conjunction (q<0 and r>0 and q^2-r^2*radicand=0) to the substitution result.
759  _result.emplace_back();
760  _result.back().push_back( smtrat::ConstraintT( _q, Relation::LESS ) );
761  _result.back().push_back( smtrat::ConstraintT( _r, Relation::GREATER ) );
762  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::EQ ) );
763  // Add conjunction (q>0 and r<0 and q^2-r^2*radicand=0) to the substitution result.
764  _result.emplace_back();
765  _result.back().push_back( smtrat::ConstraintT( _q, Relation::GREATER ) );
766  _result.back().push_back( smtrat::ConstraintT( _r, Relation::LESS ) );
767  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::EQ ) );
768  }
769  return true;
770  }
771 
772  bool substituteNormalSqrtNeq( const smtrat::Poly& _radicand,
773  const smtrat::Poly& _q,
774  const smtrat::Poly& _r,
775  DisjunctionOfConstraintConjunctions& _result,
776  bool _accordingPaper )
777  {
778  if( _q.size() > MAX_NUM_OF_TERMS || _r.size() > MAX_NUM_OF_TERMS || _radicand.size() > MAX_NUM_OF_TERMS )
779  return false;
780  smtrat::Poly lhs = carl::pow(_q, 2) - carl::pow(_r, 2) * _radicand;
781  if( _accordingPaper )
782  {
783  smtrat::Poly qr = _q * _r;
784  // Add conjunction (q*r>0 and q^2-r^2*radicand!=0) to the substitution result.
785  _result.emplace_back();
786  _result.back().push_back( smtrat::ConstraintT( qr, Relation::GREATER ) );
787  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::NEQ ) );
788  }
789  else
790  {
791  // Add conjunction (q>0 and r>0) to the substitution result.
792  _result.emplace_back();
793  _result.back().push_back( smtrat::ConstraintT( _q, Relation::GREATER ) );
794  _result.back().push_back( smtrat::ConstraintT( _r, Relation::GREATER ) );
795  // Add conjunction (q<0 and r<0) to the substitution result.
796  _result.emplace_back();
797  _result.back().push_back( smtrat::ConstraintT( _q, Relation::LESS ) );
798  _result.back().push_back( smtrat::ConstraintT( _r, Relation::LESS ) );
799  // Add conjunction (q^2-r^2*radicand!=0) to the substitution result.
800  _result.emplace_back();
801  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::NEQ ) );
802  }
803  return true;
804  }
805 
806  bool substituteNormalSqrtLess( const smtrat::Poly& _radicand,
807  const smtrat::Poly& _q,
808  const smtrat::Poly& _r,
809  const smtrat::Poly& _s,
810  DisjunctionOfConstraintConjunctions& _result,
811  bool _accordingPaper )
812  {
813  if( _q.size() > MAX_NUM_OF_TERMS || _r.size() > MAX_NUM_OF_TERMS || _radicand.size() > MAX_NUM_OF_TERMS )
814  return false;
815  smtrat::Poly lhs = carl::pow(_q, 2) - carl::pow(_r, 2) * _radicand;
816  if( _accordingPaper )
817  {
818  smtrat::Poly qs = _q * _s;
819  smtrat::Poly rs = _r * _s;
820  // Add conjunction (q*s<0 and q^2-r^2*radicand>0) to the substitution result.
821  _result.emplace_back();
822  _result.back().push_back( smtrat::ConstraintT( qs, Relation::LESS ) );
823  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GREATER ) );
824  // Add conjunction (r*s<=0 and q*s<0) to the substitution result.
825  _result.emplace_back();
826  _result.back().push_back( smtrat::ConstraintT( rs, Relation::LEQ ) );
827  _result.back().push_back( smtrat::ConstraintT( qs, Relation::LESS ) );
828  // Add conjunction (r*s<=0 and q^2-r^2*radicand<0) to the substitution result.
829  _result.emplace_back();
830  _result.back().push_back( smtrat::ConstraintT( rs, Relation::LEQ ) );
831  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LESS ) );
832  }
833  else
834  {
835  // Add conjunction (q<0 and s>0 and q^2-r^2*radicand>0) to the substitution result.
836  _result.emplace_back();
837  _result.back().push_back( smtrat::ConstraintT( _q, Relation::LESS ) );
838  _result.back().push_back( smtrat::ConstraintT( _s, Relation::GREATER ) );
839  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GREATER ) );
840  // Add conjunction (q>0 and s<0 and q^2-r^2*radicand>0) to the substitution result.
841  _result.emplace_back();
842  _result.back().push_back( smtrat::ConstraintT( _q, Relation::GREATER ) );
843  _result.back().push_back( smtrat::ConstraintT( _s, Relation::LESS ) );
844  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GREATER ) );
845  // Add conjunction (r>0 and s<0 and q^2-r^2*radicand<0) to the substitution result.
846  _result.emplace_back();
847  _result.back().push_back( smtrat::ConstraintT( _r, Relation::GREATER ) );
848  _result.back().push_back( smtrat::ConstraintT( _s, Relation::LESS ) );
849  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LESS ) );
850  // Add conjunction (r<0 and s>0 and q^2-r^2*radicand<0) to the substitution result.
851  _result.emplace_back();
852  _result.back().push_back( smtrat::ConstraintT( _r, Relation::LESS ) );
853  _result.back().push_back( smtrat::ConstraintT( _s, Relation::GREATER ) );
854  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LESS ) );
855  // Add conjunction (r>=0 and q<0 and s>0) to the substitution result.
856  _result.emplace_back();
857  _result.back().push_back( smtrat::ConstraintT( _r, Relation::GEQ ) );
858  _result.back().push_back( smtrat::ConstraintT( _q, Relation::GREATER ) );
859  _result.back().push_back( smtrat::ConstraintT( _s, Relation::LESS ) );
860  // Add conjunction (r<=0 and q>0 and s<0) to the substitution result.
861  _result.emplace_back();
862  _result.back().push_back( smtrat::ConstraintT( _r, Relation::LEQ ) );
863  _result.back().push_back( smtrat::ConstraintT( _q, Relation::LESS ) );
864  _result.back().push_back( smtrat::ConstraintT( _s, Relation::GREATER ) );
865  }
866  return true;
867  }
868 
869  bool substituteNormalSqrtLeq( const smtrat::Poly& _radicand,
870  const smtrat::Poly& _q,
871  const smtrat::Poly& _r,
872  const smtrat::Poly& _s,
873  DisjunctionOfConstraintConjunctions& _result,
874  bool _accordingPaper )
875  {
876  if( _q.size() > MAX_NUM_OF_TERMS || _r.size() > MAX_NUM_OF_TERMS || _radicand.size() > MAX_NUM_OF_TERMS )
877  return false;
878  smtrat::Poly lhs = carl::pow(_q, 2) - carl::pow(_r, 2) * _radicand;
879  if( _accordingPaper )
880  {
881  smtrat::Poly qs = _q * _s;
882  smtrat::Poly rs = _r * _s;
883  // Add conjunction (q*s<=0 and q^2-r^2*radicand>=0) to the substitution result.
884  _result.emplace_back();
885  _result.back().push_back( smtrat::ConstraintT( qs, Relation::LEQ ) );
886  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GEQ ) );
887  // Add conjunction (r*s<=0 and q^2-r^2*radicand<=0) to the substitution result.
888  _result.emplace_back();
889  _result.back().push_back( smtrat::ConstraintT( rs, Relation::LEQ ) );
890  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LEQ ) );
891  }
892  else
893  {
894  // Add conjunction (q<0 and s>0 and q^2-r^2*radicand>=0) to the substitution result.
895  _result.emplace_back();
896  _result.back().push_back( smtrat::ConstraintT( _q, Relation::LESS ) );
897  _result.back().push_back( smtrat::ConstraintT( _s, Relation::GREATER ) );
898  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GEQ ) );
899  // Add conjunction (q>0 and s<0 and q^2-r^2*radicand>=0) to the substitution result.
900  _result.emplace_back();
901  _result.back().push_back( smtrat::ConstraintT( _q, Relation::GREATER ) );
902  _result.back().push_back( smtrat::ConstraintT( _s, Relation::LESS ) );
903  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::GEQ ) );
904  // Add conjunction (r>0 and s<0 and q^2-r^2*radicand<=0) to the substitution result.
905  _result.emplace_back();
906  _result.back().push_back( smtrat::ConstraintT( _r, Relation::GREATER ) );
907  _result.back().push_back( smtrat::ConstraintT( _s, Relation::LESS ) );
908  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LEQ ) );
909  // Add conjunction (r<0 and s>0 and q^2-r^2*radicand<=0) to the substitution result.
910  _result.emplace_back();
911  _result.back().push_back( smtrat::ConstraintT( _r, Relation::LESS ) );
912  _result.back().push_back( smtrat::ConstraintT( _s, Relation::GREATER ) );
913  _result.back().push_back( smtrat::ConstraintT( lhs, Relation::LEQ ) );
914  // Add conjunction (r=0 and q=0) to the substitution result.
915  _result.emplace_back();
916  _result.back().push_back( smtrat::ConstraintT( _r, Relation::EQ ) );
917  _result.back().push_back( smtrat::ConstraintT( _q, Relation::EQ ) );
918  // Add conjunction (radicand=0 and q=0) to the substitution result.
919  _result.emplace_back();
920  _result.back().push_back( smtrat::ConstraintT( _radicand, Relation::EQ ) );
921  _result.back().push_back( smtrat::ConstraintT( _q, Relation::EQ ) );
922  }
923  return true;
924  }
925 
926  bool substitutePlusEps( const smtrat::ConstraintT& _cons,
927  const Substitution& _subs,
928  DisjunctionOfConstraintConjunctions& _result,
929  bool _accordingPaper,
930  Variables& _conflictingVariables,
931  const smtrat::EvalDoubleIntervalMap& _solutionSpace )
932  {
933  bool result = true;
934  if( !_cons.variables().empty() )
935  {
936  if( _cons.variables().has( _subs.variable() ) )
937  {
938  switch( _cons.relation() )
939  {
940  case Relation::EQ:
941  {
942  substituteTrivialCase( _cons, _subs, _result );
943  break;
944  }
945  case Relation::NEQ:
946  {
947  substituteNotTrivialCase( _cons, _subs, _result );
948  break;
949  }
950  case Relation::LESS:
951  {
952  result = substituteEpsGradients( _cons, _subs, Relation::LESS, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
953  break;
954  }
955  case Relation::GREATER:
956  {
957  result = substituteEpsGradients( _cons, _subs, Relation::GREATER, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
958  break;
959  }
960  case Relation::LEQ:
961  {
962  substituteTrivialCase( _cons, _subs, _result );
963  result = substituteEpsGradients( _cons, _subs, Relation::LESS, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
964  break;
965  }
966  case Relation::GEQ:
967  {
968  substituteTrivialCase( _cons, _subs, _result );
969  result = substituteEpsGradients( _cons, _subs, Relation::GREATER, _result, _accordingPaper, _conflictingVariables, _solutionSpace );
970  break;
971  }
972  default:
973  assert( false );
974  }
975  simplify( _result, _conflictingVariables, _solutionSpace );
976  }
977  else
978  {
979  _result.emplace_back();
980  _result.back().push_back( _cons );
981  }
982  }
983  else
984  {
985  assert( false );
986  std::cerr << "Warning in substitutePlusEps: The chosen constraint has no variable" << std::endl;
987  }
988  return result;
989  }
990 
991  bool substituteEpsGradients( const smtrat::ConstraintT& _cons,
992  const Substitution& _subs,
993  const Relation _relation,
994  DisjunctionOfConstraintConjunctions& _result,
995  bool _accordingPaper,
996  Variables& _conflictingVariables,
997  const smtrat::EvalDoubleIntervalMap& _solutionSpace )
998  {
999  assert( _cons.variables().has( _subs.variable() ) );
1000  // Create a substitution formed by the given one without an addition of epsilon.
1001  Substitution substitution = Substitution( _subs.variable(), _subs.term(), Substitution::NORMAL, carl::PointerSet<Condition>(_subs.originalConditions()) );
1002  // Call the method substituteNormal with the constraint f(x)~0 and the substitution [x -> t], where the parameter relation is ~.
1003  smtrat::ConstraintT firstCaseInequality = smtrat::ConstraintT( _cons.lhs(), _relation );
1004  if( !substituteNormal( firstCaseInequality, substitution, _result, _accordingPaper, _conflictingVariables, _solutionSpace ) )
1005  return false;
1006  // Create a vector to store the results of each single substitution.
1007  std::vector<DisjunctionOfConstraintConjunctions> substitutionResultsVector;
1008  /*
1009  * Let k be the maximum degree of x in f, then call for every 1<=i<=k substituteNormal with:
1010  *
1011  * f^0(x)=0 and ... and f^i-1(x)=0 and f^i(x)~0 as constraints and
1012  * [x -> t] as substitution,
1013  *
1014  * where the relation is ~.
1015  */
1016  smtrat::Poly deriv = smtrat::Poly( _cons.lhs() );
1017  while( deriv.has( _subs.variable() ) )
1018  {
1019  // Change the relation symbol of the last added constraint to "=".
1020  smtrat::ConstraintT equation = smtrat::ConstraintT( deriv, Relation::EQ );
1021  // Form the derivate of the left hand side of the last added constraint.
1022  deriv = carl::derivative(deriv, _subs.variable(), 1);
1023  // Add the constraint f^i(x)~0.
1024  smtrat::ConstraintT inequality = smtrat::ConstraintT( deriv, _relation );
1025  // Apply the substitution (without epsilon) to the new constraints.
1026  substitutionResultsVector.emplace_back();
1027  if( !substituteNormal( equation, substitution, substitutionResultsVector.back(), _accordingPaper, _conflictingVariables, _solutionSpace ) )
1028  return false;
1029  substitutionResultsVector.emplace_back();
1030  if( !substituteNormal( inequality, substitution, substitutionResultsVector.back(), _accordingPaper, _conflictingVariables, _solutionSpace ) )
1031  return false;
1032  if( !combine( substitutionResultsVector, _result ) )
1033  return false;
1034  simplify( _result, _conflictingVariables, _solutionSpace );
1035  // Remove the last substitution result.
1036  substitutionResultsVector.pop_back();
1037  }
1038  return true;
1039  }
1040 
1041  void substituteInf( const smtrat::ConstraintT& _cons, const Substitution& _subs, DisjunctionOfConstraintConjunctions& _result, Variables& _conflictingVariables, const smtrat::EvalDoubleIntervalMap& _solutionSpace )
1042  {
1043  if( !_cons.variables().empty() )
1044  {
1045  if( _cons.variables().has( _subs.variable() ) )
1046  {
1047  if( _cons.relation() == Relation::EQ )
1048  substituteTrivialCase( _cons, _subs, _result );
1049  else if( _cons.relation() == Relation::NEQ )
1050  substituteNotTrivialCase( _cons, _subs, _result );
1051  else
1052 
1053  substituteInfLessGreater( _cons, _subs, _result );
1054  simplify( _result, _conflictingVariables, _solutionSpace );
1055  }
1056  else
1057  {
1058  _result.emplace_back();
1059  _result.back().push_back( _cons );
1060  }
1061  }
1062  else
1063  std::cout << "Warning in substituteInf: The chosen constraint has no variable" << std::endl;
1064  }
1065 
1066  void substituteInfLessGreater( const smtrat::ConstraintT& _cons, const Substitution& _subs, DisjunctionOfConstraintConjunctions& _result )
1067  {
1068  assert( _cons.relation() != Relation::EQ );
1069  assert( _cons.relation() != Relation::NEQ );
1070  // Determine the relation for the coefficients of the odd and even degrees.
1071  Relation oddRelationType = Relation::GREATER;
1072  Relation evenRelationType = Relation::LESS;
1073  if( _subs.type() == Substitution::MINUS_INFINITY )
1074  {
1075  if( _cons.relation() == Relation::GREATER || _cons.relation() == Relation::GEQ )
1076  {
1077  oddRelationType = Relation::LESS;
1078  evenRelationType = Relation::GREATER;
1079  }
1080  }
1081  else
1082  {
1083  assert( _subs.type() == Substitution::PLUS_INFINITY );
1084  if( _cons.relation() == Relation::LESS || _cons.relation() == Relation::LEQ )
1085  {
1086  oddRelationType = Relation::LESS;
1087  evenRelationType = Relation::GREATER;
1088  }
1089  }
1090  // Check all cases according to the substitution rules.
1091  carl::uint varDegree = _cons.maxDegree( _subs.variable() );
1092  assert( varDegree > 0 );
1093  for( carl::uint i = varDegree + 1; i > 0; --i )
1094  {
1095  // Add conjunction (a_n=0 and ... and a_i~0) to the substitution result.
1096  _result.emplace_back();
1097  for( carl::uint j = varDegree; j > i - 1; --j )
1098  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), j ), Relation::EQ ) );
1099  if( i > 1 )
1100  {
1101  if( fmod( i - 1, 2.0 ) != 0.0 )
1102  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), i - 1 ), oddRelationType ) );
1103  else
1104  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), i - 1 ), evenRelationType ) );
1105  }
1106  else
1107  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), i - 1 ), _cons.relation() ) );
1108  }
1109  }
1110 
1111  void substituteTrivialCase( const smtrat::ConstraintT& _cons, const Substitution& _subs, DisjunctionOfConstraintConjunctions& _result )
1112  {
1113  assert( _cons.relation() == Relation::EQ || _cons.relation() == Relation::LEQ || _cons.relation() == Relation::GEQ );
1114  carl::uint varDegree = _cons.maxDegree( _subs.variable() );
1115  // Check the cases (a_0=0 and ... and a_n=0)
1116  _result.emplace_back();
1117  for( carl::uint i = 0; i <= varDegree; ++i )
1118  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), i ), Relation::EQ ) );
1119  }
1120 
1121  void substituteNotTrivialCase( const smtrat::ConstraintT& _cons, const Substitution& _subs, DisjunctionOfConstraintConjunctions& _result )
1122  {
1123  assert( _cons.relation() == Relation::NEQ );
1124  carl::uint varDegree = _cons.maxDegree( _subs.variable() );
1125  for( carl::uint i = 0; i <= varDegree; ++i )
1126  {
1127  // Add conjunction (a_i!=0) to the substitution result.
1128  _result.emplace_back();
1129  _result.back().push_back( smtrat::ConstraintT( _cons.coefficient( _subs.variable(), i ), Relation::NEQ ) );
1130  }
1131  }
1132 } // end namspace vs
1133 }
MAX_NUM_OF_TERMS
const unsigned MAX_NUM_OF_TERMS
Class containing a method applying a virtual substitution.
Definition: Substitute.cpp:18
MAX_PRODUCT_SPLIT_NUMBER
const unsigned MAX_PRODUCT_SPLIT_NUMBER
Class containing a method applying a virtual substitution.
Definition: Substitute.h:19
smtrat::vs::Substitution::term
const smtrat::SqrtEx & term() const
Definition: Substitution.h:83
smtrat::vs::Substitution::variable
const carl::Variable & variable() const
Definition: Substitution.h:75
smtrat::vs::Substitution::originalConditions
const carl::PointerSet< Condition > & originalConditions() const
Definition: Substitution.h:126
smtrat::vs::Substitution::type
const Type & type() const
Definition: Substitution.h:110
smtrat::cadcells::operators::rules::filter_util::result
result
Definition: rules_filter_util.h:72
smtrat::covering_ng::formula::formula_ds::EQ
@ EQ
Definition: FormulaEvaluationGraph.cpp:203
smtrat::qe::vars
std::vector< carl::Variable > vars(const std::pair< QuantifierType, std::vector< carl::Variable >> &p)
Definition: QEQuery.h:43
smtrat::vs::substituteNormalSqrtNeq
bool substituteNormalSqrtNeq(const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square...
Definition: Substitute.cpp:772
smtrat::vs::combine
bool combine(const std::vector< std::vector< std::vector< combineType > > > &_toCombine, std::vector< std::vector< combineType > > &_combination)
Combines vectors.
Definition: Substitute.h:44
smtrat::vs::substituteInfLessGreater
void substituteInfLessGreater(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result)
Applies the given substitution to the given constraint, where the substitution is of the form [x -> +...
Definition: Substitute.cpp:1066
smtrat::vs::substituteNormal
bool substituteNormal(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:608
smtrat::vs::substituteNormalSqrtLeq
bool substituteNormalSqrtLeq(const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, const smtrat::Poly &_s, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square...
Definition: Substitute.cpp:869
smtrat::vs::substituteEpsGradients
bool substituteEpsGradients(const smtrat::ConstraintT &_cons, const Substitution &_subs, const Relation _relation, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:991
smtrat::vs::getEvenBitStrings
void getEvenBitStrings(std::size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
Definition: Substitute.cpp:512
smtrat::vs::substituteNormalSqrtLess
bool substituteNormalSqrtLess(const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, const smtrat::Poly &_s, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square...
Definition: Substitute.cpp:806
smtrat::vs::splitProducts
DisjunctionOfConstraintConjunctions splitProducts(const smtrat::ConstraintT &_constraint, bool _onlyNeq)
Splits the given constraint into a set of constraints which compare the factors of the factorization ...
Definition: Substitute.cpp:204
smtrat::vs::substituteInf
void substituteInf(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:1041
smtrat::vs::substituteNotTrivialCase
void substituteNotTrivialCase(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result)
Deals with the case, that the left hand side of the constraint to substitute is not a trivial polynom...
Definition: Substitute.cpp:1121
smtrat::vs::DisjunctionOfConstraintConjunctions
std::vector< ConstraintVector > DisjunctionOfConstraintConjunctions
a vector of vectors of constraints
Definition: Substitute.h:33
smtrat::vs::splitSosDecompositions
void splitSosDecompositions(DisjunctionOfConstraintConjunctions &_toSimplify)
Definition: Substitute.cpp:262
smtrat::vs::simplify
void simplify(DisjunctionOfConstraintConjunctions &_toSimplify, Variables &_conflictingVars, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:59
smtrat::vs::ConstraintVector
std::vector< smtrat::ConstraintT > ConstraintVector
a vector of constraints
Definition: Substitute.h:31
smtrat::vs::substitutePlusEps
bool substitutePlusEps(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:926
smtrat::vs::substitute
bool substitute(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper, Variables &_conflictingVariables, const smtrat::EvalDoubleIntervalMap &_solutionSpace)
Definition: Substitute.cpp:553
smtrat::vs::getSignCombinations
DisjunctionOfConstraintConjunctions getSignCombinations(const smtrat::ConstraintT &_constraint)
For a given constraint f_1*...*f_n ~ 0 this method computes all combinations of constraints f_1 ~_1 0...
Definition: Substitute.cpp:397
smtrat::vs::substituteNormalSqrtEq
bool substituteNormalSqrtEq(const smtrat::Poly &_radicand, const smtrat::Poly &_q, const smtrat::Poly &_r, DisjunctionOfConstraintConjunctions &_result, bool _accordingPaper)
Sub-method of substituteNormalSqrt, where applying the substitution led to a term containing a square...
Definition: Substitute.cpp:731
smtrat::vs::substituteTrivialCase
void substituteTrivialCase(const smtrat::ConstraintT &_cons, const Substitution &_subs, DisjunctionOfConstraintConjunctions &_result)
Deals with the case, that the left hand side of the constraint to substitute is a trivial polynomial ...
Definition: Substitute.cpp:1111
smtrat::vs::print
void print(DisjunctionOfConstraintConjunctions &_substitutionResults)
Prints the given disjunction of conjunction of constraints.
Definition: Substitute.cpp:530
smtrat::vs::getOddBitStrings
void getOddBitStrings(std::size_t _length, std::vector< std::bitset< MAX_PRODUCT_SPLIT_NUMBER > > &_strings)
Definition: Substitute.cpp:494
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::NORMAL
@ NORMAL
Definition: types.h:53
smtrat::SqrtEx
carl::SqrtEx< Poly > SqrtEx
Definition: model.h:22
smtrat::Poly
carl::MultivariatePolynomial< Rational > Poly
Definition: types.h:25
smtrat::ConstraintT
carl::Constraint< Poly > ConstraintT
Definition: types.h:29
smtrat::Rational
mpq_class Rational
Definition: types.h:19
smtrat::EvalDoubleIntervalMap
std::map< carl::Variable, DoubleInterval > EvalDoubleIntervalMap
Definition: model.h:29