Logical Formulas

A boolean expression is everything that evaluates to a truth value and can thus be used as a condition.

Operations on lists of boolean values

pop_front(LIST_EXPR)
pop_back(LIST_EXPR)
LIST_EXPR[INDEX]

Boolean field access

COMPOUND_EXPR . BOOLEAN_FIELD_NAME

Verbatim truth value

true
false

Boolean operations

BOOLEAN_LHS &  BOOLEAN_RHS // Conjunction
BOOLEAN_LHS |  BOOLEAN_RHS // Disjunction
BOOLEAN_LHS == BOOLEAN_RHS // Equivalence
BOOLEAN_LHS != BOOLEAN_RHS // XOR
BOOLEAN_LHS -> BOOLEAN_RHS // Implication

Comparison

EXPR_LHS == EXPR_RHS
EXPR_LHS != EXPR_RHS
EXPR_LHS >  EXPR_RHS
EXPR_LHS >= EXPR_RHS
EXPR_LHS <  EXPR_RHS
EXPR_LHS <= EXPR_RHS

Both EXPR_LHS and EXPR_RHS must have the same type.

Negation

! BOOLEAN_EXPR

Quantification

exists (VAR) BOOLEAN_EXPR(VAR)
forall (VAR) BOOLEAN_EXPR(VAR)

For the quantification operator to work correctly, the possible assignments for VAR must be somehow restricted. Currently, the only way to do that is to use VAR as parameter of an action or fluent that defines a domain for that parameter.