A collection of methods that lead directly to the computation of the CAD. More...

#include <CAD.h>

Collaboration diagram for GiNaCRA::CAD:

Public Member Functions
	CAD ()
	CAD (const UnivariatePolynomialSet &s, const vector< symbol > &v, CADSettings setting=CADSettings::getSettings())
	CAD (const CAD &cad)
const vector< symbol >	variables ()
const vector < UnivariatePolynomial >	polynomials ()
const vector< vector < UnivariatePolynomial > >	eliminationSets ()
bool	isComplete () const
void	complete ()
	Computes all samples in this cad.
const vector< RealAlgebraicPoint >	samples ()
	Generates all real algebraic points of cad cells computed so far.
bool	check (const vector< Constraint > &constraints, RealAlgebraicPoint &r)
	Checks an arbitrary constraint for satisfiability on this set of samples.
void	printSampleTree (std::ostream &os=std::cout)
	Prints the current sample tree to the designated output stream.
void	addPolynomial (const UnivariatePolynomial &p, const vector< GiNaC::symbol > &v, unsigned setting=DEFAULT_CADSETTING)
	Insert the given polynomial to the cad.
template<class InputIterator >
void	addPolynomials (InputIterator first, InputIterator last, const vector< GiNaC::symbol > &v, unsigned setting=DEFAULT_CADSETTING)
	Insert the polynomials starting at first ending the point before last.
Static Public Member Functions
static const UnivariatePolynomialSet	eliminationSet (const UnivariatePolynomialSet &P, const symbol &nextVariable) throw ( invalid_argument )
	Elimination/projection due to Hoon Hong ["An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition", ACM, 1990.
static const SampleList	samples (const list< RealAlgebraicNumberPtr > &roots, SampleList &currentSamples) throw ( invalid_argument )
	Constructs the samples at the base level of a CAD construction, provided a set of prevailing samples.
static const SampleList	samples (const list< RationalUnivariatePolynomial > &polynomials, SampleList &currentSamples) throw ( invalid_argument )
	Generates a list of sample points for a list of rational univariate polynomials.
static void	elimination (const UnivariatePolynomial &p, const symbol &variable, UnivariatePolynomialSet &eliminated) throw ( invalid_argument )
	Performs all steps of a CAD elimination/projection operator which are related to one single polynomial.
static void	elimination (const UnivariatePolynomial &p, const UnivariatePolynomial &q, const symbol &variable, UnivariatePolynomialSet &eliminated) throw ( invalid_argument )
	Performs all steps of a CAD elimination/projection operator which are related to a pair of polynomials.
static const SampleList	samples (const RationalUnivariatePolynomial &p, SampleList &currentSamples, CADSettings settings=CADSettings::getSettings()) throw ( invalid_argument )
	Constructs the samples at the base level of a CAD construction.
static const SampleList	samples (const UnivariatePolynomial &p, const list< RealAlgebraicNumberPtr > &sample, const list< symbol > &variables, SampleList &currentSamples, CADSettings settings=CADSettings::getSettings()) throw ( invalid_argument )
	Constructs the samples for `p` given the sample values `sample` with their corresponding variables for the coefficient polynomials.
Private Member Functions
void	alterSetting (unsigned setting=DEFAULT_CADSETTING, RealAlgebraicNumberSettings::IsolationStrategy isolationStrategy=RealAlgebraicNumberSettings::DEFAULT_ISOLATIONSTRATEGY)
	Change the setting of the current CAD object.
const RealAlgebraicPoint	constructSampleAt (tree< RealAlgebraicNumberPtr >::iterator node, const tree< RealAlgebraicNumberPtr >::iterator &root) const
	Constructs the path from the given node to the root and conjoins all RealAlgebraicNumbers on the nodes of the path.
const bool	liftCheck (tree< RealAlgebraicNumberPtr >::iterator node, const list< RealAlgebraicNumberPtr > &sample, unsigned level, const list< symbol > &variables, const vector< Constraint > &constraints, RealAlgebraicPoint &r) throw ( invalid_argument )
	Constructs new samples in the sample tree by successive evaluation of projection polynomial coefficients and univariate sample construction until a satisfying sample is found or there is none.
const bool	satisfys (const RealAlgebraicPoint &r, const vector< Constraint > &constraints) const
	Returns the truth value as to whether the conjunction of the `constraints`is satisfied by the real algebraic point `r`.
Static Private Member Functions
static const UnivariatePolynomialSet	truncation (const UnivariatePolynomial &P)
	Generates the set of truncations of the polynomial.
static const UnivariatePolynomialSet	truncation (const UnivariatePolynomialSet &P)
	Generates the set of truncations of the polynomial set.
Private Attributes
vector< symbol >	mVariables
	fix list of variables for all computations
tree< RealAlgebraicNumberPtr >	mSampleTree
	sample components built during the computation arranged in a tree
vector< SampleList >	mSampleListIncrements
	level-wise list of sample components representing the samples belonging to the current lifting position
vector< vector < UnivariatePolynomial > >	mEliminationSets
	lists of polynomials occurring in every elimination level (immutable; new polynomials are appended at the tail)
vector< list< unsigned > >	mLiftingPositions
	stack of positions for the next lifting in each level
bool	mIsComplete
	flag indicating whether the sample construction is completed or not
CADSettings	mSetting
	setting for internal heuristics

Detailed Description

A collection of methods that lead directly to the computation of the CAD.

Author:: Joachim Redies; Ulrich Loup

Since:: 2011-11-03

Definition at line 707 of file CAD.h.

Constructor & Destructor Documentation

GiNaCRA::CAD::CAD ( )

Definition at line 48 of file CAD.cpp.

References GiNaCRA::tree< T, tree_node_allocator >::begin(), GiNaCRA::tree< T, tree_node_allocator >::insert(), and mSampleTree.

GiNaCRA::CAD::CAD	(	const UnivariatePolynomialSet &	s,
		const vector< symbol > &	v,
		CADSettings	setting = `CADSettings::getSettings()`
	)

Parameters:

s	input polynomials whose solution space is covered by this cad.
v	main symbols of the polynomials in desired order of elimination (lifting order is vice versa!)
setting	a setting type for a collection of CAD settings (standard option is the standard option of CADSettings::getSettings( ))

Runtime complexity:: O( 2^(2^v.size()) ) many polynomials could be generated during the initial elimination

A note on the elimination and lifting order: (n be the number of variables)

The (i-1)-th variable (main variable of the current UnivariatePolynomialSet) is eliminated in the i-th step, thus ending up with the variable n-1 in the last elimination set.

Definition at line 61 of file CAD.cpp.

References GiNaCRA::VariableListPool::addVariable(), GiNaCRA::tree< T, tree_node_allocator >::begin(), GiNaCRA::RationalUnivariatePolynomial::countRealRoots(), eliminationSet(), GiNaCRA::MultivariatePolynomialSettings::InitializeGiNaCRAMultivariateMR(), GiNaCRA::UnivariatePolynomialSet::insert(), GiNaCRA::tree< T, tree_node_allocator >::insert(), mEliminationSets, mIsComplete, mLiftingPositions, mSampleTree, mSetting, GiNaCRA::CADSettings::mUP_isLess, mVariables, GiNaCRA::CADSettings::simplifyByGroebner(), GiNaCRA::CADSettings::simplifyByRootcounting(), and GiNaCRA::CADSettings::simplifyBySquarefreeing().

GiNaCRA::CAD::CAD ( const CAD & cad ) [inline]

Definition at line 732 of file CAD.h.

Member Function Documentation

void GiNaCRA::CAD::addPolynomial	(	const UnivariatePolynomial &	p,
		const vector< GiNaC::symbol > &	v,
		unsigned	setting = `DEFAULT_CADSETTING`
	)		`[inline]`

Insert the given polynomial to the cad.

All elimination sets are recomputed.

Parameters:

p	polynomial to be added
v	the polynomial's variables (parameters and main variable)
setting	a setting type for a collection of CAD settings (standard option is CADSettings::GENERIC_CADSETTING). The settings are altered before the new polynomial is added.

Runtime complexity:: O( 2^(2^mVariables.size()) ) many polynomials could be generated during the initial elimination

Definition at line 825 of file CAD.h.

References addPolynomials().

template<class InputIterator >

void GiNaCRA::CAD::addPolynomials	(	InputIterator	first,
		InputIterator	last,
		const vector< GiNaC::symbol > &	v,
		unsigned	setting = `DEFAULT_CADSETTING`
	)		`[inline]`

Insert the polynomials starting at first ending the point before last.

All elimination sets are recomputed.

Parameters:

first	iterator marking the beginning of the elements to insert
last	iterator marking the end of the elements to insert (not inserted!)
v	the polynomials' variables (parameters and main variable)
setting	a setting type for a collection of CAD settings (standard option is CADSettings::GENERIC_CADSETTING). The settings are altered before the new polynomials are added.

Runtime complexity:: O( 2^(2^variables.size()) ) many polynomials could be generated during the elimination

Definition at line 843 of file CAD.h.

References GiNaCRA::VariableListPool::addVariable(), alterSetting(), GiNaCRA::RationalUnivariatePolynomial::countRealRoots(), eliminationSet(), GiNaCRA::MultivariatePolynomialSettings::InitializeGiNaCRAMultivariateMR(), GiNaCRA::UnivariatePolynomialSet::insert(), mEliminationSets, mIsComplete, mLiftingPositions, mSampleListIncrements, mSetting, GiNaCRA::CADSettings::mUP_isLess, mVariables, GiNaCRA::CADSettings::simplifyByGroebner(), GiNaCRA::CADSettings::simplifyByRootcounting(), and GiNaCRA::CADSettings::simplifyBySquarefreeing().

Referenced by addPolynomial().

void GiNaCRA::CAD::alterSetting	(	unsigned	setting = `DEFAULT_CADSETTING`,
		RealAlgebraicNumberSettings::IsolationStrategy	isolationStrategy = `RealAlgebraicNumberSettings::DEFAULT_ISOLATIONSTRATEGY`
	)		`[inline, private]`

Change the setting of the current CAD object.

Parameters:

setting
isolationStrategy

Definition at line 1067 of file CAD.h.

References GiNaCRA::CADSettings::getSettings(), and mSetting.

Referenced by addPolynomials().

bool GiNaCRA::CAD::check	(	const vector< Constraint > &	constraints,
		RealAlgebraicPoint &	r
	)

Checks an arbitrary constraint for satisfiability on this set of samples.

The cad is extended if there are still samples not computed. Remarks:

If all input constraints are build upon factors of the polynomials underlying this cad, then check returns a sound and complete result.
If there is a constraint whose polynomial is no factor of the polynomials underlying this cad, then only soundness is guaranteed.

Parameters:

constraints	conjunction of input constraints
r	contains a satisfying sample if the constraint is satisfiable by the cad

Returns:: true if the constraint was satisfied by a cell in the cad, false otherwise

Definition at line 171 of file CAD.cpp.

References GiNaCRA::tree< T, tree_node_allocator >::begin(), GiNaCRA::tree< T, tree_node_allocator >::head, liftCheck(), mIsComplete, mSampleTree, mVariables, samples(), and satisfys().

Referenced by complete().

void GiNaCRA::CAD::complete ( )

Computes all samples in this cad.

Definition at line 151 of file CAD.cpp.

References check(), mVariables, and GiNaC::ZERO_SIGN.

const RealAlgebraicPoint GiNaCRA::CAD::constructSampleAt	(	tree< RealAlgebraicNumberPtr >::iterator	node,
		const tree< RealAlgebraicNumberPtr >::iterator &	root
	)		const `[inline, private]`

Constructs the path from the given node to the root and conjoins all RealAlgebraicNumbers on the nodes of the path.

Parameters:

node
root	of the sample tree

Returns:: RealAlgebraicPoint belonging to leaf

Definition at line 359 of file CAD.cpp.

References mSampleTree, and GiNaCRA::tree< T, tree_node_allocator >::parent().

Referenced by samples().

void GiNaCRA::CAD::elimination	(	const UnivariatePolynomial &	p,
		const symbol &	variable,
		UnivariatePolynomialSet &	eliminated
	)		throw ( invalid_argument ) `[static]`

Performs all steps of a CAD elimination/projection operator which are related to one single polynomial.

Note that the set returned by this method should be disjoint to the set returned by the two-polynomial variant of eliminate.

Parameters:

p	input polynomial for the elimination procedure
variable	the new main variable for the returned set
eliminated	the set of eliminated polynomials to be augmented by the result of the elimination

Runtime complexity:: O ( deg(P) ) subresultant computations. The degree of the output is bound by O(deg(P)^2)!

Returns:: a list of polynomials in which the main variable of p is eliminated

Definition at line 312 of file CAD.cpp.

References GiNaCRA::UnivariatePolynomial::diff(), GiNaCRA::UnivariatePolynomial::isZero(), GiNaCRA::UnivariatePolynomial::principalSubresultantCoefficients(), and truncation().

void GiNaCRA::CAD::elimination	(	const UnivariatePolynomial &	p,
		const UnivariatePolynomial &	q,
		const symbol &	variable,
		UnivariatePolynomialSet &	eliminated
	)		throw ( invalid_argument ) `[static]`

Performs all steps of a CAD elimination/projection operator which are related to a pair of polynomials.

Note that the set returned by this method should be disjoint to the set returned by the single-polynomial variant of eliminate.

Parameters:

p	first input polynomial for the elimination procedure
q	second input polynomial for the elimination procedure
variable	the new main variable for the returned set
eliminated	the set of eliminated polynomials to be augmented by the result of the elimination

Runtime complexity:: O( deg(P)^2 ) subresultant computations. The degree of the output is bound by O(max(deg(P),deg(Q))^2)!

Returns:: a list of polynomials in which the main variable of p1 and p2 is eliminated

Definition at line 329 of file CAD.cpp.

References GiNaCRA::UnivariatePolynomial::principalSubresultantCoefficients(), and truncation().

const UnivariatePolynomialSet GiNaCRA::CAD::eliminationSet	(	const UnivariatePolynomialSet &	P,
		const symbol &	nextVariable
	)		throw ( invalid_argument ) `[static]`

Elimination/projection due to Hoon Hong ["An Improvement of the Projection Operator in Cylindrical Algebraic Decomposition", ACM, 1990.

]

Parameters:

P	set of polynomials in the variable to eliminate
nextVariable	the new main variable for the returned set

Runtime complexity:: O( m^2 * d^2 ) where m is the size of P and d the maximum degree of the polynomials in P

Returns:: A set of polynomials in which the main variable of P is eliminated

Definition at line 209 of file CAD.cpp.

References GiNaCRA::UnivariatePolynomialSet::makePrimitive(), and GiNaCRA::UnivariatePolynomialSet::removeNumbers().

Referenced by addPolynomials(), and CAD().

const vector<vector<UnivariatePolynomial> > GiNaCRA::CAD::eliminationSets ( ) [inline]

Definition at line 768 of file CAD.h.

References mEliminationSets.

bool GiNaCRA::CAD::isComplete ( ) const [inline]

Definition at line 776 of file CAD.h.

References mIsComplete.

const bool GiNaCRA::CAD::liftCheck	(	tree< RealAlgebraicNumberPtr >::iterator	node,
		const list< RealAlgebraicNumberPtr > &	sample,
		unsigned	level,
		const list< symbol > &	variables,
		const vector< Constraint > &	constraints,
		RealAlgebraicPoint &	r
	)		throw ( invalid_argument ) `[inline, private]`

Constructs new samples in the sample tree by successive evaluation of projection polynomial coefficients and univariate sample construction until a satisfying sample is found or there is none.

Parameters:

node	of the current level (initiate with child of mSampleTreeRoot)
level	index of the current lifting level (initialize with number of variables)
sample	list of sample components in order corresponding to the variables. The sample values (and the corresponding variables) are stored in reverse order compared to the lifting order. This is crucial to meet the same variable order as for the constraints.
variables	list of variables. Note that the first variable is always the last one lifted.
constraints	conjunction of constraints for the final check of against the current constructed RealAlgebraicPoint
r	RealAlgebraicPoint which contains the satisfying sample point if the check results true

Returns:: true if from node a path in the sample tree can be constructed so that the corresponding sample satisfies the c, false otherwise.

determines whether new samples shall be constructed regardless of other flags

the current list of samples at this position in the sample tree

Definition at line 371 of file CAD.cpp.

References GiNaCRA::tree< T, tree_node_allocator >::append_child(), GiNaCRA::tree< T, tree_node_allocator >::end(), GiNaCRA::RealAlgebraicNumberFactory::equal(), GiNaCRA::SampleList::insert(), GiNaCRA::tree< T, tree_node_allocator >::insert(), GiNaCRA::RealAlgebraicNumberFactory::less(), GiNaCRA::print(), and GiNaCRA::tree< T, tree_node_allocator >::replace().

Referenced by check().

const vector<UnivariatePolynomial> GiNaCRA::CAD::polynomials ( ) [inline]

Definition at line 758 of file CAD.h.

References mEliminationSets.

void GiNaCRA::CAD::printSampleTree ( std::ostream & os = std::cout )

Prints the current sample tree to the designated output stream.

Parameters:

os	output stream (standard value is `std::cout`)

Definition at line 194 of file CAD.cpp.

References GiNaCRA::tree< T, tree_node_allocator >::begin(), GiNaCRA::tree< T, tree_node_allocator >::depth(), GiNaCRA::tree< T, tree_node_allocator >::end(), mSampleTree, and GiNaCRA::print().

const vector< RealAlgebraicPoint > GiNaCRA::CAD::samples ( ) [inline]

Generates all real algebraic points of cad cells computed so far.

Returns:: all samples computed so far

Definition at line 157 of file CAD.cpp.

References GiNaCRA::tree< T, tree_node_allocator >::begin(), GiNaCRA::tree< T, tree_node_allocator >::begin_leaf(), constructSampleAt(), GiNaCRA::RealAlgebraicPoint::dim(), GiNaCRA::tree< T, tree_node_allocator >::end_leaf(), GiNaCRA::tree< T, tree_node_allocator >::head, mSampleTree, and mVariables.

Referenced by check(), and samples().

const SampleList GiNaCRA::CAD::samples	(	const list< RealAlgebraicNumberPtr > &	roots,
		SampleList &	currentSamples
	)		throw ( invalid_argument ) `[static]`

Constructs the samples at the base level of a CAD construction, provided a set of prevailing samples.

This method only returns samples which are new, i.e. not contained in currentSamples.

Parameters:

roots	list of real roots
currentSamples	samples already present where the new samples shall be integrated

Returns:: a set of sample points for the given univariate polynomial sorted in ascending order.

Runtime complexity:: linear in roots.size()

Situation: One, next or previous, has to be a root (assumption) or we meet one of the outmost positions. --------|-------------------|-----------------|--- previous insertValue.first next (root?) (root) (root?)

Definition at line 591 of file CAD.cpp.

References GiNaCRA::SampleList::insert(), and GiNaC::ZERO().

const SampleList GiNaCRA::CAD::samples	(	const list< RationalUnivariatePolynomial > &	polynomials,
		SampleList &	currentSamples
	)		throw ( invalid_argument ) `[static]`

Generates a list of sample points for a list of rational univariate polynomials.

It uses Sturm sequences to generate isolating intervals of the roots and adds numeric sample points of the non-root cells in between. The return format is pointers to real algebraic numbers.

Parameters:

polynomials	rational univariate polynomials
currentSamples	samples already present where the new samples shall be integrated

Runtime complexity:: linear in the number of common roots of polynomials plus the accumulated complexities of RealAlgebraicNumberFactory::realRoots calls.

Returns:: a list of pointers to real algebraic numbers

Definition at line 344 of file CAD.cpp.

References GiNaCRA::RealAlgebraicNumberFactory::realRoots(), and samples().

const SampleList GiNaCRA::CAD::samples	(	const RationalUnivariatePolynomial &	p,
		SampleList &	currentSamples,
		CADSettings	settings = `CADSettings::getSettings()`
	)		throw ( invalid_argument ) `[static]`

Constructs the samples at the base level of a CAD construction.

Parameters:

p	rational univariate polynomial
currentSamples	samples already present where the new samples shall be integrated. Each new sample is automatically inserted in this list.
settings	a setting type for a collection of CAD settings (standard option is the standard option of CADSettings::getSettings( ))

Returns:: a list of sample points for the given univariate polynomial

Runtime complexity:: linear in the number of roots of p plus the complexity of RealAlgebraicNumberFactory::realRoots( p )

Definition at line 234 of file CAD.cpp.

References GiNaCRA::RealAlgebraicNumberFactory::realRoots(), and samples().

const SampleList GiNaCRA::CAD::samples	(	const UnivariatePolynomial &	p,
		const list< RealAlgebraicNumberPtr > &	sample,
		const list< symbol > &	variables,
		SampleList &	currentSamples,
		CADSettings	settings = `CADSettings::getSettings()`
	)		throw ( invalid_argument ) `[static]`

Constructs the samples for p given the sample values sample with their corresponding variables for the coefficient polynomials.

Parameters:

p	univariate polynomial with coefficients in the given variables. `p` is univariate in a variable not contained in `variables`.
sample	list of sample components in order corresponding to the variables
variables	variables of the coefficients of p
currentSamples	samples already present where the new samples shall be integrated. Each new sample is automatically inserted in this list.
settings	a setting type for a collection of CAD settings (standard option is the standard option of CADSettings::getSettings( ))

Returns:: a set of sample points for the given univariate polynomial

Runtime complexity:: linear in the number of roots of p plus the complexity of RealAlgebraicNumberFactory::realRoots( p )

Definition at line 242 of file CAD.cpp.

References GiNaCRA::RealAlgebraicNumberFactory::realRootsEval().

const bool GiNaCRA::CAD::satisfys	(	const RealAlgebraicPoint &	r,
		const vector< Constraint > &	constraints
	)		const `[inline, private]`

Returns the truth value as to whether the conjunction of the constraintsis satisfied by the real algebraic point r.

Parameters:

r
constraints

Returns:: the truth value as to whether the conjunction of the constraints is satisfied by the real algebraic point

Definition at line 572 of file CAD.cpp.

Referenced by check().

const UnivariatePolynomialSet GiNaCRA::CAD::truncation ( const UnivariatePolynomial & P ) [static, private]

Generates the set of truncations of the polynomial.

The Algorithm is based on the notation from "Algorithms in Real Algebraic Geometry" - Saugata Basu, Richard Pollack, Marie-Francoise Roy see page 21-22

Parameters:

P	The polynomial

Runtime complexity:: O ( deg(P) )

Returns:: The set of truncations

Definition at line 711 of file CAD.cpp.

References GiNaCRA::UnivariatePolynomialSet::insert(), GiNaCRA::UnivariatePolynomial::isConstant(), and GiNaCRA::UnivariatePolynomial::trunc().

Referenced by elimination(), and truncation().

const UnivariatePolynomialSet GiNaCRA::CAD::truncation ( const UnivariatePolynomialSet & P ) [static, private]

Generates the set of truncations of the polynomial set.

The Algorithm is based on the notation from "Algorithms in Real Algebraic Geometry" - Saugata Basu, Richard Pollack, Marie-Francoise Roy see page 21-22

Parameters: