Namespaces
	levelwise

	recursive
	OneCell Explanation.

Data Structures
class	RealAlgebraicPoint
	Represent a multidimensional point whose components are algebraic reals. More...

struct	TagPoly
	Tagged Polynomials. More...

struct	Section
	Represent a cell's (closed-interval-boundary) component along th k-th axis. More...

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

class	OneCellCAD

Typedefs
using	RAN = smtrat::RAN

using	RANMap = std::map< carl::Variable, RAN >

using	CADCell = std::vector< std::variant< Sector, Section > >
	Represent a single cell [brown15]. More...

Enumerations
enum class	InvarianceType { ORD_INV , SIGN_INV }
	Invariance Types. More...

Functions
template<typename PolyType >
bool	hasOnlyNonConstIrreducibles (const std::vector< PolyType > &polys)

template<typename PolyType >
bool	isNonConstIrreducible (const PolyType &poly)

template<typename T >
bool	hasUniqElems (const std::vector< T > &container)

template<typename T >
bool	isSubset (const std::vector< T > &c1, const std::vector< T > &c2)

template<typename T >
std::vector< T >	asVector (const std::set< T > s)

template<typename PolyType >
bool	polyVarsAreAllInList (const std::vector< PolyType > &polys, const std::vector< carl::Variable > &variables)

template<typename Number >
bool	operator== (RealAlgebraicPoint< Number > &lhs, RealAlgebraicPoint< Number > &rhs)
	Check if two RealAlgebraicPoints are equal. More...

template<typename Number >
std::ostream &	operator<< (std::ostream &os, const RealAlgebraicPoint< Number > &r)
	Streaming operator for a RealAlgebraicPoint. More...

std::ostream &	operator<< (std::ostream &os, const InvarianceType &inv)

bool	operator< (const InvarianceType &l, const InvarianceType &r)

std::ostream &	operator<< (std::ostream &os, const TagPoly &p)

bool	operator== (const TagPoly &lhs, const TagPoly &rhs)

std::ostream &	operator<< (std::ostream &os, const std::vector< TagPoly > &polys)

std::ostream &	operator<< (std::ostream &os, const std::vector< std::vector< TagPoly >> &lvls)

std::size_t	getDegree (TagPoly p, carl::Variable v)

std::optional< std::size_t >	levelOf (const std::vector< carl::Variable > &variableOrder, const Poly &poly)
	Find the index of the highest variable (wrt. More...

std::vector< TagPoly >	nonConstIrreducibleFactors (std::vector< carl::Variable > variableOrder, Poly poly, InvarianceType tag)

void	appendOnCorrectLevel (const Poly &poly, InvarianceType tag, std::vector< std::vector< TagPoly >> &polys, std::vector< carl::Variable > variableOrder)

std::ostream &	operator<< (std::ostream &os, const Section &s)

std::ostream &	operator<< (std::ostream &os, const Sector &s)

std::ostream &	operator<< (std::ostream &os, const CADCell &cell)

std::vector< Poly >	asMultiPolys (const std::vector< TagPoly > polys)

bool	contains (const std::vector< TagPoly > &polys, const Poly &poly)

template<typename T >
bool	contains (const std::vector< T > &list, const T &elem)

MultivariateRootT	asRootExpr (carl::Variable rootVariable, Poly poly, std::size_t rootIdx)

RealAlgebraicPoint< smtrat::Rational >	asRANPoint (const mcsat::Bookkeeping &data)

template<typename T >
std::vector< T >	prefix (const std::vector< T > vars, std::size_t prefixSize)

std::vector< std::pair< Poly, Poly > >	duplicateElimination (std::vector< std::pair< Poly, Poly >> vec)

void	duplicateElimination (std::vector< Poly > &vec)

Poly	discriminant (const carl::Variable &mainVariable, const Poly &p)
	Projection related utilities for onecellcad. More...

Poly	resultant (const carl::Variable &mainVariable, const Poly &p1, const Poly &p2)

Poly	leadcoefficient (const carl::Variable &mainVariable, const Poly &p)

void	addResultants (std::vector< std::pair< Poly, Poly >> &resultants, std::vector< std::vector< TagPoly >> &polys, carl::Variable mainVar, const std::vector< carl::Variable > &variableOrder)

std::size_t	cellDimension (const CADCell &cell, const std::size_t uptoLevel)

CADCell	fullSpaceCell (std::size_t cellComponentCount)

bool	optimized_singleLevelFullProjection (carl::Variable mainVar, size_t currentLevel, std::vector< std::vector< TagPoly >> &projectionLevels, OneCellCAD &cad)

void	singleLevelFullProjection (std::vector< carl::Variable > &variableOrder, carl::Variable mainVar, size_t currentLevel, std::vector< std::vector< TagPoly >> &projectionLevels)

Typedef Documentation

◆ CADCell

using smtrat::mcsat::onecellcad::CADCell = typedef std::vector<std::variant<Sector, Section> >

Represent a single cell [brown15].

A cell is a collection of boundary objects along each axis, called cell-components based on math. vectors and their components.

Definition at line 280 of file utils.h.

◆ RAN

using smtrat::mcsat::onecellcad::RAN = typedef smtrat::RAN

Definition at line 31 of file utils.h.

◆ RANMap

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

Definition at line 33 of file utils.h.

Enumeration Type Documentation

◆ InvarianceType

enum smtrat::mcsat::onecellcad::InvarianceType

strong

Invariance Types.

Enumerator
ORD_INV
SIGN_INV

Definition at line 42 of file utils.h.

Function Documentation

◆ addResultants()

void smtrat::mcsat::onecellcad::addResultants	(	std::vector< std::pair< Poly, Poly >> &	resultants,
		std::vector< std::vector< TagPoly >> &	polys,
		carl::Variable	mainVar,
		const std::vector< carl::Variable > &	variableOrder
	)

inline

Definition at line 417 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ appendOnCorrectLevel()

void smtrat::mcsat::onecellcad::appendOnCorrectLevel	(	const Poly &	poly,
		InvarianceType	tag,
		std::vector< std::vector< TagPoly >> &	polys,
		std::vector< carl::Variable >	variableOrder
	)

inline

Definition at line 186 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asMultiPolys()

std::vector<Poly> smtrat::mcsat::onecellcad::asMultiPolys ( const std::vector< TagPoly > polys )

inline

Definition at line 307 of file utils.h.

Here is the caller graph for this function:

◆ asRANPoint()

RealAlgebraicPoint<smtrat::Rational> smtrat::mcsat::onecellcad::asRANPoint ( const mcsat::Bookkeeping & data )

inline

Definition at line 336 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asRootExpr()

MultivariateRootT smtrat::mcsat::onecellcad::asRootExpr	(	carl::Variable	rootVariable,
		Poly	poly,
		std::size_t	rootIdx
	)

inline

Parameters

rootVariable The variable with respect to which the roots are computed in the end. It will be replaced by the special unique root-variable "_z" common in root-expressions.

Definition at line 330 of file utils.h.

Here is the caller graph for this function:

◆ asVector()

template<typename T >

std::vector<T> smtrat::mcsat::onecellcad::asVector ( const std::set< T > s )

Definition at line 58 of file Assertables.h.

◆ cellDimension()

std::size_t smtrat::mcsat::onecellcad::cellDimension	(	const CADCell &	cell,
		const std::size_t	uptoLevel
	)

inline

Returns: Dimension of a hybercube to which the given cell is homeomorphic, i.e., count the number of sectors of the given Cell restricted to its first components (with index 0 to 'uptoLevel').

Definition at line 438 of file utils.h.

Here is the caller graph for this function:

◆ contains() [1/2]

template<typename T >

bool smtrat::mcsat::onecellcad::contains	(	const std::vector< T > &	list,
		const T &	elem
	)

Definition at line 322 of file utils.h.

Here is the call graph for this function:

◆ contains() [2/2]

bool smtrat::mcsat::onecellcad::contains	(	const std::vector< TagPoly > &	polys,
		const Poly &	poly
	)

inline

Definition at line 314 of file utils.h.

Here is the caller graph for this function:

◆ discriminant()

Poly smtrat::mcsat::onecellcad::discriminant	(	const carl::Variable &	mainVariable,
		const Poly &	p
	)

inline

Projection related utilities for onecellcad.

Definition at line 398 of file utils.h.

Here is the caller graph for this function:

◆ duplicateElimination() [1/2]

void smtrat::mcsat::onecellcad::duplicateElimination ( std::vector< Poly > & vec )

inline

Definition at line 375 of file utils.h.

◆ duplicateElimination() [2/2]

std::vector<std::pair<Poly, Poly> > smtrat::mcsat::onecellcad::duplicateElimination ( std::vector< std::pair< Poly, Poly >> vec )

inline

Definition at line 355 of file utils.h.

Here is the caller graph for this function:

◆ fullSpaceCell()

CADCell smtrat::mcsat::onecellcad::fullSpaceCell ( std::size_t cellComponentCount )

inline

Definition at line 446 of file utils.h.

Here is the caller graph for this function:

◆ getDegree()

std::size_t smtrat::mcsat::onecellcad::getDegree	(	TagPoly	p,
		carl::Variable	v
	)

inline

Parameters

p	Polynomial to get degree from
v	Rootvariable for degree calc

Returns

Definition at line 115 of file utils.h.

Here is the caller graph for this function:

◆ hasOnlyNonConstIrreducibles()

template<typename PolyType >

bool smtrat::mcsat::onecellcad::hasOnlyNonConstIrreducibles ( const std::vector< PolyType > & polys )

Definition at line 23 of file Assertables.h.

Here is the caller graph for this function:

◆ hasUniqElems()

template<typename T >

bool smtrat::mcsat::onecellcad::hasUniqElems ( const std::vector< T > & container )

Definition at line 42 of file Assertables.h.

Here is the caller graph for this function:

◆ isNonConstIrreducible()

template<typename PolyType >

bool smtrat::mcsat::onecellcad::isNonConstIrreducible ( const PolyType & poly )

Definition at line 37 of file Assertables.h.

Here is the caller graph for this function:

◆ isSubset()

template<typename T >

bool smtrat::mcsat::onecellcad::isSubset	(	const std::vector< T > &	c1,
		const std::vector< T > &	c2
	)

Definition at line 48 of file Assertables.h.

Here is the call graph for this function:

◆ leadcoefficient()

Poly smtrat::mcsat::onecellcad::leadcoefficient	(	const carl::Variable &	mainVariable,
		const Poly &	p
	)

inline

Definition at line 412 of file utils.h.

Here is the caller graph for this function:

◆ levelOf()

std::optional<std::size_t> smtrat::mcsat::onecellcad::levelOf	(	const std::vector< carl::Variable > &	variableOrder,
		const Poly &	poly
	)

inline

Find the index of the highest variable (wrt.

the ordering in 'variableOrder') that occurs with positive degree in 'poly'. Although 'level' is a math concept that starts counting at 1 we start counting at 0 and represent "no level/variable" as std::nullopt because it simplifies using the level directly as an index into arrays or vectors. Examples:

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

Definition at line 138 of file utils.h.

Here is the caller graph for this function:

◆ nonConstIrreducibleFactors()

std::vector<TagPoly> smtrat::mcsat::onecellcad::nonConstIrreducibleFactors	(	std::vector< carl::Variable >	variableOrder,
		Poly	poly,
		InvarianceType	tag
	)

inline

Definition at line 171 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator<()

bool smtrat::mcsat::onecellcad::operator<	(	const InvarianceType &	l,
		const InvarianceType &	r
	)

inline

Definition at line 58 of file utils.h.

◆ operator<<() [1/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const CADCell &	cell
	)

inline

Definition at line 282 of file utils.h.

◆ operator<<() [2/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const InvarianceType &	inv
	)

inline

Definition at line 47 of file utils.h.

◆ operator<<() [3/8]

template<typename Number >

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const RealAlgebraicPoint< Number > &	r
	)

Streaming operator for a RealAlgebraicPoint.

Definition at line 119 of file RealAlgebraicPoint.h.

Here is the call graph for this function:

◆ operator<<() [4/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const Section &	s
	)

inline

Definition at line 242 of file utils.h.

◆ operator<<() [5/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const Sector &	s
	)

inline

Definition at line 266 of file utils.h.

◆ operator<<() [6/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const std::vector< std::vector< TagPoly >> &	lvls
	)

inline

Definition at line 98 of file utils.h.

◆ operator<<() [7/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const std::vector< TagPoly > &	polys
	)

inline

Definition at line 91 of file utils.h.

◆ operator<<() [8/8]

std::ostream& smtrat::mcsat::onecellcad::operator<<	(	std::ostream &	os,
		const TagPoly &	p
	)

inline

Definition at line 83 of file utils.h.

◆ operator==() [1/2]

bool smtrat::mcsat::onecellcad::operator==	(	const TagPoly &	lhs,
		const TagPoly &	rhs
	)

inline

Definition at line 87 of file utils.h.

◆ operator==() [2/2]

template<typename Number >

bool smtrat::mcsat::onecellcad::operator==	(	RealAlgebraicPoint< Number > &	lhs,
		RealAlgebraicPoint< Number > &	rhs
	)

Check if two RealAlgebraicPoints are equal.

Definition at line 106 of file RealAlgebraicPoint.h.

Here is the call graph for this function:

◆ optimized_singleLevelFullProjection()

bool smtrat::mcsat::onecellcad::optimized_singleLevelFullProjection	(	carl::Variable	mainVar,
		size_t	currentLevel,
		std::vector< std::vector< TagPoly >> &	projectionLevels,
		OneCellCAD &	cad
	)

inline

Definition at line 602 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ polyVarsAreAllInList()

template<typename PolyType >

bool smtrat::mcsat::onecellcad::polyVarsAreAllInList	(	const std::vector< PolyType > &	polys,
		const std::vector< carl::Variable > &	variables
	)

Definition at line 69 of file Assertables.h.

Here is the caller graph for this function:

◆ prefix()

template<typename T >

std::vector<T> smtrat::mcsat::onecellcad::prefix	(	const std::vector< T >	vars,
		std::size_t	prefixSize
	)

Definition at line 349 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ resultant()

Poly smtrat::mcsat::onecellcad::resultant	(	const carl::Variable &	mainVariable,
		const Poly &	p1,
		const Poly &	p2
	)

inline

Definition at line 404 of file utils.h.

Here is the caller graph for this function:

◆ singleLevelFullProjection()

void smtrat::mcsat::onecellcad::singleLevelFullProjection	(	std::vector< carl::Variable > &	variableOrder,
		carl::Variable	mainVar,
		size_t	currentLevel,
		std::vector< std::vector< TagPoly >> &	projectionLevels
	)

inline

Definition at line 655 of file utils.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Namespaces

Data Structures

Typedefs

Enumerations

Functions

Typedef Documentation

◆ CADCell

◆ RAN

◆ RANMap

Enumeration Type Documentation

◆ InvarianceType

Function Documentation

◆ addResultants()

◆ appendOnCorrectLevel()

◆ asMultiPolys()

◆ asRANPoint()

◆ asRootExpr()

◆ asVector()

◆ cellDimension()

◆ contains() [1/2]

◆ contains() [2/2]

◆ discriminant()

◆ duplicateElimination() [1/2]

◆ duplicateElimination() [2/2]

◆ fullSpaceCell()

◆ getDegree()

◆ hasOnlyNonConstIrreducibles()

◆ hasUniqElems()

◆ isNonConstIrreducible()

◆ isSubset()

◆ leadcoefficient()

◆ levelOf()

◆ nonConstIrreducibleFactors()

◆ operator<()

◆ operator<<() [1/8]

◆ operator<<() [2/8]

◆ operator<<() [3/8]

◆ operator<<() [4/8]

◆ operator<<() [5/8]

◆ operator<<() [6/8]

◆ operator<<() [7/8]

◆ operator<<() [8/8]

◆ operator==() [1/2]

◆ operator==() [2/2]

◆ optimized_singleLevelFullProjection()

◆ polyVarsAreAllInList()

◆ prefix()

◆ resultant()

◆ singleLevelFullProjection()