LiteralWithIndexLists

gapt.cutintro.LiteralWithIndexLists

class LiteralWithIndexLists(val literal: Formula, val leafIndexList: List[LeafIndex], val numberOfDNTAs: Int, val foundNonEmptyPList: Boolean, val foundEmptyMList: Boolean)

Supposed to contain the data of a unified literal and whether it makes a non-tautological leaf of the reduced representation true

Value parameters

foundEmptyMList: Supposed to be true if there is a at least one leaf of the reduced representation and one substitution of the form (xCut->r_j,yCut->beta_j) such that the leaf becomes true
foundNonEmptyPList: Supposed to be true if there is a at least one leaf of the reduced representation and one substitution of the form (xCut->alpha,yCut->t_i(alpha)) such that the leaf becomes true
leafIndexList: Supposed to contain the data which leaf of the reduced representation becomes true for which substitution of the literal