smtrat::mcsat::nlsat::helper Namespace Reference

Functions
FormulaT	buildFormulaFromVC (VariableComparisonT &&vc)
	Construct a formula representing a variable comparison. More...
template<typename MVRootParams >
FormulaT	buildEquality (carl::Variable var, const MVRootParams &mvp)
	Construct an atomic formula representing a variable being equal to the given multivariate root. More...
template<typename MVRootParams >
FormulaT	buildBelow (carl::Variable var, const MVRootParams &mvp)
	Construct an atomic formula representing a variable being less than the given multivariate root. More...
template<typename MVRootParams >
FormulaT	buildAbove (carl::Variable var, const MVRootParams &mvp)
	Construct an atomic formula representing a variable being greater than the given multivariate root. More...
std::set< ConstraintT >	convertToConstraints (std::vector< FormulaT > constraintAtoms)
	Transform constraints represented as atomic formualas into the easier to use objects of the Constraint class. More...

Function Documentation

buildAbove()

template<typename MVRootParams >

FormulaT smtrat::mcsat::nlsat::helper::buildAbove	(	carl::Variable	var,
		const MVRootParams &	mvp
	)

Construct an atomic formula representing a variable being greater than the given multivariate root.

"v > root(..)"

Definition at line 48 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

buildBelow()

template<typename MVRootParams >

FormulaT smtrat::mcsat::nlsat::helper::buildBelow	(	carl::Variable	var,
		const MVRootParams &	mvp
	)

Construct an atomic formula representing a variable being less than the given multivariate root.

"v < root(..)"

Definition at line 40 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

buildEquality()

template<typename MVRootParams >

FormulaT smtrat::mcsat::nlsat::helper::buildEquality	(	carl::Variable	var,
		const MVRootParams &	mvp
	)

Construct an atomic formula representing a variable being equal to the given multivariate root.

"v = root(..)"

Definition at line 32 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

buildFormulaFromVC()

FormulaT smtrat::mcsat::nlsat::helper::buildFormulaFromVC ( VariableComparisonT &&  vc )

inline

Construct a formula representing a variable comparison.

Simplify to a regular constraint if possible.

Definition at line 19 of file ExplanationGenerator.h.

Here is the caller graph for this function:

convertToConstraints()

std::set<ConstraintT> smtrat::mcsat::nlsat::helper::convertToConstraints ( std::vector< FormulaT >  constraintAtoms )

inline

Transform constraints represented as atomic formualas into the easier to use objects of the Constraint class.

Definition at line 58 of file ExplanationGenerator.h.

Here is the caller graph for this function: