- CacheSet<E> - Class in kodkod.util.collections
-
Implements the Set interface, backed by a hash table.
- CacheSet() - Constructor for class kodkod.util.collections.CacheSet
-
Constructs a new, empty set; the backing map has
default initial capacity (16) and load factor (0.75).
- CacheSet(int, float) - Constructor for class kodkod.util.collections.CacheSet
-
Constructs a new, empty set; the backing map has
the specified initial capacity and the specified load factor.
- CacheSet(Collection<? extends E>) - Constructor for class kodkod.util.collections.CacheSet
-
Constructs a new set containing the elements in the specified
collection.
- capacity() - Method in class kodkod.engine.bool.Dimensions
-
Returns the capacity of this.
- capacity() - Method in class kodkod.instance.TupleSet
-
Returns the capacity of this set -- the maximum number of tuples
that it can hold, given its universe and arity.
- capacity() - Method in class kodkod.util.ints.IntBitSet
-
Returns the capacity of this int bit set
- CapacityExceededException - Exception in kodkod.engine
-
Indicates that a problem construction or translation task failed because
the capacity of the index representation was exceeded.
- CapacityExceededException(IntVector) - Constructor for exception kodkod.engine.CapacityExceededException
-
Constructs a CapacityExceededException from the given dimensions.
- CapacityExceededException(String, IntVector) - Constructor for exception kodkod.engine.CapacityExceededException
-
Constructs a CapacityExceededException with the given message and dimensions.
- CapacityExceededException(Throwable, IntVector) - Constructor for exception kodkod.engine.CapacityExceededException
-
Constructs a CapacityExceededException with the given cause.
- CapacityExceededException(String, Throwable, IntVector) - Constructor for exception kodkod.engine.CapacityExceededException
-
Constructs a CapacityExceededException with the given message and cause.
- cardinality() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns an Int that represents the cardinality (number of non-FALSE entries) of this
matrix using this.factory.intEncoding.
- carry(BooleanValue, BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is the carry out bit of a full binary adder.
- cast(IntCastOperator) - Method in class kodkod.ast.IntExpression
-
Returns an expression that is the relational representation of this
integer expression specified by the given operator.
- ceil(int) - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns the entry whose index is the ceiling of the given index in this sequence.
- ceil(int) - Method in class kodkod.util.ints.ArrayIntSet
-
- ceil(int) - Method in class kodkod.util.ints.ArraySequence
-
If an entry for the given index exists, it is returned.
- ceil(int) - Method in class kodkod.util.ints.HomogenousSequence
-
If an entry for the given index exists, it is returned.
- ceil(int) - Method in class kodkod.util.ints.IntBitSet
-
Returns the smallest element in this set that
is greater than or equal to i.
- ceil(int) - Method in interface kodkod.util.ints.IntSet
-
Returns the smallest element in this set that
is greater than or equal to i.
- ceil(int) - Method in class kodkod.util.ints.IntTreeSet
-
Returns the smallest element in this set that
is greater than or equal to i.
- ceil(int) - Method in class kodkod.util.ints.RangeSequence
-
Returns the entry whose index is the ceiling of the given index in this sequence.
- ceil(int) - Method in interface kodkod.util.ints.SparseSequence
-
If an entry for the given index exists, it is returned.
- ceil(int) - Method in class kodkod.util.ints.TreeSequence
-
Returns the entry whose index is the ceiling of the given index in this sequence.
- checkIncrementalBounds(Bounds, Translation.Incremental) - Static method in class kodkod.engine.fol2sat.Translator
-
Checks that the given inc bounds are incremental with respect to the given translation.
- checkIncrementalOptions(Options) - Static method in class kodkod.engine.fol2sat.Translator
-
Checks that the given options are suitable for incremental translation.
- child(int) - Method in class kodkod.ast.NaryExpression
-
Returns the ith child of this associative expression.
- child(int) - Method in class kodkod.ast.NaryFormula
-
Returns the ith child of this formula.
- child(int) - Method in class kodkod.ast.NaryIntExpression
-
Returns the ith child of this int expression.
- choice(BooleanValue, BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a boolean matrix m such that m = this if the given condition evaluates
to TRUE and m = other otherwise.
- choice(BooleanValue, Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that evaluates to this if the condition is true, otherwise it
evaluates to the given Int.
- Clause - Class in kodkod.engine.satlab
-
A propositional clause.
- clauses() - Method in class kodkod.engine.Statistics
-
Returns the number of clauses needed to
encode this.formula in CNF.
- clear() - Method in class kodkod.instance.TupleSet
-
Removes all tuples from this tupleset.
- clear() - Method in class kodkod.util.collections.CacheSet
-
Removes all elements from this set.
- clear() - Method in class kodkod.util.collections.IdentityHashSet
-
- clear() - Method in class kodkod.util.ints.AbstractIntCollection
-
This implementation iterates over this set, removing each
element using the Iterator.remove operation.
- clear() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Removes all entries from this sequences.
- clear() - Method in class kodkod.util.ints.ArraySequence
-
Removes all entries from this sequences.
- clear() - Method in class kodkod.util.ints.HomogenousSequence
-
Removes all entries from this sequences.
- clear() - Method in class kodkod.util.ints.IntBitSet
-
Removes all elements from this set.
- clear() - Method in interface kodkod.util.ints.IntCollection
-
Removes all elements from this collection.
- clear() - Method in interface kodkod.util.ints.IntSet
-
Removes all elements from this set.
- clear() - Method in class kodkod.util.ints.IntTreeSet
-
Removes all elements from this set.
- clear() - Method in interface kodkod.util.ints.IntVector
-
Removes all of the elements from this vector (optional operation).
- clear() - Method in class kodkod.util.ints.RangeSequence
-
Removes all entries from this sequences.
- clear() - Method in interface kodkod.util.ints.SparseSequence
-
Removes all entries from this sequences.
- clear() - Method in class kodkod.util.ints.TreeSequence
-
Removes all entries from this sequences.
- clone() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a copy of this boolean matrix.
- clone() - Method in class kodkod.engine.config.Options
-
Returns a shallow copy of this Options object.
- clone() - Method in class kodkod.instance.Bounds
-
Returns a deep (modifiable) copy of this Bounds object.
- clone() - Method in class kodkod.instance.Instance
-
Returns a deep copy of this Instance object.
- clone() - Method in class kodkod.instance.TupleSet
-
Returns a deep copy of this tuple set.
- clone() - Method in class kodkod.util.ints.AbstractIntSet
-
Returns the result of calling super.clone().
- clone() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns the result of calling super.clone().
- clone() - Method in class kodkod.util.ints.ArraySequence
-
Returns a copy of this sparse sequence.
- clone() - Method in class kodkod.util.ints.HomogenousSequence
-
Returns a copy of this sparse sequence.
- clone() - Method in class kodkod.util.ints.IntBitSet
-
Returns a copy of this int bit set.
- clone() - Method in interface kodkod.util.ints.IntSet
-
Returns a copy of this IntSet.
- clone() - Method in class kodkod.util.ints.IntTreeSet
-
Returns a copy of this int tree set.
- clone() - Method in class kodkod.util.ints.RangeSequence
-
Returns a copy of this sparse sequence.
- clone() - Method in interface kodkod.util.ints.SparseSequence
-
Returns a copy of this sparse sequence.
- clone() - Method in class kodkod.util.ints.TreeSequence
-
Returns a copy of this sparse sequence.
- closure() - Method in class kodkod.ast.Expression
-
Returns the transitive closure of this.
- closure() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the transitive closure of this matrix.
- cnf() - Method in class kodkod.engine.fol2sat.Translation
-
Returns the SATSolver object containing the CNF encoding of this.formula.
- cnf() - Method in class kodkod.engine.fol2sat.Translation.Incremental
-
Returns the SATSolver object containing the CNF encoding of this.formula.
- cnf() - Method in class kodkod.engine.fol2sat.Translation.Whole
-
Returns the SATSolver object containing the CNF encoding of this.formula.
- column(int) - Method in class kodkod.ast.ProjectExpression
-
Returns the ith column.
- columns() - Method in class kodkod.ast.ProjectExpression
-
Returns an iterator over this.columns, in proper sequence.
- compare(ExprCompOperator, Expression) - Method in class kodkod.ast.Expression
-
Returns the formula that represents the comparison of this and the
given expression using the given comparison operator.
- compare(IntCompOperator, IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns a formula comparing this and the given integer expression using the
specified operator.
- compareTo(BooleanValue) - Method in class kodkod.engine.bool.BooleanValue
-
Boolean components are ordered according to their labels.
- compareTo(Operator) - Method in class kodkod.engine.bool.Operator
-
Returns an integer i such that i < 0 if this.ordinal < op.ordinal,
i = 0 when this.ordinal = op.ordinal, and i > 0 when this.ordinal > op.ordinal.
- comparisonDepth() - Method in class kodkod.engine.bool.BooleanFactory
-
Returns the depth (from the root) to which components are checked for
semantic equality during gate construction.
- ComparisonFormula - Class in kodkod.ast
-
A formula that compares two expressions, e.g.
- complement() - Method in class kodkod.engine.bool.Operator.Nary
-
Returns the binary operator whose identity and short circuit
values are the negation of this operator's identity and
short circuit.
- compose(ExprOperator, Expression) - Method in class kodkod.ast.Expression
-
Returns the composition of this and the specified expression, using the
given binary operator.
- compose(ExprOperator, Expression...) - Static method in class kodkod.ast.Expression
-
Returns the composition of the given expressions using the given operator.
- compose(ExprOperator, Collection<? extends Expression>) - Static method in class kodkod.ast.Expression
-
Returns the composition of the given expressions using the given operator.
- compose(FormulaOperator, Formula) - Method in class kodkod.ast.Formula
-
Returns the composition of this and the specified formula using the
given binary operator.
- compose(FormulaOperator, Formula...) - Static method in class kodkod.ast.Formula
-
Returns the composition of the given formulas using the given operator.
- compose(FormulaOperator, Collection<? extends Formula>) - Static method in class kodkod.ast.Formula
-
Returns the composition of the given formulas using the given operator.
- compose(IntOperator, IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an expression that combines this and the given integer expression using the
specified operator.
- compose(IntOperator, IntExpression...) - Static method in class kodkod.ast.IntExpression
-
Returns the composition of the given int expressions using the given operator.
- compose(IntOperator, Collection<? extends IntExpression>) - Static method in class kodkod.ast.IntExpression
-
Returns the composition of the given int expressions using the given operator.
- Comprehension - Class in kodkod.ast
-
A comprehension expression, e.g.
- comprehension(Decls) - Method in class kodkod.ast.Formula
-
Returns the comprehension expression constructed from this formula and
the given declarations.
- condition() - Method in class kodkod.ast.IfExpression
-
Returns the if-condition.
- condition() - Method in class kodkod.ast.IfIntExpression
-
Returns the if-condition.
- conjuncts(Formula) - Static method in class kodkod.util.nodes.Nodes
-
Returns an unmodifiable set consisting of the children of the given formula, if the formula is a binary or an nary conjunction.
- ConsoleReporter - Class in kodkod.engine.config
-
An implementation of the reporter interface that prints messages
to the standard output stream.
- ConsoleReporter() - Constructor for class kodkod.engine.config.ConsoleReporter
-
Constructs a new instance of the ConsoleReporter.
- CONST - Static variable in class kodkod.engine.bool.Operator
-
- constant(boolean) - Static method in class kodkod.ast.Formula
-
Returns the constant formula with the given value.
- constant(int) - Static method in class kodkod.ast.IntConstant
-
Returns an IntConstant corresponding to the given value.
- constant(boolean) - Static method in class kodkod.engine.bool.BooleanConstant
-
Returns the BooleanConstant that represents the given boolean value.
- ConstantExpression - Class in kodkod.ast
-
A constant valued expression.
- constantFactory(Options) - Static method in class kodkod.engine.bool.BooleanFactory
-
Returns a BooleanFactory with no variables; the returned factory
can manipulate only constants.
- ConstantFormula - Class in kodkod.ast
-
- Containers - Class in kodkod.util.collections
-
Provides utility methods for working with arrays and collections.
- contains(BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns true if v is in this.components.
- contains(Relation) - Method in class kodkod.instance.Instance
-
Returns true if this instance maps the given relation to a set
of tuples; otherwise returns false.
- contains(int) - Method in class kodkod.instance.Instance
-
Returns true if this instance maps the given integer to a singleton
tupleset; otherwise returns false.
- contains(Object) - Method in class kodkod.instance.Tuple
-
Returns true if atom is in this tuple, otherwise returns false.
- contains(Object) - Method in class kodkod.instance.TupleSet
-
Returns true if this contains the given object.
- contains(Object) - Method in class kodkod.instance.Universe
-
Returns true if atom is in this universe, otherwise returns false.
- contains(Object) - Method in class kodkod.util.collections.CacheSet
-
Returns true if this set contains the given element.
- contains(Object) - Method in class kodkod.util.collections.IdentityHashSet
-
Tests whether the specified object reference is an element in this identity
hash map.
- contains(Object) - Method in class kodkod.util.collections.SingletonIdentitySet
-
Returns true iff this.element and obj are the same object.
- contains(int) - Method in class kodkod.util.ints.AbstractIntCollection
-
Iterates through this.ints and returns true if it
finds i, otherwise returns false.
- contains(int) - Method in class kodkod.util.ints.AbstractIntVector
-
Iterates through this.ints and returns true if it
finds i, otherwise returns false.
- contains(Object) - Method in class kodkod.util.ints.AbstractSparseSequence
-
Iterates through all the entries in this sequence and returns
true if one of the encountered entries has the given object as
its value.
- contains(int) - Method in class kodkod.util.ints.ArrayIntSet
-
Returns true if i is in this set.
- contains(Object) - Method in class kodkod.util.ints.HomogenousSequence
-
Returns true if this sequence has an entry with the given value;
otherwise returns false.
- contains(int) - Method in class kodkod.util.ints.IntBitSet
-
Returns true if i is in this set.
- contains(int) - Method in interface kodkod.util.ints.IntCollection
-
Returns true if i is an element in this collection.
- contains(int) - Method in class kodkod.util.ints.IntRange
-
Returns true if the given integer is within
this range; otherwise returns false.
- contains(IntRange) - Method in class kodkod.util.ints.IntRange
-
Returns true if this range contains the
given range.
- contains(int) - Method in interface kodkod.util.ints.IntSet
-
Returns true if i is in this set.
- contains(int) - Method in class kodkod.util.ints.IntTreeSet
-
Returns true if i is in this set.
- contains(int) - Method in interface kodkod.util.ints.IntVector
-
Returns true if this vector contains the specified element.
- contains(Object) - Method in interface kodkod.util.ints.SparseSequence
-
Returns true if this sequence has an entry with the given value;
otherwise returns false.
- containsAll(Collection<?>) - Method in class kodkod.instance.TupleSet
-
Returns true if this contains all tuples from c.
- containsAll(Collection<?>) - Method in class kodkod.util.collections.SingletonIdentitySet
-
- containsAll(IntCollection) - Method in class kodkod.util.ints.AbstractIntCollection
-
Returns true if this collection contains all of the elements in the specified collection.
- containsAll(IntCollection) - Method in class kodkod.util.ints.IntBitSet
-
Returns true if this collection contains all of the elements in the specified collection.
- containsAll(IntCollection) - Method in interface kodkod.util.ints.IntCollection
-
Returns true if this collection contains all of the elements in the specified collection.
- containsAll(IntCollection) - Method in interface kodkod.util.ints.IntSet
-
Returns true if the elements of c are a subset of this set.
- containsAll(IntCollection) - Method in class kodkod.util.ints.IntTreeSet
-
Returns true if this collection contains all of the elements in the specified collection.
- containsIndex(int) - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsIndex(int) - Method in class kodkod.util.ints.ArraySequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsIndex(int) - Method in class kodkod.util.ints.HomogenousSequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsIndex(int) - Method in class kodkod.util.ints.RangeSequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsIndex(int) - Method in interface kodkod.util.ints.SparseSequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsIndex(int) - Method in class kodkod.util.ints.TreeSequence
-
Returns true if this sparse sequence has an entry for the
given index; otherwise returns false.
- containsKey(Object) - Method in class kodkod.util.collections.FixedMap
-
Tests whether the specified object reference is a key in this fixed map.
- containsValue(Object) - Method in class kodkod.util.collections.FixedMap
-
Tests whether the specified object reference is a value in this fixed map.
- convert(int) - Method in class kodkod.engine.bool.Dimensions
-
Converts an integer index into a matrix with these dimensions into a vector index.
- convert(int, int[]) - Method in class kodkod.engine.bool.Dimensions
-
Converts an integer index into a matrix with these dimensions into a vector index,
and stores the result in the provided array.
- convert(int[]) - Method in class kodkod.engine.bool.Dimensions
-
Converts the first this.n positions of the given vector index
into an integer index.
- copy(T[], int, T[], int, int) - Static method in class kodkod.util.collections.Containers
-
Calls System.arraycopy(src, srcPos, dest, destPos, length) and returns the destination array.
- copy(T[], T[]) - Static method in class kodkod.util.collections.Containers
-
Calls System.arraycopy(src, 0, dest, 0, src.length) and returns the destination array.
- core() - Method in class kodkod.engine.Proof
-
Returns an iterator over the
log records for the nodes
that are in the unsatisfiable core of this.log.formula.
- core() - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of the axioms that form the unsatisfiable core of this trace.
- coreGranularity() - Method in class kodkod.engine.config.Options
-
Returns the core granularity level.
- coreUnits(ResolutionTrace) - Static method in class kodkod.engine.ucore.StrategyUtils
-
Returns the set of all variables in the core of the given trace
that form unit clauses.
- coreVars(ResolutionTrace) - Static method in class kodkod.engine.ucore.StrategyUtils
-
Returns relevant core variables; that is, all variables that occur both in the positive and
negative phase in trace.core.
- count() - Method in class kodkod.ast.Expression
-
Returns the cardinality of this expression.
- cross(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the cross product of this and other matrix, using conjunction instead of
multiplication.
- cross(BooleanMatrix...) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the cross product of this and other matrices, using conjunction instead of
multiplication.
- cross(Dimensions) - Method in class kodkod.engine.bool.Dimensions
-
Returns the dimensions of a matrix that would result from taking the cross
product of a matrix of dimensions given by this and a matrix whose dimensions are
specified by dim.
- CRRStrategy - Class in kodkod.engine.ucore
-
A basic implementation of the Complete ResolutionTrace Refutation algorithm
for for producing locally minimal cores.
- CRRStrategy() - Constructor for class kodkod.engine.ucore.CRRStrategy
-
Constructs a new instance of CRRStrategy.