smtrat::mcsat::variableordering::detail::FeatureCollector< Objects > Struct Template Reference

This class manages features that are used to valuate variables on objects. More...

#include <feature_based.h>

Collaboration diagram for smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >:

Public Types
using	Extractor = std::function< double(Objects, carl::Variable)>
using	Valuation = std::vector< double >

Public Member Functions
void	addFeature (Extractor &&e, std::size_t level, double weight)
Valuation	valuateVariable (const Objects &o, carl::Variable v) const
std::vector< carl::Variable >	sortVariables (const Objects &o, std::vector< carl::Variable > vars) const

Data Fields
std::vector< std::tuple< Extractor, std::size_t, double > >	mFeatures

Detailed Description

template<typename Objects>
struct smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >

This class manages features that are used to valuate variables on objects.

Each feature consists of a valuation function, a level and a weight. All feature valuations of a certain level are combined linearly using the respective weights. Valuations are then compared lexicographically.

Definition at line 26 of file feature_based.h.

Member Typedef Documentation

Extractor

template<typename Objects >

using smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::Extractor = std::function<double(Objects, carl::Variable)>

Definition at line 27 of file feature_based.h.

Valuation

template<typename Objects >

using smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::Valuation = std::vector<double>

Definition at line 28 of file feature_based.h.

Member Function Documentation

addFeature()

template<typename Objects >

void smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::addFeature ( Extractor &&  e, std::size_t  level, double  weight  )

inline

Definition at line 31 of file feature_based.h.

Here is the caller graph for this function:

sortVariables()

template<typename Objects >

std::vector<carl::Variable> smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::sortVariables ( const Objects &  o, std::vector< carl::Variable >  vars  ) const

inline

Definition at line 46 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

valuateVariable()

template<typename Objects >

Valuation smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::valuateVariable ( const Objects &  o, carl::Variable  v  ) const

inline

Definition at line 35 of file feature_based.h.

Here is the caller graph for this function:

Field Documentation

mFeatures

template<typename Objects >

std::vector<std::tuple<Extractor, std::size_t, double> > smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >::mFeatures

Definition at line 29 of file feature_based.h.

---

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

• smtrat-mcsat/variableordering/feature_based.h