kodkod.instance

Class TupleFactory

java.lang.Object

kodkod.instance.TupleFactory

public final class TupleFactory
extends Object

A factory class that facilitates creation of tuples and tuple sets drawn from a given universe. Only one factory per universe exists.

Author:

Emina Torlak

Specfields:

universe: Universe

Invariants:

no f: TupleFactory - this | f.universe = this.universe

Method Summary

Modifier and Type	Method and Description
TupleSet	allOf(int arity) Returns a set of all tuples of the given arity, drawn from this.universe.
TupleSet	area(Tuple upperLeft, Tuple lowerRight) Returns a tuple set that contains all tuples in the specified area of the n-dimensional space, where n is the arity of the argument tuples.
TupleSet	noneOf(int arity) Returns an initially empty tuple set of the given arity, based on this.universe.
TupleSet	range(Tuple from, Tuple to) Returns a tuple set that contains all tuples between from and to, inclusive.
TupleSet	setOf(Collection<Tuple> tuples) Returns a tuple set consisting of specified tuples.
TupleSet	setOf(int arity, IntSet tupleIndices) Returns a set of the given arity that contains all tuples whose indeces are contained in the given int set.
TupleSet	setOf(Object... atoms) Returns a set of tuples of arity 1, each of which wraps one of the given objects.
TupleSet	setOf(Tuple first, Tuple... rest) Returns a tuple set consisting of specified tuples.
Tuple	tuple(int arity, int index) Returns a tuple with the specified arity whose index in an arity-dimensional space over this.universe is given by the index parameter.
Tuple	tuple(List<?> atoms) Returns a tuple that contains the specified sequence of atoms, drawn from this.universe.
Tuple	tuple(Object... atoms) Returns a tuple that contains the specified sequence of atoms, drawn from this.universe.
Universe	universe() Returns the universe to which this factory belongs.

Methods inherited from class java.lang.Object

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

Method Detail

allOf

public TupleSet allOf(int arity)

Returns a set of all tuples of the given arity, drawn from this.universe.

Returns:

{ s: TupleSet | s.universe = this.universe && s.arity = arity && s.tuples = {t: Tuple | t.universe = this.universe && t.arity = arity} }

Throws:

IllegalArgumentException - arity < 1

area

public TupleSet area(Tuple upperLeft,
                     Tuple lowerRight)

Returns a tuple set that contains all tuples in the specified area of the n-dimensional space, where n is the arity of the argument tuples. For example, suppose that this.universe consists of atoms {atom0, atom1, atom2, atom3}, where atom0 has index 0, atom1 has index 1, etc. Calling this method with tuples [atom0, atom2] and [atom1, atom3] as the first and second arguments would result in the set {[atom0, atom2], [atom0,atom3], [atom1,atom2], [atom1, atom3]}. That is, the returned set consists of all points in the rectangle whose upper left corner is the point [atom0, atom2] and whose lower right corner is at [atom1, atom3].

Returns:

{s: TupleSet | s.arity = upperLeft.arity && s.universe = this.universe && s.tuples = {t: Tuple | all i: [0..s.arity) | this.universe.index(upperLeft.atoms[i]) <= this.universe.index(t.atoms[i]) <= this.universe.index(lowerRight.atoms[i]}}

Throws:

NullPointerException - upperLeft = null || lowerRight = null

IllegalArgumentException - upperLeft.arity != lowerRight.arity

IllegalArgumentException - lowerRight.universe != this.universe || upperLeft.universe != this.universe

IllegalArgumentException - some i: [0..upperLeft.arity) | this.universe.index(upperLeft.atoms[i]) > this.universe.index(lowerRight.atoms[i])

noneOf

public TupleSet noneOf(int arity)

Returns an initially empty tuple set of the given arity, based on this.universe.

Returns:

{ s: TupleSet | s.universe = this.universe && s.arity = arity && no s.tuples }

Throws:

IllegalArgumentException - arity < 1

range

public TupleSet range(Tuple from,
                      Tuple to)

Returns a tuple set that contains all tuples between from and to, inclusive. More formally, the returned set contains all tuples whose indices are in the range [from.index()..to.index()].

Returns:

{ s: TupleSet | s.universe = this.universe && s.arity = from.arity && s.tuples = {t: Tuple | t.universe = this.universe && t.arity = s.arity && from.index()<=t.index()<=to.index() }}

Throws:

NullPointerException - from = null || to = null

IllegalArgumentException - from.arity != to.arity

IllegalArgumentException - from.universe != this.universe || to.universe != this.universe

IllegalArgumentException - from.index > to.index

setOf

public TupleSet setOf(Collection<Tuple> tuples)

Returns a tuple set consisting of specified tuples. The method requires that all given tuples have the same arity and be drawn from this.universe.

Returns:

{s: TupleSet | s.universe = this.universe && s.arity = first.arity && s.tuples = tuples }

Throws:

NullPointerException - tuples = null

IllegalArgumentException - tuples.isEmpty()

IllegalArgumentException - tuples.universe != this.universe || #tuples.arity > 1

setOf

public TupleSet setOf(int arity,
                      IntSet tupleIndices)

Returns a set of the given arity that contains all tuples whose indeces are contained in the given int set. Throws an IllegalArgumentException if the set contains an index that is either negative or greater than this.universe.size()^arity - 1. The returned TupleSet is backed by a clone of tupleIndices.

Requires:

tupleIndices is cloneable

Returns:

{s: TupleSet | s.universe = this.universe && s.arity = arity && s.tuples = {t: Tuple | t.index() in tupleIndices} }

Throws:

NullPointerException - tupleIndices = null

IllegalArgumentException - tupleIndices is uncloneable

IllegalArgumentException - arity < 1

IllegalArgumentException - tupleIndices.min() < 0 || tupleIndices.max() >= this.universe.size()^arity

setOf

public TupleSet setOf(Object... atoms)

Returns a set of tuples of arity 1, each of which wraps one of the given objects. The method requires that the specified object be atoms in this.universe.

Returns:

{s: TupleSet | s.universe = this.universe && s.arity = 1 && s.tuples = { t: Tuple | t.universe=this.universe && t.arity=1 && t.atoms[0] in atoms[int]}}

Throws:

NullPointerException - atoms = null

IllegalArgumentException - some atoms[int] - this.universe.atoms[int]

setOf

public TupleSet setOf(Tuple first,
                      Tuple... rest)

Returns a tuple set consisting of specified tuples. The method requires that all given tuples have the same arity and be drawn from this.universe.

Returns:

{s: TupleSet | s.universe = this.universe && s.arity = first.arity && s.tuples = first + rest[int] }

Throws:

NullPointerException - first = null || rest = null

IllegalArgumentException - first.universe != this.universe

IllegalArgumentException - some t: rest[int] | t.universe != this.universe || t.arity != first.arity

tuple

public Tuple tuple(int arity,
                   int index)

Returns a tuple with the specified arity whose index in an arity-dimensional space over this.universe is given by the index parameter.

Returns:

{t: Tuple | t.universe = this.universe && t.arity = arity && index = sum({i : [0..arity) | universe.index(t.atoms[i]) * universe.size^(arity - 1 - i))}) }

Throws:

IllegalArgumentException - arity < 1 || index < 0 || index >= universe.size^arity

tuple

public Tuple tuple(List<?> atoms)

Returns a tuple that contains the specified sequence of atoms, drawn from this.universe.

Returns:

{t: Tuple | t.universe = this.universe && t.atoms = atoms }

Throws:

NullPointerException - atoms = null

IllegalArgumentException - atoms.size < 1

IllegalArgumentException - some a: atoms[int] | a !in this.universe.atoms[int]

tuple

public Tuple tuple(Object... atoms)

Returns a tuple that contains the specified sequence of atoms, drawn from this.universe.

Returns:

{t: Tuple | t.universe = this.universe && t.atoms = atoms }

Throws:

NullPointerException - atoms = null

IllegalArgumentException - atoms.length < 1

IllegalArgumentException - some a: atoms[int] | a !in this.universe.atoms[int]

universe

public Universe universe()

Returns the universe to which this factory belongs.

Returns:

this.universe