QE.mesa
DIRECTORY
Rope,
IO,
AlgebraClasses,
Variables,
RatPolynomials,
AlgebraicNumbers,
RealFields,
AlgebraicPolynomials,
Formulas,
QETypes,
QEIO,
Cad;
QE:
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.