Encapsulates all computations on polynomials. More...

#include <projections.h>

Collaboration diagram for smtrat::cadcells::datastructures::Projections:

[legend]

Public Member Functions
auto	main_var (PolyRef p) const

	Projections (PolyPool &pool)

auto &	polys ()

const auto &	polys () const

void	clear_cache (size_t)
	Clears all polynomials of the specified level and higher in the polynomial cache as well as their projection results. More...

void	clear_assignment_cache (const Assignment &)
	Clears all projections cached with respect to this assignment. More...

PolyRef	res (PolyRef p, PolyRef q)

bool	know_disc (PolyRef p) const

bool	know_res (PolyRef p, PolyRef q) const

bool	known (const Polynomial &p) const

PolyRef	disc (PolyRef p)

PolyRef	ldcf (PolyRef p)

const std::vector< PolyRef > &	factors_nonconst (PolyRef p)

bool	is_zero (const Assignment &sample, PolyRef p)

size_t	num_roots (const Assignment &sample, PolyRef p)

const std::vector< RAN > &	real_roots (const Assignment &sample, PolyRef p)

const std::vector< RAN >	real_roots_reducible (const Assignment &sample, PolyRef p)

bool	is_nullified (const Assignment &sample, PolyRef p)

bool	is_ldcf_zero (const Assignment &sample, PolyRef p)

bool	is_disc_zero (const Assignment &sample, PolyRef p)

bool	is_const (PolyRef p)

bool	is_zero (PolyRef p)

std::vector< PolyRef >	coeffs (PolyRef p)

bool	has_const_coeff (PolyRef p) const

PolyRef	simplest_nonzero_coeff (const Assignment &sample, PolyRef p, std::function< bool(const Polynomial &, const Polynomial &)> compare)

std::vector< carl::Variable >	variables (PolyRef p)

PolyRef	derivative (PolyRef p, carl::Variable var)

std::size_t	degree (PolyRef p) const

std::size_t	total_degree (PolyRef p)

const std::vector< std::size_t > &	monomial_total_degrees (PolyRef p)

const std::vector< std::size_t > &	monomial_degrees (PolyRef p)

RAN	evaluate (const Assignment &sample, IndexedRoot r)

std::pair< RAN, std::vector< datastructures::IndexedRoot > >	evaluate_min (const Assignment &ass, const std::vector< datastructures::IndexedRoot > &roots)

std::pair< RAN, std::vector< datastructures::IndexedRoot > >	evaluate_max (const Assignment &ass, const std::vector< datastructures::IndexedRoot > &roots)

std::pair< RAN, std::vector< datastructures::IndexedRoot > >	evaluate (const Assignment &ass, const datastructures::CompoundMinMax &bound)

std::pair< RAN, std::vector< datastructures::IndexedRoot > >	evaluate (const Assignment &ass, const datastructures::CompoundMaxMin &bound)

std::pair< RAN, std::vector< datastructures::IndexedRoot > >	evaluate (const Assignment &ass, const datastructures::RootFunction &f)

PolyConstraint	negation (const PolyConstraint &constraint) const

auto	evaluate (const Assignment &ass, const PolyConstraint &constraint)

Private Member Functions
auto &	cache (PolyRef p)

const auto &	cache (PolyRef p) const

bool	has_cache (PolyRef p) const

size_t	level_of (const Assignment &a) const

auto &	cache (const Assignment &a)

const auto &	cache (const Assignment &a) const

Assignment	restrict_assignment (Assignment ass, PolyRef p)

Assignment	restrict_base_assignment (Assignment ass, PolyRef p)

Private Attributes
PolyPool &	m_pool

std::vector< std::vector< detail::PolyProperties > >	m_poly_cache

std::vector< std::map< Assignment, detail::AssignmentProperties > >	m_assignment_cache

Detailed Description

Encapsulates all computations on polynomials.

Computations are cached with respect to a PolyPool.

Definition at line 46 of file projections.h.

Constructor & Destructor Documentation

◆ Projections()

smtrat::cadcells::datastructures::Projections::Projections ( PolyPool & pool )

inline

Definition at line 124 of file projections.h.

Member Function Documentation

◆ cache() [1/4]

auto& smtrat::cadcells::datastructures::Projections::cache ( const Assignment & a )

inlineprivate

Definition at line 83 of file projections.h.

Here is the call graph for this function:

◆ cache() [2/4]

const auto& smtrat::cadcells::datastructures::Projections::cache ( const Assignment & a ) const

inlineprivate

Definition at line 87 of file projections.h.

Here is the call graph for this function:

◆ cache() [3/4]

auto& smtrat::cadcells::datastructures::Projections::cache ( PolyRef p )

inlineprivate

Definition at line 51 of file projections.h.

Here is the caller graph for this function:

◆ cache() [4/4]

const auto& smtrat::cadcells::datastructures::Projections::cache ( PolyRef p ) const

inlineprivate

Definition at line 61 of file projections.h.

◆ clear_assignment_cache()

void smtrat::cadcells::datastructures::Projections::clear_assignment_cache ( const Assignment & )

inline

Clears all projections cached with respect to this assignment.

Definition at line 145 of file projections.h.

◆ clear_cache()

void smtrat::cadcells::datastructures::Projections::clear_cache ( size_t )

inline

Clears all polynomials of the specified level and higher in the polynomial cache as well as their projection results.

Definition at line 132 of file projections.h.

◆ coeffs()

std::vector<PolyRef> smtrat::cadcells::datastructures::Projections::coeffs ( PolyRef p )

inline

Definition at line 341 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ degree()

std::size_t smtrat::cadcells::datastructures::Projections::degree ( PolyRef p ) const

inline

Definition at line 403 of file projections.h.

Here is the caller graph for this function:

◆ derivative()

PolyRef smtrat::cadcells::datastructures::Projections::derivative	(	PolyRef	p,
		carl::Variable	var
	)

inline

Definition at line 381 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ disc()

PolyRef smtrat::cadcells::datastructures::Projections::disc ( PolyRef p )

inline

Definition at line 204 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluate() [1/5]

std::pair<RAN,std::vector<datastructures::IndexedRoot> > smtrat::cadcells::datastructures::Projections::evaluate	(	const Assignment &	ass,
		const datastructures::CompoundMaxMin &	bound
	)

inline

Definition at line 483 of file projections.h.

Here is the call graph for this function:

◆ evaluate() [2/5]

std::pair<RAN,std::vector<datastructures::IndexedRoot> > smtrat::cadcells::datastructures::Projections::evaluate	(	const Assignment &	ass,
		const datastructures::CompoundMinMax &	bound
	)

inline

Definition at line 467 of file projections.h.

Here is the call graph for this function:

◆ evaluate() [3/5]

std::pair<RAN,std::vector<datastructures::IndexedRoot> > smtrat::cadcells::datastructures::Projections::evaluate	(	const Assignment &	ass,
		const datastructures::RootFunction &	f
	)

inline

Definition at line 499 of file projections.h.

Here is the call graph for this function:

◆ evaluate() [4/5]

auto smtrat::cadcells::datastructures::Projections::evaluate	(	const Assignment &	ass,
		const PolyConstraint &	constraint
	)

inline

Definition at line 510 of file projections.h.

Here is the call graph for this function:

◆ evaluate() [5/5]

RAN smtrat::cadcells::datastructures::Projections::evaluate	(	const Assignment &	sample,
		IndexedRoot	r
	)

inline

Definition at line 429 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluate_max()

std::pair<RAN,std::vector<datastructures::IndexedRoot> > smtrat::cadcells::datastructures::Projections::evaluate_max	(	const Assignment &	ass,
		const std::vector< datastructures::IndexedRoot > &	roots
	)

inline

Definition at line 451 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ evaluate_min()

std::pair<RAN,std::vector<datastructures::IndexedRoot> > smtrat::cadcells::datastructures::Projections::evaluate_min	(	const Assignment &	ass,
		const std::vector< datastructures::IndexedRoot > &	roots
	)

inline

Definition at line 435 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ factors_nonconst()

const std::vector<PolyRef>& smtrat::cadcells::datastructures::Projections::factors_nonconst ( PolyRef p )

inline

Definition at line 238 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ has_cache()

bool smtrat::cadcells::datastructures::Projections::has_cache ( PolyRef p ) const

inlineprivate

Definition at line 67 of file projections.h.

Here is the caller graph for this function:

◆ has_const_coeff()

bool smtrat::cadcells::datastructures::Projections::has_const_coeff ( PolyRef p ) const

inline

Definition at line 352 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_const()

bool smtrat::cadcells::datastructures::Projections::is_const ( PolyRef p )

inline

Definition at line 333 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_disc_zero()

bool smtrat::cadcells::datastructures::Projections::is_disc_zero	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 329 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_ldcf_zero()

bool smtrat::cadcells::datastructures::Projections::is_ldcf_zero	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 325 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_nullified()

bool smtrat::cadcells::datastructures::Projections::is_nullified	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 309 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_zero() [1/2]

bool smtrat::cadcells::datastructures::Projections::is_zero	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 250 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ is_zero() [2/2]

bool smtrat::cadcells::datastructures::Projections::is_zero ( PolyRef p )

inline

Definition at line 337 of file projections.h.

◆ know_disc()

bool smtrat::cadcells::datastructures::Projections::know_disc ( PolyRef p ) const

inline

Definition at line 187 of file projections.h.

Here is the call graph for this function:

◆ know_res()

bool smtrat::cadcells::datastructures::Projections::know_res	(	PolyRef	p,
		PolyRef	q
	)		const

inline

Definition at line 192 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ known()

bool smtrat::cadcells::datastructures::Projections::known ( const Polynomial & p ) const

inline

Definition at line 200 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ ldcf()

PolyRef smtrat::cadcells::datastructures::Projections::ldcf ( PolyRef p )

inline

Definition at line 221 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ level_of()

size_t smtrat::cadcells::datastructures::Projections::level_of ( const Assignment & a ) const

inlineprivate

Definition at line 72 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ main_var()

auto smtrat::cadcells::datastructures::Projections::main_var ( PolyRef p ) const

inline

Definition at line 94 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ monomial_degrees()

const std::vector<std::size_t>& smtrat::cadcells::datastructures::Projections::monomial_degrees ( PolyRef p )

inline

Definition at line 422 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ monomial_total_degrees()

const std::vector<std::size_t>& smtrat::cadcells::datastructures::Projections::monomial_total_degrees ( PolyRef p )

inline

Definition at line 415 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ negation()

PolyConstraint smtrat::cadcells::datastructures::Projections::negation ( const PolyConstraint & constraint ) const

inline

Definition at line 506 of file projections.h.

Here is the caller graph for this function:

◆ num_roots()

size_t smtrat::cadcells::datastructures::Projections::num_roots	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 262 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ polys() [1/2]

auto& smtrat::cadcells::datastructures::Projections::polys ( )

inline

Definition at line 126 of file projections.h.

Here is the caller graph for this function:

◆ polys() [2/2]

const auto& smtrat::cadcells::datastructures::Projections::polys ( ) const

inline

Definition at line 127 of file projections.h.

◆ real_roots()

const std::vector<RAN>& smtrat::cadcells::datastructures::Projections::real_roots	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 277 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ real_roots_reducible()

const std::vector<RAN> smtrat::cadcells::datastructures::Projections::real_roots_reducible	(	const Assignment &	sample,
		PolyRef	p
	)

inline

Definition at line 292 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ res()

PolyRef smtrat::cadcells::datastructures::Projections::res	(	PolyRef	p,
		PolyRef	q
	)

inline

Definition at line 165 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ restrict_assignment()

Assignment smtrat::cadcells::datastructures::Projections::restrict_assignment	(	Assignment	ass,
		PolyRef	p
	)

inlineprivate

Definition at line 99 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ restrict_base_assignment()

Assignment smtrat::cadcells::datastructures::Projections::restrict_base_assignment	(	Assignment	ass,
		PolyRef	p
	)

inlineprivate

Definition at line 111 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ simplest_nonzero_coeff()

PolyRef smtrat::cadcells::datastructures::Projections::simplest_nonzero_coeff	(	const Assignment &	sample,
		PolyRef	p,
		std::function< bool(const Polynomial &, const Polynomial &)>	compare
	)

inline

Definition at line 359 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ total_degree()

std::size_t smtrat::cadcells::datastructures::Projections::total_degree ( PolyRef p )

inline

Definition at line 407 of file projections.h.

Here is the call graph for this function:

Here is the caller graph for this function:

◆ variables()

std::vector<carl::Variable> smtrat::cadcells::datastructures::Projections::variables ( PolyRef p )

inline

Definition at line 377 of file projections.h.

Here is the caller graph for this function:

Field Documentation

◆ m_assignment_cache

std::vector<std::map<Assignment,detail::AssignmentProperties> > smtrat::cadcells::datastructures::Projections::m_assignment_cache

private

Definition at line 49 of file projections.h.

◆ m_poly_cache

std::vector<std::vector<detail::PolyProperties> > smtrat::cadcells::datastructures::Projections::m_poly_cache

private

Definition at line 48 of file projections.h.

◆ m_pool

PolyPool& smtrat::cadcells::datastructures::Projections::m_pool

private

Definition at line 47 of file projections.h.

The documentation for this class was generated from the following file:

smtrat-cadcells/datastructures/projections.h

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Projections()

Member Function Documentation

◆ cache() [1/4]

◆ cache() [2/4]

◆ cache() [3/4]

◆ cache() [4/4]

◆ clear_assignment_cache()

◆ clear_cache()

◆ coeffs()

◆ degree()

◆ derivative()

◆ disc()

◆ evaluate() [1/5]

◆ evaluate() [2/5]

◆ evaluate() [3/5]

◆ evaluate() [4/5]

◆ evaluate() [5/5]

◆ evaluate_max()

◆ evaluate_min()

◆ factors_nonconst()

◆ has_cache()

◆ has_const_coeff()

◆ is_const()

◆ is_disc_zero()

◆ is_ldcf_zero()

◆ is_nullified()

◆ is_zero() [1/2]

◆ is_zero() [2/2]

◆ know_disc()

◆ know_res()

◆ known()

◆ ldcf()

◆ level_of()

◆ main_var()

◆ monomial_degrees()

◆ monomial_total_degrees()

◆ negation()

◆ num_roots()

◆ polys() [1/2]

◆ polys() [2/2]

◆ real_roots()

◆ real_roots_reducible()

◆ res()

◆ restrict_assignment()

◆ restrict_base_assignment()

◆ simplest_nonzero_coeff()

◆ total_degree()

◆ variables()

Field Documentation

◆ m_assignment_cache

◆ m_poly_cache

◆ m_pool