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

Returns the multiplicity in this declaration. @return this.multiplicity

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

Returns true iff the problem has been solved and the result is satisfiable.

Returns the node whose key is the ceiling of <tt>k</tt> in this tree, or null if no such node exists. @return {n: this.nodes | n.key >= k &&

Truncate the log to the given length; if the log is shorter than the number given, then nothing happens.

Translates the given formula using the specified bounds and options. The CNF representation of the given formula and bounds is generated so that the

Send the following zero-argument event to every listener.

Returns whether this textarea is based on an actual disk file.

Returns the size of this solver's vocabulary. @return #this.variables

Peek without consuming the next character, or return -1 if end-of-file is reached. @throws IOException if an I/O error occurred.

The length of the prefix of this temporal instance, i.e., the number of unique states prior to looping. @return

Read the next character. @throws IOException if end-of-file is reached. @throws IOException if an I/O error occurred.

Prints a human-readable description of this Tuple.

Converts this into a "set or relation" if possible; otherwise, returns an Expr with a nonempty error list

Returns an implementation of the int set interface that offers the best time/space trade-off for a set that can store all elements in the half open ra

Returns this.defCond @return this.defCond

Returns the size of the ith dimensions @return this.dimensions[i] @throws ArrayIndexOutOfBoundsException i < 0 || i >= this.capacity

Returns a set view of the mappings contained in this map. Each element in the returned set is a reference-equality-based <tt>Map.Entry</tt>. The set

Returns the length of the finite prefix.

Returns true iff this contains an entry of the given arity.

Returns true if this.size()>0 and at least one entry consists of something other than NONE.

{@inheritDoc}

Returns true if we can determine the two expressions are equivalent; may sometimes return false.

If x = SOMETHING->RELATION where SOMETHING.arity==1, then return the RELATION, else return null.

Sets this.bitwidth to the given value.

Returns the scope for a sig (or -1 if we don't know).

Splits the z entry into the least number of entries that do not contain the given index. @requires z.min() <= index <= z.max() @requires z != NIL @ens

{@inheritDoc} @see java.lang.Object#toString()

Helper method that refreshes the right-side visualization panel with the latest settings.

Returns true if index is a valid flat index for a matrix with these dimensions; otherwise returns false. @return 0 <= i < this.capacity

Returns the "from" node.

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

Add the given formula to the list of Kodkod formulas, and associate it with the given Pos object (pos can be null if unknown).

Creates menu items from boolean preferences (<code>prefs</code>) and adds them to a given parent menu (<code>parent</code>).

Returns the "to" node.

Sets the "changed since last save" flag, then flush any cached generated graphs.

Returns the composition of this and the specified expression, using the given binary operator. @requires op in ExprOperator.BINARY @return {e: Express

Returns true if this.size()==0 or every entry consists only of NONE.

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

Looks up the given variable in this environment and its ancestors. If the variable is not bound in this environment or any of its ancestors, null is

Returns the operator of this. @return this.op

Returns the expression (this+x) <p> this and x must be expressions with the same arity, or both be integer expressions <p> Note: as a special guarante

Returns the number of tuples in this tupleset (this answer may be truncated if it cannot fit in a 32-bit integer)

Returns the transpose of these dimensions. @return { d: Dimensions | d.n = 2 && d.dimensions[0] = this.dimensions[1] && d.d

Returns the indices of the axioms in this trace. @return { i: int | this.elts[i] in this.prover.clauses }

Returns an unmodifiable copy of the list of all skolems if the problem is solved and is satisfiable; else returns an empty list.

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

Returns the relational override of this with the specified expression. The effect of this method is the same as calling this.compose(OVERRIDE, expr).

Encodes the result of reading a subarray of length 4 from the given array, starting at the given index. @requires m.arity = 2 and pos.arity = 1 @retur

Encodes the result of reading a subarray of length 4 from the given array, starting at the given index. @requires m.arity = 2 and pos.arity = 1 @retur

Reads a subarray of length 4 from the given array, starting at the given index. @requires m.length >= 4 @requires pos >= 0 and pos + 4 <= m.length @re

Transfer focus to this component.

@return false

Returns this.universe. @return this.universe

Returns an annotation for the given node. The source map of the returned annotation object maps each descendant of the node to itself. @return { a: A

Returns the expression that results from applying the given unary operator to this. @requires op.unary() @return {e: Expression | e.expression = this

Returns the i_th atom in this universe @return this.atoms[i] @throws IndexOutOfBoundsException i < 0 || i >= this.size

Returns the capacity of this. @return this.capacity

Returns the largest element in this set that is smaller than or equal to i. If this is emtpy or i is less than this.min(), NoSuchElementException is

Returns the formula (all...| this) <p> this must be a formula

Returns an unmodifiable sorted set of all AlloyRelation(s) in this model.

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

Return a new position that merges this and that (it is assumed that the two Pos objects have same filename) @param that - the other position object

Returns true iff running on Windows

Returns the ordinal of this operator constant. @return the ordinal of this operator constant.

Read everything from "file" and parse it; if it mentions submodules, open them and parse them too. @param rep - if nonnull, we will report compilatio

Returns the cross product of this and the specified tuple. @return {t : Tuple | t.atoms = this.atoms->tuple.atoms} @throws NullPointerException tupl

Replaces the old node, o, with the given new node, n, in this tree. @requires no n.(left + right + parent) @requires o = o.parent.left => n.key < o.pa

{@inheritDoc} @see kodkod.engine.bool.Int#width()

Width including its borders on left and right

Merge "x" into the set of entries, then return the new arity bitmask. <br> Precondition: entries and arities are consistent

Find a temporary directory to store Alloy files; it's guaranteed to be a canonical absolute path.

This method is called by the BoundsComputer to report the bounds chosen for each sig and each field.

Returns true if this contains all tuples from c. Otherwise returns false. @return c.elements in this.tuples @throws IllegalArgumentException some t:

Returns the entry with the smallest index. If the sequence is empty, returns null. @return {e: IndexedEntry | e.index = min(this.entries.E) &&

Releases the resources, if any, associated with this solver.

Returns the original unprojected model.

Returns the relation representing the grid. @return relation representing the grid.

Returns true iff { A&B | A is in this, and B is in that } can have tuples.