smtrat::SATModule< Settings >::VarData Struct Reference

Stores information about a Minisat variable. More...

Collaboration diagram for smtrat::SATModule< Settings >::VarData:

Public Member Functions
	VarData (Minisat::CRef _reason, int _level, int _trailIndex)

Data Fields
Minisat::CRef	reason
	A reference to the clause, which implied the current assignment of this variable. More...
int	level
	The level in which the variable has been assigned, if it is not unassigned. More...
int	mTrailIndex
	The index in the trail. More...
int	mExpPos
	Position of explanation. More...

Detailed Description

template<class Settings>
struct smtrat::SATModule< Settings >::VarData

Stores information about a Minisat variable.

Definition at line 76 of file SATModule.h.

Constructor & Destructor Documentation

VarData()

template<class Settings >

smtrat::SATModule< Settings >::VarData::VarData ( Minisat::CRef  _reason, int  _level, int  _trailIndex  )

inline

Definition at line 94 of file SATModule.h.

Field Documentation

level

template<class Settings >

int smtrat::SATModule< Settings >::VarData::level

The level in which the variable has been assigned, if it is not unassigned.

Definition at line 86 of file SATModule.h.

mExpPos

template<class Settings >

int smtrat::SATModule< Settings >::VarData::mExpPos

Position of explanation.

Definition at line 92 of file SATModule.h.

mTrailIndex

template<class Settings >

int smtrat::SATModule< Settings >::VarData::mTrailIndex

The index in the trail.

Definition at line 89 of file SATModule.h.

reason

template<class Settings >

Minisat::CRef smtrat::SATModule< Settings >::VarData::reason

A reference to the clause, which implied the current assignment of this variable.

It is not defined, if the assignment of the variable follows from a clause of size 0 or if the variable is unassigned.

Definition at line 83 of file SATModule.h.

---

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

• smtrat-modules/SATModule/SATModule.h