Returns a tuple that contains the specified sequence of atoms, drawn from this.universe. @return {t: Tuple | t.universe = this.universe && t.atoms =

Returns the expression (this -> x) which can also be regarded as a multiplicity constraint (this set->set x) <p> this must be a set or relation <p> x

Adds the specified tuple to this tupleset. Returns true if this set was changed as the result of the operation. @ensures this.tuples' = this.tuples +

Returns the join of this and the specified expression. The effect of this method is the same as calling this.compose(JOIN, expr). @return this.compos

Returns product axiom. @return product

Adds the given integer to this set if not already present and returns true. Otherwise does nothing and returns false. @ensures this.ints' = this.ints

Returns the element at the specified position in this vector. @return this.elements[index] @throws IndexOutOfBoundsException if the index is out of

Returns the declaration that constrains this variable to be bound to exactly one element of the given expression: 'this: one expr'. @return {d: Decl

Returns a sequence of this.size + other.size decls that has these decls as the prefix and the given decls as the suffix. @return {ds: Decls | ds.size

Returns a new variable with the specified name and arity 1. @ensures this.name' = name && this.arity' = 1

Returns the cardinality of this set. @return #this.ints

Returns a BooleanValue encoding the comparator circuit that checks whether the integer represented by this Int is equal to the integer represented by

Copy the input list, append "element" to it, then return the result as an unmodifiable list.

Returns a formula that represents a universal quantification of this formula over the given declarations. The effect of this method is the same as cal

Returns true if the records with the given node, formula derived from the node, literal, and environment should be returned by iterators produced by

Returns a new unary relation with the given name. The effect of this method is the same as calling Relation.nary(name,1). @return {r: Relation | r.ari

Returns the conjunction of this and the specified formula. The effect of this method is the same as calling this.compose(AND, formula). @return this.c

Puts the given value at the specified index. If the sequence already mapped the index to a value, the previous value is replaced with the new one and

Returns a->b in in. @return a->b in in

Sets the lower and upper bounds for the given relation. @requires lower.tuples in upper.tuples && lower.arity = upper.arity = r.arity && lo

Compares the specified object with this set for equality. Returns true if the specified object is also an IntSet, the two sets have the same size, and

Sets both the lower and upper bounds of the given relation to the given set of tuples. @requires tuples.arity = r.arity && tuples.universe = this.uni

Returns a tuple set that contains all tuples between <code>from</code> and <code>to</code>, inclusive. More formally, the returned set contains all t

@ensures this.tokens' = concat [ this.tokens, token ]

Returns the intersection of this and the specified expression. The effect of this method is the same as calling this.compose(INTERSECTION, expr). @re

Returns an Int that represents bitwise negation of this integer. @return ~[[this]] @throws UnsupportedOperationException this.encoding does not suppo

Returns an initially empty tuple set of the given arity, based on this.universe. @return { s: TupleSet | s.universe = this.universe && s.arity = arity

Makes the specified expression the upper bound on the contents of the given relation. The lower bound automatically becomes an NONE expression with th

Returns union[a] @return union[a]

Returns true if this set has no elements; otherwise returns false. @return no this.ints

Returns a new binary relation with the given name. The effect of this method is the same as calling Relation.nary(name,2). @return {r: Relation | r.ar

Returns the boolean value assigned to the given variable by the last successful call to {@link #solve()}. @requires {@link #solve() } has been called

Returns the formula 'this in expr'. The effect of this method is the same as calling this.compare(SUBSET, expr). @return this.compare(SUBSET, expr)

Returns the formula 'no this'. The effect of this method is the same as calling this.apply(NO). @return this.apply(NO)

Returns Operator.ITE. @return Operator.ITE

Returns true if i is in this set. @return i in this.ints

Returns the implication of the specified formula by this. The effect of this method is the same as calling this.compose(IMPLIES, formula). @return thi

Returns the next int in the iteration, if any. Otherwise throws a NoSuchElementException. @return the next element in the iteration @throws java.util.

Returns true if this iteration has more elements. @return true if this iteration has more elements.

{@inheritDoc}

Returns the union of this and the specified expression. The effect of this method is the same as calling this.compose(UNION, expr). @return this.comp

Returns the difference of this and the specified expression. The effect of this method is the same as calling this.compose(DIFFERENCE, expr). @return

Returns the length of this trace. @return #this.elts

Returns a tuple set that is the cross product of this and the specified set. @return {t: TupleSet | t.arity = this.arity + s.arity &&

Removes the given integer from this set if already present and returns true. Otherwise does nothing and returns false. @ensures this.ints' = this.int

Returns the set of tuples that r may contain (the upper bound on r's contents). If r is not mapped by this, null is returned. @return r in this.relat

Returns the formula 'one this'. The effect of this method is the same as calling this.apply(ONE). @return this.apply(ONE)

Returns the formula 'some this'. The effect of this method is the same as calling this.apply(SOME). @return this.apply(SOME)

Returns the Options object used by this Solver to guide translation of formulas from first-order logic to cnf. @return this.options

Returns this.factory @return this.factory

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

Returns the clause at the given index. Note that this method is not required to always return the same Clause object; it is only required to return C

Returns a TupleFactory that can be used to construct tuples and sets of tuples based on this universe. @return this.factory

Returns an iterator over the integers in this set, in the ascending element order. @return an IntIterator over the integers in this set.

Returns the index of this entry. @return this.index

Constructs a ExprITE expression. @param cond - the condition formula @param left - the then-clause @param right - the else-clause

This constructs a Kodkod Tuple from the list of atoms, and returns null if no such Tuple can be constructed.

Returns the left child of this. @return this.left

Transposes a 4x4 matrix m given as an array of 16 values. @requires m.length = 16 @return some t: int[] | t.length = 16 and all i, j

@ensures this.tokens' = concat [ this.tokens, token ]

Visits the given sequence of declarations.

This method is called by the A4SolutionWriter when it is writing a particular sig, field, or skolem.

Returns an unmodifiable List with same elements as the array.

Returns the expression in this declaration. @return this.exresssion

Removes all elements from this set. @ensures no this.ints'

Returns a new type { A | A is in this, or A is in that } <p> ReturnValue.is_int == this.is_int || that.is_int <br> ReturnValue.is_bool == this.is_bool

Adds all of the elements in the specified collection to this set if they're not already present. @ensures this.ints' = this.ints + { i: int | c.contai

Attempts to satisfy the given {@code formula} and {@code bounds} with respect to {@code this.options} or, optionally, prove the problem's unsatisfiabi

Returns the atom at the specified index @return this.atoms[i] @throws IndexOutOfBoundsException i < 0 || i >= this.arity

Returns a formula that represents an existential quantification of this formula over the given declarations. The effect of this method is the same as

Returns the right child of this. @return this.right

Sets both the lower and upper bounds of the given relation to the given expression. @requires expr.arity = r.arity @ensures this.relations' = this.re

Returns the smallest element in this set. Throws a NoSuchElementException if this set is empty. @return min(this.ints) @throws java.util.NoSuchElement

Replaces the element at the specified position in this vector with the specified element, and returns the previous element (optional operation). @ens

Returns a new relation with the given name and arity. @return {r: Relation | r.arity = arity && r.name = name } @throws IllegalArgumentException arit

Returns a pretty-printed string representation of the given node, with each line offset by at least the given number of whitespaces. The line paramet

Makes this TempList unmodifiable, then construct a ConstList backed by this TempList.

This method is called by Swing to enable/disable a component.

Returns the arity of this tuple. @return this.arity

Evaluates the specified formula with respect to the relation-tuple mappings given by this.instance and using this.options. If temporal expression, eva

Construct a SimAtom for the given label, or if an existing SimAtom hasn't been garbage collected yet then return that instead.

Sets the primitive solver factory used to generate {@link kodkod.engine.PrimitiveSolver primitive solvers}. @param solver the primitive solver factor

Returns the value stored in this entry. @return this.value

Returns the formula 'this = expr'. The effect of this method is the same as calling this.compare(EQUALS, expr). @return this.compare(EQUALS, expr)

Returns a Collection view of the values stored in this sequence. The returned collection supports removal iff this is not an unmodifiable sparse seque

If every entry has the same arity, that arity is returned; <br> else if some entries have different arities, we return -1; <br> else we return 0 (whic

Returns the composition of this and the specified formula using the given binary operator. @return {f: Formula | f.left = this and f.right = formula a

Returns the name of this element.

Returns the next subtrace of the specified trace to be analyzed, given as a set of indices into the trace. If there are no more subtraces to be analyz

Returns a formula stating that the given relation is a total function with the specified domain and range. @return {f: Formula | f <=> expr in domain-