smtrat::mcsat::vs::ExplanationGenerator< Settings > Class Template Reference

#include <ExplanationGenerator.h>

Collaboration diagram for smtrat::mcsat::vs::ExplanationGenerator< Settings >:

Public Member Functions
	ExplanationGenerator (const std::vector< FormulaT > &constraints, const std::vector< carl::Variable > &variableOrdering, const carl::Variable &targetVar, const Model &model)
std::optional< mcsat::Explanation >	getExplanation () const

Private Member Functions
std::pair< std::vector< carl::Variable >::const_iterator, std::vector< carl::Variable >::const_iterator >	getUnassignedVariables () const
std::optional< FormulaT >	eliminateVariable (const FormulaT &inputFormula, const carl::Variable &var) const
std::optional< FormulaT >	eliminateVariables () const

Private Attributes
const std::vector< FormulaT > &	mConstraints
const std::vector< carl::Variable > &	mVariableOrdering
const carl::Variable &	mTargetVar
const Model &	mModel

Detailed Description

template<class Settings>
class smtrat::mcsat::vs::ExplanationGenerator< Settings >

Definition at line 18 of file ExplanationGenerator.h.

Constructor & Destructor Documentation

ExplanationGenerator()

template<class Settings >

smtrat::mcsat::vs::ExplanationGenerator< Settings >::ExplanationGenerator ( const std::vector< FormulaT > &  constraints, const std::vector< carl::Variable > &  variableOrdering, const carl::Variable &  targetVar, const Model &  model  )

inline

Definition at line 26 of file ExplanationGenerator.h.

Member Function Documentation

eliminateVariable()

template<class Settings >

std::optional<FormulaT> smtrat::mcsat::vs::ExplanationGenerator< Settings >::eliminateVariable ( const FormulaT &  inputFormula, const carl::Variable &  var  ) const

inlineprivate

Definition at line 56 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

eliminateVariables()

template<class Settings >

std::optional<FormulaT> smtrat::mcsat::vs::ExplanationGenerator< Settings >::eliminateVariables ( ) const

inlineprivate

Definition at line 122 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

getExplanation()

template<class Settings >

std::optional<mcsat::Explanation> smtrat::mcsat::vs::ExplanationGenerator< Settings >::getExplanation ( ) const

inline

Definition at line 150 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

getUnassignedVariables()

template<class Settings >

std::pair<std::vector<carl::Variable>::const_iterator, std::vector<carl::Variable>::const_iterator> smtrat::mcsat::vs::ExplanationGenerator< Settings >::getUnassignedVariables ( ) const

inlineprivate

Definition at line 35 of file ExplanationGenerator.h.

Here is the call graph for this function:

Here is the caller graph for this function:

Field Documentation

mConstraints

template<class Settings >

const std::vector<FormulaT>& smtrat::mcsat::vs::ExplanationGenerator< Settings >::mConstraints

private

Definition at line 20 of file ExplanationGenerator.h.

mModel

template<class Settings >

const Model& smtrat::mcsat::vs::ExplanationGenerator< Settings >::mModel

private

Definition at line 23 of file ExplanationGenerator.h.

mTargetVar

template<class Settings >

const carl::Variable& smtrat::mcsat::vs::ExplanationGenerator< Settings >::mTargetVar

private

Definition at line 22 of file ExplanationGenerator.h.

mVariableOrdering

template<class Settings >

const std::vector<carl::Variable>& smtrat::mcsat::vs::ExplanationGenerator< Settings >::mVariableOrdering

private

Definition at line 21 of file ExplanationGenerator.h.

---

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

• smtrat-mcsat/explanations/vs/ExplanationGenerator.h