carl::vs Namespace Reference

Namespaces
	detail

Data Structures
class	Term
struct	zero
	A square root expression with side conditions. More...

Typedefs
template<typename Poly >
using	ConstraintConjunction = std::vector< Constraint< Poly > >
	a vector of constraints More...
template<typename Poly >
using	CaseDistinction = std::vector< ConstraintConjunction< Poly > >
	a vector of vectors of constraints More...

Enumerations
enum class	TermType { NORMAL , PLUS_EPSILON , MINUS_INFINITY , PLUS_INFINITY }

Functions
template<typename Poly >
bool	simplify_inplace (CaseDistinction< Poly > &cases)
	Simplifies the case distinction in place. More...
template<typename Poly >
std::optional< CaseDistinction< Poly > >	substitute (const Constraint< Poly > &cons, const Variable var, const Term< Poly > &term)
	Applies a substitution to a constraint. More...
template<typename Poly >
static std::optional< std::variant< CaseDistinction< Poly >, VariableComparison< Poly > > >	substitute (const VariableComparison< Poly > &varcomp, const Variable var, const Term< Poly > &term)
	Applies a substitution to a variable comparison. More...
template<class Poly >
std::ostream &	operator<< (std::ostream &os, const Term< Poly > &s)
template<typename Poly >
std::ostream &	operator<< (std::ostream &out, const zero< Poly > &z)
template<typename Poly >
static bool	gather_zeros (const Constraint< Poly > &constraint, const Variable &eliminationVar, std::vector< zero< Poly >> &results)
	Gathers zeros with side conditions from the given constraint in the given variable. More...
template<typename Poly >
static bool	gather_zeros (const VariableComparison< Poly > &varcomp, const Variable &eliminationVar, std::vector< zero< Poly >> &results)

Typedef Documentation

CaseDistinction

template<typename Poly >

using carl::vs::CaseDistinction = typedef std::vector<ConstraintConjunction<Poly> >

a vector of vectors of constraints

Definition at line 29 of file substitute.h.

ConstraintConjunction

template<typename Poly >

using carl::vs::ConstraintConjunction = typedef std::vector<Constraint<Poly> >

a vector of constraints

Definition at line 26 of file substitute.h.

Enumeration Type Documentation

TermType

enum carl::vs::TermType

strong

Enumerator
NORMAL
PLUS_EPSILON
MINUS_INFINITY
PLUS_INFINITY

Definition at line 7 of file term.h.

Function Documentation

gather_zeros() [1/2]

template<typename Poly >

static bool carl::vs::gather_zeros ( const Constraint< Poly > &  constraint, const Variable &  eliminationVar, std::vector< zero< Poly >> &  results  )

static

Gathers zeros with side conditions from the given constraint in the given variable.

Definition at line 27 of file zeros.h.

Here is the call graph for this function:

Here is the caller graph for this function:

gather_zeros() [2/2]

template<typename Poly >

static bool carl::vs::gather_zeros ( const VariableComparison< Poly > &  varcomp, const Variable &  eliminationVar, std::vector< zero< Poly >> &  results  )

static

Definition at line 139 of file zeros.h.

Here is the call graph for this function:

operator<<() [1/2]

template<class Poly >

std::ostream& carl::vs::operator<<	(	std::ostream &	os,
		const Term< Poly > &	s
	)

operator<<() [2/2]

template<typename Poly >

std::ostream& carl::vs::operator<<	(	std::ostream &	out,
		const zero< Poly > &	z
	)

Definition at line 18 of file zeros.h.

simplify_inplace()

template<typename Poly >

bool carl::vs::simplify_inplace ( CaseDistinction< Poly > &  cases )

inline

Simplifies the case distinction in place.

Template Parameters

Poly	Polynomial type.

Parameters

cases

Case distiction to simplify.

Returns

true On success.

false Fail, cases is now invalid.

Definition at line 360 of file substitute.h.

Here is the call graph for this function:

Here is the caller graph for this function:

substitute() [1/2]

template<typename Poly >

std::optional<CaseDistinction<Poly> > carl::vs::substitute ( const Constraint< Poly > &  cons, const Variable  var, const Term< Poly > &  term  )

inline

Applies a substitution to a constraint.

Parameters

cons	The constraint to substitute in.
subs	The substitution to apply.

Returns

std::nullopt, if the upper limit in the number of combinations in the result of the substitution is exceeded. Note, that this hinders a combinatorial blow up. Thr substitution result, otherwise.

Definition at line 375 of file substitute.h.

Here is the call graph for this function:

Here is the caller graph for this function:

substitute() [2/2]

template<typename Poly >

static std::optional<std::variant<CaseDistinction<Poly>, VariableComparison<Poly> > > carl::vs::substitute ( const VariableComparison< Poly > &  varcomp, const Variable  var, const Term< Poly > &  term  )

static

Applies a substitution to a variable comparison.

Parameters

varcomp	The variable comparison to substitute in.
subs	The substitution to apply.

Returns

std::nullopt, if the upper limit in the number of combinations in the result of the substitution is exceeded or the substitution cannot be applied. Note, that this hinders a combinatorial blow up. Thr substitution result, otherwise.

Definition at line 401 of file substitute.h.

Here is the call graph for this function: