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

#include <CAD.h>

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

Public Types

using SettingsT = Settings
 

Public Member Functions

 CAD ()
 
 ~CAD ()
 
std::size_t dim () const
 
const auto & getVariables () const
 
const auto & getProjection () const
 
const auto & getLifting () const
 
const auto & getConstraints () const
 
const auto & getConstraintMap () const
 
bool isIdValid (std::size_t id) const
 
const auto & getBounds () const
 
void reset (const std::vector< carl::Variable > &vars)
 
void addConstraint (const ConstraintT &c)
 
void removeConstraint (const ConstraintT &c)
 
template<typename ConstraintIt >
bool evaluateSample (Sample &sample, const ConstraintIt &constraint, Assignment &assignment) const
 
std::vector< Assignment > enumerateSolutions ()
 
Answer checkFullSamples (Assignment &assignment)
 
template<typename Iterator >
Answer checkPartialSample (Iterator &it, std::size_t level)
 
Answer check (Assignment &assignment, std::vector< FormulaSetT > &mis)
 
ConflictGraph generateConflictGraph () const
 
auto generateCovering () const
 

Data Fields

debug::TikzHistoryPrinter thp
 

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
 
CADConstraints< Settings::backtracking > mConstraints
 
ProjectionT< Settings > mProjection
 
LiftingTree< Settings > mLifting
 

Friends

template<CoreHeuristic CH>
struct CADCore
 

Detailed Description

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

Definition at line 20 of file CAD.h.

Member Typedef Documentation

◆ SettingsT

template<typename Settings >
using smtrat::cad::CAD< Settings >::SettingsT = Settings

Definition at line 24 of file CAD.h.

Constructor & Destructor Documentation

◆ CAD()

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

Definition at line 44 of file CAD.h.

Here is the call graph for this function:

◆ ~CAD()

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

Definition at line 62 of file CAD.h.

Here is the call graph for this function:

Member Function Documentation

◆ addConstraint()

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

Definition at line 98 of file CAD.h.

Here is the call graph for this function:

◆ check()

template<typename Settings >
Answer smtrat::cad::CAD< Settings >::check ( Assignment &  assignment,
std::vector< FormulaSetT > &  mis 
)
inline

Definition at line 194 of file CAD.h.

Here is the call graph for this function:

◆ checkFullSamples()

template<typename Settings >
Answer smtrat::cad::CAD< Settings >::checkFullSamples ( Assignment &  assignment)
inline

Definition at line 150 of file CAD.h.

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

◆ checkPartialSample()

template<typename Settings >
template<typename Iterator >
Answer smtrat::cad::CAD< Settings >::checkPartialSample ( Iterator &  it,
std::size_t  level 
)
inline

Definition at line 176 of file CAD.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::CAD< Settings >::dim ( ) const
inline

Definition at line 68 of file CAD.h.

Here is the caller graph for this function:

◆ enumerateSolutions()

template<typename Settings >
std::vector<Assignment> smtrat::cad::CAD< Settings >::enumerateSolutions ( )
inline

Definition at line 128 of file CAD.h.

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

◆ evaluateSample()

template<typename Settings >
template<typename ConstraintIt >
bool smtrat::cad::CAD< Settings >::evaluateSample ( Sample &  sample,
const ConstraintIt &  constraint,
Assignment &  assignment 
) const
inline

Definition at line 113 of file CAD.h.

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

◆ generateConflictGraph()

template<typename Settings >
ConflictGraph smtrat::cad::CAD< Settings >::generateConflictGraph ( ) const
inline

Definition at line 212 of file CAD.h.

Here is the call graph for this function:

◆ generateCovering()

template<typename Settings >
auto smtrat::cad::CAD< Settings >::generateCovering ( ) const
inline

Definition at line 234 of file CAD.h.

Here is the caller graph for this function:

◆ getBounds()

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

Definition at line 89 of file CAD.h.

Here is the call graph for this function:

◆ getConstraintMap()

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

Definition at line 83 of file CAD.h.

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

◆ getConstraints()

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

Definition at line 80 of file CAD.h.

Here is the call graph for this function:

◆ getLifting()

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

Definition at line 77 of file CAD.h.

◆ getProjection()

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

Definition at line 74 of file CAD.h.

◆ getVariables()

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

Definition at line 71 of file CAD.h.

◆ idLP()

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

Definition at line 38 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::cad::CAD< Settings >::idPL ( std::size_t  level) const
inlineprivate

Definition at line 34 of file CAD.h.

Here is the call graph for this function:

◆ isIdValid()

template<typename Settings >
bool smtrat::cad::CAD< Settings >::isIdValid ( std::size_t  id) const
inline

Definition at line 86 of file CAD.h.

Here is the call graph for this function:

◆ removeConstraint()

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

Definition at line 104 of file CAD.h.

Here is the call graph for this function:

◆ reset()

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

Definition at line 92 of file CAD.h.

Here is the call graph for this function:

Friends And Related Function Documentation

◆ CADCore

template<typename Settings >
template<CoreHeuristic CH>
friend struct CADCore
friend

Definition at line 23 of file CAD.h.

Field Documentation

◆ mConstraints

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

Definition at line 27 of file CAD.h.

◆ mLifting

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

Definition at line 29 of file CAD.h.

◆ mProjection

template<typename Settings >
ProjectionT<Settings> smtrat::cad::CAD< Settings >::mProjection
private

Definition at line 28 of file CAD.h.

◆ mVariables

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

Definition at line 26 of file CAD.h.

◆ thp

template<typename Settings >
debug::TikzHistoryPrinter smtrat::cad::CAD< Settings >::thp

Definition at line 43 of file CAD.h.

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