pipe.modules.invariantAnalysis
Class IntMatrix

java.lang.Object
  |
  +--pipe.modules.invariantAnalysis.IntMatrix

public class IntMatrix

extends java.lang.Object

Field Summary

private int[][]	A Array for internal storage of elements.
private int	m Row and column dimensions.
private int	n Row and column dimensions.

Constructor Summary

IntMatrix(int[][] A)
Construct a matrix from a 2-D array.

IntMatrix(int[][] A, int m, int n)
Construct a matrix quickly without checking arguments.

IntMatrix(int[] vals, int m)
Construct a matrix from a one-dimensional packed array

IntMatrix(int m, int n)
Construct an m-by-n matrix of zeros.

IntMatrix(int m, int n, int s)
Construct an m-by-n constant matrix.

Method Summary

IntMatrix	appendVector(IntMatrix X) Append a column matrix (vector) to the right of another matrix.
int	cardinalityCondition() Check if a matrix has a row that satisfies the cardinality condition 1.1.b of the algorithm.
int	cardinalityOne() Find the column index of the element in the pPlus or pMinus set, where pPlus or pMinus has cardinality == 1.
boolean	checkCase11() Check if a matrix satisfies condition 1.1 of the algorithm.
private void	checkMatrixDimensions(IntMatrix B) Check if size(A) == size(B)
java.lang.Object	clone() Clone the IntMatrix object.
int[]	colsToUpdate() Find the comlumn indices to be changed by linear combination.
static IntMatrix	constructWithCopy(int[][] A) Construct a matrix from a copy of a 2-D array.
IntMatrix	copy() Make a deep copy of a matrix
IntMatrix	divideEquals(int s) Divide a matrix by an int in place, A = s*A
IntMatrix	eliminateCol(int toDelete) Eliminate a column from the matrix, column index is toDelete
int	findNonMinimal() Find a column with non-minimal support.
int[]	findRemainingNZCoef(int h) Find the coefficients corresponding to column indices of all but the first non zero elements of row h.
int[]	findRemainingNZIndices(int h) Find the column indices of all but the first non zero elements of row h.
int	firstNonZeroElementIndex(int h) Find the column index of the first non zero element of row h.
int	firstNonZeroRowIndex() Find the first non-zero row of a matrix.
int	gcd() Find the greatest common divisor of a column matrix (vector) of integers.
private int	gcd2(int a, int b) Find the greatest common divisor of 2 integers.
int	get(int i, int j) Get a single element.
int[][]	getArray() Access the internal two-dimensional array.
int[][]	getArrayCopy() Copy the internal two-dimensional array.
int	getColumnDimension() Get column dimension.
int[]	getColumnPackedCopy() Make a one-dimensional column packed copy of the internal array.
IntMatrix	getMatrix(int[] r, int[] c) Get a submatrix.
IntMatrix	getMatrix(int[] r, int j0, int j1) Get a submatrix.
IntMatrix	getMatrix(int i0, int i1, int[] c) Get a submatrix.
IntMatrix	getMatrix(int i0, int i1, int j0, int j1) Get a submatrix.
int[]	getNegativeIndices(int rowNo) For row rowNo of the matrix received return the column indices of all the negative elements
int[]	getPositiveIndices(int rowNo) For row rowNo of the matrix received return the column indices of all the positive elements
int	getRowDimension() Get row dimension.
int[]	getRowPackedCopy() Make a one-dimensional row packed copy of the internal array.
boolean	hasNegativeElements() Find if a column vector has negative elements.
static IntMatrix	identity(int m, int n) Generate identity matrix]
boolean	isCovered() Find if a matrix of invariants is covered.
boolean	isZeroMatrix() Check if a matrix is all zeros.
boolean	isZeroRow(int r) isZeroRow returns true if the ith row is all zeros
void	linearlyCombine(int k, int[] alpha, int[] j, int[] beta) Add a linear combination of column k to columns in array j[].
void	linearlyCombine(int k, int chk, int[] j, int[] jC) Add a linear combination of column k to columns in array j[].
IntMatrix	minus(IntMatrix B) C = A - B
IntMatrix	minusEquals(IntMatrix B) A = A - B
IntMatrix	nonZeroIndices() Form a matrix with columns the row indices of non-zero elements.
IntMatrix	plus(IntMatrix B) C = A + B
IntMatrix	plusEquals(IntMatrix B) A = A + B
void	print(int w, int d) Print the matrix to stdout.
void	print(java.text.NumberFormat format, int width) Print the matrix to stdout.
void	print(java.io.PrintWriter output, int w, int d) Print the matrix to the output stream.
void	print(java.io.PrintWriter output, java.text.NumberFormat format, int width) Print the matrix to the output stream.
void	printArray(int[] a) Used to display intermiadiate results for checking
java.lang.String	printString(int w, int d) Print the matrix to a string.
int	rowWithNegativeElement() Find the first row with a negative element in a matrix.
void	set(int i, int j, int s) Set a single element.
void	setMatrix(int[] r, int[] c, IntMatrix X) Set a submatrix.
void	setMatrix(int[] r, int j0, int j1, IntMatrix X) Set a submatrix.
void	setMatrix(int i0, int i1, int[] c, IntMatrix X) Set a submatrix.
void	setMatrix(int i0, int i1, int j0, int j1, IntMatrix X) Set a submatrix.
IntMatrix	timesEquals(int s) Multiply a matrix by an int in place, A = s*A
IntMatrix	transpose() Matrix transpose.
IntMatrix	uminus() Unary minus
int	vectorTimes(IntMatrix B) Multiply a row matrix by a column matrix, A = s*A

Methods inherited from class java.lang.Object

, equals, finalize, getClass, hashCode, notify, notifyAll, registerNatives, toString, wait, wait, wait

Field Detail

A

private int[][] A

Array for internal storage of elements.

m

private int m

Row and column dimensions.

n

private int n

Row and column dimensions.

Constructor Detail

IntMatrix

public IntMatrix(int m,
                 int n)

Construct an m-by-n matrix of zeros.

Parameters:

m - Number of rows.

n - Number of colums.

IntMatrix

public IntMatrix(int m,
                 int n,
                 int s)

Construct an m-by-n constant matrix.

Parameters:

m - Number of rows.

n - Number of colums.

s - Fill the matrix with this scalar value.

IntMatrix

public IntMatrix(int[][] A)

Construct a matrix from a 2-D array.

Parameters:

A - Two-dimensional array of integers.

Throws:

java.lang.IllegalArgumentException - All rows must have the same length

See Also:

constructWithCopy(int[][])

IntMatrix

public IntMatrix(int[][] A,
                 int m,
                 int n)

Construct a matrix quickly without checking arguments.

Parameters:

A - Two-dimensional array of integers.

m - Number of rows.

n - Number of colums.

IntMatrix

public IntMatrix(int[] vals,
                 int m)

Construct a matrix from a one-dimensional packed array

Parameters:

vals - One-dimensional array of integers, packed by columns (ala Fortran).

m - Number of rows.

Throws:

java.lang.IllegalArgumentException - Array length must be a multiple of m.

Method Detail

appendVector

public IntMatrix appendVector(IntMatrix X)

Append a column matrix (vector) to the right of another matrix.

Parameters:

X - Column matrix (vector) to append.

Returns:

The matrix with the column vector appended to the right.

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

cardinalityCondition

public int cardinalityCondition()

Check if a matrix has a row that satisfies the cardinality condition 1.1.b of the algorithm.

Returns:

True if the matrix satisfies the condition and linear combination of columns followed by column elimination is required.

cardinalityOne

public int cardinalityOne()

Find the column index of the element in the pPlus or pMinus set, where pPlus or pMinus has cardinality == 1.

Returns:

The column index, -1 if unsuccessful (this shouldn't happen under normal operation).

checkCase11

public boolean checkCase11()

Check if a matrix satisfies condition 1.1 of the algorithm.

Returns:

True if the matrix satisfies the condition and column elimination is required.

colsToUpdate

public int[] colsToUpdate()

Find the comlumn indices to be changed by linear combination.

Returns:

An array of integers, these are the indices increased by 1 each.

constructWithCopy

public static IntMatrix constructWithCopy(int[][] A)

Construct a matrix from a copy of a 2-D array.

Parameters:

A - Two-dimensional array of integers.

Returns:

The copied matrix.

Throws:

java.lang.IllegalArgumentException - All rows must have the same length

copy

public IntMatrix copy()

Make a deep copy of a matrix

Returns:

The matrix copy.

clone

public java.lang.Object clone()

Clone the IntMatrix object.

Overrides:

clone in class java.lang.Object

Returns:

The clone of the current matrix.

eliminateCol

public IntMatrix eliminateCol(int toDelete)

Eliminate a column from the matrix, column index is toDelete

Parameters:

toDelete - The column number to delete.

Returns:

The matrix with the required row deleted.

getArray

public int[][] getArray()

Access the internal two-dimensional array.

Returns:

Pointer to the two-dimensional array of matrix elements.

getArrayCopy

public int[][] getArrayCopy()

Copy the internal two-dimensional array.

Returns:

Two-dimensional array copy of matrix elements.

getColumnPackedCopy

public int[] getColumnPackedCopy()

Make a one-dimensional column packed copy of the internal array.

Returns:

Matrix elements packed in a one-dimensional array by columns.

getRowPackedCopy

public int[] getRowPackedCopy()

Make a one-dimensional row packed copy of the internal array.

Returns:

Matrix elements packed in a one-dimensional array by rows.

getRowDimension

public int getRowDimension()

Get row dimension.

Returns:

The number of rows.

getColumnDimension

public int getColumnDimension()

Get column dimension.

Returns:

The number of columns.

firstNonZeroRowIndex

public int firstNonZeroRowIndex()

Find the first non-zero row of a matrix.

Returns:

Row index (starting from 0 for 1st row) of the first row from top that is not only zeros, -1 of there is no such row.

nonZeroIndices

public IntMatrix nonZeroIndices()

Form a matrix with columns the row indices of non-zero elements.

Returns:

The matrix with columns the row indices of non-zero elements. First row has index 1.

findNonMinimal

public int findNonMinimal()

Find a column with non-minimal support.

Returns:

The column index that has non-minimal support, -1 if there is none.

hasNegativeElements

public boolean hasNegativeElements()

Find if a column vector has negative elements.

Returns:

True or false.

firstNonZeroElementIndex

public int firstNonZeroElementIndex(int h)

Find the column index of the first non zero element of row h.

Parameters:

h - The row to look for the non-zero element in

Returns:

Column index (starting from 0 for 1st column) of the first non-zero element of row h, -1 if there is no such column.

findRemainingNZIndices

public int[] findRemainingNZIndices(int h)

Find the column indices of all but the first non zero elements of row h.

Parameters:

h - The row to look for the non-zero element in

Returns:

Array of ints of column indices (starting from 0 for 1st column) of all but the first non-zero elements of row h.

findRemainingNZCoef

public int[] findRemainingNZCoef(int h)

Find the coefficients corresponding to column indices of all but the first non zero elements of row h.

Parameters:

h - The row to look for the non-zero coefficients in

Returns:

Array of ints of coefficients of all but the first non-zero elements of row h.

get

public int get(int i,
               int j)

Get a single element.

Parameters:

i - Row index.

j - Column index.

Returns:

A(i,j)

Throws:

ArrayIndexOutOfBoundsException -

getMatrix

public IntMatrix getMatrix(int i0,
                           int i1,
                           int j0,
                           int j1)

Get a submatrix.

Parameters:

i0 - Initial row index

i1 - Final row index

j0 - Initial column index

j1 - Final column index

Returns:

A(i0:i1,j0:j1)

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

getMatrix

public IntMatrix getMatrix(int[] r,
                           int[] c)

Get a submatrix.

Parameters:

r - Array of row indices.

c - Array of column indices.

Returns:

A(r(:),c(:))

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

getMatrix

public IntMatrix getMatrix(int i0,
                           int i1,
                           int[] c)

Get a submatrix.

Parameters:

i0 - Initial row index

i1 - Final row index

c - Array of column indices.

Returns:

A(i0:i1,c(:))

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

getMatrix

public IntMatrix getMatrix(int[] r,
                           int j0,
                           int j1)

Get a submatrix.

Parameters:

r - Array of row indices.

j0 - Initial column index

j1 - Final column index

Returns:

A(r(:),j0:j1)

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

getNegativeIndices

public int[] getNegativeIndices(int rowNo)

For row rowNo of the matrix received return the column indices of all the negative elements

Parameters:

rowNo - row iside the Matrix to check for -ve elements

Returns:

Integer array of indices of negative elements.

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

getPositiveIndices

public int[] getPositiveIndices(int rowNo)

For row rowNo of the matrix received return the column indices of all the positive elements

Parameters:

rowNo - row iside the Matrix to check for +ve elements

Returns:

The integer array of indices of all positive elements.

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

isZeroMatrix

public boolean isZeroMatrix()

Check if a matrix is all zeros.

Returns:

true if all zeros, false otherwise

isZeroRow

public boolean isZeroRow(int r)

isZeroRow returns true if the ith row is all zeros

Parameters:

r - row to check for full zeros.

Returns:

true if the row is full of zeros.

isCovered

public boolean isCovered()

Find if a matrix of invariants is covered.

Returns:

true if it is covered, false otherwise.

linearlyCombine

public void linearlyCombine(int k,
                            int chk,
                            int[] j,
                            int[] jC)

Add a linear combination of column k to columns in array j[].

Parameters:

k - Column index to add.

chk - Coefficient of col to add

j - Array of column indices to add to.

jC - Array of coefficients of column indices to add to.

Throws:

ArrayIndexOutOfBoundsException -

linearlyCombine

public void linearlyCombine(int k,
                            int[] alpha,
                            int[] j,
                            int[] beta)

Add a linear combination of column k to columns in array j[].

Parameters:

k - Column index to add.

alpha - Array of coefficients of col to add

j - Array of column indices to add to.

beta - Array of coefficients of column indices to add to.

Throws:

ArrayIndexOutOfBoundsException -

rowWithNegativeElement

public int rowWithNegativeElement()

Find the first row with a negative element in a matrix.

Returns:

Row index (starting from 0 for 1st row) of the first row from top that is has a negative element, -1 of there is no such row.

set

public void set(int i,
                int j,
                int s)

Set a single element.

Parameters:

i - Row index.

j - Column index.

s - A(i,j).

Throws:

ArrayIndexOutOfBoundsException -

setMatrix

public void setMatrix(int i0,
                      int i1,
                      int j0,
                      int j1,
                      IntMatrix X)

Set a submatrix.

Parameters:

i0 - Initial row index

i1 - Final row index

j0 - Initial column index

j1 - Final column index

X - A(i0:i1,j0:j1)

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

setMatrix

public void setMatrix(int[] r,
                      int[] c,
                      IntMatrix X)

Set a submatrix.

Parameters:

r - Array of row indices.

c - Array of column indices.

X - A(r(:),c(:))

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

setMatrix

public void setMatrix(int[] r,
                      int j0,
                      int j1,
                      IntMatrix X)

Set a submatrix.

Parameters:

r - Array of row indices.

j0 - Initial column index

j1 - Final column index

X - A(r(:),j0:j1)

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

setMatrix

public void setMatrix(int i0,
                      int i1,
                      int[] c,
                      IntMatrix X)

Set a submatrix.

Parameters:

i0 - Initial row index

i1 - Final row index

c - Array of column indices.

X - A(i0:i1,c(:))

Throws:

ArrayIndexOutOfBoundsException - Submatrix indices

transpose

public IntMatrix transpose()

Matrix transpose.

Returns:

A'

gcd

public int gcd()

Find the greatest common divisor of a column matrix (vector) of integers.

Returns:

The gcd of the column matrix.

gcd2

private int gcd2(int a,
                 int b)

Find the greatest common divisor of 2 integers.

Parameters:

a - The first integer.

b - The second integer.

Returns:

The gcd of the column

uminus

public IntMatrix uminus()

Unary minus

Returns:

-A

plus

public IntMatrix plus(IntMatrix B)

C = A + B

Parameters:

B - another matrix

Returns:

A + B

plusEquals

public IntMatrix plusEquals(IntMatrix B)

A = A + B

Parameters:

B - another matrix

Returns:

A + B

minus

public IntMatrix minus(IntMatrix B)

C = A - B

Parameters:

B - another matrix

Returns:

A - B

minusEquals

public IntMatrix minusEquals(IntMatrix B)

A = A - B

Parameters:

B - another matrix

Returns:

A - B

timesEquals

public IntMatrix timesEquals(int s)

Multiply a matrix by an int in place, A = s*A

Parameters:

s - int multiplier

Returns:

replace A by s*A

vectorTimes

public int vectorTimes(IntMatrix B)

Multiply a row matrix by a column matrix, A = s*A

Parameters:

B - column vector

Returns:

product of row vector A by column vector B

divideEquals

public IntMatrix divideEquals(int s)

Divide a matrix by an int in place, A = s*A

Parameters:

s - int divisor

Returns:

replace A by A/s

identity

public static IntMatrix identity(int m,
                                 int n)

Generate identity matrix]

Parameters:

m - Number of rows.

n - Number of colums.

Returns:

An m-by-n matrix with ones on the diagonal and zeros elsewhere.

print

public void print(int w,
                  int d)

Print the matrix to stdout. Line the elements up in columns with a Fortran-like 'Fw.d' style format.

Parameters:

w - Column width.

d - Number of digits after the decimal.

printString

public java.lang.String printString(int w,
                                    int d)

Print the matrix to a string. Line the elements up in columns with a Fortran-like 'Fw.d' style format.

Parameters:

w - Column width.

d - Number of digits after the decimal.

Returns:

The formated string to output.

print

public void print(java.io.PrintWriter output,
                  int w,
                  int d)

Print the matrix to the output stream. Line the elements up in columns with a Fortran-like 'Fw.d' style format.

Parameters:

output - Output stream.

w - Column width.

d - Number of digits after the decimal.

print

public void print(java.text.NumberFormat format,
                  int width)

Print the matrix to stdout. Line the elements up in columns. Use the format object, and right justify within columns of width characters. Note that if the matrix is to be read back in, you probably will want to use a NumberFormat that is set to UK Locale.

Parameters:

format - A Formatting object for individual elements.

width - Field width for each column.

See Also:

DecimalFormat.setDecimalFormatSymbols(java.text.DecimalFormatSymbols)

print

public void print(java.io.PrintWriter output,
                  java.text.NumberFormat format,
                  int width)

Print the matrix to the output stream. Line the elements up in columns. Use the format object, and right justify within columns of width characters. Note that is the matrix is to be read back in, you probably will want to use a NumberFormat that is set to US Locale.

Parameters:

output - the output stream.

format - A formatting object to format the matrix elements

width - Column width.

See Also:

DecimalFormat.setDecimalFormatSymbols(java.text.DecimalFormatSymbols)

checkMatrixDimensions

private void checkMatrixDimensions(IntMatrix B)

Check if size(A) == size(B)

Parameters:

B - The matrix to check the dimensions.

printArray

public void printArray(int[] a)

Used to display intermiadiate results for checking

Parameters:

a - The array of integers to print.