Encodes the result of writing the four elements from the source into the destination array at the specified position. @requires dst.arity = 2 and pos.

Encodes the result of writing the four elements from the source into the destination array at the specified position. @requires dst.arity = 2 and pos.

Writes out this database to the given file. Each puzzle is written out as a string of N N numbers, where each subsequence of N numbers represents one

Writes the four elements from the source into the destination array at the specified position. @requires src.length = 4 and dst.length >= 4 @requires

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

Add a directed edge from start node to end node (if there wasn't such an edge already).

Returns op[X][Y]. @return op[X][Y]

Returns a boolean value whose meaning is (if [[i]] then [[t]] else [[e]]). @requires i + t + e in (this.values + this.values.negation + BooleanConstan

Returns the boolean value that corresponds to this constant formula. @return this=TRUE => true, false

(Re-)calculate this node's bounds.

@return e.card

Returns the smallest element in this set that is greater than or equal to i. If this is emtpy or i is greater than this.max(), NoSuchElementException

@throws IllegalArgumentException !d0.equals(d1)

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

Returns a formula comparing this and the given integer expression using the specified operator. @return {f: Formula | f.left = this and f.right = intE

This method takes an Object input and produces a String output. @throws Exception if an error occurred during the computation.

Returns true if this sparse sequence has an entry for the given index; otherwise returns false. @return some this.entries[index]

Converts Windows/Mac/Unix linebreaks into '\n', and replace non-tab non-linebreak control characters into space.

Calls System.arraycopy(src, srcPos, dest, destPos, length) and returns the destination array. @ensures System.arraycopy(src, srcPos, dest, destPos, le

Whether the solver should run in decomposed mode. Will require an appropriate {@link DecomposedSolver solver} that is able to handle such execution mo

A slightly modified implementation of the CLR deletion algorithm. @requires z in this.nodes @ensures this.nodes' = this.nodes - z

Write a String into a PrintWriter, and encode special characters using XML-specific encoding. <p> In particular, it changes LESS THAN, GREATER THAN, A

Helper method for enumerating all possibilities for a quantification-expression.

Explain this clause for tooltips etc. @return a string formatted like a set

Find the lowest level expr that encompasses pos and that has a reference @param pos the position @return the matchin expr or null

Frees the memory used by this solver. Once free() is called, all subsequent calls to methods other than free() may fail. @ensures frees the memory us

Return the i-th parameter where i goes from 0 to count()-1

Returns the i-th element.

Returns the arity of this AlloyTuple.

Return the list of per-atom facts; each expression is allowed to refer to this.decl.get()

Gets an unmodifiable copy of the set of types we are currently projecting over.

Returns a boolean value whose meaning is [[v0]] <=> [[v1]]. The behavior of this method is unspecified if v0 or v1 are not components of this factory.

Returns a boolean value whose meaning is [[v0]] => [[v1]]. The behavior of this method is unspecified if v0 or v1 are not components of this factory.

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

Returns the set of all integers corresponding to some atom in this.universe. @return this.ints

Helper method that evaluates the formula "a in b" where b.mult==0

Helper method that translates the formula "a in b" into a Kodkod formula.

This returns the constant prefix to denote whether Util.readAll() should read from a JAR or read from the file system. (The reason we made this into a

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

Returns an iterator over the literals in this clause, in the ascending order of absolute values. @return an iterator over this.literals

Constructs a LET expression. @param pos - the position of the '=' token in the original Alloy model (or null if unknown) @param var - the

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

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

Select the content between offset a and offset b, and move the caret to offset b.

If this solution is UNSAT, return itself; else return the next solution (which could be SAT or UNSAT). @throws ErrorAPI if the solver was not an incr

Return the multiplicity expression "one this" <p> this must be already fully typechecked, and must be a unary set

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

Returns the range of this.relation. @return this.range

Removes the last returned element from the underlying collection. @ensures removes the last returned element from the underlying collection. @throws U

Replace the i-th atom, and return the resulting SimTuple.

{@inheritDoc} @see kodkod.engine.fol2sat.TranslationLog#replay(kodkod.engine.fol2sat.RecordFilter)

Helper method that repopulates the Projection popup menu.

@return true if resolvent literals have been computed for the resolvent at the given index

@return e.room

The task should send zero or more non-null Objects to out.callback(msg) to report progress to the parent process.

Returns true iff this solution has a (trivially) satisfiable outcome. @return this.outcome = Outcome.SATISFIABLE || this.outcome = Outcome.TR

{@inheritDoc}

Changes the X coordinate of the center of the node, without invalidating the computed bounds.

Make the frame visible, non-iconized, and focused.

Returns the depth to which existential quantifiers are skolemized. A negative depth means that no skolemization is performed. The default depth of 0 m

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

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

{@inheritDoc}

Returns the start node. @return this.start

Returns a boolean value whose meaning is the sum bit of a full binary adder. The behavior of this method is unspecified if v0, v1, or cin are not comp

Performs the hashing step of Paul Hsieh's hashing function, described at http://www.azillionmonkeys.com/qed/hash.html. The method returns a 32 bit has

Terminates the thread executor and the running solvers. @throws InterruptedException if interrupted while waiting.

Make a JTextArea with the given text and number of rows and columns, then call Util.make() to apply a set of attributes to it. @param attributes - se

{@inheritDoc} @see kodkod.ast.Node#toString()

Returns the name for this sig; this name need not be unique.

Returns the expression (~this) <p> this must be a binary relation

This method is called by the typechecker to report the type for each field/function/predicate/assertion, etc.

Returns a map view of this.upperBound. The returned map is not modifiable. @return a map view of this.upperBound

Returns the version string.

Write the given byte into this byte buffer.

Returns the weight of r for TO runs. r may be in this.targets and not have weights set. If r is not mapped by this, null is returned. @return r in th

Open then overwrite the file with the given content; throws Err if an error occurred.

Returns the result of adding the non-negative given constant to the given index. @requires idx.arity = 1 and k >= 0 @return idx + k

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

{@inheritDoc} @see kodkod.util.ints.IntSet#addAll(kodkod.util.ints.IntCollection)

Appends the elements in the given collection to the list, then return itself.

Add a global expression; if the name already exists, it is removed first.

Adds a target. @param lit the target