smtrat::cad::projection::brown Namespace Reference

Contains the implementation of Browns projection operator as specified in [3] after Theorem 3.1. More...

Functions
template<typename Poly , typename Callback >
void	single (const Poly &p, carl::Variable variable, Callback &&cb)
	Implements the part of Browns projection operator from [3] 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 Browns projection operator from [3] 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 Browns projection operator as specified in [3] after Theorem 3.1.

Function Documentation

paired()

template<typename Poly , typename Callback >

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

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

Definition at line 30 of file Brown.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::brown::single	(	const Poly &	p,
		carl::Variable	variable,
		Callback &&	cb
	)

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

Definition at line 20 of file Brown.h.

Here is the call graph for this function:

Here is the caller graph for this function: