Returns the largest element in this set. Throws a NoSuchElementException if this set is empty. @return max(this.ints) @throws java.util.NoSuchElementE

Returns an Int that represents the bitwise disjunction of this and the given Int. @requires this.factory = other.factory @return an Int that represent

Appends the given element to the list, then return itself.

Returns a copy of this IntSet. The copy is independent of this IntSet unless this is a singleton or an immutable set, in which case clone() may retur

Returns a satisfiying instance for this.formula, if the value returned by {@link #outcome() this.outcome()} is either SATISFIABLE or TRIVIALLY_SATISFI

Returns a set of all tuples of the given arity, drawn from this.universe. @return { s: TupleSet | s.universe = this.universe && s.arity = arity &&

Returns the negation of this formula. @return {f : NotFormula | f.formula = this }

Returns the size of this tupleset. @return #this.tuples

Returns this.label @return this.label @see kodkod.engine.bool.BooleanValue#label()

Construct a new JMenuItem then add it to an existing JMenu. @param parent - the JMenu to add this JMenuItem into (or null if you don't wan

Precondition: this.lastX==next.firstX and this.lastY==next.firstY. Note: the resulting Curve will still share the same CubicCurve2D objects as this an

Write the given number into this byte buffer, followed by a space.

Returns the formula (this and x) <p> this and x must both be formulas <p> Note: as a special guarantee, if x==null, then the method will return this E

Returns an iterator over the elements in this trace in proper sequence. <p><b>Note:</b>The clause objects returned by the iterator are not required t

Change a.pos to be the merger of a.pos and b.pos, then change a.sym to be sym, then return a.

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

Returns the reflexive transitive closure of this. The effect of this method is the same as calling this.apply(REFLEXIVE_CLOSURE). @return this.apply(

This is the start method that begins a traversal over the given expression.

Returns this.formula. @return this.formula

Given a node, call the visitor to dump its text out, then return its name.

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

Returns a reporter. @return a reporter

Returns an unmodifiable view of the mappings in this map.

Returns the node width.

Returns the BooleanValue at the specified index. @requires 0 <= i < this.factory.bitwidth @return this.bits[i]

Returns the hash code value for this set. The hash code of a set is defined to be the {@link Ints#superFastHash(int[])} of the elements in the set, ta

Returns the ith child of this formula. @requires 0 <= i < #this.children @return this.children[i]

Returns an IntConstant corresponding to the given value. @return {c: IntConstant | c.value = value}

Returns the X coordinate of the center of the node.

Returns the i-th atom in this Tuple.

Convenience method that evaluates x and cast the result to be a tupleset @return the tupleset - if x evaluates to a tupleset @throws ErrorFatal - if

@return this.decls

Returns a ternary relation with the specified name. @return {r: Relation | r.name = name && r.arity = 3}

Return the A4TupleSet for the given sig (if solution not yet solved, or unsatisfiable, or sig not found, then return an empty tupleset).

Returns this.intExpr. @return this.intExpr

Returns an unmodifiable view of the keys in this map.

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

Returns the expression y.(x.sum) @return y.(x.sum)

Wraps the calling method into a Runnable whose run() will call the calling method with (false) as the only argument.

Returns the name of this leaf. @return this.name

If this tupleset is empty, then return 0, else return the arity of every tuple in this tupleset.

Returns the arity.

Attempt to close the file/stream/reader/writer and return true if and only if we successfully closed it. (If object==null, we return true right away)

Returns the primed version of this. The effect of this method is the same as calling this.apply(PRIME). @return this.apply(PRIME)

Returns a formula stating that this relation imposes a total ordering over the atoms in the set <code>ordered</code>, and that thet first and last ele

Convenience method that evaluаtes x and cast the result to be a Kodkod Expression. @return the expression - if x evaluates to an Expression @throws E

Returns the index in this vector of the first occurrence of the specified element, or -1 if this vector does not contain this element. @return elemen

Helper method that returns a unique id for the given Sig, Field, or Skolem.

Returns the value associated with the given attribute name; if the attribute doesn't exist, return "".

Return the list of fields as a combined unmodifiable list (without telling you which fields are declared to be disjoint)

Change the entire text to the given text (and sets the modified flag)

Returns the set of tuples assigned to the given relation by this Instance. If the relation is not mapped by the model, null is returned. @return this

Returns the universe from which the atoms in this tuple are drawn. @return this.universe

Returns the canonical absolute path for a file. If an IO error occurred, or if the file doesn't exist yet, we will at least return a noncanonical but

Returns the SATSolver object containing the CNF encoding of this.formula. Satisfiability of the formula can be checked by calling {@link kodkod.engin

Returns the cardinality of this expression. The effect of this method is the same as calling this.apply(CARDINALITY). @return this.apply(CARDINALITY)

Returns true if the type of this element is equal to the given type.

Returns the number of tuples in this tupleset (this answer will never overflow)

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

Returns an Int that represents the absolute value of this integer. @return abs([[this]])

Returns a formula that equates this and the specified formula. The effect of this method is the same as calling this.compose(IFF, formula). @return th

Returns this.factory. @return this.factory.

Associate the given formula with the given expression, then return the formula as-is.

The position of this complete clause.

Returns true if this is empty.

Returns the text if this is a text node, returns "" otherwise.

Caches the given value for the specified node, if this is a caching visitor, and returns Boolean.valueOf(val). @ensures n in this.cached => this.cache

Convenience method that evaluates x and cast the result to be a Kodkod IntExpression. @return the integer expression - if x evaluates to an IntExpres

Query the current length of the log.

Returns an unmodifiable int set view of the tuples stored in this set. Specifically, the returned int set contains an integer i iff this set contains

Returns true iff running on Mac OS X.

Returns the node shape (or null if the node is a dummy node).

Returns the statistics gathered while solving this.formula. @return the statistics gathered while solving this.formula.

Adds all tuples from c to this, if not present, and returns true. Otherwise does nothing and returns false. @ensures this.tuples' = this.tuples + c.e

Convenience method that evaluates x and cast the result to be a int. @return the int - if x evaluates to an int @throws ErrorFatal - if x does not ev

Copies all of the entries from the specified sparse sequence to this sequence. The effect of this call is equivalent to that of calling put(e.index, e

Write a debugging message to System.err for the debugging version of the parser. @param mess the text of the debugging message.

Returns the negation of this boolean value @return { f: BooleanFormula | [[f]] = ![[this]] }

Returns the if expression constructed from this formula and the specified then and else expressions. @return {e: Expression | e.condition = this and e

Returns the universe of discourse. @return this.universe

Wraps the calling method into a Runnable whose run() will call the calling method with (false) as the only argument.

Convenience method that evaluates x and casts the result to be a Kodkod Formula. @return the formula - if x evaluates to a Formula @throws ErrorFatal

Make a JPanel using horizontal BoxLayout, and add the components to it (each component will be center-aligned). <br> If a component is Color, it's the

Return the type for this node; EMPTY if it is not well-typed.

Return the union of this and that; (if this tupleset and that tupleset does not have compatible arity, then we return this tupleset as is). <br/> Note

Returns an unmodifiable copy of the map from each Sig/Field/Skolem/Atom to its corresponding Kodkod expression.

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

Caches the given replacement for the specified node, if this is a caching visitor. Otherwise does nothing. The method returns the replacement node.

Returns the node height.