BEGIN
T Y P E S
RTSmSetRange: TYPE = INT [0..16);
RTSmSet: TYPE = PACKED ARRAY RTSmSetRange OF BOOLEAN ← ALL[FALSE];
RTMdSetRange: TYPE = INT [0..64);
RTMdSet:
TYPE =
PACKED
ARRAY RTMdSetRange
OF
BOOLEAN ←
ALL[
FALSE];
RTLgSetRange: TYPE = INT [0..256);
RTLgSet: TYPE = PACKED ARRAY RTLgSetRange OF BOOLEAN ← ALL[FALSE];
C O N S T A N T S A N D P R O C S
RTSmSetEmpty: RTSmSet = ALL[FALSE];
RTSmSetGenerateElement:
PROCEDURE [i: INT]
RETURNS [RTSmSet] = INLINE {s: RTSmSet; s[i] ← TRUE; RETURN[s]};
RTSmSetGenerateInterval:
PROCEDURE [i, j: INT]
RETURNS [RTSmSet] = INLINE
BEGIN
s: RTSmSet;
k: INT;
FOR k IN [i..j] DO s[k] ← TRUE ENDLOOP;
RETURN[s]
END;
RTSmSetAddElement:
PROCEDURE [s: RTSmSet, i: INT]
RETURNS [RTSmSet] = INLINE {s[i] ← TRUE; RETURN[s]};
RTSmSetAddInterval:
PROCEDURE [s: RTSmSet, i, j: INT]
RETURNS [RTSmSet] = INLINE
BEGIN k: INT; FOR k IN [i..j] DO s[k] ← TRUE ENDLOOP; RETURN[s] END;
RTSmSetUnion:
PROCEDURE [x, y: RTSmSet]
RETURNS [RTSmSet] =
TRUSTED INLINE {RETURN[LOOPHOLE[PrincOpsUtils.BITOR[LOOPHOLE[x],LOOPHOLE[y]]]]};
RTSmSetIntersection:
PROCEDURE [x, y: RTSmSet]
RETURNS [RTSmSet] =
TRUSTED INLINE {RETURN[LOOPHOLE[PrincOpsUtils.BITAND[LOOPHOLE[x],LOOPHOLE[y]]]]};
RTSmSetDifference:
PROCEDURE [x, y: RTSmSet]
RETURNS [RTSmSet] = TRUSTED INLINE {
RETURN[LOOPHOLE[PrincOpsUtils.BITAND[LOOPHOLE[x], PrincOpsUtils.BITNOT[LOOPHOLE[y]]]]]};
RTSmSetIsSubset:
PROCEDURE [x, y: RTSmSet]
RETURNS [BOOLEAN] = INLINE {RETURN[y = RTSmSetUnion[y, x]]};
RTSmSetIsSuperset:
PROCEDURE [x, y: RTSmSet]
RETURNS [BOOLEAN] = INLINE {RETURN[x = RTSmSetUnion[y, x]]};
RTSmSetIsSame:
PROCEDURE [x, y: RTSmSet]
RETURNS [BOOLEAN] =
INLINE {RETURN[LOOPHOLE[y, CARDINAL] = LOOPHOLE[x, CARDINAL]]};
RTSmSetIsDifferent:
PROCEDURE [x, y: RTSmSet]
RETURNS [BOOLEAN] = INLINE {
RETURN[LOOPHOLE[y, CARDINAL] # LOOPHOLE[x, CARDINAL]]};
RTSmSetCARD:
PROCEDURE [x: RTSmSet]
RETURNS [INT] =
TRUSTED INLINE
BEGIN OPEN PrincOpsUtils;
fast bit-counter that adds a pair of eight one-bit registers to
yield eight two-bit sums, then breaks those into a pair of four two-bit registers which
are combined to yield four four-bit sums, and so on.
c: CARDINAL ← BITAND[LOOPHOLE[x], 52525B] + BITAND[BITSHIFT[LOOPHOLE[x], -1], 52525B];
c ← BITAND[c, 31463B] + BITAND[BITSHIFT[c, -2], 31463B];
c ← BITAND[c, 7417B] + BITAND[BITSHIFT[c, -4], 7417B];
RETURN[BITAND[c, 377B] + BITAND[BITSHIFT[c, -8], 377B]];
END;
RTSmSetContains:
PROCEDURE [s: RTSmSet, e: INT]
RETURNS [BOOLEAN] = INLINE {RETURN[s[e]]};
RTMdSetEmpty: RTMdSet = ALL[FALSE];
RTMdSetGenerateElement:
PROCEDURE [i: INT]
RETURNS [RTMdSet];
RTMdSetGenerateInterval:
PROCEDURE [i, j: INT]
RETURNS [RTMdSet];
RTMdSetAddElement:
PROCEDURE [i: INT, s: RTMdSet]
RETURNS [RTMdSet];
RTMdSetAddInterval:
PROCEDURE [i, j: INT, s: RTMdSet]
RETURNS [RTMdSet];
RTMdSetUnion, RTMdSetIntersection, RTMdSetDifference:
PROCEDURE [x, y: RTMdSet] RETURNS [RTMdSet];
RTMdSetIsSubset,
RTMdSetIsSame:
PROCEDURE [
x, y: RTMdSet] RETURNS [BOOLEAN];
RTMdSetIsSuperset:
PROCEDURE [x, y: RTMdSet]
RETURNS [BOOLEAN] = INLINE {RETURN[RTMdSetIsSubset[y, x]]};
RTMdSetIsDifferent:
PROCEDURE [x, y: RTMdSet]
RETURNS [BOOLEAN] = INLINE {RETURN[NOT RTMdSetIsSame[x, y]]};
RTMdSetCARD: PROCEDURE [x: RTMdSet] RETURNS [INT];
RTMdSetContains:
PROCEDURE [s: RTMdSet, e: INT]
RETURNS [BOOLEAN] = INLINE {RETURN[s[e]]};
RTLgSetEmpty: RTLgSet = ALL[FALSE];
RTLgSetGenerateElement:
PROCEDURE [i: INT]
RETURNS [RTLgSet];
RTLgSetGenerateInterval:
PROCEDURE [i, j: INT]
RETURNS [RTLgSet];
RTLgSetAddElement:
PROCEDURE [i: INT, s: RTLgSet]
RETURNS [RTLgSet];
RTLgSetAddInterval:
PROCEDURE [i, j: INT, s: RTLgSet]
RETURNS [RTLgSet];
RTLgSetUnion, RTLgSetIntersection, RTLgSetDifference:
PROCEDURE [x, y: RTLgSet] RETURNS [RTLgSet];
RTLgSetIsSubset,
RTLgSetIsSame:
PROCEDURE [x, y: RTLgSet]
RETURNS [BOOLEAN];
RTLgSetIsSuperset:
PROCEDURE [x, y: RTLgSet]
RETURNS [BOOLEAN] = INLINE {RETURN[RTLgSetIsSubset[y, x]]};
RTLgSetIsDifferent:
PROCEDURE [x, y: RTLgSet]
RETURNS [BOOLEAN] = INLINE {RETURN[NOT RTLgSetIsSame[x, y]]};
RTLgSetCARD: PROCEDURE [x: RTLgSet] RETURNS [INT];
RTLgSetContains:
PROCEDURE [s: RTLgSet, e: INT]
RETURNS [BOOLEAN] = INLINE {RETURN[s[e]]};
END. -- RTSets