- Decl - Class in kodkod.ast
-
A variable declaration, such as 'x : lone X'.
- decl() - Method in exception kodkod.engine.fol2sat.HigherOrderDeclException
-
Returns this.decl
- declare(Multiplicity, Expression) - Method in class kodkod.ast.Variable
-
Returns the declaration that constrains this variable to
be bound to the specified number of the elements in the given expression: 'this: mult expr'.
- decls() - Method in class kodkod.ast.Comprehension
-
- Decls - Class in kodkod.ast
-
A sequence of decls.
- decls() - Method in class kodkod.ast.QuantifiedFormula
-
Returns this.decls.
- decls() - Method in class kodkod.ast.SumExpression
-
Returns this.decls.
- DefaultSAT4J - Static variable in class kodkod.engine.satlab.SATFactory
-
The factory that produces instances of the default sat4j solver.
- denseIndices() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the set of all indices in this matrix that contain
non-FALSE values.
- density() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the number of non-FALSE entries in this matrix.
- detectedSymmetries(Set<IntSet>) - Method in class kodkod.engine.config.AbstractReporter
-
Reports the symmetry partitions that were detected.
- detectedSymmetries(Set<IntSet>) - Method in class kodkod.engine.config.ConsoleReporter
-
Reports the symmetry partitions that were detected.
- detectedSymmetries(Set<IntSet>) - Method in interface kodkod.engine.config.Reporter
-
Reports the symmetry partitions that were detected.
- detectingSymmetries(Bounds) - Method in class kodkod.engine.config.AbstractReporter
-
Reports that symmetry detection started on the given bounds.
- detectingSymmetries(Bounds) - Method in class kodkod.engine.config.ConsoleReporter
-
Reports that symmetry detection started on the given bounds.
- detectingSymmetries(Bounds) - Method in interface kodkod.engine.config.Reporter
-
Reports that symmetry detection started on the given bounds.
- difference(Expression) - Method in class kodkod.ast.Expression
-
Returns the difference of this and the specified expression.
- difference(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a matrix representing the asymmetric difference between
the entries in this and the given matrix.
- dimension(int) - Method in class kodkod.engine.bool.Dimensions
-
Returns the size of the ith dimensions
- dimensions() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the dimensions of this matrix.
- Dimensions - Class in kodkod.engine.bool
-
Stores information about the size of a matrix.
- dims() - Method in exception kodkod.engine.CapacityExceededException
-
Returns the vector of dimensions which, when multiplied together, exceed
the representation capacity.
- directlyLearnable(IntSet) - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of all clauses in this trace that can be learned solely and directly from the
clauses with the given indices.
- divide(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the quotient of the division
between this and the given int node.
- divide(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the quotient of the division between this and the given Int.
- domain() - Method in class kodkod.ast.RelationPredicate.Function
-
Returns the domain of this.relation.
- dot(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns the dot product of this and other matrix, using conjunction instead of
multiplication and disjunction instead of addition.
- dot(Dimensions) - Method in class kodkod.engine.bool.Dimensions
-
Returns the dimensions of a matrix that would result from multiplying a
matrix of dimensions given by this by a matrix whose dimensions are
specified by dim.
- dotify(Node) - Static method in class kodkod.util.nodes.PrettyPrinter
-
Returns a dot representation of the given node that can be visualized with GraphViz.
- DynamicRCEStrategy - Class in kodkod.engine.ucore
-
Dynamic Recycling Core Extraction is a strategy for generating unsat cores that are minimal at the logic level.
- DynamicRCEStrategy(TranslationLog) - Constructor for class kodkod.engine.ucore.DynamicRCEStrategy
-
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.
- DynamicRCEStrategy(TranslationLog, double, double, double) - Constructor for class kodkod.engine.ucore.DynamicRCEStrategy
-
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.