smtrat::cad::projection::lazard Namespace Reference

Contains the implementation of Lazards projection operator as specified in [Lauard1994]. More...

Functions
template<typename Poly , typename Callback >
void	single (const Poly &p, carl::Variable variable, Callback &&cb)
	Implements the part of Lazards projection operator from [21] that deals with a single polynomial p: . More...
template<typename Poly , typename Callback >
void	paired (const Poly &p, const UPoly &q, carl::Variable variable, Callback &&cb)
	Implements the part of Lazard projection operator from [21] that deals with two polynomials p and q which is just the respective part of McCallums projection operator mccallum::paired. More...

Detailed Description

Contains the implementation of Lazards projection operator as specified in [Lauard1994].

Function Documentation

paired()

template<typename Poly , typename Callback >

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

Implements the part of Lazard projection operator from [21] that deals with two polynomials p and q which is just the respective part of McCallums projection operator mccallum::paired.

Definition at line 31 of file Lazard.h.

Here is the call graph for this function:

Here is the caller graph for this function:

single()

template<typename Poly , typename Callback >

void smtrat::cad::projection::lazard::single	(	const Poly &	p,
		carl::Variable	variable,
		Callback &&	cb
	)

Implements the part of Lazards projection operator from [21] that deals with a single polynomial p: .

Definition at line 20 of file Lazard.h.

Here is the call graph for this function:

Here is the caller graph for this function: