-- Tableau.mesa -- Last Edited by: Gnelson, November 10, 1983 2:45 pm Tableau: DEFINITIONS = { Variable: TYPE = REF VariableRec; VariableRec: TYPE = RECORD [r: REF, i: INT, j: INT, restricted: BOOL]; -- r is for the client: Tableau does not use it. -- i is the index of the row owned by this variable, or -1 if it doesn't own a row -- j is the index of the column owned by this variable, or -1 if it doesn't own a column -- the unit variable, 1 if it is the unit variable, and the negative of the unit -- entry in its row if it owns a row. nrows: INT = 10; ncols: INT = 10; x: REF ARRAY [1 .. ncols] OF Variable; y: REF ARRAY [1 .. nrows] OF Variable; -- (A j: j in [1, m]: x(j).j = j) -- (A i: i in [1, n]: y(i).i = i) NewVariable: PROC RETURNS [Variable]; Init: PROC; -- client should throw away all Variables upon calling Init. Pivot: PROC[rowvar, colvar: Variable]; matrix: REF ARRAY[1 .. nrows] OF ARRAY[1 .. ncols] OF REAL; -- client may want to traverse the rows or columns of the tableau, so the -- underlying matrix is visible n, m: INT; -- n = current number of rows; m = current number of columns. unit: Variable; -- the variable that is implicitly constrained equal to 1. dcol: INT; -- in [0, m]; the largest index of a dead column. satisfiable: BOOL; -- Init sets this to TRUE. The Assert procedures may set it to FALSE. -- It is an error to call and Assert procedure when it is FALSE. -- The Assert procedures call PropEQ when they -- detect an equality between two variables. LinearMonomial: TYPE = RECORD [coef: REAL, var: Variable]; LinearForm: TYPE = LIST OF LinearMonomial; AssertZ: PROC[l: LinearForm, PropEQ: PROC[u, v: Variable]]; AssertZ2: PROC[c1, c2: REAL, v1, v2: Variable, PropEQ: PROC[u, v: Variable]]; -- constrains the Tableau so that c1*v1 + c2*v2 = 0. AssertZ3: PROC[c1, c2, c3: REAL, v1, v2, v3: Variable, PropEQ: PROC[u, v: Variable]]; -- constrains the tableau so that c1*v1 + c2*v2 + c3*v3 = 0. Restrict: PROC[v:Variable, PropEQ: PROC[u, v: Variable]]; -- constrains the tableau so that v ge 0. }.