smtrat::Module::Lemma Struct Reference

#include <Module.h>

Public Member Functions
	Lemma (const FormulaT &_lemma, const LemmaType &_lemmaType, const FormulaT &_preferredFormula)
	Constructor. More...

Data Fields
FormulaT	mLemma
	The lemma to learn. More...
LemmaType	mLemmaType
	The type of the lemma. More...
FormulaT	mPreferredFormula
	The formula within the lemma, which should be assigned to true in the next decision. More...

Detailed Description

Definition at line 125 of file Module.h.

Constructor & Destructor Documentation

Lemma()

smtrat::Module::Lemma::Lemma ( const FormulaT &  _lemma, const LemmaType &  _lemmaType, const FormulaT &  _preferredFormula  )

inline

Constructor.

Parameters

_lemma	The lemma to learn.
_lemmaType	The type of the lemma.
_preferredFormula	The formula within the lemma, which should be assigned to true in the next decision.

Definition at line 140 of file Module.h.

Field Documentation

mLemma

FormulaT smtrat::Module::Lemma::mLemma

The lemma to learn.

Definition at line 128 of file Module.h.

mLemmaType

LemmaType smtrat::Module::Lemma::mLemmaType

The type of the lemma.

Definition at line 130 of file Module.h.

mPreferredFormula

FormulaT smtrat::Module::Lemma::mPreferredFormula

The formula within the lemma, which should be assigned to true in the next decision.

Definition at line 132 of file Module.h.

---

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

• smtrat-solver/Module.h