- IDEN - Static variable in class kodkod.ast.Expression
-
- identity() - Method in class kodkod.engine.bool.Operator.Nary
-
Returns the boolean constant c such that
for all logical values x, c composed
with x using this operator will result in x.
- identityBinarySearch(Object[], Object) - Static method in class kodkod.util.collections.Containers
-
Searches the specified array for the specified object using the binary search algorithm
and reference equality.
- identityComparator() - Static method in class kodkod.util.collections.Containers
-
- IdentityHashSet<T> - Class in kodkod.util.collections
-
Implements the Set interface with a hash table, using
reference-equality in place of object-equality when comparing elements.
- IdentityHashSet() - Constructor for class kodkod.util.collections.IdentityHashSet
-
Constructs a new, empty identity hash map with a default expected
maximum size of 16.
- IdentityHashSet(int) - Constructor for class kodkod.util.collections.IdentityHashSet
-
Constructs a new, empty set with the specified expected maximum size.
- IdentityHashSet(Collection<? extends T>) - Constructor for class kodkod.util.collections.IdentityHashSet
-
Constructs a new identity hash set containing the elements
in the specified collection.
- identitySort(T[]) - Static method in class kodkod.util.collections.Containers
-
- IfExpression - Class in kodkod.ast
-
An expression whose value depends on the truth of a given condition.
- iff(Formula) - Method in class kodkod.ast.Formula
-
Returns a formula that equates this and the specified formula.
- iff(BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is [[v0]] <=> [[v1]].
- IfIntExpression - Class in kodkod.ast
-
An int expression whose value depends on the truth of a condition.
- implies(Formula) - Method in class kodkod.ast.Formula
-
Returns the implication of the specified formula by this.
- implies(BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is [[v0]] => [[v1]].
- in(Expression) - Method in class kodkod.ast.Expression
-
Returns the formula 'this in expr'.
- incremental() - Method in class kodkod.engine.satlab.SATFactory
-
Returns true if the solvers returned by this.instance() are incremental;
i.e.
- IncrementalSolver - Class in kodkod.engine
-
A computational engine for solving a sequence of related relational
formulas and
bounds
(e.g., generated by a software verification or synthesis tool)
with respect to a given set of configuration
options
.
- index() - Method in class kodkod.instance.Tuple
-
A Tuple encodes a number with this.arity digits in radix this.universe.size;
a Tuple's index is the decimal representation of this number.
- index(Object) - Method in class kodkod.instance.Universe
-
Returns the index of the specified atom in this universe; if the
atom is not in this universe, an IllegalArgumentException is thrown.
- index() - Method in interface kodkod.util.ints.IndexedEntry
-
Returns the index of this entry.
- IndexedEntry<E> - Interface in kodkod.util.ints
-
- Indexer<K> - Interface in kodkod.util.collections
-
An index generator for a set of keys.
- indexOf(K) - Method in class kodkod.util.collections.FixedMap
-
Returns the index of the given key, if it is in this.keys.
- indexOf(K) - Method in interface kodkod.util.collections.Indexer
-
Returns the index of the given key, if it is in this.keys.
- indexOf(int) - Method in class kodkod.util.ints.AbstractIntVector
-
Returns the index in this vector of the first occurrence of the specified
element, or -1 if this vector does not contain this element.
- indexOf(int) - Method in interface kodkod.util.ints.IntVector
-
Returns the index in this vector of the first occurrence of the specified
element, or -1 if this vector does not contain this element.
- indexView() - Method in class kodkod.instance.TupleSet
-
Returns an unmodifiable int set view of the tuples stored in this set.
- indices() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns the set of all indices mapped by this sparse sequence.
- indices() - Method in class kodkod.util.ints.HomogenousSequence
-
Returns the set of all indices mapped by this sparse sequence.
- indices() - Method in interface kodkod.util.ints.SparseSequence
-
Returns the set of all indices mapped by this sparse sequence.
- input(int) - Method in class kodkod.engine.bool.BooleanFormula
-
Returns the ith input to this gate.
- input(int) - Method in class kodkod.engine.bool.BooleanVariable
-
Throws an IndexOutOfBoundsException.
- input(int) - Method in class kodkod.engine.bool.ITEGate
-
Returns this.inputs[i].
- input(int) - Method in class kodkod.engine.bool.NotGate
-
Returns this.input[i].
- instance() - Method in class kodkod.engine.Evaluator
-
Returns this.instance.
- instance() - Method in class kodkod.engine.satlab.SATFactory
-
Returns an instance of a SATSolver produced by this factory.
- instance() - Method in class kodkod.engine.Solution
-
Returns a satisfiying instance for this.formula, if the
value returned by
this.outcome()
is either
SATISFIABLE or TRIVIALLY_SATISFIABLE.
- Instance - Class in kodkod.instance
-
- Instance(Universe) - Constructor for class kodkod.instance.Instance
-
Constructs an empty instance over the given universe
- Int - Class in kodkod.engine.bool
-
- IntBitSet - Class in kodkod.util.ints
-
An implementation of the IntSet interface based on a bit map.
- IntBitSet(int) - Constructor for class kodkod.util.ints.IntBitSet
-
Constructs an empty IntBitSet that can store up
to capacity elements.
- IntBitSet(int, long[]) - Constructor for class kodkod.util.ints.IntBitSet
-
Constructs an IntBitSet that can store up to capacity elements.
- intBounds() - Method in class kodkod.instance.Bounds
-
Returns a sparse sequence view of this.intBound.
- IntCastOperator - Enum in kodkod.ast.operator
-
Represents an intexpression 'cast' operator.
- IntCollection - Interface in kodkod.util.ints
-
The root interface in the int collection hierarchy.
- IntComparisonFormula - Class in kodkod.ast
-
An integer comparison formula, e.g.
- IntCompOperator - Enum in kodkod.ast.operator
-
Enumerates binary comparison operators: =, < , >, <=, >=.
- IntConstant - Class in kodkod.ast
-
An integer constant (literal).
- integer(int) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns an Int that represents the given number using this.intEncoding.
- integer(int, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns an Int that represents 0 or the given number, depending on the value of the given bit.
- integers() - Method in class kodkod.engine.config.Options
-
Returns the range of integers that can be encoded
using this.intEncoding and this.bitwidth.
- intEncoding() - Method in class kodkod.engine.bool.BooleanFactory
-
Returns the encoding used by this factory to represent integers.
- intEncoding() - Method in class kodkod.engine.config.Options
-
Returns the integer encoding that will be used for translating
int nodes
.
- interpret() - Method in class kodkod.engine.fol2sat.Translation
-
If this.solver.solve()
is true, returns an interpretation of the CNF solution as a
mapping from Relations to sets of Tuples.
- intersection(Expression) - Method in class kodkod.ast.Expression
-
Returns the intersection of this and the specified expression.
- intersection(Expression...) - Static method in class kodkod.ast.Expression
-
Returns the intersection of the given expressions.
- intersection(Collection<? extends Expression>) - Static method in class kodkod.ast.Expression
-
Returns the intersection of the given expressions.
- intersects(IntRange) - Method in class kodkod.util.ints.IntRange
-
Returns true if this and the given range intersect.
- intExpr() - Method in class kodkod.ast.IntToExprCast
-
Returns this.intExpr.
- intExpr() - Method in class kodkod.ast.SumExpression
-
Returns this.intExpr.
- intExpr() - Method in class kodkod.ast.UnaryIntExpression
-
Returns this.intExpr.
- IntExpression - Class in kodkod.ast
-
A Node whose value is an integer
rather than a relational expression.
- IntIterator - Interface in kodkod.util.ints
-
An iterator over integer primitives.
- IntOperator - Enum in kodkod.ast.operator
-
Enumerate unary (-, ~, abs, sgn), binary (+, *, &, |, -, /, %, >>, >>>, <<) and nary (+, *, &, |) operators on integer expressions.
- IntRange - Class in kodkod.util.ints
-
Represents a range of integers, [min..max].
- INTS - Static variable in class kodkod.ast.Expression
-
The integer relation: contains all atoms
bound
to integers
- ints() - Method in class kodkod.instance.Bounds
-
Returns the set of all integers bound by this Bounds.
- ints() - Method in class kodkod.instance.Instance
-
Returns the integers mapped by this instance.
- Ints - Class in kodkod.util.ints
-
- IntSet - Interface in kodkod.util.ints
-
An ordered set of integers.
- IntToExprCast - Class in kodkod.ast
-
- IntTreeSet - Class in kodkod.util.ints
-
An implementation of the IntTreeSet interface based
on a balanced binary search tree.
- IntTreeSet() - Constructor for class kodkod.util.ints.IntTreeSet
-
Constructs an empty int set.
- IntTreeSet(IntSet) - Constructor for class kodkod.util.ints.IntTreeSet
-
Constructs a new int set containing the elements
in the specified set.
- intTuples() - Method in class kodkod.instance.Instance
-
Returns a sparse sequence view of int<:this.tuples.
- IntVector - Interface in kodkod.util.ints
-
A resizable array of integers.
- isConstant() - Method in class kodkod.engine.bool.Int
-
Returns true if all the bits representing this Int
are BooleanConstants.
- isEmpty() - Method in class kodkod.util.collections.CacheSet
-
Returns true if this set is empty.
- isEmpty() - Method in class kodkod.util.collections.FixedMap
-
- isEmpty() - Method in class kodkod.util.collections.IdentityHashSet
-
- isEmpty() - Method in class kodkod.util.collections.SingletonIdentitySet
-
Returns false.
- isEmpty() - Method in class kodkod.util.ints.AbstractIntCollection
-
Returns true if this collection has no elements;
otherwise returns false.
- isEmpty() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns true if the size of this sequence is 0.
- isEmpty() - Method in class kodkod.util.ints.ArraySequence
-
Returns true if this sequence is empty; otherwise returns false.
- isEmpty() - Method in class kodkod.util.ints.IntBitSet
-
Returns true if this collection has no elements;
otherwise returns false.
- isEmpty() - Method in interface kodkod.util.ints.IntCollection
-
Returns true if this collection has no elements;
otherwise returns false.
- isEmpty() - Method in interface kodkod.util.ints.IntSet
-
Returns true if this set has no elements;
otherwise returns false.
- isEmpty() - Method in interface kodkod.util.ints.IntVector
-
Returns true if this vector contains no elements.
- isEmpty() - Method in interface kodkod.util.ints.SparseSequence
-
Returns true if this sequence is empty; otherwise returns false.
- isShortCircuited() - Method in class kodkod.engine.bool.BooleanAccumulator
-
Returns true if this gate is short circuited; that is,
its inputs are reduced to this.op.shortCircuit.
- isSquare() - Method in class kodkod.engine.bool.Dimensions
-
Returns true if this represents the dimensions of a square matrix;
otherwise returns false.
- ite(BooleanValue, BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is [[i]] ? [[t]] : [[e]].
- ITE - Static variable in class kodkod.engine.bool.Operator
-
- ITEGate - Class in kodkod.engine.bool
-
An if-then-else gate.
- iterate(E...) - Static method in class kodkod.util.collections.Containers
-
Returns a new iterator over the given array of items.
- iterate(int, int, E...) - Static method in class kodkod.util.collections.Containers
-
Returns a new iterator over the given array of items.
- iterator() - Method in class kodkod.ast.Decls
-
Returns an unmodifiable iterator over the decls in this Decls object.
- iterator() - Method in class kodkod.ast.NaryExpression
-
Returns an iterator over this expression's children,
in the increasing order of indices.
- iterator() - Method in class kodkod.ast.NaryFormula
-
Returns an iterator over this formula's children,
in the increasing order of indices.
- iterator() - Method in class kodkod.ast.NaryIntExpression
-
Returns an iterator over this int expression's children,
in the increasing order of indices.
- iterator() - Method in class kodkod.engine.bool.BooleanAccumulator
-
Returns an iterator over this.components, in
the increasing order of labels.
- iterator() - Method in class kodkod.engine.bool.BooleanFormula
-
Returns an iterator over the inputs to this gate.
- iterator() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns an IndexedEntry-based view of the non-FALSE entries in this matrix.
- iterator() - Method in class kodkod.engine.bool.BooleanVariable
-
Returns an empty iterator.
- iterator() - Method in class kodkod.engine.bool.ITEGate
-
Returns an iterator over this.inputs
- iterator() - Method in class kodkod.engine.bool.NotGate
-
Returns an iterator that returns this gate's single input.
- iterator() - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns an iterator over the elements in this trace in proper sequence.
- iterator(IntSet) - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns an iterator over the elements at the given indices in this trace, in proper sequence.
- iterator() - Method in class kodkod.instance.TupleSet
-
Returns an iterator over the tuples in this tupleset.
- iterator() - Method in class kodkod.instance.Universe
-
Returns an iterator over atoms in this universe, according to their
order in the universe.
- iterator() - Method in class kodkod.util.collections.ArrayStack
-
Iterates over the items in this Stack, starting
at the top of the stack and working its way down.
- iterator() - Method in class kodkod.util.collections.CacheSet
-
Returns an iterator over the elements in this set.
- iterator() - Method in class kodkod.util.collections.IdentityHashSet
-
- iterator() - Method in class kodkod.util.collections.LinkedStack
-
Iterates over the items in this LinkedStack, starting
at the top of the stack and working its way down.
- iterator() - Method in class kodkod.util.collections.SingletonIdentitySet
-
- iterator() - Method in class kodkod.util.collections.Stack
-
Iterates over the items in this Stack, starting
at the top of the stack and working its way down.
- iterator() - Method in class kodkod.util.ints.AbstractIntSet
-
Returns an ascending iterator over all elements in this set.
- iterator() - Method in class kodkod.util.ints.AbstractIntVector
-
Calls this.iterator(0, length())
- iterator(int, int) - Method in class kodkod.util.ints.AbstractIntVector
-
Returns an iterator over the elements in this vector in proper sequence,
starting fromIndex<\tt>, inclusive, and ending at toIndex<\tt>, exclusive.
- iterator() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns an iterator over the entries in this sequence
in the ascending order of indeces, starting at this.first().
- iterator(int, int) - Method in class kodkod.util.ints.ArrayIntSet
-
Returns an iterator over the elements of this set that
are in the closed range [from..to].
- iterator(int, int) - Method in class kodkod.util.ints.ArraySequence
-
Returns an iterator over the entries in this sequence,
whose indeces are between from and to.
- iterator(int, int) - Method in class kodkod.util.ints.HomogenousSequence
-
Returns an iterator over the entries in this sequence,
whose indeces are between from and to.
- iterator() - Method in class kodkod.util.ints.IntBitSet
-
Returns an ascending iterator over all elements in this set.
- iterator(int, int) - Method in class kodkod.util.ints.IntBitSet
-
Returns an iterator over the elements of this set that
are in the closed range [from..to].
- iterator() - Method in interface kodkod.util.ints.IntCollection
-
Returns an iterator over the elements in this collection.
- iterator() - Method in interface kodkod.util.ints.IntSet
-
Returns an iterator over the integers in this set,
in the ascending element order.
- iterator(int, int) - Method in interface kodkod.util.ints.IntSet
-
Returns an iterator over the elements of this set that
are in the closed range [from..to].
- iterator(int, int) - Method in class kodkod.util.ints.IntTreeSet
-
Returns an iterator over the elements of this set that
are in the closed range [from..to].
- iterator() - Method in interface kodkod.util.ints.IntVector
-
Returns an iterator over the elements in this vector in proper sequence.
- iterator(int, int) - Method in interface kodkod.util.ints.IntVector
-
Returns an iterator over the elements in this vector in proper sequence,
starting fromIndex<\tt>, inclusive, and ending at toIndex<\tt>, exclusive.
- iterator(int, int) - Method in class kodkod.util.ints.RangeSequence
-
Returns an iterator over the entries in this sequence,
whose indeces are between from and to.
- iterator() - Method in interface kodkod.util.ints.SparseSequence
-
Returns an iterator over the entries in this sequence
in the ascending order of indeces, starting at this.first().
- iterator(int, int) - Method in interface kodkod.util.ints.SparseSequence
-
Returns an iterator over the entries in this sequence,
whose indeces are between from and to.
- iterator(int, int) - Method in class kodkod.util.ints.TreeSequence
-
Returns an iterator over the entries in this sequence,
whose indeces are between from and to.