-- JunoSolverImpl.mesa
-- June 11, 1983 12:05 am
-- GNelson
-- Last Edited by: Gnelson, December 11, 1983 10:10 pm
DIRECTORY SolverCommon, JunoSolver, JunoSyntax, RealSolver,
PairSolver, JunoBind, Lisp, JunoLookup, LinearSolver;
JunoSolverImpl: PROGRAM
IMPORTS SolverCommon, JunoSyntax, RealSolver, PairSolver,
JunoBind, Lisp, JunoLookup, LinearSolver
EXPORTS JunoSolver
= BEGIN OPEN SolverCommon, JunoSolver, Lisp, JS: JunoSyntax, JB: JunoBind;
Solve: PUBLIC PROC [f: JS.Formula, vl: JS.Varlist, al: JunoBind.Alist, defs: REF]
RETURNS [al2: JunoBind.Alist, rc: ResultCode]
= {g: JS.Formula;
vl2: JS.Varlist;
rcon: RealSolver.Context;
lcon: PairSolver.Context;
eq: Value;
[g, vl2] ← Normalize[f, defs];
al2 ← JB.EmptyBinding[];
{vll: JS.Varlist ← vl;
WHILE vll # NIL DO
{temp: Solvee ← NewSolvee[Car[vll]];
al2 ← JB.NewBind[al2, Car[vll], temp];
vll ← Cdr[vll]}
ENDLOOP};
rc ← $solved;
[eq, rcon, lcon] ← SetUp[al2, vl2, al, g ! ExplicitOccurrenceOfFalse => rc ← $refuted];
IF rc = $refuted THEN RETURN;
rc ← SolveLoop[eq, rcon, lcon];
SELECT TRUE FROM
rc = $refuted OR rc = $stumped => NULL;
rc = $solved OR rc = $close => al2 ← ConstructSolution[vl, al2, rcon, lcon]
ENDCASE => ERROR};
ExplicitOccurrenceOfFalse: SIGNAL = CODE;
SetUp: PROC [al2: JS.Alist, vl2: JS.Varlist, al: JS.Alist, g: JS.Formula]
RETURNS [eq: Value, rcon: RealSolver.Context, lcon: PairSolver.Context]
= {rcon ← RealSolver.NewContext[];
lcon ← PairSolver.NewContext[];
al2 ← JB.Push[al2];
eq ← NIL;
WHILE g # NIL DO
{f: JS.Formula ← Car[g];
pred: JS.PredName ← JS.PredOfAtomicFormula[f];
args: JS.Varlist ← JS.TermlistOfAtomicFormula[f];
ndl: Value;
g ← Cdr[g];
[ndl, al2] ← VarlistToNodeList[args, al2, vl2, al, rcon, lcon];
SELECT TRUE FROM
pred = JS.true => NULL;
pred = JS.false => SIGNAL ExplicitOccurrenceOfFalse;
pred = JS.eq => eq ← Cons[ndl, eq];
pred = JS.neq => lcon.neq ← Cons[ndl, lcon.neq];
pred = JS.isPairOf => lcon.pa ← Cons[ndl, lcon.pa];
pred = JS.isSumOf => rcon.su ← Cons[ndl, rcon.su];
pred = JS.isPositive => rcon.po ← Cons[ndl, rcon.po];
pred = JS.isProductOf => rcon.pr ← Cons[ndl, rcon.pr];
Pair[pred] AND Car[pred] = JS.constant AND
(ISTYPE[Cadr[pred], REF INT] OR ISTYPE[Cadr[pred], REF REAL])
=> rcon.b ← Cons[Cons[Cadr[pred], ndl], rcon.b];
Pair[pred] AND Car[pred] = JS.constant AND ISTYPE[Cadr[pred], ATOM]
=> lcon.b ← Cons[Cons[Cadr[pred], ndl], lcon.b]
ENDCASE => ERROR}
ENDLOOP;
al2 ← JB.Pop[al2]};
VarlistToNodeList: PROC [args: JS.Varlist,
al2: JB.Alist,
vl2: JS.Varlist,
al: JB.Alist,
rcon: RealSolver.Context,
lcon: PairSolver.Context]
RETURNS [ndl: Value, newal2: JB.Alist]
= {ndl ← NIL;
WHILE args # NIL DO
{arg: Value ← Car[args];
args ← Cdr[args];
SELECT TRUE FROM
~JB.InDomain[arg, al2] AND ~ Memq[arg, vl2] =>
{u: Value ← JB.Lookup[arg, al];
temp: Solvee ← NewSolvee[arg];
ndl ← Cons[temp, ndl];
IF Pair[u]
THEN lcon.b ← Cons[Cons[u, temp], lcon.b]
ELSE rcon.b ← Cons[Cons[u, temp], rcon.b]};
JB.InDomain[arg, al2] =>
ndl ← Cons[JB.Lookup[arg, al2], ndl];
~JB.InDomain[arg, al2] AND Memq[arg, vl2] =>
{temp: Solvee ← NewSolvee[arg];
al2 ← JB.NewBind[al2, arg, temp];
ndl ← Cons[temp, ndl]}
ENDCASE => ERROR};
ENDLOOP;
ndl ← Reverse[ndl];
newal2 ← al2};
SolveLoop: PROC [eq: Value, rcon: RealSolver.Context, lcon: PairSolver.Context]
RETURNS [rc: ResultCode]
= {rc ← $solved;
DO SELECT TRUE FROM
rc # $refuted AND eq # NIL =>
{x: Solvee = NARROW[Car[Car[eq]]];
y: Solvee = NARROW[Cadr[Car[eq]]];
eq ← Cdr[eq];
[eq, rc] ← PairSolver.Merge[x, y, eq, lcon];
[eq, rc] ← RealSolver.Merge[x, y, eq, rcon]};
rc # $refuted AND lcon.b # NIL =>
{u: Value ← Car[Car[lcon.b]];
x: Solvee ← NARROW[Cadr[Car[lcon.b]]];
lcon.b ← Cdr[lcon.b];
[eq, rc] ← PairSolver.Fix[u, x, eq, lcon]};
rc # $refuted AND lcon.neq # NIL =>
{x: Solvee ← NARROW[Car[Car[lcon.neq]]];
y: Solvee ← NARROW[Cadr[Car[lcon.neq]]];
lcon.neq ← Cdr[lcon.neq];
rc ← PairSolver.Neq[x, y, lcon]};
rc # $refuted AND rcon.b # NIL =>
{u: Value ← Car[Car[rcon.b]];
x: Solvee ← NARROW[Cadr[Car[rcon.b]]];
rcon.b ← Cdr[rcon.b];
[eq, rc] ← RealSolver.Fix[u, x, eq, rcon]};
rc # $refuted AND lcon.pa # NIL =>
{x: Solvee ← NARROW[Car[Car[lcon.pa]]];
y: Solvee ← NARROW[Cadr[Car[lcon.pa]]];
z: Solvee ← NARROW[Caddr[Car[lcon.pa]]];
lcon.pa ← Cdr[lcon.pa];
[eq, rc] ← PairSolver.IsPairOf[x, y, z, eq, lcon]};
rc # $refuted AND rcon.su # NIL =>
{x: Solvee ← NARROW[Car[Car[rcon.su]]];
y: Solvee ← NARROW[Cadr[Car[rcon.su]]];
z: Solvee ← NARROW[Caddr[Car[rcon.su]]];
rcon.su ← Cdr[rcon.su];
[eq, rc] ← RealSolver.IsSumOf[x, y, z, eq, rcon]};
rc # $refuted AND rcon.po # NIL =>
{x: Solvee ← NARROW[Car[Car[rcon.po]]];
rcon.po ← Cdr[rcon.po];
[eq, rc] ← RealSolver.IsPositive[x, rcon, eq]}
ENDCASE => EXIT ENDLOOP;
IF rc # $refuted AND rcon.pr # NIL
THEN {rc ← $close; NewtonRaphson[]}}; --end of SolveLoop
NewtonRaphson: PROC;
Normalize: PROC [f: JS.Formula, defs:REF] RETURNS [g: Value, vl: JS.Varlist]
= {h: Value ← NIL;
g ← NIL;
vl ← NIL;
-- h and g are lists of formulas; vl is a list of variables.
-- h contains conjuncts of f that remain to be normalized;
-- g contains the normalization as it is built up.
DO SELECT TRUE FROM
-- invariant: Let f0 be the original formula f. Then f0 is equivalent to
--
-- (E vl: f and g and h),
--
-- wherein the formula lists h and g represent the conjunctions of their elements.
-- Also, all formulas on g are atomic predicates applied to variables. At the conclusion
-- if the loop we will have h = nil and f is an atomic predicate applied to variables,
-- hence the postcondition is established after the loop by g ← Cons[f, g].
-- The variables on vl are all created by gensym, so we have f0 = (E vl: f0).
JS.IsConjunction[f] =>
{h ← Cons[JS.LHSOfConjunction[f], h];
f ← JS.RHSOfConjunction[f]};
-- (f1 and f2) and g and h == f2 and g and (f1 and h)
JS.IsParenthesized[f] => f ← JS.ContentsOfParentheses[f];
-- (f1) == f1
JS.IsQuantification[f] AND JS.QuantifierOfQuantification[f] = JS.ex =>
{vl2: JS.Varlist ← JS.QuantifierVarlistOfQuantification[f];
f ← JS.QuantifieeOfQuantification[f];
WHILE vl2 # NIL DO
{temp: JS.Variable ← JS.Gensym[];
vl ← Cons[temp, vl];
f ← Subst[f, Car[vl2], temp];
vl2 ← Cdr[vl2]}
ENDLOOP};
-- (E vl: (E vl2: f) and g and h)
-- == {if gl2 is a list of distinct symbols of the same length as vl2}
-- (E vl: (E gl2: f(vl2:gl2)) and g and h)
-- == {if no var in gl2 is free in g or h
-- (E vl, gl2: f(vl2:gl2) and g and h)
--
-- The loop above constructs the concatenation of gl2 and vl by repeated conses
-- and simultaneously constructs f(vl2:gl2) by repeated substitutions.
JS.IsAtomicFormula[f] AND JS.PredOfAtomicFormula[f] = JS.eq AND
JS.IsVar[Car[JS.TermlistOfAtomicFormula[f]]] AND
LevelOneTerm[Cadr[JS.TermlistOfAtomicFormula[f]]] AND
NOT JS.IsConstant[Cadr[JS.TermlistOfAtomicFormula[f]]] =>
-- I.e., if f is an equality between a variable and a function applied to a list of variables
{lhs: JS.Variable = Car[JS.TermlistOfAtomicFormula[f]];
rhs: JS.Term = Cadr[JS.TermlistOfAtomicFormula[f]];
fun: JS.FunName = JS.FunctionOfTerm[rhs];
args: JS.Termlist = JS.TermlistOfTerm[rhs];
def: JS.FunDef = JunoLookup.GetFunDef[fun, defs];
formals: JS.Varlist ← JS.VarlistOfFunDef[def];
result: JS.Variable ← JS.ResultnameOfFunDef[def];
body: JS.Formula ← JS.BodyOfFunDef[def];
f ← MapSubst[body, Cons[result, formals], Cons[lhs, args]]};
-- with f defined by f(formals) = result == body , we have
--
-- lhs = f(args) == body(result, formals : lhs, args).
--
-- Note that the guard is stronger than logically necessary: we do not
-- use this operation unless args is a list of variables. This is to
-- guarantee that the substitution does not blow up the size of body .
JS.IsAtomicFormula[f] AND JS.PredOfAtomicFormula[f] = JS.eq AND
JS.IsVar[Cadr[JS.TermlistOfAtomicFormula[f]]] AND
LevelOneTerm[Car[JS.TermlistOfAtomicFormula[f]]] AND
NOT JS.IsConstant[Car[JS.TermlistOfAtomicFormula[f]]] =>
{tl: JS.Termlist ← JS.TermlistOfAtomicFormula[f];
newtl: JS.Termlist ← Cons[Cadr[tl], Cons[Car[tl], NIL]];
-- newtl = reverse(tl)
f ← JS.MakeAtomicFormula[JS.eq, newtl]};
-- f(varlist) = x == x = f(varlist)
-- termination of this loop depends on the next cases being below the two above
JS.IsAtomicFormula[f] AND (NOT IsVarlist[JS.TermlistOfAtomicFormula[f]]) =>
{temp: JS.Variable ← JS.Gensym[];
t: JS.Term;
pred: JS.PredName ← JS.PredOfAtomicFormula[f];
tl: JS.Termlist ← JS.TermlistOfAtomicFormula[f];
[tl, t] ← SwapVarForProperTerm[tl, temp];
-- this finds the first non-variable in tl, replaces it by temp,
-- sets tl to be the new list, and t to be the term that was replaced.
f ← JS.MakeAtomicFormula[pred, tl];
IF JS.IsConstant[t]
THEN h ← Cons[LIST[LIST[JS.constant, t], temp], h]
ELSE h ← Cons[JS.MakeAtomicFormula[JS.eq, Cons[temp, Cons[t, NIL]]], h];
vl ← Cons[temp, vl]};
-- pred(... t ...) == (E temp: pred(... temp ...) and temp = t)
JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]]
AND NOT JS.KernelPredicate[JS.PredOfAtomicFormula[f]] =>
{def: JS.PredDef ← JunoLookup.GetPredDef[Car[f], defs];
parameters: JS.Varlist ← JS.VarlistOfPredDef[def];
body: JS.Formula ← JS.BodyOfPredDef[def];
f ← MapSubst[body, parameters, JS.TermlistOfAtomicFormula[f]]};
-- With p defined by p(parameters) = body , we have p(tl) == body(parameters: tl).
JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]]
AND JS.KernelPredicate[JS.PredOfAtomicFormula[f]] AND h # NIL =>
{g ← Cons[f, g]; f ← Car[h]; h ← Cdr[h]};
-- g and f and (h1 and h2) == (g and f) and h1 and h2
ENDCASE => EXIT ENDLOOP;
-- At this point f is an application of a Kernel predicate to a list of Level Zero terms,
-- and h is NIL. f may also be a constant predicate T or F.
IF f # JS.true
AND f # JS.false
AND NOT (JS.IsAtomicFormula[f] AND IsVarlist[JS.TermlistOfAtomicFormula[f]] AND h = NIL)
THEN ERROR;
g ← Cons[f, g]}; -- end of Normalize
LevelOneTerm: PROC [t: JS.Term] RETURNS [BOOLEAN]
= {RETURN[IsVarlist[JS.TermlistOfTerm[t]]]};
IsVarlist: PROC [tl: JS.Termlist] RETURNS [BOOLEAN]
= {WHILE tl # NIL AND JS.IsVar[Car[tl]] DO tl ← Cdr[tl] ENDLOOP;
RETURN [tl = NIL]};
SwapVarForProperTerm: PROC[f:JS.Termlist, v: JS.Variable]
RETURNS [g: JS.Termlist, t: JS.Term] =
{l: JS.Termlist ← NIL;
WHILE JS.IsVar[Car[f]] DO l ← Cons[Car[f], l]; f ← Cdr[f] ENDLOOP;
t ← Car[f];
f ← Cons[v, Cdr[f]];
WHILE l # NIL DO f ← Cons[Car[l], f]; l ← Cdr[l] ENDLOOP;
g ← f};
ConstructSolution:
PROC[vl: JS.Varlist, alin: JB.Alist, rcon: RealSolver.Context, lcon: PairSolver.Context]
RETURNS [alout: JB.Alist] =
{alout ← JB.EmptyBinding[];
WHILE vl # NIL DO
temp: LinearSolver.Unknown = NARROW[JB.Lookup[Car[vl], alin], Solvee].tableau;
alout ← JB.NewBind[
alout,
Car[vl],
SELECT TRUE FROM
temp = NIL => NIL,
temp # NIL => NEW[REAL ← LinearSolver.Solution[temp]]
ENDCASE => ERROR];
vl ← Cdr[vl]
ENDLOOP
};
END.