- ECFPStrategy - Class in kodkod.engine.ucore
-
A non-optimal minimization strategy based on the Empty Clause Cone algorithm.
- ECFPStrategy() - Constructor for class kodkod.engine.ucore.ECFPStrategy
-
Constructs a new instance of the empty clause cone strategy for
minimizing unsatisfiable cores.
- elseExpr() - Method in class kodkod.ast.IfExpression
-
Returns the else-expression.
- elseExpr() - Method in class kodkod.ast.IfIntExpression
-
Returns the else-expression.
- empty() - Method in class kodkod.util.collections.ArrayStack
-
- empty() - Method in class kodkod.util.collections.LinkedStack
-
Returns true if the stack is empty; otherwise returns false.
- empty() - Method in class kodkod.util.collections.Stack
-
Returns true if the stack is empty; otherwise returns false.
- EMPTY_SEQUENCE - Static variable in class kodkod.util.ints.Ints
-
An immutable empty sequence.
- EMPTY_SET - Static variable in class kodkod.util.ints.Ints
-
An immutable empty int set.
- emptyIterator() - Static method in class kodkod.util.collections.Containers
-
Returns an iterator that has no elements.
- emptySequence() - Static method in class kodkod.util.ints.Ints
-
- ensureCapacity(int) - Method in class kodkod.util.collections.ArrayStack
-
Increases the capacity of this ArrayStack, if necessary, to ensure that
it can hold at least the number of elements specified by the minimum
capacity argument.
- ensureCapacity(int) - Method in class kodkod.util.ints.ArrayIntVector
-
Increases the capacity of this MutableIntVector instance, if
necessary, to ensure that it can hold at least the number of elements
specified by the minimum capacity argument.
- entrySet() - Method in class kodkod.util.collections.FixedMap
-
Returns a set view of the mappings contained in this map.
- env() - Method in class kodkod.engine.fol2sat.TranslationRecord
-
Returns a map view of this.env.
- eq(Expression) - Method in class kodkod.ast.Expression
-
Returns the formula 'this = expr'.
- eq(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns a formula stating that the given int expression and
this have the same value.
- eq(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a formula stating that the entries in this matrix are equivalent to
the entries in the given matrix; i.e.
- eq(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 equal to the integer represented by the specified Int.
- equals(Object) - Method in class kodkod.ast.IntConstant
-
Return true if o is an IntConstant with the same value as this.
- equals(Object) - Method in class kodkod.engine.satlab.Clause
-
Returns true if o is a Clause whose literals and antecedents
are equal to those of this clause.
- equals(Object) - Method in class kodkod.instance.Tuple
-
Returns true if o is a tuple with the same sequence of atoms as this,
drawn from the same universe as this.
- equals(Object) - Method in class kodkod.instance.TupleSet
-
Returns true if o contains the same tuples as this.
- equals(Object) - Method in class kodkod.util.collections.FixedMap
-
Compares the specified object with this map for equality.
- equals(Object) - Method in class kodkod.util.collections.IdentityHashSet
-
Compares the specified object with this set for equality.
- equals(Object) - Method in class kodkod.util.collections.SingletonIdentitySet
-
Compares the specified object with this set for equality.
- equals(Object) - Method in class kodkod.util.collections.Stack
-
Returns true if o is a stack containing the same elements
as this stack, in the same order.
- equals(Object) - Method in class kodkod.util.ints.AbstractIntSet
-
Compares the specified object with this set for equality.
- equals(Object) - Method in class kodkod.util.ints.AbstractIntVector
-
Compares the specified object with this vector for equality.
- equals(Object) - Method in class kodkod.util.ints.AbstractSparseSequence
-
Compares the specified object with this sequence for equality.
- equals(Object) - Method in class kodkod.util.ints.ArrayIntSet
-
Compares the specified object with this set for equality.
- equals(Object) - Method in interface kodkod.util.ints.IndexedEntry
-
Compares the specified object with this entry for equality.
- equals(Object) - Method in class kodkod.util.ints.IntRange
-
Returns true if o is an int range with the same endpoints as this.
- equals(Object) - Method in interface kodkod.util.ints.IntSet
-
Compares the specified object with this set for equality.
- equals(Object) - Method in interface kodkod.util.ints.IntVector
-
Compares the specified object with this vector for equality.
- equals(Object) - Method in interface kodkod.util.ints.SparseSequence
-
Compares the specified object with this sequence for equality.
- evaluate(Formula) - Method in class kodkod.engine.Evaluator
-
Evaluates the specified formula with respect to the relation-tuple mappings
given by this.instance and using this.options.
- evaluate(Expression) - Method in class kodkod.engine.Evaluator
-
Evaluates the specified expession with respect to the relation-tuple mappings
given by this.instance and using this.options.
- evaluate(IntExpression) - Method in class kodkod.engine.Evaluator
-
Evaluates the specified int expession with respect to the relation-tuple mappings
given by this.instance and using this.options.
- evaluate(Formula, Instance, Options) - Static method in class kodkod.engine.fol2sat.Translator
-
Evaluates the given formula to a BooleanConstant using the provided instance and options.
- evaluate(Expression, Instance, Options) - Static method in class kodkod.engine.fol2sat.Translator
-
Evaluates the given expression to a BooleanMatrix using the provided instance and options.
- evaluate(IntExpression, Instance, Options) - Static method in class kodkod.engine.fol2sat.Translator
-
Evalutes the given intexpression to an
Int using the provided instance and options.
- Evaluator - Class in kodkod.engine
-
An evaluator for relational formulas and expressions with
respect to a given
instance
and
options.
- Evaluator(Instance) - Constructor for class kodkod.engine.Evaluator
-
Constructs a new Evaluator for the given instance, using a
default Options object.
- Evaluator(Instance, Options) - Constructor for class kodkod.engine.Evaluator
-
Constructs a new Evaluator for the given instance and options
- exactBound(int) - Method in class kodkod.instance.Bounds
-
Returns the set of tuples representing the given integer.
- ExprCastOperator - Enum in kodkod.ast.operator
-
Enumerates expression 'cast' operators.
- ExprCompOperator - Enum in kodkod.ast.operator
-
Enumerates relational comparison operators.
- expression() - Method in class kodkod.ast.Decl
-
Returns the expression in this declaration.
- Expression - Class in kodkod.ast
-
A relational expression.
- expression() - Method in class kodkod.ast.ExprToIntCast
-
Returns this.expression.
- expression() - Method in class kodkod.ast.MultiplicityFormula
-
Returns the expression of this.
- expression() - Method in class kodkod.ast.ProjectExpression
-
Returns this.expression.
- expression() - Method in class kodkod.ast.UnaryExpression
-
Returns this.expression.
- ExprOperator - Enum in kodkod.ast.operator
-
Enumerates unary (~, ^, *), binary (+, &, ++, ->, -, .) and nary (+, &, ++, ->) expression operators.
- ExprToIntCast - Class in kodkod.ast
-
An
IntExpression representing the
cardinality of an
Expression or the
sum of all the integer atoms contained in the expression.
- externalFactory(String, String, String...) - Static method in class kodkod.engine.satlab.SATFactory
-
Returns a SATFactory that produces SATSolver wrappers for the external
SAT solver specified by the executable parameter.