org.jcsp.util.filter

Class FilterHolder

java.lang.Object

org.jcsp.util.filter.FilterHolder

class FilterHolder
extends java.lang.Object

Storage scheme for a set of filters that is dynamically sized and supports insert and remove operations to keep the filters in a contiguous block.

Field Summary

Fields

Modifier and Type	Field and Description
private int	count Number of filters currently installed.
private Filter[]	filters The array of filters.

Constructor Summary

Constructors

Constructor and Description
FilterHolder() Constructs a new FilterHolder with an intial capacity of 2.
FilterHolder(int initialSize) Constructs a new FilterHolder with the given initial capacity.

Method Summary

Modifier and Type	Method and Description
void	addFilter(Filter filter) Adds a filter to the end of the array, possibly enlarging it if it is full.
void	addFilter(Filter filter, int index) Adds a filter at the given index.
private void	compact() Shrinks the array to save space if it is 75% empty.
Filter	getFilter(int index) Returns a filter at the given array index.
int	getFilterCount() Returns the number of filters current installed.
private void	makeSpace() Enlarges the size of the array to make room for more filters.
void	removeFilter(Filter filter) Removes a filter from the set.
void	removeFilter(int index) Removes a filter at a given index.

Methods inherited from class java.lang.Object

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

Field Detail

filters

private Filter[] filters

The array of filters. The installed filters are in a block at the start of the array.

count

private int count

Number of filters currently installed.

Constructor Detail

FilterHolder

FilterHolder()

Constructs a new FilterHolder with an intial capacity of 2.

FilterHolder

FilterHolder(int initialSize)

Constructs a new FilterHolder with the given initial capacity.

Parameters:

initialSize - the initial size for the array.

Method Detail

addFilter

public void addFilter(Filter filter)

Adds a filter to the end of the array, possibly enlarging it if it is full.

Parameters:

filter - the filter to add.

addFilter

public void addFilter(Filter filter,
                      int index)

Adds a filter at the given index. If the index is past the end of the array, the filter is placed at the end of the array. If the index is in use, filter is inserted, shifting the existing ones. If necessary, the array may be enlarged.

Parameters:

filter - the filter to add.

index - the position to add the filter.

removeFilter

public void removeFilter(Filter filter)

Removes a filter from the set. The first filter, f, satisfying the condition f.equals (filter) is removed and the remaining filters shifted to close the gap.

Parameters:

filter - the filter to remove.

removeFilter

public void removeFilter(int index)

Removes a filter at a given index. The remaining filters are shifted to close the gap.

Parameters:

index - the array index to remove the filter.

getFilter

public Filter getFilter(int index)

Returns a filter at the given array index.

getFilterCount

public int getFilterCount()

Returns the number of filters current installed.

makeSpace

private void makeSpace()

Enlarges the size of the array to make room for more filters. Currently the array is doubled in size.

compact

private void compact()

Shrinks the array to save space if it is 75% empty.