Element Representation
SignatureTableEntry: AlgebraClasses.Object;
SignatureTableEntryData: REF SignatureTableEntryDataRec;
SignatureTableEntryDataRec:
TYPE =
RECORD[
signature: AlgebraClasses.Object; -- Sequence of ASAtomicFormulaOps.Operator's, of the same length as the sequence of polynomials which defines the SignatureTable Structure. Store like this, rather than as Signatures, to remove one level of indirection.
clustersWithThisSignature: AlgebraClasses.Object -- Set of clusters, each of which has this signature
];
Obvious consistency requirement: the signatures of the entries of a SignatureTable are all with respect to the same set of signature polynomials.
SignatureTable: TYPE = AlgebraClasses.Object; -- sequence of SignatureTableEntry's;
Structure Instance Data
SignatureTableStructureData: TYPE = REF SignatureTableStructureDataRec;
SignatureTableStructureDataRec:
TYPE =
RECORD [
polynomials: AlgebraClasses.Object, -- Sequence of polynomials whose signatures will be represented by elements of this structure
clusterStructure: AlgebraClasses.Object, -- for these clusters. Thus we assume that signatures are always wrt clusters; if we want wrt cells, for example, must represent cells as clusters.
];
Structure Operations
PrintName: AlgebraClasses.ToRopeOp;
ShortPrintName: AlgebraClasses.ToRopeOp;
IsSignatureStructure: AlgebraClasses.UnaryPredicate;
Polynomials: AlgebraClasses.UnaryOp;
selector: polynomials of a Signature Structure
StructureData: AlgebraClasses.UnaryToListOp;
selector: returns LIST[polynomials] of a Signature Structure
Element Conversion and IO
Recast: AlgebraClasses.BinaryOp;
CanRecast: AlgebraClasses.BinaryPredicate;
ToExpr: AlgebraClasses.ToExprOp;
LegalFirstChar: AlgebraClasses.LegalFirstCharOp;
Read: AlgebraClasses.ReadOp;
FromRope: AlgebraClasses.FromRopeOp;
ToRope: AlgebraClasses.ToRopeOp;
Write: AlgebraClasses.WriteOp;
SacCad.tioga routines
MakeSignatureTable:
PROC;
Get CurrentDimension, get CurrentDimClusters, make table in obvious way and set InSignatureTable to it.
DisambiguateSignatureTable:
PROC;
Get table from InSignatureTable;
While there is an ambiguous entry (i.e. some of its clusters are in the solution set, some not) in table, do the following:
1. Select some basis polynomial F (in any dimension) that is not currently a signature polynomial. Initialize newTable ← NIL;
2. For each current table entry E, create between 1 and 3 new table entries by calling RefineSignatureTableEntryByPolynomial[E, F], add to newTable.
3. Set table ← newTable;
Set OutSignatureTable to table.
RefineSignatureTableEntryByPolynomial:
PROC [
E: SignatureTableEntry,
F: Polynomial]
RETURNS [
LIST
OF SignatureTableEntry];
Initializes lists Pos, Zero, Neg to NIL, looks up F in bases to get (i, j) reference to it (jth element of i-dimensional basis), for each cluster C of E, sets [neg, zero, pos] ← RefineClusterByPolynomial[C, (i, j)], adds whichever of neg, zero, pos nonNIL to appropriate list. When done, for each of Pos, Zero, Neg which is nonempty, creates a new SignatureTableEntry with appropriate signature, adds to return list.
RefineClusterByPolynomial:
PROC [
C: Cluster, (i, j): RefToBasisElement]
RETURNS [negativeSign, zeroSign, positiveSign: Cluster];
For each constituent cell c, applies GetCellSignAtBasisElement[c, (i, j)], adds c to whichever of pos, zero, or neg lists is appropriate. When done, for each of the three lists, if nonempty, makes a new cluster (picks rep cell, new PolynomialSequenceFile of augmented signature polynomials, augmented signature, same value of truthValue, list of constituent cells, appropriate intracluster adjacencies), and returns it as the appropriate output, else returns NIL for that output.
GetCellSignAtBasisElement:
PROC [c: Cell, (i, j): RefToBasisElement]
RETURNS [Sign];
c is cell in r >= i space, (i, j) is a reference to (jth element of i-dimensional basis), looks into stack file for rep cell e of i-space cluster containing i-space cell d induced by c (how do we know in what file to find that cluster?), and returns jth element of e's basis signature
ExtractSolutionSignatures:
PROC [
T: SignatureTable]
RETURNS [solutionSignatures, dontOccur:
LIST
OF Signature];
T is assumed to be a disambiguated SignatureTable. solutionSignatures is a list of the signatures whose clusters are all in the solution set. dontOccur is signatures which don't occur at all.
SimplifySignatures:
PROC [
LIST
OF Signature]
RETURNS [
LIST
OF Signature];
Sort into lexicographical order and combine.
SignaturesToFormula:
PROC [
LIST
OF Signature]
RETURNS [Formula];
Convert to a formula.
MakeSolutionFormula:
PROC;
MakeSignatureTable, DisambiguateSignatureTable, [solutionSignatures, dontOccur] ← ExtractSolutionSignatures, S ← SimplifySignatures[CONC[solutionSignatures, dontOccur]]; Phi ← SignaturesToFormula[S]; Set environment variable SolutionFormula to Phi.
QE.mesa routines
DisambiguateSignatureTable:
PROC [inTable:
QET.SignatureTable]
RETURNS [outTable:
QET.SignatureTable];
Assume that initially inTable.polynomials ← inTable.cad.primaryPolynomials.
outTable ← copy(inTable).
While there is an ambiguous entry in outTable, do for each such ambiguous entry:
1. Select some polynomial P from the basis of some (proper) induced cad, such that P is not an element of outTable.polynomials (use hashing).
2. Augment the secondarySignature's of all cells of all regions of this entry by sign(P).
3. For each region of this entry, form the subgraph it induces, and construct signed components in this subgraph wrt secondarySignature.
4. Collect the cumulative data: if the sign(s) of P on all newly formed components which are contained in the solution set differ from the sign(s) of P on all newly formed components which are external to the solution set, then we have succeeded in disambiguating this entry with P.
5. Delete this entry, and create two new appropriate unambiguous entries, with appropriately augmented signatures.
6. For all unambiguous entries, augment their signatures with "don't care" in the P position, and augment appropriately (i.e. with the correct P sign) the secondarySignature's of all constituent cells of all entry regions.
7. For each ambiguous entry, carry out steps 2,3,4, and see if we have succeeding in disambiguating that entry with P. If so, then carry out step 5 for this entry. If not, then split this entry into up to three or more (each of which may be ambiguous or unambiguous, but at least one of which must be ambiguous if we are here) entries, corresponding to splitting each of the prior entry regions into up to three or more new regions by the sign of P.
SimplifySignatureSeq:
PROC [
QET.SignatureSeq]
RETURNS [
QET.SignatureSeq];
First determine signatures which do not occur, and use them when helpful.
Sort into lexicographical order and combine.
SignatureSeqToFormula:
PROC [
QET.SignatureSeq]
RETURNS [
QFF.QFFormula];
Convert to a formula.