smtrat::mcsat::variableordering::detail Namespace Reference

Data Structures
struct	FeatureCollector
	This class manages features that are used to valuate variables on objects. More...

Functions
template<typename Constraints , typename Calculator >
double	abstract_feature (const Constraints &constraints, double initial, std::function< double(double, double)> &&comb, Calculator &&calc)
template<typename Constraints >
double	max_degree (const Constraints &constraints, carl::Variable v)
	The maximum degree of this variable. More...
template<typename Constraints >
double	max_term_total_degree (const Constraints &constraints, carl::Variable v)
	The maximum total degree of a term involving this variable. More...
template<typename Constraints >
double	max_coefficient (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	num_occurrences (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	max_lcoeff_total_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	sum_max_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	sum_sum_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	avg_avg_degree (const Constraints &constraints, carl::Variable v)
carl::Bitset	variablesOf (const ConstraintT &c, VariableIDs &vids)
long	countUnivariates (const std::vector< carl::Bitset > &constraints, std::size_t id)
bool	stillOccurs (const std::vector< carl::Bitset > &constraints, std::size_t id)
carl::Variable	findMax (const std::vector< carl::Bitset > &constraints, const VariableIDs &vids)
void	purgeVariable (std::vector< carl::Bitset > &constraints, carl::Variable v, const VariableIDs &vids)

Function Documentation

abstract_feature()

template<typename Constraints , typename Calculator >

double smtrat::mcsat::variableordering::detail::abstract_feature	(	const Constraints &	constraints,
		double	initial,
		std::function< double(double, double)> &&	comb,
		Calculator &&	calc
	)

Definition at line 59 of file feature_based.h.

Here is the caller graph for this function:

avg_avg_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::avg_avg_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 158 of file feature_based.h.

Here is the call graph for this function:

countUnivariates()

long smtrat::mcsat::variableordering::detail::countUnivariates ( const std::vector< carl::Bitset > &  constraints, std::size_t  id  )

inline

Definition at line 26 of file greedy_max_univariate.h.

Here is the caller graph for this function:

findMax()

carl::Variable smtrat::mcsat::variableordering::detail::findMax ( const std::vector< carl::Bitset > &  constraints, const VariableIDs &  vids  )

inline

Definition at line 32 of file greedy_max_univariate.h.

Here is the call graph for this function:

Here is the caller graph for this function:

max_coefficient()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::max_coefficient	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 92 of file feature_based.h.

Here is the call graph for this function:

max_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::max_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

The maximum degree of this variable.

Definition at line 67 of file feature_based.h.

Here is the call graph for this function:

max_lcoeff_total_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::max_lcoeff_total_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 122 of file feature_based.h.

Here is the call graph for this function:

max_term_total_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::max_term_total_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

The maximum total degree of a term involving this variable.

Definition at line 77 of file feature_based.h.

Here is the call graph for this function:

num_occurrences()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::num_occurrences	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 107 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

purgeVariable()

void smtrat::mcsat::variableordering::detail::purgeVariable ( std::vector< carl::Bitset > &  constraints, carl::Variable  v, const VariableIDs &  vids  )

inline

Definition at line 52 of file greedy_max_univariate.h.

Here is the caller graph for this function:

stillOccurs()

bool smtrat::mcsat::variableordering::detail::stillOccurs ( const std::vector< carl::Bitset > &  constraints, std::size_t  id  )

inline

Definition at line 29 of file greedy_max_univariate.h.

Here is the caller graph for this function:

sum_max_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::sum_max_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 134 of file feature_based.h.

Here is the call graph for this function:

sum_sum_degree()

template<typename Constraints >

double smtrat::mcsat::variableordering::detail::sum_sum_degree	(	const Constraints &	constraints,
		carl::Variable	v
	)

Definition at line 142 of file feature_based.h.

Here is the call graph for this function:

variablesOf()

carl::Bitset smtrat::mcsat::variableordering::detail::variablesOf ( const ConstraintT &  c, VariableIDs &  vids  )

inline

Definition at line 18 of file greedy_max_univariate.h.

Here is the caller graph for this function: