DIRECTORY Rope, IO, AlgebraClasses, ASAtomicFormulaOps, Variables, Polynomials; QESamplePointStructure: CEDAR DEFINITIONS = BEGIN SamplePoint: TYPE = AlgebraClasses.Object; SamplePointData: TYPE = REF SamplePointDataRec; SamplePointDataRec: TYPE ~ RECORD [ cell: CellIndex, -- cell to which this sample point belongs SELECT type:* FROM null => [ ], extended => [ basePoint: PTS.Point, -- an (r-1)-tuple of elements of baseNumberField; this should be a pointer to a cell sample point in one lower dimension definingPolynomial: POL.Polynomial, -- a univariate algebraic polynomial over baseNumberField. isolatingInterval: RI.RatInterval _ NIL, -- for root of definingPolynomial ], primitive => [ point: PTS.Point -- an r-tuple of elements of primitiveNumberField ], ENDCASE ]; SamplePointStructureData: TYPE = REF SamplePointStructureDataRec; SamplePointStructureDataRec: TYPE = RECORD [ ]; MakeFormulaAlgebra: PROC [polynomialRing: AlgebraClasses.Object] RETURNS [formulaAlgebra: AlgebraClasses.Object]; PrintName: AlgebraClasses.ToRopeOp; ShortPrintName: AlgebraClasses.ToRopeOp; IsFormulaAlgebra: AlgebraClasses.UnaryPredicate; PolynomialRing: AlgebraClasses.UnaryOp; Quantify: PROC [quantifiers: LIST OF Quantifier, in: Formula] RETURNS [out: Formula]; QuantifyChecked: PROC [quantifiers: LIST OF Quantifier, variables: LIST OF Variables.Variable, in: Formula] RETURNS [out: Formula]; Recast: AlgebraClasses.BinaryOp; CanRecast: AlgebraClasses.BinaryPredicate; ToExpr: AlgebraClasses.ToExprOp; LegalFirstChar: AlgebraClasses.LegalFirstCharOp; Read: AlgebraClasses.ReadOp; FromRope: AlgebraClasses.FromRopeOp; ToRope: AlgebraClasses.ToRopeOp; Write: AlgebraClasses.WriteOp; FreeVariables: AlgebraClasses.UnaryToListOp; Negate: AlgebraClasses.UnaryOp; And: AlgebraClasses.NaryOp; Or: AlgebraClasses.NaryOp; XOr: AlgebraClasses.BinaryOp; Difference: AlgebraClasses.BinaryOp; Implies: AlgebraClasses.BinaryOp; Equiv: AlgebraClasses.BinaryOp; AllVarEval: AlgebraClasses.BinaryOp; Eval: AlgebraClasses.BinaryOp; END. ˆQESamplePointStructure.mesa Last Edited by: Arnon, June 10, 1985 4:19:22 pm PDT Quantified formulas (first-order predicate calculus formulas) over a polynomial ring. Element Representation Structure Instance Data Structure Constructor The baseCoeffRing of polynomialRing may be either ordered or unordered; if unordered, it is the user's responsibility not to create atomic formulas with relations like "less". However, AllVarEval will catch an attempt to eval such a bogus atomic formula. Record that the resulting Structure is a BooleanAlgebra. Structure Operations selector: polynomialRing of a Formula Structure Element Constructors No check that the quantifiers actually correspond to the rightmost free variables of the representation of the input Formula in the way that the caller intended. Gets the free variables V of the input formula, and checks that the supplied list of m variables is exactly the rightmost m variables of V. Element Conversion and I/O Element Operations Returns an (ordered) list of the free variables of a Formula Checks that args have same free variables, as do all binary or more ops. First arg is a Formula, secondArg a point (Vector). Checks that length(point) = num free vars of Formula. Returns an element of the Structure Bools. Or should be BinaryPredicate? Lazy evaluation: For a conjunction, stops and returns false as soon as one false conjunct found. For a disjunction, stops and returns true as soon as one true disjunct found. For a difference, returns AllVarEv[A AND (NOT B)]. For an implication, returns AllVarEv[(NOT A) OR B]. For an equivalence, returns AllVarEv[A=>B AND B=>A]. Should complain if baseCoeffRing of polynomialRing of the formulaAlgebra is unordered, and input formula is an atomic formula with an order relation (e.g. "less"). First arg is a Formula, secondArg a point (Vector). Checks that n = length(point) <= m = num free vars of Formula. Assumes that rightmost free vars are to be evaluated If n < m, then returns a Formula with m-n free variables; if n = m, returns AllVarEval[firstArg, secondArg]; If n < m, basically just walks the formula and evaluates the polynomials in the atomic formulas. Êh˜Jšœ™J™3J™J™UJ™J˜šÏk ˜ Jšœ˜Jšœ˜Jšœ˜Jšœ˜Jšœ ˜ Jšœ ˜ —J˜head2šœœ ˜)J˜—Jšœ˜headšÏn™Jšœ œ˜*J™Jšœœœ˜/codešœœ˜šœ˜JšœÏc*˜;šœ˜˜ M˜—˜ Jšœ œŸx˜ŽJšœœ Ÿ;˜_JšœœœŸ!˜JM˜—˜JšœœŸ1˜BM˜—Mš˜—M˜———šœ™Mšœœœ˜Ašœœœ˜,M˜——™šžœœ)œ)˜qMšœÿ™ÿM™8——™šž œ˜#M˜—šžœ˜(M˜—šžœ ˜0M˜—šžœ˜'Jšœ/™/J™——™š žœœœœœ˜UJšœ¡™¡J™—šžœœœœœœ"œ˜ƒJšœŒ™Œ——šœ™šžœ˜ J˜—šž œ!˜*J˜—šžœ˜ J˜—šžœ"˜0J˜—šžœ˜J˜—šžœ˜$J™—šžœ˜ J˜—Jšžœ˜—™šž œ˜,Jšœ<™