DIRECTORY Rope, IO, AlgebraClasses, ASAtomicFormulaOps, Variables, Polynomials; ASFormulaStructure: CEDAR DEFINITIONS = BEGIN Formula: TYPE = AlgebraClasses.Object; Quantifier: TYPE = {exists, forAll}; PropositionalConnective: TYPE = {and, or, xOr, difference, implies, equivalent}; FormulaData: TYPE = REF FormulaDataRec; FormulaDataRec: TYPE ~ RECORD [ SELECT type:* FROM atomic => [ rel: ASAtomicFormulaOps.Operator, -- relation polynomial: Polynomials.Polynomial -- standard form assumed, i.e. polynomial rel 0. ], negation => [ arg: Formula ], compound => [ op: PropositionalConnective, args: LIST OF Formula -- two or more, obviously; assumed to all have same free variables ], quantified => [ quantifiers: LIST OF Quantifier, -- a sequence of m >= 1 Quantifiers matrix: Formula -- it is assumed that matrix has at least m free variables, and that the quantifiers bind the "upper" ("rightmost") m of them. ] ENDCASE ]; Formula: TYPE = AC.Object; FormulaData: TYPE = REF FormulaDataRec; FormulaDataRec: TYPE = RECORD [ numFreeVars: CARDINAL, quantifiers: QuantifierSeq _ NIL, -- Assert length(quantifiers) = numTotalVars - numFreeVars = r - k. It is assumed that the lowest k variables are free, and the highest r - k are quantified. atomicMatrix: BOOL _ FALSE, mainOperator: FormulaOperators.Operator, -- (and, or, or not if not atomicMatrix; otherwise a Relation) operands: LIST OF Formula _ NIL, -- nonNIL iff not atomicMatrix; then each assumed to have r free variables, of which last (r - k) will be governed by the above quantifiers. polynomial: POL.Polynomial _ NIL -- nonNIL iff atomicMatrix ]; QuantifierSeq: TYPE = REF QuantifierSeqRec; QuantifierSeqRec: TYPE = RECORD [SEQUENCE lengthPlus1: [1..100] OF Quantifier]; Quantifier: TYPE = {Exists, ForAll}; FormulaAlgebraData: TYPE = REF FormulaAlgebraDataRec; FormulaAlgebraDataRec: TYPE = RECORD [ polynomialRing: AlgebraClasses.Object -- the Structure for the polynomials occurring in the atomic formulas of this FormulaStructure. ]; 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; ReadFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Object] RETURNS [formula: Formula, termChar: CHAR]; ReadAtomicFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Object] RETURNS [formula: Formula, termChar: CHAR]; 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; Simplify: AlgebraClasses.UnaryOp; END. pASFormulaStructure.mesa Last Edited by: Arnon, June 10, 1985 4:19:22 pm PDT Quantified formulas (first-order predicate calculus formulas) over a polynomial ring. New Element Representation It is not assumed that Formulas are "simplified", or in "canonical form" (notions which may well be meaningless for a given FormulaStructure). Old Element Representation Formulas are represented as (not necessarily simplified) words that are elements of a certain Boolean Algebra. 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. Do easy simplifications. Harder ones will be done by a cad-based method that, when available, will dynamically replace this one in the property list (that e.g. makes use of signatures that do-not occur). Êó˜Jšœ™J™3J™J™UJ™J˜šÏk ˜ Jšœ˜Jšœ˜Jšœ˜Jšœ˜Jšœ ˜ Jšœ ˜ —J˜head2šœœ ˜%J˜—Jšœ˜headšÏn™Jšœ œ˜&J™šœ œ˜$J˜—Jšœœ3˜PJ™Jšœ œœ˜'codešœœ˜šœ˜šœ˜˜ Mšœ"Ïc ˜-Mšœ$Ÿ0˜TM˜—˜ Mšœ ˜ M˜—˜ Mšœ˜Mšœœœ ŸB˜YM˜—˜Mšœ œœ Ÿ#˜DMšœŸ~˜ŽM˜—Mš˜—M˜M˜——J™Ž—šž™Jšœn™nJ™J˜Jšœ œœ˜J˜Jšœ œœ˜'šœœœ˜Jšœ œ˜JšœœŸž˜ÀJšœœœ˜Jšœ)ŸžŸžŸžŸ+˜gJšœ œœ œŸŒ˜­Jšœ œœŸ˜