SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Data Fields
smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD Class Reference

#include <OneCellCAD.h>

Inheritance diagram for smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD:
Inheritance graph
[legend]
Collaboration diagram for smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD:
Collaboration graph
[legend]

Public Member Functions

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 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)
 

Data Fields

const std::vector< carl::Variable > & variableOrder
 Variables can also be indexed by level. More...
 
const RealAlgebraicPoint< Rational > & point
 

Detailed Description

Definition at line 29 of file OneCellCAD.h.

Member Function Documentation

◆ coeffNonNull()

std::optional<Poly> smtrat::mcsat::onecellcad::OneCellCAD::coeffNonNull ( const TagPoly &  boundCandidate)
inlineinherited

Definition at line 529 of file utils.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ constructCADCellEnclosingPoint()

std::optional<CADCell> smtrat::mcsat::onecellcad::levelwise::LevelwiseCAD::constructCADCellEnclosingPoint ( std::vector< std::vector< TagPoly >> &  polys,
int  sectionHeuristic,
int  sectorHeuristic 
)
inline

Construct a single CADCell that contains the given 'point' and is sign-invariant for the given polynomials in 'polys'.

The construction fails if a polynomial vanishes ( p(a_1,...,a_i-1,x_i) ). Note that this cell is cylindrical only with respect to the given 'variableOrder'.

Parameters
variableOrdermust contain unique variables and at least one, because constant polynomials (without a variable) are prohibited.
pointpoint.size() >= variables.size().
polysmust contain only non-constant, irreducible tagged polynomials that mention only variables that appear in 'variableOrder'.

Current level is a Section

Projection part for section case

Current level is a Sector

Projection part for sector case

optimize memory

optimize memory

Definition at line 46 of file OneCellCAD.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isMainPointInsideCell()

bool smtrat::mcsat::onecellcad::OneCellCAD::isMainPointInsideCell ( const CADCell &  cell)
inlineinherited

Definition at line 574 of file utils.h.

Here is the caller graph for this function:

◆ isolateLastVariableRoots()

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.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isPointRootOfPoly() [1/2]

bool smtrat::mcsat::onecellcad::OneCellCAD::isPointRootOfPoly ( const std::size_t  polyLevel,
const Poly &  poly 
)
inlineinherited

Definition at line 511 of file utils.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ isPointRootOfPoly() [2/2]

bool smtrat::mcsat::onecellcad::OneCellCAD::isPointRootOfPoly ( const TagPoly &  poly)
inlineinherited

Definition at line 524 of file utils.h.

Here is the call graph for this function:

◆ OneCellCAD()

smtrat::mcsat::onecellcad::OneCellCAD::OneCellCAD
inline

Definition at line 459 of file utils.h.

◆ prefixPointToStdMap()

std::map<carl::Variable, RAN> smtrat::mcsat::onecellcad::OneCellCAD::prefixPointToStdMap ( const std::size_t  componentCount)
inlineinherited

Create a mapping from the first variables (with index 0 to 'componentCount') in the 'variableOrder' to the first components of the given 'point'.

Definition at line 471 of file utils.h.

Here is the caller graph for this function:

◆ vanishesEarly()

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.

Here is the call graph for this function:
Here is the caller graph for this function:

Field Documentation

◆ point

const RealAlgebraicPoint<Rational>& smtrat::mcsat::onecellcad::OneCellCAD::point
inherited

Definition at line 456 of file utils.h.

◆ variableOrder

const std::vector<carl::Variable>& smtrat::mcsat::onecellcad::OneCellCAD::variableOrder
inherited

Variables can also be indexed by level.

Polys with mathematical level 1 contain the variable in variableOrder[0]

Definition at line 455 of file utils.h.

The documentation for this class was generated from the following file: