<> <> <<>> <> <<>> 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]; <<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.>> <<>> <<>> <> <> <> <> <<};>> <<>> <<>> EliminateInnermostQuantifier: PROC [StacksInEr: QET.StackSeq, formula: QFF.Formula]; <> <<>> EliminateInnerQuantifier: PROC [i: CARDINAL, StacksInEi, StacksInEiM1: QET.StackSeq, formula: QFF.Formula]; <> <<>> END.