-- 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}}; }.  JJ  >