- label() - Method in class kodkod.engine.bool.BooleanAccumulator
-
Returns 0.
- label() - Method in class kodkod.engine.bool.BooleanConstant
-
Returns the label for this value.
- label() - Method in class kodkod.engine.bool.BooleanValue
-
Returns the label for this value.
- label() - Method in class kodkod.engine.bool.BooleanVariable
-
Returns the label for this value.
- label() - Method in class kodkod.engine.bool.ITEGate
-
Returns this.label
- label() - Method in class kodkod.engine.bool.MultiGate
-
Returns the label for this value.
- label() - Method in class kodkod.engine.bool.NotGate
-
Returns the label for this value.
- last() - Method in class kodkod.ast.RelationPredicate.TotalOrdering
-
Returns the relation representing the last element
in the ordering imposed by this.relation.
- last() - Method in class kodkod.util.ints.AbstractSparseSequence
-
Returns the last element in this sequence, if any.
- last() - Method in class kodkod.util.ints.ArraySequence
-
Returns the entry with the largest index.
- last() - Method in class kodkod.util.ints.HomogenousSequence
-
Returns the entry with the largest index.
- last() - Method in class kodkod.util.ints.RangeSequence
-
Returns the last element in this sequence, if any.
- last() - Method in interface kodkod.util.ints.SparseSequence
-
Returns the entry with the largest index.
- last() - Method in class kodkod.util.ints.TreeSequence
-
Returns the last element in this sequence, if any.
- lastIndexOf(int) - Method in class kodkod.util.ints.AbstractIntVector
-
Returns the index in this vector of the last occurrence of the specified
element, or -1 if this vector does not contain this element.
- lastIndexOf(int) - Method in interface kodkod.util.ints.IntVector
-
Returns the index in this vector of the last occurrence of the specified
element, or -1 if this vector does not contain this element.
- leaf() - Method in exception kodkod.engine.fol2sat.UnboundLeafException
-
Returns this.leaf.
- LeafExpression - Class in kodkod.ast
-
An expression with no children.
- learnable(IntSet) - Method in interface kodkod.engine.satlab.ResolutionTrace
-
Returns the indices of all clauses in this trace that can be learned solely from the
clauses with the given indices.
- left() - Method in class kodkod.ast.BinaryExpression
-
Returns the left child of this.
- left() - Method in class kodkod.ast.BinaryFormula
-
Returns the left child of this.
- left() - Method in class kodkod.ast.BinaryIntExpression
-
Returns the left child of this.
- left() - Method in class kodkod.ast.ComparisonFormula
-
Returns the left child of this.
- left() - Method in class kodkod.ast.IntComparisonFormula
-
Returns the left child of this.
- LightSAT4J - Static variable in class kodkod.engine.satlab.SATFactory
-
The factory that produces instances of the "light" sat4j solver.
- Lingeling - Static variable in class kodkod.engine.satlab.SATFactory
-
The factory that produces instances of Armin Biere's
Lingeling solver.
- LinkedStack<T> - Class in kodkod.util.collections
-
A Stack implementation based on a singly linked list.
- LinkedStack() - Constructor for class kodkod.util.collections.LinkedStack
-
Constructs an empty stack.
- literal() - Method in class kodkod.engine.fol2sat.TranslationRecord
-
Returns this.literal.
- literals() - Method in class kodkod.engine.satlab.Clause
-
Returns an iterator over the literals in this clause,
in the ascending order of absolute values.
- log() - Method in class kodkod.engine.fol2sat.Translation.Whole
-
If translation logging was enabled (by setting
this.options.logTranslation > 0),
returns the
log of
records
generated for this translation.
- log() - Method in class kodkod.engine.Proof
-
Returns the log of the translation that resulted
in this proof.
- logTranslation() - Method in class kodkod.engine.config.Options
-
Returns the translation logging level (0, 1, or 2), where 0
means logging is not performed, 1 means only the translations of
top level formulas are logged, and 2 means all formula translations
are logged.
- lone() - Method in class kodkod.ast.Expression
-
Returns the formula 'lone this'.
- lone() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a BooleanValue that constrains at most one value in this.elements to be true.
- loneOf(Expression) - Method in class kodkod.ast.Variable
-
Returns the declaration that constrains this variable to
be bound to at most one element of the given expression: 'this: lone expr'.
- lowerBound(Relation) - Method in class kodkod.instance.Bounds
-
Returns the set of tuples that r must contain (the lower bound on r's contents).
- lowerBounds() - Method in class kodkod.instance.Bounds
-
Returns a map view of this.lowerBound.
- lt(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns a formula stating that the value of this int expression is less than the
value of the given int expression The effect
of this method is the same as calling this.compare(LT, intExpr).
- lt(Int) - Method in class kodkod.engine.bool.Int
-
Returns a BooleanValue encoding the comparator circuit
that checks whether the integer represented by this
Int is less than the integer
represented by the specified Int.
- lte(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns a formula stating that the value of this int expression is less than
or equal to the value of the given int expression The effect
of this method is the same as calling this.compare(LTE, intExpr).
- lte(Int) - Method in class kodkod.engine.bool.Int
-
Returns a BooleanValue encoding the comparator circuit
that checks whether the integer represented by this
Int is less than or equal to the integer
represented by the specified Int