- one() - Method in class kodkod.ast.Expression
-
Returns the formula 'one this'.
- one() - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a BooleanValue that constraints exactly one value in this.elements to be true.
- oneOf(Expression) - Method in class kodkod.ast.Variable
-
Returns the declaration that constrains this variable to
be bound to exactly one element of the given expression: 'this: one expr'.
- op() - Method in class kodkod.ast.BinaryExpression
-
Returns this.op.
- op() - Method in class kodkod.ast.BinaryFormula
-
Returns the operator of this.
- op() - Method in class kodkod.ast.BinaryIntExpression
-
Returns the operator of this.
- op() - Method in class kodkod.ast.ComparisonFormula
-
Returns the operator of this.
- op() - Method in class kodkod.ast.ExprToIntCast
-
Returns this.op.
- op() - Method in class kodkod.ast.IntComparisonFormula
-
Returns the operator of this.
- op() - Method in class kodkod.ast.IntToExprCast
-
Returns this.op
- op() - Method in class kodkod.ast.NaryExpression
-
Returns this.op.
- op() - Method in class kodkod.ast.NaryFormula
-
Returns the operator of this.
- op() - Method in class kodkod.ast.NaryIntExpression
-
Returns the operator of this.
- op() - Method in class kodkod.ast.UnaryExpression
-
Returns this.op.
- op() - Method in class kodkod.ast.UnaryIntExpression
-
Returns the operator of this.
- op() - Method in class kodkod.engine.bool.BooleanAccumulator
-
Returns the operator for this accumulator.
- op() - Method in class kodkod.engine.bool.BooleanConstant
-
Returns Operator.CONST.
- op() - Method in class kodkod.engine.bool.BooleanValue
-
Returns the operator representing the function
computed by this gate.
- op() - Method in class kodkod.engine.bool.BooleanVariable
-
Returns the VAR operator.
- op() - Method in class kodkod.engine.bool.ITEGate
-
Returns Operator.ITE.
- op() - Method in class kodkod.engine.bool.MultiGate
-
Returns the operator used to combine the input
variables of this connective gate.
- op() - Method in class kodkod.engine.bool.NotGate
-
Returns Operator.NOT.
- Operator - Class in kodkod.engine.bool
-
- Operator.Nary - Class in kodkod.engine.bool
-
An n-ary operator, where n>=2
- optimizingBoundsAndFormula() - Method in class kodkod.engine.config.AbstractReporter
-
- optimizingBoundsAndFormula() - Method in class kodkod.engine.config.ConsoleReporter
-
- optimizingBoundsAndFormula() - Method in interface kodkod.engine.config.Reporter
-
Reports that bounds optimization is in progress (stage 2).
- Options - Class in kodkod.engine.config
-
Stores information about various
user-level translation and analysis options.
- Options() - Constructor for class kodkod.engine.config.Options
-
Constructs an Options object initialized with default values.
- options() - Method in class kodkod.engine.Evaluator
-
Returns the Options object used by this evaluator.
- options() - Method in class kodkod.engine.fol2sat.Translation
-
Returns the translation options.
- options() - Method in class kodkod.engine.IncrementalSolver
-
Returns a copy of this.options.
- options() - Method in interface kodkod.engine.KodkodSolver
-
Returns the Options object used by this solver.
- options() - Method in class kodkod.engine.Solver
-
Returns the Options object used by this Solver
to guide translation of formulas from first-order
logic to cnf.
- Options.IntEncoding - Enum in kodkod.engine.config
-
- or(Formula) - Method in class kodkod.ast.Formula
-
Returns the conjunction of this and the specified formula.
- or(Formula...) - Static method in class kodkod.ast.Formula
-
Returns the disjunction of the given formulas.
- or(Collection<? extends Formula>) - Static method in class kodkod.ast.Formula
-
Returns the disjunction of the given formulas.
- or(IntExpression) - Method in class kodkod.ast.IntExpression
-
Returns an IntExpression that represents the bitwise OR of this and
the given int node.
- or(IntExpression...) - Static method in class kodkod.ast.IntExpression
-
Returns the bitwise or of the given int expressions.
- or(Collection<? extends IntExpression>) - Static method in class kodkod.ast.IntExpression
-
Returns the bitwise or of the given int expressions.
- or(BooleanValue, BooleanValue) - Method in class kodkod.engine.bool.BooleanFactory
-
Returns a boolean value whose meaning is the disjunction of the input components.
- or(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a new matrix such that an entry in the returned matrix represents a
combination of the corresponding entries in this and other matrix.
- or(BooleanMatrix...) - Method in class kodkod.engine.bool.BooleanMatrix
-
Returns a new matrix such that an entry in the returned matrix represents a
disjunction of the corresponding entries in this and other matrices.
- or(Int) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the bitwise disjunction of this and the given Int.
- or(Int...) - Method in class kodkod.engine.bool.Int
-
Returns an Int that represents the bitwise disjunction of this and the given Ints.
- OR - Static variable in class kodkod.engine.bool.Operator
-
- ordered() - Method in class kodkod.ast.RelationPredicate.TotalOrdering
-
Returns the relation representing the atoms which
are ordered by this.relation.
- ordinal() - Method in class kodkod.engine.bool.Operator
-
Returns the ordinal of this operator constant.
- outcome() - Method in class kodkod.engine.Solution
-
Returns the outcome of the attempt to find
a model for this.formula.
- override(Expression) - Method in class kodkod.ast.Expression
-
Returns the relational override of this with the specified expression.
- override(Expression...) - Static method in class kodkod.ast.Expression
-
Returns the override of the given expressions.
- override(Collection<? extends Expression>) - Static method in class kodkod.ast.Expression
-
Returns the override of the given expressions.
- override(BooleanMatrix) - Method in class kodkod.engine.bool.BooleanMatrix
-
Overrides the values in this matrix with those in other.
- override(BooleanMatrix...) - Method in class kodkod.engine.bool.BooleanMatrix
-
Overrides the values in this matrix with those in other.