DIRECTORY Rope, IO, AlgebraClasses, Variables, RatPolynomials, AlgebraicNumbers, RealFields, AlgebraicPolynomials, Formulas, QETypes, QEIO, Cad; QEManager: CEDAR DEFINITIONS IMPORTS AlgebraicNumbers, RealFields ~ BEGIN OPEN AC: AlgebraClasses, VARS: Variables, RP: RatPolynomials, AN: AlgebraicNumbers, RF: RealFields, AP: AlgebraicPolynomials, QFF: Formulas, QET: QETypes, QEIO, Cad; MakeQEProblem: PROC [inputFormula: QFF.Formula, localizationFormula: QFF.QFFormula, inputVariables: VARS.VariableSeq, minPolyVariable: VARS.VariableSeq _ AN.defaultMinPolyVariable, fieldElementVariable: VARS.VariableSeq _ RF.defaultFieldElementVariable] RETURNS [QET.QEProblem]; EliminateQuantifiers: PROC [QET.QEProblem]; EliminateInnermostQuantifier: PROC [StacksInEr: QET.StackSeq, formula: QFF.Formula]; EliminateInnerQuantifier: PROC [i: CARDINAL, StacksInEi, StacksInEiM1: QET.StackSeq, formula: QFF.Formula]; END. ΠQEManager.mesa Last Edited by: Arnon, November 24, 1987 8:11:12 am PST This is a shell for QECadManager.mesa. QEManager processes the input data for a qe problem, sets up the data for invoking QECadManager, that actually builds the cad, then when the cad is built, QEManager carries out the quantifier elimination. QEManager may interact with ASCompManager. 1. Extract polynomials of formula and localizationFormula; cad _ ProjectionPhase[polynomials, inputVariables, localizationFormula]. 2. CadBasePhase[cad]; 3. For i in [2,...,k] do Cad.RegionExtendCadToCad[i, cad]. 4. Cad.MaximalSignedRegions[k, cad, TRUE]; regions _ Cad.ExtractSignedRegions[k, cad, TRUE]; Sort regions into order of decreasing dimension (for k = 3, put degenerate 0-dimensional regions after nondegenerate), since qe for larger dimensional regions should go faster, since they are likely to have lower degree sample points. 5. For each region of regions, using representative cell = cellInEk (which has extended or primitive sample point), do: 5.1 StacksInEk+1 _ Cad.ExtendCellToStacks[k+1, cellInEk, cad]; 5.2 For i in [k+2,...,r] do StacksInEi _ Cad.ExtendStacksToStacks[i, StacksInEiM1, cad]. 5.3. EliminateInnermostQuantifier[StacksInEr, formula]; 5.4. For i decreasing in [k+1,...,r-1] do EliminateInnerQuantifier[i, StacksInEi, StacksInEiM1, formula]; 5.5 If StacksInEk+1.baseTruthValue then insert this signed component into SignatureTable. 6. DisambiguateSignatureTable, extract signatures corresponding to regions in solution set, bundle them up as a SignatureSeq 7. Apply SimplifySignatureSeq; Return SignatureSeqToFormula and the final SignatureTable. Alternatively (from SacCad.tioga) IF qe problem THEN { Apply proc named by environment variable QEProc; QESignatureTables.MakeSolutionFormula }; Go through StacksInEr determing truth value of formula on each element of each stack, looking at innermost quantifier, and setting baseTruthValue accordingly. Assume baseTruthValue's of StacksInEi already set, and for each stack S in StacksInEiM1, find the stacks in StacksInEi whose bases are the elements of S. Looking at the baseTruthValue's of these stacks in StacksInEi, and the appropriate quantifier in formula, set the baseTruthValue of S. Κ4˜Jšœ™J™7J™Jšœ‘™‘J™šΟk ˜ J˜Jšœ˜J˜Jšœ ˜ Jšœ˜Jšœ˜J˜ Jšœ˜J˜ Jšœ˜Jšœ˜Jšœ˜—J˜head2šœ œ ˜Jšœ˜$J˜—Jšœœœœœ œœœœœ œ œ˜­J˜codešΟn œœœœœœœ/œœœœ ˜–L˜—šžœœœ ˜+LšœAžœ4™„Lšœž œ™Lšœžœ ™:Lšœžœžœϊ™Ηšœw™wLšœžœ™>Lšœ)žœ™XLšœžœ™9Lšœ*žœ)™kLšœZ™Z—Lšœžœ_™}Lšœ žœ žœ™YL™L™J™!šœ œ™Jšœ0™0Jšž%™%J™—L™L™L˜—šžœœœœ ˜TJšœž™žL™—š žœœœœœ ˜kJšœ‘™‘L™—J˜Jšœ˜—…—’–