DIRECTORY Rope, QESignatureStructure; QESignatureTableStructure: CEDAR DEFINITIONS ~ BEGIN 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 ]; SignatureTable: TYPE = AlgebraClasses.Object; -- sequence of SignatureTableEntry's; 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. ]; MakeSignatureTableStructure: PROC [polynomials, clusterStructure: AlgebraClasses.Object, ] RETURNS [structure: AlgebraClasses.Object]; PrintName: AlgebraClasses.ToRopeOp; ShortPrintName: AlgebraClasses.ToRopeOp; IsSignatureStructure: AlgebraClasses.UnaryPredicate; Polynomials: AlgebraClasses.UnaryOp; StructureData: AlgebraClasses.UnaryToListOp; Recast: AlgebraClasses.BinaryOp; CanRecast: AlgebraClasses.BinaryPredicate; ToExpr: AlgebraClasses.ToExprOp; LegalFirstChar: AlgebraClasses.LegalFirstCharOp; Read: AlgebraClasses.ReadOp; FromRope: AlgebraClasses.FromRopeOp; ToRope: AlgebraClasses.ToRopeOp; Write: AlgebraClasses.WriteOp; MakeSignatureTable: PROC; DisambiguateSignatureTable: PROC; RefineSignatureTableEntryByPolynomial: PROC [E: SignatureTableEntry, F: Polynomial] RETURNS [LIST OF SignatureTableEntry]; RefineClusterByPolynomial: PROC [C: Cluster, (i, j): RefToBasisElement] RETURNS [negativeSign, zeroSign, positiveSign: Cluster]; GetCellSignAtBasisElement: PROC [c: Cell, (i, j): RefToBasisElement] RETURNS [Sign]; ExtractSolutionSignatures: PROC [T: SignatureTable] RETURNS [solutionSignatures, dontOccur: LIST OF Signature]; SimplifySignatures: PROC [LIST OF Signature] RETURNS [LIST OF Signature]; SignaturesToFormula: PROC [LIST OF Signature] RETURNS [Formula]; MakeSolutionFormula: PROC; DisambiguateSignatureTable: PROC [inTable: QET.SignatureTable] RETURNS [outTable: QET.SignatureTable]; SimplifySignatureSeq: PROC [QET.SignatureSeq] RETURNS [QET.SignatureSeq]; SignatureSeqToFormula: PROC [QET.SignatureSeq] RETURNS [QFF.QFFormula]; END. QESignatureTableStructure.mesa Last Edited by: Arnon, March 5, 1986 10:49:31 am PST Structure constructor: SignatureTable Entries SignatureTable algorithms Element Representation Obvious consistency requirement: the signatures of the entries of a SignatureTable are all with respect to the same set of signature polynomials. Structure Instance Data Structure Constructor Structure Operations selector: polynomials of a Signature Structure selector: returns LIST[polynomials] of a Signature Structure Element Conversion and IO SacCad.tioga routines Get CurrentDimension, get CurrentDimClusters, make table in obvious way and set InSignatureTable to it. 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. 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. 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. 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 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. Sort into lexicographical order and combine. Convert to a formula. MakeSignatureTable, DisambiguateSignatureTable, [solutionSignatures, dontOccur] _ ExtractSolutionSignatures, S _ SimplifySignatures[CONC[solutionSignatures, dontOccur]]; Phi _ SignaturesToFormula[S]; Set environment variable SolutionFormula to Phi. QE.mesa routines 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. First determine signatures which do not occur, and use them when helpful. Sort into lexicographical order and combine. Convert to a formula. Ê<˜Jšœ™J™4J˜Jšœ-™-J™Jšœ™J™šÏk ˜ Jšœ˜Jšœ˜—J˜head2šœœ˜,J˜—Jšœ˜headšÏn™Jšœ*˜+J˜Jšœœ˜8šœœœ˜*Jšœ"ÏcÜ˜þJšœ1Ÿ4˜eJšœ˜J˜—Jšœ‘™‘J˜JšœœŸ%˜T—šœ™Icodešœœœ ˜Gšœ œœ˜/Mšœ%Ÿ]˜‚Mšœ*Ÿ”˜¾M˜——™Mšžœœ:œ$˜†—šœ™šž œ˜#M˜—šžœ˜(M˜—šžœ ˜4J˜—šžœ˜$Jšœ.™.J™—šž œ˜,Jšœ=™=——šœ™šžœ˜ J˜—šž œ!˜*J˜—šžœ˜ J˜—šžœ"˜0J˜—šžœ˜J˜—šžœ˜$J˜—šžœ˜ J˜—šžœ˜J˜——™šžœœ˜Jšœžœžœ$žœ ™iM˜—šžœœ˜!Mšœžœ™ šœ{™{Mšœ~™~MšœWž%œ™”Mšœ™—Jšœžœ ™M˜—šž%œœžœžœœœœ˜|Mšœ²žœÕ™ M˜—šžœœžœ&œ1˜€Jšœ%žœ£™áM˜—šžœœ&œ˜TMšœœ™œJ™—šžœœžœœ!œœ˜oJšœÁ™ÁM˜—šžœœœœœœœ˜IJ™,M˜—š žœœœœœ˜@J™J™—šžœœ˜Jš žœžœ$žœžœ.žœ6™ú——™š žœœœœœ˜fMšœL™LMšœ™šœP™PMšœ™MšœY™YMšœˆ™ˆMšœš™šM™rMšœÞ™ÞM™Ã—M˜—š žœœœœœ˜IJ™IJ™,M˜—š žœœœœœ˜GJ™M˜——J˜Jšœ˜—…— ø