SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Go to the source code of this file.
Namespaces | |
smtrat | |
Class to create the formulas for axioms. | |
smtrat::cadcells | |
A framework for sample-based CAD algorithms. | |
smtrat::cadcells::operators | |
Projection operators. | |
smtrat::cadcells::operators::rules | |
Implementation of derivation rules. | |
Functions | |
template<typename P > | |
bool | smtrat::cadcells::operators::rules::poly_del_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly) |
template<typename P > | |
bool | smtrat::cadcells::operators::rules::poly_proj_del (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly) |
template<typename P > | |
void | smtrat::cadcells::operators::rules::poly_irreducible_ord_inv_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly) |
template<typename P > | |
void | smtrat::cadcells::operators::rules::poly_ord_inv_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly) |
template<typename P > | |
void | smtrat::cadcells::operators::rules::root_ordering_holds_pdel (datastructures::SampledDerivation< P > &deriv, const datastructures::IndexedRootOrdering &ordering) |
template<typename P > | |
void | smtrat::cadcells::operators::rules::poly_irreducible_sgn_inv_pdel (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell, const datastructures::IndexedRootOrdering &, const boost::container::flat_set< datastructures::PolyRef > &ordering_non_projective_polys, datastructures::PolyRef poly) |