|
cudd
3.0.0
The University of Colorado Decision Diagram Package
|
This structure holds the set of clauses for a node. More...
Data Fields | |
| DdHalfWord * | vars |
| ptruint * | phases |
| DdHalfWord | cnt |
This structure holds the set of clauses for a node.
Each clause consists of two literals. For one-literal clauses, the second literal is FALSE. Each literal is composed of a variable and a phase. A variable is a node index, and requires sizeof(DdHalfWord) bytes. The constant literals use CUDD_MAXINDEX as variable indicator. Each phase is a bit: 0 for positive phase, and 1 for negative phase. Variables and phases are stored separately for the sake of compactness. The variables are stored in an array of DdHalfWord's terminated by a sentinel (a pair of zeroes). The phases are stored in a bit vector. The cnt field holds, at the end, the number of clauses. The clauses of the set are kept sorted. For each clause, the first literal is the one of least index. So, the clause with literals +2 and -4 is stored as (+2,-4). A one-literal clause with literal +3 is stored as (+3,-CUDD_MAXINDEX). Clauses are sorted in decreasing order as follows:
That is, one first looks at the variable of the first literal, then at the phase of the first literal, then at the variable of the second literal, and finally at the phase of the second literal.
1.8.14