SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Public Member Functions | Protected Types | Protected Member Functions | Protected Attributes | Private Attributes
smtrat::cad::ModelBasedProjection< incrementality, backtracking, Settings > Class Template Referenceabstract

#include <Projection.h>

Inheritance diagram for smtrat::cad::ModelBasedProjection< incrementality, backtracking, Settings >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::cad::ModelBasedProjection< incrementality, backtracking, Settings >:
Collaboration graph
[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

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<Incrementality incrementality, Backtracking backtracking, typename Settings>
class smtrat::cad::ModelBasedProjection< incrementality, backtracking, Settings >

Definition at line 22 of file Projection.h.

Member Typedef Documentation

◆ Constraints

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

Definition at line 22 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 
)
inlineinherited

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

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

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 virtualinherited

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
inlineprotectedinherited

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
inlineprotectedinherited

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
inlineinherited

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

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 virtualinherited

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
inlinevirtualinherited

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

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

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
inlinevirtualinherited

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

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 virtualinherited

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 virtualinherited

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

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

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 virtualinherited

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

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

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
inlineinherited

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 virtualinherited

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
inlineprotectedinherited

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
inlineinherited

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
protectedinherited

Definition at line 28 of file BaseProjection.h.

◆ mIDPools

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

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
protectedinherited

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
protectedinherited

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
protectedinherited

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
protectedinherited

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: