Returns the operator of this. @return this.op

Returns the cache for gates with the given operator. @requires op in AND + OR + ITE @return cache[op.ordinal]

Returns an Int that represents the sum of this and the given Int. @requires this.factory = other.factory @return an Int that represents the sum of thi

Returns the node's current position in the node list, which is always between 0 and node.size()-1

Returns a proof of this.formula's unsatisfiability if the value returned by {@link #outcome() this.outcome()} is UNSATISFIABLE or TRIVIALLY_UNSATISFIA

Create a new type that is the same as "old", except the "is_bool" and "is_int" flags are both set to false.

This method is called by Swing to replace text in this document.

Converts this into a "set or relation" if possible, then resolves it if ambiguous. <p> On success: the return value will be a well-typed unambiguous s

Returns a new Solution with a SATISFIABLE outcome, given stats and instance. @return {s: Solution | s.outcome() = SATISFIABLE && s.stats() = stats &&

This method is called by Swing to change its background color.

Modifies the current "default directory" which is used by the FileOpen and FileSave dialogs.

{@inheritDoc}

Changes the font name, font size, and tabsize of every text buffer.

Sets the intEncoding option to the given value.

Returns set_intersection2[A][B] @return set_intersection2[A][B]

Returns an unmodifiable IntSet whose sole element is the given integer. The clone method of the returned set returns the set itself. @return {s: IntS

Returns the size of the list.

Returns the formula (some this) <p> this must be a set or a relation

{@inheritDoc}

Returns a new Dimensions object with n dimensions, each of which has the specified size. @return {d: Dimensions | d.n = n && d.dimensions[int] = size

Retrieves the i-th state of this trace, considering the normalization of indices after looping. @param i @return

Implementation of the tree-successor algorithm from CLR. Returns the given node's successor, if it exists. Otherwise returns null. @return the given n

Returns the set of tuples that are the target of r. r may be in this.relations and not have targets set. If r is not mapped by this, null is returned.

If the atom starts with "-" or "0-9" then convert it into a 32-bit int (here we assume that it came from a 32-bit int) <p> If the atom does not start

Returns a string representation of this annotated node. @return string representation of this annotated node.

{@inheritDoc}

Returns union[a] @return union[a]

Returns a list of valid choices for this multi-choice preference

Returns true if the given node has been visited before. @ensures this.visited' = this.visited + n @return n in this.visited

Returns the application of the Authentic predicate. @return application of the Authentic predicate.

Maps the given relation to the given tuple set. @ensures this.tuples' = this.tuples ++ relation->s @throws NullPointerException relation = null || s

Repaint this component.

Returns a copy of this boolean matrix. @return {m: BooleanMatrix - this | m.dimensions = this.dimensions && m.eleme

Silently closes the given resource if it is non-null.

Silently closes the given resource if it is non-null.

Returns the transitive closure of this matrix. @return { m: BooleanMatrix | m = ^this } @throws UnsupportedOperationException #this.diensions != 2 |

Returns coerce_to_class[A]. @return coerce_to_class[A]

Returns true if i is in this set. @return i in this.ints @see kodkod.util.ints.IntSet#contains(int)

Returns the declarations. @return one a && one b && one c

This method concatenates a Throwable's message and stack trace and all its causes into a single String.

Executes the given command line, wait for its completion, then return its output. @param timeLimit - we will attempt to terminate the process after t

Based on the specified "options", execute one command and return the resulting A4Solution object. @param rep - if nonnull, we'll send compilation dia

Translates {@link PardinusBounds temporal bound} into standard bounds by expanding the bound trace over {@link kodkod.ast.VarRelation variable relatio

Returns the value at the given index, without checking that the index is in bounds. @return this.elements[index]

Popup the given error message, then terminate the program.

Return the first variable in this declaration.

Returns an unmodifiable list of the AlloyAtoms in this AlloyTuple.

Returns the last AlloyAtom in this AlloyTuple.

Assuming layout() has been called, this returns the top edge.

Assuming layout() has been called, this returns the total height.

Assuming layout() has been called, this returns the total width.

Returns the recommended font to use in the visualizer, based on the OS.

Returns true if the solvers returned by this.instance() are incremental; i.e. if clauses/variables can be added to the solver between multiple calls t

Initializes the given sig to be associated with the given unary value; should only be called at the beginning. <p> The resulting instance may or may n

This method is called by Swing to insert a String into this document. We intentionally ignore "attr" and instead use our own coloring.

Checks whether an AST node has temporal constructs, i.e., occurrences of {@link kodkod.ast.operator.TemporalOperator temporal operations} or {@link ko

Return the number of layers; can be 0.

Load the XML instance.

Write a horizontal separator into the log window.

Generates a call to a builtin predicate

Returns the right endpoint of this range. @return this.max

The maximum trace length that will be explored by the temporal model finder. {@link UnboundedSolver unbounded temporal solvers} will ignore this value

Circularly traverse table of size length.

Converts identifiers into a version that is compatible with Electrod by removing '/', '.' and '$' symbols. TODO: what if id already has # symbols? @

Returns ordered_pair[A][B] @return ordered_pair[A][B]

Helper method that writes the given String to the output file, then return the number of bytes written.

Return the simplest path pointing to this Module ("" if this is the main module)

Returns a new type { A | (A is in this && A.arity in that) } <p> ReturnValue.is_int == false <br> ReturnValue.is_bool == false <p> If this.size()==0 o

Returns an integer range from min, inclusive, to max, inclusive. @return { r: IntRange | r.min = min && r.max = max } @throws IllegalArgumentException

Removes all tuples in c from this, if present, and returns true. Otherwise does nothing and returns false. @ensures this.tuples' = this.tuples - c.el

Converts this into a "formula" if possible, then resolves it if ambiguous. <p> On success: the return value will be a well-typed unambiguous formula e

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

Returns set_union2[A][B] @return set_union2[A][B]

Highlights the text editor, based on the location information in the set of Pos objects.

Returns the set of all non-leaf descendants of this.node that have more than one parent. @return {n: Node | some n.children && #(n.~components & this.

Simulates the shufps SIMD instruction. @requires xmm1.length = 4 and xmm2.length = 4 and imm8.length = 4 @requires all i: [0..3] | 0 <= imm8[i] < 4 @r

Encodes the shufps SIMD instruction. @requires xmm1.arity = 2 and xmm2.arity = 2 and imm8.length = 4 @requires all i: [0..3] | imm8[i].arity = 1 @retu

Encodes the shufps SIMD instruction. @requires xmm1.arity = 2 and xmm2.arity = 2 and imm8.length = 4 @requires all i: [0..3] | imm8[i].arity = 1 @retu

{@inheritDoc}

{@inheritDoc}

Returns the last atom of this tuple.

Whether the solver should run in target-oriented mode. Will require an appropriate {@link TargetOrientedSolver solver} that is able to handle such exe

Converts the given tupleset to an array of ints.

Returns a string representation of this Solution. @return a string representation of this Solution.

Converts this into an "integer expression" if possible; otherwise, returns an Expr with a nonempty error list