SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
IntBlastModule.tpp
Go to the documentation of this file.
1 /**
2  * @file IntBlastModule.tpp
3  * @author Andreas Krueger <andreas.krueger@rwth-aachen.de>
4  * @author Florian Corzilius <corzilius@cs.rwth-aachen.de>
5  */
6 
7 #include "IntBlastModule.h"
8 
9 #define INTBLAST_DEBUG_ENABLED 0
10 #define INTBLAST_DEBUG(x) do { \
11  if (INTBLAST_DEBUG_ENABLED) { std::cout << "[IntBlast] " << x << std::endl; } \
12 } while (0)
13 
14 namespace smtrat
15 {
16  /**
17  * Constructors.
18  */
19 
20  template<class Settings>
21  IntBlastModule<Settings>::IntBlastModule( const ModuleInput* _formula, Conditionals& _conditionals, Manager* _manager ):
22  Module( _formula, _conditionals, _manager ),
23  mBoundsFromInput(),
24  mBoundsInRestriction(),
25  mInputVariables(),
26  mNonlinearInputVariables(),
27  mpICPInput(new ModuleInput()),
28  mICPFoundAnswer( std::vector< std::atomic_bool* >( 1, new std::atomic_bool( false ) ) ),
29  mICP(mpICPInput, mICPFoundAnswer),
30  mConstraintFromBounds(carl::fresh_boolean_variable()),
31  mProcessedFormulasFromICP(),
32  mpBVInput(new ModuleInput()),
33  mpBVSolver(new BVSolver()),
34  mFormulasToEncode(),
35  mSolutionOrigin(SolutionOrigin::NONE),
36  mPolyBlastings(),
37  mConstrBlastings(),
38  mSubstitutes(),
39  mPolyParents(),
40  mShrunkPolys()
41  {
42  // TODO: Do we have to do some more initialization stuff here? Settings?
43  }
44 
45  /**
46  * Destructor.
47  */
48 
49  template<class Settings>
50  IntBlastModule<Settings>::~IntBlastModule()
51  {
52  delete mpICPInput;
53  while( !mICPFoundAnswer.empty() )
54  {
55  std::atomic_bool* toDel = mICPFoundAnswer.back();
56  mICPFoundAnswer.pop_back();
57  delete toDel;
58  }
59  mICPFoundAnswer.clear();
60 
61  delete mpBVSolver;
62  delete mpBVInput;
63  };
64 
65  template<class Settings>
66  bool IntBlastModule<Settings>::informCore( const FormulaT& _constraint )
67  {
68  informBackends(_constraint);
69  return true;
70  }
71 
72  template<class Settings>
73  void IntBlastModule<Settings>::init()
74  {}
75 
76  template<class Settings>
77  bool IntBlastModule<Settings>::addCore( ModuleInput::const_iterator _subformula )
78  {
79  const FormulaT& formula = _subformula->formula();
80  INTBLAST_DEBUG("ADD " << formula);
81 
82  std::vector<ConstraintT> containedConstraints;
83  carl::arithmetic_constraints(formula, containedConstraints);
84 
85  /*
86  * Steps that are applied for every constraint in formula
87  */
88 
89  for(const ConstraintT& constraint : containedConstraints) {
90  // Retrieve all arithmetic variables in formula
91  carl::carlVariables nonlinearVariablesInFormula;
92  const Poly& poly = constraint.lhs();
93  carl::Variables variablesInFormula = carl::arithmetic_variables(formula).as_set();
94  for(auto termIt = poly.begin();termIt != poly.end();++termIt) {
95  if(termIt->num_variables() > 1 || ! termIt->is_linear()) {
96  carl::variables(*termIt, nonlinearVariablesInFormula);
97  }
98  }
99 
100  // Update 'mInputVariables' and 'mNonlinearInputVariables' sets
101  for(auto& variable : variablesInFormula) {
102  mInputVariables.add(variable, formula);
103  }
104  for(auto& variable : nonlinearVariablesInFormula) {
105  mNonlinearInputVariables.add(variable, formula);
106  }
107 
108  // Introduce substitutes in ICP
109  if(Settings::apply_icp) {
110  addSubstitutesToICP(constraint, formula);
111  }
112 
113  // Update mPolyParents (child->parent relationship)
114  addPolyParents(constraint);
115  }
116 
117  /*
118  * Steps that are applied if the formula is only a single constraint
119  */
120 
121  if(formula.type() == carl::FormulaType::CONSTRAINT) {
122  // Update mBoundsFromInput using the new formula
123  mBoundsFromInput.addBound(formula.constraint(), formula);
124 
125  // Pass global formula to ICP
126  if(Settings::apply_icp) {
127  addConstraintFormulaToICP(formula);
128  }
129  }
130 
131  /*
132  * Steps that are applied for the whole formula
133  */
134 
135  // Schedule formula for encoding to BV logic
136  mFormulasToEncode.insert(formula);
137 
138  // Add new formula to backend
139  addReceivedSubformulaToPassedFormula(_subformula);
140 
141  return ! mBoundsFromInput.isConflicting();
142  }
143 
144  template<class Settings>
145  void IntBlastModule<Settings>::removeCore( ModuleInput::const_iterator _subformula )
146  {
147  const FormulaT& formula = _subformula->formula();
148  INTBLAST_DEBUG("REMOVE " << formula);
149 
150  mInputVariables.removeOrigin(formula);
151  mNonlinearInputVariables.removeOrigin(formula);
152 
153  if(formula.type() == carl::FormulaType::CONSTRAINT) {
154  mBoundsFromInput.removeBound(formula.constraint(), formula);
155  }
156  // mBoundsInRestriction: updated by updateBoundsFromICP() in next check
157 
158  if(Settings::apply_icp) {
159  removeOriginFromICP(formula);
160  }
161  removeOriginFromBV(formula);
162 
163  mFormulasToEncode.erase(formula);
164  }
165 
166  template<class Settings>
167  void IntBlastModule<Settings>::updateModel() const
168  {
169  mModel.clear();
170  if(solverState() == SAT)
171  {
172  switch(mSolutionOrigin) {
173  case SolutionOrigin::ICP:
174  updateModelFromICP();
175  break;
176  case SolutionOrigin::BV:
177  updateModelFromBV();
178  break;
179  case SolutionOrigin::BACKEND:
180  getBackendsModel();
181  break;
182  default:
183  assert(false);
184  }
185  }
186  }
187 
188  template<class Settings>
189  carl::BVTerm IntBlastModule<Settings>::encodeBVConstant(const Integer& _constant, const BVAnnotation& _type) const
190  {
191  assert(_constant >= _type.lower_bound() && _constant <= _type.upper_bound());
192  carl::BVValue constValue(_type.width(), _constant - _type.offset());
193  return carl::BVTerm(carl::BVTermType::CONSTANT, constValue);
194  }
195 
196  template<class Settings>
197  Integer IntBlastModule<Settings>::decodeBVConstant(const carl::BVValue& _value, const BVAnnotation& _type) const
198  {
199  Integer summand(1);
200  Integer converted(0);
201 
202  // Unsigned conversion from binary to integer
203  for(std::size_t position = 0;position<_value.width();++position) {
204  if(_value[position]) {
205  converted += summand;
206  }
207  summand *= Integer(2);
208  }
209 
210  // For negative numbers in two's complement, subtract 2^width from result
211  if(_type.isSigned() && _value[_value.width()-1]) {
212  converted -= summand;
213  }
214 
215  return converted + _type.offset();
216  }
217 
218  template<class Settings>
219  carl::BVTerm IntBlastModule<Settings>::resizeBVTerm(const AnnotatedBVTerm& _term, std::size_t _width) const
220  {
221  assert(_width >= _term.type().width());
222 
223  if(_width == _term.type().width()) {
224  return _term.term();
225  } else {
226  carl::BVTermType ext = (_term.type().isSigned() ? carl::BVTermType::EXT_S : carl::BVTermType::EXT_U);
227  return carl::BVTerm(ext, _term.term(), _width - _term.type().width());
228  }
229  }
230 
231  template<class Settings>
232  BlastedPoly IntBlastModule<Settings>::blastSum(const BlastedPoly& _summand1, const BlastedPoly& _summand2)
233  {
234  if(_summand1.is_constant() && _summand2.is_constant()) {
235  return BlastedPoly(_summand1.constant() + _summand2.constant());
236  } else if(_summand1.is_constant() || _summand2.is_constant()) {
237  const BlastedPoly& constantSummand = (_summand1.is_constant() ? _summand1 : _summand2);
238  const BlastedPoly& termSummand = (_summand1.is_constant() ? _summand2 : _summand1);
239  const BVAnnotation& termType = termSummand.term().type();
240 
241  return BlastedPoly(AnnotatedBVTerm(termType.withOffset(termType.offset() + constantSummand.constant()), termSummand.term().term()));
242  } else {
243  BVAnnotation annotation = BVAnnotation::forSum(_summand1.term().type(), _summand2.term().type());
244 
245  carl::BVTerm bvSummand1 = resizeBVTerm(_summand1.term(), annotation.width());
246  carl::BVTerm bvSummand2 = resizeBVTerm(_summand2.term(), annotation.width());
247  carl::BVTerm bvSum(carl::BVTermType::ADD, bvSummand1, bvSummand2);
248 
249  if(Settings::allow_encoding_into_complex_bvterms) {
250  return BlastedPoly(AnnotatedBVTerm(annotation, bvSum), FormulasT());
251  } else {
252  AnnotatedBVTerm sum(annotation);
253  FormulasT constraints;
254  constraints.push_back(FormulaT(carl::BVConstraint::create(carl::BVCompareRelation::EQ, bvSum, sum.term())));
255  return BlastedPoly(sum, constraints);
256  }
257  }
258  }
259 
260  template<class Settings>
261  BlastedPoly IntBlastModule<Settings>::blastProduct(const BlastedPoly& _factor1, const BlastedPoly& _factor2)
262  {
263  if(_factor1.is_constant() && _factor2.is_constant()) {
264  return BlastedPoly(_factor1.constant() * _factor2.constant());
265  } else if(_factor1.is_constant() || _factor2.is_constant()) {
266  const BlastedPoly& constantFactor = (_factor1.is_constant() ? _factor1 : _factor2);
267  const BlastedPoly& variableFactor = (_factor1.is_constant() ? _factor2 : _factor1);
268  const BVAnnotation& variableType = variableFactor.term().type();
269 
270  bool constantNegative = constantFactor.constant() < 0;
271  BVAnnotation constantType(chooseWidth(constantFactor.constant(), 0, constantNegative), constantNegative, 0);
272  BVAnnotation annotation = BVAnnotation::forProduct(variableType.withOffset(0), constantType).withOffset(variableType.offset() * constantFactor.constant());
273 
274  carl::BVTerm bvConstantFactor = encodeBVConstant(constantFactor.constant(), annotation);
275  carl::BVTerm bvVariableFactor = resizeBVTerm(variableFactor.term(), annotation.width());
276  carl::BVTerm bvProduct(carl::BVTermType::MUL, bvConstantFactor, bvVariableFactor);
277 
278  if(Settings::allow_encoding_into_complex_bvterms) {
279  return BlastedPoly(AnnotatedBVTerm(annotation, bvProduct), FormulasT());
280  } else {
281  AnnotatedBVTerm product(annotation);
282  FormulasT constraints;
283  constraints.push_back(FormulaT(carl::BVConstraint::create(carl::BVCompareRelation::EQ, bvProduct, product.term())));
284  return BlastedPoly(product, constraints);
285  }
286  } else {
287  BVAnnotation annotation = BVAnnotation::forProduct(_factor1.term().type(), _factor2.term().type());
288 
289  carl::BVTerm bvFactor1 = resizeBVTerm(_factor1.term(), annotation.width());
290  carl::BVTerm bvFactor2 = resizeBVTerm(_factor2.term(), annotation.width());
291  carl::BVTerm bvProduct(carl::BVTermType::MUL, bvFactor1, bvFactor2);
292 
293  if(Settings::allow_encoding_into_complex_bvterms) {
294  return BlastedPoly(AnnotatedBVTerm(annotation, bvProduct), FormulasT());
295  } else {
296  AnnotatedBVTerm product(annotation);
297  FormulasT constraints;
298  constraints.push_back(FormulaT(carl::BVConstraint::create(carl::BVCompareRelation::EQ, bvProduct, product.term())));
299  return BlastedPoly(product, constraints);
300  }
301  }
302  }
303 
304  template<class Settings>
305  const BlastedConstr& IntBlastModule<Settings>::blastConstrTree(const ConstrTree& _constraint, FormulasT& _collectedFormulas)
306  {
307  const BlastedPoly& left = blastPolyTree(_constraint.left(), _collectedFormulas);
308  const BlastedPoly& right = blastPolyTree(_constraint.right(), _collectedFormulas);
309 
310  auto blastedConstrIt = mConstrBlastings.find(_constraint.constraint());
311 
312  if(blastedConstrIt != mConstrBlastings.end()) {
313  // This tree has already been encoded. Add its formulas to _collectedFormulas
314  // and return the previously blasted node.
315  const FormulasT& constraints = blastedConstrIt->second.constraints();
316  _collectedFormulas.insert(_collectedFormulas.end(), constraints.begin(), constraints.end());
317  return blastedConstrIt->second;
318  }
319 
320  BlastedConstr blasted;
321  bool simpleBlast = false;
322 
323  if(left.is_constant() && right.is_constant()) {
324  blasted = BlastedConstr(evaluateRelation(_constraint.relation(), left.constant(), right.constant()));
325  simpleBlast = true;
326  } else {
327  assert(left.is_constant() || right.is_constant()); // Our ConstrTree is constructed like that
328 
329  const BlastedPoly& constantPol = left.is_constant() ? left : right;
330  const BlastedPoly& variablePol = left.is_constant() ? right : left;
331  const Integer& constant = constantPol.constant();
332 
333  // Assuming "variable op constant" now (i.e., constant is on the right side)
334  carl::Relation relation = left.is_constant() ? carl::turn_around(_constraint.relation()) : _constraint.relation();
335 
336  if(relation == carl::Relation::EQ || relation == carl::Relation::NEQ) {
337  // is the constant outside the range of the variable?
338  if(constant < variablePol.lower_bound() || constant > variablePol.upper_bound()) {
339  blasted = BlastedConstr(_constraint.relation() == carl::Relation::NEQ);
340  simpleBlast = true;
341  }
342  } else { // relation is one of LESS, GREATER, LEQ, GEQ
343  bool lowerEvaluation = evaluateRelation(_constraint.relation(), left.lower_bound(), constant);
344  bool upperEvaluation = evaluateRelation(_constraint.relation(), left.upper_bound(), constant);
345 
346  if(lowerEvaluation == upperEvaluation) {
347  blasted = BlastedConstr(lowerEvaluation);
348  simpleBlast = true;
349  }
350  }
351 
352  if(! simpleBlast) {
353  // The constraint cannot be decided from the range of variablePol alone.
354  // Translate into BV logic
355 
356  carl::BVTerm bvConstant = encodeBVConstant(constantPol.constant(), variablePol.term().type());
357 
358  carl::BVCompareRelation rel;
359 
360  switch(relation) {
361  case carl::Relation::EQ:
362  rel = carl::BVCompareRelation::EQ;
363  break;
364  case carl::Relation::NEQ:
365  rel = carl::BVCompareRelation::NEQ;
366  break;
367  case carl::Relation::LESS:
368  rel = (variablePol.term().type().isSigned() ? carl::BVCompareRelation::SLT : carl::BVCompareRelation::ULT);
369  break;
370  case carl::Relation::GREATER:
371  rel = (variablePol.term().type().isSigned() ? carl::BVCompareRelation::SGT : carl::BVCompareRelation::UGT);
372  break;
373  case carl::Relation::LEQ:
374  rel = (variablePol.term().type().isSigned() ? carl::BVCompareRelation::SLE : carl::BVCompareRelation::ULE);
375  break;
376  case carl::Relation::GEQ:
377  rel = (variablePol.term().type().isSigned() ? carl::BVCompareRelation::SGE : carl::BVCompareRelation::UGE);
378  break;
379  default:
380  assert(false);
381  }
382 
383  blasted = BlastedConstr(FormulaT(carl::BVConstraint::create(rel, left.term().term(), bvConstant)));
384  }
385  }
386 
387  _collectedFormulas.insert(_collectedFormulas.end(), blasted.constraints().begin(), blasted.constraints().end());
388  return mConstrBlastings.insert(std::make_pair(_constraint.constraint(), blasted)).first->second;
389  }
390 
391  template<class Settings>
392  bool IntBlastModule<Settings>::evaluateRelation(carl::Relation _relation, const Integer& _first, const Integer& _second) const
393  {
394  switch(_relation) {
395  case carl::Relation::EQ: return _first == _second;
396  case carl::Relation::NEQ: return _first != _second;
397  case carl::Relation::LESS: return _first < _second;
398  case carl::Relation::GREATER: return _first > _second;
399  case carl::Relation::LEQ: return _first <= _second;
400  case carl::Relation::GEQ: return _first >= _second;
401  }
402  assert(false);
403  return false;
404  }
405 
406  template<class Settings>
407  const BlastedPoly& IntBlastModule<Settings>::blastPolyTree(const PolyTree& _poly, FormulasT& _collectedFormulas)
408  {
409  const BlastedPoly* left = nullptr;
410  const BlastedPoly* right = nullptr;
411 
412  if(_poly.type() == PolyTree::Type::SUM || _poly.type() == PolyTree::Type::PRODUCT) {
413  left = &(blastPolyTree(_poly.left(), _collectedFormulas));
414  right = &(blastPolyTree(_poly.right(), _collectedFormulas));
415  }
416 
417  auto blastedPolyIt = mPolyBlastings.find(_poly.poly());
418 
419  if(blastedPolyIt != mPolyBlastings.end()) {
420  // This tree has already been encoded. Add its formulas to _collectedFormulas
421  // and return the previously blasted node.
422  const FormulasT& constraints = blastedPolyIt->second.constraints();
423  _collectedFormulas.insert(_collectedFormulas.end(), constraints.begin(), constraints.end());
424  return blastedPolyIt->second;
425  }
426 
427  // Tree has not yet been encoded (only its subtrees, if any).
428 
429  BlastedPoly blasted;
430 
431  switch(_poly.type()) {
432  case PolyTree::Type::CONSTANT: {
433  blasted = BlastedPoly(_poly.constant());
434  break;
435  }
436  case PolyTree::Type::VARIABLE: {
437  // This should not happen.
438  // Variables should have been blasted by 'blastVariable' method upfront.
439  assert(false);
440  break;
441  }
442  case PolyTree::Type::SUM:
443  case PolyTree::Type::PRODUCT: {
444  BlastedPoly intermediate = (_poly.type() == PolyTree::Type::SUM) ?
445  blastSum(*left, *right) :
446  blastProduct(*left, *right);
447 
448  if(Settings::apply_icp) {
449  // Obtain range from ICP substitute
450  carl::Variable substitute = mSubstitutes.at(_poly.poly());
451  IntegerInterval interval = get_num(mBoundsInRestriction.getInterval(substitute));
452  if(interval.lower_bound_type() == carl::BoundType::WEAK && interval.upper_bound_type() == carl::BoundType::WEAK) {
453  auto shrunk = shrinkToRange(intermediate, interval);
454  blasted = shrunk.first;
455  if(shrunk.second) {
456  mShrunkPolys.insert(_poly.poly());
457  }
458  } else {
459  INTBLAST_DEBUG("Bad ICP interval for " << _poly.poly() << ": " << interval);
460  // assert(false);
461  blasted = intermediate;
462  }
463  } else {
464  blasted = intermediate;
465  }
466 
467  break;
468  }
469  default: {
470  assert(false);
471  }
472  }
473 
474  _collectedFormulas.insert(_collectedFormulas.end(), blasted.constraints().begin(), blasted.constraints().end());
475  return mPolyBlastings.insert(std::make_pair(_poly.poly(), blasted)).first->second;
476  }
477 
478  template<class Settings>
479  std::pair<BlastedPoly, bool> IntBlastModule<Settings>::shrinkToRange(const BlastedPoly& _input, const IntegerInterval& _interval) const
480  {
481  if(_interval.lower_bound_type() != carl::BoundType::WEAK || _interval.upper_bound_type() != carl::BoundType::WEAK) {
482  assert(false);
483  }
484 
485  assert(_input.lower_bound() <= _interval.lower() && _input.upper_bound() >= _interval.upper());
486 
487  if(_interval.is_point_interval()) {
488  if(_input.is_constant()) {
489  return std::make_pair(_input, false);
490  } else {
491  FormulasT constraints(_input.constraints());
492  carl::BVTerm bvConstant = encodeBVConstant(_interval.lower(), _input.term().type());
493  constraints.push_back(FormulaT(carl::BVConstraint::create(carl::BVCompareRelation::EQ, _input.term().term(), bvConstant)));
494  return std::make_pair(BlastedPoly(_interval.lower(), constraints), true);
495  }
496  }
497 
498  // Interval is not a point interval, and interval is included in _input interval.
499  // This also implies that _input is not constant.
500  // Let's see whether resizing actually has any benefits.
501 
502  const BVAnnotation& inputType = _input.term().type();
503 
504  std::size_t newWidth = std::max(
505  chooseWidth(_interval.lower() - inputType.offset(), 0, inputType.isSigned()),
506  chooseWidth(_interval.upper() - inputType.offset(), 0, inputType.isSigned())
507  );
508 
509  assert(newWidth <= inputType.width());
510  if(newWidth == inputType.width()) {
511  // Resizing is not possible, return _input without modifications
512  return std::make_pair(_input, false);
513  }
514 
515  // Resize to a new, smaller BlastedPoly
516  FormulasT constraints(_input.constraints());
517  AnnotatedBVTerm newTerm(inputType.withWidth(newWidth));
518 
519  constraints.push_back(FormulaT(carl::BVConstraint::create(carl::BVCompareRelation::EQ,
520  carl::BVTerm(carl::BVTermType::EXTRACT, _input.term().term(), newWidth-1, 0),
521  newTerm.term())));
522 
523  // add constraint which ensures a safe resizing
524  carl::BVTermType extend = inputType.isSigned() ? carl::BVTermType::EXT_S : carl::BVTermType::EXT_U;
525  constraints.push_back(FormulaT(carl::BVConstraint::create(
526  carl::BVCompareRelation::EQ,
527  carl::BVTerm(extend, newTerm.term(), inputType.width() - newWidth),
528  _input.term().term()
529  )));
530 
531  return std::make_pair(BlastedPoly(newTerm, constraints), true);
532  }
533 
534  template<class Settings>
535  FormulasT IntBlastModule<Settings>::blastConstraint(const ConstraintT& _constraint)
536  {
537  ConstrTree constraintTree(_constraint);
538  FormulasT blastedFormulas;
539 
540  blastConstrTree(constraintTree, blastedFormulas);
541  return blastedFormulas;
542  }
543 
544  template<class Settings>
545  Answer IntBlastModule<Settings>::checkCore()
546  {
547  mSolutionOrigin = SolutionOrigin::NONE;
548 
549  // Choose blastings for new variables,
550  // and ensure compatibility of previous blastings for all variables
551 
552  bool reachedMaxWidth = false;
553  for(auto variableWO : mInputVariables)
554  {
555  const carl::Variable& variable = variableWO.element();
556  bool linear = ! mNonlinearInputVariables.contains(variable);
557  IntegerInterval interval = get_num(mBoundsFromInput.getInterval(variable));
558 
559  Poly variablePoly(variable);
560  auto blastingIt = mPolyBlastings.find(variablePoly);
561  bool needsBlasting = (blastingIt == mPolyBlastings.end() || reblastingNeeded(blastingIt->second, interval, linear));
562 
563  if(needsBlasting)
564  {
565  if(blastingIt != mPolyBlastings.end()) {
566  unblastVariable(variable);
567  }
568  switch( blastVariable(variable, interval, linear) )
569  {
570  case -1:
571  return callBackends();
572  case 0:
573  reachedMaxWidth = true;
574  break;
575  default:
576  break;
577  }
578  }
579  }
580 
581  if(INTBLAST_DEBUG_ENABLED) {
582  INTBLAST_DEBUG("Blastings:");
583  for(auto blaPa : mPolyBlastings) {
584  INTBLAST_DEBUG(blaPa.first << " --> " << blaPa.second);
585  }
586 
587  INTBLAST_DEBUG("Substitutes:");
588  for(auto substi : mSubstitutes) {
589  INTBLAST_DEBUG(substi.first << " --> " << substi.second);
590  }
591  }
592 
593  Answer icpAnswer = UNKNOWN;
594 
595  if(Settings::apply_icp) {
596  // Run ICP
597  if(INTBLAST_DEBUG_ENABLED) {
598  INTBLAST_DEBUG("Running ICP on these formulas:");
599 
600  for(const auto& formulaWO : *mpICPInput) {
601  INTBLAST_DEBUG(" - " << formulaWO.formula());
602  for(const auto& origin : formulaWO.origins()) {
603  INTBLAST_DEBUG(" (o) " << origin);
604  }
605  }
606  }
607  icpAnswer = mICP.check();
608  INTBLAST_DEBUG("icpAnswer: " << icpAnswer);
609 
610  if(icpAnswer == SAT && rReceivedFormula().satisfiedBy( mICP.model() ) == 1) {
611  mSolutionOrigin = SolutionOrigin::ICP;
612  return SAT;
613  }
614  }
615 
616  if(icpAnswer != UNSAT) {
617  if(Settings::apply_icp) {
618  INTBLAST_DEBUG("Updating bounds from ICP.");
619 
620  updateBoundsFromICP();
621  }
622 
623  while(! mFormulasToEncode.empty()) {
624  auto firstFormulaToEncode = mFormulasToEncode.begin();
625  const FormulaT& formulaToEncode = *firstFormulaToEncode;
626  encodeFormulaToBV(formulaToEncode);
627  mFormulasToEncode.erase(firstFormulaToEncode);
628  }
629 
630  INTBLAST_DEBUG("Running BV solver.");
631 
632  Answer bvAnswer = mpBVSolver->check();
633  INTBLAST_DEBUG("Answer from BV solver: " << bvAnswer);
634 
635  if(bvAnswer == SAT) {
636  mSolutionOrigin = SolutionOrigin::BV;
637  return SAT;
638  }
639  }
640 
641  // At this point, the restriction is unsatisfiable
642  // (determined either by the ICP module or by the BV solver).
643  // Call backend
644 
645  if( reachedMaxWidth )
646  {
647  //updateOutsideRestrictionConstraint(icpAnswer == UNSAT);
648  return callBackends();
649  }
650  if( rReceivedFormula().containsRealVariables() )
651  return UNKNOWN;
652  bool originalBoundsCovered = true;
653  for(auto variableWO : mInputVariables)
654  {
655  const carl::Variable& variable = variableWO.element();
656  IntegerInterval interval = get_num(mBoundsFromInput.getInterval(variable));
657 
658  Poly variablePoly(variable);
659  auto blastingIt = mPolyBlastings.find( Poly(variable) );
660  assert( blastingIt != mPolyBlastings.end() );
661  const carl::Interval<Integer>& blastBounds = blastingIt->second.term().type().bounds();
662  if( blastBounds != interval && !blastBounds.contains( interval ) )
663  {
664  originalBoundsCovered = false;
665  break;
666  }
667  }
668  if( originalBoundsCovered )
669  {
670  generateTrivialInfeasibleSubset();
671  return UNSAT;
672  }
673  return UNKNOWN;
674  }
675 
676  template<class Settings>
677  Answer IntBlastModule<Settings>::callBackends()
678  {
679  INTBLAST_DEBUG("Running backend.");
680  Answer backendAnswer = runBackends();
681  INTBLAST_DEBUG("Answer from backend: " << backendAnswer);
682  mSolutionOrigin = SolutionOrigin::BACKEND;
683 
684  if(backendAnswer == UNSAT) {
685  getInfeasibleSubsets();
686  }
687 
688  return backendAnswer;
689  }
690 
691  template<class Settings>
692  void IntBlastModule<Settings>::encodeFormulaToBV(const FormulaT& _formula)
693  {
694  INTBLAST_DEBUG("Formula " << _formula << " encoded to BV:");
695 
696  FormulasT bitvectorConstraints;
697  std::function<FormulaT(FormulaT)> encodeConstraints = std::bind(&IntBlastModule::encodeConstraintToBV, this, std::placeholders::_1, &bitvectorConstraints);
698  FormulaT bitvectorFormula = carl::visit_result(_formula, encodeConstraints);
699 
700  addFormulaToBV(bitvectorFormula, _formula);
701 
702  for(const FormulaT& bitvectorConstraint : bitvectorConstraints) {
703  addFormulaToBV(bitvectorConstraint, _formula);
704  }
705  }
706 
707  template<class Settings>
708  FormulaT IntBlastModule<Settings>::encodeConstraintToBV(const FormulaT& _original, FormulasT* _collectedBitvectorConstraints)
709  {
710  if(_original.type() == carl::FormulaType::CONSTRAINT && _original.constraint().integer_valued())
711  {
712  ConstrTree constraintTree(_original.constraint());
713  const BlastedConstr& blastedConstraint = blastConstrTree(constraintTree, *_collectedBitvectorConstraints);
714  return blastedConstraint.formula();
715  }
716  return _original;
717  }
718 
719  template<class Settings>
720  bool IntBlastModule<Settings>::reblastingNeeded(const BlastedPoly& _previousBlasting, const IntegerInterval& _interval, bool _linear) const
721  {
722  if(_previousBlasting.is_constant()) {
723  return ! _interval.is_point_interval() || _interval.lower() != _previousBlasting.constant();
724  }
725 
726  const BVAnnotation& previousType = _previousBlasting.term().type();
727 
728  if(previousType.hasOffset() && ! _linear) {
729  return true;
730  }
731  return previousType.bounds() != _interval && !previousType.bounds().contains(_interval);
732  }
733 
734  template<class Settings>
735  void IntBlastModule<Settings>::unblastVariable(const carl::Variable& _variable)
736  {
737  if(Settings::apply_icp) {
738  removeBoundRestrictionsFromICP(_variable);
739  }
740  unblastPoly(Poly(_variable));
741  }
742 
743  template<class Settings>
744  int IntBlastModule<Settings>::blastVariable( const carl::Variable& _variable, const IntegerInterval& _interval, bool _allowOffset )
745  {
746  Poly variablePoly( _variable );
747  if( _interval.is_point_interval() )
748  {
749  mPolyBlastings[variablePoly] = BlastedPoly( _interval.lower() );
750  }
751 
752  std::size_t maxWidth = Settings::max_variable_encoding_width;
753  _allowOffset = _allowOffset && Settings::use_offsets_in_encoding;
754 
755  /*
756  * If interval is unbounded:
757  * Start with no offset, signed, maximum width (tempType)
758  * If offset is not allowed
759  * Remove sign if interval is semi-positive
760  * Else:
761  * If lower bound of interval is higher than tempType's lower bound, shift range using offset and remove sign
762  * (similar for upper bound)
763  *
764  * If interval is bounded:
765  * If offset allowed:
766  * Lower bound as offset, width "as small as possible" (at most maximum width), unsigned
767  * Else:
768  * Make signed iff interval not semipositive
769  * Width "as small as possible" (at most maximum width)
770  */
771 
772  BVAnnotation blastedType;
773  int ret = 1;
774  if( _interval.lower_bound_type() == carl::BoundType::INFTY || _interval.upper_bound_type() == carl::BoundType::INFTY )
775  {
776  if( _allowOffset )
777  {
778  BVAnnotation tempType( maxWidth, true, 0 );
779 
780  if( _interval.lower_bound_type() != carl::BoundType::INFTY && _interval.lower() > tempType.lower_bound() )
781  {
782  blastedType = BVAnnotation( maxWidth, false, _interval.lower() );
783  }
784  else if( _interval.upper_bound_type() != carl::BoundType::INFTY && _interval.upper() < tempType.upper_bound() )
785  {
786  blastedType = BVAnnotation( maxWidth, false, _interval.upper() - (tempType.upper_bound() - tempType.lower_bound()) );
787  }
788  else
789  {
790  blastedType = tempType;
791  }
792  }
793  else
794  {
795  if( maxWidth == 0 )
796  return -1;
797  blastedType = BVAnnotation( maxWidth, !_interval.is_semi_positive(), 0 );
798  }
799  ret = 0;
800  }
801  else
802  {
803  // interval is bounded
804  std::size_t width = 0;
805  if( _allowOffset )
806  {
807  width = chooseWidth( _interval.upper() - _interval.lower(), maxWidth, false );
808  blastedType = BVAnnotation( width, false, _interval.lower() );
809  }
810  else
811  {
812  if( _interval.is_semi_positive() )
813  {
814  width = chooseWidth( _interval.upper(), maxWidth, false );
815  blastedType = BVAnnotation( width, false, 0 );
816  }
817  else // @todo: do something clever, if semi-negative
818  {
819  std::size_t widthForUpper = chooseWidth( _interval.upper(), maxWidth, true );
820  std::size_t widthForLower = chooseWidth(_interval.lower(), maxWidth, true );
821  width = std::max( widthForUpper, widthForLower );
822  blastedType = BVAnnotation( width, true, 0 );
823  }
824  }
825  if( maxWidth > 0 )
826  ret = width <= maxWidth ? 1 : 0;
827  }
828 
829  if( Settings::apply_icp )
830  {
831  addBoundRestrictionsToICP( _variable, blastedType );
832  }
833 
834  mPolyBlastings[variablePoly] = BlastedPoly( AnnotatedBVTerm(blastedType) );
835  return ret;
836  }
837 
838  template<class Settings>
839  void IntBlastModule<Settings>::addBoundRestrictionsToICP(carl::Variable _variable, const BVAnnotation& blastedType)
840  {
841  addFormulaToICP(FormulaT(ConstraintT(_variable, carl::Relation::GEQ, blastedType.lower_bound())), mConstraintFromBounds);
842  addFormulaToICP(FormulaT(ConstraintT(_variable, carl::Relation::LEQ, blastedType.upper_bound())), mConstraintFromBounds);
843  }
844 
845  template<class Settings>
846  void IntBlastModule<Settings>::removeBoundRestrictionsFromICP(carl::Variable _variable)
847  {
848  auto& blastedVariable = mPolyBlastings.at(Poly(_variable));
849 
850  if(! blastedVariable.is_constant()) {
851  const BVAnnotation& blastedType = blastedVariable.term().type();
852 
853  removeFormulaFromICP(FormulaT(ConstraintT(_variable, carl::Relation::GEQ, blastedType.lower_bound())), mConstraintFromBounds);
854  removeFormulaFromICP(FormulaT(ConstraintT(_variable, carl::Relation::LEQ, blastedType.upper_bound())), mConstraintFromBounds);
855  }
856  }
857 
858  template<class Settings>
859  std::size_t IntBlastModule<Settings>::chooseWidth(const Integer& _numberToCover, std::size_t _maxWidth, bool _signed) const
860  {
861  assert(_numberToCover >= 0 || _signed);
862  std::size_t width = 1;
863  carl::Interval<Integer> interval(Integer(_signed ? -1 : 0), Integer(_signed ? 0 : 1));
864  while((width < _maxWidth || _maxWidth == 0) && !interval.contains(_numberToCover)) {
865  ++width;
866  interval.set_lower(interval.lower() * 2);
867  interval.set_upper((interval.upper()+1)*2 - 1);
868  }
869  return width;
870  }
871 
872  template<class Settings>
873  void IntBlastModule<Settings>::updateBoundsFromICP()
874  {
875  for(const FormulaT& formula : mProcessedFormulasFromICP) {
876  mBoundsInRestriction.removeBound(formula.constraint(), formula);
877  }
878  mProcessedFormulasFromICP.clear();
879 
880  for(ModuleInput::const_iterator fwo=mICP.rPassedFormula().begin(); fwo != mICP.rPassedFormula().end(); fwo++) {
881  if(INTBLAST_DEBUG_ENABLED) INTBLAST_DEBUG("from ICP: " << fwo->formula());
882  mBoundsInRestriction.addBound(fwo->formula().constraint(), fwo->formula());
883  mProcessedFormulasFromICP.push_back(fwo->formula());
884  }
885 
886  FormulasT icpBounds = mICP.getCurrentBoxAsFormulas();
887  for( auto& f : icpBounds ) {
888  if(INTBLAST_DEBUG_ENABLED) INTBLAST_DEBUG("from ICP: " << f);
889  mBoundsInRestriction.addBound(f.constraint(), f);
890  mProcessedFormulasFromICP.push_back(f);
891  }
892  recheckShrunkPolys();
893  }
894 
895  template<class Settings>
896  void IntBlastModule<Settings>::updateOutsideRestrictionConstraint(bool _fromICPOnly)
897  {
898  FormulasT outsideConstraints;
899 
900  auto& inputBounds = mBoundsFromInput.getEvalIntervalMap();
901  for(auto& variableWithOrigins : mInputVariables) {
902  const carl::Variable& variable = variableWithOrigins.element();
903  auto& blastedVar = mPolyBlastings.at(Poly(variable));
904  Integer blastedLowerBound = (blastedVar.is_constant() ? blastedVar.constant() : blastedVar.term().type().lower_bound());
905  Integer blastedUpperBound = (blastedVar.is_constant() ? blastedVar.constant() : blastedVar.term().type().upper_bound());
906  auto inputBoundsIt = inputBounds.find(variable);
907 
908  if(inputBoundsIt == inputBounds.end() || get_num(inputBoundsIt->second).contains(blastedLowerBound - 1)) {
909  outsideConstraints.push_back(FormulaT(ConstraintT(variable, carl::Relation::LESS, blastedLowerBound)));
910  }
911 
912  if(inputBoundsIt == inputBounds.end() || get_num(inputBoundsIt->second).contains(blastedUpperBound + 1)) {
913  outsideConstraints.push_back(FormulaT(ConstraintT(variable, carl::Relation::GREATER, blastedUpperBound)));
914  }
915  }
916 
917  FormulaT newOutsideConstraint(carl::FormulaType::OR, outsideConstraints);
918 
919  // Construct origins of the "outside restriction" constraint.
920  // They should be picked in a suitable way for the infeasible subset derivation.
921 
922  // If the ICP module has returned UNSAT, we can use the infeasible subset from ICP.
923  // The origins of the constraints are turned into a conjunction and inserted as
924  // one origin of the "outside restriction" constraint.
925 
926  // If the ICP module has returned UNKNOWN, and the BV module has returned UNSAT,
927  // the infeasible subset of the BV module is not sufficient: When encoding into
928  // Bitvector logic, the contracted bounds from ICP are used and become an implicit
929  // constraint of the Bitvector problem. However, the ICP module currently does not
930  // give us any insights about the constraints which have been used to contract
931  // a certain clause. Therefore, we cannot create a reasonable infeasible subset here.
932  // Instead, we use the conjunction of all input formulas as origin of the
933  // "outside restriction" constraint.
934 
935  FormulaSetT origins;
936 
937  if(_fromICPOnly) {
938  const std::vector<FormulaSetT>& infeasibleInRestriction = mICP.infeasibleSubsets();
939  ModuleInput* restrictionInput = mpICPInput;
940 
941  for(const FormulaSetT& infeasibleSubset : infeasibleInRestriction) {
942  FormulasT originsOfInfSubset;
943  for(const FormulaT& infSubsetElement : infeasibleSubset) {
944  // Collect origins of element (i.e. subformulas of the received formula of IntBlastModule)
945  ModuleInput::const_iterator posInModuleInput = restrictionInput->find(infSubsetElement);
946  assert(posInModuleInput != restrictionInput->end());
947  if(posInModuleInput->hasOrigins()) {
948  bool isConstraintFromRestriction = false;
949  for(const auto& origin : posInModuleInput->origins()) {
950  if(origin == mConstraintFromBounds) {
951  isConstraintFromRestriction = true;
952  break;
953  }
954  }
955 
956  if(! isConstraintFromRestriction) {
957  collectOrigins(*findBestOrigin(posInModuleInput->origins()), originsOfInfSubset);
958  }
959  }
960  }
961  origins.insert(FormulaT(carl::FormulaType::AND, originsOfInfSubset));
962  }
963  } else {
964  FormulasT allInputFormulas;
965  for(const auto& inputFormula : rReceivedFormula()) {
966  allInputFormulas.push_back(inputFormula.formula());
967  }
968  origins.insert(FormulaT(carl::FormulaType::AND, allInputFormulas));
969  }
970 
971  if(INTBLAST_DEBUG_ENABLED) {
972  INTBLAST_DEBUG("'outside restriction' formula has origins:");
973  for(const FormulaT& origin : origins) {
974  INTBLAST_DEBUG("- " << origin);
975  }
976  }
977 
978  addSubformulaToPassedFormula(newOutsideConstraint, std::make_shared<std::vector<FormulaT>>(origins.begin(), origins.end()));
979  }
980 
981  template<class Settings>
982  void IntBlastModule<Settings>::addFormulaToICP(const FormulaT& _formula, const FormulaT& _origin)
983  {
984  INTBLAST_DEBUG("-[ICP+]-> " << _formula);
985  INTBLAST_DEBUG(" (origin: " << _origin << ")");
986  auto insertionResult = mpICPInput->add(_formula, _origin);
987 
988  if(insertionResult.second) {
989  mICP.inform(_formula);
990  mICP.add(insertionResult.first);
991  }
992  }
993 
994  template<class Settings>
995  void IntBlastModule<Settings>::addSubstitutesToICP(const ConstraintT& _constraint, const FormulaT& _origin)
996  {
997  // Create a substitute for every node of the constraint tree of _formula
998  // in order to receive bounds from ICP for these expressions
999 
1000  ConstrTree constraintTree(_constraint);
1001 
1002  // Walk through the ConstraintTree in a breadth-first search
1003  std::list<PolyTree> nodesForSubstitution;
1004  nodesForSubstitution.push_back(constraintTree.left());
1005  nodesForSubstitution.push_back(constraintTree.right());
1006 
1007  while(! nodesForSubstitution.empty()) {
1008  const PolyTree& currentPoly = nodesForSubstitution.front();
1009 
1010  Poly substituteEq;
1011 
1012  switch(currentPoly.type()) {
1013  case PolyTree::Type::SUM:
1014  substituteEq = Poly(getICPSubstitute(currentPoly.left().poly()))
1015  + getICPSubstitute(currentPoly.right().poly());
1016  break;
1017  case PolyTree::Type::PRODUCT:
1018  substituteEq = Poly(getICPSubstitute(currentPoly.left().poly()))
1019  * getICPSubstitute(currentPoly.right().poly());
1020  break;
1021  default:
1022  substituteEq = currentPoly.poly();
1023  }
1024 
1025  substituteEq -= getICPSubstitute(currentPoly.poly());
1026  FormulaT constraintForICP(substituteEq, carl::Relation::EQ);
1027  addFormulaToICP(constraintForICP, _origin);
1028 
1029  if(currentPoly.type() == PolyTree::Type::SUM || currentPoly.type() == PolyTree::Type::PRODUCT) {
1030  // Schedule left and right subtree of current PolyTree
1031  // for being visited in the breadth-first search
1032  nodesForSubstitution.push_back(currentPoly.left());
1033  nodesForSubstitution.push_back(currentPoly.right());
1034  }
1035 
1036  nodesForSubstitution.pop_front();
1037  }
1038  }
1039 
1040  template<class Settings>
1041  void IntBlastModule<Settings>::addConstraintFormulaToICP(const FormulaT& _formula)
1042  {
1043  assert(_formula.type() == carl::FormulaType::CONSTRAINT);
1044  ConstrTree constraintTree(_formula.constraint());
1045 
1046  // Add the root (the constraint itself) to ICP
1047  Poly rootPoly(getICPSubstitute(constraintTree.left().poly()));
1048  rootPoly -= getICPSubstitute(constraintTree.right().poly());
1049  ConstraintT rootConstraint(rootPoly, constraintTree.relation());
1050 
1051  addFormulaToICP(FormulaT(rootConstraint), _formula);
1052  }
1053 
1054  template<class Settings>
1055  carl::Variable::Arg IntBlastModule<Settings>::getICPSubstitute(const Poly& _poly)
1056  {
1057  auto substituteLookup = mSubstitutes.find(_poly);
1058  if(substituteLookup != mSubstitutes.end()) {
1059  return substituteLookup->second;
1060  }
1061 
1062  mSubstitutes[_poly] = carl::fresh_integer_variable();
1063  return mSubstitutes[_poly];
1064  }
1065 
1066  template<class Settings>
1067  void IntBlastModule<Settings>::removeFormulaFromICP(const FormulaT& _formula, const FormulaT& _origin)
1068  {
1069  auto formulaInInput = mpICPInput->find(_formula);
1070  if(formulaInInput != mpICPInput->end()) {
1071  if(mpICPInput->removeOrigin(formulaInInput, _origin)) {
1072  INTBLAST_DEBUG("-[ICP-]-> " << _formula);
1073  mICP.remove(formulaInInput);
1074  mpICPInput->erase(formulaInInput);
1075  }
1076  }
1077  }
1078 
1079  template<class Settings>
1080  void IntBlastModule<Settings>::removeOriginFromICP(const FormulaT& _origin)
1081  {
1082  ModuleInput::iterator icpFormula = mpICPInput->begin();
1083  while(icpFormula != mpICPInput->end())
1084  {
1085  // Remove the given formula from the set of origins.
1086  if(mpICPInput->removeOrigin(icpFormula, _origin)) {
1087  INTBLAST_DEBUG("-[ICP-]-> " << icpFormula->formula());
1088  mICP.remove(icpFormula);
1089  icpFormula = mpICPInput->erase(icpFormula);
1090  } else {
1091  ++icpFormula;
1092  }
1093  }
1094  }
1095 
1096  template<class Settings>
1097  void IntBlastModule<Settings>::addFormulaToBV(const FormulaT& _formula, const FormulaT& _origin)
1098  {
1099  INTBLAST_DEBUG("-[BV +]-> " << _formula);
1100  INTBLAST_DEBUG(" (origin: " << _origin << ")");
1101 
1102  auto insertionResult = mpBVInput->add(_formula, _origin);
1103  if(insertionResult.second) { // The formula was fresh
1104  mpBVSolver->inform(_formula);
1105  mpBVSolver->add(_formula);
1106  }
1107  }
1108 
1109  template<class Settings>
1110  void IntBlastModule<Settings>::removeOriginFromBV(const FormulaT& _origin)
1111  {
1112  ModuleInput::iterator bvFormula = mpBVInput->begin();
1113  while(bvFormula != mpBVInput->end())
1114  {
1115  // Remove the given formula from the set of origins.
1116  if(mpBVInput->removeOrigin(bvFormula, _origin)) {
1117  mpBVSolver->removeFormula(bvFormula->formula());
1118  bvFormula = mpBVInput->erase(bvFormula);
1119  } else {
1120  ++bvFormula;
1121  }
1122  }
1123  }
1124 
1125  template<class Settings>
1126  void IntBlastModule<Settings>::updateModelFromICP() const
1127  {
1128  clearModel();
1129  mICP.updateModel();
1130  mModel = mICP.model();
1131  }
1132 
1133  template<class Settings>
1134  void IntBlastModule<Settings>::updateModelFromBV() const
1135  {
1136  clearModel();
1137  const Model& bvModel = mpBVSolver->model();
1138 
1139  // Transfer all non-bitvector assignments
1140  for(const auto& varAndValue : bvModel) {
1141  if(! varAndValue.first.isBVVariable()) {
1142  mModel.insert(varAndValue);
1143  }
1144  }
1145 
1146  // For each input variable, look up bitvector value and convert it back to integer
1147  for(auto inputVariableIt = mInputVariables.cbegin();inputVariableIt != mInputVariables.cend();++inputVariableIt) {
1148  auto& inputVariable = *inputVariableIt;
1149  const carl::Variable& variable = inputVariable.element();
1150  const BlastedPoly& blasting = mPolyBlastings.at(Poly(variable));
1151 
1152  if(blasting.is_constant()) {
1153  auto modelValue = RAN(blasting.constant());
1154  mModel.emplace(ModelVariable(variable), ModelValue(modelValue));
1155  } else {
1156  const carl::BVTerm& blastedTerm = blasting.term().term();
1157  assert(blastedTerm.type() == carl::BVTermType::VARIABLE);
1158  const carl::BVVariable& bvVariable = blastedTerm.variable();
1159 
1160  Integer integerValue(0);
1161 
1162  auto bvValueInModel = bvModel.find(ModelVariable(bvVariable));
1163  if(bvValueInModel != bvModel.end()) {
1164  const carl::BVValue& bvValue = bvValueInModel->second.asBVValue();
1165  integerValue = decodeBVConstant(bvValue, blasting.term().type());
1166  }
1167  // If the bitvector variable does not appear in the model of the
1168  // BV solver, the BV solver has not received any constraints
1169  // containing this variable. This implies that an arbitrary value is allowed.
1170  // We simply use constant 0.
1171  mModel.emplace(ModelVariable(variable), ModelValue(integerValue));
1172  }
1173  }
1174  }
1175 
1176  template<class Settings>
1177  typename IntBlastModule<Settings>::IntegerInterval IntBlastModule<Settings>::get_num(const RationalInterval& _interval) const
1178  {
1179  return IntegerInterval(
1180  carl::get_num(_interval.lower()), _interval.lower_bound_type(),
1181  carl::get_num(_interval.upper()), _interval.upper_bound_type()
1182  );
1183  }
1184 
1185  template<class Settings>
1186  void IntBlastModule<Settings>::addPolyParents(const ConstraintT& _constraint)
1187  {
1188  ConstrTree constraintTree(_constraint);
1189 
1190  // Perform a BFS
1191  std::list<PolyTree> nodes;
1192  nodes.push_back(constraintTree.left());
1193  nodes.push_back(constraintTree.right());
1194 
1195  while(! nodes.empty()) {
1196  const PolyTree& current = nodes.front();
1197 
1198  if(current.type() == PolyTree::Type::SUM || current.type() == PolyTree::Type::PRODUCT) {
1199  addPolyParent(current.left().poly(), current.poly());
1200  addPolyParent(current.right().poly(), current.poly());
1201  nodes.push_back(current.left());
1202  nodes.push_back(current.right());
1203  }
1204 
1205  nodes.pop_front();
1206  }
1207  }
1208 
1209  template<class Settings>
1210  void IntBlastModule<Settings>::addPolyParent(const Poly& _child, const Poly& _parent)
1211  {
1212  auto inserted = mPolyParents.insert(std::make_pair(_child, std::set<Poly>()));
1213  inserted.first->second.insert(_parent);
1214  }
1215 
1216  template<class Settings>
1217  std::set<Poly> IntBlastModule<Settings>::parentalClosure(std::set<Poly> _children)
1218  {
1219  std::set<Poly> closure(_children);
1220  std::list<Poly> incomplete(_children.begin(), _children.end());
1221 
1222  while(! incomplete.empty()) {
1223  const Poly& current = incomplete.front();
1224  for(auto parent : mPolyParents[current]) {
1225  auto parentInserted = closure.insert(parent);
1226  if(parentInserted.second) {
1227  incomplete.push_back(parent);
1228  }
1229  }
1230  incomplete.pop_front();
1231  }
1232 
1233  return closure;
1234  }
1235 
1236  template<class Settings>
1237  void IntBlastModule<Settings>::recheckShrunkPolys()
1238  {
1239  auto& icpBounds = mBoundsInRestriction.getEvalIntervalMap();
1240  std::set<Poly> polysToReencode;
1241 
1242  for(const Poly& shrunkPoly : mShrunkPolys) {
1243  auto& blastedPoly = mPolyBlastings.at(shrunkPoly);
1244  auto& substitute = mSubstitutes.at(shrunkPoly);
1245 
1246  IntegerInterval encodedBounds = IntegerInterval(blastedPoly.lower_bound(), blastedPoly.upper_bound());
1247  auto icpBoundsIt = icpBounds.find(substitute);
1248 
1249  if(icpBoundsIt == icpBounds.end() || ! encodedBounds.contains(get_num(icpBoundsIt->second))) {
1250  polysToReencode.insert(shrunkPoly);
1251  }
1252  }
1253 
1254  if(! polysToReencode.empty()) {
1255  unblastPolys(polysToReencode);
1256  }
1257  }
1258 
1259  template<class Settings>
1260  void IntBlastModule<Settings>::unblastPoly(const Poly& _polys)
1261  {
1262  std::set<Poly> polySet;
1263  polySet.insert(_polys);
1264  unblastPolys(polySet);
1265  }
1266 
1267  template<class Settings>
1268  void IntBlastModule<Settings>::unblastPolys(const std::set<Poly>& _polys)
1269  {
1270  std::set<Poly> obsolete = parentalClosure(_polys);
1271 
1272  // Erase all PolyBlastings belonging to the polynomials in 'obsolete'
1273  auto polyIt = mPolyBlastings.begin();
1274  while(polyIt != mPolyBlastings.end()) {
1275  if(obsolete.find(polyIt->first) != obsolete.end()) {
1276  mShrunkPolys.erase(polyIt->first);
1277  polyIt = mPolyBlastings.erase(polyIt);
1278  } else {
1279  ++polyIt;
1280  }
1281  }
1282 
1283  // Erase all ConstrBlastings which used a PolyBlasting that is now deleted
1284  auto constrIt = mConstrBlastings.begin();
1285  while(constrIt != mConstrBlastings.end()) {
1286  ConstrTree constrTree(constrIt->first);
1287  if(obsolete.find(constrTree.left().poly()) != obsolete.end()) {
1288  constrIt = mConstrBlastings.erase(constrIt);
1289  } else {
1290  ++constrIt;
1291  }
1292  }
1293 
1294  // Reencode all formulas which contain constraints whose
1295  // ConstrBlastings is now deleted
1296  for(const auto& inputFormula : rReceivedFormula()) {
1297  std::vector<ConstraintT> constraintsInFormula;
1298  arithmetic_constraints(inputFormula.formula(),constraintsInFormula);
1299 
1300  bool needsReencoding = false;
1301  for(const ConstraintT& constraint : constraintsInFormula) {
1302  if(mConstrBlastings.find(constraint) == mConstrBlastings.end()) {
1303  needsReencoding = true;
1304  break;
1305  }
1306  }
1307 
1308  if(needsReencoding) {
1309  removeOriginFromBV(inputFormula.formula());
1310  mFormulasToEncode.insert(inputFormula.formula());
1311  }
1312  }
1313  }
1314 }
1315 
1316