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

#include <CAD.h>

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

Public Types

using TreeIterator = typename smtrat::cad::LiftingTree< Settings >::Iterator
 

Public Member Functions

 CAD ()
 
void reset (const std::vector< carl::Variable > &vars)
 
std::size_t dim () const
 
const auto & getProjection () const
 
const auto & getLifting () const
 
void addConstraint (const ConstraintT &c)
 
void removeConstraint (const ConstraintT &c)
 
void addPolynomial (const Poly &p)
 
void removePolynomial (std::size_t level, std::size_t id)
 
void project ()
 
void lift ()
 

Private Member Functions

std::size_t idPL (std::size_t level) const
 
std::size_t idLP (std::size_t level) const
 

Private Attributes

std::vector< carl::Variable > mVariables
 
smtrat::cad::CADConstraints< Settings::backtracking > mConstraints
 
std::vector< Poly > polynomials
 
Projection< Settings > mProjection
 
smtrat::cad::LiftingTree< Settings > mLifting
 

Detailed Description

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

Definition at line 12 of file CAD.h.

Member Typedef Documentation

◆ TreeIterator

template<typename Settings >
using smtrat::qe::cad::CAD< Settings >::TreeIterator = typename smtrat::cad::LiftingTree<Settings>::Iterator

Definition at line 14 of file CAD.h.

Constructor & Destructor Documentation

◆ CAD()

template<typename Settings >
smtrat::qe::cad::CAD< Settings >::CAD ( )
inline

Definition at line 31 of file CAD.h.

Here is the call graph for this function:

Member Function Documentation

◆ addConstraint()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::addConstraint ( const ConstraintT &  c)
inline

Definition at line 62 of file CAD.h.

Here is the call graph for this function:

◆ addPolynomial()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::addPolynomial ( const Poly &  p)
inline

Definition at line 76 of file CAD.h.

◆ dim()

template<typename Settings >
std::size_t smtrat::qe::cad::CAD< Settings >::dim ( ) const
inline

Definition at line 52 of file CAD.h.

Here is the caller graph for this function:

◆ getLifting()

template<typename Settings >
const auto& smtrat::qe::cad::CAD< Settings >::getLifting ( ) const
inline

Definition at line 58 of file CAD.h.

◆ getProjection()

template<typename Settings >
const auto& smtrat::qe::cad::CAD< Settings >::getProjection ( ) const
inline

Definition at line 55 of file CAD.h.

◆ idLP()

template<typename Settings >
std::size_t smtrat::qe::cad::CAD< Settings >::idLP ( std::size_t  level) const
inlineprivate

Definition at line 26 of file CAD.h.

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

◆ idPL()

template<typename Settings >
std::size_t smtrat::qe::cad::CAD< Settings >::idPL ( std::size_t  level) const
inlineprivate

Definition at line 22 of file CAD.h.

Here is the call graph for this function:

◆ lift()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::lift ( )
inline

Definition at line 89 of file CAD.h.

Here is the call graph for this function:

◆ project()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::project ( )
inline

Definition at line 83 of file CAD.h.

Here is the call graph for this function:

◆ removeConstraint()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::removeConstraint ( const ConstraintT &  c)
inline

Definition at line 68 of file CAD.h.

Here is the call graph for this function:

◆ removePolynomial()

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

Definition at line 79 of file CAD.h.

◆ reset()

template<typename Settings >
void smtrat::qe::cad::CAD< Settings >::reset ( const std::vector< carl::Variable > &  vars)
inline

Definition at line 45 of file CAD.h.

Here is the call graph for this function:

Field Documentation

◆ mConstraints

template<typename Settings >
smtrat::cad::CADConstraints<Settings::backtracking> smtrat::qe::cad::CAD< Settings >::mConstraints
private

Definition at line 17 of file CAD.h.

◆ mLifting

template<typename Settings >
smtrat::cad::LiftingTree<Settings> smtrat::qe::cad::CAD< Settings >::mLifting
private

Definition at line 20 of file CAD.h.

◆ mProjection

template<typename Settings >
Projection<Settings> smtrat::qe::cad::CAD< Settings >::mProjection
private

Definition at line 19 of file CAD.h.

◆ mVariables

template<typename Settings >
std::vector<carl::Variable> smtrat::qe::cad::CAD< Settings >::mVariables
private

Definition at line 16 of file CAD.h.

◆ polynomials

template<typename Settings >
std::vector<Poly> smtrat::qe::cad::CAD< Settings >::polynomials
private

Definition at line 18 of file CAD.h.

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