Formula (Kodkod API)

java.lang.Object
- kodkod.ast.Node
- - kodkod.ast.Formula

Direct Known Subclasses:

BinaryFormula, ComparisonFormula, ConstantFormula, IntComparisonFormula, MultiplicityFormula, NaryFormula, NotFormula, QuantifiedFormula, RelationPredicate
```
public abstract class Formula
extends Node
```
A first-order formula. Unless otherwise noted, all methods in this class throw a NullPointerException when given null arguments.

Author:

Emina Torlak

Field Summary

Fields
Modifier and Type Field and Description

static Formula FALSE
Constant formula false

static Formula TRUE
Constant formula true

Fields
Modifier and Type	Field and Description
`static Formula`	`FALSE` Constant formula false
`static Formula`	`TRUE` Constant formula true

Method Summary

All Methods Static Methods Instance Methods Abstract Methods Concrete Methods
Modifier and Type	Method and Description
`abstract <E,F,D,I> F`	`accept(ReturnVisitor<E,F,D,I> visitor)` Accepts the given visitor and returns the result.
`static Formula`	`and(Collection<? extends Formula> formulas)` Returns the conjunction of the given formulas.
`static Formula`	`and(Formula... formulas)` Returns the conjunction of the given formulas.
`Formula`	`and(Formula formula)` Returns the conjunction of this and the specified formula.
`static Formula`	`compose(FormulaOperator op, Collection<? extends Formula> formulas)` Returns the composition of the given formulas using the given operator.
`static Formula`	`compose(FormulaOperator op, Formula... formulas)` Returns the composition of the given formulas using the given operator.
`Formula`	`compose(FormulaOperator op, Formula formula)` Returns the composition of this and the specified formula using the given binary operator.
`Expression`	`comprehension(Decls decls)` Returns the comprehension expression constructed from this formula and the given declarations.
`static Formula`	`constant(boolean value)` Returns the constant formula with the given value.
`Formula`	`forAll(Decls decls)` Returns a formula that represents a universal quantification of this formula over the given declarations.
`Formula`	`forSome(Decls decls)` Returns a formula that represents an existential quantification of this formula over the given declarations.
`Formula`	`iff(Formula formula)` Returns a formula that equates this and the specified formula.
`Formula`	`implies(Formula formula)` Returns the implication of the specified formula by this.
`Formula`	`not()` Returns the negation of this formula.
`static Formula`	`or(Collection<? extends Formula> formulas)` Returns the disjunction of the given formulas.
`static Formula`	`or(Formula... formulas)` Returns the disjunction of the given formulas.
`Formula`	`or(Formula formula)` Returns the conjunction of this and the specified formula.
`Formula`	`quantify(Quantifier quantifier, Decls decls)` Returns a quantification of this formula using the given quantifier over the specified declarations.
`Expression`	`thenElse(Expression thenExpr, Expression elseExpr)` Returns the if expression constructed from this formula and the specified then and else expressions.
`IntExpression`	`thenElse(IntExpression thenExpr, IntExpression elseExpr)` Returns the if expression constructed from this formula and the specified then and else integer expressions.

Methods inherited from class kodkod.ast.Node
accept, toString

Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - FALSE
```
public static final Formula FALSE
```
    Constant formula false
  - TRUE
```
public static final Formula TRUE
```
    Constant formula true
- Method Detail
  - accept
```
public abstract <E,F,D,I> F accept(ReturnVisitor<E,F,D,I> visitor)
```
    Accepts the given visitor and returns the result.
    
    Specified by:
    
    accept in class Node
    
    Returns:
    
    the result of being visited by the given visitor
    
    See Also:
    
    Node.accept(kodkod.ast.visitor.ReturnVisitor)
  - and
```
public static Formula and(Collection<? extends Formula> formulas)
```
    Returns the conjunction of the given formulas. The effect of this method is the same as calling compose(AND, formulas).
    
    Returns:
    
    compose(AND, formulas)
  - and
```
public static Formula and(Formula... formulas)
```
    Returns the conjunction of the given formulas. The effect of this method is the same as calling compose(AND, formulas).
    
    Returns:
    
    compose(AND, formulas)
  - and
```
public final Formula and(Formula formula)
```
    Returns the conjunction of this and the specified formula. The effect of this method is the same as calling this.compose(AND, formula).
    
    Returns:
    
    this.compose(AND, formula)
  - compose
```
public static Formula compose(FormulaOperator op,
                              Collection<? extends Formula> formulas)
```
    Returns the composition of the given formulas using the given operator.
    Requires:
    
    formulas.size() != 2 => op.nary()
    
    Returns:
    formulas.size() = 0 => constant(op=AND) else formulas.size() = 1 => formulas.iterator().next() else {e: Formula | e.children = formulas.toArray() and e.op = this }
  - compose
```
public static Formula compose(FormulaOperator op,
                              Formula... formulas)
```
    Returns the composition of the given formulas using the given operator.
    Requires:
    
    formulas.length != 2 => op.nary()
    
    Returns:
    formulas.length = 0 => constant(op=AND) else formulas.length=1 => formulas[0] else {e: Formula | e.children = formulas and e.op = this }
  - compose
```
public final Formula compose(FormulaOperator op,
                             Formula formula)
```
    Returns the composition of this and the specified formula using the given binary operator.
    
    Returns:
    
    {f: Formula | f.left = this and f.right = formula and f.op = op }
  - comprehension
```
public final Expression comprehension(Decls decls)
```
    Returns the comprehension expression constructed from this formula and the given declarations.
    
    Requires:
    
    all d: decls.decls[int] | decl.variable.arity = 1 and decl.multiplicity = ONE
    
    Returns:
    
    {e: Expression | e.decls = decls and e.formula = this }
  - constant
```
public static Formula constant(boolean value)
```
    Returns the constant formula with the given value.
    
    Returns:
    
    value ? TRUE : FALSE
  - forAll
```
public final Formula forAll(Decls decls)
```
    Returns a formula that represents a universal quantification of this formula over the given declarations. The effect of this method is the same as calling this.quantify(ALL, decls).
    
    Returns:
    
    this.quantify(ALL, decls)
  - forSome
```
public final Formula forSome(Decls decls)
```
    Returns a formula that represents an existential quantification of this formula over the given declarations. The effect of this method is the same as calling this.quantify(SOME, decls).
    
    Returns:
    
    this.quantify(SOME, decls)
  - iff
```
public final Formula iff(Formula formula)
```
    Returns a formula that equates this and the specified formula. The effect of this method is the same as calling this.compose(IFF, formula).
    
    Returns:
    
    this.compose(IFF, formula)
  - implies
```
public final Formula implies(Formula formula)
```
    Returns the implication of the specified formula by this. The effect of this method is the same as calling this.compose(IMPLIES, formula).
    
    Returns:
    
    this.compose(IMPLIES, formula)
  - not
```
public final Formula not()
```
    Returns the negation of this formula.
    
    Returns:
    
    {f : NotFormula | f.formula = this }
  - or
```
public static Formula or(Collection<? extends Formula> formulas)
```
    Returns the disjunction of the given formulas. The effect of this method is the same as calling compose(OR, formulas).
    
    Returns:
    
    compose(OR, formulas)
  - or
```
public static Formula or(Formula... formulas)
```
    Returns the disjunction of the given formulas. The effect of this method is the same as calling compose(OR, formulas).
    
    Returns:
    
    compose(OR, formulas)
  - or
```
public final Formula or(Formula formula)
```
    Returns the conjunction of this and the specified formula. The effect of this method is the same as calling this.compose(OR, formula).
    
    Returns:
    
    this.compose(OR, formula)
  - quantify
```
public final Formula quantify(Quantifier quantifier,
                              Decls decls)
```
    Returns a quantification of this formula using the given quantifier over the specified declarations.
    
    Returns:
    
    {f: Formula | f.decls = decls and f.formula = this and f.quantifier = quantifer }
  - thenElse
```
public final Expression thenElse(Expression thenExpr,
                                 Expression elseExpr)
```
    Returns the if expression constructed from this formula and the specified then and else expressions.
    
    Returns:
    
    {e: Expression | e.condition = this and e.thenExpr = thenExpr and e.elseExpr = elseExpr}
  - thenElse
```
public final IntExpression thenElse(IntExpression thenExpr,
                                    IntExpression elseExpr)
```
    Returns the if expression constructed from this formula and the specified then and else integer expressions.
    
    Returns:
    
    {e: IntExpression | e.condition = this and e.thenExpr = thenExpr and e.elseExpr = elseExpr}

Class Formula

Field Summary

Method Summary

Methods inherited from class kodkod.ast.Node

Methods inherited from class java.lang.Object

Field Detail

FALSE

TRUE

Method Detail

accept

and

and

and

compose

compose

compose

comprehension

constant

forAll

forSome

iff

implies

not

or

or

or

quantify

thenElse

thenElse