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

This section provides an overview of the input languages of
grounder \gringo, combined grounder and solver \clingo,
incremental grounder and solver \iclingo, and of solver \clasp.
The joint input language of \gringo\ and \clingo\ is detailed in
Section~\ref{subsec:lang:gringo}.
It is extended by \iclingo\ with a few directives described in Section~\ref{subsec:lang:iclingo}.
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 translating
logic programs provided by users into equivalent ground programs.
The output of \gringo\ can be piped into solver \clasp~\cite{gekanesc07b},
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 passed via the command line
in an invocation of either \gringo\ or \clingo.
We below provide a description of constructs belonging to the input language of \gringo\ and \clingo.


\subsubsection{Normal Programs and Integrity Constraints}\label{subsec:gringo:normal}
\index{Terms}
\index{Terms!Constants}
\index{Terms!Variables}
\index{Terms!Variables!Anonymous}
\index{Terms!Functions}
\index{Terms!\code{\#supremum}}
\index{Terms!\code{\#infimum}}

\begin{figure}
\begin{rail}
	constant    : ('\_'*) '[a-z]' ('[A-Za-z0-9]'*);
	variable    : ('\_'*) '[A-Z]' ('[A-Za-z0-9]'*);
	simpleterm  : ('integer' | constant | variable | '\_' | '\#supremum' | '\#infimum');
	function    : constant '(' simpleterm (',' simpleterm*) ')';
	term        : simpleterm | function;
\end{rail}
\caption{Terms\label{fig:terms}}
\end{figure}

Every logic program is constructed from terms.
An overview of \gringo{} terms is depicted in Figure \ref{fig:terms}.
The most basic terms are integers, constants, and variables.
Furthermore, there are some special variables and constants.
An anonymous variable denoted by `\_' is simialar to a normal variable 
but each occurrence is treated like a different variable 
(intuitively a new unique variable name is substituted).
Additionally, there are the two special constants `\#supremum' and `\#infimum'
representing the largest and the smallest possible values, respectively,
which behave essentially like constants.
Finally, there are function symbols which are composed of other terms.
A term that does not contain any (anonymous) variables is called a ground term.
More complex terms involving arithmetics and other constructs
are introduced later on.

\index{Statements!Rules}
\index{Statements!Facts}
\index{Statements!Integrity Constraints}
Rules are defined as follows:\\

\begin{tabular}{rl@{}l}\label{eq:normal:rule}
\textbf{Rule:} & $A_0$& $\code{:-}~L_1\code{,}\dots\code{,}L_n$\code{.}
\\
\textbf{Fact:} & $A_0$&\code{.}
\\
\textbf{Integrity Constraint:} & & $\code{:-}~L_1\code{,}\dots\code{,}L_n$\code{.}
\end{tabular}
\\

\noindent
The head~$A_0$ of a fact or a rule is an \emph{atom} of the same form
as a function symbol or constant.
Any $L_j$ is a \emph{literal} of the form $A$ or $\code{not}~A$
for an atom~$A$ where the connective \code{not} corresponds to default negation\index{Literals!Default Negation}.
The set of literals $\{L_1,\dots,L_n\}$ is called the body of the rule.
Facts have an empty body.
Throughout this section we further extend the predicates that can be used 
in a rule including comparison predicates (Section \ref{subsec:gringo:comp}) and aggregates (Section \ref{subsec:gringo:aggregate}).
Furthermore, \gringo{} expects rules to be safe, i.e., \index{Safe Program}
all variables that appear in a rule have to appear in some positive literal (a literal not preceded by \code{not}) in the body.
If a variable appears positively in some predicate, then we say that this predicate binds the variable.

Intuitively, the head of a rule has to be true whenever all its body literals are true.
In ASP every atom needs some derivation, i.e., 
an atom cannot be true if there is no rule deriving it.
This implies that only atoms appearing in some head can appear in answer sets.
Furthermore, derivations%
\footnote{There are extensions like disjunctions 
that go beyond simple derivability and also require minimality w.r.t. a reduct. 
We do not cover the semantics of such constraints in this guide.}%
have to be acyclic,
a feature that is important to model reachability.
As a simple example, consider the program \code{a :- b. b :- a.}
The only answer set to this program is the empty set.
Adding either \code{a.} or \code{b.} to the program results in the answer set $\{a,b\}$.
Finally, note that default negation is ignored when checking for acyclic derivations 
(we do not need a reason for an atom being false).
Default negation can be used to express choices, e.g., the program \code{a :- not b. b :- not a.} 
has the two answer sets $\{a\}$ and $\{b\}$.
But in practice it is never needed to express choices this way.
For example in the introductory example in Section~\ref{sec:quickstart} we used a cardinality 
constraint, which provides a much more readable way to introduce choices.
%\com{This paragraph contains a lot of information. Could someone help me making it more readable?}

A fact has an empty body and thus its associated head predicate is always true 
and appears in all answer sets.
On the other hand, integrity constraints eliminate answer set candidates.
They are merely tests that discard unwanted answer sets.
That is, there are no answer sets that satisfy all literals an integrity constraint.
Elaborate examples on the usage of facts, rules, and integrity constraints
are provided in Section~\ref{sec:examples}.

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

In logic programs, connective \code{not} expresses default negation,
that is, a literal $\code{not}~A$ is assumed to hold unless~$A$ is derived.
In contrast, the classical (or strong) negation of some proposition
holds if the complement of the proposition is derived~\cite{gellif91a}.
Classical negation, indicated by symbol ``\code{-},'' is permitted in front of atoms.
That is, if~$A$ is an atom, then~$\code{-}A$ is the complement of~$A$.
Semantically, $\code{-}A$ is simply a new atom,
with the additional condition that~$A$ and~$\code{-}A$ must not jointly hold.
Observe that classical negation is merely a syntactic feature that can be
implemented via integrity constraints whose effect is to eliminate
any answer set candidate containing complementary atoms.

\begin{example}\label{ex:flies:neg}
Consider a logic program comprising the following facts:
%
\lstinputlisting[nolol]{examples/bird.lp}
\lstinputlisting[firstnumber=3]{examples/flycn.lp}
%
Logically, classical negation is reflected by
(implicit) integrity constraints as follows:%
\marginlabel{By invoking\\
  \code{\mbox{~}gringo -t \textbackslash\\
        \mbox{~}\attach{examples/bird.lp}{bird.lp}~\attach{examples/flycn.lp}{flycn.lp}}
the reader can observe that \gringo\ indeed produces the integrity constraint
in Line~7.}
%
\begin{lstlisting}[firstnumber=6]
:- flies(tux),    -flies(tux).
:- flies(tweety), -flies(tweety).
\end{lstlisting}
The program has two answer sets.
One contains \code{flies(tweety)} and the other contains \code{-flies(tweety)}.
Let us now add a new fact to the program:
\begin{lstlisting}[firstnumber=8]
flies(tux).
\end{lstlisting}
There no longer is any answer set for our new program using classical negation.
In fact, answer set candidates that contain both
\code{\pred{flies}(\const{tux})} and
\code{\pred{-flies}(\const{tux})} violate the integrity constraint in Line~6.
\eexample
\end{example}


\subsubsection{Disjunction}\label{subsec:gringo:disjunction}
\index{Aggregates!Disjunction}
Disjunctive logic programs permit connective~``\code{|}'' between atoms in rule heads.
A disjunction is true if at least one of its atoms is true.
Additionally, logic programs have to satisfy a minimality criterion, 
which we do not detail in this guide.
The simple program \code{a | b.} has the two answer sets $\{a\}$ and $\{b\}$ but
does not admit the answer set ${a,b}$ because it is no minimal model.

In general, the use of disjunction however increases
computational complexity~\cite{eitgot95a}.
This is why \clingo%
\footnote{Run as a monolithic system performing both grounding and solving.}
and solvers like 
\assat~\cite{linzha04a},
\clasp~\cite{gekanesc07b},
\nomorepp~\cite{angelinesc05c},
\smodels~\cite{siniso02a}, and
\smodelscc~\cite{warsch04a}
do not work on disjunctive programs.
Rather,
\claspD~\cite{drgegrkakoossc08a},
\cmodels~\cite{gilima06a,lierler05a}, or
\gnt~\cite{janisesiyo06a}
need to be used for solving a disjunctive program.%
\footnote{System \dlv~\cite{dlv03a} also deals with disjunctive programs,
  but it uses a different syntax than presented here.}
We thus suggest to use ``choice constructs'' (cf.\ Section~\ref{subsec:gringo:aggregate})
instead of disjunction, unless the latter is required for complexity reasons
(see~\cite{eitpol06a} for an implementation methodology in disjunctive ASP).


\subsubsection{Built-In Arithmetic Functions}\label{subsec:gringo:arith}
\index{Literals!Arithmetic Functions}
\index{Literals!Arithmetic Functions!Addition, \code{+}}
\index{Literals!Arithmetic Functions!Subtraction, \code{-}}
\index{Literals!Arithmetic Functions!Multiplication, \code{*}}
\index{Literals!Arithmetic Functions!Division, \code{/}}
\index{Literals!Arithmetic Functions!Modulo, \code{\%}}
\index{Literals!Arithmetic Functions!Exponentation, \code{**}}
\index{Literals!Arithmetic Functions!Absolute Value, \code{\#abs}}
\index{Literals!Arithmetic Functions!Bitwise AND, \code{\&}}
\index{Literals!Arithmetic Functions!Bitwise OR, \code{?}}
\index{Literals!Arithmetic Functions!Bitwise XOR, \code{\^}}
\index{Literals!Arithmetic Functions!Bitwise Complement, \code{\textasciitilde}}

\gringo\ and \clingo\ support a number 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{/} or \code{\#div} (integer division),
\code{\textbackslash} or \code{\#mod} (modulo function),
\code{**} or \code{\#pow} (exponentation),
\code{|$\cdot$|} or \code{\#abs} (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 logic program:%
\marginlabel{%
  The unique answer set of the program,
  obtained after evaluating all arithmetic functions,
  can be inspected by invoking:\\
  \code{\mbox{~}gringo -t \attach{examples/arithf.lp}{arithf.lp}}}
%
\lstinputlisting{examples/arithf.lp}
%
Note that 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 also be dropped,
while spaces after tokens \code{\#div} and \code{\#mod} are mandatory.
Furthermore, the argument of function \code{\#abs}, \code{\#div}, and \code{\#mod} must be enclosed in parentheses.
The four bitwise functions apply to signed integers,
using the two's complement of a negative integer.
\eexample
\end{example}

\begin{Note}
that it is important that variables
in the scope of an arithmetic function are not bound by a corresponding atom.
For instance, the rule \code{p(X) :- p(X+1).} is not safe but \code{p(X-1) :- p(X).} is.
Although, the latter might produce an infinite grounding 
and \gringo{} not necessarily halts when given such an input.
\end{Note}

\subsubsection{Built-In Comparison Predicates}\label{subsec:gringo:comp}
\index{Literals!Comparison Predicates}
\index{Literals!Comparison Predicates!Equality, \code{==}}
\index{Literals!Comparison Predicates!Inequality, \code{!=}}
\index{Literals!Comparison Predicates!Less, \code{<}}
\index{Literals!Comparison Predicates!Less or Equal, \code{<=}}
\index{Literals!Comparison Predicates!Greater,\code{>}}
\index{Literals!Comparison Predicates!Greater or Equal\code{>=}}

The following built-in predicates permit term comparisons
within the bodies of rules:
\code{==} (equal),
\code{!=} (not equal),
\code{<} (less than),
\code{<=} (less than or equal),
\code{>} (greater than),
\code{>=} (greater than or equal).

\begin{example}\label{ex:arith:pred}
The usage of comparison predicates is illustrated by the logic program:%
\marginlabel{%
  The unique answer set of the program is obtained via call:\\
  \code{\mbox{~}gringo -t \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 predicates, so that the latter actually compare integers.

All comparison predicates can also be used with arbitrary ground terms,
as in the next program:%
\marginlabel{%
  As above, invoking:\\
  \code{\mbox{~}gringo -t \attach{examples/symbc.lp}{symbc.lp}}
  yields the unique answer set of the program in terms of facts.}
%
\lstinputlisting{examples/symbc.lp}
%
Integers are compared in the usual way and constants are ordered lexicographically.
Function symbols are compared first using their arity.
If the arity differs, then the name of the function symbol is compared lexicographically.
If again the name differs, then arguments are compared component wise.
Finally, integers are always smaller than constants and constants are always smaller than function symbols.
\eexample
%\comment{add \#sup and \#inf?}
\end{example}

\begin{Note}
that a built-in comparison predicate cannot bind variables, i.e.,
when checking whether a rule is safe, 
comparison predicates are not considered to be positive.
\end{Note}


\subsubsection{Assignments}\label{subsec:gringo:assign}
\index{Literals!Assignments}
\index{Literals!Assignments!Term Unification, \code{:=}}
\index{Literals!Assignments!Variable Assignment, \code{=}}

The built-in predicates~\code{:=} and ~\code{=} can be used in the body of a rule
to unify a term on their right-hand side 
to a (non-ground) term or variable on its left-hand side, respectively.

\begin{example}\label{ex:assign}
The next program demonstrates how terms can be assigned to variables:%
\marginlabel{%
  The unique answer set of the program is obtained via call:\\
  \code{\mbox{~}gringo -t \attach{examples/assign.lp}{assign.lp}}}%
%
\lstinputlisting{examples/assign.lp}
%
Line~3 contains four assignments, where the right-hand sides directly or indirectly
depend on~\var{X} and~\var{Y}.
These two variables are bound in Line~5 via atoms of predicate \pred{num}/$1$.
Also observe the different usage and role of built-in comparison predicate~\code{==}.
\eexample
\end{example}

\begin{example}\label{ex:unify}
The second program demonstrates the usage of \code{:=},
which allows for terms on the left hand side:
\marginlabel{%
  The unique answer set of the program is obtained via call:\\
  \code{\mbox{~}gringo -t \attach{examples/unify.lp}{unify.lp}}}%
%
\lstinputlisting{examples/unify.lp}
%
Here the term \code{f(a,X,X+1)} is unified with every function symbol provided by \code{sym}/$1$.
Note the usage of \code{X+1} in the term.
\gringo{} does not try to unify any term containing arithmetic 
but in this example \code{X} occurs also directly as second argument of the argument
and can thus be unified with.
The term $X+1$ is merely a test that is deferred and checked later.
For example, the fourth line is equivalent to:
\begin{lstlisting}[firstnumber=6]
unifyf(X) :- f(a,X,Y) := F, sym(F), Y == X + 1.
\end{lstlisting}%
\eexample
\end{example}

\begin{Note}
that assignments to some extent can bind variables.
Of course cyclic assignments cannot bind variables.
For example the rule \code{p(X) :- X = Y, Y = X.} is rejected by \gringo{}.
Either \code{X} or \code{Y} has to be provided by some positive predicate in this case.
Additionally, unification is restricted to ground terms on the right hand side of the assignment, 
that is, all variables on the right hand side have to be bound by some other predicate.
\end{Note}

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

In Line~1 of Example~\ref{ex:assign},
there are five facts~\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$,
where~$i$ and~$j$ are integers.
Such an interval represents each integer~$k$ such that $i\leq k\leq j$,
and intervals are expanded during grounding.

\begin{example}\label{ex:int}
The next program makes use of integer intervals:
%
\lstinputlisting{examples/int.lp}
%
The facts in Line~1 and~2 are expanded as follows:
%
\begin{lstlisting}[numbers=none]
num(1).    num(2).   num(3).   num(4).   num(5).
top5(5).  top5(6).  top5(7).  top5(8).  top5(9).
\end{lstlisting}
%
By instantiating~\var{X} to~\const{9},
the rule in Line~4 becomes:
%
\begin{lstlisting}[numbers=none]
top5num(1..5,5..9) :- num(5..9), top5(1..5), top(9).
\end{lstlisting}
%
It is expanded to the cross product
$(\code{\const{1}..\const{5}})\times
 (\code{\const{5}..\const{9}})\times
 (\code{\const{5}..\const{9}})\times
 (\code{\const{1}..\const{5}})$
of intervals:
%
\begin{lstlisting}[numbers=none,escapechar=@]
top5num(1,5) :- num(5), top5(1), top(9).
top5num(2,5) :- num(5), top5(1), top(9).
        @\rlap{\vdots}@
top5num(5,5) :- num(5), top5(1), top(9).
top5num(1,6) :- num(5), top5(1), top(9).
top5num(2,6) :- num(5), top5(1), top(9).
        @\rlap{\vdots}@  @\rlap{\vdots}@
top5num(5,9) :- num(5), top5(1), top(9).
top5num(1,5) :- num(6), top5(1), top(9).
top5num(2,5) :- num(6), top5(1), top(9).
        @\rlap{\vdots}@  @\rlap{\vdots}@          @\rlap{\vdots}@
top5num(5,9) :- num(9), top5(1), top(9).
top5num(1,5) :- num(5), top5(2), top(9).
top5num(2,5) :- num(5), top5(2), top(9).
        @\rlap{\vdots}@  @\rlap{\vdots}@          @\rlap{\vdots}@         @\rlap{\vdots}@
top5num(5,9) :- num(9), top5(4), top(9).
top5num(1,5) :- num(5), top5(5), top(9).
top5num(2,5) :- num(5), top5(5), top(9).
        @\rlap{\vdots}@  @\rlap{\vdots}@
top5num(5,9) :- num(5), top5(5), top(9).
top5num(1,5) :- num(6), top5(5), top(9).
top5num(2,5) :- num(6), top5(5), top(9).
        @\rlap{\vdots}@  @\rlap{\vdots}@          @\rlap{\vdots}@
top5num(5,9) :- num(9), top5(5), top(9).
\end{lstlisting}
%
Note that only the rules with
\code{\pred{num}(\const{5})} and
\code{\pred{top5}(\const{5})}
\marginlabel{%
  Again the unique answer set is obtained via call:\\
  \code{\mbox{~}gringo -t \attach{examples/int.lp}{int.lp}}}
%
in the body actually contribute to the unique answer set
of the above program by deriving all atoms \code{\pred{top5num}($m$,$n$)}
for $\const{1}\leq m\leq\const{5}$ and $\const{5}\leq n\leq\const{9}$.
\eexample
\end{example}

\begin{Note}
that as with built-in arithmetic functions,
an integer interval mentioning some variable (like~\var{X} in Line~4 of Example~\ref{ex:int})
cannot be used to bind the variable.
\end{Note}

\subsubsection{Conditions}\label{subsec:gringo:condition}
\index{Aggregates!Conditions}

Conditions allow for instantiating variables to
collections of terms within a single rule.
This is particularly useful for encoding conjunctions or disjunctions over
arbitrarily many ground atoms as well as for the compact representation of aggregates
(cf.\ Section~\ref{subsec:gringo:aggregate}).
The symbol~``\code{:}'' is used to formulate conditions.

\begin{example}\label{ex:cond}
The following program uses conditions in a rule body and in a rule head:
%
\lstinputlisting{examples/cond.lp}
%
We are particularly interested in the rules in Line~5 and~6,
instantiated as follows:%
%
\begin{lstlisting}[firstnumber=5]
meet :- available(jane), available(john).
on(mon) | on(tue) | on(wed) | on(thu) | on(fri) :- meet.
\end{lstlisting}
%
The conjunction in Line~5 is obtained by replacing~\var{X} in
\marginlabel{%
  The reader can reproduce these ground rules by invoking:\\
  \code{\mbox{~}gringo -t \attach{examples/cond.lp}{cond.lp}}}
\code{\pred{available}(\var{X})} with all ground terms~$t$ such that
\code{\pred{person}($t$)} holds, namely, $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})} where~\var{X} is substituted by some term~$t$
such that
\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.

Composite conditions can also be constructed via~``\code{:},''
as in the additional rules:
%
\lstinputlisting[firstnumber=7]{examples/twocond.lp}
%
Observe that we may use the same atom, viz., \code{\pred{day}(\var{X})},
both on the left-hand and on the right-hand side of~``\code{:}.''
Furthermore, negative literals like \code{not \pred{weekend}(\var{X})}
can occur on both sides of a condition.
Note that literals on the right-hand side of a condition are connected conjunctively, that is,
all of them must hold for ground instances of an atom in front
of the condition.
Thus, the instantiated rule in Line~8 looks as follows:
%
\begin{lstlisting}[firstnumber=8]
weekdays :- day(mon), day(tue), day(wed), day(thu), day(fri).
\end{lstlisting}
%
The atoms in the body of this rule follow from facts, so that
the rule can be simplified to a fact \code{\pred{weekdays}.}
(as done by \gringo).
\eexample
\end{example}

\begin{Note}
that there are three important issues about the correct usage of conditions:
\begin{enumerate}
\item All predicates of atoms on the right-hand side of a condition
must be either domain predicates,%\comment{refer to appendix?}
i.e., predicates that can be completely evaluated during grounding,
or built-in, which is due to the fact that conditions are evaluated during grounding.
\item Any variable occurring within a condition is considered as \emph{local},
that is, a condition cannot be used to bind variables outside the condition.
In turn, variables outside conditions are \emph{global}, and each variable
within an atom in front of a condition must occur on the right-hand side or
be global.
\item Global variables take priority over local ones, that is,
they are instantiated first.
As a consequence, a local variable that also occurs globally is substituted by a term
before the ground instances of a condition are determined.
Hence, the names of local variables must be chosen with care,
making sure that they do not accidentally match the names of global variables.
\end{enumerate}
\end{Note}

\subsubsection{Pooling}\label{subsec:gringo:pool}
\index{Terms!Pooling}

Symbol~``\code{;}'' allows for pooling alternative terms to be used as
argument within an atom, thus, specifying rules more compactly.
An atom written in the form \code{\pred{p}($\dots$,X;Y,$\dots$)}
abbreviates two options:
\code{\pred{p}($\dots$,X,$\dots$)} and \code{\pred{p}($\dots$,Y,$\dots$)}.
Pooled arguments in any term of a rule body 
(or on the right-hand side of a condition) are expanded to a conjunction
of the options within the same body (or within the same condition),
while they are expanded to multiple rules 
(or multiple literals connected via~``\code{,}'')
when occurring in the head (or in front of a condition).

\begin{example}\label{ex:pool}
The following logic program makes use of pooling:
%
\lstinputlisting{examples/pool.lp}
%
Let us consider instantiations of the rule in Line~3 obtained with substitution 
$\{\var{A}\mapsto\const{a},\linebreak[1]\var{B}\mapsto\const{b},
   \var{M}\mapsto\const{1},\var{N}\mapsto\const{2}\}$.
Note that \pred{mix}/$2$ and \pred{-mix}/$2$ each admit four options,
corresponding to the cross product of $\{\const{a},\const{b}\}$ substituted
for~\var{A} and~\var{B}, respectively, together with $\{\const{1},\const{2}\}$
substituted for~\var{M} and~\var{N}.
While the instances obtained for \pred{mix}/$2$ give rise to four rules,
the instances for \pred{-mix}/$2$ jointly belong to the body.
The (repeated) body also contains two instances each of \pred{sym}/$1$ and of \pred{num}/$1$.
We thus get the rules:%
\marginlabel{%
  Simplified versions of these rules are produced via call:\\
  \code{\mbox{~}gringo -t \attach{examples/pool.lp}{pool.lp}}}
%
\begin{lstlisting}[numbers=none]
mix(a,1) :- sym(a),sym(b), num(1),num(2), not -mix(1,a),
  not -mix(1,b), not -mix(2,a), not -mix(2,b).
mix(a,2) :- sym(a),sym(b), num(1),num(2), not -mix(1,a),
  not -mix(1,b), not -mix(2,a), not -mix(2,b).
mix(b,1) :- sym(a),sym(b), num(1),num(2), not -mix(1,a),
  not -mix(1,b), not -mix(2,a), not -mix(2,b).
mix(b,2) :- sym(a),sym(b), num(1),num(2), not -mix(1,a),
  not -mix(1,b), not -mix(2,a), not -mix(2,b).
\end{lstlisting}
\eexample
\end{example}
%
Additionally, there is the \code{;;} operator for pooling, 
which can only be used to separate arguments of predicates.
This operator does not work on single terms but
simply lists arguments of predicates.
The rules for expanding the predicates are the same as for the \code{;} operator.

\begin{example}\label{ex:sep}
The following example show the difference between the \code{;} and \code{;;} operator:
\marginlabel{%
  Simplified versions of these rules are produced via call:\\
  \code{\mbox{~}gringo -t \attach{examples/sep.lp}{sep.lp}}}
%
\lstinputlisting{examples/sep.lp}
%
The second line is expanded into the following:
\begin{lstlisting}[firstnumber=2]
p(X,Z) :- p(X,Y), p(Y,Z). 
\end{lstlisting}%
and the third line into:
\begin{lstlisting}[firstnumber=3]
p(X,Z) :- p(X,Y,Z), p(X,Y,Z).
\end{lstlisting}%
Clearly, the first variant is the desired expansion in this case 
to calculate the transitive closure.
Both operators have their usages in different scenarios 
to keep the encoding more compact and readable.
\eexample
\end{example}


\subsubsection{Aggregates}\label{subsec:gringo:aggregate}
\index{Aggregates}

An aggregate is an operation on a multiset of weighted literals that evaluates to some value. 
In combination with comparisons, we can extract a truth value from an aggregate's evaluation,
thus, obtaining an aggregate atom.
We consider aggregate atoms of the form:
\[l\,\mathsf{op}\,\code{[}\, L_1\code{=}w_1\code{,} \dots\code{,} L_n\code{=}w_n {\,]\,} u\]

An aggregate has a lower bound $l$, an upper bound $u$, an operation $\mathsf{op}$, 
and a multiset of literal $L_i$ each assigned to a weight $w_i$.
An aggregate is true if operation $\mathsf{op}$ applied to the multiset of weights 
of true literals is between the bounds (inclusive).
Currently, \gringo\ supports the aggregates 
\code{\#sum} (the sum of weights), \index{Aggregates!Sum, \code{\#sum}}
\code{\#min} (the minimum weight), \index{Aggregates!Minimum, \code{\#min}}
\code{\#max} (the maximum weight), and \index{Aggregates!Maximum, \code{\#max}}
\code{\#avg} (the average of all weights \index{Aggregates!Average, \code{\#avg}}
\footnote{The average aggregate over an empty set of weights is defined to be always true irrespective of any bounds.}%
).
Furthermore, there are three aggregates that are syntactically different.
The first is the \code{\#count}\index{Aggregates!Count, \code{\#count}} aggregate:
\[l\,\code{\#count}\,\code{\char`\{}\, L_1\code{,} \dots\code{,} L_n \,\code{\char`\}}\, u\]%
which basically are \code{\#sum} aggregates with all weights set to one 
and duplicate true literals counted only once.
Finally, there are the two parity aggregates:
\index{Aggregates!Even Parity, \code{\#even}}%
\index{Aggregates!Odd Parity, \code{\#odd}}%
\begin{align*}
&\code{\#even}\,\code{\char`\{}\, L_1\code{,} \dots\code{,} L_n \,\code{\char`\}} & &
\code{\#odd}\,\code{\char`\{}\, L_1\code{,} \dots\code{,} L_n \,\code{\char`\}}
\end{align*}%
These aggregates are true if the number of different true literals is even or odd, respectively.

As regards syntactic representation,
weight~\const{1} is considered a default,
so that $L_i\code{=}\const{1}$ can simply be written as $L_i$.
For instance, the following (multi)sets of (weighted) literals are the same
when combined with any kind of aggregate operation and bounds:
\begin{lstlisting}[numbers=none,escapechar=@]
[a=1, not b=1, c=2]  @\textnormal{and}@
[a,   not b,   c=2]@\textnormal{.}@
\end{lstlisting}
%
Furthermore,
keyword \const{\#sum} may be omitted, which in a sense makes \const{\#sum} the default
aggregate operation.
In fact, the following aggregate atoms are synonyms:
\begin{lstlisting}[numbers=none,escapechar=@]
2 #sum [a, not b, c=2] 3  @\textnormal{and}@
2      [a, not b, c=2] 3@\textnormal{.}@
\end{lstlisting}
By omitting keyword \const{\#sum}, we obtain the same notation as the one of 
so-called ``weight constraints''~\cite{siniso02a,lparseManual}, which are actually aggregate atoms
whose operation is addition.

It is important to note that the (weighted) literals within an aggregate
belong to a multiset.
In particular, if there are multiple occurrences
$L\code{=}w_1,\dots,L\code{=}w_k$
of a literal~$L$, in combination with \const{\#min} and \const{\#max},
it is not the same like having $L\code{=}w_1+\dots+w_k$.
To see this, note that the program consisting of the facts:
\begin{lstlisting}[numbers=none]
2 #max [a=2].  2 #min [a=2].
\end{lstlisting}
has $\{\code{a}\}$ as its unique answer set, while there is no answer set for:
\begin{lstlisting}[numbers=none]
2 #max [a,a].  2 #min [a,a].
\end{lstlisting}

If literals ought not to be repeated,
we can use \const{\#count} instead of \const{\#sum}.
Syntactically, \const{\#count} requires curly instead of square
brackets, and there must not be any weights within a \const{\#count} aggregate.
Regarding semantics,
% \begin{equation*}%\label{eq:aggregate:atom}
$(
  l\,
  \const{\#count} 
  \,
  \code{\char`\{}
  \,
  L_1\code{,}
  \dots\code{,}
  L_n
  \,
  \code{\char`\}}
  \,
  u
)$ 
%\end{equation*}
reduces to
$(
  l\,
  \const{sum}
  \,
  \code{[}
  \,
  L_1\code{=}\const{1}\code{,}
  \dots\code{,}
  L_m\code{=}\const{1}
  \,
  \code{]}
  \,
  u
)$,
where $\{L_1,\dots,L_m\}=\{L_i \mid 1\leq i\leq n\}$ is obtained by dropping
repeated literals.
Of course, the use of~$l$ and~$u$ is optional also with \const{\#count}.
As an example, note that the next aggregate atoms express the same:
\begin{lstlisting}[numbers=none,escapechar=@]
1 #sum   [a=1, not b=1]     1  @\textnormal{and}@ 
1 #count {a,a, not b,not b} 1@\textnormal{.}@  
\end{lstlisting}
Keyword \const{\#count} can be omitted (like \const{\#sum}),
so that the following are synonyms:
\begin{lstlisting}[numbers=none,escapechar=@]
1 #count {a, not b} 1  @\textnormal{and}@ 
1        {a, not b} 1@\textnormal{.}@  
\end{lstlisting}
The last notation is similar to the one of so-called
``cardinality constraints''~\cite{siniso02a,lparseManual},
which are aggregate atoms using counting as their operation.

After considering the syntax and semantics of ground aggregate atoms,
we now turn our attention to non-ground aggregates.
Regarding contained variables, an atom occurring in an aggregate behaves
similar to an atom on the left-hand side of a condition
(cf.\ Section~\ref{subsec:gringo:condition}).
That is, any variable occurring within an aggregate is a priori local,
and it must be bound via a variable of the same name that is global
or that occurs on the right-hand side of a condition
(with the atom containing the variable in front).
As with local variables of conditions, global variables take priority
during grounding, so that the names of local variables must be chosen
with care to avoid accidental clashes.
Beyond conditions (which are more or less the natural construct to use
for instantiating variables within an aggregate),
classical negation (cf.\ Section~\ref{subsec:gringo:negation}),
built-in arithmetic functions (cf.\ Section~\ref{subsec:gringo:arith}),
intervals (cf.\ Section~\ref{subsec:gringo:interval}), and 
pooling (cf.\ Section~\ref{subsec:gringo:pool})
can be incorporated as usual within aggregates,
where intervals and pooling are expanded locally.%
\footnote{%
  Assignments (cf.\ Section~\ref{subsec:gringo:assign}) 
  are permitted on the right-hand sides of conditions only.}
That is, an interval gives rise to multiple literals connected via~``\code{,}''
within the same aggregate.
The same applies to pooling in front of a condition,
while it turns into a composite condition chained by~``\code{:}'' on the right-hand side.
Finally, note that aggregates 
\code{\#sum}, \code{\#count}, \code{\#min}, and \code{\#max}
without bounds are also permitted on the
right-hand sides of assignments, but using this feature is only recommended
for aggregates whose atoms belong to domain predicates because space blow-up
can become a bottleneck otherwise.
The following example, making exhaustive use of aggregates,
nonetheless demonstrates this and other features.

\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 first condition is that~\const{3} to~\const{6} courses should be enrolled:
%
\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{~}gringo -t \attach{examples/aggr.lp}{aggr.lp}}}
%
\begin{lstlisting}[firstnumber=9,stepnumber=9]
3 { enroll(1), enroll(2), enroll(3), enroll(4), 
    enroll(5), enroll(6), enroll(7), 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=15,firstnumber=10]{examples/aggr.lp}
%
Each of the three integrity constraints above contains a \const{sum} aggregate,
using default weight~\const{1} for literals.
Recalling that \const\#{sum} aggregates operate on multisets,
duplicates are not removed.
Thus, the integrity constraint in Line~10 is instantiated as follows:
%
\begin{lstlisting}[firstnumber=10,stepnumber=10]
:- [ enroll(1) = 1, enroll(1) = 1, 
     enroll(2) = 1, enroll(2) = 1,
     enroll(3) = 1, enroll(3) = 1,
     enroll(4) = 1, enroll(4) = 1, enroll(4) = 1,
     enroll(5) = 1, enroll(5) = 1,
     enroll(6) = 1, enroll(6) = 1,
     enroll(7) = 1, enroll(7) = 1, enroll(7) = 1,
     enroll(8) = 1, enroll(8) = 1 ] 10.
\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'').
Also note that, given the facts in Line~1--8,
we could equivalently have used \const{count} rather than \const{sum} in Line~11,
but not in Line~10 and~12.

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=17,lastline=18,firstnumber=13]{examples/aggr.lp}
%
The rule in Line~13 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:
%
\lstinputlisting[nolol,firstline=20,lastline=22,firstnumber=15]{examples/aggr.lp}
%
As Line~15 shows,
we may use default negation via ``\code{not}'' in front of aggregate atoms,
and bounds may be specified in terms of variables.
In fact, by instantiating~\var{M} to~\const{20},
we obtain the following ground instance of the integrity constraint in Line~15:
%
\begin{lstlisting}[firstnumber=15,stepnumber=15]
:- not 18 [ enroll(1) = 5, enroll(2) = 4, 
            enroll(3) = 6, enroll(4) = 3,
            enroll(5) = 4, enroll(6) = 2,
            enroll(7) = 4, enroll(8) = 5 ] 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~16 and~17, respectively,
work on the same (multi)set of weighted literals as in Line~15.
While the integrity constraint in Line~16 stipulates that any course to enroll
must include more than~\const{2} contact hours,
the one in Line~17 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=16]
:- 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 within assignments:
%
\lstinputlisting[nolol,firstline=24,lastline=25,firstnumber=18]{examples/aggr.lp}
%
Note that the above aggregates have already been used in Line~9 and~15, respectively,
where keywords \const{\#count} and \const{\#sum} have been omitted for convenience.
These keywords can be dropped here too, and we merely include them to show the
more verbose notations of \const{\#count} and \const{\#sum} aggregates.
However, the usage of aggregates in the last two lines is different from before,
as they now serve to assign an integer to a variable~\var{N}.
In this context, bounds are not permitted, and so none are provided in Line~18 and~19.
The effect of these two lines 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{~}gringo \attach{examples/aggr.lp}{aggr.lp} | \textbackslash\\
        \mbox{~}clasp -n 0}\\
  or alternatively:\\
  \code{\mbox{~}clingo -n 0 \attach{examples/aggr.lp}{aggr.lp}}}
%
In fact, running \clasp\ shows the student 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.

Although the above program does not reflect this possibility,
it should be noted that (as has been mentioned in Section~\ref{subsec:gringo:condition})
multiple literals may be connected via ``\code{:}'' in order to construct
composite conditions within an aggregate.
As before, the predicates of atoms on the right-hand side of such conditions
must be either domain predicates or built-in.
Furthermore, the usage of non-domain predicates within an aggregate
on the right-hand side of an assignment (like \pred{enroll}/$1$ in Line~18 and~19 above)
is not recommended in general because the space blow-up may be significant.
\eexample
\end{example}

%\com{Should we mention stratifed aggregates that do not necessarily need conditions?}

\subsubsection{Optimization}\label{subsec:gringo:optimize}
\index{Statements!Optimize Statements}

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 the
optimization statements of \lparse~\cite{lparseManual},
indicated via keywords \const{\#maximize} and \const{\#minimize}.
As an optimization statement does not admit a body, any (local) variable
in it must also occur in an atom (over a domain or built-in predicate)
on the right-hand side of a condition (cf.\ Section~\ref{subsec:gringo:condition})
within the optimization statement.
In multiset notation (square brackets),
weights may be provided as with \const{\#sum} aggregates. %,
In set notation (curly brackets),
duplicates of literals are removed
as with \const{count} aggregates.
Additionally, priorities can be associated with each literal.
A (ground) optimize statement has the form: 
\index{Statements!Optimize Statements!\#minimize}%
\index{Statements!Optimize Statements!\#maximize}%
\[\mathsf{opt}\,\code{[}\,L_1=w_1@p_1,\dots,L_n=w_n@p_n\,\code{\char`\}}\] 
\[\mathsf{opt}\,\code{\char`\{}\,L_1@p_1,\dots,L_n@p_n\,\code{\char`\}}\]
where $\mathsf{opt}$ is either \code{\#maximize} or \code{\#minimize} , $L_i$ are literals 
with associates (integer) weights $w_i$ and (integer) priorities $p_i$.

The semantics of an optimization statement is intuitive:
an answer set is \emph{optimal} if the sum of weights
(using~\const{1} for unsupplied weights)
of literals that hold is maximal or minimal, as required by the statement,
among all answer sets of the given program.
This definition is sufficient if a single optimization statement is specified
along with a logic program.
If different priorities occur in the program, 
then, depending on the type of optimize statement,
answer sets whose sum of weights assigned to higher priorities
is maximized or minimized, respectively.

Note that for compatibility with \lparse, if multiple optimize statements are used, 
default priorities are assigned.
The $n$-th statement gets priority $n$, thus, the later statements have higher priorities.
We suggest that if you want to use more than one optimization statement,
to always specify priorities to make the program more readable and order independent.

\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 an 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--5 of the following program:
%
\lstinputlisting[xrightmargin=-26pt]{examples/opt.lp}
%
Line~6--8 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~8 states that
avoiding noise is our main priority.
The secondary optimization criterion in Line~7 consists of
minimizing the cost per star.
Finally, the third optimization statement in Line~6 specifies that we want
to maximize the number of stars among hotels that are otherwise indistinguishable.
The optimization statements in Line~6--8 are instantiated as follows:%
\marginlabel{%
  The full ground program is obtained by invoking:\\
  \code{\mbox{~}gringo -t \attach{examples/opt.lp}{opt.lp}}}
%
\begin{lstlisting}[firstnumber=6,breakindent=0pt,escapechar=&]
#maximize [ hotel(1)=5@1, hotel(2)=4@1, &\\&            hotel(3)=3@1, hotel(4)=3@1, hotel(5)=2@1 ].
#minimize [ hotel(1)=34@2, hotel(2)=35@2, &\\&            hotel(3)=30@2, hotel(4)=25@2, hotel(5)=30@2 ].
#minimize [ noisy=1@3 ].
\end{lstlisting}
If we now use \clasp\ to compute an optimal answer set,%
\marginlabel{%
  To compute the unique optimal answer set, invoke:\\
  \code{\mbox{~}gringo \attach{examples/opt.lp}{opt.lp} | \textbackslash\\
        \mbox{~}clasp -n 0}\\
  or alternatively:\\
  \code{\mbox{~}clingo -n 0 \attach{examples/opt.lp}{opt.lp}}}
we find that hotel~\const{4} is not eligible because it implies \pred{noisy}.
Thus, hotel~\const{3} and~\const{5} remain as optimal w.r.t.\ the second most
significant optimization statement in Line~7.
This tie is broken via the least significant optimization statement in Line~6
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.
\eexample
\end{example}


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

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

\paragraph{Comments.}
\index{Meta-Statements!Comments}
To keep records of the contents 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=@]
@\textit{logic program}@  %* enclosed comment *%  @\textit{logic program}@
@\textit{logic program}@  % comment till end of line
@\textit{logic program}@
%*
comment over multiple lines
*%
@\textit{logic program}@
\end{lstlisting}

\paragraph{Hiding Predicates.}
\index{Meta-Statements!Hiding Predicates, \code{\#show}, \code{\#hide}}%
Sometimes, one may be interested only in a subset of the atoms belonging
to an answer set.
In order to suppress the atoms of ``irrelevant'' predicates from the output,
the \code{\#hide} declarative can be used.
The meanings of the following statements are indicated via accompanying comments:
%
\begin{lstlisting}[numbers=none]
#hide.     % Suppress all atoms in output
#hide p/3. % Suppress all atoms of predicate p/3 in output
#hide p(X,Y) : q(X). % Supress p/3 if the condition holds
\end{lstlisting}
Note that for the conditionals on the right-hand side, 
the same conditions as described in Section \ref{subsec:gringo:condition} apply.

In order to selectively include the atoms of a certain predicate in the output,
one may use the \code{\#show} declarative.
Here are some examples:
%
\begin{lstlisting}[numbers=none]
#show p/3. % Include all atoms of predicate p/3 in output
#show(X,Y) : q(X). % Include p/3 if the condition holds
\end{lstlisting}
%
A typical usage of \code{\#hide} and \code{\#show} is to hide all predicates
via ``\code{\#hide.}'' and to selectively re-add atoms of certain predicates
\code{p/$n$} to the output via ``\code{\#show p/$n$.}''

\paragraph{Constant Replacement.}
\index{Meta-Statements!Constant Replacement, \code{\#const}}%
Constants appearing in a logic program may actually be placeholders for
concrete values to be provided by a user.
An example of this is given in Section~\ref{subsec:ex:color}.
Via the \code{\#const} declarative,
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 (symbolic) constant on the left-hand side and a term on the right-hand side.
Some exemplary constant declarations are:
%
\begin{lstlisting}[numbers=none]
#const x = 42.
#const y = f(x,h).
\end{lstlisting}

\begin{Note}
that (for efficiency reasons) constant declarations are order dependent.
In the example above \code{x} would be replaced by \code{42}
but when reversing the directives this would no longer be the case.
\end{Note}

\paragraph{Domain Declarations.}
\index{Meta-Statements!Domain Declarations, \code{\#domain}}%
Usually, variable names are local to a rule,
where they must be bound via appropriate atoms.
This locality can be undermined by using
\code{\#domain} declarations 
that globally associate variable names to atoms.
An associated atom is then simply added to the body of a rule in which
such a predefined variable name occurs in.
The following is a made-up example:
%
\begin{lstlisting}[numbers=none]
p(1,1). p(1,2).
#domain p(X,Y).
#domain p(Y,Z).
q(Z,X) :- not p(Z,X).
\end{lstlisting}
%
The above program is a priori not safe because
variables~\var{X} and~\var{Z} are unbound in the last rule.
However, as they belong to \code{\#domain} declarations,
\gringo\ and \clingo\ expand the last rule to:
%
\begin{lstlisting}[numbers=none]
q(Z,X) :- p(X,Y), p(Y,Z), not p(Z,X).
\end{lstlisting}
%
Observe that the resulting program is safe.

\begin{Note}
that we suggest not to use domain statements because 
in ASP it is common to use very short variable names and
using domain statements likely results in name clashes
and undesired behavior.
\end{Note}

\paragraph{Compute Statements.}
\index{Meta-Statements!Compute Statements, \code{\#compute}}%
These statements are artifacts supported for backward compatibility.
Although we strongly recommend to avoid compute statements,
we now describe their syntax.
A compute statement is of the form
``$\const{\#compute}~n \code{\char`\{}\dots\code{\char`\}}\code{.}$''
(the non-negative integer $n$ is optional),
where the ``$\code{\char`\{}\dots\code{\char`\}}$'' part
is similar to a \const{\#count} aggregate.
The meaning is that all literals contained in
``$\code{\char`\{}\dots\code{\char`\}}$'' must hold w.r.t.\ answer sets
that are to be computed,
while~$n$ specifies a number of answer sets to compute.
As \clasp, \clingo, and \iclingo\ provide command line option
\code{--number} (cf.\ Section~\ref{subsec:opt:clasp})
to specify how many answer sets are to be computed,
they simply ignore~$n$.
Furthermore,
the ``$\code{\char`\{}\dots\code{\char`\}}$'' part can equivalently
be expressed in terms of integrity constraints,
as indicated in the comments provided along with the following example:
%
\begin{lstlisting}[xrightmargin=-20pt,numbers=none]
q(1;2).
{ p(1..5) }.
#compute 0 { p(X) : q(X) }.       % :- 1 { not p(X) : q(X) }.
#compute   { not p(X) : X=4..5 }. % :- 1 { p(X) : X=4..5 }.
\end{lstlisting}

\begin{Note}
that compute statement are not needed in general.
The same behavior can be achieved by using integrity constraints.
In fact, compute statements exist mainly for compatibility reasons with \lparse.
We suggest to not use them.
\end{Note}

\paragraph{External Statements.}
\index{Meta-Statements!External Statements, \code{\#external}}%
External statements are used to mark certain atoms as external. This means 
that those atoms are not subject of simplification and consequently are not removed 
from the logic program. There are two kinds of external directives, 
global and local external statements.

Global external statements have the form \code{\#external predicate/arity.} where 
\code{predicate} refers to the name of a predicate and \code{arity} to the arity of the predicate.
They mark complete predicates irrespective of any arguments as external.
This means that nothing is known about the predicate and hence it cannot be used 
for instantiation.
\begin{example}
Consider the following example:
\begin{lstlisting}[numbers=none]
#external q/1.
p(1). p(2).
r(X) :- q(X), p(X).
\end{lstlisting}
Here, the external predicate \code{q}/$1$ is not used for simplification
of the problem and hence two ground rules (excluding facts) are printed.
\eexample
\end{example}

Local external statements have the form \code{\#external predicate (: conditional)*.} where
\code{predicate} is some non-ground predicate and \code{conditional} some conditional.
In contrast to global external directives, local external statements precisely specify 
which atoms are external and hence can be used for instantiation.
\begin{example}
Again, consider a similar example:
\begin{lstlisting}[numbers=none]
#external q(X) : p(X).
p(1). p(2).
r(X) :- q(X).
\end{lstlisting}
Here, the external predicate \code{q}/$1$ is used to bind variable \code{X}, 
yielding the same rules as in the example above.
\eexample
\end{example}

Furthermore, the \lparse\ output\cite{lparseManual} has been modified to include an additional table 
that stores a list  of all external atoms. For compatibility, this table is only inserted if the 
program actually contains external directives. It contains the respective atom indices terminated
by a zero and is inserted directly after \lparse' compute statement.
\begin{example}
The following listing shows schematic example output of \gringo\ when external statements are used:
\begin{lstlisting}[numbers=none]
  ...
  0
  ...
  0
  B+
  ...
  0
  B-
  ...
  0
  E
  2
  3
  4
  ...
  0
  1
\end{lstlisting}
\eexample
\end{example}

\subsubsection{Integrated Scripting Language}\label{subsec:lang:lua}
\index{Lua}%
Utilizing the scripting language Lua\footnote{\url{http://www.lua.org}}, 
\gringo's input language can be enriched by arbitrary arithmetical functions and implicit domains,
answer sets can be intercepted and for example inserted into a database, or
interactions between grounding and solving are possible when incrementally solving with \iclingo.
We do not give an introduction to Lua here (there are numerous tutorials on the web), 
but give some examples showing the capabilities of this integration.

\begin{example}
The first example shows basic Lua usage:
\lstinputlisting{examples/luaf.lp}
\marginlabel{%
To compute the unique answer set, invoke:\\
\code{%
\mbox{~}gringo -t \attach{examples/luaf.lp}{luaf.lp}}
}%
In Line 3 we add a function that calculates the greatest common divisor of two numbers.
This function is called in Line 20 and the result stored in predicate \code{gcd}/$3$.
Note that Lua function calls look like function symbols but are preceded by ``\code{@}''. 
\index{Terms!Lua Function Call}%
\index{Lua!Function Call}%
Regarding binding of variables, the same restrictions as with arithmetic in Section \ref{subsec:gringo:arith} apply.

In Line 9 we add a function that emulates a range term.
It returns a table containing all numbers in the interval $[\code{a},\code{b}]$.
\index{Lua!Term Insertion}%
The values in this table are then successively inserted for the call \code{\@rng(X,Y)}.
In fact, this function exactly behaves like a range term.
\eexample
\end{example}

\begin{table}[ht]
\centering
\index{Lua!Val Metatable}%
\begin{tabular}{||l|l||}
 \hline 
 \code{Val.NUM}  & Type identifier for \gringo\ numbers.\\
 \hline 
 \code{Val.ID}   & Type identifier for \gringo\ strings.\\
 \hline 
 \code{Val.FUNC} & Type identifier for function symbols.\\
 \hline 
 \code{Val.SUP}  & Type identifier for \gringo's \code{\#supremum}.\\
 \hline 
 \code{Val.INF}  & Type identifier for \gringo's \code{\#infimum}.\\
 \hline 
 \code{Val.new(type[,value][,args])}  & Creates new ground terms (see Example \ref{ex:lua:values}).\\
 \hline 
 \code{Val.cmp(a,b)}  & Compares two ground \gringo\ terms. \\
 \hline 
 \code{Val.type(a)} & Returns the type of a term. \\
 \hline 
 \code{Val.name(f)} & Returns the name of function symbol \code{f}. \\
 \hline 
 \code{Val.args(f)} & Returns the arguments of function symbol \code{f} \\
 \hline
\end{tabular}
\caption{The Val meta-table.\label{tab:val}}
\end{table}


\begin{example}\label{ex:lua:values}
The second example shows how to create ground terms from within Lua:
\lstinputlisting{examples/luav.lp}
\marginlabel{%
To compute the unique answer set, invoke:\\
\code{%
\mbox{~}gringo -t \attach{examples/luav.lp}{luav.lp}}
}%
Function \code{f} in Line 2 returns a tuple 
whose first member is a string indicating the type of the argument 
and the second reconstructs the value passed to function \code{f}.
Note that in Line 4, 6, 9, 11 and 13 the function \code{Val.new} is called.
Its first argument indicates that a function symbol is to be created and 
the second argument passes the arguments of the function symbol.
We do not give a name for the function symbol,
thus a tuple is created (this is equivalent to passing the empty string as name).
Similarly, \gringo's other in-built ground terms are created.
Finally, note that \gringo\ integers and strings are directly mapped 
to the respective Lua types.
\eexample
\end{example}

\begin{table}[ht]
\index{Lua!Assignment Metatable}%
\centering
\begin{tabular}{||l|p{6cm}||}
 \hline 
 \code{Assignment.begin(n,a)} & Starts iteration over an atom with name~\code{n} with arity~\code{a}. \\
 \hline 
 \code{Assignment.next()}     & Advances to the next atom in the assignment and returns false if there is none. \\
 \hline 
 \code{Assignment.args()}     & The arguments of the current atom. \\
 \hline 
 \code{Assignment.isTrue()}   & The current atom is true. \\
 \hline 
 \code{Assignment.isFalse()}  & The current atom is false. \\
 \hline 
 \code{Assignment.isUndef()}  & The current atom is undefined. \\
 \hline 
 \code{Assignment.level()}    & The decision level on which the current atom has been assigned. \\
 \hline
\end{tabular}
\caption{The Assignment meta-table.\label{tab:assignment}}
\end{table}

\begin{example}
The next example show some advanced usage also accessing \clasp's truth assignment:
\lstinputlisting{examples/sql.lp}
This example creates a database connection using SQLite\footnote{\url{http://www.sqlite.org/}}.
The database connection is created Lines 3-4 using LuaSQL\footnote{\url{http://www.keplerproject.org/luasql/}}.
Initially, a new table \code{test} is created if it does not already exists (Lines 5-7).
There are two functions to access this table.
The first function \code{query} in Line 9 selects everything from the table and 
returns it in form of a Lua table, which is then used in the logic program
to provide new instantiations of~\code{p}/$2$ in Line 42.
The second function \code{insert} is a helper function that expects a predicate name
and then inspects \clingo's (or \iclingo's) possibly partial assignment and
inserts all true atoms into the database.
It makes use of the \code{Assignment} meta-table.
Next, note the three functions
\code{onBeginStep},
\code{onModel}, and
\code{onEndStep} 
in Line 35-37.
The first function is called directly before solving but after preprocessing.
At this point grounded facts are accessible via the \code{Assignment} meta-table (Table \ref{tab:assignment}),
we call \code{insert} to insert all ground instantiation of \code{p}/$2$ into the \code{test} table.
The same is done in the \code{onModel} function whenever a model is found.
At this point \clingo's assignment is total and 
we insert all instantiation of \code{q}/2 into the database that are contained in the answer set.
Finally, in function \code{onEndStep} we print the number of tuples inserted during grounding and after solving.

\marginlabel{%
Try to invoke this program multiple times using:\\
\code{%
\mbox{~}clingo \attach{examples/sql.lp}{sql.lp}}
}
Note that the values from the answer set are inserted into the database.
In fact the output of the program changes when it is consecutively called.
Even more non-determinism can be added by using the option \code{--rand-freq=1.0}
to induce 100 percent random decisions.
%\com{Admittedly, this example is somewhat spacy. Better ideas?}
\eexample
\end{example}

\subsection{Input Language of \iclingo}\label{subsec:lang:iclingo}
\index{Incremental Grounding}%

System \iclingo~\cite{gekakaosscth08a} extends \clingo\ by an
\emph{incremental} computation mode that incorporates both grounding and solving.
Hence, its input language includes all constructs described
in Section~\ref{subsec:lang:gringo}.
In addition, \iclingo\ deals with statements of the following form:
%
\begin{lstlisting}[numbers=none,escapechar=@]
#base.
#cumulative @\textit{constant}@.
#volatile   @\textit{constant}@.
\end{lstlisting}
%
\index{Incremental Grounding!Base Part, \code{\#base}}%
\index{Meta-Statements!Base Part, \code{\#base}}%
Via ``\code{\const{\#base}.},''
the subsequent part of a logic program is declared as static, that is,
it is processed only once at the beginning of an incremental computation.
In contrast, ``\code{\const{\#cumulative} \textit{constant}.}''
and ``\code{\const{\#volatile} \textit{constant}.}'' are used to declare
a (symbolic) \code{\textit{constant}} as a placeholder for incremental step numbers.
In the parts of a logic program below a \const{\#cumulative} statement,
\code{\textit{constant}} is in each step replaced with the current step number,
and the resulting rules, facts, and integrity constraints are accumulated
over a whole incremental computation.
While the replacement of \code{\textit{constant}} is similar,
a logic program part below a \const{\#volatile} statement is local to steps,
that is, all rules, facts, and integrity constraints computed in one step
are dismissed before the next incremental step.
Note that the type of a logic program part (static, cumulative, or volatile)
is determined by the last
\index{Incremental Grounding!Cumulative Part, \code{\#cumulative}}%
\index{Meta-Statements!Cumulative Part, \code{\#cumulative}}%
\index{Incremental Grounding!Volatile Part, \code{\#volatile}}%
\index{Meta-Statements!Volatile Part, \code{\#volatile}}%
\const{\#base}, \const{\#cumulative}, or \const{\#volatile} statement
preceding it.

During an incremental computation, all static program parts are grounded first,
while cumulative and volatile parts are grounded step-wise,
replacing \code{\textit{constant}}s with successive step numbers starting from~\const{1}.
Note that due to \gringo's grounding algorithm,
rules are not grounded twice using the same substitution of global variables
(the incremental constant is treated like a global constant here).
After a grounding step, \clasp\ is usually invoked via an internal interface
(like with \clingo), and the incremental computation stops after a step
in which at least one answer set has been found by \clasp.
This default behavior can be readapted via command line 
options (cf.\ Section~\ref{subsec:opt:iclingo}).
For obtaining a well-defined incremental computation result,
it is important that (ground) head atoms within static, cumulative, and volatile program parts
are distinct from each other, and they must also be different from step to step
(see~\cite{gekakaosscth08a} for details).
In Section~\ref{subsec:ex:block},
we provide a typical example in which these conditions naturally hold.

\begin{example}
For now, consider this simple Schur number example:
\lstinputlisting{examples/inc.lp}
\marginlabel{%
  To calculate the Schur number, invoke:\\
  \code{\mbox{~}iclingo \attach{examples/inc.lp}{inc.lp} \textbackslash\\
  --istop=UNSAT
  }\\
  The solving stops when the largest number has been found.
}%
The Schur number~$n$ w.r.t. to a given number~$c$ is the largest integer 
such that the interval~$[1..n]$ can be partitioned into $c$ sum-free sets.
A set $S=\{c_1 ,\dots, c_k\}$ is sum-free if for each~$x_i$ and~$x_j$, 
it holds that~$x_i + x_j \not \in S$.

In the base part in Line 2 we specify the number of partitions.
Then, in the cumulative part in Line 4 each fresh integer $k$
is assigned to exactly one partition.
In Line 5 we check whether the guessed partition is sum-free.
Note that we put this check in the cumulative part and incrementally extend it.
The idea here is to keep as much constraints in the cumulative part
because \clasp\ applies nogood learning and only information learnt from 
the cumulative part can be kept among further solving steps;
all information learnt from the volatile part has to be forgotten.
Additionally, we use the comparison  \code{X <= Y}, 
which helps to avoid grounding some redundant rules.
Furthermore, note that there appears no incremental constant in this rule,
\gringo's grounding algorithm makes sure that no ground instantiation of this rule 
is grounded twice just the new slice for the next step is instantiated.
Finally, we break symmetries in Line 6, i.e.,
number one is always assigned to partition one, number two to partition two 
if it is not in partition one, and so on. 

We use option \code{--istop=UNSAT} to solve as long as 
\iclingo\ is able to find a solution, i.e., there is a 
valid partitioning. Once this is no longer possible, the grounding/solving 
process stops.\eexample
\end{example}

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

Solver \clasp~\cite{gekanesc07b} works on logic programs in \lparse's
output format~\cite{lparseManual}.
This numerical format, which is not supposed to be human-readable,
is output by \gringo\ and can be piped into \clasp.
Such an invocation of \clasp\ looks as follows:
%
\begin{lstlisting}[numbers=none]
gringo [ options | filenames ] | clasp [ number | options ]
\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{--number} or its abbreviation \code{-n}
(cf.\ Section~\ref{subsec:opt:clasp}).
By default, \clasp\ computes one answer set (if it exists).
If a logic program in \lparse's output format has been stored in a \code{file},
it can be redirected into \clasp\ as follows:%
\footnote{%
  The same is achieved by using option \code{--file} or its short form \code{-f}
  (cf.\ Section~\ref{subsec:opt:clasp}).}
%
\begin{lstlisting}[numbers=none]
clasp [ number | options ] < file
\end{lstlisting}
%
Via option \code{--dimacs},
\clasp\ can also be instructed to compute models of a propositional formula
in DIMACS/CNF format~\cite{dimacs}.
If such a formula is contained in \code{file},
then \clasp\ can be invoked in the following way:
%
\begin{lstlisting}[numbers=none]
clasp [ number | options ] --dimacs < file
\end{lstlisting}
%
Finally, \clasp\ may be used as a library, as done within \clingo\ and \iclingo.

Solver \clasp~\cite{gekanesc07b} works on logic programs in \lparse's
output format~\cite{lparseManual}.
This numerical format, which is not supposed to be human-readable,
is output by \gringo\ and can be piped into \clasp.
Such an invocation of \clasp\ looks as follows:
%
\begin{lstlisting}[numbers=none]
gringo [ options | filenames ] | clasp [ number | options ]
\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{--number} or its abbreviation \code{-n}
(cf.\ Section~\ref{subsec:opt:clasp}).
By default, \clasp\ computes one answer set (if it exists).
If a logic program in \lparse's output format has been stored in a \code{file},
it can be redirected into \clasp\ as follows:%
\footnote{%
  The same is achieved by using option \code{--file} or its short form \code{-f}
  (cf.\ Section~\ref{subsec:opt:clasp}).}
%
\begin{lstlisting}[numbers=none]
clasp [ number | options ] < file
\end{lstlisting}
%
Via option \code{--dimacs},
\clasp\ can also be instructed to compute models of a propositional formula
in DIMACS/CNF format~\cite{dimacs}.
If such a formula is contained in \code{file},
then \clasp\ can be invoked in the following way:
%
\begin{lstlisting}[numbers=none]
clasp [ number | options ] --dimacs < file
\end{lstlisting}
%
Finally, \clasp\ may be used as a library, as done within \clingo\ and \iclingo.
%