Given a PU allocation, the SAT constraints (without switching Dup nodes) yields a 2SAT problem which is described by the following data type that offers facts for the node and buffer ordering as well as constraints which are equivalences between the latter.
Union case | Description |
Full Usage:
BufOrd(string, string)
Parameters:
string
Item2 : string
|
|
Full Usage:
Equat(int * int, string * string)
Parameters:
int * int
Item2 : string * string
|
|
Full Usage:
NodOrd(int, int)
Parameters:
int
Item2 : int
|
|