- AbortedException - Exception in kodkod.engine
-
Indicates that a solving or evaluation task has been aborted.
- abs() - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the absolute value of this int expression.
- abs() - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the absolute value of this integer.
- AbstractCollector<T> - Class in kodkod.ast.visitor
-
A depth first collector.
- AbstractDetector - Class in kodkod.ast.visitor
-
A depth first detector.
- AbstractIntCollection - Class in kodkod.util.ints
-
A skeletal implementation of the IntCollection interface.
- AbstractIntSet - Class in kodkod.util.ints
-
A skeletal implementation of the IntSet interface.
- AbstractIntVector - Class in kodkod.util.ints
-
A skeletal implementation of the IntVector interface.
- AbstractReplacer - Class in kodkod.ast.visitor
-
A depth first replacer.
- AbstractReporter - Class in kodkod.engine.config
-
A skeleton implementation of the
Reporter interface.
- AbstractSparseSequence<V> - Class in kodkod.util.ints
-
A skeletal implementation of the SparseSequence interface.
- AbstractVoidVisitor - Class in kodkod.ast.visitor
-
Implements a depth first traversal of the kodkod AST.
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.BinaryExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.BinaryExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.BinaryFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.BinaryFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.BinaryIntExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.BinaryIntExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.ComparisonFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.ComparisonFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Comprehension
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.Comprehension
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.ConstantExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.ConstantExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.ConstantFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.ConstantFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Decl
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.Decl
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Decls
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.Decls
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Expression
-
Accepts the given visitor and returns the result.
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.ExprToIntCast
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.ExprToIntCast
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Formula
-
Accepts the given visitor and returns the result.
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IfExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.IfExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IfIntExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.IfIntExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IntComparisonFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.IntComparisonFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IntConstant
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.IntConstant
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IntExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.IntExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.IntToExprCast
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.IntToExprCast
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.MultiplicityFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.MultiplicityFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.NaryExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.NaryExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.NaryFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.NaryFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.NaryIntExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.NaryIntExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Node
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.Node
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.NotFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.NotFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.ProjectExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.ProjectExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.QuantifiedFormula
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.QuantifiedFormula
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Relation
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.Relation
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.RelationPredicate
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.RelationPredicate
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.SumExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.SumExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.UnaryExpression
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.UnaryExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.UnaryIntExpression
-
Accepts the given visitor and returns the result
of the visit (i.e.
- accept(VoidVisitor) - Method in class kodkod.ast.UnaryIntExpression
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(ReturnVisitor<E, F, D, I>) - Method in class kodkod.ast.Variable
-
Accepts the given visitor and returns the result.
- accept(VoidVisitor) - Method in class kodkod.ast.Variable
-
Accepts the given void visitor by calling visitor.visit(this).
- accept(BooleanVisitor<T, A>, A) - Method in class kodkod.engine.bool.BooleanFormula
-
Passes this value and the given
argument value to the visitor, and returns the resulting value.
- accept(BooleanVisitor<T, A>, A) - Method in class kodkod.engine.bool.BooleanVariable
-
Passes this value and the given
argument value to the visitor, and returns the resulting value.
- accept(BooleanVisitor<T, A>, A) - Method in class kodkod.engine.bool.ITEGate
-
Passes this value and the given
argument value to the visitor, and returns the resulting value.
- accept(BooleanVisitor<T, A>, A) - Method in class kodkod.engine.bool.MultiGate
-
Passes this value and the given
argument value to the visitor, and returns the resulting value.
- accept(BooleanVisitor<T, A>, A) - Method in class kodkod.engine.bool.NotGate
-
Passes this value and the given
argument value to the visitor, and returns the resulting value.
- accept(Node, Formula, int, Map<Variable, TupleSet>) - Method in interface kodkod.engine.fol2sat.RecordFilter
-
Returns true if the records with the given node, formula derived from the node, literal, and environment
should be returned by iterators produced by the
TranslationLog.replay() method.
- accumulate(BooleanAccumulator) - Method in class kodkod.engine.bool.BooleanFactory
-
Converts the given accumulator into an immutable boolean value and adds it to this.components.
- acyclic() - Method in class kodkod.ast.Relation
-
Returns a formula stating that this relation is acyclic.
- AdaptiveRCEStrategy - Class in kodkod.engine.ucore
-
Adaptive Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level.
- AdaptiveRCEStrategy(TranslationLog) - Constructor for class kodkod.engine.ucore.AdaptiveRCEStrategy
-
Constructs an ARCE strategy that will use the given translation
log to relate the cnf clauses back to the logic constraints from
which they were generated.
- AdaptiveRCEStrategy(TranslationLog, double, double, double) - Constructor for class kodkod.engine.ucore.AdaptiveRCEStrategy
-
Constructs an ARCE strategy that will use the given translation
log to relate the cnf clauses back to the logic constraints from
which they were generated.
- add(BooleanValue) - Method in class kodkod.engine.bool.BooleanAccumulator
-
Adds the given value to this.components and returns the result.
- add(Relation, TupleSet) - Method in class kodkod.instance.Instance
-
Maps the given relation to the given tuple set.
- add(int, TupleSet) - Method in class kodkod.instance.Instance
-
Maps the given integer to the given tuple set.
- add(Tuple) - Method in class kodkod.instance.TupleSet
-
Adds the specified tuple to this tupleset.
- add(E) - Method in class kodkod.util.collections.CacheSet
-
Adds the given element to this set, if not already present.
- add(T) - Method in class kodkod.util.collections.IdentityHashSet
-
- add(int) - Method in class kodkod.util.ints.AbstractIntCollection
-
Throws an UnsupportedOperationException.
- add(int) - Method in class kodkod.util.ints.AbstractIntVector
-
Calls this.add(this.size(), element)
- add(int, int) - Method in class kodkod.util.ints.AbstractIntVector
-
- add(int) - Method in class kodkod.util.ints.ArrayIntVector
-
Calls this.add(this.size(), element)
- add(int, int) - Method in class kodkod.util.ints.ArrayIntVector
-
- add(int) - Method in class kodkod.util.ints.IntBitSet
-
Adds the given integer to this set if not already present
and returns true.
- add(int) - Method in interface kodkod.util.ints.IntCollection
-
Ensures that this collection contains the given integer, and returns true
if this collection has changed as a result of the call.
- add(int) - Method in interface kodkod.util.ints.IntSet
-
Adds the given integer to this set if not already present
and returns true.
- add(int) - Method in class kodkod.util.ints.IntTreeSet
-
Adds the given integer to this set if not already present
and returns true.
- add(int) - Method in interface kodkod.util.ints.IntVector
-
Adds the specified element to the end of this vector (optional
operation), and returns true if this vector has changed as a result
of the call.
- add(int, int) - Method in interface kodkod.util.ints.IntVector
-
Inserts the specified element at the specified position in this vector
(optional operation), and returns true if this vector has changed as a result of the call.
- addAll(Collection<? extends Tuple>) - Method in class kodkod.instance.TupleSet
-
Adds all tuples from c to this, if not present, and returns
true.
- addAll(Collection<? extends T>) - Method in class kodkod.util.collections.IdentityHashSet
-
- addAll(IntCollection) - Method in class kodkod.util.ints.AbstractIntCollection
-
Adds all of the elements in the specified collection to this collection.
- addAll(IntCollection) - Method in class kodkod.util.ints.AbstractIntVector
-
- addAll(int, IntCollection) - Method in class kodkod.util.ints.AbstractIntVector
-
Throws an UnsupportedOperationException.
- addAll(int, IntCollection) - Method in class kodkod.util.ints.ArrayIntVector
-
Throws an UnsupportedOperationException.
- addAll(IntCollection) - Method in class kodkod.util.ints.IntBitSet
-
Adds all of the elements in the specified collection to this collection.
- addAll(IntCollection) - Method in interface kodkod.util.ints.IntCollection
-
Adds all of the elements in the specified collection to this collection.
- addAll(IntCollection) - Method in interface kodkod.util.ints.IntSet
-
Adds all of the elements in the specified collection to this set
if they're not already present.
- addAll(IntCollection) - Method in interface kodkod.util.ints.IntVector
-
Appends the specified elements to the end of this vector (optional
operation), and returns true if this vector has changed as a result of the call.
- addAll(int, IntCollection) - Method in interface kodkod.util.ints.IntVector
-
Inserts the specified elements at the specified position in this vector
(optional operation), and returns true if this vector has changed as a result of the call.
- addClause(int[]) - Method in interface kodkod.engine.satlab.SATSolver
-
Ensures that this solver logically contains the given
clause, and returns true if this.clauses changed as a
result of the call.
- addVariables(int) - Method in class kodkod.engine.bool.BooleanFactory
-
Adds the specified number of fresh variables to this.components.
- addVariables(int) - Method in interface kodkod.engine.satlab.SATSolver
-
Adds the specified number of new variables
to the solver's vocabulary.
- ALL - Static variable in interface kodkod.engine.fol2sat.RecordFilter
-
A record filter that accepts all records.
- allOf(int) - Method in class kodkod.instance.TupleFactory
-
Returns a set of all tuples of the given arity, drawn from this.universe.
- allRoots(Formula, Collection<? extends Node>) - Static method in class kodkod.util.nodes.Nodes
-
Returns all
roots of the given formula such that a node in the given collection
is reachable from that root.
- and(Decls) - Method in class kodkod.ast.Decls
-
Returns a sequence of this.size + other.size decls that has
these decls as the prefix and the given decls as the suffix.
- and(Formula) - Method in class kodkod.ast.Formula
-
Returns the conjunction of this and the specified formula.
- and(Formula...) - Static method in class kodkod.ast.Formula
-
Returns the conjunction of the given formulas.
- and(Collection<? extends Formula>) - Static method in class kodkod.ast.Formula
-
Returns the conjunction of the given formulas.
- and(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the bitwise AND of this and
the given int node.
- and(IntExpression...) - Static method in class kodkod.ast.IntExpression
-
Returns the bitwise and of the given int expressions.
- and(Collection<? extends IntExpression>) - Static method in class kodkod.ast.IntExpression
-
Returns the bitwise and of the given int expressions.
- and(BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is the conjunction of the input components.
- and(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a new matrix such that an entry in the returned matrix represents a
conjunction of the corresponding entries in this and other matrix.
- and(BooleanMatrix...) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a new matrix such that an entry in the returned matrix represents a
conjunction of the corresponding entries in this and other matrices.
- and(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the bitwise conjunction of this and the given Int.
- and(Int...) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the bitwise conjunction of this and the given Ints.
- AND - Static variable in class kodkod.engine.bool.Operator
-
- annotate(N) - Static method in class kodkod.util.nodes.AnnotatedNode
-
Returns an annotation for the given node.
- annotate(N, Map<? extends Node, ? extends Node>) - Static method in class kodkod.util.nodes.AnnotatedNode
-
Returns an annotation for the given node.
- AnnotatedNode<N extends Node> - Class in kodkod.util.nodes
-
A node annotated with information about
structural sharing in its ast/dag.
- annotateRoots(Formula) - Static method in class kodkod.util.nodes.AnnotatedNode
-
Returns an annotation for an n-ary conjunctions of
roots of the given formula.
- antecedents() - Method in class kodkod.engine.satlab.Clause
-
Returns an iterator that traverses this.antecedents in proper sequence.
- apply(ExprOperator) - Method in class kodkod.ast.Expression
-
Returns the expression that results from applying the given unary operator
to this.
- apply(ExprCastOperator) - Method in class kodkod.ast.Expression
-
Returns the cast of this expression to an integer expression,
that represents either the cardinality of this expression (if op is CARDINALITY)
or the sum of the integer atoms it contains (if op is SUM).
- apply(Multiplicity) - Method in class kodkod.ast.Expression
-
Returns the formula that results from applying the specified multiplicity to
this expression.
- apply(IntOperator) - Method in class kodkod.ast.IntExpression
-
Returns an expression that represents the application of the given unary
operator to this integer expression.
- approximate(Expression, Bounds, Options) - Static method in class kodkod.engine.fol2sat.Translator
-
Overapproximates the value of the given expression using the provided bounds and options.
- area(Tuple, Tuple) - Method in class kodkod.instance.TupleFactory
-
Returns a tuple set that contains all tuples in the specified area
of the n-dimensional space, where n is the arity of the argument
tuples.
- arity() - Method in class kodkod.ast.BinaryExpression
-
Returns the arity of this binary expression.
- arity() - Method in class kodkod.ast.Comprehension
-
Returns the arity of this comprehension expression, which is the sum
of the arities of declared variables
- arity() - Method in class kodkod.ast.Expression
-
Returns the arity of this expression.
- arity() - Method in class kodkod.ast.IfExpression
-
Returns the arity of this.
- arity() - Method in class kodkod.ast.IntToExprCast
-
Returns 1.
- arity() - Method in class kodkod.ast.LeafExpression
-
Returns the arity of this leaf.
- arity() - Method in class kodkod.ast.NaryExpression
-
Returns the arity of this associative expression.
- arity() - Method in class kodkod.ast.ProjectExpression
-
Returns the arity of this expression.
- arity() - Method in class kodkod.ast.UnaryExpression
-
Returns the arity of this expression.
- arity() - Method in class kodkod.instance.Tuple
-
Returns the arity of this tuple.
- arity() - Method in class kodkod.instance.TupleSet
-
Returns this.arity
- ArrayIntSet - Class in kodkod.util.ints
-
An immutable set of integers, stored in a sorted array.
- ArrayIntSet(int[]) - Constructor for class kodkod.util.ints.ArrayIntSet
-
Constructs a set view for the given array.
- ArrayIntSet(IntSet) - Constructor for class kodkod.util.ints.ArrayIntSet
-
Constructs an ArrayIntSet that is equal to the
given set.
- ArrayIntVector - Class in kodkod.util.ints
-
A mutable implementation of the IntVector interface.
- ArrayIntVector(int) - Constructor for class kodkod.util.ints.ArrayIntVector
-
Constructs an empty MutableIntVector with the specified initial capacity.
- ArrayIntVector() - Constructor for class kodkod.util.ints.ArrayIntVector
-
Constructs an empty MutableIntVector with an initial capacity of ten.
- ArrayIntVector(int[]) - Constructor for class kodkod.util.ints.ArrayIntVector
-
Constructs a MutableIntVector containing the elements of the specified
array, in proper sequence.
- ArraySequence<V> - Class in kodkod.util.ints
-
An implementation of a sparse sequence based on an array.
- ArraySequence(IntSet) - Constructor for class kodkod.util.ints.ArraySequence
-
Constructs an array sequence that contains
the given indeces.
- ArraySequence(SparseSequence<? extends V>) - Constructor for class kodkod.util.ints.ArraySequence
-
Constructs a new array sequence with the same index/value mappings
as the given sequence.
- ArrayStack<T> - Class in kodkod.util.collections
-
A Stack implementation based on an array.
- ArrayStack() - Constructor for class kodkod.util.collections.ArrayStack
-
Constructs an empty stack with the inital capacity of 10.
- ArrayStack(int) - Constructor for class kodkod.util.collections.ArrayStack
-
- asHashSet(T[]) - Static method in class kodkod.util.collections.Containers
-
Returns a set backed by the given array (i.e.
- asIdentitySet(T[]) - Static method in class kodkod.util.collections.Containers
-
Returns an identity set backed by the given array (i.e.
- asIntVector(int[]) - Static method in class kodkod.util.ints.Ints
-
Returns an unmodifiable IntArray backed by the given array of integers.
- asSet(int[]) - Static method in class kodkod.util.ints.Ints
-
Returns an IntSet that is backed by the given array of integers.
- atom(int) - Method in class kodkod.instance.Tuple
-
Returns the atom at the specified index
- atom(int) - Method in class kodkod.instance.Universe
-
Returns the i_th atom in this universe
- atomIndex(int) - Method in class kodkod.instance.Tuple
-
Returns the index of the ith atom as given by this.universe.
- available(SATFactory) - Static method in class kodkod.engine.satlab.SATFactory
-
Returns true iff the given factory generates solvers that
are available for use on this system.
- axioms() - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of the axioms in this trace.