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

#include <LevelWiseInformation.h>

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

Public Member Functions

 LevelWiseInformation ()
 
 LevelWiseInformation (LevelWiseInformation &&other)
 
void addDerivation (const datastructures::SampledDerivationRef< PropSet > &derivation)
 
void addDerivation (datastructures::SampledDerivationRef< PropSet > &&derivation)
 
const std::set< datastructures::SampledDerivationRef< PropSet >, SampledDerivationRefCompare > & getDerivations () const
 
void clear ()
 
bool computeCovering ()
 
const cadcells::RAN & getSampleOutside () const
 
bool isPartialCovering () const
 
bool isFullCovering () const
 
bool isUnknownCovering () const
 
bool isFailedCovering () const
 
CoveringStatus getCoveringStatus () const
 
LevelWiseInformation & operator= (LevelWiseInformation &&other)
 
void setDerivations (std::vector< datastructures::SampledDerivationRef< PropSet >> &&derivations)
 
void removeDerivation (const datastructures::SampledDerivationRef< PropSet > &derivation)
 
void removeDerivation (const std::vector< datastructures::SampledDerivationRef< PropSet >> &derivations)
 
void removeConstraint (const cadcells::Constraint &constraint, const std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &derivationConstraints)
 
std::vector< cadcells::Constraint > getConstraintsOfCovering (std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &mDerivationToConstraint)
 
std::optional< datastructures::SampledDerivationRef< PropSet > > constructDerivation (std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &mDerivationToConstraint)
 

Private Types

using op = typename Settings::op
 
using PropSet = typename op::PropertiesSet
 

Private Attributes

std::set< datastructures::SampledDerivationRef< PropSet >, SampledDerivationRefCompare > mDerivations
 
CoveringStatus mCoveringStatus
 
std::optional< datastructures::CoveringRepresentation< PropSet > > mCovering
 
cadcells::RAN mSamplePoint
 

Static Private Attributes

static constexpr cadcells::representation::CoveringHeuristic covering_heuristic = Settings::covering_heuristic
 
static constexpr SamplingAlgorithm sampling_algorithm = Settings::sampling_algorithm
 
static constexpr IsSampleOutsideAlgorithm is_sample_outside_algorithm = Settings::is_sample_outside_algorithm
 

Detailed Description

template<class Settings>
class smtrat::LevelWiseInformation< Settings >

Definition at line 40 of file LevelWiseInformation.h.

Member Typedef Documentation

◆ op

template<class Settings >
using smtrat::LevelWiseInformation< Settings >::op = typename Settings::op
private

Definition at line 44 of file LevelWiseInformation.h.

◆ PropSet

template<class Settings >
using smtrat::LevelWiseInformation< Settings >::PropSet = typename op::PropertiesSet
private

Definition at line 47 of file LevelWiseInformation.h.

Constructor & Destructor Documentation

◆ LevelWiseInformation() [1/2]

template<class Settings >
smtrat::LevelWiseInformation< Settings >::LevelWiseInformation ( )
inline

Definition at line 65 of file LevelWiseInformation.h.

◆ LevelWiseInformation() [2/2]

template<class Settings >
smtrat::LevelWiseInformation< Settings >::LevelWiseInformation ( LevelWiseInformation< Settings > &&  other)
inline

Definition at line 69 of file LevelWiseInformation.h.

Member Function Documentation

◆ addDerivation() [1/2]

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::addDerivation ( const datastructures::SampledDerivationRef< PropSet > &  derivation)
inline

Definition at line 76 of file LevelWiseInformation.h.

◆ addDerivation() [2/2]

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::addDerivation ( datastructures::SampledDerivationRef< PropSet > &&  derivation)
inline

Definition at line 81 of file LevelWiseInformation.h.

◆ clear()

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::clear ( )
inline

Definition at line 90 of file LevelWiseInformation.h.

◆ computeCovering()

template<class Settings >
bool smtrat::LevelWiseInformation< Settings >::computeCovering ( )
inline

Definition at line 101 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ constructDerivation()

template<class Settings >
std::optional<datastructures::SampledDerivationRef<PropSet> > smtrat::LevelWiseInformation< Settings >::constructDerivation ( std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &  mDerivationToConstraint)
inline

Definition at line 279 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ getConstraintsOfCovering()

template<class Settings >
std::vector<cadcells::Constraint> smtrat::LevelWiseInformation< Settings >::getConstraintsOfCovering ( std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &  mDerivationToConstraint)
inline

Definition at line 254 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ getCoveringStatus()

template<class Settings >
CoveringStatus smtrat::LevelWiseInformation< Settings >::getCoveringStatus ( ) const
inline

Definition at line 167 of file LevelWiseInformation.h.

Here is the caller graph for this function:

◆ getDerivations()

template<class Settings >
const std::set<datastructures::SampledDerivationRef<PropSet>, SampledDerivationRefCompare>& smtrat::LevelWiseInformation< Settings >::getDerivations ( ) const
inline

Definition at line 85 of file LevelWiseInformation.h.

Here is the caller graph for this function:

◆ getSampleOutside()

template<class Settings >
const cadcells::RAN& smtrat::LevelWiseInformation< Settings >::getSampleOutside ( ) const
inline

Definition at line 145 of file LevelWiseInformation.h.

Here is the caller graph for this function:

◆ isFailedCovering()

template<class Settings >
bool smtrat::LevelWiseInformation< Settings >::isFailedCovering ( ) const
inline

Definition at line 163 of file LevelWiseInformation.h.

◆ isFullCovering()

template<class Settings >
bool smtrat::LevelWiseInformation< Settings >::isFullCovering ( ) const
inline

Definition at line 155 of file LevelWiseInformation.h.

Here is the caller graph for this function:

◆ isPartialCovering()

template<class Settings >
bool smtrat::LevelWiseInformation< Settings >::isPartialCovering ( ) const
inline

Definition at line 151 of file LevelWiseInformation.h.

Here is the caller graph for this function:

◆ isUnknownCovering()

template<class Settings >
bool smtrat::LevelWiseInformation< Settings >::isUnknownCovering ( ) const
inline

Definition at line 159 of file LevelWiseInformation.h.

◆ operator=()

template<class Settings >
LevelWiseInformation& smtrat::LevelWiseInformation< Settings >::operator= ( LevelWiseInformation< Settings > &&  other)
inline

Definition at line 172 of file LevelWiseInformation.h.

◆ removeConstraint()

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::removeConstraint ( const cadcells::Constraint &  constraint,
const std::map< datastructures::SampledDerivationRef< PropSet >, std::vector< cadcells::Constraint >> &  derivationConstraints 
)
inline

Definition at line 222 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ removeDerivation() [1/2]

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::removeDerivation ( const datastructures::SampledDerivationRef< PropSet > &  derivation)
inline

Definition at line 193 of file LevelWiseInformation.h.

Here is the call graph for this function:

◆ removeDerivation() [2/2]

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::removeDerivation ( const std::vector< datastructures::SampledDerivationRef< PropSet >> &  derivations)
inline

Definition at line 213 of file LevelWiseInformation.h.

◆ setDerivations()

template<class Settings >
void smtrat::LevelWiseInformation< Settings >::setDerivations ( std::vector< datastructures::SampledDerivationRef< PropSet >> &&  derivations)
inline

Definition at line 181 of file LevelWiseInformation.h.

Field Documentation

◆ covering_heuristic

template<class Settings >
constexpr cadcells::representation::CoveringHeuristic smtrat::LevelWiseInformation< Settings >::covering_heuristic = Settings::covering_heuristic
staticconstexprprivate

Definition at line 43 of file LevelWiseInformation.h.

◆ is_sample_outside_algorithm

template<class Settings >
constexpr IsSampleOutsideAlgorithm smtrat::LevelWiseInformation< Settings >::is_sample_outside_algorithm = Settings::is_sample_outside_algorithm
staticconstexprprivate

Definition at line 46 of file LevelWiseInformation.h.

◆ mCovering

template<class Settings >
std::optional<datastructures::CoveringRepresentation<PropSet> > smtrat::LevelWiseInformation< Settings >::mCovering
private

Definition at line 58 of file LevelWiseInformation.h.

◆ mCoveringStatus

template<class Settings >
CoveringStatus smtrat::LevelWiseInformation< Settings >::mCoveringStatus
private

Definition at line 55 of file LevelWiseInformation.h.

◆ mDerivations

template<class Settings >
std::set<datastructures::SampledDerivationRef<PropSet>, SampledDerivationRefCompare> smtrat::LevelWiseInformation< Settings >::mDerivations
private

Definition at line 52 of file LevelWiseInformation.h.

◆ mSamplePoint

template<class Settings >
cadcells::RAN smtrat::LevelWiseInformation< Settings >::mSamplePoint
private

Definition at line 61 of file LevelWiseInformation.h.

◆ sampling_algorithm

template<class Settings >
constexpr SamplingAlgorithm smtrat::LevelWiseInformation< Settings >::sampling_algorithm = Settings::sampling_algorithm
staticconstexprprivate

Definition at line 45 of file LevelWiseInformation.h.

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