feature_based.h File Reference

#include "helper.h"
#include <algorithm>
#include <carl-arith/core/Variable.h>
#include <smtrat-common/smtrat-common.h>
#include <numeric>

Include dependency graph for feature_based.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	smtrat::mcsat::variableordering::detail::FeatureCollector< Objects >
	This class manages features that are used to valuate variables on objects. More...

Namespaces
	smtrat
	Class to create the formulas for axioms.
	smtrat::mcsat
	smtrat::mcsat::variableordering
	smtrat::mcsat::variableordering::detail

Functions
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)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::max_degree (const Constraints &constraints, carl::Variable v)
	The maximum degree of this variable. More...
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. More...
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::max_coefficient (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::num_occurrences (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::max_lcoeff_total_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::sum_max_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::sum_sum_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
double	smtrat::mcsat::variableordering::detail::avg_avg_degree (const Constraints &constraints, carl::Variable v)
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based_z3 (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based_brown (const Constraints &c)
	According to https://www.usna.edu/Users/cs/wcbrown/research/ISSAC04/handout.pdf. More...
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based_triangular (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based_pickering (const Constraints &c)
	According to Pickering, Lynn, Tereso Del Rio Almajano, Matthew England, and Kelly Cohen. More...
template<typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::variableordering::feature_based_lexicographic (const Constraints &c)