VariableOrdering.h File Reference

#include <carl-arith/core/Variable.h>
#include <carl-formula/formula/Formula.h>
#include <carl-formula/formula/functions/Variables.h>
#include <smtrat-common/types.h>
#include "types.h"
#include <smtrat-mcsat/variableordering/VariableOrdering.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::covering_ng
	smtrat::covering_ng::variables
	smtrat::covering_ng::variables::impl

Enumerations
enum	smtrat::covering_ng::variables::VariableOrderingHeuristics {   smtrat::covering_ng::variables::GreedyMaxUnivariate , smtrat::covering_ng::variables::FeatureBased , smtrat::covering_ng::variables::FeatureBasedZ3 , smtrat::covering_ng::variables::FeatureBasedBrown ,   smtrat::covering_ng::variables::FeatureBasedTriangular , smtrat::covering_ng::variables::FeatureBasedLexicographic , smtrat::covering_ng::variables::FeatureBasedPickering , smtrat::covering_ng::variables::EarliestSplitting }
	Possible heuristics for variable ordering. More...

Functions
std::string	smtrat::covering_ng::variables::get_name (VariableOrderingHeuristics ordering)
template<mcsat::VariableOrdering vo>
std::vector< carl::Variable >	smtrat::covering_ng::variables::impl::variable_ordering (const carl::QuantifierPrefix &quantifiers, const FormulaT &formula)
	Calculates a variable ordering based on the given quantifier blocks and the given formula. More...
std::vector< carl::Variable >	smtrat::covering_ng::variables::impl::sort_earliest_splitting (const carl::QuantifierPrefix &prefix, const FormulaT &base_formula)
	Calculates a variable ordering based on the given quantifier blocks and the given formula. More...
template<VariableOrderingHeuristics vo>
std::vector< carl::Variable >	smtrat::covering_ng::variables::get_variable_ordering (const carl::QuantifierPrefix &quantifiers, const FormulaT &formula)