DIRECTORY Rope, IO, MathExpr, AlgebraClasses, Bools, FormulaOperators, Points, Variables, DistribPolys, Polynomials; Formulas: CEDAR DEFINITIONS = BEGIN OPEN AC: AlgebraClasses, VARS: Variables, DP: DistribPolys, POL: Polynomials; 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}; formulaClass: AC.StructureClass; FormulaAlgebraData: TYPE = REF FormulaAlgebraDataRec; FormulaAlgebraDataRec: TYPE = RECORD [ polynomialRing: AC.Structure -- contains the polynomials occurring in matrices of formulas of this FormulaAlgebra. ]; FormulaAllVarEvalOp: TYPE = PROC [in: Formula, point: Points.Point] RETURNS [Bools.Bool]; FormulaOps: TYPE = REF FormulaOpsRec; -- prop key is $FormulaRing. FormulaOpsRec: TYPE = RECORD [ allVarEval: FormulaAllVarEvalOp ]; MakeFormulaAlgebra: PROC [polynomialRing: AC.Structure] RETURNS [formulaAlgebra: AC.Structure]; IsFormulaAlgebra: PROC [structure: AC.Structure] RETURNS [BOOL]; AllVarEval: PROC [formulaAlgebra: AC.Structure] RETURNS [FormulaAllVarEvalOp]; Quantify: PROC [quantifier: Quantifier, in: Formula] RETURNS [out: Formula]; ReadFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR]; ReadAtomicFormula: PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR]; FormulaFromRope: PROC [in: Rope.ROPE, formulaAlgebra: AC.Structure] RETURNS [out: Formula]; FormulaToRope: PROC [in: Formula, termRope: Rope.ROPE _ NIL] RETURNS [out: Rope.ROPE]; MakeFormulaExpr: PROC [in: Formula] RETURNS [out: MathExpr.EXPR]; WriteFormula: PROC [in: Formula, out: IO.STREAM]; Disjunct: PROC [in1, in2: Formula] RETURNS [out: Formula]; Conjunct: PROC [in1, in2: Formula] RETURNS [out: Formula]; Negate: PROC [in: Formula] RETURNS [out: Formula]; Difference: PROC [in1, in2: Formula] RETURNS [Formula]; AllVarEv: FormulaAllVarEvalOp; END. NFormulas.mesa Last Edited by: Arnon, June 10, 1985 4:19:22 pm PDT Types Formulas are represented as (not necessarily simplified) words that are elements of a certain Boolean Algebra. Class for a Boolean Algebra of Formulas Instance Data for a Boolean Algebra of Formulas Operations unique to Boolean Algebras of Formulas Evaluate all variables of in at a point over the baseCoeffRing of in. Constructor for a Boolean Algebra of Formulas Extract Formula Operations from Class Property Lists Constructors Conversion and I/O termRope is written following the polynomial. Arithmetic Κε˜Jšœ ™ J™3J˜šΟk ˜ Jšœ˜Jšœ˜J˜ Jšœ˜J˜J˜Jšœ˜Jšœ ˜ Jšœ ˜ Jšœ ˜ —J˜head2šœ œ ˜J˜—Jš œœœœ œœ˜UheadšΟn™Jšœn™nJ™J˜Jšœ œœ˜J˜Jšœ œœ˜'šœœœ˜Jšœ œ˜JšœœΟcž˜ΐJšœœœ˜Jšœ)ŸžŸžŸžŸ+˜gJšœ œœ œŸŒ˜­Jšœ œœŸ˜