SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Namespaces | Functions
smtrat::covering_ng::formula::complexity Namespace Reference

Namespaces

 features
 

Functions

bool pickering_total (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 Inspired by Pickering, Lynn, Tereso Del Rio Almajano, Matthew England, and Kelly Cohen. More...
 
bool min_level_min_size (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool min_size (cadcells::datastructures::Projections &, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool sotd (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 Dolzmann et al 2004. More...
 
bool min_level_min_sotd (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool min_vars_min_sotd (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool sotd_reverse (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool min_max_tdeg_min_size (cadcells::datastructures::Projections &proj, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &a, const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &b)
 
bool min_sotd (cadcells::datastructures::Projections &proj, const cadcells::datastructures::PolyConstraint &a, const cadcells::datastructures::PolyConstraint &b)
 
bool min_tdeg (cadcells::datastructures::Projections &proj, const cadcells::datastructures::PolyConstraint &a, const cadcells::datastructures::PolyConstraint &b)
 

Function Documentation

◆ min_level_min_size()

bool smtrat::covering_ng::formula::complexity::min_level_min_size ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 126 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ min_level_min_sotd()

bool smtrat::covering_ng::formula::complexity::min_level_min_sotd ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 147 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ min_max_tdeg_min_size()

bool smtrat::covering_ng::formula::complexity::min_max_tdeg_min_size ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 169 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ min_size()

bool smtrat::covering_ng::formula::complexity::min_size ( cadcells::datastructures::Projections &  ,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 134 of file FormulaEvaluationComplexity.h.

Here is the caller graph for this function:

◆ min_sotd()

bool smtrat::covering_ng::formula::complexity::min_sotd ( cadcells::datastructures::Projections &  proj,
const cadcells::datastructures::PolyConstraint &  a,
const cadcells::datastructures::PolyConstraint &  b 
)
inline

Definition at line 175 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ min_tdeg()

bool smtrat::covering_ng::formula::complexity::min_tdeg ( cadcells::datastructures::Projections &  proj,
const cadcells::datastructures::PolyConstraint &  a,
const cadcells::datastructures::PolyConstraint &  b 
)
inline

Definition at line 179 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ min_vars_min_sotd()

bool smtrat::covering_ng::formula::complexity::min_vars_min_sotd ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 155 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ pickering_total()

bool smtrat::covering_ng::formula::complexity::pickering_total ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Inspired by 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 110 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ sotd()

bool smtrat::covering_ng::formula::complexity::sotd ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Dolzmann et al 2004.

Definition at line 141 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function:

◆ sotd_reverse()

bool smtrat::covering_ng::formula::complexity::sotd_reverse ( cadcells::datastructures::Projections &  proj,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  a,
const boost::container::flat_set< cadcells::datastructures::PolyConstraint > &  b 
)
inline

Definition at line 163 of file FormulaEvaluationComplexity.h.

Here is the call graph for this function:
Here is the caller graph for this function: