StructuralComparisonDataStructure:
CEDAR
DEFINITIONS =
BEGIN
LORA: TYPE = LIST OF REF ANY;
LOLORA: TYPE = LIST OF LORA;
ROPE: TYPE = Rope.ROPE;
RopeList: TYPE = LIST OF ROPE;
SymbolTable: TYPE = HashTable.Table;
Assertions: TYPE = Asserting.Assertions;
ColorTable: TYPE = CardHashTableThreaded.Table;
GraphID: TYPE = {A, B, Unspecified};
RealGraphID: TYPE = GraphID[A .. B];
OtherGraph: ARRAY RealGraphID OF RealGraphID = [A: B, B: A];
graphIDToRope: GraphDescriptions;
GraphDescriptions: TYPE ~ ARRAY GraphID OF ROPE;
RealGraphDescriptions: TYPE ~ ARRAY RealGraphID OF ROPE;
Color: TYPE = CARD;
noColor: Color = LAST[Color];
someColor: Color = 87654321H;
FilterColor:
PROC [color: Color]
RETURNS [filtered: Color] =
INLINE {
filtered ← IF color # noColor THEN color ELSE someColor};
VertexClass: TYPE = {net, cell};
OtherClass: ARRAY VertexClass OF VertexClass = [net: cell, cell: net];
CellType: TYPE = REF CellTypeRep;
CellTypeRep:
TYPE =
RECORD [
name: ROPE ← NIL,
color: Color ← noColor,
ports: PortS ← NIL,
internalsKnown, destroyed: BOOL ← FALSE,
firstPart: Vertex ← NIL,
size: NAT ← 0, --number of parts
mirror: Vertex ←
NIL,
--the outside world, as seen from the inside
AM1: A mirror is not entered in its parent's parts list.
AM2: A mirror is not linked in as an instance of its type.
netCount, cellCount:
NAT ← 0,
Counts are redundant with parts.
otherPublic, otherPrivate: Assertions ← NIL];
transistorTolerancesKey: READONLY ATOM;
defaultTransistorTolerances: READONLY TransistorTolerances;
TransistorTolerances: TYPE ~ REF TransistorTolerancesPrivate;
TransistorTolerancesPrivate: TYPE ~ ARRAY TransistorDim OF Tolerance;
TransistorDim: TYPE ~ {length, width};
Tolerance: TYPE ~ RECORD [min, max: REAL--a/b--];
TransistorDimName: READONLY ARRAY TransistorDim OF ROPE;
IsMirror: PROC [v: Vertex] RETURNS [is: BOOL] = INLINE {is ← v.isMirror};
EnumerateParts:
PROC [ct: CellType,
Consume:
PROC [Vertex], mirrorToo:
BOOL] =
INLINE {
next: Vertex;
FOR v: Vertex ← ct.firstPart, next
WHILE v #
NIL
DO
next ← v.nextPart;
IF NOT v.deleted THEN Consume[v]
ENDLOOP;
IF mirrorToo THEN Consume[ct.mirror];
};
PortS: TYPE = REF PortSeq;
PortSeq: TYPE = RECORD [length: PortIndex, ports: SEQUENCE size: PortIndex OF Port];
PortIndex: TYPE = NAT;
NullPortIndex: PortIndex = LAST[PortIndex];
Port: TYPE = RECORD [name: ROPE ← NIL, net: Vertex ← NIL, other: Assertions ← NIL, color: Color ← noColor];
VertexList: TYPE = LIST OF Vertex;
Vertex: TYPE = REF VertexRep;
VertexRep:
PRIVATE
TYPE =
RECORD [
name: ROPE,
QNext: Vertex ← notInQ,
nextPart: Vertex ← NIL,
colorNext, equiv: Vertex ← NIL,
firstEdge, lastEdge: Edge ← NIL,
type: CellType ← NIL,
other: Assertions ← NIL,
oldColor, curColor: Color ← noColor,
better: Vertex ← NIL,
graph: GraphID ← Unspecified,
class: VertexClass,
unique, suspect, isMirror, deleted: BOOL ← FALSE];
Edge: TYPE = REF EdgeRep;
EdgeRep:
TYPE =
RECORD [
sides: ARRAY VertexClass OF RECORD [v: Vertex, next, prev: Edge],
color: Color];
notInQ: Vertex --don't look:-- = NIL --you looked!--;
endOfQ: Vertex;
ColorData: TYPE = REF ColorDataPrivate;
ColorDataPrivate:
TYPE =
RECORD [
color: Color,
nextColor: ColorData ← NIL,
firstVertex: Vertex ← NIL,
count: ARRAY RealGraphID OF CARDINAL ← [0, 0],
newColor: Color ← noColor,
suspect, multicolored: BOOL ← FALSE
];
newColor and multicolored are indexed by oldColor; the rest by curColor.
EnumerateEdges:
PROC [v: Vertex,
Consume:
PROC [Color, Vertex], includeMirror:
BOOL] =
INLINE {
FOR e: Edge ← v.firstEdge, e.sides[v.class].next
WHILE e #
NIL
DO
w: Vertex = e.sides[OtherClass[v.class]].v;
IF e.sides[v.class].v # v THEN ERROR;
IF includeMirror OR NOT IsMirror[w] THEN Consume[e.color, w];
ENDLOOP;
};
EnumerateFullEdges:
PROC [v: Vertex,
Consume:
PROC [e: Edge], includeMirror:
BOOL] =
INLINE {
nextEdge: Edge ← v.firstEdge;
FOR e: Edge ← v.firstEdge, nextEdge
WHILE e #
NIL
DO
w: Vertex = e.sides[OtherClass[v.class]].v;
IF e.sides[v.class].v # v THEN ERROR;
nextEdge ← e.sides[v.class].next;
IF includeMirror OR NOT IsMirror[w] THEN Consume[e];
ENDLOOP;
};
InitialColor: PROC [v: Vertex] RETURNS [Color];
VName: PROC [v: Vertex] RETURNS [r: ROPE] = INLINE {r ← v.name};
VDead: PROC [v: Vertex] RETURNS [ded: BOOL] = INLINE {ded ← v.class = cell AND v.type.destroyed};
OldColor: PROC [v: Vertex] RETURNS [c: Color] = INLINE {c ← v.oldColor};
SetOldColor: PROC [v: Vertex, c: Color] = INLINE {v.oldColor ← c};
CurColor: PROC [v: Vertex] RETURNS [c: Color] = INLINE {c ← v.curColor};
SetCurColor: PROC [v: Vertex, c: Color] = INLINE {v.curColor ← c};
GetGraph: PROC [v: Vertex] RETURNS [g: GraphID] = INLINE {g ← v.graph};
SetGraph: PROC [v: Vertex, g: GraphID] = INLINE {v.graph ← g};
GetUnique: PROC [v: Vertex] RETURNS [b: BOOL] = INLINE {b ← v.unique};
SetUnique: PROC [v: Vertex, b: BOOL] = INLINE {v.unique ← b};
GetSuspect: PROC [v: Vertex] RETURNS [b: BOOL] = INLINE {b ← v.suspect};
SetSuspect: PROC [v: Vertex, b: BOOL] = INLINE {v.suspect ← b};
GetQNext: PROC [v: Vertex] RETURNS [w: Vertex] = INLINE {w ← v.QNext};
SetQNext: PROC [v: Vertex, w: Vertex] = INLINE {v.QNext ← w};
GetColorNext: PROC [v: Vertex] RETURNS [w: Vertex] = INLINE {w ← v.colorNext};
SetColorNext: PROC [v: Vertex, w: Vertex] = INLINE {v.colorNext ← w};
GetEquiv: PROC [v: Vertex] RETURNS [w: Vertex] = INLINE {w ← v.equiv};
SetEquiv: PROC [v: Vertex, w: Vertex] = INLINE {v.equiv ← w};
END.