FormulasImpl.mesa
Last Edited by: Arnon, June 10, 1985 4:19:22 pm PDT
DIRECTORY
Rope,
Basics,
IO,
Atom,
AlgebraClasses,
Bools,
MathExpr,
MathConstructors,
Variables,
DistribPolys,
Polynomials,
FormulaOperators,
Formulas;
FormulasImpl: CEDAR PROGRAM
IMPORTS Rope, IO, Atom, AlgebraClasses, Bools, DistribPolys, Polynomials, MathConstructors, FormulaOperators
EXPORTS Formulas =
BEGIN OPEN AC: AlgebraClasses, VARS: Variables, DP: DistribPolys, POL: Polynomials, Formulas;
TypeError: PUBLIC ERROR [message: ATOM ← $Unspecified] = CODE;
Class for a Boolean Algebra of Formulas
ClassPrintName: AC.PrintNameProc = {
data: FormulaAlgebraData ← NARROW[structure.instanceData];
RETURN[Rope.Concat[
"Formulas in ",
data.polynomialRing.class.printName[data.polynomialRing]
] ];
};
ClassIsElementOf: AC.ElementOfProc = {
Assumes that if item is a formula, then it really belongs to the domain pointed to by its structure field.
formula: Formula;
IF NOT ISTYPE[item, Formula] THEN RETURN[FALSE];
formula ← NARROW[item];
IF NOT structure.class.structureEqual[structure, formula.structure] THEN RETURN[FALSE];
RETURN[ TRUE ]
};
ClassLegalFirstChar: AC.LegalFirstCharOp = {
data: FormulaAlgebraData ← NARROW[structure.instanceData];
IF data.polynomialRing.class.legalFirstChar[char, data.polynomialRing] THEN RETURN[TRUE];
RETURN[char = '( OR char = '~ OR char = '[ ];
Legal first char of formula is either legal first char of polynomial, or ( or [ or ~
};
ClassRead: AC.ReadOp = {
termChar: CHAR;
formula: Formula;
[formula, termChar] ← ReadFormula[in, structure];
RETURN[formula ];
};
ClassFromRope: AC.FromRopeOp = {
stream: IO.STREAM ← IO.RIS[in];
RETURN[ ClassRead[stream, structure] ];
};
ClassToRope: AC.ToRopeOp = {
formula: Formula ← NARROW[in];
RETURN[ FormulaToRope[formula] ] -- use default termRope
};
ClassWrite: AC.WriteOp = {
formula: Formula ← NARROW[in];
IO.PutRope[stream, ClassToRope[formula] ] -- avoid WriteFormula newlines
};
ClassToExpr: AC.ToExprOp = {
formula: Formula ← NARROW[in];
RETURN[ MakeFormulaExpr[formula] ];
};
ClassDisjunct: AC.BinaryOp = {
firstFormula: Formula ← NARROW[firstArg];
secondFormula: Formula ← NARROW[secondArg];
IF NOT firstFormula.structure.class.structureEqual[firstFormula.structure, secondFormula.structure] THEN TypeError[];
RETURN[ Disjunct[firstFormula, secondFormula] ]
};
ClassConjunct: AC.BinaryOp = {
firstFormula: Formula ← NARROW[firstArg];
secondFormula: Formula ← NARROW[secondArg];
IF NOT firstFormula.structure.class.structureEqual[firstFormula.structure, secondFormula.structure] THEN TypeError[];
RETURN[ Conjunct[firstFormula, secondFormula] ]
};
ClassComplement: AC.UnaryOp = {
formula: Formula ← NARROW[arg];
RETURN[ Negate[formula] ]
};
ClassDifference: AC.BinaryOp = {
firstFormula: Formula ← NARROW[firstArg];
secondFormula: Formula ← NARROW[secondArg];
IF NOT firstFormula.structure.class.structureEqual[firstFormula.structure, secondFormula.structure] THEN TypeError[];
RETURN[ Difference[firstFormula, secondFormula] ]
};
formulaOps: FormulaOps ← NEW[FormulaOpsRec ← [
allVarEval: AllVarEv
] ];
formulaProp: Atom.DottedPair ← NEW[Atom.DottedPairNode← [$FormulaAlgebra, formulaOps]];
formulaClass: PUBLIC AC.StructureClass ← NEW[AC.StructureClassRec ← [
category: lattice,
printName: ClassPrintName,
structureEqual: AC.defaultStructureEqualityTest,
isElementOf: ClassIsElementOf,
legalFirstChar: ClassLegalFirstChar,
read: ClassRead,
fromRope: ClassFromRope,
toRope: ClassToRope,
write: ClassWrite,
toExpr: ClassToExpr,
add: ClassDisjunct,
negate: ClassComplement, -- hack
multiply: ClassConjunct,
divide: ClassDifference,
booleanAlgebra: TRUE,
complement: ClassComplement,
propList: LIST[formulaProp]
] ];
Constructor for a Boolean Algebra of Formulas
MakeFormulaAlgebra: PUBLIC PROC [polynomialRing: AC.Structure] RETURNS [formulaAlgebra: AC.Structure] ~ {
formulaAlgebraData: FormulaAlgebraData ← NEW[FormulaAlgebraDataRec ← [
polynomialRing: polynomialRing
] ];
formulaAlgebra ← NEW[AC.StructureRec ← [
class: formulaClass,
instanceData: formulaAlgebraData
] ];
};
Extract Formula Operations from Class Property Lists
IsFormulaAlgebra: PUBLIC PROC [structure: AC.Structure] RETURNS [BOOL] ~ {
IF Atom.GetPropFromList[structure.class.propList, $FormulaAlgebra] # NIL THEN RETURN[TRUE] ELSE RETURN[FALSE];
};
AllVarEval: PUBLIC PROC [formulaAlgebra: AC.Structure] RETURNS [FormulaAllVarEvalOp] ~ {
formulaOps: FormulaOps ← NARROW[ Atom.GetPropFromList[formulaAlgebra.class.propList, $FormulaAlgebra] ];
IF formulaOps = NIL THEN ERROR;
RETURN[formulaOps.allVarEval];
};
Conversion and I/O
ReadFormula: PUBLIC PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR] ~ {
Assumes that formula is quantifier-free, and is either an atomic formula, a formula enclosed in parentheses, the negation of a formula enclosed in parenthesis, a disjunction of formulas, or a conjunction of formulas. Termination is either by end of stream, or $, or an extra ) (for recursive calls). If by end of stream, then termChar = NUL. If by $, then the $ is removed from in. If by ), the ) is not removed from in.
char: CHAR;
junct: Formula;
list, listTail: LIST OF Formula ← NIL;
formulaAlgebraData: FormulaAlgebraData ← NARROW[formulaAlgebra.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
ReadJunct: PROC ~ {
Skips preceding white space and read a junct. At exit, char is "terminating char", i.e. first nonblank char beyond junct (NUL if end of stream). char has been removed if = $, otherwise not.
[]← in.SkipWhitespace[];
char ← in.PeekChar[];
IF polynomialRing.class.legalFirstChar[char, polynomialRing] THEN -- unparenthesized atomic formula
[junct, char] ← ReadAtomicFormula[in, formulaAlgebra]
ELSE IF char='~ THEN {
char ← in.GetChar[]; -- remove tilde
[]← in.SkipWhitespace[];
char ← in.PeekChar[];
IF char='( THEN {
[] ← in.GetChar[]; -- remove left paren
[junct, char] ← ReadFormula[in, formulaAlgebra];
IF char#') THEN ERROR;
junct ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["not", FormulaOperators.Operators],
operands: LIST[junct]
]]
]];
[] ← in.GetChar[]; -- remove right paren
[]← in.SkipWhitespace[];
IF in.EndOf[] THEN {char ← 000C; RETURN};
char ← in.PeekChar[];
IF char = '$ THEN [] ← in.GetChar[]; -- remove $
RETURN;
}
ELSE ERROR;
}
ELSE IF char='( THEN {
[] ← in.GetChar[]; -- move past left paren
[junct, char] ← ReadFormula[in, formulaAlgebra];
IF char#') THEN ERROR;
[] ← in.GetChar[]; -- remove right paren
[]← in.SkipWhitespace[];
IF in.EndOf[] THEN {char ← 000C; RETURN};
char ← in.PeekChar[];
IF char = '$ THEN [] ← in.GetChar[]; -- remove $
RETURN;
}
ELSE ERROR;
};
ReadJunct[]; formula ← junct;
IF in.EndOf[] THEN RETURN[formula, char];
IF char='| THEN {
list ← listTail ← LIST[junct];
WHILE char='| DO
[] ← in.GetChar[]; -- remove |
ReadJunct[];
listTail ← listTail.rest ← LIST[junct];
ENDLOOP;
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["or", FormulaOperators.Operators],
operands: list
]]
]];
};
IF char='& THEN {
list ← listTail ← LIST[junct];
WHILE char='& DO
[] ← in.GetChar[]; -- remove |
ReadJunct[];
listTail ← listTail.rest ← LIST[junct];
ENDLOOP;
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["and", FormulaOperators.Operators],
operands: list
]]
]];
};
RETURN[formula, char];
};
ReadAtomicFormula: PUBLIC PROC [in: IO.STREAM, formulaAlgebra: AC.Structure] RETURNS [formula: Formula, termChar: CHAR] ~ {
May be terminated by end of stream, or by &, |, ), or $. If by end of stream, then termChar ← NUL. If by $, then $ has been removed from in. If by any of the other chars, then not removed from in.
leftPoly, rightPoly, formulaPoly: POL.Polynomial;
leftDPoly, rightDPoly: DP.DPolynomial;
firstRelationChar: CHAR;
relation: Rope.ROPE;
polySign: Basics.Comparison;
formulaAlgebraData: FormulaAlgebraData ← NARROW[formulaAlgebra.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
RelationProc: DP.TermCharProc = {
SELECT char FROM
'<, '>, '=, '#,'~ => RETURN[TRUE];
ENDCASE => RETURN[FALSE];
};
EndAtomicFormulaProc: DP.TermCharProc = {
SELECT char FROM
'&, '|, '), '$ => RETURN[TRUE];
ENDCASE => RETURN[FALSE];
};
[leftDPoly, firstRelationChar] ← DP.ReadDPoly[in, V, polyRingData.baseCoeffRing, RelationProc];
IF in.EndOf[] OR firstRelationChar = '$ THEN ERROR; -- check that we saw a relation char
[] ← in.GetChar[]; -- remove firstRelationChar
leftPoly ← NARROW[POL.PolyFromDPoly[leftDPoly, polynomialRing]];
SELECT firstRelationChar FROM
'< => IF in.PeekChar[] = '= THEN {relation ← "le"; [] ← in.GetChar[] } ELSE relation ← "lt";
'> => IF in.PeekChar[] = '= THEN {relation ← "ge"; [] ← in.GetChar[] } ELSE relation ← "gt";
'~ => IF in.PeekChar[] = '= THEN {relation ← "ne"; [] ← in.GetChar[] } ELSE ERROR; -- no other valid meaning for ~ here
'= => relation ← "eq";
'# => relation ← "ne";
ENDCASE => ERROR; -- only cases possible
[rightDPoly, termChar] ← DP.ReadDPoly[in, V, polyRingData.baseCoeffRing, EndAtomicFormulaProc];
rightPoly ← NARROW[POL.PolyFromDPoly[rightDPoly, polynomialRing]];
formulaPoly ← NARROW[ polynomialRing.class.subtract[leftPoly, rightPoly] ];
IF polynomialRing.class.ordered THEN
polySign ← polynomialRing.class.sign[formulaPoly]
ELSE
polySign ← greater;
IF polySign = less THEN {
formulaPoly ← NARROW[ polynomialRing.class.negate[formulaPoly] ]; -- polynomial in atomic formula must be nonnegative
SELECT relation FROM
"lt" => relation ← "gt";
"le" => relation ← "ge";
"gt" => relation ← "lt";
"ge" => relation ← "le";
ENDCASE;
};
formula ← NEW[AC.ObjectRec ← [
structure: formulaAlgebra,
data: NEW[FormulaDataRec ← [
numFreeVars: polyRingData.allVariables.lengthPlus1 - 1,
atomicMatrix: TRUE,
mainOperator: FormulaOperators.FromRope[relation, FormulaOperators.Operators],
polynomial: formulaPoly
]]
]];
RETURN[formula, termChar];
};
FormulaFromRope: PUBLIC PROC [in: Rope.ROPE, formulaAlgebra: AC.Structure] RETURNS [out: Formula] ~ {
stream: IO.STREAM ← IO.RIS[in];
termChar: CHAR;
[out, termChar ] ← ReadFormula[stream, formulaAlgebra];
};
FormulaToRope: PUBLIC PROC [in: Formula, termRope: Rope.ROPE ← NIL] RETURNS [out: Rope.ROPE] ~ {
formulaAlgebraData: FormulaAlgebraData ← NARROW[in.structure.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
coeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[in.data];
IF inData.atomicMatrix THEN {
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
out ← Rope.Concat[ "( ", POL.PolyToRope[inData.polynomial, ""]];
SELECT mainOperatorData^ FROM
lt => out ← Rope.Concat[out, " < 0 )"];
le => out ← Rope.Concat[out, " <= 0 )"];
gt => out ← Rope.Concat[out, " > 0 )"];
ge => out ← Rope.Concat[out, " >= 0 )"];
eq => out ← Rope.Concat[out, " = 0 )"];
ne => out ← Rope.Concat[out, " # 0 )"];
ENDCASE;
RETURN[ Rope.Concat[out, termRope] ];
}
ELSE {
terms: LIST OF Formula ← inData.operands;
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ # not THEN out ← "( " ELSE out ← "~ ( ";
WHILE terms#NIL DO
out ← Rope.Concat[out, FormulaToRope[terms.first] ];
terms ← terms.rest;
IF terms#NIL THEN SELECT mainOperatorData^ FROM
and => out ← Rope.Concat[out, " & "];
or => out ← Rope.Concat[out, " | "];
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
ENDLOOP;
out ← Rope.Cat[out, " )", termRope];
};
};
MakeFormulaExpr: PUBLIC PROC [in: Formula] RETURNS [out: MathExpr.EXPR] ~ {
formulaAlgebraData: FormulaAlgebraData ← NARROW[in.structure.instanceData];
polynomialRing: AC.Structure ← formulaAlgebraData.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
V: VARS.VariableSeq ← polyRingData.allVariables;
coeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[in.data];
IF inData.atomicMatrix THEN {
polynomial: POL.Polynomial ← inData.polynomial;
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
SELECT mainOperatorData^ FROM
lt => RETURN[MathConstructors.MakeLtFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
le => RETURN[MathConstructors.MakeLeFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
gt => RETURN[MathConstructors.MakeGtFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ge => RETURN[MathConstructors.MakeGeFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
eq => RETURN[MathConstructors.MakeEqFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ne => RETURN[MathConstructors.MakeNotEqFormula[
POL.MakePolyExpr[polynomial], MathConstructors.MakeInt["0"] ] ];
ENDCASE;
}
ELSE {
terms: LIST OF Formula ← inData.operands;
firstTermExpr: MathExpr.EXPR ← MakeFormulaExpr[terms.first];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ = not THEN
RETURN[MathConstructors.MakeNot[MathConstructors.MakeParen[firstTermExpr] ] ];
out ← MathConstructors.MakeParen[firstTermExpr];
terms ← terms.rest;
WHILE terms#NIL DO
SELECT mainOperatorData^ FROM
and => out ← MathConstructors.MakeAnd[out, MathConstructors.MakeParen[MakeFormulaExpr[terms.first] ] ];
or => out ← MathConstructors.MakeOr[out, MathConstructors.MakeParen[MakeFormulaExpr[terms.first] ] ];
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
terms ← terms.rest;
ENDLOOP;
};
};
WriteFormula: PUBLIC PROC [in: Formula, out: IO.STREAM] ~ {
formulaRope: Rope.ROPE ← FormulaToRope[in];
out.PutF["\n %g \n", IO.rope[formulaRope] ];
};
Arithmetic
Disjunct: PUBLIC PROC [in1, in2: Formula] RETURNS [out: Formula] = {
data1: FormulaData ← NARROW[in1.data];
data2: FormulaData ← NARROW[in2.data];
RETURN[NEW[AC.ObjectRec ← [
structure: in1.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: MAX[data1.numFreeVars, data2.numFreeVars],
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["or", FormulaOperators.Operators],
operands: LIST[in1,in2]
]]
]]
];
};
Conjunct: PUBLIC PROC [in1, in2: Formula] RETURNS [out: Formula] = {
data1: FormulaData ← NARROW[in1.data];
data2: FormulaData ← NARROW[in2.data];
RETURN[NEW[AC.ObjectRec ← [
structure: in1.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: MAX[data1.numFreeVars, data2.numFreeVars],
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["and", FormulaOperators.Operators],
operands: LIST[in1,in2]
]]
]]
];
};
Negate: PUBLIC PROC [in: Formula] RETURNS [out: Formula] = {
data: FormulaData ← NARROW[in.data];
RETURN[NEW[AC.ObjectRec ← [
structure: in.structure,
data: NEW[FormulaDataRec ← [
numFreeVars: data.numFreeVars,
atomicMatrix: FALSE,
mainOperator: FormulaOperators.FromRope["not", FormulaOperators.Operators],
operands: LIST[in]
]]
]]
];
};
Difference: PUBLIC PROC [in1, in2: Formula] RETURNS [Formula] = {
RETURN[ Conjunct[in1, Negate[in2] ] ];
};
AllVarEv: PUBLIC FormulaAllVarEvalOp ~ {
data: FormulaAlgebraData ← NARROW[in.structure.instanceData];
polynomialRing: AC.Structure ← data.polynomialRing;
polyRingData: POL.PolynomialRingData ← NARROW[polynomialRing.instanceData];
baseCoeffRing: AC.Structure ← polyRingData.baseCoeffRing;
inData: FormulaData ← NARROW[in.data];
IF NOT baseCoeffRing.class.ordered THEN TypeError[$OrderedStructureNeeded];
IF inData.atomicMatrix THEN {
sign: Basics.Comparison ← baseCoeffRing.class.sign[POL.AllVarEv[inData.polynomial, point] ];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
SELECT mainOperatorData^ FROM
lt => RETURN[IF sign = less THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE]];
le => RETURN[IF sign = less OR sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
gt => RETURN[IF sign = greater THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE]];
ge => RETURN[IF sign = greater OR sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
eq => RETURN[IF sign = equal THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
ne => RETURN[IF sign = less OR sign = greater THEN Bools.FromBOOL[TRUE] ELSE Bools.FromBOOL[FALSE] ];
ENDCASE;
}
ELSE {
terms: LIST OF Formula ← inData.operands;
bool: Bools.Bool ← AllVarEv[terms.first, point];
mainOperatorData: FormulaOperators.OperatorData ← NARROW[inData.mainOperator.data];
IF mainOperatorData^ = not THEN
RETURN[Bools.Negate[bool] ];
terms ← terms.rest;
WHILE terms#NIL DO
SELECT mainOperatorData^ FROM
and => {
IF NOT NARROW[bool.data, Bools.BoolData]^ THEN RETURN[Bools.FromBOOL[FALSE]];
bool ← Bools.Conjunct[bool, AllVarEv[terms.first, point] ];
};
or => {
IF NARROW[bool.data, Bools.BoolData]^ THEN RETURN[Bools.FromBOOL[TRUE]];
bool ← Bools.Disjunct[bool, AllVarEv[terms.first, point] ];
};
ENDCASE => ERROR; -- shouldn't be in here when mainOperator = not
terms ← terms.rest;
ENDLOOP;
RETURN[bool];
};
RETURN[Bools.FromBOOL[TRUE]]; -- satisfy compiler
};
END.