- sat() - Method in class kodkod.engine.Solution
-
Returns true iff this solution has a (trivially) satisfiable outcome.
- sat4jFactory(String) - Static method in class kodkod.engine.satlab.SATFactory
-
Returns a SATFactory that produces instances of the specified
SAT4J solver.
- SATAbortedException - Exception in kodkod.engine.satlab
-
A runtime exception thrown when a sat solver
terminates abnormally, usually because it was cancelled.
- SATFactory - Class in kodkod.engine.satlab
-
A factory for generating SATSolver instances of a given type.
- SATProver - Interface in kodkod.engine.satlab
-
Provides an interface to a SAT solver that can generate
proofs of unsatisfiability.
- SATSolver - Interface in kodkod.engine.satlab
-
Provides an interface to a SAT solver.
- SCEStrategy - Class in kodkod.engine.ucore
-
Simple Core Extraction is a strategy for generating unsat cores that are minimal at the logic level.
- SCEStrategy(TranslationLog) - Constructor for class kodkod.engine.ucore.SCEStrategy
-
Constructs an SCE strategy that will use the given translation
log to relate the cnf clauses back to the logic constraints from
which they were generated.
- search(Object) - Method in class kodkod.util.collections.ArrayStack
-
- search(Object) - Method in class kodkod.util.collections.LinkedStack
-
Returns the 1-based position where an object is on this stack.
- search(Object) - Method in class kodkod.util.collections.Stack
-
Returns the 1-based position where an object is on this stack.
- set(int, BooleanValue) - Method in class kodkod.engine.bool.BooleanMatrix
-
Sets the specified index to the given value.
- set(int, int) - Method in class kodkod.util.ints.AbstractIntVector
-
- set(int, int) - Method in class kodkod.util.ints.ArrayIntVector
-
- set(int, int) - Method in interface kodkod.util.ints.IntVector
-
Replaces the element at the specified position in this vector with the
specified element, and returns the previous element (optional operation).
- setBitwidth(int) - Method in class kodkod.engine.config.Options
-
Sets this.bitwidth to the given value.
- setComparisonDepth(int) - Method in class kodkod.engine.bool.BooleanFactory
-
Sets the comparison depth to the given value.
- setCoreGranularity(int) - Method in class kodkod.engine.config.Options
-
Sets the core granularity level.
- setDifference(Set<T>, Set<T>) - Static method in class kodkod.util.collections.Containers
-
Returns a new set that contains the asymmetric difference between the left and the right sets.
- setIntEncoding(Options.IntEncoding) - Method in class kodkod.engine.config.Options
-
Sets the intEncoding option to the given value.
- setLogTranslation(int) - Method in class kodkod.engine.config.Options
-
Sets the translation logging level.
- setOf(Expression) - Method in class kodkod.ast.Variable
-
Returns the declaration that constrains this variable to
be bound to a subset of the elements in the given expression: 'this: set expr'.
- setOf(Object...) - Method in class kodkod.instance.TupleFactory
-
Returns a set of tuples of arity 1, each of which wraps one of the given objects.
- setOf(Tuple, Tuple...) - Method in class kodkod.instance.TupleFactory
-
Returns a tuple set consisting of specified tuples.
- setOf(Collection<Tuple>) - Method in class kodkod.instance.TupleFactory
-
Returns a tuple set consisting of specified tuples.
- setOf(int, IntSet) - Method in class kodkod.instance.TupleFactory
-
Returns a set of the given arity that contains all tuples whose indeces
are contained in the given int set.
- setReporter(Reporter) - Method in class kodkod.engine.config.Options
-
Sets this.reporter to the given reporter.
- setSharing(int) - Method in class kodkod.engine.config.Options
-
Sets the sharing option to the given value.
- setSkolemDepth(int) - Method in class kodkod.engine.config.Options
-
Sets the skolemDepth to the given value.
- setSolver(SATFactory) - Method in class kodkod.engine.config.Options
-
Sets the solver option to the given value.
- setSymmetryBreaking(int) - Method in class kodkod.engine.config.Options
-
Sets the symmetryBreaking option to the given value.
- sgn() - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the signum of this integer.
- sha(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the right shift of this and
the given int node, with sign extension.
- sha(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents this shifted to the right by the given Int,
with sign extension.
- sharedNodes() - Method in class kodkod.util.nodes.AnnotatedNode
-
Returns the set of all non-leaf descendants of this.node that have more than one parent.
- sharing() - Method in class kodkod.engine.config.Options
-
Returns the depth to which circuits are checked for equivalence during translation.
- shl(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the left shift of this by
the given int node.
- shl(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents this shifted to the left by the given Int.
- shortCircuit() - 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 c.
- shr(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the right shift of this and
the given int node, with zero extension.
- shr(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents this shifted to the right by the given Int,
with zero extension.
- signum() - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the sign of this int expression.
- singleton(int) - Static method in class kodkod.util.ints.Ints
-
Returns an unmodifiable IntSet whose sole
element is the given integer.
- SingletonIdentitySet<V> - Class in kodkod.util.collections
-
This is an immutable singleton set implementation that tests for
membership using reference-equality in place of object-equality when comparing elements.
- SingletonIdentitySet(V) - Constructor for class kodkod.util.collections.SingletonIdentitySet
-
Constructs a SingletonIdentitySet that will hold the given element.
- SingletonIdentitySet(Collection<? extends V>) - Constructor for class kodkod.util.collections.SingletonIdentitySet
-
Constructs a SingletonIdentitySet that will hold the first element
returned by the given collection's iterator.
- size() - Method in class kodkod.ast.Decls
-
Returns the number of decls in this Decls object.
- size() - Method in class kodkod.ast.NaryExpression
-
Returns the number of children of this expression.
- size() - Method in class kodkod.ast.NaryFormula
-
Returns the number of children of this formula.
- size() - Method in class kodkod.ast.NaryIntExpression
-
Returns the number of children of this int expression.
- size() - Method in class kodkod.engine.bool.BooleanAccumulator
-
Returns the size of this accumulator.
- size() - Method in class kodkod.engine.bool.BooleanFormula
-
Returns the number of inputs to this gate.
- size() - Method in class kodkod.engine.bool.BooleanVariable
-
Returns 0.
- size() - Method in class kodkod.engine.bool.ITEGate
-
Returns 3.
- size() - Method in class kodkod.engine.bool.NotGate
-
Returns 1.
- size() - Method in class kodkod.engine.satlab.Clause
-
Returns the size of this clause, measured in the
number of literals.
- size() - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the length of this trace.
- size() - Method in class kodkod.instance.TupleSet
-
Returns the size of this tupleset.
- size() - Method in class kodkod.instance.Universe
-
Returns the size of this universe
- size() - Method in class kodkod.util.collections.ArrayStack
-
- size() - Method in class kodkod.util.collections.CacheSet
-
Returns the number of elements in this set.
- size() - Method in class kodkod.util.collections.FixedMap
-
- size() - Method in class kodkod.util.collections.IdentityHashSet
-
- size() - Method in interface kodkod.util.collections.Indexer
-
Returns the number of keys in this.indexer.
- size() - Method in class kodkod.util.collections.LinkedStack
-
- size() - Method in class kodkod.util.collections.SingletonIdentitySet
-
Returns 1.
- size() - Method in class kodkod.util.collections.Stack
-
Returns the size of this stack.
- size() - Method in class kodkod.util.ints.ArrayIntSet
-
Returns the cardinality of this set.
- size() - Method in class kodkod.util.ints.ArrayIntVector
-
Returns the number of elements in this vector.
- size() - Method in class kodkod.util.ints.ArraySequence
-
Returns the number of entries in this sequence.
- size() - Method in class kodkod.util.ints.HomogenousSequence
-
Returns the number of entries in this sequence.
- size() - Method in class kodkod.util.ints.IntBitSet
-
Returns the cardinality of this set.
- size() - Method in interface kodkod.util.ints.IntCollection
-
Returns the number of elements in this collection.
- size() - Method in class kodkod.util.ints.IntRange
-
Returns the number of element in this range.
- size() - Method in interface kodkod.util.ints.IntSet
-
Returns the cardinality of this set.
- size() - Method in class kodkod.util.ints.IntTreeSet
-
Returns the cardinality of this set.
- size() - Method in interface kodkod.util.ints.IntVector
-
Returns the number of elements in this vector.
- size() - Method in class kodkod.util.ints.RangeSequence
-
Returns the number of entries in this sequence.
- size() - Method in interface kodkod.util.ints.SparseSequence
-
Returns the number of entries in this sequence.
- size() - Method in class kodkod.util.ints.TreeSequence
-
Returns the number of entries in this sequence.
- skolemDepth() - Method in class kodkod.engine.config.Options
-
Returns the depth to which existential quantifiers are skolemized.
- skolemizing(Decl, Relation, List<Decl>) - Method in class kodkod.engine.config.AbstractReporter
-
Reports that the given declaration is being skolemized using the
given skolem relation.
- skolemizing(Decl, Relation, List<Decl>) - Method in class kodkod.engine.config.ConsoleReporter
-
Reports that the given declaration is being skolemized using the
given skolem relation.
- skolemizing(Decl, Relation, List<Decl>) - Method in interface kodkod.engine.config.Reporter
-
Reports that the given declaration is being skolemized using the
given skolem relation.
- Solution - Class in kodkod.engine
-
Represents the full solution to a formula: an
instance if the formula is satisfiable or a
proof of unsatisfiability if not.
- Solution.Outcome - Enum in kodkod.engine
-
Enumerates the possible outcomes of an attempt
to find a model for a FOL formula.
- solve(Formula, Bounds) - Method in class kodkod.engine.IncrementalSolver
-
Adds the specified formula and bounds to the solver's state, modifies
the current solution to reflect the updated state (if needed),
and returns this solver.
- solve(Formula, Bounds) - Method in interface kodkod.engine.KodkodSolver
-
Attempts to satisfy the given formula and bounds with respect to
this.options or, optionally, prove the problem's unsatisfiability.
- solve() - Method in interface kodkod.engine.satlab.SATSolver
-
Returns true if there is a satisfying assignment for this.clauses.
- solve(Formula, Bounds) - Method in class kodkod.engine.Solver
-
Attempts to satisfy the given formula and bounds with respect to
this.options or, optionally, prove the problem's unsatisfiability.
- solveAll(Formula, Bounds) - Method in class kodkod.engine.Solver
-
Attempts to find all solutions to the given formula with respect to the specified bounds or
to prove the formula's unsatisfiability.
- solver() - Method in class kodkod.engine.config.Options
-
Returns the value of the solver options.
- solver(Options) - Static method in class kodkod.engine.IncrementalSolver
-
- Solver - Class in kodkod.engine
-
A computational engine for solving relational satisfiability problems.
- Solver() - Constructor for class kodkod.engine.Solver
-
Constructs a new Solver with the default options.
- Solver(Options) - Constructor for class kodkod.engine.Solver
-
Constructs a new Solver with the given options.
- solvingCNF(int, int, int) - Method in class kodkod.engine.config.AbstractReporter
-
- solvingCNF(int, int, int) - Method in class kodkod.engine.config.ConsoleReporter
-
- solvingCNF(int, int, int) - Method in interface kodkod.engine.config.Reporter
-
Reports that the cnf generated in stage 6, consisting of the
given number of variables and clauses, is being analyzed by
a sat solver (stage 7 of the analysis).
- solvingTime() - Method in class kodkod.engine.Statistics
-
Returns the number of miliseconds spent
on solving the CNF encoding of this.formula.
- some() - Method in class kodkod.ast.Expression
-
Returns the formula 'some this'.
- some() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a BooleanValue that constrains at least one value in this.elements to be true.
- someOf(Expression) - Method in class kodkod.ast.Variable
-
Returns the declaration that constrains this variable to
be bound to at least one element of the given expression: 'this: some expr'.
- sourceOf(Node) - Method in class kodkod.util.nodes.AnnotatedNode
-
Returns the source of the the given descendant of this.node.
- SparseSequence<V> - Interface in kodkod.util.ints
-
Represents a sparse sequence -- a sequence whose indices are not
necessarily contiguous.
- square(int, int) - Static method in class kodkod.engine.bool.Dimensions
-
Returns a new Dimensions object with n dimensions, each of
which has the specified size.
- Stack<T> - Class in kodkod.util.collections
-
Represents a last-in-first-out (LIFO) stack of objects.
- Statistics - Class in kodkod.engine
-
Stores the statistics gathered while solving
a given formula.
- stats() - Method in class kodkod.engine.Solution
-
Returns the statistics gathered while solving
this.formula.
- StrategyUtils - Class in kodkod.engine.ucore
-
A collection of utility methods for implementing
logic-level reduction strategies.
- subset(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a formula stating that the entries in this matrix are a subset of
the entries in the given matrix; i.e.
- sum() - Method in class kodkod.ast.Expression
-
Returns the sum of the integer atoms in this expression.
- sum(Decls) - Method in class kodkod.ast.IntExpression
-
Returns an integer expression that is the sum of all
values that this integer expression can take given the
provided declarations.
- sum(BooleanValue, BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is the sum bit of a full binary adder.
- sum(Collection<BooleanValue>) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns an Int that represents the sum of all values in the given collection.
- SumExpression - Class in kodkod.ast
-
Denotes the integer obtained by summing the values of an iteger expression ie
for all values of a scalar x drawn from a set e.
- superFastHash(int) - Static method in class kodkod.util.ints.Ints
-
An implementation of Paul Hsieh's hashing function,
described at http://www.azillionmonkeys.com/qed/hash.html.
- superFastHash(int...) - Static method in class kodkod.util.ints.Ints
-
An implementation of Paul Hsieh's hashing function,
described at http://www.azillionmonkeys.com/qed/hash.html.
- superFastHash(Object...) - Static method in class kodkod.util.ints.Ints
-
An implementation of Paul Hsieh's hashing function,
described at http://www.azillionmonkeys.com/qed/hash.html.
- superFastHashAvalanche(int) - Static method in class kodkod.util.ints.Ints
-
Performs the bit avalanching step of Paul Hsieh's
hashing function (http://www.azillionmonkeys.com/qed/hash.html)
- superFastHashIncremental(int, int) - Static method in class kodkod.util.ints.Ints
-
Performs the hashing step of Paul Hsieh's hashing function,
described at http://www.azillionmonkeys.com/qed/hash.html.
- symmetryBreaking() - Method in class kodkod.engine.config.Options
-
Returns the 'amount' of symmetry breaking to perform.
- SymmetryDetector - Class in kodkod.engine.fol2sat
-
Partitions a universe into equivalence classes based
on the bounding constraints given by a Bounds object.