VariableOrdering.h File Reference

#include "feature_based.h"
#include "greedy_max_univariate.h"

Include dependency graph for VariableOrdering.h:

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

Go to the source code of this file.

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

Enumerations
enum class	smtrat::mcsat::VariableOrdering {   smtrat::mcsat::GreedyMaxUnivariate , smtrat::mcsat::FeatureBased , smtrat::mcsat::FeatureBasedZ3 , smtrat::mcsat::FeatureBasedBrown ,   smtrat::mcsat::FeatureBasedTriangular , smtrat::mcsat::FeatureBasedLexicographic , smtrat::mcsat::FeatureBasedPickering }

Functions
std::string	smtrat::mcsat::get_name (VariableOrdering ordering)
std::ostream &	smtrat::mcsat::operator<< (std::ostream &os, VariableOrdering ordering)
template<VariableOrdering vot, typename Constraints >
std::vector< carl::Variable >	smtrat::mcsat::calculate_variable_order (const Constraints &c)
template<VariableOrdering vot>
std::vector< carl::Variable >	smtrat::mcsat::calculate_variable_order (const std::vector< ConstraintT > &constraints)