smtrat::icp Namespace Reference

Data Structures
class	ContractionCandidate
struct	contractionCandidateComp
class	ContractionCandidateManager
class	HistoryNode
class	IcpVariable
struct	icpVariableComp

Typedefs
template<template< typename > class Operator>
using	Contractor = carl::Contraction< Operator, Poly >
typedef LRAModule< LRASettings1 >::LRAVariable	LRAVariable
typedef std::set< const IcpVariable *, icpVariableComp >	set_icpVariable

Enumerations
enum class	Updated { LEFT , RIGHT , BOTH , NONE }

Functions
std::vector< Poly >	getNonlinearMonomials (const Poly &_expr)
	Obtains the non-linear monomials of the given polynomial. More...
std::pair< ConstraintT, ConstraintT >	intervalToConstraint (const Poly &_lhs, const smtrat::DoubleInterval _interval)
	Creates a new constraint from an existing interval. More...
bool	intervalBoxContainsEmptyInterval (const EvalDoubleIntervalMap &_intervals)
	Checks mIntervals if it contains an empty interval. More...
const LRAModule< LRASettings1 >::LRAVariable *	getOriginalLraVar (carl::Variable::Arg _var, const LRAModule< LRASettings1 > &_lra)

Typedef Documentation

Contractor

template<template< typename > class Operator>

using smtrat::icp::Contractor = typedef carl::Contraction<Operator, Poly>

Definition at line 24 of file ContractionCandidate.h.

LRAVariable

typedef LRAModule<LRASettings1>::LRAVariable smtrat::icp::LRAVariable

Definition at line 33 of file IcpVariable.h.

set_icpVariable

typedef std::set<const IcpVariable*, icpVariableComp> smtrat::icp::set_icpVariable

Definition at line 336 of file IcpVariable.h.

Enumeration Type Documentation

Updated

enum smtrat::icp::Updated

strong

Enumerator
LEFT
RIGHT
BOTH
NONE

Definition at line 22 of file IcpVariable.h.

Function Documentation

getNonlinearMonomials()

std::vector< Poly > smtrat::icp::getNonlinearMonomials

(

const Poly &

_expr

)

Obtains the non-linear monomials of the given polynomial.

Parameters

_expr

The polynomial to obtain the non-linear monomials for.

Returns

The non-linear monomials.

Definition at line 17 of file utils.cpp.

getOriginalLraVar()

const LRAModule< LRASettings1 >::LRAVariable * smtrat::icp::getOriginalLraVar	(	carl::Variable::Arg	_var,
		const LRAModule< LRASettings1 > &	_lra
	)

Definition at line 92 of file utils.cpp.

Here is the call graph for this function:

intervalBoxContainsEmptyInterval()

bool smtrat::icp::intervalBoxContainsEmptyInterval

(

const EvalDoubleIntervalMap &

_intervals

)

Checks mIntervals if it contains an empty interval.

Returns

Definition at line 82 of file utils.cpp.

intervalToConstraint()

std::pair< ConstraintT, ConstraintT > smtrat::icp::intervalToConstraint	(	const Poly &	_lhs,
		const smtrat::DoubleInterval	_interval
	)

Creates a new constraint from an existing interval.

Parameters

_interval

Returns

pair <lowerBoundConstraint*, upperBoundConstraint*>

Definition at line 37 of file utils.cpp.