smtrat::mcsat::fm::ConflictGenerator< Comparator > Struct Template Reference

#include <ConflictGenerator.h>

Collaboration diagram for smtrat::mcsat::fm::ConflictGenerator< Comparator >:

Public Member Functions
	ConflictGenerator (const std::vector< ConstraintT > &bounds, const Model &m, carl::Variable v)
template<typename Callback >
void	generateExplanation (Callback &&callback)

Private Member Functions
ConstraintT	sideCondition (const Bound &b)
ConstraintT	sideConditionLoUp (const Bound &b)
FormulasT	conflictLowerAndUpperBound (const Bound &lower, const Bound &upper)
FormulasT	conflictEqualityAndInequality (const Bound &eq, const Bound &ineq)
FormulasT	conflictInequalitiesAndInequality (const Bound &lower, const Bound &upper, const Bound &ineq)

Private Attributes
const std::vector< ConstraintT > &	mBounds
const Model &	mModel
carl::Variable	mVariable
Comparator	comparator

Detailed Description

template<class Comparator>
struct smtrat::mcsat::fm::ConflictGenerator< Comparator >

Definition at line 66 of file ConflictGenerator.h.

Constructor & Destructor Documentation

ConflictGenerator()

template<class Comparator >

smtrat::mcsat::fm::ConflictGenerator< Comparator >::ConflictGenerator ( const std::vector< ConstraintT > &  bounds, const Model &  m, carl::Variable  v  )

inline

Definition at line 79 of file ConflictGenerator.h.

Member Function Documentation

conflictEqualityAndInequality()

template<class Comparator >

FormulasT smtrat::mcsat::fm::ConflictGenerator< Comparator >::conflictEqualityAndInequality ( const Bound &  eq, const Bound &  ineq  )

inlineprivate

Definition at line 109 of file ConflictGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

conflictInequalitiesAndInequality()

template<class Comparator >

FormulasT smtrat::mcsat::fm::ConflictGenerator< Comparator >::conflictInequalitiesAndInequality ( const Bound &  lower, const Bound &  upper, const Bound &  ineq  )

inlineprivate

Definition at line 121 of file ConflictGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

conflictLowerAndUpperBound()

template<class Comparator >

FormulasT smtrat::mcsat::fm::ConflictGenerator< Comparator >::conflictLowerAndUpperBound ( const Bound &  lower, const Bound &  upper  )

inlineprivate

Definition at line 94 of file ConflictGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

generateExplanation()

template<class Comparator >

template<typename Callback >

void smtrat::mcsat::fm::ConflictGenerator< Comparator >::generateExplanation ( Callback &&  callback )

inline

Definition at line 139 of file ConflictGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

sideCondition()

template<class Comparator >

ConstraintT smtrat::mcsat::fm::ConflictGenerator< Comparator >::sideCondition ( const Bound &  b )

inlineprivate

Definition at line 82 of file ConflictGenerator.h.

Here is the caller graph for this function:

sideConditionLoUp()

template<class Comparator >

ConstraintT smtrat::mcsat::fm::ConflictGenerator< Comparator >::sideConditionLoUp ( const Bound &  b )

inlineprivate

Definition at line 88 of file ConflictGenerator.h.

Here is the caller graph for this function:

Field Documentation

comparator

template<class Comparator >

Comparator smtrat::mcsat::fm::ConflictGenerator< Comparator >::comparator

private

Definition at line 76 of file ConflictGenerator.h.

mBounds

template<class Comparator >

const std::vector<ConstraintT>& smtrat::mcsat::fm::ConflictGenerator< Comparator >::mBounds

private

Definition at line 72 of file ConflictGenerator.h.

mModel

template<class Comparator >

const Model& smtrat::mcsat::fm::ConflictGenerator< Comparator >::mModel

private

Definition at line 73 of file ConflictGenerator.h.

mVariable

template<class Comparator >

carl::Variable smtrat::mcsat::fm::ConflictGenerator< Comparator >::mVariable

private

Definition at line 74 of file ConflictGenerator.h.

---

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

• smtrat-mcsat/explanations/fm/ConflictGenerator.h