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

#include <utils.h>

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

Public Member Functions

 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 450 of file utils.h.

Constructor & Destructor Documentation

◆ OneCellCAD()

smtrat::mcsat::onecellcad::OneCellCAD::OneCellCAD ( const std::vector< carl::Variable > &  variableOrder,
const RealAlgebraicPoint< Rational > &  point 
)
inline

Definition at line 459 of file utils.h.

Here is the call graph for this function:

Member Function Documentation

◆ coeffNonNull()

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

Definition at line 529 of file utils.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)
inline

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

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

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

Definition at line 524 of file utils.h.

Here is the call graph for this function:

◆ prefixPointToStdMap()

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

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

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

Definition at line 456 of file utils.h.

◆ variableOrder

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

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: