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.
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. Cad.BasePhase[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];
Go through StacksInEr determing truth value of formula on each element of each stack, looking at innermost quantifier, and setting baseTruthValue accordingly.
EliminateInnerQuantifier:
PROC [i:
CARDINAL, StacksInEi, StacksInEiM1:
QET.StackSeq, formula:
QFF.Formula];
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.
END.