Contains the implementation of Collins projection operator as specified in [5] below Theorem 4. More...

Functions
template<typename Poly , typename Callback >
void	single (const Poly &p, carl::Variable variable, Callback &&cb)
	Implements the part of Collins projection operator from [5] that deals with a single polynomial `p`: $\bigcup_{B \in RED(p)} \{ ldcf(B) \} \cup PSC(B, B')$ . More...

template<typename Poly , typename Callback >
void	paired (const Poly &p, const UPoly &q, carl::Variable variable, Callback &&cb)
	Implements the part of Collins projection operator from [5] that deals with two polynomials `p` and `q`: $\bigcup_{B_1 \in RED(p), B_2 \in RED(q)} PSC(B_1, B_2)$ . More...

Detailed Description

Contains the implementation of Collins projection operator as specified in [5] below Theorem 4.

Function Documentation

◆ paired()

template<typename Poly , typename Callback >

void smtrat::cad::projection::collins::paired	(	const Poly &	p,
		const UPoly &	q,
		carl::Variable	variable,
		Callback &&	cb
	)

Implements the part of Collins projection operator from [5] that deals with two polynomials p and q: $\bigcup_{B_1 \in RED(p), B_2 \in RED(q)} PSC(B_1, B_2)$ .

Definition at line 49 of file Collins.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ single()