<> <> <> <> LinearSolver: CEDAR DEFINITIONS = BEGIN RowMax: INT = 100; ColMax: INT = 100; Row: TYPE = [0 .. RowMax); Col: TYPE = [0 .. ColMax); Tableau: TYPE = REF TableauRec; TableauRec: TYPE = RECORD [ n: [0 .. RowMax], m: [0 .. ColMax], maxN: [0 .. RowMax], maxM: [0 .. ColMax], a: REF ARRAY Row OF ARRAY Col OF REAL, <> x: REF ARRAY Col OF Unknown, y: REF ARRAY Row OF Unknown, unity: Unknown, satisfiable: BOOL, nameCount: NAT ]; Unknown: TYPE = REF UnknownRec; UnknownRec: TYPE = RECORD [r, name: REF, i, j: INT, restricted: BOOL]; <> <> <> <> NewUnknown: PROCEDURE [t: Tableau, name: REF] RETURNS [Unknown]; <> Push, Pop: PROCEDURE; C: PROCEDURE [x: LinearMonomial] RETURNS [r: REF]; AssertZero: PROCEDURE [t: Tableau, c: Constraint, propEQ: PropEQProc _ NIL]; <> AssertZero2: PROCEDURE [t: Tableau, c1: REAL, v1: Unknown, c2: REAL, v2: Unknown, propEQ: PropEQProc _ NIL]; <> AssertZero3: PROCEDURE [t: Tableau, c1: REAL, v1: Unknown, c2: REAL, v2: Unknown, c3: REAL, v3: Unknown, propEQ: PropEQProc _ NIL]; <> AssertGEZero: PROCEDURE [t: Tableau, c: Constraint, propEQ: PropEQProc _ NIL]; <= 0>> AssertGEZero2: PROCEDURE [t: Tableau, c1: REAL, v1: Unknown, c2: REAL, v2: Unknown, propEQ: PropEQProc _ NIL]; <= 0>> AssertGEZero3: PROCEDURE [t: Tableau, c1: REAL, v1: Unknown, c2: REAL, v2: Unknown, c3: REAL, v3: Unknown, propEQ: PropEQProc _ NIL]; <= 0>> Restrict: PROCEDURE [t: Tableau, v: Unknown, propEQ: PropEQProc _ NIL]; <= 0>> PropEQProc: TYPE = PROCEDURE [t: Tableau, u, v: Unknown]; Maximize: PROCEDURE [t: Tableau, v: Unknown] RETURNS [unbounded: BOOLEAN]; <> Satisfiable: PROCEDURE [t: Tableau] RETURNS [BOOL]; Solution: PROCEDURE [t: Tableau, v: Unknown] -- to be called only if Satisfiable[] -- RETURNS [REAL]; <> Constraint: TYPE = LIST OF REF -- to LinearMonomial --; LinearMonomial: TYPE = RECORD [coefficient: REAL, unknown: Unknown]; <<"unity" is an Unknown representing one unit. It exists before any Unknowns are created. Solution[unity] = 1 invariantly. The constraint represented by a list of linear monomials is that the some of them is zero. Thus the constraint x+x=4 would be asserted Assert[[[2, x], [-4, unity]]], which asserts that 2*x+(-4)*unity = 0, or that x+x=4.>> <> <<-- Madman's code.>> <<-- BEGIN OPEN LinearSolver;>> <<-- x: Unknown;>> <<-- WHILE TRUE DO>> <<-- Push[];>> <<-- x := NewUnknown[];>> <<-- Assert[LIST[[2, x], [-4, unity]]];>> <<-- IF NOT Satisfiable[] OR Solution[x] # 2 THEN SIGNAL Madman;>> <<-- Pop[]>> <<-- ENDLOOP>> <<-- END.>> Init: PROCEDURE RETURNS [t: Tableau]; -- Client must call it once before using the solver. END. -- of LinearSolver.mesa