language.tex

\section{Input Languages}\label{sec:language}

This section provides an overview of the input languages of
grounder \gringo, combined grounder and solver \clingo, and solver \clasp.
The joint input language of \gringo\ and \clingo\ is detailed in
Section~\ref{subsec:lang:gringo}.
Finally, Section~\ref{subsec:lang:clasp} is dedicated to the inputs handled by \clasp.

\subsection{Input Language of \gringo\ and \clingo}\label{subsec:lang:gringo}

The tool \gringo~\cite{gescth07a} is a grounder capable of transforming
user-defined logic programs (usually containing variables) into
equivalent ground (that is, variable-free) programs.
The output of \gringo\ can be piped into solver \clasp~\cite{gekanesc07a,gekasc09c},
which then computes answer sets.
System \clingo\ internally couples \gringo\ and \clasp, thus,
it takes care of both grounding and solving.
In contrast to \gringo\ outputting ground programs,
\clingo\ returns answer sets.

Usually, logic programs are specified in one or more (text) files whose names are
provided as arguments in an invocation of either \gringo\ or \clingo.
In what follows, 
we describe the constructs belonging to the input language of \gringo\ and \clingo.

\subsubsection{Terms}\label{subsec:gringo:terms}
\index{term}
\index{term!constant}
\index{term!string}
\index{term!variable}
\index{term!anonymous variable}
\index{term!function}
\index{term!integer}
\index{term!\code{\#sup}}
\index{term!\code{\#inf}}

\begin{figure}
\railnontermfont{\rmfamily\itshape}%
\railalias{rusc}{\tt\char95}\railterm{rusc}
\railalias{rlsc}{[A-Za-z0-9\tt\char95']}\railterm{rlsc}
\railalias{any}{[\^{}\symbol{92}"$\dlsh$]}\railterm{any}
\railalias{bs}{\symbol{92}}\railterm{bs}
\railalias{esc}{[\symbol{92}"n]}\railterm{esc}
\begin{rail}
  term        : simpleterm | function | tuple;
  simpleterm  : (integer | constant | string | variable | rusc | '\#sup' | '\#inf');
  constant    : (rusc*) '[a-z]' (rlsc*);
  string      : '"' ((any | (bs esc))*) '"';
  variable    : (rusc*) '[A-Z]' (rlsc*);
  function    : constant '(' term (',' term*) ')';
  tuple       :          '(' (term (',' | ',' term+))? ')';
\end{rail}
\caption{Grammar for Terms.\label{fig:terms}}
\end{figure}

Every (non-propositional) logic program includes \emph{terms},
mainly to specify the arguments of atoms (see below).
The grammar for \gringo's (and \clingo's) terms is shown in Figure~\ref{fig:terms}.

% syntax: simple terms
The basic building blocks are simple terms:
\emph{integers}, \emph{constants}, \emph{strings}, and \emph{variables}
as well as the tokens `\var{\char`\_}', \const{\#sup}, and \const{\#inf}.
An integer is represented by means of an arithmetic expression,
further explained in Section~\ref{subsec:gringo:arith}.
Constants and variables are distinguished by their first letters,
which are \emph{lowercase} and \emph{uppercase}, respectively,
where leading occurrences of `\code{\char`\_}' are allowed
(may be useful to circumvent name clashes).
Furthermore, a string is an arbitrary sequence of characters
enclosed in double quotes (\code{"$\cdot$"}),
where any occurrences of `\code{\textbackslash}', newline, and double quote
must be escaped via `\code{\textbackslash\textbackslash}', `\code{\textbackslash n}',
or `\code{\textbackslash"}', respectively.

% semantics: simple terms
While a constant or string represents itself,
a variable is a placeholder for \emph{all} variable-free terms
in the language of a logic program.%
\footnote{The set of all terms constructible from the available
          constants and function symbols is called \emph{Herbrand universe}.}
Unlike a variable name whose recurrences within a rule refer to the same variable,
the token `\var{\char`\_}' (not followed by any letter)
% Note: currently, there is the hidden feature: not p(_) where _ is *not* an anonymous variable
stands for an \emph{anonymous variable} that does not recur anywhere.
(One can view this as if a new variable name is invented on each occurrence of `\var{\char`\_}'.)
In addition, there are the special constants \const{\#sup} and \const{\#inf}
representing the greatest and smallest element among all variable-free terms%
\footnote{Their is a total order defined on variable-free terms; for details see Section~\ref{subsec:gringo:comp}.}
, respectively;
we illustrate their use in Section~\ref{subsec:gringo:aggregate}.

% syntax: tuples and functions
Next, (uninterpreted) \emph{functions} are complex terms composed of a name (like a constant)
and one or more terms as arguments.
For instance,
\code{\const{at}(\const{peter},\const{time}(12),X)}
is a function with three arguments:
constant \const{peter}, another function \code{\const{time}(12)}
with an integer argument, and variable~\var{X}.
Finally, there are \emph{tuples},
which are similar to \emph{functions} but without a name.
Examples for tuples are:
the empty tuple \code{()} and
the tuple \code{(\const{at},\const{peter},\const{time}(12),X)} with four elements.
Tuples may optionally end in a comma `\code{,}'
for distinguishing one-elementary tuples.
That is, \code{($t$,)} is a one-elementary tuple,
while a term of form \code{($t$)} is equivalent to \code{$t$}.
For instance, \code{(42,)} is a one-elementary tuple, whereas \code{(42)} is not,
and the above quadruple is equivalent to \code{(\const{at},\const{peter},\const{time}(12),X,)}.

\subsubsection{Normal Programs and Integrity Constraints}\label{subsec:gringo:normal}
Rules of the following forms are admitted in a
\emph{normal logic program} (with integrity constraints):
\begin{align*}
\textbf{Fact:} & \quad \code{$A_0$.} \\
\textbf{Rule:} & \quad \code{$A_0$ :- $L_1$,$\dots$,$L_n$.} \\
\textbf{Integrity Constraint:} & \quad \code{\phantom{$A_0$} :- $L_1$,$\dots$,$L_n$.}
\end{align*}
\index{logic program}
\index{logic program!normal}%
\index{rule!fact}%
\index{rule!normal}%
\index{rule!integrity constraint}%
The \emph{head}~$A_0$ of a rule or a fact is an \emph{atom} of the same
syntactic form as a constant or function.
\index{atom}%
\index{atom|seealso{literal}}%
In the \emph{body} of a rule or an integrity constraint,
every $L_j$ for $1\leq j\leq n$ is a \emph{literal} of the form $A$ or $\code{not}~A$,
where $A$ is an atom and
the connective \code{not} denotes default negation.
\index{literal}%
\index{literal|seealso{atom}}%
\index{negation|seealso{literal}}%
\index{negation!default}%
We say that a literal~$L$ is \emph{positive} if it is an atom,
and \emph{negative} otherwise.
While the head atom~$A_0$ of a fact must unconditionally be true,
the intuitive reading of a rule corresponds to an implication:
if all positive literals in the rule's body are true and all negative
literals are satisfied, then~$A_0$ must be true.
On the other hand, an integrity constraint is a rule that filters solution candidates,
meaning that the literals in its body must not jointly be satisfied.

A set of (propositional) atoms is called a \emph{model} of a logic program if it satisfies all rules, facts, and integrity constraints.
Atoms are considered true if and only if they are in the model.
In ASP, a model is called an \emph{answer set} if every atom in the model has an (acyclic) derivation from the program.
%
See~\cite{gellif88b,gelfond08a,lifschitz08a} for formal definitions of answer sets of logic programs.

To get the idea, let us consider some small examples.
%
\begin{example}\label{ex:as:one}
Consider the following logic program:
%
\begin{lstlisting}[numbers=none]
a :- b.
b :- a.
\end{lstlisting}
%
When \pred{a} and \pred{b} are false, the bodies of both rules are false as well,
so that the rules are satisfied.
Furthermore, there is no (true) atom to be derived,
which shows that the empty set is an answer set.
On the other hand, 
if \pred{a} is true but \pred{b} is not,
then the first rule is unsatisfied because the body holds but the head does not.
Similarly, the second rule is unsatisfied if \pred{b} is true and \pred{a} is not.
Hence, an answer set cannot contain only one of the atoms \pred{a} and~\pred{b}.
It remains to investigate the set including both \pred{a} and~\pred{b}.
Although both rules are satisfied,
\pred{a} and~\pred{b} cannot be derived acyclically:
\pred{a} relies on~\pred{b}, and vice versa.
That is, the set including both \pred{a} and~\pred{b} is not an answer set.
Hence, the empty set is the only answer set of the logic program.
We say that there is a \emph{positive cycle} through \pred{a} and~\pred{b}
subject to minimization.
\end{example}

Consider the following logic program:
%
\begin{lstlisting}[numbers=none]
a :- not b.
b :- not a.
\end{lstlisting}
%
Here, the empty set is not a model because both rules are unsatisfied.
However, the sets containing only~\pred{a} or only~\pred{b} are models.
To see that each of them is an answer set,
note that~\pred{a} is derived by the rule \code{\pred{a}\,:-\:not\:\pred{b}.}
if \pred{b} is false;
similarly,
\pred{b} is derived by \code{\pred{b}\,:-\:not\:\pred{a}.}
if \pred{a} is false.
Note that the set including both~\pred{a} and~\pred{b} is not an answer set
because neither atom can be derived if both are assumed to be true:
the bodies of the rules
\code{\pred{a}\,:-\:not\:\pred{b}.} and
\code{\pred{b}\,:-\:not\:\pred{a}.} are false.
Hence, we have that
either~\pred{a} or~\pred{b} belongs to
an answer set of the logic program.

To illustrate the use of facts and integrity constraints,
let us augment the previous logic program:
\begin{lstlisting}[numbers=none]
a :- not b.
b :- not a.
c.
:- c, not b.
\end{lstlisting}
Since \code{\pred{c}.} is a fact,
atom \pred{c} must unconditionally be true, i.e.,
it belongs to every model.
In view of this,
the integrity constraint
\code{:-\:c,\:not\:\pred{b}.}
tells us that \pred{b} must be true as well
in order to prevent its body from being satisfied.
However, this kind of reasoning does not provide us with
a derivation of \pred{b}.
Rather, we still need to make sure that the body
of the rule \code{\pred{b}\,:-\:not\:\pred{a}.} is satisfied,
so that atom~\pred{a} must be false.
Hence, the set containing \pred{b} and~\pred{c}
is the only answer set of our logic program.

In the above examples,
we used propositional logic programs to exemplify the idea
of an answer set: a model of a logic program such that all its true atoms are
(acyclically) derivable.
In practice, logic programs are typically non-propositional, i.e.,
they include schematic rules with variables.
The next example illustrates this.

\begin{example}\label{ex:flies}
Consider a child from the south pole watching cartoons,
where it sees a yellow bird that is not a penguin.
The child knows that penguins can definitely not fly (due to small wingspread),
but it is unsure about whether the yellow bird flies.
This knowledge is generalized by
the following schematic rules:
%
\lstinputlisting{examples/fly.lp}
%
The first rule expresses that it is generally possible that a bird flies,
unless the contrary, subject to the second rule, is the case.
The definite knowledge that penguins cannot fly
is specified by the third rule.

Later on, the child learns that the yellow bird
is a chicken called ``tweety'',
while its favorite penguin is called ``tux''.
The knowledge about these two individuals is
represented by the following facts:
\lstinputlisting[firstnumber=4]{examples/bird.lp}

When we instantiate the variable~\var{X} in the three schematic rules
with \const{tweety} and \const{tux},
we obtain the following ground rules:
%
\lstinputlisting[numbers=none,xrightmargin=-15pt,nolol]{examples/gfly.lp}
%
Further taking into account that \const{tweety} and \const{tux} are known to
be birds, that \const{tux} is a penguin, while \const{tweety} is not, and that
penguins can definitely not fly,
we can simplify the previous ground rules to obtain the following ones:%
\marginlabel{The reader can reproduce these ground rules
             by invoking:\\
             \code{\mbox{~}clingo --text \textbackslash\\
                   \mbox{~}\attach{examples/bird.lp}{bird.lp} \attach{examples/fly.lp}{fly.lp}}\\
             or alternatively:\\
             \code{\mbox{~}gringo --text \textbackslash\\
                   \mbox{~}\attach{examples/bird.lp}{bird.lp} \attach{examples/fly.lp}{fly.lp}}}
%
\lstinputlisting[numbers=none,nolol]{examples/sfly.lp}
%
Now it becomes apparent that \const{tweety}
may fly or not, while \const{tux} surely does not fly.
Thus, there are two answer sets for the three schematic rules above,
instantiated with \const{tweety} and \const{tux}.%
\marginlabel{To compute both answer sets,
             invoke:\\
             \code{\mbox{~}clingo \attach{examples/bird.lp}{bird.lp} \textbackslash\\
                   \mbox{~}\attach{examples/fly.lp}{fly.lp} 0}\\
             or alternatively:\\
             \code{\mbox{~}gringo \attach{examples/bird.lp}{bird.lp} \textbackslash\\
                   \mbox{~}\attach{examples/fly.lp}{fly.lp} | clasp 0}}
\end{example}

The above example illustrated how variables are used to represent all instances of
rules with respect to the language of a logic program.
In fact, grounder \gringo\ (or the grounding component of \clingo)
takes care of instantiating variables
such that an equivalent propositional logic program is obtained.
To this end,
rules are required to be \emph{safe},
\label{pg:safe}%
\index{safety}%
i.e.,
all variables in a rule must occur in some positive literal
(a literal not preceded by \code{not}) in the body of the rule.
For instance, the first two schematic rules in Example~\ref{ex:flies}
are safe because they include \code{\pred{bird}(\var{X})} in their positive bodies.
This tells \gringo\ (or \clingo)
that the values to be substituted for~\var{X} are limited to birds.

Up to now, we have introduced terms, facts, (normal) rules, and integrity constraints.
Before we proceed to describe handy extensions to this simple core language,
keep in mind that the role of a rule (or fact) is that an atom in the
head can be derived to be true if the body is satisfied.
Unlike this, an integrity constraint implements a test,
but it cannot be used to derive any atom.
This universal meaning still applies when more sophisticated language constructs,
as described in the following, are used.

\subsubsection{Classical Negation}\label{subsec:gringo:negation}
\index{negation!classical}

The connective \code{not} expresses default negation,
i.e., a literal $\code{not}~A$ is assumed to hold unless atom~$A$ is derived to be true.
In contrast, the classical (or strong) negation of an atom~\cite{gellif91a}
holds only if it can be derived.
Classical negation, indicated by symbol `\code{-}', is permitted in front of atoms.
That is, if $A$ is an atom, then $\code{-}A$ is
an atom representing the complement of~$A$.
The semantic relationship between $A$ and~$\code{-}A$
is simply that they
must not jointly hold.
Hence,
classical negation can be understood as a syntactic feature
allowing us to impose an integrity constraint \code{:-\;$A$,\:-$A$.}
without explicitly writing it in a logic program.
Depending on the logic program at hand,
it may be possible that neither~$A$ nor~$\code{-}A$ is contained in an answer set,
thus representing a state where the truth and the falsity of~$A$ are both unknown.

\begin{example}\label{ex:flies:neg}
Using classical negation,
we can rewrite the schematic rules in Example~\ref{ex:flies}
in the following way:
%
\lstinputlisting{examples/flycn.lp}
%
Given the individuals \const{tweety} and \const{tux},
classical negation is reflected by
the following (implicit) integrity constraints:%
\marginlabel{By invoking:\\
  \code{\mbox{~}clingo --text \textbackslash\\
        \mbox{~}\attach{examples/bird.lp}{bird.lp} \attach{examples/flycn.lp}{flycn.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash\\
        \mbox{~}\attach{examples/bird.lp}{bird.lp} \attach{examples/flycn.lp}{flycn.lp}}\\
the reader can observe
that the integrity constraint in Line~4 is indeed part of the grounding.
The second one in Line 5 is not printed;
it becomes obsolete by a static analysis exhibiting that
\const{tux} does surely not fly.}
%
\begin{lstlisting}[firstnumber=4]
:- fly(tweety), -fly(tweety).
:- fly(tux),    -fly(tux).
\end{lstlisting}
There are still two answer sets,
containing \code{-\pred{fly}(\const{tux})} and
either \code{\pred{fly}(\const{tweety})} or \code{-\pred{fly}(\const{tweety})}.

Now assume that we add the following fact to the program:
\begin{lstlisting}[numbers=none]
fly(tux).
\end{lstlisting}
Then,
\code{\pred{fly}(\const{tux})} must unconditionally be true,
and \code{-\pred{fly}(\const{tux})} is still derived by
an instance of the third schematic rule.
Since every answer set candidate containing
both \code{\pred{fly}(\const{tux})} and \code{-\pred{fly}(\const{tux})}
triggers
the (implicit) integrity constraint in Line~5,
there is no longer any answer set.
\end{example}

\subsubsection{Disjunction}\label{subsec:gringo:disjunction}
\index{logic program!disjunctive}
\index{rule!disjunctive}
Disjunctive logic programs permit connective~`\code{;}' between atoms in rule heads.%
\footnote{Note that disjunction in rule heads was not supported by \clasp\ and \clingo\ versions before series~3 and~4, respectively.}
\begin{align*}
\textbf{Fact:} & \quad \code{$A_0$;\dots;$A_m$.} \\
\textbf{Rule:} & \quad \code{$A_0$;\dots;$A_m$ :- $L_1$,$\dots$,$L_n$.}
\end{align*}
A disjunctive head holds if at least one of its atoms is true.
Answer sets of a disjunctive logic program satisfy a minimality criterion
that we do not detail here
(see~\cite{eitpol06a,gekasc11b} for an implementation methodology in disjunctive ASP).
We only mention that the simple disjunctive program \code{\pred{a};\pred{b}.} has two answer sets,
one containing~\pred{a} and another one containing~\pred{b},
while both atoms do not jointly belong to an answer set.
After adding the rules of Example~\ref{ex:as:one}, a single answer set containing both~\pred{a} and~\pred{b} is obtained.
This illustrates that disjunction in ASP is neither strictly exclusive or inclusive but subject to minimization.

In general, the use of disjunction may increase
computational complexity~\cite{eitgot95a}.
We thus suggest to use ``choice constructs'' (detailed in Section~\ref{subsec:gringo:aggregate})
instead of disjunction, unless the latter is required for complexity reasons.

\subsubsection{Double Negation and Head Literals}\label{subsec:gringo:double}
\index{negation!double}
\index{literal!head}

The input language of \gringo\ also supports double default negated literals,
written $\code{not}~\code{not}~A$.
They are satisfied whenever their positive counterparts are.
But like negative literals of form $\code{not}~A$,
double negated ones are also preceded by \code{not} and 
do thus not require an (acyclic) derivation from the program;
it is sufficient that they are true in the model at hand.

Consider the logic program:
\begin{lstlisting}[numbers=none]
a :- not not b.
b :- not not a.
\end{lstlisting}
%
This program has an empty answer set, like the program in Example~\ref{ex:as:one},
as well as the additional answer set containing both \pred{a} and \pred{b}.
This is because neither `\code{not not a}' nor `\code{not not b}' requires an acyclic derivation from the program.
Note that, in contrast to Example~\ref{ex:as:one},
the above program does not induce
mutual positive dependencies between~\pred{a} and~\pred{b}.
Given this, \pred{a} and~\pred{b} can thus be both true or false, just like in classical logic.

Also, negative literals are admitted in the head of rules.
When disregarding disjunction,
this offers just another way to write integrity constraints,
putting the emphasis on the head literal.
In fact, the rule
\(\code{not}~A_0\)~\code{:-}~\(L_1\text{\code{,}}\dots\text{\code{,}}L_n\)\code{.}
is equivalent to
\code{:-}~\(L_1\text{\code{,}}\dots\text{\code{,}}L_n\text{\code{,}}\code{not}~\code{not}~A_0\)\code{.},
and with double negation in the head, rule
\(\code{not}~\code{not}~A_0\)~\code{:-}~\(L_1\text{\code{,}}\dots\text{\code{,}}L_n\)\code{.}
is equivalent to
\code{:-}~\(L_1\text{\code{,}}\dots\text{\code{,}}L_n\text{\code{,}}\code{not}~A_0\)\code{.}

\begin{example}\label{ex:as:flynn}
Consider the logic program:

\marginlabel{To compute both answer sets, invoke:\\
  \code{\mbox{~}clingo \attach{examples/bird.lp}{bird.lp} \textbackslash\\
        \mbox{~}\attach{examples/flynn.lp}{flynn.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo~\attach{examples/bird.lp}{bird.lp} \textbackslash\\
        \mbox{~}\attach{examples/flynn.lp}{flynn.lp} | clasp 0}
}
\lstinputlisting{examples/flynn.lp}
The possibility that a bird flies is expressed with a double negation in the first line.
Solutions with flying penguins are filtered out in the second line.
Like in Example~\ref{ex:flies} there are two answer sets,
but without an explicit atom to indicate that a bird does not fly.
Hence, the answer set where tweety does not fly contains no atoms over predicate \pred{fly}/$1$.
\end{example}

\begin{note}
  Note that negative head literals are also supported in disjunctions.
  For more information see \cite{litatu99a}.
\end{note}

\subsubsection{Boolean Constants}
\index{atom!Boolean constant}
%
Sometimes it is useful to have literals possessing a constant truth value.
Literals over the two \emph{Boolean constants} \code{\#true} and \code{\#false},
which are always true or false, respectively,
have a constant truth value.

\begin{example}
Consider the following program:
\marginlabel{%
  The unique answer set of the program,
  can be inspected by invoking:\\
  \code{\mbox{~}clingo \attach{examples/bool.lp}{bool.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/bool.lp}{bool.lp} \textbackslash \\ \mbox{~}| clasp 0}\\
  Note that this program simply produces an empty grounding:
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/bool.lp}{bool.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/bool.lp}{bool.lp}}
  }
%
\lstinputlisting{examples/bool.lp}
The first rule uses \code{\#true} in the head.
Because this rule is a fact, it is trivially satisfied.
Similarly, the rules in Line~2 and~3 have satisfied heads.
The bodies of the last three integrity constraints are false.
Hence, the constraints do not cause a conflict.
Note that neither of the rules above derives any atom.
Thus, we obtain the empty answer set for the program.
\end{example}
See Example~\ref{ex:sort} below for an application of interest.
\subsubsection{Built-in Arithmetic Functions}\label{subsec:gringo:arith}
\index{term!integer}
\index{term!arithmetic function@\gobblecomma|see{arithmetic function}}
\index{arithmetic function}
\index{arithmetic function!addition, \code{+}}
\index{arithmetic function!subtraction, \code{-}}
\index{arithmetic function!unary minus, \code{-}}
\index{arithmetic function!multiplication, \code{*}}
\index{arithmetic function!division, \code{/}}
\index{arithmetic function!modulo, \code{\textbackslash}}
\index{arithmetic function!exponentiation, \code{**}}
\index{arithmetic function!absolute value, \mbox{\textbar$\cdot$\textbar}}
\index{arithmetic function!bitwise and, \code{\&}}
\index{arithmetic function!bitwise or, \code{?}}
\index{arithmetic function!bitwise xor, \code{\^}}
\index{arithmetic function!bitwise complement, \code{\textasciitilde}}

Besides integers (constant arithmetic functions),
written as sequences of the digits \code{0}\dots\code{9}
possibly preceded by `\code{-}',
\gringo\ and \clingo\ support a variety of arithmetic functions that
are evaluated during grounding.
The following symbols are used for these functions:
\code{+} (addition),
\code{-} (subtraction, unary minus),
\code{*} (multiplication),
\code{/} (integer division),
\code{\textbackslash} (modulo),
\code{**} (exponentiation),
\code{|$\cdot$|} (absolute value),
\code{\&} (bitwise AND),
\code{?} (bitwise OR),
\code{\^} (bitwise exclusive OR), and
\code{\textasciitilde} (bitwise complement).

\begin{example}\label{ex:arith:fun}
The usage of arithmetic functions is illustrated by the program:%
\marginlabel{%
  The unique answer set of the program,
  obtained after evaluating all arithmetic functions,
  can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/arithf.lp}{arithf.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/arithf.lp}{arithf.lp}}}
%
\lstinputlisting{examples/arithf.lp}
%
Note that the variables~\var{L} and~\var{R} are instantiated to~\const{7} and~\const{2},
respectively, before arithmetic evaluations.
Consecutive and non-separative (e.g., before `\code{(}')
spaces can optionally be dropped.
The four bitwise functions apply to signed integers,
using two's complement arithmetic.
\end{example}

\begin{note}\label{note:simple}
An occurrence of a variable in the scope of an arithmetic function
only counts as positive in the sense of safety (cf.\ Page~\pageref{pg:safe}) for simple arithmetic terms.
Such simple arithmetic terms are terms with exactly one variable occurrence
composed of the arithmetic functions `\code{+}', `\code{-}', `\code{*}', and integers.
Moreover,
if multiplication is used, then the constant part must not evaluate to $0$ for the variable occurrence to be considered positive.
E.g., the rule~\code{\pred{q}(\var{X})\,:-\:\pred{p}(\const{2}*(\var{X}+\const{1})).}
is considered safe, but
the rule~\code{\pred{q}(\var{X})\,:-\:\pred{p}(\var{X}+\const{X}).} is not.
\index{safety!arithmetic function}
\end{note}

\subsubsection{Built-in Comparison Predicates}\label{subsec:gringo:comp}
\index{comparison predicate}
\index{comparison predicate!inequality, \code{"!=}}
\index{comparison predicate!less, \code{<}}
\index{comparison predicate!less or equal, \code{<=}}
\index{comparison predicate!greater, \code{>}}
\index{comparison predicate!greater or equal, \code{>=}}
\index{atom!comparison predicate@\gobblecomma|see{comparison predicate}}

Grounder \gringo\ (and \clingo)
feature a total order among variable-free terms (without arithmetic functions).
The built-in predicates to compare terms are
\code{=} (equal),
\code{!=} (not equal),
\code{<} (less than),
\code{<=} (less than or equal),
\code{>} (greater than), and
\code{>=} (greater than or equal).
\emph{Comparison literals} over the above \emph{comparison predicates} are used like
other literals (cf.\ Section~\ref{subsec:gringo:normal})
but are evaluated during grounding.

\begin{example}\label{ex:arith:pred}
The application of comparison literals to integers
is illustrated by the following program:%
\marginlabel{%
  The simplified ground program obtained by evaluating built-ins
  can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash}\\
  \code{\mbox{~}\attach{examples/arithc.lp}{arithc.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash}\\
  \code{\mbox{~}\attach{examples/arithc.lp}{arithc.lp}}}
%
\lstinputlisting{examples/arithc.lp}
%
The last two lines hint at the fact that arithmetic functions are evaluated
before comparison literals, so that the latter actually compare the
results of arithmetic evaluations.
\end{example}

\begin{example}\label{ex:symb:pred}
Comparison literals can also be applied to constants and functions,
as illustrated by the following program:%
\marginlabel{%
  As above, by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/symbc.lp}{symbc.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/symbc.lp}{symbc.lp}}\\
  one can inspect the simplified ground program
  obtained by evaluating built-ins.}
%
\lstinputlisting{examples/symbc.lp}
%
Integers are compared in the usual way, constants are ordered lexicographically,
and functions both structurally and lexicographically.
Furthermore, all integers are smaller than constants,
which in turn are smaller than functions.
\end{example}

The built-in comparison predicate~`\code{=}' has another interesting use case. 
Apart from just testing whether a relation between two terms holds,
it can be used to define shorthands (via unification) for terms.

\begin{example}\label{ex:define}
This usage is illustrated by the following program:%
\marginlabel{%
  The simplified ground program can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/define.lp}{define.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/define.lp}{define.lp}}}
%
\lstinputlisting[lastline=2,belowskip=0pt]{examples/define.lp}%
\lstinputlisting[firstline=3,aboveskip=0pt,numbers=none,nolol]{examples/define.lp}
%
The body of the rule in Line~2 defines four comparison predicates over~`\code{=}',
which directly or indirectly depend on~\var{X} and~\var{Y}.
The values of~\var{X} and~\var{Y} are obtained via instances of the predicate \pred{num}/$1$.
The first comparison predicate depends on~\var{X} to provide shortcut~\var{XX}.
Similarly, the second comparison predicate depends on~\var{Y} to provide shortcut~\var{YY}.
The third comparison predicate provides variable \var{Y'} because it occurs in a simple arithmetic term,
which is solved during unification.
The last comparison predicate provides no variables and,
hence, is just a test,
checking whether its left-hand and right-hand sides are equal.
\end{example}

\begin{example}\label{ex:unify}
This example illustrates how to unify with function terms and tuples:
\marginlabel{%
  The simplified ground program can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/unify.lp}{unify.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/unify.lp}{unify.lp}}}
%
\lstinputlisting{examples/unify.lp}
%
Here, \code{\const{f}(\const{a},\var{X},\var{X}+\const{1})} or
\code{(\const{a},\var{X},\var{X}+\const{1})}, respectively,
is unified with instances of the predicate \code{sym}/$1$.
To this end,
arguments of \code{sym}/$1$ with matching arity
are used to instantiate the variable~\var{X} occurring
as the second argument in terms on the left-hand sides of~\code{=}.
With a value for~\var{X} at hand,
we can further check whether the arithmetic evaluation of~\code{\var{X}+\const{1}},
occurring as the third argument, coincides with the
corresponding value given on the right-hand side of~`\code{=}'.
%
\end{example}

\begin{note}
Note that comparison literals can be preceded by \code{not} or \code{not}~\code{not}.
In the first case, this is equivalent to using the complementary comparison literal
(e.g.,~`\code{<}' and~`\code{>=}' complement each other).
In the second case, the prefix has no effect on the meaning of the literal.

An occurrence of a variable in the scope of a built-in comparison literal over~`\code{!=}', `\code{<}', `\code{<=}',`\code{>}', or `\code{>=}'
does not count as a positive occurrence in the sense of safety (cf.\ Page~\pageref{pg:safe}),
i.e.,
such comparison literals are not considered to be positive.

Unlike with the built-in comparison literals above,
comparisons predicates over~`\code{=}' are considered as positive (body) literals in the sense of safety (cf.\ Page~\pageref{pg:safe}),
so that variables occurring on one side can be instantiated.
However, this only works when unification can be made directionally,
i.e., it must be possible to instantiate one side without knowing the values of variables on the other side.
For example, the rule~\code{\pred{p}(\var{X})\,:-\:\var{X}\:=\:\var{Y},\:\var{Y}\:=\:\var{X}.}
is not accepted by \gringo\ (or \clingo)
because values for~\var{X} rely on values for~\var{Y}, and vice versa.
Only simple arithmetic terms can be unified with (cf.\ Remark~\ref{note:simple}).
Hence, variable~\var{X} in literal~\code{X*X=8} must be bound by some other positive literal.
%
\index{safety!comparison predicate}%
\end{note}

\subsubsection{Intervals}\label{subsec:gringo:interval}
\index{term!interval}

Line~1 of Example~\ref{ex:define} contains
five facts of the form \code{\pred{num}($k$).}
over consecutive integers~$k$.
For a more compact representation,
\gringo\ and \clingo\ support integer intervals of the form $i$\code{..}$j$.
Such an interval, representing each integer~$k$ such that $i\leq k\leq j$,
is expanded during grounding.
An interval is expanded differently depending on where it occurs.
In the head of a rule, an interval is expanded conjunctively,
while in the body of a rule, it is expanded disjunctively.
So we could have simply written \code{num(1..5).} to represent the five facts.

\begin{example}\label{ex:int}
Consider the following program:
\marginlabel{%
  The simplified ground program obtained from intervals
  can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \attach{examples/int.lp}{int.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \attach{examples/int.lp}{int.lp}}}
\lstinputlisting{examples/int.lp}
Because all intervals in the second rule occur in the rule head,
they expand conjunctively.
Furthermore, the two intervals expand into the cross product \code{(1..3)$\times$(1..3)},
resulting in the following set of facts:
\begin{lstlisting}[escapechar=@,firstnumber=2]
grid(1,1).  grid(1,2).  grid(1,3).@\\@grid(2,1).  grid(2,2).  grid(2,3).@\\@grid(3,1).  grid(3,2).  grid(3,3).
\end{lstlisting}
Similarly, intervals can be used in a rule body.
Typically, this is done using comparison literals over `\code{=}', which expand disjunctively:
\begin{lstlisting}[firstnumber=2]
grid(X,Y) :- X = 1..S, Y = 1..S, size(S).
\end{lstlisting}
This rule expands into the same set of facts as before.
But intervals in comparison literals have the advantage that additional constraints can be added.
For example, one could add the comparison literals \code{X-Y!=0} and \code{X+Y-1!=S}
to the rule body to exclude the diagonals of the grid.
\end{example}

\begin{note}
An occurrence of a variable in the specification of the bounds
of an integer interval, like~\var{S} in Line~2 of Example~\ref{ex:int},
does not count as a positive occurrence
in the sense of safety (cf.\ Page~\pageref{pg:safe}).
Hence, such a variable must also have another positive occurrence elsewhere;
here in \lstinline{size(S)}.
\index{safety!interval}%
\end{note}

\subsubsection{Pooling}\label{subsec:gringo:pool}
\index{pooling, \code{;}}
\index{term!pooling@\gobblecomma|see{pooling}}
\index{atom!pooling@\gobblecomma|see{pooling}}

The token `\code{;}' admits pooling alternative terms
to be used as arguments of an atom, function, or tuple.
Argument lists written in the form \code{($\dots$,X;Y,$\dots$)} abbreviate multiple options:
\code{($\dots$,X),\linebreak[1]\:(Y,$\dots$)}.
Pools are expanded just like intervals, i.e.,
conjunctively in the head and disjunctively in the body of a rule.
In fact, the interval \code{1..3} is equivalent to the pool \code{(1;2;3)}.%
\footnote{%
We make use of the fact that one-elementary tuples
must be made explicit by a trailing `\code{,}' (cf.\ Section~\ref{subsec:gringo:terms}).
E.g., \code{(1;1,)} expands into \code{(1)} and \code{(1,)},
where \code{(1)} is equal to the integer~\code{1}.
On the other hand, note that the rule
\code{\pred{p}(\var{X})\,:-\;\var{X}\;=\,(1,2;3,4).}
is expanded into 
\code{\pred{p}((1,2)).} and \code{\pred{p}((3,4)).},
given that \code{(1,2)} and \code{(3,4)} are proper tuples,
and the same facts are also obtained from
\code{\pred{p}((1,2;3,4)).}
Unlike that, \code{\pred{p}(1,2;3,4).} yields
\code{\pred{p}(1,2).} and \code{\pred{p}(3,4).}
because `\code{;}' here splits an argument list,
rather than a tuple.}
\begin{example}\label{ex:pool}
The following program makes use of pooling.
It is similar to Example~\ref{ex:int}
but with the difference that, unlike intervals, pools have a fixed size:%
\marginlabel{%
  The simplified ground program obtained from pools
  can be inspected by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash\newline\mbox{~}\attach{examples/pool.lp}{pool.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/pool.lp}{pool.lp}}}
\lstinputlisting[xrightmargin=-5pt]{examples/pool.lp}
%
Because all pools in this rule occur in the head,
they are expanded conjunctively.
Furthermore, the two pools expand into the cross product \code{(1..3)$\times$(1..3)},
resulting again in the following set of facts:
\begin{lstlisting}[numbers=none]
grid(1,1).  grid(1,2).  grid(1,3).
grid(2,1).  grid(2,2).  grid(2,3).
grid(3,1).  grid(3,2).  grid(3,3).
\end{lstlisting}
Like intervals, pools can also be used in the body of a rule,
where they are expanded disjunctively:
\begin{lstlisting}
grid(X,Y) :- X = (1;2;3), Y = (1;2;3).
\end{lstlisting}
This rule expands into the same set of facts as before.
As in Example~\ref{ex:int}, additional constraints involving~\code{X} and~\code{Y} can be added.
\end{example}

For another example on pooling, featuring non-consecutive elements, see Section~\ref{subsec:color:instance}.

\subsubsection{Conditions and Conditional Literals}\label{subsec:gringo:condition}
\index{aggregate!condition}
\index{conditional literal}%
\index{literal!conditional}%
%
A \emph{conditional literal} is of the form
\[\code{$L_0$:$L_1$,$\dots$,$L_n$}\]
%
where every $L_j$ for $0\leq j\leq n$ is a \emph{literal},
\code{$L_1$,$\dots$,$L_n$} is called \textit{condition},
and `\code{:}' resembles mathematical set notation.
Whenever $n=0$, we get a regular literal and denote it as usual by $L_0$.

For example, the rule
\begin{lstlisting}[numbers=none]
a :- b : c.
\end{lstlisting}
yields \code{a} whenever either \code{c} is false (and thus no matter whether \code{b} holds or not) or both \code{b} and \code{c} are true.

\begin{note}
Logically, $L_0$ and \code{$L_1$,$\dots$,$L_n$} act as
head and body, respectively,
which gives \code{$L_0$:$L_1$,$\dots$,$L_n$} 
the flavor of a nested implication
(see~\cite{haliya14a} for details).
\end{note}

Together with variables,
conditions allow for specifying collections of expressions within a single rule or aggregate.
This is particularly useful for encoding conjunctions (or disjunctions) over
arbitrarily many ground atoms as well as for the compact representation of aggregates
(detailed in Section~\ref{subsec:gringo:aggregate}).

\begin{example}\label{ex:cond}
The following program uses, in Line~5 and~6, conditions in a rule body and in a rule head, respectively:
%
\lstinputlisting{examples/cond.lp}
%
The rules in Line~5 and~6 are instantiated as follows:%
\marginlabel{%
  The reader can reproduce these ground rules by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/cond.lp}{cond.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/cond.lp}{cond.lp}}}
\begin{lstlisting}[numbers=none]
meet :- available(jane), available(john).
on(mon); on(tue); on(wed); on(thu); on(fri) :- meet.
\end{lstlisting}
%
The conjunction in the body of the first ground rule is obtained by replacing~\var{X} in
\code{\pred{available}(\var{X})} with all ground terms~$t$ such that
\code{\pred{person}($t$)} holds, namely, with $t=\const{jane}$ and $t=\const{john}$.
Furthermore, the condition in the head of the rule in Line~6 turns into
a disjunction over all ground instances of
\code{\pred{on}(\var{X})} such that \var{X} is substituted by terms~$t$
for which \code{\pred{day}($t$)} holds.
That is, conditions in the body and in the head of a rule
are expanded to different basic language constructs.\footnote{%
Recall our suggestion from Section~\ref{subsec:gringo:disjunction}
to use ``choice constructs'' (detailed in Section~\ref{subsec:gringo:aggregate})
instead of disjunction, unless the latter is required for complexity reasons.
This also means that conditions must not be used \emph{outside of aggregates} in rule heads
if disjunction is unintended.}
\end{example}

Further following set notation,
a condition can be composed by separating literals with a comma, viz.~`\code{,}'.
Note that commas are used to separate both literals in rule bodies as well as conditions.
To resolve this ambiguity,
a condition is terminated with a semicolon `\code{;}' (rather than `\code{,}')
when further body literals follow.

\begin{example}\label{ex:sort}
The following program uses a literal with a composite condition in the middle of the rule body.
Note the semicolon `\code{;}' after the condition:
%
\lstinputlisting[breaklines,breakatwhitespace]{examples/sort.lp}
%
The conditional literal in the second rule evaluates to false
whenever there is an element~\code{Y} between~\code{X} and~\code{Z}.
Hence, all rule instantiations where~\code{X} and~\code{Z} are not direct successors are discarded
because they have a false body.
On the other hand, whenever~\code{X} and~\code{Z} succeed each other,
the condition is false for all elements~\code{Y}.
This means that the literal with condition stands for an empty conjunction, which is true:%
\marginlabel{%
  The reader can reproduce these ground rules by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/sort.lp}{sort.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/sort.lp}{sort.lp}}}%
\begin{lstlisting}[numbers=none]
set(1). set(2). set(3). set(4).
next(1,2). next(2,3). next(3,4).
\end{lstlisting}
We obtain an answer set where the elements of \code{set}/$1$ are ordered via \code{next}/$2$.
\end{example}

\begin{note}\label{note:domain}
There are three important issues about the usage of conditions:
\begin{enumerate}
%
\item
Any variable occurring within a condition
does not count as a positive occurrence outside the condition
in the sense of safety (cf.\ Page~\pageref{pg:safe}).
Variables occurring in atoms not subject to any condition are \emph{global}.
Each variable within an atom in front of a condition
must be global or have a positive occurrence on the right-hand side of
the condition.
%
\item
During grounding,
the instantiation of global variables takes precedence over non-global ones,
that is, the former are instantiated before the latter.
As a consequence, variables that occur globally are substituted by terms
before a condition is further evaluated.
Hence, the names of variables in conditions must be chosen with care,
making sure that they do not \emph{accidentally} match the names of global variables.
%
\item
We suggest using \emph{domain predicates}~\cite{lparseManual}
or built-ins (both used in Line~3  of Example~\ref{ex:sort})
in conditions.
\index{domain predicate}%
\label{pg:domain}%
Literals over such predicates are completely evaluated during grounding.
In a logic program, domain predicates can be recognized by observing
that they are neither subject to negative recursion (through \code{not})
nor to disjunction or ``choice constructs'' (detailed in Section~\ref{subsec:gringo:aggregate})
in the head of any rule.
The domain predicates defined in Example~\ref{ex:sort} are
\pred{set}/$1$ and \pred{next}/$1$.
Literals with such conditions expand to arbitrary length disjunctions or conjunctions in the head or body of a rule, respectively.
Otherwise, conditions give rise to nested implications.
For further details see~\cite{haliya14a}.
\end{enumerate}
\end{note}

\subsubsection{Aggregates}\label{subsec:gringo:aggregate}
\index{atom!aggregate@\gobblecomma|see{aggregate}}
\index{aggregate}

Aggregates are expressive modeling constructs that allow for forming values from groups of selected items.
Together with comparisons they allow for expressing conditions over these terms.
For instance, we may state that the sum of a semester's course credits must be at least 20,
or that the sum of prizes of shopping items should not exceed 30 Euros.

More formally,
an aggregate is a function on a set of tuples that are normally subject to conditions.
By comparing an aggregated value with given values, we can extract a truth value from an aggregate's evaluation,
thus
obtaining an aggregate atom.
Aggregate atoms come in two variants depending on whether they occur in a rule head or body.

\paragraph{Body Aggregates}
The form of an \emph{aggregate atom} occurring in a rule body is as follows:
\index{aggregate!body}
%
\[\code{$s_1$~$\prec_1$~$\alpha$~\{~$\boldsymbol{t}_1$:$\boldsymbol{L}_1$;$\dots$;$\boldsymbol{t}_n$:$\boldsymbol{L}_n$ \}~$\prec_2$~$s_2$}\]
%
Here, all $\boldsymbol{t}_i$ and $\boldsymbol{L}_i$, forming \emph{aggregate elements}, are tuples of terms and literals
(as introduced in Section~\ref{subsec:gringo:terms}), respectively.
If a literal tuple is empty and the corresponding term tuple is non-empty, then the colon can be omitted.
$\alpha$ is the name of some function that is to be applied to the term tuples $\boldsymbol{t}_i$
that remain after evaluating the conditions expressed by $\boldsymbol{L}_i$.
%
Finally,
the result of applying $\alpha$ is compared by means of the comparison predicates $\prec_1$ and $\prec_2$
to the terms $s_1$ and~$s_2$, respectively.
Note that one of the \emph{guards} `\code{$s_1$~$\prec_1$}' or `\code{$\prec_2$~$s_2$}'
(or even both) can be omitted;
left out comparison predicates $\prec_1$ or $\prec_2$ default to `\code{<=}',
thus interpreting~$s_1$ and~$s_2$ as lower or upper bound, respectively.

Currently, \gringo\ (and \clingo) support the aggregates
\code{\#count}
\index{aggregate!count, \code{\#count}}%
(the number of elements; used for expressing cardinality constraints),
\code{\#sum}
\index{aggregate!sum, \code{\#sum}}%
(the sum of weights; used for expressing weight constraints),
\code{\#sum+}
\index{aggregate!sum plus, \code{\#sum+}}%
(the sum of positive weights),
\code{\#min}
\index{aggregate!minimum, \code{\#min}}%
(the minimum weight), and
\code{\#max}
\index{aggregate!maximum, \code{\#max}}%
(the maximum weight).
The weight refers to the first element of a term tuple.
Aggregate atoms, as described above, are obtained by writing
either \code{\#count}, \code{\#sum}, \code{\#sum+}, \code{\#min}, or \code{\#max} for~$\alpha$.
%
Note that, unlike the other aggregates, the \code{\#count} aggregate does not require weights.

For example,
instances of the natural language examples for aggregates given at the beginning of this section
can be expressed as follows.
%
\begin{lstlisting}[numbers=none]
20 <= #sum { 4 : course(db);      6 : course(ai);
             8 : course(project); 3 : course(xml) }

#sum { 3 : bananas; 25 : cigars; 10 : broom } <= 30
\end{lstlisting}
Both aggregate atoms can be used in the body of a rule like any other atom, possibly preceded by negation.
Within both aggregate atoms,
atoms like \lstinline{course(ai)} or \lstinline{broom} are associated with weights.
Assuming that \lstinline{course(db)}, \lstinline{course(ai)} as well as \lstinline{bananas} and \lstinline{broom} are true,
the aggregates inner sets evaluate to \lstinline[mathescape]{$\{$4;6$\}$} and \lstinline[mathescape]{$\{$3;10$\}$}, respectively.
After applying the \lstinline{#sum} aggregate function to both sets, we get \lstinline{20 <= 10} and \lstinline{13 <= 30};
hence, in this case, the second aggregate atom holds while the first one does not.

As indicated by the curly braces, the elements within aggregates are treated as members of a set.
Hence, duplicates are not accounted for twice.
%
For instance, the following aggregate atoms express the same:
\begin{lstlisting}[numbers=none,escapechar=@]
#count { 42 : a;         t : not b            } = 2
#count { 42 : a; 42 : a; t : not b; t : not b } = 2
\end{lstlisting}
That is, if \lstinline{a} holds but not \lstinline{b}, both inner sets reduce to \lstinline[mathescape]{$\{$42;t$\}$};
and so both aggregate atoms evaluate to true.
%
However, both are different from the aggregate
\begin{lstlisting}[numbers=none,escapechar=@]
#count { 42 : a; t : not b; s : not b } = 2
\end{lstlisting}
that holds if both \lstinline{a} and \lstinline{b} are false,
yielding \lstinline[mathescape]{#count$\{$t;s$\}$ = 2}.

Likewise, the elements of other aggregates are understood as sets.
%
Consider the next two summation aggregates:
\begin{lstlisting}[numbers=none]
#sum { 3 : cost(1,2,3); 3 : cost(2,3,3) } = 3
#sum { 3,1,2 : cost(1,2,3);
       3,2,3 : cost(2,3,3) } = 6
\end{lstlisting}
As done in Section~\ref{subsec:tsp:instance},
an atom like \lstinline{cost(1,2,3)} can be used to represent an arc from node \lstinline{1} to \lstinline{2} with cost \lstinline{3}.
If both \lstinline{cost(1,2,3)} and \lstinline{cost(2,3,3)} hold,
the first sum evaluates to \lstinline{3}, while the second yields \lstinline{6}.
Note that all term tuples, the singular tuple \lstinline{3} as well as the ternary tuples \lstinline{3,1,2} and \lstinline{3,2,3}
share the same weight, viz.~\lstinline{3}.
However,
the set property makes the first aggregate count edges with the same cost only once,
while the second one accounts for each edge no matter whether they have the same cost or not.
To see this, observe that after evaluating the conditions in each aggregate, the first one reduces to
\lstinline[mathescape]{#sum$\{$3$\}$}, while the second results in \lstinline[mathescape]{#sum$\{$3,1,2;3,2,3$\}$}.
In other words, associating each cost with its respective arc enforces a multi-set property;
in this way, the same cost can be accounted for several times.

\paragraph{Head Aggregates}
Whenever a rule head is a (single) aggregate atom, the derivable head literals must be distinguished.
This is done by appending such atoms (or in general literals) separated by an additional `:' to the tuples of the aggregate elements:
\index{aggregate!head}
%
\[\code{$s_1$~$\prec_1$~$\alpha$~\{~$\boldsymbol{t}_1$:$L_1$:$\boldsymbol{L_1}$;$\dots$;$\boldsymbol{t}_n$:$L_n$:$\boldsymbol{L_n}$~\}~$\prec_2$~$s_2$}\]
%
Here, all $L_i$ are literals as introduced in Section~\ref{subsec:gringo:normal},
while all other entities are as described above.
The second colon in
\code{$\boldsymbol{t}_i$:$L_i$:$\boldsymbol{L_i}$}
is dropped whenever $\boldsymbol{L_i}$ is empty,
yielding
\code{$\boldsymbol{t}_i$:$L_i$}.

\begin{note}
Aggregate atoms in the head can be understood as a combination of unrestricted choices with body aggregates enforcing the constraint expressed by the
original head aggregate.
In fact, when producing \smodels\ format, all aggregate atoms occurring in rule heads are transformed away.
For details consult~\cite{siniso02a,gekakasc12a}.
\end{note}

\paragraph{Shortcuts}
There are some shorthands that can be used in the syntactic representation of aggregates.
%
The expression
%
\[\code{$s_1$~$\prec_1$~\{~$L_1$:$\boldsymbol{L_1}$;$\dots$;$L_n$:$\boldsymbol{L_n}$~\}~$\prec_2$~$s_2$}\]
%
where all entities are defined as above
is a shortcut for
%
\[\code{$s_1$~$\prec_1$~\#count \{ $\boldsymbol{t}_1$:$L_1$:$\boldsymbol{L_1}$;$\dots$;$\boldsymbol{t}_n$:$L_n$:$\boldsymbol{L_n}$~\}~$\prec_2$~$s_2$}\]
%
if it appears in the head of a rule, and
it is a shortcut for
%
\[\code{$s_1$~$\prec_1$~\#count~\{~$\boldsymbol{t}_1$:$L_1$,$\boldsymbol{L_1}$;$\dots$;$\boldsymbol{t}_n$:$L_n$,$\boldsymbol{L_n}$~\}~$\prec_2$~$s_2$}\]
%
if it appears in the body of a rule.
In both cases, all $\boldsymbol{t}_i$ are pairwise distinct term tuples generated by \gringo\
whenever the distinguished (head) literals $L_i$ are different.
%
Just like with aggregates, the guards~`\code{$s_1$~$\prec_1$}' and~`\code{$\prec_2$~$s_2$}' are optional, and the symbols `$\prec_1$' and `$\prec_2$' default to `\code{<=}' if omitted.

For example, the rule
\begin{lstlisting}[numbers=none]
{ a; b }.
\end{lstlisting}
is expanded to
\begin{lstlisting}[numbers=none]
#count { 0,a : a; 0,b : b }.
\end{lstlisting}
Here, \gringo\ generates two distinct term tuples \lstinline{0,a} and \lstinline{0,b}.
With \clingo, we obtain four answer sets representing all sets over \code{a} and \code{b}.

Recurrences of literals yield identical terms, as we see next.
The rule
\begin{lstlisting}[numbers=none]
{ a; a }.
\end{lstlisting}
is expanded to
\begin{lstlisting}[numbers=none]
#count { 0,a : a; 0,a : a }.
\end{lstlisting}

In fact, within the term tuple produced by \gringo,
the first term indicates the number of preceding default negations,
and the second reproduces the atom as a term in order to make the whole term tuple unique.
%
To see this, observe that the integrity constraint
\begin{lstlisting}[numbers=none]
:- { a; not b; not not c } > 0.
\end{lstlisting}
is expanded to
\begin{lstlisting}[numbers=none]
:- #count { 0,a : a; 
            1,b : not b;
            2,c : not not c } > 0.
\end{lstlisting}

\begin{note}
By allowing the omission of \const{\#count},
so-called ``cardinality constraints''~\cite{siniso02a}
can almost be written in their traditional notation (without keyword, yet different separators),
as put forward in the \lparse\ grounder~\cite{lparseManual}.
\end{note}

Having discussed head and body aggregate atoms,
let us note that there is a second way to use body aggregates:
they act like positive literals when used together with comparison predicate~`\code{=}'.
For instance, variable~\var{X} is safe in the following rules:
\begin{lstlisting}[numbers=none]
cnt(X) :- X = #count { 2 : a; 3 : a }.
sum(X) :- X = #sum   { 2 : a; 3 : a }.
pos(X) :- X = #sum+  { 2 : a; 3 : a }.
min(X) :- X = #min   { 2 : a; 3 : a }.
max(X) :- X = #max   { 2 : a; 3 : a }.
\end{lstlisting}
Under the assumption that atom~\pred{a} holds,
the atoms 
\code{\pred{cnt}(\const{2})},
\code{\pred{sum}(\const{5})},
\code{\pred{pos}(\const{5})},
\code{\pred{min}(\const{2})}, and
\code{\pred{max}(\const{3})} are
derived by the above rules.
If~\pred{a} does not hold, we derive
\code{\pred{cnt}(\const{0})},
\code{\pred{sum}(\const{0})},
\code{\pred{pos}(\const{0})},
\code{\pred{min}(\const{\#sup})}, and
\code{\pred{max}(\const{\#inf})}.
%
Here, the special constants \const{\#sup} and \const{\#inf}
(introduced in Section~\ref{subsec:gringo:terms}),
obtained by applying \code{\#min} and \code{\#max} to the empty set of weights,
indicate the neutral elements of the aggregates.
%
These constants can also be used as weights, subject to
\code{\#min} and \code{\#max} (in order to exceed any other ground term):
\begin{lstlisting}[numbers=none]
bot :-      #min { #inf : a } -1000.
top :- 1000 #max { #sup : a }.
\end{lstlisting}
Assuming that atom~\pred{a} holds,
the atoms~\pred{bot} and~\pred{top} are derived by the above rules
because both \code{\#inf <= -1000} and \code{1000 <= \#sup} hold
(cf.~Section~\ref{subsec:gringo:comp} for details how terms are ordered).

\begin{note}\label{rem:aggr-assign}
Although it seems convenient to use aggregates together with the `\code{=}'~predicate,
this feature should be used with care.
If the literals of an aggregate belong to domain predicates (see Remark~\ref{note:domain}) or built-ins,
the aggregate is evaluated during grounding to exactly one value.
Otherwise, if the literals do not belong to domain predicates,
the value of an aggregate is not known during grounding,
in which case \gringo\ or \clingo\ unwraps all possible outcomes of the
aggregate's evaluation.
The latter can lead to a space blow-up,
which should be avoided whenever possible.
For instance, unwrapping the aggregate in
\begin{lstlisting}[numbers=none]
{ a; b; c }.
:- #sum { 1 : a; 2 : b; 3 : c } = N, N > 3.
\end{lstlisting}
yields three integrity constraints:
\begin{lstlisting}[numbers=none]
:- #sum { 1 : a; 2 : b; 3 : c } = 4.
:- #sum { 1 : a; 2 : b; 3 : c } = 5.
:- #sum { 1 : a; 2 : b; 3 : c } = 6.
\end{lstlisting}
Such duplication does not happen
when we use a comparison predicate instead:
\begin{lstlisting}[numbers=none]
:- #sum { 1 : a; 2 : b; 3 : c } > 3.
\end{lstlisting}
Hence, it is advisable to rather apply comparison predicate~`\code{>}' directly.
In general, aggregates should only be used to bind variables
if they refer solely to domain predicates and built-ins.
\end{note}

\paragraph{Non-ground Aggregates}

After considering the syntax and semantics of ground aggregate atoms,
we now turn our attention to non-ground aggregates.
Regarding contained variables,
only variable occurrences in the guards give rise to global variables.
Hence, any variable in an aggregate element must be bound by either a positive global occurrence or a variable
that occurs positively in its condition $\boldsymbol{L_i}$.
\index{safety!aggregate}
Variable names in aggregate elements have to be chosen carefully to avoid clashes with global variables.
Furthermore, pools and intervals in aggregate elements give rise to multiple aggregate elements;
very similar to the disjunctive unpacking of pools and intervals in rules.
The following example, making exhaustive use of aggregates,
demonstrates a variety of features
(note that it ignores Remark~\ref{rem:aggr-assign}).

\begin{example}\label{ex:aggr}
Consider a situation where an informatics student
wants to enroll for a number of courses at the beginning of a new term.
In the university calendar, eight courses are found eligible,
and they are represented by the following facts:
%
\lstinputlisting[xrightmargin=-20pt,lastline=8]{examples/aggr.lp}
%
In an instance of \const{course}/$3$,
the first argument is a number identifying one of the eight courses,
and the third argument provides the course's contact hours per week.
The second argument stands for a subject area:
\const{1} corresponding to ``theoretical informatics'',
\const{2}               to ``practical informatics'',
\const{3}               to ``technical informatics'',
and~\const{4}               to ``applied informatics''.
For instance, atom \code{\const{course}(\const{1},\const{2},\const{5})}
expresses that course~\const{1} accounts for~\const{5} contact hours per week
that may be credited to subject area~\const{2} (``practical informatics'').
Observe that a single course is usually eligible for multiple
subject areas.

After specifying the above facts,
the student starts to provide personal constraints on the courses to enroll.
The student's first condition is to enroll in~\const{3} to~\const{6} courses:
%
\lstinputlisting[nolol,firstline=11,lastline=11,firstnumber=9]{examples/aggr.lp}
%
Instantiating the above \const{\#count} aggregate
yields the following ground rule:%
\marginlabel{%
  The full ground program is obtained by invoking:\\
  \code{\mbox{~}clingo --text \textbackslash \\ \mbox{~}\attach{examples/aggr.lp}{aggr.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \textbackslash \\ \mbox{~}\attach{examples/aggr.lp}{aggr.lp}}}
%
\begin{lstlisting}[numbers=none]
3 <= #count { 0,enroll(1) : enroll(1);
              0,enroll(2) : enroll(2);
              0,enroll(3) : enroll(3);
              0,enroll(4) : enroll(4);
              0,enroll(5) : enroll(5);
              0,enroll(6) : enroll(6);
              0,enroll(7) : enroll(7);
              0,enroll(8) : enroll(8) } <= 6.
\end{lstlisting}
%
Observe that an instance of atom~\code{\const{enroll}(\var{C})} is included for each
instantiation of~\var{C} such that \code{\const{course}(\var{C},\var{S},\var{H})}
holds for some values of~\var{S} and~\var{H}.
Duplicates resulting from distinct values for~\var{S} are removed, thus
obtaining the above set of ground atoms.

The next constraints of the student regard the subject areas of enrolled courses:
%
\lstinputlisting[nolol,firstline=13,lastline=16,firstnumber=10]{examples/aggr.lp}
%
Each of the three integrity constraints above contains a \code{\#count} aggregate,
in which `\code{,}' is used to construct composite conditions
(introduced in Section~\ref{subsec:gringo:condition}).
Recall that aggregates operate on sets and thus duplicates are removed;
hence, we use term tuples to take into account courses together with their subject areas.
Thus, the integrity constraint in Line~10 is instantiated as follows:%
\footnote{Because contact hours are uniquely associated to a course,
\gringo's shortcut expansion of \lstinline{:- \{ course(C,S,H) : enroll(C) \} 10.} is equivalent to the rule in Line~10 here.
Similar equivalences hold for the other \code{\#count} aggregates.}
%
\begin{lstlisting}[firstnumber=10,stepnumber=10]
:- 10 >= #count { 1,1 : enroll(1); 1,2 : enroll(1);
                  2,1 : enroll(2); 2,2 : enroll(2);
                  3,1 : enroll(3); 3,3 : enroll(3);
 4,1 : enroll(4); 4,3 : enroll(4); 4,4 : enroll(4);
                  5,1 : enroll(5); 5,4 : enroll(5);
                  6,2 : enroll(6); 6,3 : enroll(6);
 7,2 : enroll(7); 7,3 : enroll(7); 7,4 : enroll(7);
                  8,3 : enroll(8); 8,4 : enroll(8) }.
\end{lstlisting}
%
Note that courses~\const{4} and~\const{7} count three times because
they are eligible for three subject areas, viz., there are three
distinct instantiations for~\var{S} in
\code{\const{course}(\var{4},\var{S},\const{3})} and
\code{\const{course}(\var{7},\var{S},\const{4})}, respectively.
Comparing the above ground instance,
the meaning of the integrity constraint in Line~10 is that the
number of eligible subject areas over all enrolled courses
must be more than~\const{10}.
Similarly, the integrity constraint in Line~11 expresses the requirement
that at most one course of subject area~\const{2} (``practical informatics'')
is not enrolled,
while Line~12 stipulates that the enrolled courses
amount to less than six nominations of
subject area~\const{3} (``technical informatics'')
or~\const{4} (``applied informatics'').

The remaining constraints of the student deal with contact hours.
To express them, we first introduce an auxiliary rule and a fact:
%
\lstinputlisting[nolol,firstline=18,lastline=19,firstnumber=14]{examples/aggr.lp}
%
The rule in Line~14 projects instances of \pred{course}/$3$ to
\pred{hours}/$2$, thereby, dropping courses' subject areas.
This is used to not consider the same course multiple times within the following
integrity constraints:%
\footnote{Alternatively, we could also use \lstinline{course(C,_,H).}}
%
\lstinputlisting[nolol,firstline=21,lastline=23,firstnumber=16,breakatwhitespace,breaklines]{examples/aggr.lp}
%
As illustrated in Line~16,
we may use default negation via `\code{not}' in front of aggregate atoms,
and bounds may be specified by terms with variables.
In fact, by instantiating~\var{M} to~\const{20},
we obtain the following ground instance of the integrity constraint in Line~16:
%
\begin{lstlisting}[firstnumber=16,stepnumber=16]
:- not 18 <= #sum {
        5,1 : enroll(1); 4,2 : enroll(2);
        6,3 : enroll(3); 3,4 : enroll(4);
        4,5 : enroll(5); 2,6 : enroll(6);
        4,7 : enroll(7); 5,8 : enroll(8) } <= 20.
\end{lstlisting}
%
The above integrity constraint states that the \const{\#sum} of contact hours per week
must lie in-between~\const{18} and~\const{20}.
Note that the \const{\#min} and \const{\#max} aggregates in Line~17 and~18, respectively,
work on the same set of aggregate elements as in Line~16.
While the integrity constraint in Line~17 stipulates that any course to enroll
must include more than~\const{2} contact hours,
the one in Line~18 prohibits enrolling for courses of~\const{6} or more contact hours.
Of course, the last two requirements could also be formulated as follows:
%
\begin{lstlisting}[firstnumber=17]
:- enroll(C), hours(C,H), H <= 2.
:- enroll(C), hours(C,H), H >= 6.
\end{lstlisting}

Finally, the following rules illustrate the use of aggregates together with comparison predicate~`\code{=}'.
%
\lstinputlisting[nolol,firstline=25,lastline=26,firstnumber=19]{examples/aggr.lp}
%
The role of aggregates here is different from before,
as they now serve to bind an integer to variable~\var{N}.
The effect of Line~19 and~20,
which do not follow the recommendation in Remark~\ref{rem:aggr-assign},
is that the student can read off the number of courses to enroll and 
the amount of contact hours per week from instances of \pred{courses}/$1$ and \pred{hours}/$1$
belonging to an answer set.%
\marginlabel{%
  To compute the unique answer set of the program, invoke:\\
  \code{\mbox{~}clingo \attach{examples/aggr.lp}{aggr.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/aggr.lp}{aggr.lp} | \textbackslash\\
        \mbox{~}clasp 0}}
%
In fact, running \clingo\ or \clasp\ shows
that a unique collection of~\const{5} courses to enroll satisfies all requirements:
the courses~\const{1}, \const{2}, \const{4}, \const{5}, and~\const{7},
amounting to~\const{20} contact hours per week.
%
\end{example}

\begin{note}
Users familiar with \gringo~3 may remember that conditions in aggregates
had to be either literals over domain predicates or built-ins.
This restriction does not exist anymore in \gringo\ and \clingo~4.
\end{note}

\subsubsection{Optimization}\label{subsec:gringo:optimize}
\index{optimization}
\index{optimization!weak constraint}
\index{optimization!minimize, \code{\#minimize}}
\index{optimization!maximize, \code{\#maximize}}

Optimization statements extend the basic question of
whether a set of atoms is an answer set to
whether it is an optimal answer set.
To support this reasoning mode, \gringo\ and \clingo\ adopt \dlv's weak constraints~\cite{bflnrp00a}.
The form of weak constraints is similar to integrity constraints (cf.~Section \ref{subsec:gringo:normal})
being associated with a term tuple:
\[
    \code{:{\raise.17ex\hbox{$\scriptstyle\sim$}}~$L_1$,$\dots$,$L_n$.~[$w$@$p$,$t_1$,$\dots$,$t_n$]}
\]
The priority `\code{@$p$}' is optional.
For simplicity, we first consider the non-prioritized case omitting `\code{@$p$}'.
Whenever the body of a weak constraint is satisfied,
it contributes its term tuple (as with aggregates, each tuple is included at most once) to a cost function.
This cost function accumulates the integer weights $w$ of all contributed tuples just like a \const{\#sum} aggregate does (cf.~Section~\ref{subsec:gringo:aggregate}).
The semantics of a program with weak constraints is intuitive:
an answer set is \emph{optimal}
if the obtained cost is minimal among all answer sets of the given program.
Whenever there are different priorities attached to tuples,
we obtain a (possibly zero) cost for each priority.
To determine whether an answer set is optimal,
we do not just compare two single costs
but lexicographically compare cost tuples whose elements are ordered by priority (greater is more important).
Note that a tuple is always associated with a priority;
if it is omitted, then the priority defaults to zero.
\index{meta-statement!optimization@\gobblecomma|see{optimization}}
\index{safety!weak constraint}
\index{safety!minimize, \code{\#minimize}}
\index{safety!maximize, \code{\#maximize}}
A weak constraint is safe if the variables in its term tuples are bound by the atoms in the body
and the safety requirements for the body itself are the same as for integrity constraints.

As an alternative way to express an optimization problem,
there are optimization statements.
A minimize statement of the form
\[
    \code{\#minimize~\{~$w_1$@$p_1$,$\boldsymbol{t}_1$:$\boldsymbol{L}_1$,$\dots$,$w_n$@$p_n$,$\boldsymbol{t}_n$:$\boldsymbol{L}_n$~\}.}
\]
represents the following $n$ weak constraints:
\[
    \code{:\Sim~$\boldsymbol{L}_1$.~[$w_1$@$p_1$,$\boldsymbol{t}_1$]}
    \quad \dots \quad
    \code{:\Sim~$\boldsymbol{L}_n$.~[$w_n$@$p_n$,$\boldsymbol{t}_n$]}
\]
%
Moreover, maximize statements can be viewed as minimize statements
with inverse weights.
Hence, a maximize statement of the form
\[
    \code{\#maximize~\{~$w_1$@$p_1$,$\boldsymbol{t}_1$:$\boldsymbol{L}_1$,$\dots$,$w_n$@$p_n$,$\boldsymbol{t}_n$:$\boldsymbol{L}_n$~\}.}
\]
represents the following $n$ weak constraints:
\[
    \code{:\Sim~$\boldsymbol{L}_1$.~[-$w_1$@$p_1$,$\boldsymbol{t}_1$]}
    \quad \dots \quad
    \code{:\Sim~$\boldsymbol{L}_n$.~[-$w_n$@$p_n$,$\boldsymbol{t}_n$]}
\]
As with weak constraints, the priorities `\code{@$p_i$}' are optional
and default to zero.

\begin{example}\label{ex:opt}
To illustrate optimization, we consider a hotel booking situation
where we want to choose one among five available hotels.
The hotels are identified via numbers assigned in descending order of stars.
Of course, the more stars a hotel has, the more it costs per night.
As ancillary information, we know that hotel~\const{4} is located
on a main street, which is why we expect its rooms to be noisy.
This knowledge is specified in Line~1--7 of the following program:
%
\lstinputlisting[xrightmargin=-35pt]{examples/opt.lp}
%
Line~8--9 contribute optimization statements in inverse order of significance,
according to which we want to choose the best hotel to book.
The most significant optimization statement in Line~10 states that
avoiding noise is our main priority.
The secondary optimization criterion in Line~9 consists of minimizing the cost per star.
Finally, the third optimization statement in Line~8 specifies
that we want to maximize the number of stars among hotels that are otherwise indistinguishable.
The optimization statements in Line~8--10 are instantiated as follows:%
\marginlabel{%
  The full ground program is obtained by invoking:\\
  \code{\mbox{~}clingo --text \attach{examples/opt.lp}{opt.lp}}\\
  or alternatively:\\
  \code{\mbox{~}gringo --text \attach{examples/opt.lp}{opt.lp}}}
%
\begin{lstlisting}[firstnumber=8,breakindent=0pt,escapechar=&]
:~ hotel(1). [-5@1,1]&\\&:~ hotel(2). [-4@1,2]&\\&:~ hotel(3). [-3@1,3]&\\&:~ hotel(4). [-3@1,4]&\\&:~ hotel(5). [-2@1,5]
:~ hotel(1). [34@2,1]&\\&:~ hotel(2). [35@2,2]&\\&:~ hotel(3). [30@2,3]&\\&:~ hotel(4). [25@2,4]&\\&:~ hotel(5). [30@2,5]
:~ noisy. [ 1@3 ]
\end{lstlisting}
If we now use \clasp\ or \clingo\ to compute an optimal answer set,%
\marginlabel{%
  To compute the unique optimal answer set, invoke:\\
  \code{\mbox{~}clingo \attach{examples/opt.lp}{opt.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/opt.lp}{opt.lp} | \textbackslash\\
        \mbox{~}clasp 0}}
we find that hotel~\const{4} is not eligible because it implies \pred{noisy}.
Thus, hotel~\const{3} and~\const{5} remain as optimal
with respect to the second most significant optimization statement in Line~9.
This tie is broken via the least significant optimization statement in Line~8
because hotel~\const{3} has one star more than hotel~\const{5}.
We thus decide to book hotel~\const{3} offering~\const{3} stars to cost~\const{90} per night.
\end{example}


\subsubsection{External Functions}\label{subsec:lang:extfun}
\index{external function}%
\index{term!external function@\gobblecomma|see{external function}}%
\index{lua}%
\index{python}%
Utilizing the scripting languages Lua or Python\footnote{\url{http://lua.org} and \url{http://python.org}},
\gringo's input language can be enriched by arbitrary functions.
We focus on functions that are evaluated during grounding here.
In Section~\ref{sec:multi},
we explain how to take complete control of the grounding and solving process using the scripting API.
We do not give an introduction to Lua or Python here (there are numerous tutorials on the web),
but give some examples showing the capabilities of this integration.
In the following, we show code snippets for both scripting languages.
Note that our precompiled binaries ship with Lua support and can be used to run the Lua examples.
To enable Python support, \gringo\ and \clingo\ have to be compiled from source (cf.\ Section~\ref{sec:install}).
A complete reference for the Python scripting API is available at: 
\footnote{The API of \clingo{} series~4 is described at \url{http://potassco.sourceforge.net/gringo.html}.}
\begin{center}
\url{http://potassco.org/clingo}
\end{center}
\begin{example}\label{ex:gcd}
The first example shows how to add a simple arithmetic function:
\\[-8pt] % is there a better way to do this?
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoLua]{examples/gcd-lua.lp}
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoPython]{examples/gcd-py.lp}
\end{minipage}\\
In Line~6, we add a function that calculates the greatest common divisor of two numbers.
Integers from a logic program are returned as objects of type \code{Symbol}%
\footnote{Strictly speaking there are no classes in Lua, the Userdata type together with a metatable is used to emulate classes.}
--- a variant type capturing ground terms.
The numeric value can be accessed using the \code{number} property in both Lua and Python.
To construct a numeric term, the \code{Number} constructor is used.
The \code{gcd} function can then be used in a logic program:%
\marginlabel{%
To inspect the unique answer set of the program, invoke:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/gcd.lp}{gcd.lp} \attach{examples/gcd-lua.lp}{gcd-lua.lp}}\\
or:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/gcd.lp}{gcd.lp} \attach{examples/gcd-py.lp}{gcd-py.lp}}\\
Calls to \clingo\ are similar.
}
%
\lstinputlisting{examples/gcd.lp}
%
The function is called in Line~3 and the result stored in predicate \code{gcd}/$3$.
Note that external function calls look like function terms but are preceded by `\code{@}'.
As with non-simple arithmetic terms
according to Remark~\ref{note:simple},
variable occurrences in arguments to external functions
do not count as positive in the sense of safety (cf.\ Page~\pageref{pg:safe}).
In Line~3, values for~\var{X} and~\var{Y}
are thus obtained from \code{\pred{p}(\var{X},\var{Y})}
in order to apply the \code{gcd} function to them.
\end{example}

\begin{example}
This example shows how to return multiple values from a function:
\\[-8pt] % is there a better way to do this?
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoLua]{examples/rng-lua.lp}
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoPython]{examples/rng-py.lp}
\end{minipage}\\
In Line~3, we add a function that emulates an interval.
Instead of just returning one number,
this function returns a table of numbers in Lua and yields number symbols in Python, respectively.
Actually, in Python any form of iterable over symbols can be used.
The \code{rng} function can then be used in a logic program:%
\marginlabel{%
To inspect the unique answer set of the program, invoke:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/rng.lp}{rng.lp} \attach{examples/rng-lua.lp}{rng-lua.lp}}\\
or:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/rng.lp}{rng.lp} \attach{examples/rng-py.lp}{rng-py.lp}}\\
Calls to \clingo\ are similar.
}
%
\lstinputlisting{examples/rng.lp}
%
The function is called in Line~3 and the result stored in predicate \code{rng}/$3$.
The values in the table or list returned from a call to \code{\@rng(X,Y)} are then successively inserted.
In fact, this function behaves exactly like the interval~\code{X..Y}.

An interesting use case for returning multiple values is to pull whole
instances from external sources, like for example a database or some text file not already in fact format.
\end{example}

As we have seen in the previous example,
the \code{number} property is used to get the numeric representation of a term from objects of type \code{Symbol}.
In fact, all terms are captured by the \code{Symbol} class.
Similarly to numeric terms, the \code{string} property is used to get the representation of quoted strings.
For constants and functions,
there is the property \code{name} to access the string representation of the constant or the name of the function term.
Furthermore,
the arguments of a function term can be accessed using the \code{arguments} property.
Note that constants as well as tuples are considered as special cases of function terms.
The former have an empty argument list and the latter an empty name.
Finally, the terms \code{\#sup} and \code{\#inf} are mapped to the constants \code{Sup} and \code{Inf}.
Both are subclasses of class \code{Symbol}, too.
Unlike other terms both are captured by unique objects.

To construct terms from within the scripting language,
the global functions \code{Function(name, arguments)}, \code{Number(number)}, and \code{String(string)} are used.
All of them (and their advanced usage) are fully documented in the Python API documentation.

\begin{example}
This example shows how to inspect and create terms:
%
\\[-8pt] % is there a better way to do this?
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoLua]{examples/term-lua.lp}
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoPython]{examples/term-py.lp}
\end{minipage}\\
In Line~6, we add a function~\code{g}
that  takes a constant and a tuple as arguments
and returns a function term with the name of the constant and the tuple as arguments.
The \code{g} function can then be used in a logic program:%
\marginlabel{%
To inspect the unique answer set of the program, invoke:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/term.lp}{term.lp} \attach{examples/term-lua.lp}{term-lua.lp}}\\
or:\\
\code{%
\mbox{~}gringo --text \textbackslash\newline\mbox{~}\attach{examples/term.lp}{term.lp} \attach{examples/term-py.lp}{term-py.lp}}\\
Calls to \clingo\ are similar.
}
%
\lstinputlisting{examples/term.lp}
%
The function is called in Line~3 and the result stored in predicate \code{g}/$3$.
Using this scheme,
new terms
that cannot be constructed by means of plain ASP
can be created during grounding.
Another interesting application might be string concatenation.
\end{example}

\begin{note}~
\begin{enumerate}
\item The grounder assumes that all external functions are deterministic.
That is, when a function is called multiple times with the same arguments during grounding,
then it should return the same values.
Adding functions that do not comply with this assumption can lead to undesired results.
\item If an error occurs during the evaluation of an external function,
a warning is printed and the current instance of a rule or condition is dropped.
For example, this happens when the~\code{gcd} function from Example~\ref{ex:gcd} is applied to non-integer arguments.
\end{enumerate}
\end{note}

\subsubsection{Meta-Statements}\label{subsec:gringo:meta}
\index{meta-statement}

After considering the language of logic programs,
we now introduce features going beyond the contents of a program.

\paragraph{Comments}
\index{meta-statement!comment}
To annotate the source code of a logic program,
a logic program file may include comments.
A comment until the end of a line is initiated by symbol `\code{\%}',
and a comment within one or over multiple lines is enclosed
in `\code{\%*}' and `\code{*\%}'.
As an abstract example, consider:
%
\begin{lstlisting}[numbers=none,escapechar=@]
tos(jim).    %* enclosed comment *%  tos(spock).
tos(bones).  % comment till end of line
tos(scotty). tos(chekov).
%*
comment over multiple lines
*%
tos(uhura).  tos(sulu).
\end{lstlisting}

\paragraph{Show Statements}
\index{meta-statement!show, \code{\#show}}%
Usually, only a subset of the atoms belonging
to an answer set characterizes a solution.
In order to suppress the atoms of ``irrelevant'' predicates from the output
or even to show arbitrary terms,
the \code{\#show} directive can be used.
There are three different kinds of such statements:
%
\begin{align*}
   \textbf{Show atoms:}   & \quad \code{\#show~$p$/$n$.} \\
   \textbf{Show terms:}   & \quad \code{\#show~$t$:$L_1$,$\dots$,$L_n$.} \\
   \textbf{Show nothing:} & \quad \code{\#show.}
\end{align*}
%
The first~\code{\#show} statement is the most commonly used form.
Whenever there is at least one statement of this form, all atoms are hidden,
except for those over predicates~$p/n$ given by the respective~\code{\#show} statements.
The second form can be used to show arbitrary terms.
The term~$t$ is part of the output if the literals in the condition after the~`\code{:}' hold.
Unlike the previous form,
this statement does not automatically hide all atoms.
To hide all atoms in this case and only show selected terms,
the last statement (mnemonic: show nothing) can be added to suppress all atoms in the output.

\begin{example}
This example illustrates the common use case to selectively show atoms:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo \attach{examples/showa.lp}{showa.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/showa.lp}{showa.lp} | \textbackslash \\\mbox{~}clasp 0}\\
}
\lstinputlisting{examples/showa.lp}
Only atoms over \pred{q}/$1$ and \pred{a} appear in the output here.
\end{example}

\begin{example}
This example illustrates how to show terms:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo \attach{examples/showt.lp}{showt.lp} 0}\\
  or alternatively:\\
  \code{\mbox{~}gringo \attach{examples/showt.lp}{showt.lp} | \textbackslash \\\mbox{~}clasp 0}\\
}
%
\lstinputlisting{examples/showt.lp}
%
When running this example,
the same output as in the previous example is produced.
This feature is especially handy when applying meta-programming techniques (cf.~Section~\ref{sec:meta})
where the signatures of the reified atoms are not fixed and \code{holds($\cdot$)} atoms would just clutter the output.
\end{example}

\begin{note}
The second form of \code{\#show} statements to show terms may contain variables.
Regarding safety (cf.\ Page~\pageref{pg:safe}), it behaves similar to a rule,
where the term~$t$ takes the role of the head
and the condition after the colon the role of the body.
\index{safety!show, \code{\#show}}
\end{note}

\paragraph{Const Statements}\label{subset:gringo:meta:const}
\index{meta-statement!const, \code{\#const}}%
Constants appearing in a logic program may actually be placeholders for
concrete values provided by a user.
An example of this is given in Section~\ref{subsec:ex:color}.
Via the \code{\#const} directive,
one may define a default value to be inserted for a constant.
Such a default value can still be overridden via command line option
\code{--const} (cf.\ Section~\ref{subsec:opt:gringo}).
Syntactically, \code{\#const} must be followed by an assignment having
a constant on the left-hand side and a term without variables, pools, and intervals on the right-hand side.

\begin{example}
This example is about using the grounder as a simple calculator:
%
\lstinputlisting{examples/const.lp}
%
Try running this example using the following calls:
%
\begin{lstlisting}[numbers=none,escapeinside={\$}{\$}]
gringo --text $\attach{examples/const.lp}{const.lp}$
gringo --text $\attach{examples/const.lp}{const.lp}$ -c x=6   -c z=6
gringo --text $\attach{examples/const.lp}{const.lp}$ -c x=6+6 -c y=6
gringo --text $\attach{examples/const.lp}{const.lp}$ -c x="6+6*6"
\end{lstlisting}
%
Note that quotes have to be added to prevent the shell from expanding the `\code{*}' in the last call
or from interpreting parentheses in functions.
\end{example}

\paragraph{External Statements}
\index{meta-statement!external, \code{\#external}}%
External statements are used to declare atoms
that should not be subject to certain simplifications.
Namely,
atoms marked external are not removed from the bodies of rules, conditions, etc.,
even if they do not appear in the head of any rule.
The main use case is to implement extensions to plain ASP solving,
like multi-shot solving detailed in Section~\ref{sec:multi}.
An \code{\#external} statement has the following form:
%
\[\code{\#external~$A$:$L_1$,$\dots$,$L_n$.}\]
%
Here, $A$ is an atom over some predicate and
the part following the~`\code{:}' is a condition.
The condition is instantiated to obtain a set of external atoms.
Note that the condition is discarded after grounding,
hence, it is a good idea to use only domain predicates or built-ins after the colon.%
\footnote{Non-domain predicates are supported, too,
because in some situations it might be inconvenient to specify domain predicates.}

\begin{example}
Consider the following example:%
\marginlabel{%
To inspect the instantiation of externals, invoke:\\
\code{%
\mbox{~}clingo --text \attach{examples/ext.lp}{ext.lp}}\\
or alternatively:\\
\code{%
\mbox{~}gringo --text \attach{examples/ext.lp}{ext.lp}}
}
%
\lstinputlisting{examples/ext.lp}
%
The \code{\#external} statement in Line~2 gives rise to three external atoms,
which appear accordingly in the text output.
With these three atoms,
the rule in Line~4 yields three ground instantiations,
where atoms~\code{q(2)} and~\code{q(3)} appear in the body.
Because we have the fact \code{q(1)} in Line~3,
the atom \code{q(1)} is still subject to simplification
and removed from the body of the respective instantiation of the rule in Line~4.
The idea here is that no matter how \code{q(1)} is supplied externally,
there can never be an answer set that does not contain \code{q(1)}.
\end{example}

\begin{note}
External statements that contain variables
have very similar requirements regarding safety as rules (cf.\ Page~\pageref{pg:safe}).
The atom~$A$ takes the role of the head
and the condition after the colon the role of the body.
\index{safety!external, \code{\#external}}
\end{note}
\paragraph{Program Parts}
\index{meta-statement!program part, \code{\#program}}
A logic program can be organized in multiple program parts.
To begin a new program part, we write a statement
%
\[\code{\#program~$p$($s_1$,\dots,$s_n$).}\]
%
where $p$ is the program part name and the parameters $s_i$ are constants.
If $n$ is zero, then the parentheses can be omitted.
All rules, external statements, and show statements for terms up to the next \code{\#program} statement or the end of the file belong to the program part $p/n$.
Rules that are not subject to any such directive are included in the \code{base}/$0$ part.

The default behavior of \gringo\ is to ground (and solve in the case of \clingo)
the \code{base}/$0$ part.
Using the scripting API (cf.\ Section~\ref{sec:multi}),
we can ground other parts than \code{base}/$0$, too.
Occurrences of constants that are parameters of a part are replaced with ground terms when instantiating the program part.

\begin{example}
The following example shows how to instantiate program parts:
\lstinputlisting[language=GringoLua]{examples/part.lp}
The above program is organized in two parts, \code{base}/$0$ and \code{a}/$2$.
Note that the fact in the first line is implicitly in the \code{base}/$0$ part.
Solving the program as is results in answer set $\{\code{a}, \code{c}\}$,
because the \code{base}/$0$ part is instantiated by default.
Scripts to instantiate the \code{a}/$2$ part as well are as follows:%
\marginlabel{%
To inspect the instantiation of program parts, invoke:\\
\code{%
\mbox{~}gringo --text \textbackslash\\
\mbox{~}\attach{examples/part.lp}{part.lp} \attach{examples/part-lua.lp}{part-lua.lp}}\\
or:\\
\code{%
\mbox{~}gringo --text \textbackslash\\
\mbox{~}\attach{examples/part.lp}{part.lp} \attach{examples/part-py.lp}{part-py.lp}}\\
Calls to \clingo\ are similar.
}
%
\\[-8pt] % is there a better way to do this?
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoLua]{examples/part-lua.lp}
\end{minipage}
\begin{minipage}[t]{0.5\textwidth}
\lstinputlisting[language=GringoPython]{examples/part-py.lp}
\end{minipage}\\
%
In Line~9,
the script grounds the \code{base}/$0$ part (Line~7)
as well as the \code{a}/$2$ part with parameters \code{1} and \code{3} (Line~8).
The call in Line 10 is essential to solve the program with \clingo,
and even in \gringo\ some post-processing happens, e.g.,
printing the symbol table of the \smodels\ format~\cite{lparseManual}.
\end{example}

\begin{note}
Program parts are mainly interesting for incremental grounding and solving of logic programs detailed in Section~\ref{sec:multi}.
For single-shot solving, program parts are not needed.
The feature is merely listed for completeness here.
\end{note}

\paragraph{Include Statements}
Include statements allow for including files from within another file.
They have the form
%
\[\code{\#include~"{\itshape file}".}\]
%
where \codeit{file} is a path to another encoding file.
When including a file it is first looked up relative to the current working directory.
If it is not found there, then it is looked up relative to the file it was included from.
Note that program part declarations do not affect the inclusion of files,
that is, including a file is equivalent to passing it on the command line.

\begin{example}
Suppose that we have a file
\attach{examples/include.lp}{include.lp} with the following statement:%
\marginlabel{%
To inspect the instantiation, invoke:\\
\code{%
\mbox{~}clingo --text \textbackslash\\
\mbox{~}\attach{examples/include.lp}{include.lp}}\\
or alternatively:\\
\code{%
\mbox{~}gringo --text \textbackslash\\
\mbox{~}\attach{examples/include.lp}{include.lp}}
}
%
\lstinputlisting{examples/include.lp}
%
We can simply pass the file on the command line
to include file \attach{examples/bird.lp}{bird.lp} from Example~\ref{ex:flies}.
%
Since files are included from the current working directory
as well as relative to the file with the include statement,
an invocation like `\code{clingo examples/include.lp}'
works with either of the following directory layouts:
\begin{lstlisting}[numbers=none]
.
|-- bird.lp
\-- examples
    \-- include.lp

.
\-- examples
    |-- bird.lp
    \-- include.lp
\end{lstlisting}
%
\end{example}

\subsection{Input Language of \clasp}\label{subsec:lang:clasp}

Solver \clasp~\cite{gekanesc07b} (or `\clingo\code{ --mode=clasp}') accepts logic programs in 
\aspif{} format~\cite{kascwa17a} and \smodels\ format~\cite{lparseManual} (for backward compatibility),
SAT and MaxSAT instances in DIMACS-cnf\footnote{\url{http://www.satcompetition.org/2009/format-benchmarks2009.html}}
and DIMACS-wcnf\footnote{\url{http://www.maxsat.udl.cat/12/requirements/index.html}} format,
and PB problems in OPB/WBO\footnote{\url{http://www.cril.univ-artois.fr/PB12/format.pdf}} format.

For ASP solving,
\clasp\ is typically invoked in a pipe reading
a logic program output by \gringo\ (or \clingo):
%
\begin{lstlisting}[numbers=none]
gringo [ options | files ] | clasp [ options | number ]
clingo [ options | files | number ]
\end{lstlisting}
%
Note that \code{number} may be provided to specify a maximum number of answer sets
to be computed, where~\code{0} makes \clasp\ compute all answer sets.
This maximum number can also be set via
option \code{--models} or its abbreviation \code{-n}
(cf.\ Section~\ref{subsec:opt:clasp}).
By default, \clasp\ computes one (optimal) answer set (if it exists).

To solve a problem in one of the supported formats stored in a \code{file},
an invocation of \clasp\ looks as follows:%
\begin{lstlisting}[numbers=none]
clasp [ options | number ] file
clingo --mode=clasp [ options | number ] file
\end{lstlisting}
In general, \clasp\ autodetects the input format. However,
option \code{--opt-sat} is necessary to distinguish a
MaxSAT instance in DIMACS-wcnf format from a plain SAT instance
in  DIMACS-cnf format.

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "guide"
%%% End: