SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
OneCellCAD.h
Go to the documentation of this file.
1 #pragma once
2 
3 /**
4  * @file
5  * Construct a single open CAD Cell IN A LEVEL-WISE MANNER around a given point that is sign-invariant
6  * on a given set of polynomials. This is an adaptation of the already existing onecellcad in this project.
7  *
8  * @author Philippe Specht
9  * Contact: philippe.specht@rwth-aachen.de
10  *
11  * References:
12  * [brown15] Brown, Christopher W., and Marek Košta.
13  * "Constructing a single cell in cylindrical algebraic decomposition."
14  * Journal of Symbolic Computation 70 (2015): 14-48.
15  * [mccallum84] Scott McCallum.
16  * "An Improved Projection Operation for Cylindrical Algebraic Decomposition"
17  * Ph.D. Dissertation. 1984. The University of Wisconsin - Madison
18  */
19 
20 #include "../Assertables.h"
21 #include "../utils.h"
22 
23 
24 namespace smtrat {
25 namespace mcsat {
26 namespace onecellcad {
27 namespace levelwise {
28 
29 class LevelwiseCAD : public OneCellCAD {
30  public:
31  using OneCellCAD::OneCellCAD;
32 
33  /**
34  * Construct a single CADCell that contains the given 'point' and is
35  * sign-invariant for the given polynomials in 'polys'. The construction
36  * fails if a polynomial vanishes ( p(a_1,...,a_i-1,x_i) ). Note that
37  * this cell is cylindrical only with respect to the given 'variableOrder'.
38  *
39  * @param variableOrder must contain unique variables and at least one,
40  * because constant polynomials (without a variable) are prohibited.
41  * @param point point.size() >= variables.size().
42  * @param polys must contain only non-constant, irreducible tagged polynomials that
43  * mention only variables that appear in 'variableOrder'.
44  *
45  */
46  std::optional<CADCell> constructCADCellEnclosingPoint(
47  std::vector<std::vector<TagPoly>> &polys, int sectionHeuristic, int sectorHeuristic) {
48  SMTRAT_LOG_INFO("smtrat.cad", "Build CADcell enclosing point ");
49  SMTRAT_LOG_DEBUG("smtrat.cad", "Variable order: " << variableOrder);
50  SMTRAT_LOG_DEBUG("smtrat.cad", "Point: " << point);
51  for (auto &poly : polys) {
52  auto pVec = asMultiPolys(poly);
53  SMTRAT_LOG_DEBUG("smtrat.cad", "Polys: " << pVec);
54  assert(hasOnlyNonConstIrreducibles(pVec));
55  assert(polyVarsAreAllInList(pVec, variableOrder));
56  }
57 
58  CADCell cell = fullSpaceCell(point.dim());
59  SMTRAT_LOG_DEBUG("smtrat.cad", "Cell: " << cell);
60 
61  for (int i = (int) point.dim() - 1; i >= 0; i--) {
62  carl::Variable rootVariable = variableOrder[i];
63 
64  bool sector = true;
65  TagPoly t;
66  int deg = -1;
67  for (auto &poly : polys[i]) {
68  if (vanishesEarly(poly.level, poly.poly)) {
69  SMTRAT_LOG_WARN("smtrat.cad",
70  "Building failed, " << poly.poly << " vanishes early at "
71  << point[i]);
72  return std::nullopt;
73  } else if (isPointRootOfPoly(poly)) {
74  sector = false;
75  int locDeg = (int) getDegree(poly, rootVariable);
76  assert(locDeg >= 1);
77  // for section: find defining polynomial with smallest degree in i-th variable
78  if (locDeg > deg) {
79  poly.tag = InvarianceType::ORD_INV;
80  t = poly;
81  deg = locDeg;
82  }
83  }
84  }
85 
86  const RAN pointComp = point[i];
87  if (!sector) {
88  /** Current level is a Section */
89  SMTRAT_LOG_DEBUG("smtrat.cad", "Shrink cell sector at lvl " << i + 1);
90  SMTRAT_LOG_TRACE("smtrat.cad", "Transform to section");
91  SMTRAT_LOG_TRACE("smtrat.cad", "Defining poly: " << t.poly);
92  SMTRAT_LOG_TRACE("smtrat.cad", "Lvl-Var: " << variableOrder[i]);
93  SMTRAT_LOG_DEBUG("smtrat.cad", "PointComp: " << pointComp);
94 
95  assert(isNonConstIrreducible(t.poly));
96  assert(t.level == (size_t) i);
97 
98  auto isolatedRoots = isolateLastVariableRoots(t.level, t.poly);
99  assert(!isolatedRoots.empty());
100  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
101 
102  std::size_t rootIdx = 0;
103  bool found = false;
104  for (const auto &root : isolatedRoots) {
105  rootIdx++;
106  if (root == pointComp) {
107  SMTRAT_LOG_TRACE("smtrat.cad", "Equal: " << root);
108  cell[i] = Section{asRootExpr(rootVariable, t.poly, rootIdx), root};
109  SMTRAT_LOG_TRACE("smtrat.cad", "Resulting section: "
110  << (Section{asRootExpr(rootVariable, t.poly, rootIdx), root}));
111  found = true;
112  break;
113  }
114  }
115  assert(found);
116 
117  /** Projection part for section case*/
118  if (i != 0) {
119  //Project polynomial that defines section
120  SMTRAT_LOG_TRACE("smtrat.cad", "Begin projection in section case");
121 
122  Poly disc = discriminant(variableOrder[i], t.poly);
123  SMTRAT_LOG_TRACE("smtrat.cad", "Add discriminant: " << disc << " (if not const)");
124  appendOnCorrectLevel(disc, InvarianceType::ORD_INV, polys, variableOrder);
125 
126 
127  Poly ldcf = leadcoefficient(variableOrder[i], t.poly);
128  SMTRAT_LOG_TRACE("smtrat.cad",
129  "Add leadcoefficient: " << ldcf << " (if not const)");
130  appendOnCorrectLevel(ldcf, InvarianceType::SIGN_INV, polys, variableOrder);
131 
132 
133  std::vector<std::tuple<RAN, TagPoly>> upper;
134  std::vector<std::tuple<RAN, TagPoly>> lower;
135  std::vector<std::pair<Poly, Poly>> resultants;
136  std::vector<Poly> noDisc1;
137  std::vector<Poly> noDisc2;
138  std::vector<Poly> noLdcf;
139  //project rest of polynomials
140 
141 
142  if (sectionHeuristic == 1) {
143  for (auto &poly : polys[i]) {
144  //Heuristic 1: calculate resultant between defining pol t and every pol that has root above or below t
145  if (!isolateLastVariableRoots(poly.level, poly.poly).empty()) {
146  if (poly.poly != t.poly) {
147  resultants.emplace_back(std::make_pair(t.poly, poly.poly));
148  }
149  }
150  }
151 
152  #ifdef SMTRAT_DEVOPTION_Statistics
153  getStatistic().resultantBarrierCreated();
154  #endif
155 
156  } else if (sectionHeuristic == 2) {
157  for (auto &poly : polys[i]) {
158  //Heuristic 2: calculate resultant in chain-form over lower and upper
159  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
160  std::vector<RAN> isolatedRoots = isolateLastVariableRoots(poly.level,
161  poly.poly);
162 
163  if (isolatedRoots.empty()) {
164  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
165  continue;
166  } else {
167  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
168  }
169 
170  //guaranteed at least one root
171  //find closest root above and below sample (if existent) and put into upper and lower respectively
172  if (isolatedRoots.front() >= pointComp) {
173  //poly only has roots above pointComp
174  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(1): "
175  << isolatedRoots.front());
176  upper.emplace_back(std::make_tuple(isolatedRoots.front(), poly));
177  } else if (isolatedRoots.back() <= pointComp) {
178  //poly only has roots below pointComp
179  SMTRAT_LOG_DEBUG("smtrat.cad", "Biggest root below PointComp(1): "
180  << isolatedRoots.back());
181  lower.emplace_back(std::make_tuple(isolatedRoots.back(), poly));
182  } else {
183  auto lb = std::lower_bound(isolatedRoots.begin(), isolatedRoots.end(),
184  pointComp);
185  if (*(lb - 1) == std::get<Section>(cell[i]).isolatedRoot) {
186  SMTRAT_LOG_DEBUG("smtrat.cad", "Root at PointComp: " << *(lb - 1));
187  lower.emplace_back(std::make_tuple(*(lb - 1), poly));
188  } else {
189  //poly has root above and below pointComp
190  SMTRAT_LOG_DEBUG("smtrat.cad",
191  "Smallest root above PointComp(2): " << *lb);
192  upper.emplace_back(std::make_tuple(*lb, poly));
193  SMTRAT_LOG_DEBUG("smtrat.cad",
194  "Biggest root below PointComp(2): " << *(lb - 1));
195  lower.emplace_back(std::make_tuple(*(lb - 1), poly));
196  }
197  }
198 
199  //Additionally calculate disc
200  disc = discriminant(variableOrder[i], poly.poly);
201  SMTRAT_LOG_TRACE("smtrat.cad",
202  "Add discriminant: " << disc << " (if not const)");
203  appendOnCorrectLevel(disc, InvarianceType::ORD_INV, polys, variableOrder);
204  }
205 
206  //sort closest roots of pols below and above sample
207  std::sort(lower.begin(), lower.end(), [](auto const &t1, auto const &t2) {
208  return std::get<0>(t1) < std::get<0>(t2);
209  });
210  std::sort(upper.begin(), upper.end(), [](auto const &t1, auto const &t2) {
211  return std::get<0>(t1) < std::get<0>(t2);
212  });
213 
214  //calculate resultants
215  if (!lower.empty()) {
216  for (auto it = lower.begin(); it != lower.end() - 1; it++) {
217  resultants.emplace_back(std::make_pair(std::get<1>(*it).poly,
218  std::get<1>(*(it + 1)).poly));
219  #ifdef SMTRAT_DEVOPTION_Statistics
220  getStatistic().resultantBarrierCreated();
221  #endif
222  }
223  }
224 
225  if (!lower.empty() && !upper.empty()) {
226  resultants.emplace_back(std::make_pair(std::get<1>(lower.back()).poly,
227  std::get<1>(upper.front()).poly));
228  }
229 
230  if (!upper.empty()) {
231  for (auto it = upper.begin(); it != upper.end() - 1; it++) {
232  resultants.emplace_back(std::make_pair(std::get<1>(*it).poly,
233  std::get<1>(*(it + 1)).poly));
234  #ifdef SMTRAT_DEVOPTION_Statistics
235  getStatistic().resultantBarrierCreated();
236  #endif
237  }
238  }
239 
240  // Need no ldcf if its beginning or end of resultant-chain and has poly above and below sample
241  if (!lower.empty() && std::find_if(upper.begin(), upper.end(),
242  [&](auto const &t1) {
243  return (std::get<1>(t1).poly == std::get<1>(*lower.begin()).poly);
244  }) != upper.end()) {
245  noLdcf.emplace_back(std::get<1>(*lower.begin()).poly);
246  }
247  if (!upper.empty() && std::find_if(lower.begin(), lower.end(),
248  [&](auto const &t1) {
249  return (std::get<1>(t1).poly == std::get<1>(*(upper.end() - 1)).poly);
250  }) != lower.end()) {
251  noLdcf.emplace_back(std::get<1>(*(upper.end() - 1)).poly);
252  }
253 
254  for (auto &poly : polys[i]) {
255  if (!contains(noLdcf, poly.poly)) {
256  ldcf = leadcoefficient(variableOrder[i], poly.poly);
257  SMTRAT_LOG_TRACE("smtrat.cad", "Add leadcoefficient: " << ldcf << " (if not const)");
258  appendOnCorrectLevel(ldcf, InvarianceType::SIGN_INV, polys, variableOrder);
259  }
260  }
261 
262  } else if (sectionHeuristic == 3) {
263  for (auto &poly : polys[i]) {
264  //Heuristic 3: smart
265  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
266  std::vector<RAN> isolatedRoots = isolateLastVariableRoots(poly.level, poly.poly);
267 
268  if (isolatedRoots.empty()) {
269  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
270  continue;
271  } else {
272  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
273  }
274 
275  //guaranteed at least one root
276  //find closest root above and below sample (if existent) and put into upper and lower respectively
277  poly.deg = getDegree(poly, rootVariable);
278  if (isolatedRoots.front() >= pointComp) {
279  //poly only has roots above pointComp
280  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(1): "
281  << isolatedRoots.front());
282  upper.emplace_back(std::make_tuple(isolatedRoots.front(), poly));
283  } else if (isolatedRoots.back() <= pointComp) {
284  //poly only has roots below pointComp
285  SMTRAT_LOG_DEBUG("smtrat.cad", "Biggest root below PointComp(1): "
286  << isolatedRoots.back());
287  lower.emplace_back(std::make_tuple(isolatedRoots.back(), poly));
288  } else {
289  auto lb = std::lower_bound(isolatedRoots.begin(), isolatedRoots.end(), pointComp);
290  if (*(lb - 1) == std::get<Section>(cell[i]).isolatedRoot) {
291  SMTRAT_LOG_DEBUG("smtrat.cad", "Root at PointComp: " << *(lb - 1));
292  lower.emplace_back(std::make_tuple(*(lb - 1), poly));
293  } else {
294  //poly has root above and below pointComp
295  SMTRAT_LOG_DEBUG("smtrat.cad",
296  "Smallest root above PointComp(2): " << *lb);
297  upper.emplace_back(std::make_tuple(*lb, poly));
298  SMTRAT_LOG_DEBUG("smtrat.cad",
299  "Biggest root below PointComp(2): " << *(lb - 1));
300  lower.emplace_back(std::make_tuple(*(lb - 1), poly));
301  }
302  }
303  }
304 
305  //sort closest roots of pols below and above sample
306  std::sort(lower.begin(), lower.end(), [](auto const &t1, auto const &t2) {
307  return std::get<0>(t1) < std::get<0>(t2);
308  });
309  std::sort(upper.begin(), upper.end(), [](auto const &t1, auto const &t2) {
310  return std::get<0>(t1) < std::get<0>(t2);
311  });
312 
313  //calculate resultants
314  if (!lower.empty()) {
315  //optimization: for multiple entries with the same root in lower, sort the one with the
316  // lowest degree to the smallest possible position for optimal resultant calculation
317  for (auto it = lower.begin() + 1; it != lower.end(); it++) {
318  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
319  std::get<1>(*(it - 1)).deg < std::get<1>(*it).deg) {
320  std::iter_swap(it - 1, it);
321  }
322  }
323 
324  auto mark = lower.rend()-1;
325  while (mark != lower.rbegin()) {
326  auto cur = std::min_element(lower.rbegin(), mark, [](auto const &t1, auto const &t2) {
327  return std::get<1>(t1).deg < std::get<1>(t2).deg;
328  });
329 
330  for (auto it = cur + 1; it != mark+1; it++) {
331  resultants.emplace_back(std::make_pair(std::get<1>(*cur).poly, std::get<1>(*it).poly));
332  // Ldcfs of pols not necessary if they are only connected to 1 pol AND also appear on the other side of sample point
333  if (std::find_if(upper.begin(), upper.end(),
334  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(*it).poly); }) != upper.end()) {
335  noLdcf.emplace_back(std::get<1>(*it).poly);
336  }
337  }
338 
339  mark = cur;
340 
341  #ifdef SMTRAT_DEVOPTION_Statistics
342  getStatistic().resultantBarrierCreated();
343  #endif
344  }
345 
346  // optimization: find polynomials only connected to bound t because they need no discriminant
347  if (!resultants.empty()) {
348  resultants = duplicateElimination(resultants);
349  for (auto &res : resultants) {
350  if (res.first == t.poly) {
351  noDisc1.push_back(res.second);
352  }
353  if (res.second == t.poly) {
354  noDisc1.push_back(res.first);
355  }
356  }
357  if (!noDisc1.empty()) {
358  duplicateElimination(noDisc1);
359  bool inc;
360  for (auto it = noDisc1.begin(); it != noDisc1.end();) {
361  inc = true;
362  for (auto &res : resultants) {
363  if ((res.first == *it && res.second != t.poly) ||
364  (res.second == *it && res.first != t.poly)) {
365  it = noDisc1.erase(it);
366  inc = false;
367  break;
368  }
369  }
370  if (inc) { it++; }
371  }
372  }
373  }
374  }
375 
376  std::vector<std::pair<Poly, Poly>> tmpResultants;
377  if (!upper.empty()) {
378  //optimization: for multiple entries with the same root in upper, sort the one with the
379  // lowest degree to the smallest possible position for optimal resultant calculation
380  for (auto it = upper.begin() + 1; it != upper.end(); it++) {
381  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
382  std::get<1>(*(it - 1)).deg > std::get<1>(*it).deg) {
383  std::iter_swap(it - 1, it);
384  }
385  }
386 
387  auto mark = upper.end()-1;
388  while (mark != upper.begin()) {
389  auto cur = std::min_element(upper.begin(), mark, [](auto const &t1, auto const &t2) {
390  return std::get<1>(t1).deg < std::get<1>(t2).deg;
391  });
392 
393  for (auto it = cur + 1; it != mark+1; it++) {
394  tmpResultants.emplace_back(std::make_pair(std::get<1>(*cur).poly, std::get<1>(*it).poly));
395  // Ldcfs of pols not necessary if they are only connected to 1 pol AND also appear on the other side of sample point
396  if (std::find_if(lower.begin(), lower.end(),
397  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(*it).poly); }) != lower.end()) {
398  noLdcf.emplace_back(std::get<1>(*it).poly);
399  }
400  }
401 
402  mark = cur;
403 
404  #ifdef SMTRAT_DEVOPTION_Statistics
405  getStatistic().resultantBarrierCreated();
406  #endif
407  }
408 
409  // optimization: find polynomials only connected to bound t because they need no discriminant
410  if (!tmpResultants.empty()) {
411  tmpResultants = duplicateElimination(tmpResultants);
412  for (auto &res : tmpResultants) {
413  if (res.first == t.poly) {
414  noDisc2.push_back(res.second);
415  }
416  if (res.second == t.poly) {
417  noDisc2.push_back(res.first);
418  }
419  }
420  if (!noDisc2.empty()) {
421  duplicateElimination(noDisc2);
422  bool inc;
423  for (auto it = noDisc2.begin(); it != noDisc2.end();) {
424  inc = true;
425  for (auto &res : tmpResultants) {
426  if ((res.first == *it && res.second != t.poly) ||
427  (res.second == *it && res.first != t.poly)) {
428  it = noDisc2.erase(it);
429  inc = false;
430  break;
431  }
432  }
433  if (inc) { it++; }
434  }
435  }
436  resultants.insert(resultants.end(), tmpResultants.begin(), tmpResultants.end());
437  tmpResultants.clear();
438  }
439  }
440 
441  if (!lower.empty() && !upper.empty()) {
442  resultants.emplace_back(std::make_pair(std::get<1>(lower.back()).poly,
443  std::get<1>(upper.front()).poly));
444  }
445 
446  //Additionally calculate discs and ldcfs (if necessary)
447  for (auto &poly : polys[i]) {
448  if (!contains(noDisc1, poly.poly) && !contains(noDisc2, poly.poly)) {
449  disc = discriminant(variableOrder[i], poly.poly);
450  SMTRAT_LOG_TRACE("smtrat.cad", "Add discriminant: " << disc << " (if not const)");
451  appendOnCorrectLevel(disc, InvarianceType::ORD_INV, polys, variableOrder);
452  }
453 
454  if (!contains(noLdcf, poly.poly)) {
455  ldcf = leadcoefficient(variableOrder[i], poly.poly);
456  SMTRAT_LOG_TRACE("smtrat.cad", "Add leadcoefficient: " << ldcf << " (if not const)");
457  appendOnCorrectLevel(ldcf, InvarianceType::SIGN_INV, polys, variableOrder);
458  }
459  }
460 
461  } else {
462  SMTRAT_LOG_WARN("smtrat.cad", "Building failed: Incorrect heuristic input");
463  return std::nullopt;
464  }
465 
466  for (auto &poly : polys[i]) {
467  if (poly.poly != t.poly) {
468  if (isPointRootOfPoly(poly)) {
469  if (poly.tag == InvarianceType::ORD_INV) {
470  SMTRAT_LOG_TRACE("smtrat.cad", "Check for vanishing coefficient");
471  auto coeff = coeffNonNull(poly);
472  if (coeff.has_value()) {
473  SMTRAT_LOG_TRACE("smtrat.cad", "Add result of coeffNonNull: " << coeff.value() << " (if not const)");
474  appendOnCorrectLevel(coeff.value(), InvarianceType::SIGN_INV, polys, variableOrder);
475  }
476  if (sectionHeuristic == 1) {
477  //for other heuristics, discriminants have already been calculated
478  disc = discriminant(variableOrder[i], poly.poly);
479  SMTRAT_LOG_TRACE("smtrat.cad", "Add discriminant: " << disc << " (if not const)");
480  appendOnCorrectLevel(disc, InvarianceType::ORD_INV, polys, variableOrder);
481  }
482  }
483  } else {
484  poly.tag = InvarianceType::ORD_INV;
485  }
486  }
487  }
488 
489  // Add all calculate resultants (independent from heuristic)
490  addResultants(resultants, polys, variableOrder[i], variableOrder);
491  }
492  } else {
493  /** Current level is a Sector */
494  Sector &sector = std::get<Sector>(cell[i]);
495  SMTRAT_LOG_DEBUG("smtrat.cad", "Shrink cell sector at lvl " << i + 1);
496  SMTRAT_LOG_DEBUG("smtrat.cad", "Lvl-var: " << variableOrder[i]);
497  SMTRAT_LOG_DEBUG("smtrat.cad", "PointComp: " << pointComp);
498  SMTRAT_LOG_DEBUG("smtrat.cad", "Determine sector, currently: " << sector);
499 
500  std::vector<TagPoly> upper1;
501  std::vector<TagPoly> lower1;
502  std::vector<std::tuple<RAN, TagPoly, int>> upper2;
503  std::vector<std::tuple<RAN, TagPoly, int>> lower2;
504  std::vector<Poly> noLdcf;
505  TagPoly curUp;
506  TagPoly curLow;
507  // Different heuristics for resultant calculation need different setups of control data
508  // Level 1 does not need control data at all
509  if (i == 0) {
510  for (const auto &poly : polys[i]) {
511  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
512 
513  auto isolatedRoots = isolateLastVariableRoots(poly.level, poly.poly);
514 
515  if (isolatedRoots.empty()) {
516  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
517  continue;
518  } else {
519  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
520  }
521 
522  // Search for closest isolatedRoots/boundPoints to pointComp, i.e.
523  // someRoot ... < closestLower < pointComp < closestUpper < ... someOtherRoot
524  std::optional<RAN> closestLower, closestUpper;
525  int rootIdx = 0, lowerRootIdx = 0, upperRootIdx = 0;
526 
527  for (const auto &root : isolatedRoots) {
528  rootIdx++;
529  if (root < pointComp) {
530  SMTRAT_LOG_TRACE("smtrat.cad", "Smaller: " << root);
531  if (!closestLower || *closestLower < root) {
532  closestLower = root;
533  lowerRootIdx = rootIdx;
534  curLow = poly;
535  }
536  } else { // pointComp < root
537  SMTRAT_LOG_TRACE("smtrat.cad", "Bigger: " << root);
538  if (!closestUpper || root < *closestUpper) {
539  closestUpper = root;
540  upperRootIdx = rootIdx;
541  curUp = poly;
542  }
543  //break out of loop since isolatedRoots is sorted
544  break;
545  }
546  }
547 
548  if (closestLower) {
549  if (!sector.lowBound || (*(sector.lowBound)).isolatedRoot < closestLower) {
550  sector.lowBound = Section{
551  asRootExpr(rootVariable, poly.poly, lowerRootIdx),
552  *closestLower};
553  SMTRAT_LOG_TRACE("smtrat.cad", "New lower bound: "
554  << " " << sector);
555  }
556  }
557 
558  if (closestUpper) {
559  if (!sector.highBound ||
560  closestUpper < (*(sector.highBound)).isolatedRoot) {
561  sector.highBound = Section{
562  asRootExpr(rootVariable, poly.poly, upperRootIdx),
563  *closestUpper};
564  SMTRAT_LOG_TRACE("smtrat.cad", "New upper bound: "
565  << " " << sector);
566  }
567  }
568  }
569 
570  } else if (sectorHeuristic == 1) {
571  // for convenience, upper2 (lower2 respectively) is used here to save all possible upper bounds
572  // => poly with smallest degree in i-th variable is then chosen
573  std::optional<RAN> closestLower, closestUpper;
574  for (const auto &poly : polys[i]) {
575  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
576 
577  auto isolatedRoots = isolateLastVariableRoots(poly.level, poly.poly);
578 
579  if (isolatedRoots.empty()) {
580  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
581  continue;
582  } else {
583  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
584  }
585 
586  // Search for closest isolatedRoots/boundPoints to pointComp, i.e.
587  // someRoot ... < closestLower < pointComp < closestUpper < ... someOtherRoot
588  bool up = false, low = false;
589  int rootIdx = 0;
590  for (const auto &root : isolatedRoots) {
591  rootIdx++;
592  if (root < pointComp) {
593  SMTRAT_LOG_TRACE("smtrat.cad", "Smaller: " << root);
594  low = true;
595  if (!closestLower || *closestLower < root) {
596  closestLower = root;
597  lower2.clear();
598  lower2.emplace_back(std::make_tuple(root, poly, rootIdx));
599  } else if (*closestLower == root) {
600  lower2.emplace_back(std::make_tuple(root, poly, rootIdx));
601  }
602  } else { // pointComp < root
603  SMTRAT_LOG_TRACE("smtrat.cad", "Bigger: " << root);
604  up = true;
605  if (!closestUpper || root < *closestUpper) {
606  closestUpper = root;
607  upper2.clear();
608  upper2.emplace_back(std::make_tuple(root, poly, rootIdx));
609  } else if (*closestUpper == root) {
610  upper2.emplace_back(std::make_tuple(root, poly, rootIdx));
611  } else {
612  // Optimization: break out of loop since isolatedRoots is sorted
613  break;
614  }
615  }
616  }
617 
618  if (low) {
619  lower1.push_back(poly);
620  }
621 
622  if (up) {
623  upper1.push_back(poly);
624  }
625  }
626 
627  // Set bounds according to degree that is first calculated
628  if (!lower2.empty()) {
629  for (auto elem : lower2) {
630  std::get<1>(elem).deg = getDegree(std::get<1>(elem), rootVariable);
631  }
632  auto smallest = *std::min_element(lower2.begin(), lower2.end(),
633  [](auto const &t1, auto const &t2) {
634  return std::get<1>(t1).deg < std::get<1>(t2).deg;
635  });
636 
637  curLow = std::get<1>(smallest);
638  sector.lowBound = Section{
639  asRootExpr(rootVariable, curLow.poly, std::get<2>(smallest)),
640  std::get<0>(smallest)};
641  SMTRAT_LOG_TRACE("smtrat.cad", "New lower bound: "
642  << " " << sector);
643  }
644 
645  if (!upper2.empty()) {
646  for (auto elem : upper2) {
647  std::get<1>(elem).deg = getDegree(std::get<1>(elem), rootVariable);
648  }
649  auto smallest = *std::min_element(upper2.begin(), upper2.end(),
650  [](auto const &t1, auto const &t2) {
651  return std::get<1>(t1).deg < std::get<1>(t2).deg;
652  });
653 
654  curUp = std::get<1>(smallest);
655  sector.highBound = Section{
656  asRootExpr(rootVariable, curUp.poly, std::get<2>(smallest)),
657  std::get<0>(smallest)};
658  SMTRAT_LOG_TRACE("smtrat.cad", "New upper bound: "
659  << " " << sector);
660  }
661 
662  // polys with root above and below sample need no ldcf
663  for (auto &poly : polys[i]) {
664  if (contains(lower1, poly) && contains(upper1, poly)) {
665  noLdcf.emplace_back(poly.poly);
666  }
667  }
668 
669  } else if (sectorHeuristic == 2) {
670  //while determining bounds create lists upper2 and lower2 which are sorted by their order around the sample
671  for (const auto &poly : polys[i]) {
672  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
673  std::vector<RAN> isolatedRoots = isolateLastVariableRoots(poly.level,
674  poly.poly);
675 
676  if (isolatedRoots.empty()) {
677  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
678  continue;
679  } else {
680  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
681  }
682 
683  //guaranteed at least one root
684  //find closest root above and below sample (if existent) and put into upper2 and lower2 respectively
685  if (isolatedRoots.front() > pointComp) {
686  //poly only has roots above pointComp
687  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(1): "
688  << isolatedRoots.front());
689  upper2.emplace_back(std::make_tuple(isolatedRoots.front(), poly, 1));
690  } else if (isolatedRoots.back() < pointComp) {
691  //poly only has roots below pointComp
692  SMTRAT_LOG_DEBUG("smtrat.cad", "Biggest root below PointComp(1): "
693  << isolatedRoots.back());
694  lower2.emplace_back(std::make_tuple(isolatedRoots.back(), poly,
695  isolatedRoots.end() -
696  isolatedRoots.begin()));
697  } else {
698  auto lb = std::lower_bound(isolatedRoots.begin(), isolatedRoots.end(),
699  pointComp);
700  //poly has root above and below pointComp
701  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(2): " << *lb);
702  upper2.emplace_back(
703  std::make_tuple(*lb, poly, (int) (lb - isolatedRoots.begin()) + 1));
704  SMTRAT_LOG_DEBUG("smtrat.cad",
705  "Biggest root below PointComp(2): " << *(lb - 1));
706  lower2.emplace_back(std::make_tuple(*(lb - 1), poly,
707  (int) (lb - isolatedRoots.begin())));
708  }
709  }
710 
711  //sort closest roots of pols below and above sample
712  std::sort(lower2.begin(), lower2.end(), [](auto const &t1, auto const &t2) {
713  return std::get<0>(t1) < std::get<0>(t2);
714  });
715  std::sort(upper2.begin(), upper2.end(), [](auto const &t1, auto const &t2) {
716  return std::get<0>(t1) < std::get<0>(t2);
717  });
718 
719  if (!lower2.empty()) {
720  // find lower bound with smallest degree in i-th variable
721  auto curPos = lower2.rbegin();
722  int curDeg = -1;
723  auto it = lower2.rbegin() + 1;
724  while (it != lower2.rend()) {
725  if (std::get<0>(*it) == std::get<0>(*curPos)) {
726  if (curDeg == -1) {
727  curDeg = (int) getDegree(std::get<1>(*curPos), rootVariable);
728  }
729  int degree = (int) getDegree(std::get<1>(*it), rootVariable);
730  if (degree < curDeg) {
731  curPos = it;
732  curDeg = degree;
733  }
734  it++;
735  } else {
736  break;
737  }
738  }
739  std::iter_swap(curPos.base() - 1, lower2.end() - 1);
740 
741 
742  //set lower bound
743  curLow = std::get<1>(lower2.back());
744  sector.lowBound = Section{
745  asRootExpr(rootVariable, curLow.poly, std::get<2>(lower2.back())),
746  std::get<0>(lower2.back())};
747  SMTRAT_LOG_TRACE("smtrat.cad", "Lower bound: "
748  << " " << *sector.lowBound);
749 
750  } else {
751  SMTRAT_LOG_TRACE("smtrat.cad", "Open lower bound");
752  }
753 
754  if (!upper2.empty()) {
755  // find upper bound with smallest degree in i-th variable
756  auto curPos = upper2.begin();
757  int curDeg = -1;
758  auto it = upper2.begin() + 1;
759  while (it != upper2.end()) {
760  if (std::get<0>(*it) == std::get<0>(*curPos)) {
761  if (curDeg == -1) {
762  curDeg = (int) getDegree(std::get<1>(*curPos), rootVariable);
763  }
764  int degree = (int) getDegree(std::get<1>(*it), rootVariable);
765  if (degree < curDeg) {
766  curPos = it;
767  curDeg = degree;
768  }
769  it++;
770  } else {
771  break;
772  }
773  }
774  std::iter_swap(curPos, upper2.begin());
775 
776  //set upper bound
777  curUp = std::get<1>(upper2.front());
778  sector.highBound = Section{
779  asRootExpr(rootVariable, curUp.poly, std::get<2>(upper2.front())),
780  std::get<0>(upper2.front())};
781  SMTRAT_LOG_TRACE("smtrat.cad", "Upper bound: "
782  << " " << *sector.highBound);
783  } else {
784  SMTRAT_LOG_TRACE("smtrat.cad", "Open upper bound");
785  }
786 
787  } else if (sectorHeuristic == 3) {
788  //while determining bounds create lists upper2 and lower2 which are sorted by their order around the sample
789  for (auto &poly : polys[i]) {
790  SMTRAT_LOG_TRACE("smtrat.cad", "Poly: " << poly.poly);
791  std::vector<RAN> isolatedRoots = isolateLastVariableRoots(poly.level,
792  poly.poly);
793 
794  if (isolatedRoots.empty()) {
795  SMTRAT_LOG_TRACE("smtrat.cad", "No isolatable isolatedRoots");
796  continue;
797  } else {
798  SMTRAT_LOG_TRACE("smtrat.cad", "Isolated roots: " << isolatedRoots);
799  }
800 
801  //guaranteed at least one root
802  //find closest root above and below sample (if existent) and put into upper2 and lower2 respectively
803  poly.deg = getDegree(poly, rootVariable);
804  if (isolatedRoots.front() > pointComp) {
805  //poly only has roots above pointComp
806  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(1): "
807  << isolatedRoots.front());
808  upper2.emplace_back(std::make_tuple(isolatedRoots.front(), poly, 1));
809  } else if (isolatedRoots.back() < pointComp) {
810  //poly only has roots below pointComp
811  SMTRAT_LOG_DEBUG("smtrat.cad", "Biggest root below PointComp(1): "
812  << isolatedRoots.back());
813  lower2.emplace_back(std::make_tuple(isolatedRoots.back(), poly, (int) (isolatedRoots.end() - isolatedRoots.begin())));
814  } else {
815  auto lb = std::lower_bound(isolatedRoots.begin(), isolatedRoots.end(), pointComp);
816  //poly has root above and below pointComp
817  SMTRAT_LOG_DEBUG("smtrat.cad", "Smallest root above PointComp(2): " << *lb);
818  upper2.emplace_back(std::make_tuple(*lb, poly, (int) (lb - isolatedRoots.begin()) + 1));
819  SMTRAT_LOG_DEBUG("smtrat.cad",
820  "Biggest root below PointComp(2): " << *(lb - 1));
821  lower2.emplace_back(std::make_tuple(*(lb - 1), poly, (int) (lb - isolatedRoots.begin())));
822  }
823  }
824  //sort closest roots of pols below and above sample
825  std::sort(lower2.begin(), lower2.end(), [](auto const &t1, auto const &t2) {
826  return std::get<0>(t1) < std::get<0>(t2);
827  });
828  std::sort(upper2.begin(), upper2.end(), [](auto const &t1, auto const &t2) {
829  return std::get<0>(t1) < std::get<0>(t2);
830  });
831 
832  if (!lower2.empty()) {
833  //optimization: for multiple entries with the same root in lower2, sort the one with the
834  // lowest degree to the biggest possible position for optimal resultant calculation
835  for (auto it = lower2.begin() + 1; it != lower2.end(); it++) {
836  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
837  std::get<1>(*(it - 1)).deg > std::get<1>(*it).deg) {
838  std::iter_swap(it - 1, it);
839  }
840  }
841 
842  //set lower bound
843  curLow = std::get<1>(lower2.back());
844  sector.lowBound = Section{
845  asRootExpr(rootVariable, curLow.poly, std::get<2>(lower2.back())),
846  std::get<0>(lower2.back())};
847  SMTRAT_LOG_TRACE("smtrat.cad", "Lower bound: " << " " << sector);
848 
849  } else {
850  SMTRAT_LOG_TRACE("smtrat.cad", "Open lower bound");
851  }
852 
853  if (!upper2.empty()) {
854  //optimization: for multiple entries with the same root in upper2, sort the one with the
855  // lowest degree to the smallest possible position for optimal resultant calculation
856  for (auto it = upper2.begin() + 1; it != upper2.end(); it++) {
857  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
858  std::get<1>(*(it - 1)).deg > std::get<1>(*it).deg) {
859  std::iter_swap(it - 1, it);
860  }
861  }
862 
863  //set upper bound
864  curUp = std::get<1>(upper2.front());
865  sector.highBound = Section{
866  asRootExpr(rootVariable, curUp.poly, std::get<2>(upper2.front())),
867  std::get<0>(upper2.front())};
868  SMTRAT_LOG_TRACE("smtrat.cad", "Upper bound: "
869  << " " << sector);
870 
871  } else {
872  SMTRAT_LOG_TRACE("smtrat.cad", "Open upper bound");
873  }
874  } else {
875  SMTRAT_LOG_WARN("smtrat.cad", "Building failed: Incorrect heuristic input");
876  return std::nullopt;
877  }
878  SMTRAT_LOG_TRACE("smtrat.cad", "Determined bounds of sector: " << sector);
879 
880 
881  /** Projection part for sector case*/
882  if (i != 0) {
883  SMTRAT_LOG_TRACE("smtrat.cad", "Begin projection in sector case");
884  for (auto &poly : polys[i]) {
885  //Add discriminant
886  Poly disc = discriminant(variableOrder[i], poly.poly);
887  SMTRAT_LOG_TRACE("smtrat.cad",
888  "Add discriminant(" << poly.poly << ") = " << disc << " (if not const)");
889  appendOnCorrectLevel(disc, InvarianceType::ORD_INV, polys, variableOrder);
890 
891  SMTRAT_LOG_TRACE("smtrat.cad", "Check for vanishing coefficient");
892  auto coeff = coeffNonNull(poly);
893  if (coeff.has_value()) {
894  SMTRAT_LOG_TRACE("smtrat.cad",
895  "Add result of coeffNonNull: " << coeff.value() << " (if not const)");
896  appendOnCorrectLevel(coeff.value(), InvarianceType::SIGN_INV, polys, variableOrder);
897  }
898 
899  poly.tag = InvarianceType::ORD_INV;
900  }
901 
902  //Calculate and comulatively append resultants and leadcoefficients
903  std::vector<std::pair<Poly, Poly>> resultants;
904 
905  if (sector.lowBound.has_value() && sector.highBound.has_value() &&
906  sector.lowBound->boundFunction.poly() !=
907  sector.highBound->boundFunction.poly()) {
908 
909  resultants.emplace_back(std::make_pair(curLow.poly, curUp.poly));
910  }
911 
912  if (sectorHeuristic == 1) {
913  //Heuristic 1: calculate resultant between upper/lower bound and every polynomial above/below
914  if (sector.lowBound.has_value()) {
915  for (const auto &l : lower1) {
916  if (l.poly != curLow.poly) {
917  resultants.emplace_back(std::make_pair(l.poly, curLow.poly));
918  }
919  }
920  #ifdef SMTRAT_DEVOPTION_Statistics
921  getStatistic().resultantBarrierCreated();
922  #endif
923  }
924 
925  if (sector.highBound.has_value()) {
926  for (const auto &u : upper1) {
927  if (u.poly != curUp.poly) {
928  resultants.emplace_back(std::make_pair(u.poly, curUp.poly));
929  }
930  }
931  #ifdef SMTRAT_DEVOPTION_Statistics
932  getStatistic().resultantBarrierCreated();
933  #endif
934  }
935 
936  // Need no ldcf if it also appears on other side
937  for (auto &element : lower2) {
938  if (std::find_if(upper2.begin(), upper2.end(),
939  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(element).poly); }) !=
940  upper2.end()) {
941  noLdcf.emplace_back(std::get<1>(element).poly);
942  }
943  }
944 
945  for (auto &element : upper2) {
946  if (std::find_if(lower2.begin(), lower2.end(),
947  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(element).poly); }) !=
948  lower2.end()) {
949  noLdcf.emplace_back(std::get<1>(element).poly);
950  }
951  }
952 
953  } else if (sectorHeuristic == 2) {
954  //Heuristic 2: calculate resultant in chain-form over lower2 and upper2
955  if (sector.lowBound.has_value()) {
956  for (auto it = lower2.begin(); it != lower2.end() - 1; it++) {
957  resultants.emplace_back(std::make_pair(std::get<1>(*it).poly,
958  std::get<1>(*(it + 1)).poly));
959  #ifdef SMTRAT_DEVOPTION_Statistics
960  getStatistic().resultantBarrierCreated();
961  #endif
962  }
963  }
964 
965  if (sector.highBound.has_value()) {
966  for (auto it = upper2.begin(); it != upper2.end() - 1; it++) {
967  resultants.emplace_back(std::make_pair(std::get<1>(*it).poly,
968  std::get<1>(*(it + 1)).poly));
969  #ifdef SMTRAT_DEVOPTION_Statistics
970  getStatistic().resultantBarrierCreated();
971  #endif
972  }
973  }
974 
975  // Need no ldcf if its beginning or end of resultant-chain and has poly above and below sample
976  if (!lower2.empty() && std::find_if(upper2.begin(), upper2.end(), [&](auto const &t1) {
977  return (std::get<1>(t1).poly == std::get<1>(*lower2.begin()).poly);
978  }) != upper2.end()) {
979  noLdcf.emplace_back(std::get<1>(*lower2.begin()).poly);
980  }
981  if (!upper2.empty() && std::find_if(lower2.begin(), lower2.end(), [&](auto const &t1) {
982  return (std::get<1>(t1).poly == std::get<1>(*(upper2.end() - 1)).poly);
983  }) != lower2.end()) {
984  noLdcf.emplace_back(std::get<1>(*(upper2.end() - 1)).poly);
985  }
986 
987  } else if (sectorHeuristic == 3) {
988  //heuristic 3: smart
989  if (!lower2.empty()) {
990  //optimization: for multiple entries with the same root in lower, sort the one with the
991  // lowest degree to the smallest possible position for optimal resultant calculation
992  for (auto it = lower2.begin() + 1; it != lower2.end(); it++) {
993  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
994  std::get<1>(*(it - 1)).deg < std::get<1>(*it).deg) {
995  std::iter_swap(it - 1, it);
996  }
997  }
998 
999  auto mark = lower2.rend()-1;
1000  while (mark != lower2.rbegin()) {
1001  auto cur = std::min_element(lower2.rbegin(), mark,
1002  [](auto const &t1, auto const &t2) {
1003  return std::get<1>(t1).deg < std::get<1>(t2).deg;
1004  });
1005 
1006  for (auto it = cur + 1; it != mark+1; it++) {
1007  resultants.emplace_back(std::get<1>(*cur).poly, std::get<1>(*it).poly);
1008  // Ldcfs of pols not necessary if they are only connected to 1 pol AND also appear on the other side of sample point
1009  if (std::find_if(upper2.begin(), upper2.end(),
1010  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(*it).poly); }) !=
1011  upper2.end()) {
1012  noLdcf.emplace_back(std::get<1>(*it).poly);
1013  }
1014  }
1015 
1016  mark = cur;
1017  #ifdef SMTRAT_DEVOPTION_Statistics
1018  getStatistic().resultantBarrierCreated();
1019  #endif
1020  }
1021  }
1022 
1023  if (!upper2.empty()) {
1024  //optimization: for multiple entries with the same root in upper, sort the one with the
1025  // lowest degree to the smallest possible position for optimal resultant calculation
1026  for (auto it = upper2.begin() + 1; it != upper2.end(); it++) {
1027  if (std::get<0>(*(it - 1)) == std::get<0>(*it) &&
1028  std::get<1>(*(it - 1)).deg > std::get<1>(*it).deg) {
1029  std::iter_swap(it - 1, it);
1030  }
1031  }
1032 
1033  auto mark = upper2.end()-1;
1034  while (mark != upper2.begin()) {
1035  auto cur = std::min_element(upper2.begin(), mark,
1036  [](auto const &t1, auto const &t2) {
1037  return std::get<1>(t1).deg <
1038  std::get<1>(t2).deg;
1039  });
1040 
1041  for (auto it = cur + 1; it != mark+1; it++) {
1042  resultants.emplace_back(std::get<1>(*cur).poly, std::get<1>(*it).poly);
1043  // Ldcfs of pols not necessary if they are only connected to 1 pol AND also appear on the other side of sample point
1044  if (std::find_if(lower2.begin(), lower2.end(),
1045  [&](auto const &t1) { return (std::get<1>(t1).poly == std::get<1>(*it).poly); }) !=
1046  lower2.end()) {
1047  noLdcf.emplace_back(std::get<1>(*it).poly);
1048  }
1049  }
1050 
1051  mark = cur;
1052  #ifdef SMTRAT_DEVOPTION_Statistics
1053  getStatistic().resultantBarrierCreated();
1054  #endif
1055  }
1056  }
1057 
1058  } else {
1059  SMTRAT_LOG_WARN("smtrat.cad", "Building failed: Incorrect heuristic input");
1060  return std::nullopt;
1061  }
1062 
1063  lower1.clear();
1064  upper1.clear();
1065  lower2.clear();
1066  upper2.clear();
1067 
1068  //Add resultants and leadcoefficients depending on heuristic
1069  addResultants(resultants, polys, variableOrder[i], variableOrder);
1070 
1071  for (auto &poly : polys[i]) {
1072  if (!contains(noLdcf, poly.poly)) {
1073  Poly ldcf = leadcoefficient(variableOrder[i], poly.poly);
1074  SMTRAT_LOG_TRACE("smtrat.cad", "Add leadcoefficient(" << poly.poly << ") = " << ldcf << " (if not const)");
1075  appendOnCorrectLevel(ldcf, InvarianceType::SIGN_INV, polys, variableOrder);
1076  }
1077  }
1078 
1079  /** optimize memory*/
1080  resultants.clear();
1081  } else {
1082  SMTRAT_LOG_TRACE("smtrat.cad", "Level 1, so no projection");
1083  }
1084  }
1085  /** optimize memory*/
1086  polys[i].clear();
1087  }
1088 
1089  SMTRAT_LOG_DEBUG("smtrat.cad", "Finished Cell: " << cell);
1090  assert(isMainPointInsideCell(cell));
1091  return cell;
1092  }
1093 };
1094 
1095 
1096 } // namespace levelwise
1097 } // namespace onecellcad
1098 } // namespace mcsat
1099 } // namespace smtrat
smtrat::mcsat::onecellcad::OneCellCAD::variableOrder
const std::vector< carl::Variable > & variableOrder
Variables can also be indexed by level.
Definition: utils.h:455
smtrat::mcsat::onecellcad::OneCellCAD::coeffNonNull
std::optional< Poly > coeffNonNull(const TagPoly &boundCandidate)
Definition: utils.h:529
smtrat::mcsat::onecellcad::OneCellCAD::isPointRootOfPoly
bool isPointRootOfPoly(const std::size_t polyLevel, const Poly &poly)
Definition: utils.h:511
smtrat::mcsat::onecellcad::OneCellCAD::vanishesEarly
bool vanishesEarly(const std::size_t polyLevel, const Poly &poly)
Check if an n-variate 'poly' p(x1,..,xn) with n>=1 already becomes the zero poly after plugging in p(...
Definition: utils.h:498
smtrat::mcsat::onecellcad::OneCellCAD::isolateLastVariableRoots
std::vector< RAN > isolateLastVariableRoots(const std::size_t polyLevel, const Poly &poly)
src/lib/datastructures/mcsat/onecellcad/OneCellCAD.h Given a poly p(x1,..,xn), return all roots of th...
Definition: utils.h:484
smtrat::mcsat::onecellcad::OneCellCAD::isMainPointInsideCell
bool isMainPointInsideCell(const CADCell &cell)
Definition: utils.h:574
smtrat::mcsat::onecellcad::OneCellCAD::point
const RealAlgebraicPoint< Rational > & point
Definition: utils.h:456
smtrat::mcsat::onecellcad::OneCellCAD::OneCellCAD
OneCellCAD(const std::vector< carl::Variable > &variableOrder, const RealAlgebraicPoint< Rational > &point)
Definition: utils.h:459
smtrat::mcsat::onecellcad::RealAlgebraicPoint::dim
std::size_t dim() const
Give the dimension/number of components of this point.
Definition: RealAlgebraicPoint.h:59
smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD::constructCADCellEnclosingPoint
std::optional< CADCell > constructCADCellEnclosingPoint(std::vector< std::vector< TagPoly >> &polys, int sectionHeuristic, int sectorHeuristic)
Construct a single CADCell that contains the given 'point' and is sign-invariant for the given polyno...
Definition: OneCellCAD.h:46
Minisat::sort
void sort(T *array, int size, LessThan lt)
Definition: Sort.h:67
smtrat::mcsat::onecellcad::CADCell
std::vector< std::variant< Sector, Section > > CADCell
Represent a single cell [brown15].
Definition: utils.h:280
smtrat::mcsat::onecellcad::isNonConstIrreducible
bool isNonConstIrreducible(const PolyType &poly)
Definition: Assertables.h:37
smtrat::mcsat::onecellcad::contains
bool contains(const std::vector< TagPoly > &polys, const Poly &poly)
Definition: utils.h:314
smtrat::mcsat::onecellcad::RAN
smtrat::RAN RAN
Definition: utils.h:31
smtrat::mcsat::onecellcad::asMultiPolys
std::vector< Poly > asMultiPolys(const std::vector< TagPoly > polys)
Definition: utils.h:307
smtrat::mcsat::onecellcad::appendOnCorrectLevel
void appendOnCorrectLevel(const Poly &poly, InvarianceType tag, std::vector< std::vector< TagPoly >> &polys, std::vector< carl::Variable > variableOrder)
Definition: utils.h:186
smtrat::mcsat::onecellcad::getDegree
std::size_t getDegree(TagPoly p, carl::Variable v)
Definition: utils.h:115
smtrat::mcsat::onecellcad::polyVarsAreAllInList
bool polyVarsAreAllInList(const std::vector< PolyType > &polys, const std::vector< carl::Variable > &variables)
Definition: Assertables.h:69
smtrat::mcsat::onecellcad::leadcoefficient
Poly leadcoefficient(const carl::Variable &mainVariable, const Poly &p)
Definition: utils.h:412
smtrat::mcsat::onecellcad::asRootExpr
MultivariateRootT asRootExpr(carl::Variable rootVariable, Poly poly, std::size_t rootIdx)
Definition: utils.h:330
smtrat::mcsat::onecellcad::fullSpaceCell
CADCell fullSpaceCell(std::size_t cellComponentCount)
Definition: utils.h:446
smtrat::mcsat::onecellcad::addResultants
void addResultants(std::vector< std::pair< Poly, Poly >> &resultants, std::vector< std::vector< TagPoly >> &polys, carl::Variable mainVar, const std::vector< carl::Variable > &variableOrder)
Definition: utils.h:417
smtrat::mcsat::onecellcad::duplicateElimination
std::vector< std::pair< Poly, Poly > > duplicateElimination(std::vector< std::pair< Poly, Poly >> vec)
Definition: utils.h:355
smtrat::mcsat::onecellcad::hasOnlyNonConstIrreducibles
bool hasOnlyNonConstIrreducibles(const std::vector< PolyType > &polys)
Definition: Assertables.h:23
smtrat::mcsat::onecellcad::discriminant
Poly discriminant(const carl::Variable &mainVariable, const Poly &p)
Projection related utilities for onecellcad.
Definition: utils.h:398
smtrat
Class to create the formulas for axioms.
Definition: handle_options.h:10
smtrat::Poly
carl::MultivariatePolynomial< Rational > Poly
Definition: types.h:25
SMTRAT_LOG_TRACE
#define SMTRAT_LOG_TRACE(channel, msg)
Definition: logging.h:36
SMTRAT_LOG_WARN
#define SMTRAT_LOG_WARN(channel, msg)
Definition: logging.h:33
SMTRAT_LOG_INFO
#define SMTRAT_LOG_INFO(channel, msg)
Definition: logging.h:34
SMTRAT_LOG_DEBUG
#define SMTRAT_LOG_DEBUG(channel, msg)
Definition: logging.h:35
smtrat::mcsat::onecellcad::Section
Represent a cell's (closed-interval-boundary) component along th k-th axis.
Definition: utils.h:231
smtrat::mcsat::onecellcad::Sector
Represent a cell's open-interval boundary object along one single axis by two irreducible,...
Definition: utils.h:258
smtrat::mcsat::onecellcad::Sector::highBound
std::optional< Section > highBound
A std:nullopt highBound represents infinity.
Definition: utils.h:263
smtrat::mcsat::onecellcad::Sector::lowBound
std::optional< Section > lowBound
A std::nullopt lowBound represents negative infinity.
Definition: utils.h:260
smtrat::mcsat::onecellcad::TagPoly
Tagged Polynomials.
Definition: utils.h:71