smtrat::onecellcad::recursive Namespace Reference

Data Structures
struct	Section
	Represent a cell's closed-interval-boundary object along one single axis by an irreducible, multivariate polynomial of level k. More...
struct	Sector
	Represent a cell's open-interval boundary object along one single axis by two irreducible, multivariate polynomials of level k. More...

Typedefs
using	UniPoly = carl::UnivariatePolynomial< smtrat::Rational >
using	MultiPoly = carl::MultivariatePolynomial< smtrat::Rational >
using	MultiCoeffUniPoly = carl::UnivariatePolynomial< MultiPoly >
using	RANPoint = RealAlgebraicPoint< smtrat::Rational >
using	RANMap = std::map< carl::Variable, RAN >
using	OpenCADCell = std::vector< Sector >
	Represent a single open cell [1]. More...

Functions
std::ostream &	operator<< (std::ostream &o, const Section &s)
std::ostream &	operator<< (std::ostream &o, const Sector &s)
std::ostream &	operator<< (std::ostream &o, const OpenCADCell &c)
OpenCADCell	createFullspaceCoveringCell (size_t level)
size_t	levelOf (const MultiPoly &poly, const std::vector< carl::Variable > &variableOrder)
	Find the index of the highest variable (wrt. More...
std::map< carl::Variable, RAN >	toStdMap (const RANPoint &point, size_t count, const std::vector< carl::Variable > &variableOrder)
	Create a mapping from the first 'count'-many variables in the given 'variableOrder' to the first 'count'-many components of the given 'point'. More...
std::optional< OpenCADCell >	mergeCellWithPoly (OpenCADCell &cell, const RANPoint &point, const std::vector< carl::Variable > &variableOrder, const MultiPoly poly)
	Merge the given open OpenCADCell 'cell' that contains the given 'point' (called "alpha" in [1]) with a polynomial 'poly'. More...
std::optional< OpenCADCell >	createOpenCADCell (const std::vector< MultiPoly > polySet, const RANPoint &point, const std::vector< carl::Variable > &variableOrder)
	Construct a OpenCADCell for the given set of polynomials 'polySet' that contains the given 'point'. More...

Typedef Documentation

MultiCoeffUniPoly

using smtrat::onecellcad::recursive::MultiCoeffUniPoly = typedef carl::UnivariatePolynomial<MultiPoly>

Definition at line 39 of file OpenCAD.h.

MultiPoly

using smtrat::onecellcad::recursive::MultiPoly = typedef carl::MultivariatePolynomial<smtrat::Rational>

Definition at line 38 of file OpenCAD.h.

OpenCADCell

using smtrat::onecellcad::recursive::OpenCADCell = typedef std::vector<Sector>

Represent a single open cell [1].

A cell is a collection of boundary objects along each axis. In case of an open cell, the boundary objects are all sectors.

Definition at line 103 of file OpenCAD.h.

RANMap

using smtrat::onecellcad::recursive::RANMap = typedef std::map<carl::Variable, RAN>

Definition at line 41 of file OpenCAD.h.

RANPoint

using smtrat::onecellcad::recursive::RANPoint = typedef RealAlgebraicPoint<smtrat::Rational>

Definition at line 40 of file OpenCAD.h.

UniPoly

using smtrat::onecellcad::recursive::UniPoly = typedef carl::UnivariatePolynomial<smtrat::Rational>

Definition at line 37 of file OpenCAD.h.

Function Documentation

createFullspaceCoveringCell()

OpenCADCell smtrat::onecellcad::recursive::createFullspaceCoveringCell

(

size_t

level

)

Definition at line 113 of file OpenCAD.h.

Here is the caller graph for this function:

createOpenCADCell()

std::optional<OpenCADCell> smtrat::onecellcad::recursive::createOpenCADCell	(	const std::vector< MultiPoly >	polySet,
		const RANPoint &	point,
		const std::vector< carl::Variable > &	variableOrder
	)

Construct a OpenCADCell for the given set of polynomials 'polySet' that contains the given 'point'.

The returned cell represents the largest region that is sign-invariant on all polynomials in the 'polySet' and is cylindrical with respect to the variables ordering given in 'variableOrder'. Note that this construction is only correct if plugging in the 'point' into any polynomial of the 'polySet' yields a non-zero value, i.e. 'point' is not a root of any polynomial in 'polySet', otherwise no OpenCADCell is returned. Note that the dimension (number of components) of the 'point' == the number of variables in 'variableOrder' and that any polynomial of the 'polySet' must be irreducible and mention only variables from 'variableOrder'.

Definition at line 314 of file OpenCAD.h.

Here is the call graph for this function:

levelOf()

size_t smtrat::onecellcad::recursive::levelOf	(	const MultiPoly &	poly,
		const std::vector< carl::Variable > &	variableOrder
	)

Find the index of the highest variable (wrt.

the ordering in 'variableOrder') that occurs with positive degree in 'poly'. Since levelOf is a math concept it starts counting at 1! Examples:

• levelOf(2) == 0 wrt. any variable order
• levelOf(0*x+2) == 0 wrt. any variable order
• levelOf(x+2) == 1 wrt. [x < y < z]
• levelOf(x+2) == 2 wrt. [y < x < z]
• levelOf(x+2) == 3 wrt. [y < z < x]
• levelOf(x*y+2) == 2 wrt. [x < y < z] because of y
• levelOf(x*y+2) == 2 wrt. [y < x < z] because of x
• levelOf(x*y+2) == 3 wrt. [x < z < y] because of y Preconditions:
• 'variables(poly)' must be a subset of 'variableOrder'.

Definition at line 133 of file OpenCAD.h.

Here is the call graph for this function:

Here is the caller graph for this function:

mergeCellWithPoly()

std::optional<OpenCADCell> smtrat::onecellcad::recursive::mergeCellWithPoly	(	OpenCADCell &	cell,
		const RANPoint &	point,
		const std::vector< carl::Variable > &	variableOrder,
		const MultiPoly	poly
	)

Merge the given open OpenCADCell 'cell' that contains the given 'point' (called "alpha" in [1]) with a polynomial 'poly'.

Before the merge 'cell' represents a region that is sign-invariant on other (previously merged) polynomials (all signs are non-zero). The returned cell represents a region that is additionally sign-invariant on 'poly' (also with non-zero sign).

Returns

either an OpenCADCell or nothing (representing a failed construction)

Definition at line 181 of file OpenCAD.h.

Here is the call graph for this function:

Here is the caller graph for this function:

operator<<() [1/3]

std::ostream& smtrat::onecellcad::recursive::operator<<	(	std::ostream &	o,
		const OpenCADCell &	c
	)

Definition at line 105 of file OpenCAD.h.

operator<<() [2/3]

std::ostream& smtrat::onecellcad::recursive::operator<<	(	std::ostream &	o,
		const Section &	s
	)

Definition at line 61 of file OpenCAD.h.

operator<<() [3/3]

std::ostream& smtrat::onecellcad::recursive::operator<<	(	std::ostream &	o,
		const Sector &	s
	)

Definition at line 90 of file OpenCAD.h.

Here is the call graph for this function:

toStdMap()

std::map<carl::Variable, RAN> smtrat::onecellcad::recursive::toStdMap	(	const RANPoint &	point,
		size_t	count,
		const std::vector< carl::Variable > &	variableOrder
	)

Create a mapping from the first 'count'-many variables in the given 'variableOrder' to the first 'count'-many components of the given 'point'.

Definition at line 162 of file OpenCAD.h.

Here is the caller graph for this function: