-- 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.

}.