Supported KodKod Syntax
\begin{align}
\notag problem &::= universe \ relDecl^{\ast} formula^{\ast} \\
\notag universe &::= \{atom^{\ast} \} \\
\notag relDecl &::= relation:_{arity}[constant,constant] \\
\notag constant &::= \{tuple^{\ast} \} \\
\notag tuple &::= \langle atom^{\ast} \rangle \\
\notag arity &::= positive integer \\
\notag relation &::= identifier \\
\notag atom &::= identifier \\
\notag formula &::= \\
&expr \subset expr \tag{subset} \label{syn:subset} \\
\mid \ &expr=expr \tag{equality} \label{syn:equality} \\
\mid \ &\bold{some} \ expr \tag{non_empty} \label{syn:nonempty} \\
\mid \ &\bold{one} \ expr \tag{exactly one} \label{syn:exactlyone} \\
\mid \ &\bold{lone} \ expr \tag{empty or one} \label{syn:emptyorone} \\
\mid \ &\bold{no} \ expr \tag{empty} \label{syn:empty} \\
\mid \ &\neg formula \tag{negation} \label{syn:negation} \\
\mid \ &formula \wedge formula \tag{conjuction} \label{syn:conjunction} \\
\mid \ &formula \vee formula \tag{disjunction} \label{syn:disjunction} \\
\mid \ &formula \Rightarrow formula \tag{implication} \label{syn:implication} \\
\mid \ &\forall \ varDecls \mid formula \tag{universal} \label{syn:universal} \\
\mid \ &\exists \ varDecls \mid formula \tag{existential} \label{syn:existential} \\
\mid \ &intexpr \{= \bold{\mid} < \bold{\mid} > \} \ intexpr
\tag{int comparison} \label{syn:intcomparison} \\
\notag expr &::= \\
&var \tag{variable} \label{syn:variable} \\
\mid \ &expr=expr \tag{equality} \label{syn:exprequality} \\
\mid \ &\sim expr \tag{transpose} \label{syn:transpose} \\
\mid \ &\hat \ expr \tag{clousure} \label{syn:clousure} \\
\mid \ &expr \cup expr \tag{union} \label{syn:union} \\
\mid \ &expr \cap expr \tag{intersection} \label{syn:intersection} \\
\mid \ &expr \setminus expr \tag{difference} \label{syn:difference} \\
\mid \ &expr \cdot expr \tag{join} \label{syn:join} \\
\mid \ &expr \rightarrow expr \tag{product} \label{syn:product} \\
\mid \ &formula \, ? \; expr \; : \; expr
\tag{conditional} \label{syn:conditional} \\
\mid \ &\{varDcls \mid formula \} \tag{comprehension} \label{syn:comprehension} \\
\mid \ &\pi (expr,intexpr^{\ast}) \tag{projection} \label{syn:projection} \\
\mid \ &\bold{int2expr} (intexpr) \tag{int \ cast} \label{syn:intcast} \\
\mid \ &\bold{univ} \tag{universe} \label{syn:universe} \\
\notag intexpr &\::= \\
&integer \tag{literal} \label{syn:literal} \\
\mid \ &expr \tag{cardinality} \label{syn:cardinality} \\
\mid \ &\bold{sum} \; (e) \tag{sum} \label{syn:sum} \\
\mid \ &\sum{} VarDecl \mid Expr \tag{summation} \label{syn:summation} \\
\mid \ &intexpr \; \{ + \mid \_ \mid \times \mid \div \} \; intexpr
\tag{arithmetic} \label{syn:arithmetic} \\
\mid \ &intexpr \; \{ \mid \ \mid \& \mid \hat{\; } \} \; intexpr
\tag{bitwise \ ops} \label{syn:bitwiseops} \\
\mid \ &intexpr \; \{ \ll \mid \gg \mid \ggg \} intexpr
\tag{bitshifts} \label{syn:bitshifts} \\
\notag varDecls &::= (variable:expr)^{\ast} \\
\notag variable &::= identifier \\
\end{align}