smtrat::mcsat::variableordering Namespace Reference

Namespaces
	detail

Data Structures
struct	VariableIDs

Functions
template<typename Constraints >
std::vector< carl::Variable >	feature_based (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	feature_based_z3 (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	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 >	feature_based_triangular (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	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 >	feature_based_lexicographic (const Constraints &c)
template<typename Constraints >
std::vector< carl::Variable >	greedy_max_univariate (const Constraints &c)
std::ostream &	operator<< (std::ostream &os, const VariableIDs &vids)
template<typename Constraints >
void	gatherVariables (carl::carlVariables &vars, const Constraints &constraints)

Function Documentation

feature_based()

template<typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::variableordering::feature_based

(

const Constraints &

c

)

Definition at line 179 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

feature_based_brown()

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.

Definition at line 215 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

feature_based_lexicographic()

template<typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::variableordering::feature_based_lexicographic

(

const Constraints &

c

)

Definition at line 269 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

feature_based_pickering()

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.

‘Explainable AI Insights for Symbolic Computation: A Case Study on Selecting the Variable Ordering for Cylindrical Algebraic Decomposition’. arXiv, 29 August 2023. http://arxiv.org/abs/2304.12154.

Definition at line 253 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

feature_based_triangular()

template<typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::variableordering::feature_based_triangular

(

const Constraints &

c

)

Definition at line 232 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

feature_based_z3()

template<typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::variableordering::feature_based_z3

(

const Constraints &

c

)

Definition at line 196 of file feature_based.h.

Here is the call graph for this function:

Here is the caller graph for this function:

gatherVariables()

template<typename Constraints >

void smtrat::mcsat::variableordering::gatherVariables	(	carl::carlVariables &	vars,
		const Constraints &	constraints
	)

Definition at line 37 of file helper.h.

Here is the call graph for this function:

Here is the caller graph for this function:

greedy_max_univariate()

template<typename Constraints >

std::vector<carl::Variable> smtrat::mcsat::variableordering::greedy_max_univariate

(

const Constraints &

c

)

Definition at line 68 of file greedy_max_univariate.h.

Here is the call graph for this function:

Here is the caller graph for this function:

operator<<()

std::ostream& smtrat::mcsat::variableordering::operator<< ( std::ostream &  os, const VariableIDs &  vids  )

inline

Definition at line 27 of file helper.h.

Here is the call graph for this function: