- range() - Method in class kodkod.ast.RelationPredicate.Function
-
Returns the range of this.relation.
- range(Tuple, Tuple) - Method in class kodkod.instance.TupleFactory
-
Returns a tuple set that contains all tuples between from
and to, inclusive.
- range(int, int) - Static method in class kodkod.util.ints.Ints
-
Returns an integer range from min, inclusive, to max, inclusive.
- RangeSequence<V> - Class in kodkod.util.ints
-
A tree-based sparse sequence implementation.
- RangeSequence() - Constructor for class kodkod.util.ints.RangeSequence
-
Constructs an empty RangeSequence.
- rangeSet(IntRange) - Static method in class kodkod.util.ints.Ints
-
Returns an unmodifiable IntSet that contains
all the elements in the given range.
- RCEStrategy - Class in kodkod.engine.ucore
-
Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level.
- RCEStrategy(TranslationLog) - Constructor for class kodkod.engine.ucore.RCEStrategy
-
Constructs an RCE strategy that will use the given translation
log to relate the cnf clauses back to the logic constraints from
which they were generated.
- RCEStrategy(TranslationLog, int) - Constructor for class kodkod.engine.ucore.RCEStrategy
-
Constructs an RCE strategy that will use the given translation
log to relate the cnf clauses back to the logic constraints from
which they were generated.
- reachable(IntSet) - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of all clauses reachable from the clauses at the given indices
by following the antecedent relation zero or more times.
- RecordFilter - Interface in kodkod.engine.fol2sat
-
A filter for TranslationRecords, based on the value of a record's node and literal fields.
- rectangular(int[]) - Static method in class kodkod.engine.bool.Dimensions
-
Constructs a new Dimensions object with the given dimensions.
- reduce(ReductionStrategy) - Method in interface kodkod.engine.satlab.SATProver
-
Uses the given reduction strategy to remove irrelevant clauses from
the set of unsatisfiable clauses stored in this prover.
- ReductionStrategy - Interface in kodkod.engine.satlab
-
Strategy for reducing the unsatisfiable core of
a
SATProver.
- reflexiveClosure() - Method in class kodkod.ast.Expression
-
Returns the reflexive transitive closure of this.
- Relation - Class in kodkod.ast
-
A relation is a leaf expression.
- relation() - Method in class kodkod.ast.RelationPredicate
-
Returns the relation to which this predicate applies.
- RelationPredicate - Class in kodkod.ast
-
Represents common predicates on relations; e.g.
- RelationPredicate.Acyclic - Class in kodkod.ast
-
Represents the acyclic predicate.
- RelationPredicate.Function - Class in kodkod.ast
-
Represents the function predicate.
- RelationPredicate.Name - Enum in kodkod.ast
-
Enumerates built-in predicates.
- RelationPredicate.TotalOrdering - Class in kodkod.ast
-
Represents the total ordering predicate.
- relations() - Method in class kodkod.instance.Bounds
-
Returns the set of all relations bound by this Bounds.
- relations() - Method in class kodkod.instance.Instance
-
Returns the relations mapped by this instance.
- relations() - Method in class kodkod.util.nodes.AnnotatedNode
-
Returns the set of all relations at the leaves of this annotated node.
- relationTuples() - Method in class kodkod.instance.Instance
-
Returns a map view of Relation<:this.tuples.
- remove(Object) - Method in class kodkod.instance.TupleSet
-
Removes the given object from this tupleset, if present, and
returns true.
- remove(Object) - Method in class kodkod.util.collections.CacheSet
-
Removes the specified object from this set, if present.
- remove(Object) - Method in class kodkod.util.collections.FixedMap
-
- remove(Object) - Method in class kodkod.util.collections.IdentityHashSet
-
- remove(int) - Method in class kodkod.util.ints.AbstractIntCollection
-
Iterates through the elements of this, removes
i if it finds it and returns true.
- remove(int) - Method in class kodkod.util.ints.AbstractSparseSequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- remove(int) - Method in class kodkod.util.ints.ArraySequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- remove(int) - Method in class kodkod.util.ints.HomogenousSequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- remove(int) - Method in class kodkod.util.ints.IntBitSet
-
Removes the given integer from this set if already present and
returns true.
- remove(int) - Method in interface kodkod.util.ints.IntCollection
-
Removes a single instance of the given integer from this collection,
and returns true if this collection has changed as a result of the call.
- remove() - Method in interface kodkod.util.ints.IntIterator
-
Removes the last returned element from the underlying collection.
- remove(int) - Method in interface kodkod.util.ints.IntSet
-
Removes the given integer from this set if already present and
returns true.
- remove(int) - Method in class kodkod.util.ints.IntTreeSet
-
Removes the given integer from this set if already present and
returns true.
- remove(int) - Method in interface kodkod.util.ints.IntVector
-
Removes the first occurrence of the given integer from this vector,
and returns true if this vector has changed as a result of the call.
- remove(int) - Method in class kodkod.util.ints.RangeSequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- remove(int) - Method in interface kodkod.util.ints.SparseSequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- remove(int) - Method in class kodkod.util.ints.TreeSequence
-
Removes the entry with the given index, if it exists, and
returns the value previously stored at the index.
- removeAll(Collection<?>) - Method in class kodkod.instance.TupleSet
-
Removes all tuples in c from this, if present, and returns
true.
- removeAll(Collection<?>) - Method in class kodkod.util.collections.IdentityHashSet
-
- removeAll(IntCollection) - Method in class kodkod.util.ints.AbstractIntCollection
-
Removes all of this collection's elements that are also contained in the specified
collection.
- removeAll(IntCollection) - Method in class kodkod.util.ints.IntBitSet
-
Removes all of this collection's elements that are also contained in the specified
collection.
- removeAll(IntCollection) - Method in interface kodkod.util.ints.IntCollection
-
Removes all of this collection's elements that are also contained in the specified
collection.
- removeAll(IntCollection) - Method in interface kodkod.util.ints.IntSet
-
Removes from this set all of its elements that are contained in the
specified set.
- removeAll(IntCollection) - Method in interface kodkod.util.ints.IntVector
-
Removes all of this vector's elements that are also contained in the specified
collection.
- removeAt(int) - Method in class kodkod.util.ints.AbstractIntVector
-
Throws an UnsupportedOperationException.
- removeAt(int) - Method in class kodkod.util.ints.ArrayIntVector
-
Throws an UnsupportedOperationException.
- removeAt(int) - Method in interface kodkod.util.ints.IntVector
-
Removes the element at the specified position in this vector (optional
operation).
- replay(RecordFilter) - Method in class kodkod.engine.fol2sat.TranslationLog
-
Returns an iterator over the translation records in this log that are accepted
by the given filter.
- replay() - Method in class kodkod.engine.fol2sat.TranslationLog
-
Returns an iterator over all translation records in this log.
- reporter() - Method in class kodkod.engine.config.Options
-
Returns this.reporter.
- Reporter - Interface in kodkod.engine.config
-
Enables passing of messages between the kodkod engine
and the client about the following stages of the analysis:
symmetry detection
bounds and formula optimization (breaking of predicate symmetries, predicate inlining and skolemization)
translation to a boolean circuit
symmetry breaking predicate (SBP) generation
translation to cnf
running a sat solver on the generated cnf
Some of these stages may not be executed, depending on the
options used for analysis.
- ResolutionTrace - Interface in kodkod.engine.satlab
-
A proof of unsatisfiability generated by a
SATProver.
- resolvents() - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of the resolvents in this trace.
- retainAll(Collection<?>) - Method in class kodkod.instance.TupleSet
-
Removes all tuples from this that are not in c, if any, and
returns true.
- retainAll(IntCollection) - Method in class kodkod.util.ints.AbstractIntCollection
-
Retains only the elements in this collection that are contained in the specified
collection.
- retainAll(IntCollection) - Method in class kodkod.util.ints.IntBitSet
-
Retains only the elements in this collection that are contained in the specified
collection.
- retainAll(IntCollection) - Method in interface kodkod.util.ints.IntCollection
-
Retains only the elements in this collection that are contained in the specified
collection.
- retainAll(IntCollection) - Method in interface kodkod.util.ints.IntSet
-
Retains only the elements in this set that are contained in the
specified set.
- retainAll(IntCollection) - Method in interface kodkod.util.ints.IntVector
-
Retains only the elements in this vector that are contained in the specified
collection.
- ReturnVisitor<E,F,D,I> - Interface in kodkod.ast.visitor
-
A visitor that visits every node in the AST, returning some value for each.
- reverseIterator(IntSet) - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns an iterator over the elements at the given indices in this trace, in the
reverse order of indices.
- right() - Method in class kodkod.ast.BinaryExpression
-
Returns the right child of this.
- right() - Method in class kodkod.ast.BinaryFormula
-
Returns the right child of this.
- right() - Method in class kodkod.ast.BinaryIntExpression
-
Returns the right child of this.
- right() - Method in class kodkod.ast.ComparisonFormula
-
Returns the right child of this.
- right() - Method in class kodkod.ast.IntComparisonFormula
-
Returns the right child of this.
- roots() - Method in class kodkod.engine.fol2sat.TranslationLog
-
Returns the roots of this.formula.
- roots(Formula) - Static method in class kodkod.util.nodes.Nodes
-
Returns the roots of the given formula.
- rootVars(TranslationLog) - Static method in class kodkod.engine.ucore.StrategyUtils
-
Returns the variables that correspond to the roots of log.formula.