INTERFACEAnIndexedNF ; IMPORT JunoAST; TYPE T = JunoAST.NormalForm BRANDED "IndexedNF.T" OBJECT v_cnt, c_cnt: CARDINAL := 0 END;
IndexNF.T
is like a JunoAST.NormalForm
, except that the var
and
conj
fields may be arrays that are larger than the valid number of
existential variables and conjuncts stored in it.
In particular, if nf
is a T
(indexed normal form), then the valid
existential variables are stored in nf.var[0..nf.v_cnt-1]
, and the valid
conjuncts are stored in nf.conj[0..nf.c_cnt-1]
.
PROCEDURE New(var_cnt, conj_cnt: CARDINAL := 10): T;
Return a newT
from a global avail list. The valuesvar_cnt
andconj_cnt
are hints for the sizes of the existential variable and conjunct arrays; the arrays of the result may be smaller or larger than the hints.
PROCEDURE Dispose(inf: T);
Return inf
to the global avail list.
PROCEDURE ToNF(inf: T): JunoAST.NormalForm;
Return aJunoAST.NormalForm
equivalent toinf
.
PROCEDURE FromNF(nf: JunoAST.NormalForm; VAR (*INOUT*) res: T);
Setres
to an indexed normal form equivalent tonf
.
PROCEDURE AddVar(VAR (*INOUT*) res: T; var: JunoAST.NearVarLink);
Append the variablevar
to the variable list ofres
.
PROCEDURE AddConj(VAR (*INOUT*) res: T; conj: JunoAST.Formula);
Append the formulaconj
to the conjunction list ofres
.
PROCEDURE AddVarList(VAR (*INOUT*) res: T; vars: JunoAST.NearVarList);
Append the variablesvars
to the variable list ofres
.
PROCEDURE AddConjList(VAR (*INOUT*) res: T; forms: JunoAST.ExprList);
Append the formulasforms
to the conjunction list ofres
.
PROCEDURE AddVarArray(VAR (*INOUT*) res: T; READONLY vars: JunoAST.Vars);
Append the variablesvars
to the variable list ofres
.
PROCEDURE AddConjArray(VAR (*INOUT*) res: T; READONLY forms: JunoAST.Formulas);
Append the formulasforms
to the conjunction list ofres
.
END IndexedNF.