|
| bool | isAlreadyProcessed (const TagPoly &poly) |
| |
| void | shrinkSingleComponent (const std::size_t polyLevel, const Poly &poly, CADCell &cell) |
| | Shrink the component of the 'cell' at the 'boundCandidate's level around the given point if the 'boundCandidate' is a tighter bound. More...
|
| |
| std::vector< Poly > | partialDerivativesLayerWithSomeNonEarlyVanishingPoly (const TagPoly &mainPoly) |
| | Find the smallest index m such that in the set S of all m-th partial derivatives of the given poly, such that there is a derivative that does not vanish early [brown15]. More...
|
| |
| ShrinkResult | refineNull (const TagPoly &boundCandidate, CADCell &cell) |
| |
| ShrinkResult | shrinkCellWithEarlyVanishingPoly (const TagPoly &boundCandidate, CADCell &cell) |
| |
| ShrinkResult | shrinkCellWithIrreducibleFactorsOfPoly (const TagPoly &poly, CADCell &cell) |
| |
| ShrinkResult | refineNonNull (const TagPoly &boundCandidate, CADCell &cell) |
| |
| ShrinkResult | shrinkCellWithPolyHavingPointAsRoot (const TagPoly &boundCandidate, CADCell &cell) |
| |
| bool | hasPolyLastVariableRootWithinBounds (const RAN &low, const RAN &high, const Poly &poly, const std::size_t polyLevel) |
| | Check if there is a root of the given polynomial—that becomes univariate after pluggin in all but the last variable wrt. More...
|
| |
| ShrinkResult | shrinkCellWithNonRootPoint (const TagPoly &boundCandidate, CADCell &cell) |
| |
| ShrinkResult | shrinkCell (const TagPoly &boundCandidate, CADCell &cell) |
| | Merge the given open OpenCADCell 'cell' that contains the given 'point' (called "alpha" in [brown15]) with a polynomial 'poly'. More...
|
| |
| std::optional< CADCell > | pointEnclosingCADCell (const std::vector< std::vector< onecellcad::TagPoly >> &polys) |
| | Construct a single CADCell that contains the given 'point' and is sign-invariant for the given polynomials in 'polys'. More...
|
| |
| | OneCellCAD (const std::vector< carl::Variable > &variableOrder, const RealAlgebraicPoint< Rational > &point) |
| |
| std::map< carl::Variable, RAN > | prefixPointToStdMap (const std::size_t componentCount) |
| | Create a mapping from the first variables (with index 0 to 'componentCount') in the 'variableOrder' to the first components of the given 'point'. More...
|
| |
| 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 the univariate poly p(a1,..,an-1, xn), where a1,..an-1 are the first algebraic real components from 'point' (SORTED!). More...
|
| |
| 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(a1,..,an-1, xn), where a1,..an-1 are the first n-1 algebraic real components from 'point'. More...
|
| |
| bool | isPointRootOfPoly (const std::size_t polyLevel, const Poly &poly) |
| |
| bool | isPointRootOfPoly (const TagPoly &poly) |
| |
| std::optional< Poly > | coeffNonNull (const TagPoly &boundCandidate) |
| |
| bool | isMainPointInsideCell (const CADCell &cell) |
| |
Definition at line 45 of file OneCellCAD.h.
| std::vector<RAN> smtrat::mcsat::onecellcad::OneCellCAD::isolateLastVariableRoots |
( |
const std::size_t |
polyLevel, |
|
|
const Poly & |
poly |
|
) |
| |
|
inlineinherited |
src/lib/datastructures/mcsat/onecellcad/OneCellCAD.h Given a poly p(x1,..,xn), return all roots of the univariate poly p(a1,..,an-1, xn), where a1,..an-1 are the first algebraic real components from 'point' (SORTED!).
Definition at line 484 of file utils.h.
| std::vector<Poly> smtrat::mcsat::onecellcad::recursive::RecursiveCAD::partialDerivativesLayerWithSomeNonEarlyVanishingPoly |
( |
const TagPoly & |
mainPoly | ) |
|
|
inline |
Find the smallest index m such that in the set S of all m-th partial derivatives of the given poly, such that there is a derivative that does not vanish early [brown15].
Note that m > 0 i.e, this function never just returns the given poly, which is the 0th partial derivative of itself.
- Parameters
-
| poly | must not be a const-poly like 2, otherwise this function does not terminate. |
- Returns
- Actually only returns the set S
Definition at line 179 of file OneCellCAD.h.
| void smtrat::mcsat::onecellcad::recursive::RecursiveCAD::shrinkSingleComponent |
( |
const std::size_t |
polyLevel, |
|
|
const Poly & |
poly, |
|
|
CADCell & |
cell |
|
) |
| |
|
inline |
Shrink the component of the 'cell' at the 'boundCandidate's level around the given point if the 'boundCandidate' is a tighter bound.
Don't recursively shrink lower level components of the cell. Note that a cell's sector may collapse into a section, which is why we need to pass in a cell and not only its sector. Note that this shrink function is always "successful", even if the cell was not shrunk.
- Parameters
-
| boundCandidate | Must be a non-const irreducible polynomial that does not vanish early. |
Definition at line 83 of file OneCellCAD.h.
| bool smtrat::mcsat::onecellcad::OneCellCAD::vanishesEarly |
( |
const std::size_t |
polyLevel, |
|
|
const Poly & |
poly |
|
) |
| |
|
inlineinherited |
Check if an n-variate 'poly' p(x1,..,xn) with n>=1 already becomes the zero poly after plugging in p(a1,..,an-1, xn), where a1,..an-1 are the first n-1 algebraic real components from 'point'.
Definition at line 498 of file utils.h.
1.9.1 
