Expressions and Constraints

Expressions

Expressions are anything that returns a number, boolean, or set. Boolean expressions are also called Constraints.

Information about relational expressions are found in the Sets and Relations chapters. There are two additional constructs that can be used with both boolean and relational expressions.

Let

let defines a local value for the purposes of the subexpression.

let x = A + B, y = C + D |
   x + y

In the context of the let expression x + y = (A + B) + (C + D). let is mostly used to simplify complex expressions and give meaningful names to intermediate computations.

If writing a boolean expression, you may use a {} instead of |.

let bindings are not recursive. A let binding may not refer to itself or a future let binding.

Warning

As with predicate parameters, let can shadow a global value. You can use the @ operator to retrieve the global value.

implies - else

When used in conjunction with else, implies acts as a conditional. p implies A else B returns A if p is true and B if p is false. p must be a boolean expression.

If A and B are boolean expressions, then this acts as a constraint. The else can be left out if using implies as a constraint. See below for details.

Constraints

Bar expressions

A bar expression is one of the form:

some x: Set |
  expr

In this context, the expression is true iff expr is true. The newline is optional.

Paragraph expressions

If multiple constraints are surrounded with braces, they are all and-ed together. The following two are equivalent:

expr1 or {
  expr2
  expr3
    ...
}

expr1 or (expr 2 and expr3 and ...)

Constraint Types

All constraints can be inverted with not or !. To say that A is not a subset of B, you can write A !in B, A not in B, !(A in B), etc.

Relation Constraints

`=`

A = B means that both sets of atoms or relations have the exact same elements. = cannot be used to compare two booleans. Use iff instead.

`in`

A in B means that every element of A is also an element of B. This is also known as a “subset” relation.
x in A means that x is an element of the set A.

Note

The above two definitions are equivalent as all atoms are singleton sets: x is the set containing x, so x in A is “the set containing just x is a subset of A”.

size constraints

There are four constraints on the number of elements in a set:

no A means A is empty.
some A means A has at least one element.
one A means A has exactly one element.
lone A means A is either empty or has exactly one element.

In practice, no and some are considerably more useful than one and lone.

Note

Relations are each exactly one element, no matter the order of the relation. If a, b, and c are individual atoms, (a -> b -> c) is exactly one element, while (a -> b) + (a -> c) is two.

`disj[A, B]`

disj[A, B] is the predicate “A and B share no elements in common”. Any number of arguments can be used, in which case disj is pairwise-disjoint. This means that disj[A, B, C] is equivalent to disj[A, B] and disj[B, C] and disj[A, C].

Boolean Constraints

Boolean constraints operate on booleans or predicates. They can be used to create more complex constraints.

All boolean constraints have two different forms, a symbolic form and an English form. For example, A && B can also be written A and B.

word	symbol
`and`	`&&`
`or`	`\|\|`
`not`	`!`
`implies`	`=>`
`iff`	`<=>`

The first three are self-explanatory. The other two are covered below:

`implies` (`=>`)

P implies Q is true if Q is true whenever P is true. If P is true and Q is false, then P implies Q is false. If P is false, then P implies Q is automatically true. P implies Q else T is true if P and Q are true or if P is false and T is true.

(Consider the statement x > 5 implies x > 3. If we pick x = 4, then we have false implies true).

`iff` (`<=>`)

P iff Q is true if P and Q are both true or both false. Use this for booleans instead of =.

Tip

xor[A, B] can be written as A <=> !B.

Quantifiers

A quantifier is an expression about the elements of a set. All of them have the form

some x: A |
  expr

This expression is true if expr is true for any element of the set of atoms A. As with let, x becomes a valid identifier in the body of the constraint.

Instead of using a pipe, you can also write it as

some x: Set {
  expr1
  ...
}

In which case it is treated as a standard paragraph expression.

The following quantifiers are available:

some x: A | expr is true for at least one element in A.
all x: A | expr is true for every element in A.
no x: A | expr is false for every element of A.
[A] one x: A | expr is true for exactly one element of A.
[A] lone x: A is equivalent to (one x: A | expr) or (no x: A | expr).

As discussed below, one and lone can have some unintuitive consequences.

Tip

As with all constraints, A can be any set expression. So you can write some x: (A + B - C).rel, etc.

Multiple Quantifiers

There are two syntaxes to quantify over multiple elements:

-- 1
some x, y, ...: A | expr

-- 2
some x: A, y: B, ... | expr

For case (1) all elements will be drawn from A. For case (2) the quantifier will be over all possible combinations of elements from A and B. The two forms can be combined, as in all x, y: A, z: B, ... | expr.

Elements drawn do not need to be distinct. This means, for example, that the following is automatically false if A has any elements:

all x, y: A |
  x.rel != y.rel

As we can pick the same element for x and y. If this is not your intention, there are two ways to fix this:

-- 1
all x, y: A |
  x != y => x.rel != y.rel

-- 2
all disj x, y: A |
  x.rel != y.rel

For case (1) we can still select the same element for x and y; however, the x != y clause will be false, making the whole clause true. For case (2), using disj in a quantifier means we cannot select the same element for two variables.

one and lone behave unintuitively when used in multiple quantifiers. The following two statements are different:

one f, g: S | P[f, g] -- 1
one f: S | one g: S | P[f, g] -- 2

Constraint (1) is only true if there is exactly one pair f, g that satisfies predicate P. Constraint (2) says that there’s exactly one f such that there’s exactly one g. The following truth table will satisfy clause (2) but not (1):

f	g	P[f, g]
A	B	T
A	C	T
B	A	T
B	C	T
C	B	T
C	A	F

As C is the only one where there is exactly one g that satisfies P[C, g]. As a rule of thumb, use only some and all when writing multiple clauses.

Relational Quantifiers

When using a run command, you can define a some quantifier over a relation:

sig Node {
    edge: set Node
}

pred has_self_loop {
    some e: edge | e = ~e

}

run {
    has_self_loop
}

When using a check command, you can define all and no quantifiers over relations:

assert no_self_loops {
        no e: edge | e = ~e
      }

check no_self_loops

You cannot use all or no in a run command or use some in a check command. You cannot use higher-order quantifiers in the Evaluator regardless of the command.