#include <BaseProjection.h>

Inheritance diagram for smtrat::cad::BaseProjection< Settings >:

[legend]

Collaboration diagram for smtrat::cad::BaseProjection< Settings >:

[legend]

Public Member Functions
std::size_t	dim () const
	Returns the dimension of the projection. More...

const auto &	vars () const
	Returns the variables used for projection. More...

void	reset ()
	Resets all datastructures, use the given variables from now on. More...

template<typename F >
void	setRemoveCallback (F &&f)
	Sets a callback that is called whenever polynomials are removed. More...

carl::Bitset	addPolynomial (const Poly &p, std::size_t cid, bool isBound)
	Adds the given polynomial to the projection. Converts to a UPoly and calls the appropriate overload. More...

virtual carl::Bitset	addPolynomial (const UPoly &p, std::size_t cid, bool isBound)=0
	Adds the given polynomial to the projection. More...

carl::Bitset	addEqConstraint (const Poly &p, std::size_t cid, bool isBound)
	Adds the given polynomial of an equational constraint to the projection. Converts to a UPoly and calls the appropriate overload. More...

virtual carl::Bitset	addEqConstraint (const UPoly &p, std::size_t cid, bool isBound)
	Adds the given polynomial of an equational constraint to the projection. More...

void	removePolynomial (const Poly &p, std::size_t cid, bool isBound)
	Removes the given polynomial from the projection. Converts to a UPoly and calls the appropriate overload. More...

virtual void	removePolynomial (const UPoly &p, std::size_t cid, bool isBound)=0
	Removes the given polynomial from the projection. More...

virtual std::size_t	size (std::size_t level) const =0

std::size_t	size () const

virtual bool	empty (std::size_t level) const =0

virtual bool	empty ()

OptionalID	getPolyForLifting (std::size_t level, SampleLiftedWith &slw)
	Get a polynomial from this level suited for lifting. More...

virtual bool	hasPolynomialById (std::size_t level, std::size_t id) const =0

virtual const UPoly &	getPolynomialById (std::size_t level, std::size_t id) const =0
	Retrieves a polynomial from its id. More...

virtual void	exportAsDot (std::ostream &) const

virtual Origin	getOrigin (std::size_t level, std::size_t id) const

Protected Types
using	Constraints = CADConstraints< Settings::backtracking >

Protected Member Functions
	BaseProjection (const Constraints &c)

void	callRemoveCallback (std::size_t level, const SampleLiftedWith &slw) const

std::size_t	getID (std::size_t level)
	Returns a fresh polynomial id for the given level. More...

void	freeID (std::size_t level, std::size_t id)
	Frees a currently used polynomial id for the given level. More...

carl::Variable	var (std::size_t level) const
	Returns the variable that corresponds to the given level, that is the variable eliminated in this level. More...

bool	canBePurgedByBounds (const UPoly &p) const
	Checks whether a polynomial can safely be ignored due to the bounds. More...

bool	isPurged (std::size_t level, std::size_t id)

Protected Attributes
const Constraints &	mConstraints

std::vector< PolynomialLiftingQueue< BaseProjection > >	mLiftingQueues
	List of lifting queues that can be used for incremental projection. More...

ProjectionInformation	mInfo
	Additional info on projection, projection levels and projection polynomials. More...

ProjectionOperator	mOperator
	The projection operator. More...

std::function< void(std::size_t, const SampleLiftedWith &)>	mRemoveCallback
	Callback to be called when polynomials are removed. The arguments are the projection level and a bitset that indicate which polynomials were removed in this level. More...

Private Attributes
std::vector< carl::IDPool >	mIDPools
	Lift of id pools to generate fresh IDs for polynomials. More...

Detailed Description

template<typename Settings>
class smtrat::cad::BaseProjection< Settings >

Definition at line 20 of file BaseProjection.h.

Member Typedef Documentation

◆ Constraints

template<typename Settings >

using smtrat::cad::BaseProjection< Settings >::Constraints = CADConstraints<Settings::backtracking>

protected

Definition at line 22 of file BaseProjection.h.

Constructor & Destructor Documentation

◆ BaseProjection()

template<typename Settings >

smtrat::cad::BaseProjection< Settings >::BaseProjection ( const Constraints & c )

inlineprotected

Definition at line 38 of file BaseProjection.h.

Member Function Documentation

◆ addEqConstraint() [1/2]

template<typename Settings >

carl::Bitset smtrat::cad::BaseProjection< Settings >::addEqConstraint	(	const Poly &	p,
		std::size_t	cid,
		bool	isBound
	)

inline

Adds the given polynomial of an equational constraint to the projection. Converts to a UPoly and calls the appropriate overload.

Definition at line 117 of file BaseProjection.h.

Here is the call graph for this function:

◆ addEqConstraint() [2/2]

template<typename Settings >

virtual carl::Bitset smtrat::cad::BaseProjection< Settings >::addEqConstraint	(	const UPoly &	p,
		std::size_t	cid,
		bool	isBound
	)

inlinevirtual

Adds the given polynomial of an equational constraint to the projection.

Reimplemented in smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

Definition at line 121 of file BaseProjection.h.

Here is the call graph for this function:

◆ addPolynomial() [1/2]

template<typename Settings >

carl::Bitset smtrat::cad::BaseProjection< Settings >::addPolynomial	(	const Poly &	p,
		std::size_t	cid,
		bool	isBound
	)

inline

Adds the given polynomial to the projection. Converts to a UPoly and calls the appropriate overload.

Definition at line 111 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addPolynomial() [2/2]

template<typename Settings >

virtual carl::Bitset smtrat::cad::BaseProjection< Settings >::addPolynomial	(	const UPoly &	p,
		std::size_t	cid,
		bool	isBound
	)

pure virtual

Adds the given polynomial to the projection.

Implemented in smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >, and smtrat::cad::Projection< Incrementality::SIMPLE, BT, Settings >.

◆ callRemoveCallback()

template<typename Settings >

void smtrat::cad::BaseProjection< Settings >::callRemoveCallback	(	std::size_t	level,
		const SampleLiftedWith &	slw
	)		const

inlineprotected

Definition at line 40 of file BaseProjection.h.

Here is the caller graph for this function:

◆ canBePurgedByBounds()

template<typename Settings >

bool smtrat::cad::BaseProjection< Settings >::canBePurgedByBounds ( const UPoly & p ) const

inlineprotected

Checks whether a polynomial can safely be ignored due to the bounds.

Definition at line 59 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dim()

template<typename Settings >

std::size_t smtrat::cad::BaseProjection< Settings >::dim ( ) const

inline

Returns the dimension of the projection.

Definition at line 88 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ empty() [1/2]

template<typename Settings >

virtual bool smtrat::cad::BaseProjection< Settings >::empty ( )

inlinevirtual

Definition at line 140 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ empty() [2/2]

template<typename Settings >

virtual bool smtrat::cad::BaseProjection< Settings >::empty ( std::size_t level ) const

pure virtual

Implemented in smtrat::qe::cad::Projection< Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, and smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

◆ exportAsDot()

template<typename Settings >

virtual void smtrat::cad::BaseProjection< Settings >::exportAsDot ( std::ostream & ) const

inlinevirtual

Reimplemented in smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, and smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

Definition at line 168 of file BaseProjection.h.

◆ freeID()

template<typename Settings >

void smtrat::cad::BaseProjection< Settings >::freeID	(	std::size_t	level,
		std::size_t	id
	)

inlineprotected

Frees a currently used polynomial id for the given level.

Definition at line 49 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getID()

template<typename Settings >

std::size_t smtrat::cad::BaseProjection< Settings >::getID ( std::size_t level )

inlineprotected

Returns a fresh polynomial id for the given level.

Definition at line 44 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getOrigin()

template<typename Settings >

virtual Origin smtrat::cad::BaseProjection< Settings >::getOrigin	(	std::size_t	level,
		std::size_t	id
	)		const

inlinevirtual

Reimplemented in smtrat::cad::Projection< Incrementality::FULL, BT, Settings >.

Definition at line 169 of file BaseProjection.h.

Here is the call graph for this function:

◆ getPolyForLifting()

template<typename Settings >

OptionalID smtrat::cad::BaseProjection< Settings >::getPolyForLifting	(	std::size_t	level,
		SampleLiftedWith &	slw
	)

inline

Get a polynomial from this level suited for lifting.

Definition at line 148 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getPolynomialById()

template<typename Settings >

virtual const UPoly& smtrat::cad::BaseProjection< Settings >::getPolynomialById	(	std::size_t	level,
		std::size_t	id
	)		const

pure virtual

Retrieves a polynomial from its id.

Implemented in smtrat::qe::cad::Projection< Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, and smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

Here is the caller graph for this function:

◆ hasPolynomialById()

template<typename Settings >

virtual bool smtrat::cad::BaseProjection< Settings >::hasPolynomialById	(	std::size_t	level,
		std::size_t	id
	)		const

pure virtual

Implemented in smtrat::qe::cad::Projection< Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, and smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

Here is the caller graph for this function:

◆ isPurged()

template<typename Settings >

bool smtrat::cad::BaseProjection< Settings >::isPurged	(	std::size_t	level,
		std::size_t	id
	)

inlineprotected

Definition at line 76 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removePolynomial() [1/2]

template<typename Settings >

void smtrat::cad::BaseProjection< Settings >::removePolynomial	(	const Poly &	p,
		std::size_t	cid,
		bool	isBound
	)

inline

Removes the given polynomial from the projection. Converts to a UPoly and calls the appropriate overload.

Definition at line 125 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removePolynomial() [2/2]

template<typename Settings >

virtual void smtrat::cad::BaseProjection< Settings >::removePolynomial	(	const UPoly &	p,
		std::size_t	cid,
		bool	isBound
	)

pure virtual

Removes the given polynomial from the projection.

Implemented in smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >, smtrat::cad::Projection< Incrementality::SIMPLE, BT, Settings >, and smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >.

◆ reset()

template<typename Settings >

void smtrat::cad::BaseProjection< Settings >::reset ( )

inline

Resets all datastructures, use the given variables from now on.

Definition at line 98 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setRemoveCallback()

template<typename Settings >

template<typename F >

void smtrat::cad::BaseProjection< Settings >::setRemoveCallback ( F && f )

inline

Sets a callback that is called whenever polynomials are removed.

Definition at line 107 of file BaseProjection.h.

◆ size() [1/2]

template<typename Settings >

std::size_t smtrat::cad::BaseProjection< Settings >::size ( ) const

inline

Definition at line 132 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ size() [2/2]

template<typename Settings >

virtual std::size_t smtrat::cad::BaseProjection< Settings >::size ( std::size_t level ) const

pure virtual

Implemented in smtrat::qe::cad::Projection< Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::UNORDERED, Settings >, smtrat::cad::Projection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::ModelBasedProjection< Incrementality::NONE, Backtracking::ORDERED, Settings >, smtrat::cad::Projection< Incrementality::FULL, BT, Settings >, and smtrat::cad::Projection< Incrementality::FULL, Backtracking::HIDE, Settings >.

◆ var()

template<typename Settings >

carl::Variable smtrat::cad::BaseProjection< Settings >::var ( std::size_t level ) const

inlineprotected

Returns the variable that corresponds to the given level, that is the variable eliminated in this level.

Definition at line 54 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ vars()

template<typename Settings >

const auto& smtrat::cad::BaseProjection< Settings >::vars ( ) const

inline

Returns the variables used for projection.

Definition at line 94 of file BaseProjection.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

◆ mConstraints

template<typename Settings >

const Constraints& smtrat::cad::BaseProjection< Settings >::mConstraints

protected

Definition at line 28 of file BaseProjection.h.

◆ mIDPools

template<typename Settings >

std::vector<carl::IDPool> smtrat::cad::BaseProjection< Settings >::mIDPools

private

Lift of id pools to generate fresh IDs for polynomials.

Definition at line 25 of file BaseProjection.h.

◆ mInfo

template<typename Settings >

ProjectionInformation smtrat::cad::BaseProjection< Settings >::mInfo

protected

Additional info on projection, projection levels and projection polynomials.

Definition at line 32 of file BaseProjection.h.

◆ mLiftingQueues

template<typename Settings >

std::vector<PolynomialLiftingQueue<BaseProjection> > smtrat::cad::BaseProjection< Settings >::mLiftingQueues

protected

List of lifting queues that can be used for incremental projection.

Definition at line 30 of file BaseProjection.h.

◆ mOperator

template<typename Settings >

ProjectionOperator smtrat::cad::BaseProjection< Settings >::mOperator

protected

The projection operator.

Definition at line 34 of file BaseProjection.h.

◆ mRemoveCallback

template<typename Settings >

std::function<void(std::size_t, const SampleLiftedWith&)> smtrat::cad::BaseProjection< Settings >::mRemoveCallback

protected

Callback to be called when polynomials are removed. The arguments are the projection level and a bitset that indicate which polynomials were removed in this level.

Definition at line 36 of file BaseProjection.h.

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

smtrat-cad/projection/BaseProjection.h

Public Member Functions

Protected Types

Protected Member Functions

Protected Attributes

Private Attributes

Detailed Description

template<typename Settings> class smtrat::cad::BaseProjection< Settings >

Member Typedef Documentation

◆ Constraints

Constructor & Destructor Documentation

◆ BaseProjection()

Member Function Documentation

◆ addEqConstraint() [1/2]

◆ addEqConstraint() [2/2]

◆ addPolynomial() [1/2]

◆ addPolynomial() [2/2]

◆ callRemoveCallback()

◆ canBePurgedByBounds()

◆ dim()

◆ empty() [1/2]

◆ empty() [2/2]

◆ exportAsDot()

◆ freeID()

◆ getID()

◆ getOrigin()

◆ getPolyForLifting()

◆ getPolynomialById()

◆ hasPolynomialById()

◆ isPurged()

◆ removePolynomial() [1/2]

◆ removePolynomial() [2/2]

◆ reset()

◆ setRemoveCallback()

◆ size() [1/2]

◆ size() [2/2]

◆ var()

◆ vars()

Field Documentation

◆ mConstraints

◆ mIDPools

◆ mInfo

◆ mLiftingQueues

◆ mOperator

◆ mRemoveCallback

template<typename Settings>
class smtrat::cad::BaseProjection< Settings >