-- RealSolverImpl.mesa
-- August 30, 1983 3:46 pm
-- Last Edited by: Gnelson, December 12, 1983 12:53 am

DIRECTORY Lisp, JunoSolver, SolverCommon, RealSolver, LinearSolver;

RealSolverImpl: PROGRAM IMPORTS LinearSolver EXPORTS RealSolver =
{OPEN SolverCommon, RealSolver, Lisp;

NewContext: PUBLIC PROC RETURNS [Context] =
{LinearSolver.Init[]; RETURN [NEW[ContextRec ← [su:NIL, po:NIL, pr:NIL, b:NIL]]]};

LM: PROC[c: REAL, u: LinearSolver.Unknown] RETURNS [REF LinearSolver.LinearMonomial] =
{RETURN [NEW[LinearSolver.LinearMonomial ← [c, u]]]};

Merge: PUBLIC PROC[x: Solvee, y: Solvee, eqin: Lisp.Value, rcon: Context]
RETURNS [eqout: Lisp.Value, rc: ResultCode] =
{eqout ← eqin;
rc ← $solved;
IF x.tableau = NIL THEN {x.tableau ← LinearSolver.NewUnknown[x.name]; x.tableau.r ← x};
IF y.tableau = NIL THEN {y.tableau ← LinearSolver.NewUnknown[y.name]; y.tableau.r ← y};
{--P: PROC[u, v: Tableau.Variable] = {eqout ← Cons[Cons[u.r, Cons[v.r, NIL]], eqout]};
LinearSolver.Assert[LIST[LM[1, x.tableau], LM[-1, y.tableau]]]};
IF NOT LinearSolver.Satisfiable[] THEN rc ← $refuted};

Fix: PUBLIC PROC[u: REF, x: Solvee, eqin: Lisp.Value, rcon: Context]
RETURNS [eqout: Lisp.Value, rc: ResultCode] =
{eqout ← eqin;
rc ← $solved;
IF x.tableau = NIL THEN {x.tableau ← LinearSolver.NewUnknown[x.name]; x.tableau.r ← x};
{--P: PROC[u, v: Tableau.Variable] = {eqout ← Cons[Cons[u.r, Cons[v.r, NIL]], eqout]};
LinearSolver.Assert[LIST[LM[-1, x.tableau], LM[Convert[u], LinearSolver.unity]]]};
IF NOT LinearSolver.Satisfiable[] THEN rc ← $refuted};

Convert: PROC[u: REF] RETURNS [REAL] =
{WITH u SELECT FROM
rr: REF REAL => RETURN[rr^];
ri: REF INT => RETURN[ri^]
ENDCASE => ERROR};

IsSumOf: PUBLIC PROC[x, y, z: Solvee, eqin: Lisp.Value, rcon: Context]
RETURNS [eqout: Lisp.Value, rc: ResultCode] =
{eqout ← eqin;
rc ← $solved;
IF x.tableau = NIL THEN {x.tableau ← LinearSolver.NewUnknown[x.name]; x.tableau.r ← x};
IF y.tableau = NIL THEN {y.tableau ← LinearSolver.NewUnknown[y.name]; y.tableau.r ← y};
IF z.tableau = NIL THEN {z.tableau ← LinearSolver.NewUnknown[z.name]; z.tableau.r ← z};
{--P: PROC[u, v: Tableau.Variable] = {eqout ← Cons[Cons[u.r, Cons[v.r, NIL]], eqout]};
LinearSolver.Assert[LIST[LM[1, x.tableau], LM[-1, y.tableau], LM[-1, z.tableau]]]};
IF NOT LinearSolver.Satisfiable[] THEN rc ← $refuted};

IsPositive: PUBLIC PROC[x: Solvee, rcon: Context, eqin: Lisp.Value]
RETURNS [eqout: Lisp.Value, rc: ResultCode] =
{eqout ← eqin;
rc ← $solved;
IF x.tableau = NIL THEN {x.tableau ← LinearSolver.NewUnknown[x.name]; x.tableau.r ← x};
{--P: PROC[u, v: Tableau.Variable] = {eqout ← Cons[Cons[u.r, Cons[v.r, NIL]], eqout]};
--Tableau.Restrict[x.tableau, P]};
IF NOT LinearSolver.Satisfiable[] THEN rc ← $refuted}};

}.