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

#include <Projection.h>

Inheritance diagram for smtrat::qe::cad::Projection< Settings >:
Inheritance graph
[legend]
Collaboration diagram for smtrat::qe::cad::Projection< Settings >:
Collaboration graph
[legend]

Public Member Functions

 Projection (const Constraints &c)
 
void reset ()
 
carl::Bitset addPolynomial (const UPoly &p, std::size_t cid, bool) override
 
void removePolynomial (const UPoly &, std::size_t cid, bool) override
 
bool testProjectionFactor (std::size_t level, std::size_t id) const
 
void removeProjectionFactor (std::size_t level, std::size_t id)
 
std::size_t size (std::size_t level) const override
 
bool empty (std::size_t level) const override
 
bool hasPolynomialById (std::size_t level, std::size_t id) const override
 
const UPoly & getPolynomialById (std::size_t level, std::size_t id) const override
 Retrieves a polynomial from its id. More...
 
std::size_t dim () const
 Returns the dimension of the projection. More...
 
virtual std::size_t size (std::size_t level) const=0
 
std::size_t size () const
 
std::size_t dim () const
 Returns the dimension of the projection. More...
 
const auto & vars () const
 Returns the variables used for projection. 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...
 
std::size_t size () const
 
virtual bool empty ()
 
OptionalID getPolyForLifting (std::size_t level, SampleLiftedWith &slw)
 Get a polynomial from this level suited for lifting. More...
 
virtual void exportAsDot (std::ostream &) const
 
virtual Origin getOrigin (std::size_t level, std::size_t id) const
 

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
 
ProjectionInformation mInfo
 Additional info on projection, projection levels and projection polynomials. 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 Types

using Super = BaseProjection< Settings >
 
using Constraints = CADConstraints< Settings::backtracking >
 

Private Member Functions

auto & polyIDs (std::size_t level)
 
const auto & polyIDs (std::size_t level) const
 
auto & polys (std::size_t level)
 
const auto & polys (std::size_t level) const
 
carl::Bitset addToProjection (std::size_t level, const UPoly &p, const Origin::BaseType &origin)
 
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...
 

Private Attributes

std::vector< std::map< UPoly, std::size_t > > mPolynomialIDs
 
std::vector< std::vector< std::optional< std::pair< UPoly, Origin > > > > mPolynomials
 
std::vector< PolynomialLiftingQueue< BaseProjection > > mLiftingQueues
 List of lifting queues that can be used for incremental projection. More...
 
ProjectionOperator mOperator
 The projection operator. More...
 
std::vector< carl::IDPool > mIDPools
 Lift of id pools to generate fresh IDs for polynomials. More...
 

Friends

template<typename S >
std::ostream & operator<< (std::ostream &os, const Projection< S > &p)
 

Detailed Description

template<typename Settings>
class smtrat::qe::cad::Projection< Settings >

Definition at line 19 of file Projection.h.

Member Typedef Documentation

◆ Constraints

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

Definition at line 22 of file BaseProjection.h.

◆ Super

template<typename Settings >
using smtrat::qe::cad::Projection< Settings >::Super = BaseProjection<Settings>
private

Definition at line 21 of file Projection.h.

Constructor & Destructor Documentation

◆ Projection()

template<typename Settings >
smtrat::qe::cad::Projection< Settings >::Projection ( const Constraints &  c)
inline

Definition at line 93 of file Projection.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/3]

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/3]

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 >.

◆ addPolynomial() [3/3]

template<typename Settings >
carl::Bitset smtrat::qe::cad::Projection< Settings >::addPolynomial ( const UPoly &  p,
std::size_t  cid,
bool   
)
inlineoverride

Definition at line 103 of file Projection.h.

Here is the call graph for this function:

◆ addToProjection()

template<typename Settings >
carl::Bitset smtrat::qe::cad::Projection< Settings >::addToProjection ( std::size_t  level,
const UPoly &  p,
const Origin::BaseType &  origin 
)
inlineprivate

Definition at line 57 of file Projection.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ callRemoveCallback() [1/2]

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:

◆ callRemoveCallback() [2/2]

template<typename Settings >
void smtrat::cad::BaseProjection< Settings >::callRemoveCallback
inlineprivate

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() [1/2]

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:

◆ dim() [2/2]

template<typename Settings >
std::size_t smtrat::cad::BaseProjection< Settings >::dim
inline

Returns the dimension of the projection.

Definition at line 88 of file BaseProjection.h.

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 >
bool smtrat::qe::cad::Projection< Settings >::empty ( std::size_t  level) const
inlineoverridevirtual

Implements smtrat::cad::BaseProjection< Settings >.

Definition at line 161 of file Projection.h.

Here is the call graph for this function:

◆ 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() [1/2]

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:

◆ freeID() [2/2]

template<typename Settings >
void smtrat::cad::BaseProjection< Settings >::freeID
inlineprivate

Frees a currently used polynomial id for the given level.

Definition at line 49 of file BaseProjection.h.

Here is the caller graph for this function:

◆ getID() [1/2]

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:

◆ getID() [2/2]

template<typename Settings >
std::size_t smtrat::cad::BaseProjection< Settings >::getID
inlineprivate

Returns a fresh polynomial id for the given level.

Definition at line 44 of file BaseProjection.h.

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 >
const UPoly& smtrat::qe::cad::Projection< Settings >::getPolynomialById ( std::size_t  level,
std::size_t  id 
) const
inlineoverridevirtual

Retrieves a polynomial from its id.

Implements smtrat::cad::BaseProjection< Settings >.

Definition at line 170 of file Projection.h.

Here is the call graph for this function:

◆ hasPolynomialById()

template<typename Settings >
bool smtrat::qe::cad::Projection< Settings >::hasPolynomialById ( std::size_t  level,
std::size_t  id 
) const
inlineoverridevirtual

Implements smtrat::cad::BaseProjection< Settings >.

Definition at line 165 of file Projection.h.

Here is the call graph for this function:
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:

◆ polyIDs() [1/2]

template<typename Settings >
auto& smtrat::qe::cad::Projection< Settings >::polyIDs ( std::size_t  level)
inlineprivate

Definition at line 40 of file Projection.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ polyIDs() [2/2]

template<typename Settings >
const auto& smtrat::qe::cad::Projection< Settings >::polyIDs ( std::size_t  level) const
inlineprivate

Definition at line 44 of file Projection.h.

Here is the call graph for this function:

◆ polys() [1/2]

template<typename Settings >
auto& smtrat::qe::cad::Projection< Settings >::polys ( std::size_t  level)
inlineprivate

Definition at line 48 of file Projection.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ polys() [2/2]

template<typename Settings >
const auto& smtrat::qe::cad::Projection< Settings >::polys ( std::size_t  level) const
inlineprivate

Definition at line 52 of file Projection.h.

Here is the call graph for this function:

◆ removePolynomial() [1/3]

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/3]

template<typename Settings >
void smtrat::qe::cad::Projection< Settings >::removePolynomial ( const UPoly &  ,
std::size_t  cid,
bool   
)
inlineoverride

Definition at line 107 of file Projection.h.

Here is the call graph for this function:

◆ removePolynomial() [3/3]

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 >.

◆ removeProjectionFactor()

template<typename Settings >
void smtrat::qe::cad::Projection< Settings >::removeProjectionFactor ( std::size_t  level,
std::size_t  id 
)
inline

Definition at line 145 of file Projection.h.

Here is the call graph for this function:

◆ reset()

template<typename Settings >
void smtrat::qe::cad::Projection< Settings >::reset ( )
inline

Definition at line 95 of file Projection.h.

Here is the call 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/4]

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/4]

template<typename Settings >
std::size_t smtrat::cad::BaseProjection< Settings >::size ( void  )
inline

Definition at line 132 of file BaseProjection.h.

◆ size() [3/4]

template<typename Settings >
std::size_t smtrat::qe::cad::Projection< Settings >::size ( std::size_t  level) const
inlineoverridevirtual

Implements smtrat::cad::BaseProjection< Settings >.

Definition at line 158 of file Projection.h.

Here is the call graph for this function:

◆ size() [4/4]

template<typename Settings >
virtual std::size_t smtrat::cad::BaseProjection< Settings >::size ( void  )
Here is the caller graph for this function:

◆ testProjectionFactor()

template<typename Settings >
bool smtrat::qe::cad::Projection< Settings >::testProjectionFactor ( std::size_t  level,
std::size_t  id 
) const
inline

Definition at line 137 of file Projection.h.

Here is the call graph for this function:

◆ var() [1/2]

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:

◆ var() [2/2]

template<typename Settings >
carl::Variable smtrat::cad::BaseProjection< Settings >::var
inlineprivate

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 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:

Friends And Related Function Documentation

◆ operator<<

template<typename Settings >
template<typename S >
std::ostream& operator<< ( std::ostream &  os,
const Projection< S > &  p 
)
friend

Definition at line 179 of file Projection.h.

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
private

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
private

The projection operator.

Definition at line 34 of file BaseProjection.h.

◆ mPolynomialIDs

template<typename Settings >
std::vector<std::map<UPoly,std::size_t> > smtrat::qe::cad::Projection< Settings >::mPolynomialIDs
private

Definition at line 37 of file Projection.h.

◆ mPolynomials

template<typename Settings >
std::vector<std::vector<std::optional<std::pair<UPoly,Origin> > > > smtrat::qe::cad::Projection< Settings >::mPolynomials
private

Definition at line 38 of file Projection.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: