Implementation of derivation rules. More...

Namespaces
	filter_util

	ordering_util

Data Structures
struct	DelineateSettings

Functions
template<typename P >
bool	poly_non_null (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
bool	poly_del (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_ord_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_ord_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_sgn_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly, bool skip_if_ord_inv=true)

template<typename P >
void	poly_irreducible_nonzero_sgn_inv (datastructures::DelineatedDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	delineate (datastructures::DelineatedDerivation< P > &deriv, const properties::poly_irreducible_sgn_inv &prop)

template<typename P >
void	delineate (datastructures::DelineatedDerivation< P > &deriv, const properties::poly_irreducible_semi_sgn_inv &prop)

template<typename P >
void	cell_connected (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell, const datastructures::IndexedRootOrdering &ordering)

template<typename P >
void	cell_analytic_submanifold ([[maybe_unused]] datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &)

template<typename P >
void	poly_irreducible_sgn_inv_ec (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell, datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_semi_sgn_inv_ec (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell, datastructures::PolyRef poly)

template<typename P >
void	cell_represents (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell)

template<typename P >
void	root_ordering_holds (datastructures::SampledDerivation< P > &deriv, const datastructures::IndexedRootOrdering &ordering)

template<typename P >
void	poly_irreducible_sgn_inv (datastructures::SampledDerivation< P > &, const datastructures::SymbolicInterval &, const datastructures::IndexedRootOrdering &, [[maybe_unused]] datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_null_sgn_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	covering_holds (datastructures::DelineatedDerivation< P > &, const datastructures::CoveringDescription &covering, const datastructures::IndexedRootOrdering &ordering)

template<typename P >
void	delineate_all_compound (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop, bool enable_weak=true, bool enable_regular=true)

template<typename Settings , typename P >
void	delineate_all (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop, bool enable_weak=true)

template<typename P >
void	delineate_bounds_only (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop)

template<typename P >
void	delineate_noop (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop)

template<typename P >
void	delineate_all_biggest_cell (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop, bool enable_weak=true)

template<typename P >
void	delineate_compound_piecewiselinear (datastructures::SampledDerivation< P > &deriv, const properties::root_ordering_holds &prop, bool enable_weak=true)

template<typename P >
void	poly_loc_del (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &underlying_cell, const datastructures::IndexedRootOrdering &underlying_ordering, const boost::container::flat_set< datastructures::PolyRef > &ordering_polys, const datastructures::PolyRef poly)

template<typename P >
void	poly_ord_inv_base (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &cell, const datastructures::IndexedRootOrdering &, datastructures::PolyRef poly)

template<typename P >
bool	root_ordering_holds_delineated (datastructures::SampledDerivation< P > &deriv, const datastructures::SymbolicInterval &underlying_cell, const datastructures::IndexedRootOrdering &underlying_ordering, const boost::container::flat_set< datastructures::PolyRef > &ordering_polys, const datastructures::IndexedRootOrdering &ordering)

template<typename P >
void	poly_irreducible_sgn_inv_filtered (datastructures::SampledDerivation< P > &, const datastructures::SymbolicInterval &, const datastructures::IndexedRootOrdering &, [[maybe_unused]] datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_semi_sgn_inv_filtered (datastructures::SampledDerivation< P > &, const datastructures::SymbolicInterval &, const datastructures::IndexedRootOrdering &, [[maybe_unused]] datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_nonzero_semi_sgn_inv (datastructures::DelineatedDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_null_semi_sgn_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_semi_sgn_inv (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_ord_inv_nullified (datastructures::SampledDerivation< P > &deriv, const datastructures::PolyRef &poly)

template<typename P >
void	poly_ord_inv_maybe_null (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
bool	poly_del_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
bool	poly_proj_del (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_irreducible_ord_inv_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	poly_ord_inv_pdel (datastructures::SampledDerivation< P > &deriv, datastructures::PolyRef poly)

template<typename P >
void	root_ordering_holds_pdel (datastructures::SampledDerivation< P > &deriv, const datastructures::IndexedRootOrdering &ordering)

template<typename P >
void	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)

Detailed Description

Implementation of derivation rules.

Each rule is realized by a function which works on a derivation object. The parameters of the respective properties are passed as function parameter. The function realizing a derivation rule might either call other derivation rules or add properties to the given derivation.

Function Documentation

◆ cell_analytic_submanifold()

template<typename P >

void smtrat::cadcells::operators::rules::cell_analytic_submanifold	(	[[maybe_unused] ] datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &
	)

Definition at line 169 of file rules.h.

Here is the caller graph for this function:

◆ cell_connected()

template<typename P >

void smtrat::cadcells::operators::rules::cell_connected	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	cell,
		const datastructures::IndexedRootOrdering &	ordering
	)

Definition at line 160 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ cell_represents()

template<typename P >

void smtrat::cadcells::operators::rules::cell_represents	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	cell
	)

Definition at line 191 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ covering_holds()

template<typename P >

void smtrat::cadcells::operators::rules::covering_holds	(	datastructures::DelineatedDerivation< P > &	,
		const datastructures::CoveringDescription &	covering,
		const datastructures::IndexedRootOrdering &	ordering
	)

Definition at line 6 of file rules_covering.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate() [1/2]

template<typename P >

void smtrat::cadcells::operators::rules::delineate	(	datastructures::DelineatedDerivation< P > &	deriv,
		const properties::poly_irreducible_semi_sgn_inv &	prop
	)

Definition at line 143 of file rules.h.

Here is the call graph for this function:

◆ delineate() [2/2]

template<typename P >

void smtrat::cadcells::operators::rules::delineate	(	datastructures::DelineatedDerivation< P > &	deriv,
		const properties::poly_irreducible_sgn_inv &	prop
	)

Definition at line 126 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate_all()

template<typename Settings , typename P >

void smtrat::cadcells::operators::rules::delineate_all	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop,
		bool	enable_weak = `true`
	)

Definition at line 205 of file rules_filter.h.

Here is the call graph for this function:

◆ delineate_all_biggest_cell()

template<typename P >

void smtrat::cadcells::operators::rules::delineate_all_biggest_cell	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop,
		bool	enable_weak = `true`
	)

Definition at line 334 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate_all_compound()

template<typename P >

void smtrat::cadcells::operators::rules::delineate_all_compound	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop,
		bool	enable_weak = `true`,
		bool	enable_regular = `true`
	)

Definition at line 68 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate_bounds_only()

template<typename P >

void smtrat::cadcells::operators::rules::delineate_bounds_only	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop
	)

Definition at line 298 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate_compound_piecewiselinear()

template<typename P >

void smtrat::cadcells::operators::rules::delineate_compound_piecewiselinear	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop,
		bool	enable_weak = `true`
	)

Definition at line 401 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ delineate_noop()

template<typename P >

void smtrat::cadcells::operators::rules::delineate_noop	(	datastructures::SampledDerivation< P > &	deriv,
		const properties::root_ordering_holds &	prop
	)

Definition at line 317 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_del()

template<typename P >

bool smtrat::cadcells::operators::rules::poly_del	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 43 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_del_pdel()

template<typename P >

bool smtrat::cadcells::operators::rules::poly_del_pdel	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 9 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_nonzero_semi_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_nonzero_semi_sgn_inv	(	datastructures::DelineatedDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 548 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_nonzero_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_nonzero_sgn_inv	(	datastructures::DelineatedDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 118 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_null_semi_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_null_semi_sgn_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 555 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_null_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_null_sgn_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 244 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_ord_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_ord_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 54 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_ord_inv_nullified()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_ord_inv_nullified	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::PolyRef &	poly
	)

Definition at line 9 of file rules_null.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_ord_inv_pdel()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_ord_inv_pdel	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 32 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_semi_sgn_inv_ec()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_semi_sgn_inv_ec	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	cell,
		datastructures::PolyRef	poly
	)

Definition at line 185 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_semi_sgn_inv_filtered()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_semi_sgn_inv_filtered	(	datastructures::SampledDerivation< P > &	,
		const datastructures::SymbolicInterval &	,
		const datastructures::IndexedRootOrdering &	,
		[[maybe_unused] ] datastructures::PolyRef	poly
	)

Definition at line 543 of file rules_filter.h.

Here is the caller graph for this function:

◆ poly_irreducible_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_sgn_inv	(	datastructures::SampledDerivation< P > &	,
		const datastructures::SymbolicInterval &	,
		const datastructures::IndexedRootOrdering &	,
		[[maybe_unused] ] datastructures::PolyRef	poly
	)

Definition at line 239 of file rules.h.

Here is the caller graph for this function:

◆ poly_irreducible_sgn_inv_ec()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_sgn_inv_ec	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	cell,
		datastructures::PolyRef	poly
	)

Definition at line 174 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_irreducible_sgn_inv_filtered()

template<typename P >

void smtrat::cadcells::operators::rules::poly_irreducible_sgn_inv_filtered	(	datastructures::SampledDerivation< P > &	,
		const datastructures::SymbolicInterval &	,
		const datastructures::IndexedRootOrdering &	,
		[[maybe_unused] ] datastructures::PolyRef	poly
	)

Definition at line 538 of file rules_filter.h.

Here is the caller graph for this function:

◆ poly_irreducible_sgn_inv_pdel()

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
	)

Definition at line 81 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_loc_del()

template<typename P >

void smtrat::cadcells::operators::rules::poly_loc_del	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	underlying_cell,
		const datastructures::IndexedRootOrdering &	underlying_ordering,
		const boost::container::flat_set< datastructures::PolyRef > &	ordering_polys,
		const datastructures::PolyRef	poly
	)

inline

Definition at line 468 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_non_null()

template<typename P >

bool smtrat::cadcells::operators::rules::poly_non_null	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 16 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_ord_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_ord_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 71 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_ord_inv_base()

template<typename P >

void smtrat::cadcells::operators::rules::poly_ord_inv_base	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	cell,
		const datastructures::IndexedRootOrdering &	,
		datastructures::PolyRef	poly
	)

Definition at line 503 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_ord_inv_maybe_null()

template<typename P >

void smtrat::cadcells::operators::rules::poly_ord_inv_maybe_null	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 50 of file rules_null.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_ord_inv_pdel()

template<typename P >

void smtrat::cadcells::operators::rules::poly_ord_inv_pdel	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 49 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_proj_del()

template<typename P >

bool smtrat::cadcells::operators::rules::poly_proj_del	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 22 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_semi_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_semi_sgn_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly
	)

Definition at line 562 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ poly_sgn_inv()

template<typename P >

void smtrat::cadcells::operators::rules::poly_sgn_inv	(	datastructures::SampledDerivation< P > &	deriv,
		datastructures::PolyRef	poly,
		bool	skip_if_ord_inv = `true`
	)

Definition at line 85 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ root_ordering_holds()

template<typename P >

void smtrat::cadcells::operators::rules::root_ordering_holds	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::IndexedRootOrdering &	ordering
	)

Definition at line 222 of file rules.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ root_ordering_holds_delineated()

template<typename P >

bool smtrat::cadcells::operators::rules::root_ordering_holds_delineated	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::SymbolicInterval &	underlying_cell,
		const datastructures::IndexedRootOrdering &	underlying_ordering,
		const boost::container::flat_set< datastructures::PolyRef > &	ordering_polys,
		const datastructures::IndexedRootOrdering &	ordering
	)

Definition at line 518 of file rules_filter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ root_ordering_holds_pdel()

template<typename P >

void smtrat::cadcells::operators::rules::root_ordering_holds_pdel	(	datastructures::SampledDerivation< P > &	deriv,
		const datastructures::IndexedRootOrdering &	ordering
	)

Definition at line 63 of file rules_pdel.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Namespaces

Data Structures

Functions

Detailed Description

Function Documentation

◆ cell_analytic_submanifold()

◆ cell_connected()

◆ cell_represents()

◆ covering_holds()

◆ delineate() [1/2]

◆ delineate() [2/2]

◆ delineate_all()

◆ delineate_all_biggest_cell()

◆ delineate_all_compound()

◆ delineate_bounds_only()

◆ delineate_compound_piecewiselinear()

◆ delineate_noop()

◆ poly_del()

◆ poly_del_pdel()

◆ poly_irreducible_nonzero_semi_sgn_inv()

◆ poly_irreducible_nonzero_sgn_inv()

◆ poly_irreducible_null_semi_sgn_inv()

◆ poly_irreducible_null_sgn_inv()

◆ poly_irreducible_ord_inv()

◆ poly_irreducible_ord_inv_nullified()

◆ poly_irreducible_ord_inv_pdel()

◆ poly_irreducible_semi_sgn_inv_ec()

◆ poly_irreducible_semi_sgn_inv_filtered()

◆ poly_irreducible_sgn_inv()

◆ poly_irreducible_sgn_inv_ec()

◆ poly_irreducible_sgn_inv_filtered()

◆ poly_irreducible_sgn_inv_pdel()

◆ poly_loc_del()

◆ poly_non_null()

◆ poly_ord_inv()

◆ poly_ord_inv_base()

◆ poly_ord_inv_maybe_null()

◆ poly_ord_inv_pdel()

◆ poly_proj_del()

◆ poly_semi_sgn_inv()

◆ poly_sgn_inv()

◆ root_ordering_holds()

◆ root_ordering_holds_delineated()

◆ root_ordering_holds_pdel()