Manual.tex

\documentclass[a4paper, titlepage]{article}
\usepackage{graphicx}
\usepackage{url}
\usepackage{hyperref}
\usepackage{listings}
\usepackage{amsmath}
\usepackage{array}
\usepackage{longtable}
\usepackage{multirow}
\usepackage{paralist}
\usepackage{color}
\usepackage{amsthm}

\usepackage{tikz}
\usetikzlibrary{arrows}

\usepackage{csquotes}

\newcommand{\mi}[1]{\mathit{#1}}
\newcommand{\amp}[1]{\ensuremath{\&{\mathit{#1}}}}
\newcommand{\ext}[3]{\ensuremath{\&{\mathit{#1}}[#2](#3)}}
\DeclareMathOperator{\leftimpl}{:-}
\DeclareMathOperator{\weakimpl}{:\sim}
\DeclareMathOperator{\clasneg}{\text{-}}
\DeclareMathOperator{\nott}{\mathit{not}}
\DeclareMathOperator{\noteq}{!=}
\DeclareMathOperator{\noteqq}{<>}
\DeclareMathOperator{\lesseq}{<=}
\DeclareMathOperator{\geeq}{>=}
\newcommand{\lts}{\,{<}\,}
\newcommand{\gts}{\,{>}\,}
\newcommand{\les}{\,{\le}\,}
\newcommand{\ges}{\,{\ge}\,}
\newcommand{\examplelink}[1]{\url{https://github.com/hexhex/manual/tree/master/#1}}
\newcommand{\exampledownloadlink}[2]{\href{https://github.com/hexhex/manual/raw/master/#1}{#2}}

\newcommand\mycenterline[1]{\par\smallskip\centerline{#1} \smallskip}
\newcommand\leftaligned[1]{\par \smallskip \noindent \qquad #1 \smallskip \par}

%\newcommand\mycenterline[1]{\smallskip #1 \smallskip\\}

% for commenting out stuff
\newcommand\nop[1]{}


\setlength{\tabcolsep}{1.5pt}
\lstset{
    literate={~} {$\sim$}{1},
    basicstyle=\footnotesize,
    language=Python,
    showstringspaces=false,
    frame=single
}

\newcommand{\row}[1]{%
  \ensuremath{\color{black}\ensuremath{\mathbf{#1}} \color{black}}%
}

\newcommand{\rowprefix}[1]{%
  \ensuremath{\color{black}\mathbf{#1{:}}\ }%
}

\newcommand{\rowprefixprime}[1]{%
  \ensuremath{\color{black}\mathbf{#1\prime{:}}\ }%
}

\newcommand{\rowprefixprimeprime}[1]{%
  \ensuremath{\color{black}\mathbf{#1\prime\prime{:}}\ }%
}

\newcommand{\tobewritten}[0]{This section to be written.}

\allowdisplaybreaks

\begin{document}
\setcounter{page}{3}
\newcommand{\dlvhex}{{\sc dlvhex}}
\newcommand{\clasp}{{\sf Clasp}}
\newcommand{\gringo}{{\sf Gringo}}
\newcommand{\hex}{{\sc hex}}
\newcommand{\dlv}{{\sc dlv}}
\newcommand{\dlvdb}{{\sc dlvdb}}
\newcommand{\libdlv}{{\sc libdlv}}
\newcommand{\libclingo}{{\sc libclingo}}
\newcommand{\genuineii}{{\sc genuineii}}
\newcommand{\genuinegi}{{\sc genuinegi}}
\newcommand{\genuineic}{{\sc genuineic}}
\newcommand{\genuinegc}{{\sc genuinegc}}

\setcounter{secnumdepth}{4} % how many sectioning levels to assign numbers to
\setcounter{tocdepth}{4}    % how many sectioning levels to show in ToC


\theoremstyle{definition}
\newtheorem{exmpl}{Example}[section]
% add \qed to mark end of example
\newenvironment{exmp}{\begin{exmpl}}{\qed\end{exmpl}}


\begin{titlepage}
    \centering
    %\vfill
    \includegraphics[width=1.0\textwidth]{biglogo_whitebg.png}
    \vskip2cm
        {\bfseries\Huge User Guide} \\[1em]
        {\bfseries\Huge \dlvhex\ 2.X} \\
        \vskip1.0cm
        {\sc\Large INFSYS Research Report 1843-15-05} \\
        \medskip
        {\Large \today}        
        \vskip2cm
        {\bfseries\Large
        Thomas Eiter$^1$\\[2mm]
        Mustafa Mehuljic$^2$ \\[2mm] %\'{c}$^2$ \\[2mm]
        Christoph Redl$^1$ \\[2mm]
        Peter Sch\"{u}ller$^2$ \\[2mm]
        }    
        \vspace{1cm}
        \begin{tabular}{r@{}l}
        {\Large$^1$}
          & Institut f\"ur Informationssysteme,\\
          & Abteilung Wissensbasierte Systems,\\
          & Technische Universit\"at Wien, Austria \\
          & {\tt\{eiter,redl\}@kr.tuwien.ac.at} \\[1ex]
        {\Large$^2$}
          & Department of Computer Engineering,\\
          & Faculty of Engineering, \\
          & Marmara University, Turkey \\
          & {\tt mehuljic.mustafa@gmail.com}\\
          & {\tt peter.schuller@marmara.edu.tr}
        \end{tabular}
        \vspace{4cm}
\end{titlepage}
%
% pdflatex begining.tex 
% bibtex begining.aux
% pdflatex begining.tex 
% pdflatex begining.tex 
%
% Abstract part
\begin{abstract}
This document provides a user guide for the Answer Set 
Programming (ASP) system called \dlvhex{}.
%developed at Technische Universit\"at Wien.
% and in various other places (unical, deri galway(?), sabanci, marmara)
ASP is a declarative 
problem solving paradigm, rooted in logic programming and 
nonmonotonic reasoning, which has been gaining increasing 
attention during the last years. The \dlvhex{} system is a 
reasoner for computing the models of so-called \hex{}-programs, which are an extension of \emph{answer-set 
programs} towards integration of \emph{external computation 
sources}. This guide aims at explaining the syntax
of \hex{}-programs and the usage of the \dlvhex{} solver
to enable users 
to interoperate with a broad set of external computation 
sources. The guide refers to version 2.4 and higher.
\end{abstract}


% Generates table of contents
\setcounter{tocdepth}{2}
\tableofcontents


\newpage
\section{Introduction} % Section No.1
\label{sec:intro}
The \dlvhex{} system is a logic-programming reasoner for 
computing the models of so-called \hex{}-programs~\cite{efikrs2015}, which 
are an extension of \emph{answer-set programs} towards 
integration of \emph{external computation sources}. To 
enable access to external information, \hex{}-programs 
extend programs with external atoms, which allow for a 
bidirectional communication between the logic program and 
external sources of computation (e.g. description logic 
reasoners and Web resources)~\cite{efkr2012}.
The system is motivated by the need to interoperate with a 
broad set of external computation sources and the 
observation, that for meta-reasoning in the context of the 
Semantic Web, no adequate support is available in ASP to 
date.
To overcome this, \hex{}-programs support higher-order logic programs 
(which accommodate meta-reasoning through higher-order 
atoms) with external atoms for software interoperability.

This guide is intended to help beginners make use of the system and 
provide a reference for the features of the tool.
The language of \hex{}-programs is an extension of disjunctive datalog,
it largely realizes the ASP-Core-2 Standard \cite{cffiklrs2013}
and extends it with external and high-order atoms. 


\subsection{Download and Installation}
\dlvhex{} is written in the C++ programming language
and published under the GNU Lesser General 
Public License \cite{licnc}. 
In this section we provide an overview of the 
download and installation process. For a quick overview, 
some examples and the possibility to evaluate 
\hex{}-programs directly in the browser,
an online demo is available at
\url{http://www.kr.tuwien.ac.at/research/systems/dlvhex/demo.php}.
%However the system can also be installed locally. 

\subsubsection{Building from source}
There are two possibilities to install \dlvhex{} 
from source: install the latest stable release of the 
system or install the latest development version which may 
not be stable. Both ways are described in the following 
sections.  

\paragraph{Latest release version (tarball)}
\label{sec:steps}
Packages (tarballs) of \dlvhex{} can be downloaded from the 
project page
\href{http://www.kr.tuwien.ac.at/research/systems/dlvhex/}%
{\tt http://www.kr.tuwien.ac.at/res earch/systems/dlvhex/}.
The latest release of the 
software runs on Linux-based systems, Mac OS X and 
Microsoft Windows. Installation instructions are given in 
the {\tt INSTALL} and {\tt README} files of \dlvhex{} 
and plugin source directories. Changes between versions can 
be found in the {\tt NEWS} files and details about changes in the {\tt 
ChangeLog} file. 

The system requires the following packages:
git, gcc and g++ (version 4.8 or later),
BZ2, Python (version 2.7 or later), bison, scons, 
cmake, automake, autoconf,
%standard C++ library (version 4.8 or later),
Curl (version 4 or later),
libtool, and Boost (version 1.55 or later). 

After downloading Boost from
\url{http://www.boost.org/},
the following steps should be followed in order 
to install it in a way usable for \dlvhex.

Here and in the following, commands prefixed with ``\texttt{\$}'' sign are the commands executed from the system shell.
%Some commands need ``\texttt{\#}'' as prefix to ensure superuser permissions.
The following commands need to be executed:
%
\leftaligned{\texttt{\$ \thinspace ./bootstrap.sh}}
%
\leftaligned{\texttt{\$ \thinspace ./b2 install --prefix=BPREFIX}}
%
In this 
command, \texttt{BPREFIX} is the directory where Boost should 
be installed. 

After downloading the latest release version of \dlvhex{},
the following sequence of commands \dlvhex{} will 
configure \dlvhex{}:
%
\leftaligned{\texttt{\$ \thinspace ./configure}} 
%
To enable the Python 
features of \dlvhex{}, \texttt{--enable-python} needs to be 
added as an additional parameter to \texttt{configure}.
%
If Boost was installed in a non-standard location,
the parameter \texttt{--with-boost=BPREFIX} also needs to be added.

After configuration, the following command builds the system:
%
\leftaligned{\texttt{\$ \thinspace make}} 
%
To allow using of multiple 
cores one should specify the \texttt{-jN} option to make 
use of N cores. Finally, 
%
\leftaligned{\texttt{\$ \thinspace make install}}
%
installs the package.
The installation location can be set to \texttt{HPREFIX}
by adding parameter \texttt{--prefix=HPREFIX} to \texttt{configure}.
   
\paragraph{Development version (git clone)}
The source code of \dlvhex{} is hosted on github at 
\url{https://github.com/hexhex/}. To get the latest 
development version it is necessary to clone the repository as 
follows:
%
\leftaligned{\texttt{\$ \thinspace
%
git clone 
https://github.com/hexhex/core --recursive}} 
After cloning it is necessary to 
execute the script \texttt{bootstrap.sh}.
%
\leftaligned{\texttt{\$ \thinspace ./bootstrap.sh}} 
%
After that, the steps from 
Section~\ref{sec:steps} (\texttt{configure}, \texttt{make}, and 
\texttt{make install}) should be followed to 
complete the installation.

We provide a script for installing \dlvhex{} 
automatically on Ubuntu systems:
\url{https://github.com/hexhex/core/blob/master/scripts/setupdlvhex.sh}.

Once installation is completed, \dlvhex{} can be used as follows:
%
\leftaligned{\texttt{\$ \thinspace dlvhex2 program.hex}} 
%
where \texttt{program.hex} refers to the input program.
Various additional command line options are available
and explained in Section~\ref{sec:commandline}.    

\subsubsection{Pre-built binaries}
Pre-built binaries of \dlvhex{} are available for some 
systems. For details see our website 
\url{http://www.kr.tuwien.ac.at/research/systems/dlvhex/}. 

\subsection{Outline}
This guide is organized as follows. Section~\ref{sec:quick} 
provides an introductory example including
problem instance, encoding and its solution.
Section~\ref{sec:inputLang} explains the input language of \dlvhex{}.
In Section~\ref{sec:examples} we 
introduce three real life problems which can be solved 
using \hex{}. Section~\ref{sec:externalInterfaces} is 
focused on the description of external interfaces which are 
written in C++ or Python. Input-related warnings and errors 
are described into more details in 
Section~\ref{sec:inputRelatedWarnings}.

\section{Quickstart} % Section No.2
\label{sec:quick}
As an introductory example, we consider a \emph{social 
graph} as used in social networks. Beginning from a 
simplified scenario, we stepwisely extend it to present 
various features of \dlvhex{}.

\subsection{Problem Setting}
A \emph{social graph} is a graph that represents 
interconnections among people, groups 
and organizations in a social network. Services such as 
Facebook facilitate the exchange 
of information, news, photographs, literary works, music, 
art, software, opinions or even 
money among users. 
Individuals and organizations, called actors, are nodes of 
the graph.
In this environment, the social graph 
for a particular actor consists 
of the set of nodes and edges which model other actors that 
are directly connected to that actor. 
Interdependencies, 
called ties, can be multiple and diverse, including 
characteristics or concepts such as age, 
gender, ethnical group, genealogy, chain of command, ideas, financial 
transactions, trade relationships, 
political affiliations, club memberships, occupation, 
education and economic status. 
Social graphs contain edges between one person and related 
people, places, and things they interact 
with online. For this particular example, we consider a 
simulation of social graphs as used, e.g., by Facebook. 

Consider the situation where a birthday party should be 
organized and a specific number of friends will be invited. 
The \emph{person $X$} who organizes the event wants to 
call his or her friends and friends of these friends up to 
some distance from the root node $X$. A \emph{depth 
constraint} specifies how many edges we can go away from 
the root node $X$.
 

We make use of an external source which returns for a given 
person all direct friends, while a direct access to the 
full graph is not available due to privacy issues imposed 
by social networks. Also, due to the large amount of data, 
importing the whole graph would be infeasible (billions of 
users), while only a small fraction is relevant for the 
application. Given a person $X$,
the external source retrieves all 
neighbour nodes (successor nodes). More details about the 
external source implementation are given in 
Section~\ref{sec:externalInterfaces}. 
               

\subsection{Encoding}
The problem can be modeled as a \hex{}-program as follows:
\begin{exmp}[\exampledownloadlink%
  {example_2_1/example_2_1.hex}{download example\_2\_1.hex}]
\label{faceQuery}
\begin{align*}
\rowprefix{r_1} & \mathit{personOfInterest}(\mathit{john}). \\
\rowprefix{r_2} & \mathit{friendOfDegree}(\mathit{P, 0, P}) 
  \leftimpl  \mathit{personOfInterest}(P). \\
\rowprefix{r_3} &
  \begin{array}[t]{@{}r@{\,}l}
  \mathit{friendOfDegree}(\mathit{P, DegPlus, F2}) \leftimpl 
    & \mathit{friendsOfDegree}(\mathit{P,Deg,F1)},\\
    & \ext{friendsOf}{F1}{F2},\\ 
    & \mathit{DegPlus = Deg + 1}, \\
    & \mathit{DegPlus < 2},\\
    & \mathit{\#int(DegPlus)}, \mathit{\#int(Deg)}.
  \end{array} \\
\rowprefix{r_4} & \mathit{invite(P)} \vee \mathit{ninvite(P) 
  \leftimpl  friendOfDegree(J,X,P), \#int(X).} \\
\rowprefix{r_5} & \leftimpl \nott \thinspace 4 = \mathit{\#count} 
  \{ P : \mathit{invite(P)} \}.
\end{align*}
\end{exmp}
% PS: TODO we could remove all #int here, they should not be required
% PS: TODO should we say something about the ":- not" pattern?
% PS: removed "john" in r_4 because we should use personOfInterest instead, but in this example we can also just use all discovered friends
The complete source code for this example is available at
\examplelink{example_2_1}.

Rule $\row{r_1}$ specifies the person who organizes the event 
and initializes the search.
Rule $\row{r_2}$ defines that the initiating person has 
distance 0 from him- or herself. 

The most interesting part of the program is rule $\row{r_3}$.
It cyclically defines friends of 
already known persons using an external atom
and increments the distance with each 
definition. Variables used in these predicates are: 

\begin{itemize}
\item $\mathit{F1}$ to represent the person for which we are 
looking for the successors

\item $\mathit{F2}$ is the variable for successor 
nodes of $F1$ 

\item $P$ represents the person of interest

\item $\mathit{Deg}$ and $\mi{DegPlus}$ are variables used to 
compute the distance from the root node
\end{itemize}
The external atom \ext{friendsOf}{F1}{F2} has one input and 
one output parameter. For input $\mathit{F1}$, 
it finds all successor nodes of $\mi{F1}$ and returns them in 
$\mathit{F2}$.
%
In other words, \ext{friendsOf}{F1}{F2} is true for all pairs
$(\mi{F1},\mi{F2})$ such that
$\mi{F2}$ is a direct friend of $\mi{F1}$ in the graph.
%
The implementation of the external atom is 
discussed in Section~\ref{sec:externalInterfaces}.
%
The atom
\begin{align*}
& \mathit{friendOfDegree}(P, Deg, F1)
\end{align*}
is true for all friends $\mi{F1}$ of $P$ that we already know;
it binds the variable $\mathit{F1}$ to a person for which we 
want to discover more successor nodes.
%
This value is used as input to 
the external source \ext{friendsOf}{F1}{F2} 
which returns all friends $F2$ of $F1$.
For each found friend $F2$ we define:
\begin{align*}
& \mathit{friendOfDegree}(P, \mi{DegPlus}, F2)
\end{align*} 
where $\mathit{DegPlus}$ is $\mathit{Deg}$ incremented by 
$1$ to represent that the distance to $F2$ is by $1$ 
greater than to $F1$. The condition
\begin{align*}
& \mathit{DegPlus} < 2
\end{align*}
ensures the distance is limited to 2. 

We now move to the part where we handle invitations. Rule $\row{r_4}$ guesses all possible 
persons to be invited or not. Since atom 
$\mathit{friendOfDegree(J, X, P)}$ is true for person $P$, that person will be either invited or not.

We limit the number of invited persons by using an 
\emph{integrity constraint} from the $\row{r_5}$
It ensures that exactly 4 persons are invited to the party. 

The combination of $\row{r_4}$ and $\row{r_5}$
can be replaced by a construction called `choice`
as shown in $\row{r_5}\prime$.
This rule also allows to specify lower and upper bound
on the number of persons independently.
\begin{align*}
\rowprefixprime{r_5} 3 \lesseq \{ invite(P) : \mi{friendOfDegree}(J,X,P) \} \lesseq 3.
\end{align*} 
% PS: TODO should we say something about expansion with :

\subsection{Problem Solution}
Now we are ready to solve our \emph{social graph} problem. 
Consider that we have the data as specified in the Figure~\ref{fig:socialnetwork}.
\begin{figure}
\begin{center}
\begin{tikzpicture}[yscale=0.5,xscale=0.8]
\tikzset{vertex/.style = {shape=rectangle,draw,minimum width=5.5em,minimum height=2em}}
\tikzset{edge/.style = {->,> = latex'}}
% vertices
\node[vertex] (a) at  (0,0) {$\mathit{John}$};
\node[vertex] (b) at  (4,5) {$\mathit{Mike}$};
\node[vertex] (c) at  (4,0) {$\mathit{Charly}$};
\node[vertex] (d) at  (4,-5) {$\mathit{David}$};
\node[vertex] (e) at (7,7) {$\mathit{Jenifer}$};
\node[vertex] (f) at (7,5) {$\mathit{Alex}$};
\node[vertex] (g) at (7,3) {$\mathit{Serena}$};
\node[vertex] (h) at (7,0) {$\mathit{Roger}$};
\node[vertex] (i) at (7,-3) {$\mathit{Chris}$};
\node[vertex] (j) at (7,-7) {$\mathit{Joe}$};
\node[vertex] (k) at (10,7) {$\mathit{Angel}$};
\node[vertex] (l) at (10,5) {$\mathit{Thomas}$};
\node[vertex] (m) at (10,3) {$\mathit{Carolina}$};
\node[vertex] (n) at (10,0) {$\mathit{Steve}$};
\node[vertex] (o) at (10,-3) {$\mathit{Mark}$};
\node[vertex] (p) at (10,-7) {$\mathit{Christopher}$};


%edges
%\draw[edge] (a) to node [auto] {2} (b);
\draw[edge] (a) to (b);
\draw[edge] (a) to (c);
\draw[edge] (a) to (d);
\draw[edge] (b) to (e);
\draw[edge] (b) to (f);
\draw[edge] (b) to (g);
\draw[edge] (c) to (h);
\draw[edge] (d) to (i);
\draw[edge] (d) to (j);
\draw[edge] (e) to (k);
\draw[edge] (f) to (l);
\draw[edge] (g) to (m);
\draw[edge] (h) to (n);
\draw[edge] (i) to (o);
\draw[edge] (j) to (p);
\end{tikzpicture}
\end{center}
\caption{Social Network Graph}
\label{fig:socialnetwork}
\end{figure}
To compute the answer sets representing 
the solution, \dlvhex{} should be invoked as follows:
%
\leftaligned{\texttt{\$ dlvhex2 --pythonplugin=example\_2\_1.py example\_2\_1.hex}}
%
where \texttt{example\_2\_1.hex} is \hex-program and 
\texttt{example\_2\_1.py} is the Python plugin which realizes
the external source implementation.
Details of the Python plugin interface
are given in Section~\ref{sec:externalInterfaces},
the files can be downloaded from
\exampledownloadlink{example_2_1/example_2_1.py}{example\_2\_1.py}
(the plugin)
and
\exampledownloadlink{example_2_1/example_2_1.edgelist}{example\_2\_1.edgelist}
(the graph in Figure~\ref{fig:socialnetwork}).

The output of \dlvhex{} is as follows:
\begin{align*}
   \{ &\mathit{personOfInterest(john), \ friendOfDegree(john,0,john), }\\
      &\mathit{invite(john), \ friendOfDegree(john,1,mike),}\\ 
      & \mathit{friendOfDegree(john,1,david), \ friendOfDegree(john,1,charly),} \\
      & \mathit{invite(mike), \ invite(david), \ invite(charly)}
       \}
 \end{align*}
Note that the order of the atoms and the order of answer sets 
does not bear any meaning. As we specified in the previous 
section, we can travel at most 1 edge far from the root 
node. Considering the graph given above only, $\mathit{John, 
Mike, Charly}$ and $\mathit{David}$ are found since they 
are at most one edge away from the root node. The next three atoms 
express who are the new friends discovered and at which 
depth 
level. For the invitations, it is specified by using 
aggregates that answer sets must have four distinct 
$\mathit{invites}$ atoms.
In the single answer set we have four $\mathit{invites}$ atoms 
which are $\mathit{invite(john), 
invite(mike), invite(david), invite(charly)}$. Note that 
this is the only answer set possible 
from this program because
there are only 4 distinct persons with depth level 1. 

If we allow the depth level to be larger there may be more 
answer sets found due to the fact that more nodes will be 
discovered. If we decrease the minimum number of friends to be 
invited to the party there may also be more than one answer set. 
Consider the different example where instead of 4 
persons we want to invite only 3 persons to the party. 
The integrity constraint at $\row{r_5}$ will be modified to:
\begin{align*}
& \rowprefixprimeprime{r_5} \leftimpl \nott \thinspace \mathit{\#count} \{ P : \mathit{invite(P)} \} = 3.
\end{align*} 
 This time we have more than one answer set. Since the depth 
 level is still 2 there will be 4 persons discovered again, 
 however, out of these 4 persons we have to invite only 
 three of them and one of them will not be invited. 
 According to this we have 4 answer sets. Two of them are 
 shown below:
\begin{align*}
   \{ &\mathit{personOfInterest(john), 
      friendOfDegree(john,0,john),}\\
      &\mathit{invite(john), friendOfDegree(john,1,mike), 
      \mathit{ninvite(charly)},}\\
      &\mathit{friendOfDegree(john,1,david), 
      friendOfDegree(john,1,charly),}\\
      &\mathit{invite(mike),invite(david)}  \} \\
   \{&\mathit{personOfInterest(john), 
   friendOfDegree(john,0,john),} \\
   &\mathit{invite(john), friendOfDegree(john,1,mike), 
   \mathit{ninvite(mike)},}\\
   &\mathit{friendOfDegree(john,1,david), 
   friendOfDegree(john,1,charly),} \\
   &\mathit{invite(david),invite(charly)}\}
 \end{align*}
(Again, note that the order of answer sets is arbitrary
and does not bear any meaning.)
%
This time in the answer set we have 
$\mathit{ninvite(charly)}$ and $\mathit{ninvite(mike)}$ 
since one friend must be discarded and only three will be 
invited. One can experiment with the \emph{depth constraint} and 
\emph{aggregate atom} to see how the output and 
answer sets will be affected.    

\section{Input Language}% Section No. 3
\label{sec:inputLang}
This section provides an overview of the input language of 
\dlvhex{} and some examples to illustrate the concepts. 

\subsection{Terms and Atoms}
The vocabulary consists of terms, constants, variables and 
external predicates. Terms may be integers, constants, function terms, 
strings and variables as well as the \enquote{\_} token. 
Constant names begin with lowercase letters or are strings 
enclosed in quotation marks.
Variable names begin with uppercase letters.

Function terms (uninterpreted functions)
are \emph{complex terms} composed of a name
(like a constant) and one or more terms as arguments.
For instance,
$\mathit{at(john,t(10),X)}$ is a function term with three arguments:
constant $\mathit{john}$,
another function term $\mathit{t(12})$ with an integer argument,
and variable $X$ \cite{gkklorst2015}.

While a constant, function term, or string,
always represents itself; a variable is a
placeholder for all variable-free terms in the language of 
a logic program. 
An anonymous variable is a special variable
denoted by \enquote{\_} (the underscore):
each occurrence of \enquote{\_} represents 
a new and unique variable which does not occur anywhere 
else in the same rule. This might be used to specify that 
an argument can be ignored or does not matter.
%(for example the atom $p(1,2)$ contains a different predicate than $p(1)$,
%hence if we want to ignore the second argument we must write $p(1,\_)$).

An \emph{atom} has the form $\mathit{p(t_1,\dots,t_n)}$ where 
$p$ is a predicate name, $t_1,\dots,t_n$ are terms and $n \,{<}\, 0$
is the arity of the predicate $p$;
an atom $p()$ of arity 0 is usually written as $p$ without parentheses.
Atoms can be classically negated using \enquote{$\clasneg$},
yielding $q$ and $\clasneg q$.
\begin{exmp}
The following example illustrates the above concepts.

\begin{center}
\begin{tabular}{ll}
Constants:  & $a$, $1$, $\mathit{a1}$, 
  $\mathit{9862}$, $\mathit{c1}$, ''hello'' \\
Variables:  & $X$, $Y$, $Z$ \\
Atoms:      & $\mathit{parent}(X,Y)$, $\mathit{employee}
  (name, salary, ID, location)$ \\
Predicates: & $\mathit{parent}$, $\mathit{employee}$
\end{tabular}
\end{center}
\end{exmp}


\subsection{Normal Programs and Integrity Constraints}
A \hex{}-program is constructed using \emph{facts, rules 
and integrity constraints}. 

\begin{center}
\begin{tabular}{ r l@{}r }
Fact:      & \texttt{$A_0$}. & \\
Rule:      & \texttt{$A_0$}& $\leftimpl$  \texttt{$L_1$},\dots, \texttt{$L_n$}. \\
Constraint:&& $\leftimpl$  \texttt{$L_1$},\dots, \texttt{$L_n$}. 
\end{tabular}
\end{center}
The sign \enquote{$\leftimpl$} is meant to be an 
implication to the left ($\leftarrow$).
The left side of a rule is called 
its head, and its right side is called body. The head 
\texttt{$A_0$} of a rule or a fact is an atom. In the body of a 
rule or an integrity constraint,
every \texttt{$L_j$}, $1 \les j \les n$,
is a literal of the form $\mathit{A}$ or 
$\nott A$, where $A$ is an atom and the 
connective $\nott$ denotes default negation. We say 
that literal $L$ is positive if it is an atom and 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 atoms 
in the rule body are true and negated atoms are false, then 
the head $A_0$ must be true. On the other hand, an integrity 
constraint is a rule that filters solution candidates: 
the literals in its body must not jointly be 
satisfied.
A result of a \dlvhex{} computation is called an 
\emph{answer set} which is a consistent explanation (model) 
of the world
given the knowledge about the world represented by rules
as intuitively explained above.

We here give only informal semantics;
for a formal description of semantics of normal ASP programs and \hex{}-programs
we refer to \cite{gekakasc12a} and \cite{efikrs2015}, respectively.

\begin{exmp} 
Consider the following logic program:
\begin{align*}
\rowprefix{r_1}&\mathit{ joke }. \\
\rowprefix{r_2}&\mathit{ laugh }  \leftimpl \mathit{ joke }.
\end{align*} 
The first line here represents an \emph{atom} which is 
always true. The second line is a \emph{rule} and reads as 
\enquote{If $\mathit{joke}$ is true, $\mathit{laugh}$ must 
also be true}. Also we can read this as \enquote{from 
$\mathit{joke}$ follows $\mathit{laugh}$}. The single 
\emph{answer set} of the program above is $\{\mathit{joke}, 
\mathit{laugh}\}$ since they are the atoms which are true 
in the program. 
\end{exmp}
 
Another important feature of \dlvhex{} is \emph{default 
negation} which is also called ``negation as failure". 
Intuitively, negation as failure means:
if we cannot show truth of an atom,
then we may safely assume that it is false.

Variables in default negated atoms must be safe
which means that they must also occur in a positive atom
in the body of the same rule.

\begin{exmp}
With default negation we can represent the 
complementary graph $\mi{comp\_edge}(X,Y)$
of a graph given as atoms $\mi{edge}(X,Y)$.
The complementary graph has the same nodes as the original graph,
but of all possible edges it has exactly those edges,
which do not exist in the original graph.
\begin{align*}
\rowprefix{r_1}& \mathit{node}(X) \leftimpl \mathit{edge}(X, \_).  \\
\rowprefix{r_2}& \mathit{node}(Y) \leftimpl \mathit{edge}(\_, Y).  \\
\rowprefix{r_3}& \mathit{comp\_edge}(X, Y) \leftimpl 
  \mathit{node}(X), \mathit{node}(Y),
  \nott \thinspace \mathit{ edge }(X, Y). 
\end{align*}
Note that $\mathit{node}(X)$ and $\mathit{node}(Y)$ 
are included in the body to satisfy the 
safety requirement for variables $X$ and $Y$.
Also note the anonymous variables \enquote{$\_$}.
\end{exmp}

Default negation allows for generating multiple answer sets
that are equally correct as models of a single program.
%
Integrity constraints eliminate those answer set candidates
that make the body of the constraint true.
\begin{exmp}
Consider the following example for coloring nodes of a graph
either red, green or black. 
\label{nodecoloring}
\begin{align*}
\rowprefix{r_1} & \mathit{node}(X) \leftimpl \mathit{edge}(X, Y).  &\\
\rowprefix{r_2} & \mathit{node}(Y) \leftimpl \mathit{edge}(X, Y).  & \\
\rowprefix{r_3} & \mathit{colored}(X, r) \leftimpl \mathit{node}(X), \nott \  colored(X,g), \nott \ colored(X,b). & \\
\rowprefix{r_4} & \mathit{colored}(X, g) \leftimpl \mathit{node}(X), \nott \  colored(X,r), \nott \ colored(X,b). & \\
\rowprefix{r_5} & \mathit{colored}(X, b) \leftimpl \mathit{node}(X), \nott \  colored(X,r), \nott \ colored(X,g). & \\[1ex]
\rowprefix{r_6} & \leftimpl \mathit{edge}(X, Y), \mathit{colored}
(X, C), \mathit{colored}(Y, C). & \\[1ex]
\rowprefix{r_7} & \mathit{edge}(2, 4). \  \mathit{edge}(2, 3). \  
\mathit{edge}(5, 5). & \\
\rowprefix{r_8} & \mathit{edge}(4, 6). \  \mathit{edge}(4, 5). \ 
\mathit{edge}(5, 7). & \\
\rowprefix{r_9} & \mathit{edge}(6, 7). &
\end{align*} 
In the first two rules we extract the nodes
implicitly given by the edges of the graph.
Rules \row{r_3}-\row{r_5} describe a \emph{guess}
such that for each node $X$,
either $\mi{colored}(X,r)$, $\mi{colored}(X,g)$, or $\mi{colored}(X,b)$
will be true in answer sets.
These three rules generate all possible node color combinations.
Rule \row{r_6} is a constraint, sometimes called \emph{check},
that
deletes all color combinations which do not satisfy the 
requirement that there may be no edge between two nodes of 
equal color.
\end{exmp}

\subsection{Classical Negation}
\dlvhex{} supports two kinds of negation. Here we will 
emphasize the difference between explicitly expressing 
falseness of an atom and having it done by 
negation as failure.
The connective $\nott$ expresses 
default negation, i.e. a literal $\nott \thinspace A$ is assumed 
to hold unless atom $A$ is derived to be true.
This is also called \emph{Closed World Assumption}.
In contrast, 
the classical (or strong) negation of an atom holds only if 
it can be derived. In other words if there is no evidence 
that an atom is true, it is considered to be false. 
Classical negation \enquote{$\clasneg$} is 
permitted in from of an atom. The semantic relationship 
between $A$ and $\clasneg\mathit{A}$ is simply that they must not jointly 
hold.

\begin{exmp} 
Imagine a situation where an agent has to cross a railroad. 
The agent should cross it if there is no train approaching. 
With this description, one might specify the following 
program:
\begin{align*}
 \rowprefix{r_1}& \mathit{cross\_railroad} \leftimpl \nott \mathit{ train\_approaches}.
\end{align*}
This program has the answer set 
\{$\mathit{cross\_railroad}$\} because 
$\mathit{train\_approaches}$ is assumed to be false (as it 
being true is not stated anywhere). This kind of negation 
is called \emph{negation as failure}.
\end{exmp}
\begin{exmp}
Imagine, instead, that we use the following program
which uses classical negation (sometimes called strong or true negation). 
\begin{align*}
\rowprefix{r_1}\mathit{cross\_railroad} \leftimpl \ \clasneg \mathit{train\_approaches}.
\end{align*}
Since $\clasneg\mathit{train\_approaches}$ is not known to be 
true, the program has only an empty answer set.
\end{exmp}

Note the difference between the two kinds of negation:
in the first example, the railroad track is 
crossed if there is no information on any trains 
approaching;
while in the second example, it is only crossed if
we can prove that no train comes.
In that sense classical negation is stronger
than negation as failure.

\subsection{Disjunctive Programs}
\label{disjunction}
Disjunctive logic programs permit the connective ``$\vee$" 
between atoms in rule heads.
\begin{center}
\begin{tabular}{ r l l}
  \text{Fact:} & $A_0$ $\vee$ \dots $\vee$ $A_m$. \\
  \text{Rule:} & $A_0$ $\vee$ \dots $\vee$ $A_m$ 
  $\leftimpl$ $L_1,\dots,L_n. $ \\
 \end{tabular}
\end{center}
A \emph{disjunctive head} holds if at least one of its 
atoms is true. If all body literals $L_1,\dots,L_n$ of the 
rule specified above are known to be true then the head also needs to hold, i.e. one of the atoms in $A_0$ $\vee$ \dots 
$\vee$ $A_m$ needs to be true.
If our program just contains the fact 
\enquote{$\mathit{a} \vee \mathit{b}$}
we obtain two answer sets \{$a$\} and \{$b$\}.

Disjunctive logic programs intuitively make
the minimum of disjunctive heads true
that are necessary to satisfy all constraints to obtain an answer set.
%
Formally speaking semantics are not that simple:
disjunctive programs have a higher expressive power
than normal logic programs
(it is possible to encode subset minimality
using advanced techniques such as \emph{saturation}
that we will not discuss further in this manual).

\begin{exmp}
In the Example~\ref{nodecoloring} we could replace
the guess in \row{r_3}-\row{r_5}
by the following single disjunctive rule:
\begin{align*}
\mathit{colored(X,r)} \vee \mathit{colored(X,g)} \vee \mathit{colored(X,b)} \leftimpl \mathit{node(X).}
\end{align*}
This generates all possible node color combinations.
\end{exmp}

\begin{exmp}
Suppose we met a friend recently and know that he had one 
of his arms broken, but do not know which one. Now suppose 
we did not receive a greeting card for your birthday and 
wonder if you should be angry on him or he just could not 
write because his right hand is broken. 
Suppose that we encode this reasoning problem in \hex.
\begin{align*}
\rowprefix{r_1}& \mathit{left\_arm\_broken} \vee 
\mathit{right\_arm\_broken}.\\
\rowprefix{r_2}& \mathit{can\_write} \leftimpl 
\mathit{left\_arm\_broken}.\\
\rowprefix{r_3}& \mathit{be\_angry} \leftimpl 
\mathit{can\_write}.
\end{align*}
For this program,
\dlvhex{} will generate two possible explanations. The 
first rule is called a disjunctive rule which is read as 
\enquote{For sure, either the left or the right arm is broken.} Without being sure which arm is broken \dlvhex{} 
will evaluate the program and produce the two models 
$\mathit{\{left\_arm\_broken, can\_write, be\_angry\}}$ and 
$\mathit{\{right\_arm\_broken\}}$.
\end{exmp}

\subsection{Built-in Arithmetic Functions}
%Besides integers
%(constant arithmetic functions), written 
%as sequence of digits $0$,\dots,$9$,
\dlvhex{} supports 
integers and the following arithmetic operators:
%following operators for those functions: 
$+$ (addition), $-$ (subtraction),
$*$ (multiplication), and $/$ (integer division). 
Atom $+(X,Y,Z)$ is true,
iff $Z$ is the sum of $X$ and $Y$
and likewise for other operators.

Alternatively to \emph{prefix notation} one can also use 
\emph{infix notation} to use built-in arithmetic functions 
in \dlvhex{}. For instance $\mathit{+(X, Y, Z)}$ 
alternatively can be written as $\mathit{Z=X+Y}$. 

\begin{exmp}
Suppose the following program.
\begin{align*}
&\rowprefix{r_1} \ \mathit{a}(6). \\
&\rowprefix{r_2} \ \mathit{b}(2). \\
&\rowprefix{r_3} \ c(X,Y,Z) \leftimpl a(X), b(Y),+(X, Y, Z). \\
&\rowprefix{r_4}  \ d(X,Y,Z) \leftimpl a(X), b(Y),-(X, Y, Z). \\
&\rowprefix{r_5} \ e(X,Y,Z) \leftimpl a(X), b(Y),*(X, Y, Z). \\
&\rowprefix{r_6} \ f(X,Y,Z) \leftimpl a(X), b(Y),/(X, Y, Z).
\end{align*}
The single answer set for the example above is:
\begin{align*}
\{a(6),b(2),e(6,2,12),f(6,2,3),c(6,2,8),d(6,2,4)\}.
\end{align*}
The infix alternatives of rules \row{r_3}-\row{r_6} above are as follows.
\begin{align*}
&\rowprefixprime{r_3} c(X,Y,Z) \leftimpl a(X), b(Y),Z=X+Y. \\
&\rowprefixprime{r_4} d(X,Y,Z) \leftimpl a(X), b(Y),Z=X-Y. \\
&\rowprefixprime{r_5} e(X,Y,Z) \leftimpl a(X), b(Y),Z=X*Y. \\
&\rowprefixprime{r_6} f(X,Y,Z) \leftimpl a(X), b(Y),Z=X/Y.
\end{align*}
\end{exmp}

\subsection{Built-in Comparison Predicates}

\dlvhex{} features a total order among variable-free terms 
using built-in predicates $==$ (equal), $\noteq$ or $\noteqq$ (not equal), 
$<$ (less than), $\lesseq$ (less than or equal), $>$ (greater 
than) and $\geeq$ (greater than or equal).
All ground terms and integers can be compared this way.
Integer comparison is according to numeric values. All other 
comparisons just guarantee a fixed ordering 
over all terms.
\begin{exmp}
Suppose we have the following program.
\begin{align*}
\rowprefix{r_1}& a(1). \\
\rowprefix{r_2}& a(2). \\
\rowprefix{r_3}& b(1). \\[1ex]
\rowprefix{r_4}& c(X,Y) \leftimpl a(X), b(Y), X \noteq Y. \\
\rowprefix{r_5}& d(X,Y) \leftimpl a(X), b(Y), X \noteqq Y. \\
\rowprefix{r_6}& e(X,Y) \leftimpl a(X), b(Y), X < Y. \\
\rowprefix{r_7}& f(X,Y) \leftimpl a(X), b(Y), X > Y. \\
\rowprefix{r_8}& g(X,Y) \leftimpl a(X), b(Y), X \lesseq Y. \\
\rowprefix{r_9}& h(X,Y) \leftimpl a(X), b(Y), X \geeq Y. \\
\rowprefix{r_{10}}& i(X,Y) \leftimpl a(X), b(Y), Y == 1. 
\end{align*}
The single answer set this program is
\begin{align*}
\{ & a(1),a(2),b(1),i(1,1),i(2,1),c(2,1),\\
   & d(2,1),f(2,1),g(1,1),h(1,1),h(2,1)\}.
\end{align*}
\end{exmp}

\subsection{Conditions and Conditional Literals}
\label{conditions}
A \emph{conditional literal} is of the form 
\mycenterline{$L_0:L_1,\dots,L_n$}%
where every $\mathit{L_j}$ 
with $0 \les j \les n$ is a literal,
the literals $L_1,\dots,L_n$ are called \emph{condition},
and \enquote{:} resembles the vertical bar ($\mid$)
in mathematical set notation.
%Whenever $\mathit{n = 0}$, it is 
%a regular literal and we denote it usually by $L_0$.
The condition is expanded into all ground versions of $L_0$
where the condition is true.
%
For example, the rule $\mathit{a \leftimpl b : c.}$ yields 
$a$ whenever either $c$ is false (whether $b$ holds or not) 
or both $b$ and $c$ are true.
%Logically, $L_0$ and $L_1$,
%\dots,$L_n$ act as head and body, respectively, which gives 
%$L_0$:$L_1$,\dots,$L_n$ the flavour of a nested implication 

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 \cite{gkklorst2015}. 

\begin{exmp}
Consider the following program for scheduling a meeting \cite{gkklorst2015}.
\begin{align*}
\rowprefix{r_1}& \mathit{person}(\mathit{jane}). \  \mathit{person}
(\mathit{john}).\\
\rowprefix{r_2}& \mathit{day}(\mathit{mon}). \ \mathit{day}
(\mathit{tue}). \ \mathit{day}(\mathit{wed}). \ \mathit{day}
(\mathit{thu}). \ \mathit{day}(\mathit{fri}). \ \\
\rowprefix{r_3}& \mathit{available}(\mathit{jane}) \leftimpl \nott \thinspace  
\mathit{on}(\mathit{fri}).\\
\rowprefix{r_4}& \mathit{available}(\mathit{john}) \leftimpl 
\nott \thinspace \mathit{on}(\mathit{mon}), \nott \thinspace \mathit{on}(\mathit{wed}).\\
\rowprefix{r_5}& \mathit{meet} \leftimpl \mathit{available}(X) : 
\mathit{person}(X).\\
\rowprefix{r_6}& \mathit{on}(X) : \mathit{day}(X) \leftimpl 
\mathit{meet}.
\end{align*}
Conditions are used in \row{r_5} and \row{r_6}.
%
The \emph{conjunction} in \row{r_5} is instantiated by 
replacing $X$ in $\mathit{available(X)}$ with all ground 
terms $t$ such that $\mathit{person(t)}$ holds, namely
$\mathit{X=jane}$ and $\mathit{X=john}$.
%
The condition in $\row{r_6}$ is contained in the head of the rule
and turns into a \emph{disjunction} over all ground instances of 
$\mathit{on(X)}$ such that $X$ is substituted by terms $t$ 
for which $\mathit{day(t)}$ holds, i.e.,
whenever $\mathit{meet}$ holds,
one of $\mathit{on(t)}$ for which $\mathit{day(t)}$ is true should hold.

This program has the following two answer sets.
\begin{align*}
  \{ & \mi{meet,on(tue),day(mon),day(tue),day(wed),day(thu),day(fri),}  \\
     & \mi{person(jane),person(john),available(jane),available(john)}\} \\
  \{ & \mi{meet,on(thu),day(mon),day(tue),day(wed),day(thu),day(fri),}  \\
     & \mi{person(jane),person(john),available(jane),available(john)}\}
\end{align*}
\end{exmp}

%PS: this is too much information, anyways this is also in the potassco guide
%Consider that except $\mathit{on(X)}$ we have also an atom $\mathit{travel(X)}$. These two atoms are separated with a ``;'' sign, the rule would look like:
%\mycenterline{\{$\mathit{on}(X);\mathit{travel}(X) : \mathit{day}(X)\} \leftimpl 
%\mathit{meet}.$}
%where for all ground instances of $\mathit{on(X)}$ and $\mathit{travel(X)}$ such that $X$ is substituted by terms $t$ for which $\mathit{day(t)}$ holds. 
%
%Any variable occurring 
%within a condition does not count as a positive occurrence 
%outside the condition in the sense of safety. A variable 
%$X$ in an aggregate-free rule is safe if at least one of 
%the safety conditions specified in Section~\ref{safetyCheck} is satisfied.
%Variables occurring in atoms not subject to any conditions 
%are 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. During grounding, the 
%instantiation of global variables take 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 \cite{gkklorst2015}.    

\subsection{Aggregates}
\label{aggregates}
Aggregates allow to express properties over sets of 
elements. \hex{}-programs with aggregates often allow clean 
and concise problem encodings by minimizing the use of 
auxiliary predicates and recursive programs, and help the 
programmers to depict problems in a more natural way. For 
instance, we may state that the sum of a semester's course 
credits must be at least 20, or that the sum of shopping 
items must not exceed 30 Euros. We can say that 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.
Aggregates can occur in the bodies of rules and constraints, 
possibly negated using negation-as-failure \cite{gkklorst2015}.
%
The form of an \emph{aggregate atom} is as follows:
\begin{align*}
s_1 \prec_1 \alpha \{ t_1, \dots, t_n : L_1, \dots, L_m\} \prec_2 s_2
\end{align*}
where $\mathit{t_i}$ are terms,
$\mathit{L_i}$ are literals,
$\alpha$ is a function that evaluates the numerical value of the aggregate,
and $\prec_1$/$\prec_2$ are comparison predicates 
that compare the resulting value with the terms $s_1$/$s_2$. 
%
An aggregate is true if the comparison is true
with respect to evaluating $\alpha$ on those tuples $t_1,\ldots,t_n$
for which $L_1,\ldots,L_m$ in the aggregate body is true.

Supported aggregate functions $\alpha$ are
$\mathit{\#count}$, $\mathit{\#sum}$, $\mathit{\#times}$, 
$\mathit{\#min}$, and $\mathit{\#max}$.
% PS: let's only explain on an example, there is the potassco guide
%An aggregate function is applied over a set and 
%returns a numeric value. Let $f(S)$ be an aggregate 
%function. A variable, X, is a \emph{local variable} to 
%$f(S)$ if and only if $X$ appears in $S$ and $X$ does not 
%appear in any aggregate function that is outside of $f(S)$.

\begin{exmp}
Consider the following program
where we want to count how many employees of the company
earn more than 1000. 
\begin{align*}
\rowprefix{r_1}& \mi{emp(1,goofie,1250)}.\\
\rowprefix{r_2}& \mi{emp(2,willy,750)}.\\
\rowprefix{r_3}& \mi{emp(3,woody,750)}.\\
\rowprefix{r_4}& \mi{emp(4,jerry,900)}.\\
\rowprefix{r_5}& \mi{emp(5,tom,1050)}. \\
\rowprefix{r_6}& \mi{over1000}(I,S) \leftimpl \mi{emp}(I,N,S), S > 1000.\\
\rowprefix{r_7}& \mi{over1000nr}(X) \leftimpl
  \mi{\#count}\{I : \mi{over1000}(I,W)\} = X, \mi{\#int}(X).
\end{align*}
Intuitively the aggregate is expanded into
\begin{align*}
\#count\{over1000(1,1250),over1000(5,1050)\}
\end{align*}
and the (symbolic) set of tuples $I$
appearing in the aggregate looks as follows:
\begin{align*}
\{\langle 1 \rangle,\langle 5 \rangle\}.
\end{align*}
The aggregate function $\mathit{\#count}$ returns the 
cardinality of the symbolic set to which it is applied,
in this case it returns $2$.

As a result this program has the following unique answer set.
\begin{align*}
\{ & \mathit{emp(1,goofie,1250),emp(2,willy,750),emp(3,woody,750),}\\
   & \mathit{emp(4,jerry,900),emp(5,tom,1050),}\\
   & \mathit{over1000(1,1250),over1000(5,1050),over1000nr(2)} \}
\end{align*}
\end{exmp}

Aggregate functions get as input the set of tuples from the aggregate
and they operate on the first item of these tuples.
\begin{exmp}
Suppose we want to know how much the company spends on salaries,
then we can use the following rule.
\begin{align*}
  \mathit{\rowprefix{r_8} \ salaryTotal(X)} \leftimpl
    \mathit{\#sum}\{S,I : \mathit{emp(I,N,S)}\} = X.
\end{align*}
The symbolic set for the rule $\row{r_8}$ consists of 5 elements: 
\begin{align*}
  \{ & \langle 1250,1 \rangle, \langle 750,2 \rangle,
    \langle 750,3 \rangle, \langle 900,4 \rangle, \langle 1050,5 \rangle\}.
\end{align*}
The $\mi{\#sum}$ function returns
the sum over the first elements of all tuples in the set,
therefore the answer set contains the fact $\mathit{salaryTotal(4700)}$.

Note that the first term in the tuple is the salary $S$,
but we need also the second term $I$ in order to get the correct result:
consider the simplified rule
\begin{align*}
  \mathit{\rowprefix{r_8'} \ salaryTotal(X)} \leftimpl
    \mathit{\#sum}\{S : \mathit{emp(I,N,S)}\} = X.
\end{align*}
without $I$: the symbolic set with \row{r_8'} looks as follows.
\begin{align*}
  \{ \langle 1250 \rangle, \langle 750 \rangle,
  \langle 900 \rangle,  \langle 1050 \rangle\}
\end{align*}
It contains only one element for both employees with salary $750$,
therefore
we obtain the incorrect result $\mathit{salaryTotal(3950)}$.  
\end{exmp}
 
The aggregate function $\mathit{\#times}$ computes the product of 
the first values of tuples in the symbolic set.
When applied over the empty set, 
$\mathit{\#times}$ returns 1.
%
The aggregate function $\mathit{\#min}$ (resp., $\mi{\#max}$) returns 
the minimum (resp., maximum) value
of the first values of tuples in the symbolic set.
%
%PS: imho we already have enough examples
%The following rule then returns the lowest income among all employees.
%\begin{align*}
%& lowest(X) \leftimpl \#min\{S : emp(I,N,S)\} = X.
%\end{align*}
%
%The aggregate function applied to the given set returns the 
%minimum salary among of all the employees, the output thus 
%is:
%{$\mathit{lowest(750)}$}.
%
%The following program 
%computes the maximum income earned in the company
%\begin{align*}
%& \mathit{highest}(X) \leftimpl \mathit{\#max}\{S : 
%\mathit{emp}(I,N,S)\} = X.
%\end{align*}
%
%and it outputs $\{highest(1250)\}$ as a highest income in 
%the company.
%
Note that one aggregate body can contain multiple symbolic set constructors 
of form $t_1, \dots, t_n \colon L_1, \ \dots,L_m$
by separating them using \enquote{;}. 

\subsection{Optimization}
\label{optimize}
Introducing \emph{weak constraints} into \hex-programs 
allows us to formulate several optimization problems in an 
easy and natural way.
%These weak constraints have been adopted 
%from \emph{DLV}.
While standard constraints (integrity 
constraints, strong constraints) always have to be 
satisfied, weak constraints can be satisfied
\emph{at a cost}
and the answer sets of a program $P$ with a set $W$ of weak 
constraints are those answer sets of $P$ which minimize the 
cost of violated weak constraints.

Weak constraints can be weighted according to their 
importance (the higher the weight, the more important the 
constraint). In the presence of weights, best models 
minimize the sum of the weights of the violated weak 
constraints. Weak constraints can also be prioritized. 
Under prioritization, the semantics minimizes the violation 
of the constraints of the highest priority level first; 
then the lower priority levels are considered one after the 
other in descending order.

Weak constraints 
are specified as follows.
\begin{align*}
\weakimpl \mathit{b_1,\dots,b_n}.
\quad [\mathit{w}@\mathit{l},\mathit{t_1,\dots,t_m}] 
\end{align*}
As in aggregates,
$\mathit{t_1,\dots,t_m}$, $m \gts 0$, are terms that specify a symbolic set
over which the cost of constraint violations is computed.
%
As in a normal rule, $\mathit{b_1,\dots,b_n}$, $n \gts 0$,
are literals,
and $w$ and $l$ are terms standing for a \emph{weight} and a \emph{level}.
%
If omitted, the level defaults to 0.
%Writing the part ``$\mathit{@l}$'' can optionally be ommited if $l=0$; that is, a weak constraint has level 0 unless specified otherwise \cite{cffiklrs2013}.

\begin{exmp}
Consider we want to compute the minimum spanning trees 
of a weighed directed graph.
\begin{align*}
\rowprefix{r_1}& \mathit{root}(a). \\
\rowprefix{r_2}& \mathit{node}(a). \ \mathit{node}(b). \ 
  \mathit{node}(c). \ \mathit{node}(d). \ \mathit{node}(e). \ \\
\rowprefix{r_3}& \mathit{edge}(a,b,4). \ \mathit{edge}(a,c,3). \ 
  \mathit{edge}(c,b,2). \ \mathit{edge}(c,d,3). \ \\
\rowprefix{r_4}& \mathit{edge}(b,e,4). \ \mathit{edge}(d,e,5). \ \\[1ex]
\rowprefix{r_5} & \mathit{in\_tree}(X,Y,C) \vee 
  \mathit{out\_tree}(X,Y) \leftimpl \mathit{edge}(X,Y,C), 
  \mathit{reached}(X). \\
\rowprefix{r_6}& \leftimpl \mathit{root}(X), \mathit{in\_tree} (\_,X,C).\\
\rowprefix{r_7}& \leftimpl \mathit{in\_tree}(X,Y,C), 
  \mathit{in\_tree}(Z,Y,C), X \noteq Z. \\[1ex]
\rowprefix{r_8}& \mathit{reached}(X) \leftimpl \mathit{root} (X). \\
\rowprefix{r_9}& \mathit{reached}(Y) \leftimpl 
  \mathit{reached}(X), \mathit{in\_tree}(X,Y,C). \\
\rowprefix{r_{10}}& \leftimpl \mathit{node}(X), \nott \thinspace 
  \mathit{reached}(X). \\[1ex]
\rowprefix{r_{11}}&\mathit{ : \sim in\_tree}(X,Y,C). [C@1,X,Y,C]
\end{align*}
The fact $\row{r_1}$ of the example above defines the root node 
of a tree. Nodes and edges are defined in $\row{r_2}$ and $\row{r_3}$. 
Rule $\row{r_5}$ guesses for each edge from node 
$X$ to a node $Y$ (node $X$ is already reached) whether it is in the minimum spanning 
tree or out of it. The integrity constraint $\row{r_6}$ ensures 
that there is no incoming edge to the root node. Rule $\row{r_7}$ 
eliminates all answer sets where there are two outgoing 
edges going to the same node $Y$. In $\row{r_8}$ and $\row{r_9}$ 
we compute all reached nodes and $\row{r_{10}}$ removes all answer sets where there is some node 
which is not reached.

Rule $\row{r_{11}}$ is a weak 
constraint with weight $C$ and level 1.
Intuitively this constraint says that using an edge
has a cost corresponding to the weight of the edge.
As a consequence, minimizing cost of the answer set
will find a tree starting at the root node
reaching all nodes with minimal cost,
i.e., a minimal spanning tree.

The best answer set has cost 12 at level 1 and is as follows
(omitting facts).
\begin{align*}
\{ & \mi{reached(a), reached(b), reached(c), reached(d), reached(e)}, \\
   & \mi{out\_tree(a,b), out\_tree(d,e)}, \\
   & \mi{in\_tree(a,c,3), in\_tree(b,e,4), in\_tree(c,b,2), in\_tree(c,d,3)}\} 
   % \ \ Cost ([Weight:Level]): <[12:1]>
\end{align*}
The complete source code for this example is available at
\exampledownloadlink{example_3_opti/example_3_opti.hex}{example\_3\_opti.hex}.
%The source code for this example is available at \examplelink{example_3_opti}.

To obtain all optimal answer sets execute the following command.
\leftaligned{\texttt{ \$ dlvhex2 \ example\_3\_opti.hex}}

To obtain all answer sets, even non-optimal ones execute the following.
%
\leftaligned{\texttt{ \$ dlvhex2 \ example\_3\_opti.hex \ --weak-allmodels}}
\end{exmp}

More examples can be found in the DLV-User Manual \cite{brfwilvpg2009}.

\dlvhex{} supports two evaluation algorithms for weak constraints. The way they work has some implications on the runtime performance as well as memory characteristics. The default algorithm usually performs better, but may consume more memory. If the evaluation fails because of a memory shortage, one can try and rerun \dlvhex{} with the parameter \texttt{--heuristics=monolithic}. With this parameter, the second algorithm is used, which consumes less memory.

\nop
{
Finally, we show an example where both weights and 
priorities are specified. This example and some others are 
taken from the DLV-User Manual \cite{brfwilvpg2009}. Consider the 
problem of assigning a given set of employees to two 
projects. As a minor desideratum, we wish that members of 
the same group already know each other. Higher level 
constraints ask each group to be heterogeneous as far as 
skills are concerned, and require that people married with 
one another do not work in the same group.
\begin{exmp}
\begin{align*}
\rowprefix{r_1}& \mathit{employee}(a). \ \mathit{employee}(b). \ 
\mathit{employee}(c). \ \mathit{employee(d)}. \ \\
\rowprefix{r_2}& \mathit{employee}(e). \\
\rowprefix{r_3}& \mathit{know}(a,b). \ \mathit{know}(b,c). \ 
\mathit{know}(c,d). \ \mathit{know}(d,e). \ \\
\rowprefix{r_4}& \mathit{same\_skill}(a,b). \\
\rowprefix{r_5}& \mathit{married(c,d)}. \\
\\ 
\rowprefix{r_6}& \mathit{mbr}(X,p1) \vee \mathit{mbr}(X,p2) 
\leftimpl \mathit{employee}(X).\\
\rowprefix{r_7}& :\sim \mathit{mbr}(X,P), \mathit{mbr}
(Y,P), X \noteq Y, \nott \thinspace \mathit{know(X,Y)}. \thinspace [1@1, X,Y,P]\\
\rowprefix{r_8}& : \sim \mathit{mbr}(X,P), \mathit{mbr}
(Y,P), X \noteq Y, \mathit{married}(X,Y). \thinspace [1@2, X,Y,P]\\
\rowprefix{r_9}& : \sim mbr(X,P), mbr(Y,P), X \noteq Y, 
same\_skill(X,Y). \thinspace [1@2, X,Y,P] 
\end{align*}
\end{exmp}
The complete source code for this example is available at \examplelink{example_3_13}.

To run the example above following command is to be executed:
%
\leftaligned{\texttt{ \$ dlvhex2 \ example\_3\_13.hex \ --weak-allmodels}}
%
This time we have two best 
models in our solution:
\begin{align*}
\{ & \mathit{mbr}(b,p2), \mathit{mbr}(c,p2), 
   \mathit{mbr}(a,p1), \mathit{mbr}(d,p2), 
   \mathit{mbr}(e,p1) \} \\
   & \mathit{Cost} [ \mathit{Weight:Level]}):  \langle 
   [6:1],[0:2] \rangle \\ 
\{ & \mathit{mbr}(a,p2), \mathit{mbr}(b,p1), 
   \mathit{mbr}(c,p1), \mathit{mbr}(d,p1), 
   \mathit{mbr}(e,p2) \} \\
   & \mathit{Cost} ([ \mathit{Weight:Level]}):\langle 
   [6:1],[0:2] \rangle
\end{align*}

In $\row{r_1}$ and $\row{r_2}$ we defined employees as a set of the 
facts. Rules $\row{r_3}$, $\row{r_4}$ and $\row{r_5}$ specify $\mathit{know}$, 
$\mathit{same\_skill}$ and $\mathit{married}$ relations 
between some of employees. Since $\mathit{employee}(X)$ is 
true, each $\mathit{employee}$ will be assigned either to 
the project 1 or project 2 which is given in $\row{r_6}$. Rules $\row{r_7}$, $\row{r_8}$ and $\row{r_9}$ 
are weak constraints introduced earlier in this section, this time with the 
same weights but different levels of priority. Under 
prioritization, \dlvhex{} minimizes the violation of 
the constraints of the highest priority level first; then 
the lower priority levels are considered one after the 
other in descending order. This time we have two best 
models in our solution.     
}

\subsection{Higher-order Atoms}
\hex{}-programs are non-monotonic logic programs
admitting \emph{high-order atoms},
which are atoms containing a variable predicate symbol
(instead of a constant).
A high-order atom allows to quantify values over predicate names, and to 
freely exchange predicate symbols with constant symbols, 
like in the rule
%
\mycenterline{$C(X) \leftarrow \textit{subclassOf(D,C),D(X)}$}
%
where $C(X)$ and $D(X)$ are high-order atoms.
%
An atom can be seen as a tuple ($Y_0, Y_1, \dots,Y_n$),
where $Y_0, Y_1,\dots,Y_n$ are terms
and $ n \ge 0$ is the \textit{arity} of the atom.
Intuitively, $Y_0$ is the predicate name, and we thus also use the more 
familiar notation $Y_0(Y_1,\dots,Y_n)$. The atom is 
\textit{ordinary}, if $Y_0$ is a constant,
it is \textit{high-order} if $Y_0$ is a variable.

For example, 
$(x,rdf:type,c)$, $node(X)$, and $D(a,b)$, are atoms; the 
first two are ordinary atoms.

%High-order atoms are internally represented as normal atoms
%with an additional predicate symbol.

\subsection{External Atoms}
\label{extatoms}
External atoms are the central feature
that distinguishes \hex-programs from normal ASP programs.

Through external atoms, \hex{}-programs can communicate 
with other sources of computation;
this can be used to model part of a program outside of ASP
(e.g., parts that cannot be modeled in ASP
such as 3D simulations or Description Logic reasoning)
or to import knowledge into ASP
(e.g., from Semantic Web triplestores or from databases).

An \emph{external atom} is of the form
\begin{align*}
\&g[Y_1,\dots,Y_n](X_1,\dots,X_m),
\end{align*}
where $Y_1,
\dots,Y_n$ and $X_1,\dots,X_m$ are the two lists of terms 
(called \textit{input} and \textit{output} lists, 
respectively), and $\&g$ is an external 
predicate name.

Intuitively, an 
external atom provides a way for deciding the truth value 
of an output tuple depending on the input tuple
and depending on the truth of input predicates in the answer set.
%
An external atom can have three kinds of inputs:
\emph{predicate input} provides the truth values
of all atoms of a predicate to the computation,
while \emph{constant input}
only provides the constant symbol to the computation.
%
The third input type is \emph{tuple input}
which allows an arbitrary amount of constant inputs as arguments.
%
The type of an input must be specified when
implementing the external computation in the \dlvhex{} API
(see Section~\ref{sec:externalInterfaces}).

\begin{exmp}
For instance, the rule 
\begin{align*}
  reached(X) \leftarrow \&reach[edge,a](X).
\end{align*}
defines the predicate \textit{reached}
and takes values from the external predicate $\&reach$,
which computes in an external program
%via \textit{$\&reach[edge,a](X)$} 
all the reachable nodes $X$ in 
the graph specified by predicates \textit{edge} starting from node \textit{a}. 
%
Here we assume $\&reach$ takes a predicate as first input
and a constant as second input.
%
Then $edge$ is a predicate input:
the computation of $\&reach$ depends on the truth values
of predicate $edge$ in the answer set.
%
On the other hand, $a$ is a constant input:
the computation of $\&reach$ only uses the symbol $a$.
\end{exmp}
%
Note that because we used a predicate input in the previous example,
the above example can define reachability in a graph
that is part of a guessed in an answer set.
This is a feature unique to \dlvhex{}:
it cannot be emulated by externals in \gringo{}
(which have to be computed during grounding,
while \dlvhex{} computes external atoms during both grounding and solving).

In the next example we give a full program with external atoms
including their implementation.
\begin{exmp}
The following program concatenates strings specified
by the $\mi{system}$ predicate,
computes a set difference,
and then associates items in the resulting set
and the strings in a unique mapping.
\begin{align*}
  \rowprefix{r_1}& \mathit{system}(\mathit{dlvhex}). \ 
    \mathit{system}(\mathit{clasp}). \\  
  \rowprefix{r_2}& \mathit{sayhello(X)} \leftimpl 
    \ext{\mathit{concat}}{\mathit{hello, Y}}{\mathit{X}}, 
    \mathit{system(Y).}  \\[1ex] 
  \rowprefix{r_3}& \mathit{set1}(a). \ \mathit{set1}(b). \ 
    \mathit{set1}(c).\\
  \rowprefix{r_4}& \mathit{set2}(b). \ \mathit{set2}(c). \ 
    \mathit{set2}(d).\\
  \rowprefix{r_5}& \mathit{set3}(X) \leftimpl 
    \ext{\mathit{setdiff}}{\mathit{set1, set2}}{\mathit{X}}.  \\[1ex]
  \rowprefix{r_6}& \mathit{pairs}(X,Y) \leftimpl 
    \ext{\mathit{sortandmap}}{\mathit{sayhello,set3}}{X,Y}.
\end{align*}
\row{r_2} concatenates strings to produce messages in $\mi{sayhello}(X)$,
\row{r_5} computes a set difference in $\mi{set3}(X)$,
and \row{r_6} produces a unique mapping between hello messages
and the set difference.

There are three different external sources in this program, 
$\mathit{\&concat}$ has a tuple input and one output
and computes as output the concatenation of all inputs,
$\mathit{\&setdiff}$ uses two predicate inputs and also has one output
and computes as output the set difference of constants
in the first and the second input,
finally $\mathit{\&sortandmap}$ has two predicate inputs and two outputs
and computes a sorted one-to-one mapping between constants
in first and second inputs.

These external sources are implemented in the following Python plugin:

\lstinputlisting{example_3_stringset/example_3_stringset.py}

\noindent
Answer sets of the above program are obtained by invoking

\leftaligned{\texttt{\$ dlvhex2 --pythonplugin=example\_3\_stringset.py \textbackslash \\
\hphantom{\qquad \$ dlvhex2 }example\_3\_stringset.hex}}

\noindent
We obtain the following answer set.
\begin{align*}
  \{ & \mi{system(dlvhex),system(clasp),set1(a),set1(b),set1(c),set1(d),} \\
  & \mi{set2(b),set2(d),set3(a),set3(c),sayhello(hellodlvhex),sayhello(helloclasp),} \\
  & \mi{pairs(hellodlvhex,a),pairs(helloclasp,c)} \}
\end{align*}
%
Note that we use this example demonstration purposes,
in practice set difference can easier be realized using rules.
%
The complete source code for this example is available at
\examplelink{example_3_stringset}
(\exampledownloadlink{example_3_stringset/example_3_stringset.hex}{example\_3\_stringset.hex} and
\exampledownloadlink{example_3_stringset/example_3_stringset.py}{example\_3\_stringset.py}).
\end{exmp}

\section{Examples}
\label{sec:examples}
We now present three real life examples  
which are encoded and solved by \hex-programs.
In Section~\ref{sec:swimming} we solve a basic problem
about choosing a proper swimming location \cite{efikrs2015}.
In Section~\ref{sec:traveling} we solve the traveling salesperson problem.
In Section~\ref{sec:pathfinding} we show how we can use \dlvhex{}
to plan routes of one or multiple agents in the dynamic 
environment controlled by the external atoms.

\subsection{Swimming Example}
\label{sec:swimming}
In this example we present a program which selects  
the best swimming location among some available choices 
for a swim in Vienna. Selecting a location has to 
satisfy all constraints given from the user,
and properties of swimming locations are imported from external
using an external atom.

The complete source code for this example is available at
\examplelink{example_4_swim}
(\exampledownloadlink{example_4_swim/example_4_swim.hex}{example\_4\_swim.hex}
and 
\exampledownloadlink{example_4_swim/example_4_swim.py}{example\_4\_swim.py}).

\subsubsection{Problem}
Imagine Alice wants to go for a swim in Vienna. She knows 
two indoor pools called Margarethenbad and Amalienbad 
(represented by $\mathit{margB}$ and $\mathit{amalB}$, 
respectively), and she knows that outdoor swimming is 
possible in the river Danube at two locations called 
G\"anseh\"aufel and Alte Donau (denoted $\mathit{gansD}$ and 
$\mathit{altD}$, respectively). She looks up on the Web 
whether she needs to pay an entrance fee, and what 
additional equipment she needs. Finally she has the 
contraint that she does not want to pay for swimming. 
Assume Alice finds out that indoor pools in general have an 
admission fee, and that one also
has to pay at G\"anseh\"aufel, but not at Alte Donau. 
Furthermore Alice reads some reviews about swimming 
locations and finds out that she will need her Yoga mat for 
Alte Donau because the ground is so hard, and she will need 
goggles for Amalienbad because there is so much chlorine in 
the water.

The problem we will solve with \hex\ is
to find a suitable swimming location for Alice.

\subsubsection{Encoding}

A \hex-program used to select
an appropriate swimming location is as follows.

% PS: TODO put encoding and python plugin and commandline into figure on a single page
\begin{align*}
\rowprefix{r_1}& location(ind, margB). \ location(ind, amalB). \ \\& 
location(outd, gansD). \ location(outd, altD). \\  
\rowprefix{r_2}& swim(ind) \vee swim(outd).\\ 
\rowprefix{r_3}& need(inoutd, C) \leftimpl \ext{\mathit{rq}}
{\mathit{swim}}{\mathit{C}}. \\[1ex]
\rowprefix{r_4}& goto(X) \vee ngoto(X) \leftimpl swim(P), 
location(P, X).\\
\rowprefix{r_5}& go \leftimpl goto(X).\\
\rowprefix{r_6}& \leftimpl not \ go. \\
\rowprefix{r_7}& \leftimpl goto(X), goto(Y), X \noteq Y. \\[1ex]
\rowprefix{r_8}& \mathit{need}(loc, C) \leftimpl 
\ext{\mathit{rq}}{\mathit{goto}}{\mathit{C}}. \\ 
\rowprefix{r_9}& \leftimpl need(X, money).
\end{align*}

This program above represents Alice's reasoning 
problem. Rule $\row{r_1}$ contains a set of facts about possible 
swimming locations (where $\mathit{ind}$ and 
$\mathit{outd}$ are short for indoor and outdoor, 
respectively). Rule $\row{r_2}$ chooses indoor vs.\ outdoor 
swimming locations, and $\row{r_3}$ collects requirements that 
are caused by this choice using the external atom. 
%
In $\row{r_4}$ it is decided whether to visit indoor or outdoor locations.
By $\row{r_5}$ we define $go$ if at least one location is selected,
and $\row{r_6}$ removes answer set candidates where no location is selected.
Constraint $\row{r_7}$ ensures that only a single location is selected.
Rule $\row{r_8}$ collects all requirements caused by 
the choice of $\mathit{goto}$ location.
Finally $\row{r_9}$ states that all candidate solutions where 
Alice has to pay are removed.

Resources are obtained from the external atom of the form
\begin{align*}
  \ext{\mathit{rq}}{\mathit{location}\text{-}\mathit{choice}}%
  {\mathit{required}\text{-}\mathit{resources}}
\end{align*}
which intuitively 
evaluates to true if a given $\mathit{location}$-$\mathit{choice}$ 
requires a certain $\mathit{required}$-$\mathit{resource}$ and 
represents such resources  and their origin 
($\mathit{inoutd}$ or $\mathit{loc}$) using the predicate 
$\mathit{need}$. The external atom $\mathit{\&rq}$ has 
input and output arity $\mathit{in(\&rq)}$ = 
$\mathit{out(\&rq)}$ = 1. Intuitively  $\ext{\mathit{rq}}
{\mathit{\alpha}}{\mathit{\beta}}$ is true if a resource 
$\beta$ is required when swimming is a place in the 
extension of predicate $\alpha$. For example, 
$\ext{\mathit{rq}}{\mathit{swim}}{\mathit{money}}$ is true 
if $\mathit{swim(ind)}$ is true because indoor swimming 
pools charge money for swimming. 

The implementation of the external atom $\&rq$ in Python
is discussed in Example~\ref{ex:swimplugin} on page~\pageref{ex:swimplugin}.

\subsubsection{Problem Solution}

To obtain all answer sets of the above program,
execute the following command.

\leftaligned{\texttt{\$ dlvhex2 --pythonplugin=example\_4\_swim.py example\_4\_swim.hex}}

\noindent
The \dlvhex\ solver gives the following single answer set as output.
\begin{align*}
\{ & location(ind,margB),location(ind,amalB),location(outd,altD), \\
   & location(outd,gansD), swim(outd),go,ngoto(gansD),goto(altD),\\
   & need(loc,yogamat) \} 
\end{align*}

Under this answer set, the external atom
$\ext{rq}{goto}{yogamat}$ is true and all others
(e.g., $\ext{rq}{swim}{money}$, $\ext{rq}{goto}{money}$)
are false.

Intuitively, the answer set tells Alice to 
take her Yoga mat and go for a swim to Alte Donau (outside) 
which is free of charge. This is the only answer set which 
satisfies the given constraints.    

\subsubsection{Additional Remarks}

In this example, the external atom 
$\mathit{\&rq}$ uses a predicate as an input parameter.
If we want to use a constant input
instead of a predicate then
\row{r_3} and \row{r_8} should be replaced with
\begin{align*}
\rowprefix{r_3'}& need(inoutd, C) \leftimpl \ext{rq'}{Swim}{C}, swim(Swim). \\
\rowprefix{r_8'}& need(loc, C) \leftimpl \ext{rq'}{Goto}{C}, goto(Goto).
\end{align*}    
where $\&rq'$ is implemented differently from $\&rq$.

This will result in a larger grounding
(the extensions of $swim$ and $goto$ are expanded into rules).

\subsection{Traveling Salesperson Example}
\label{sec:traveling}
In this section we consider the well-known traveling 
salesperson problem, where the task is to decide whether there 
is a round trip that visits each node in a graph exactly 
once and whose accumulated edge costs must not exceed some 
budget $B$.

\subsubsection{Problem}
The traveling salesperson problem describes a salesperson who 
must travel between N cities. The order is not relevant as long as all cities are visited exactly once and the route is closed. Each of the 
links between the cities has a weight (or the 
costs) attached. The costs describe how ``difficult'' it is to 
traverse this edge on the graph, and may be given, for 
example, by the cost of an airplane ticket or train ticket, 
or perhaps by the length of the edge, or time required to 
complete the traversal \cite{wiki}.

This example is interesting for us because it is a typical 
optimization problem. Among all answer sets \dlvhex{} 
should select the best one according to the weak constraints 
concept explained in Section~\ref{optimize}. In the 
classical solver we are able to load only small graphs 
because it is not feasible to load large graphs completely into memory.
In this example we are using an external atom which is loading 
a graph from the external source edge by edge up to a specified 
depth level what makes it able to solve problems with 
extremely large graphs by considering only the part of the graph
that is relevant for solving the problem. 

The source code for this example is available at
\examplelink{example_4_travel}
(\exampledownloadlink{example_4_travel/example_4_travel.hex}{example\_4\_travel.hex},
\exampledownloadlink{example_4_travel/example_4_travel.py}{example\_4\_travel.py},
and
\exampledownloadlink{example_4_travel/example_4_travel.graph}{example\_4\_travel.graph}).

\subsubsection{Encoding}

\begin{figure}%
\begin{center}%
\begin{tikzpicture}%
\tikzset{vertex/.style = {shape=circle,draw,minimum 
size=1.5em}}
\tikzset{edge/.style = {->,> = latex'}}
% vertices
\node[vertex] (a) at  (0,0) {$\mathit{Chicago}$};
\node[vertex] (b) at  (4,-5) {$\mathit{Detroit}$};
\node[vertex] (c) at  (8,0) {$\mathit{Memphis}$};
\node[vertex] (d) at  (6,-3) {$\mathit{Boston}$};
\node[vertex] (a1) at (2,-3) {$\mathit{Austin}$};
\node[vertex] (a2) at (4,-1.5) {$\mathit{Fresno}$};
%edges
\draw[edge] (a) to [bend right=45] node [auto] {2} (b);
\draw[edge] (a) to (a1);
\draw[edge] (a) to node [auto] {2} (c);
\draw[edge] (b) to (d);
\draw[edge] (b) to node [auto] {1} (a1);
\draw[edge] (c) to (a);
\draw[edge] (c) to node [auto] {1} (a2);
\draw[edge] (c) to [bend left=45] node [auto] {2}(b);
\draw[edge] (d) to node [auto] {2} (c);
\draw[edge] (d) to node [auto] {4} (a2);
\draw[edge] (d) to node [auto] {2} (b);
\draw[edge] (a1) to node [auto] {3} (a);
\draw[edge] (a1) to node [auto] {2} (d);
\draw[edge] (a1) to (b);
\draw[edge] (a2) to node [auto,near start] {3} (a);
\draw[edge] (a2) to (c);
\draw[edge] (a2) to (d);
\end{tikzpicture}%
\end{center}%
\caption{Graph of cities for the Traveling salesperson example.}
\label{fig:travelcities}
\end{figure}

The \hex{}-program for this problem is as follows.
\begin{align*}
\rowprefix{r_1} & startingCity(austin).\\
\rowprefix{r_2} & budgetB(11).\\[1ex]
\rowprefix{r_3} & \mathit{cityOfDegree(P,0,P,0)}
  \leftimpl \mathit{startingCity(P).} \\[1ex]
\rowprefix{r_4} & \mathit{cityOfDegree(F1, DegPlus, F2, Cost)} 
  \leftimpl \mathit{cityOfDegree(\_, Deg, F1, \_)}, \\
  &\qquad\ext{edges}{F1}{F2, Cost}, \mathit{DegPlus=DegPlus+1},
    DegPlus < 4, \\
  & \qquad \#int(DegPlus), \#int(Deg)), \#int(Cost).\\
\rowprefix{r_5}& \mathit{node(Y)} \leftimpl 
  \mathit{cityOfDegree(X, V, Y, C)}.\\
\rowprefix{r_6}& \mathit{edge}(X, Y) \leftimpl 
  \mathit{cityOfDegree(X, V, Y, C).} \\
\rowprefix{r_7} & cost(X,Y,C) \leftimpl \mi{cityOfDegree}(X, V, Y, C).  \\
\rowprefix{r_8} & \{ cycle(X,Y) : edge(X,Y) \} = 1 \leftimpl 
  node(X). \\
\rowprefix{r_9} &  \{ cycle(X,Y) : edge(X,Y) \} = 1 \leftimpl 
  node(Y). \\[1ex]
\rowprefix{r_{10}} & costCalculated(X) \leftimpl \#sum \{C,X,Y : 
  cycle(X,Y), cost(X,Y,C)\} = X. \\
\rowprefix{r_{11}} & withinBudget(B,C) \leftimpl budget(B), 
  costCalculated(C), B \geeq C. \\
\rowprefix{r_{12}} & \leftimpl  budgetB(B), costCalculated(C), 
  \nott \thinspace \mathit{withinBudget(B,C).} \\[1ex]
\rowprefix{r_{13}} & reached(Y) \leftimpl cycle(\mi{Start}, Y), \mi{startingCity}(\mi{Start}). \\
\rowprefix{r_{14}} & reached(Y) \leftimpl cycle(X,Y), 
  reached(X). \\
\rowprefix{r_{15}} & \leftimpl node(Y), \nott \thinspace 
  \mathit{reached(Y)}. \\[1ex]
\rowprefix{r_{16}} & :\sim cycle(X,Y), cost(X,Y,C). \ [C@1,X,Y,C] 
\end{align*}

Fact $\row{r_1}$ specifies the starting city,
i.e., the city where the salesperson starts and finishes the trip.
Fact $\row{r_2}$ defines the available budget of the salesperson.

The predicate $\mathit{cityOfDegree}(R,D,S,C)$ keeps 
track of the cities newly discovered defined as successor 
nodes $S$ for the root node $R$, their distances from the 
root node as $D$ and the weight of the edge between $R$ and $S$ 
denoted as $C$.
Rule $\row{r_3}$ defines the starting city for discovered cities,
rule $\row{r_4}$ defines a graph of the discovered cities
using the external atom 
$\mathit{\&edges}$ to load new cities from the external 
file and use them in the program.

The external atom is of 
the form $\ext{edges}{File,F_1}{F_2,Cost}$
where $\mi{File}$ is the file to load the graph from,
and $\mathit{F_1}$ represents the node
for which we want to know all successor nodes.
The external atom semantics function
returns all pairs $(F_2,\mi{Cost})$
such that $F_2$ is successor node of $F_1$
and the edge has weight $\mathit{Cost}$.
$\mathit{DegPlus}$ is limited to be less than 4,
which means we can go at most three edges far from the root node. 
%
There are several potential advantages
of using an external atom of this type:%
\begin{inparaenum}[(i)]
\item
  the graph may be very large and it is not possible to load it 
  at once as a set of edges specified manually,
\item
  we do not know the graph completely
  (e.g., due to limited capabilities of a web service), or
\item
  we want to analyze only a subgraph of the graph that is 
  reachable from the specified node.
\end{inparaenum}

In $\row{r_5}$, $\row{r_6}$ and $\row{r_7}$ the program is extracting 
$\mathit{nodes}, \mathit{edges}$ and $\mathit{costs}$ of 
the edges from the $\mathit{cityOfDegree}$ atoms. 
%
Rules $\row{r_8}$ and $\row{r_9}$ assert that every 
node must have exactly one outgoing and exactly one 
incoming edge, respectively, belonging to the cycle.
The syntax used in these rules is described in Section~\ref{conditions}.

In $\row{r_{10}}$ we use aggregates (cf.\ Section~\ref{aggregates})
to find the sum $X$ of the costs over the 
$\mathit{cycle(X,Y)}$. In rule $\row{r_{11}}$, an atom 
$\mathit{withinBudget(B,C)}$ is true if the term of the 
$\mathit{costCalculated(C)}$ is less than or equal to the 
term of $\mathit{budgetB(B)}$ available.
The integrity constraint $\row{r_{12}}$ ensures that in the answer 
set overall sum of the costs for the cycle will be less 
than or equal to the budget available.
The same rules can be applied to limit length traveled or time spent.

Rules $\row{r_{13}}$ and $\row{r_{14}}$
define reachability of nodes, startin from the initial node
and using cycle candidates produced by the rules 
$\row{r_8}$ and $\row{r_9}$.
%
The integrity constraint $\row{r_{15}}$ 
eliminates answer sets where some nodes are not reached
\cite{gkklorst2015}.
% PS: why do we cite this here? is the example from their user guide?

In order to minimize costs, we add the weak constraint
\row{r_16}.
Here, edges belonging to the cycle are weighted according 
to their costs and \dlvhex{} lists optimal answer sets only.
For weak constraint syntax see Section~\ref{optimize}.

\subsubsection{Plugin}
\label{sec:travelplugin}

The external atom $\&edge$ can be realized in Python as follows.

\lstinputlisting{example_4_travel/example_4_travel.py}

This plugin uses the {\tt networkx} Python module
for comfortable processing of graphs stored in plain text files.
%
The plugin loads the graph, retrieves successor nodes
and returns them as output tuples.
Note that this code is for demonstrational purposes only,
a more efficient implementation is certainly possible.
%
The \enquote{finite output domain} property tells
\dlvhex{} that the instantiation of the external atom will be finite.

Details of the Python plugin API
are given in Section~\ref{sec:externalInterfaces}.

The encoding and plugin load the graph from the file
\exampledownloadlink{example_4_travel/example_4_travel.graph}{example\_4\_travel.graph}.
The file describes the directed weighted graph
shown in Figure \ref{fig:travelcities};
the first lines of that file as follows.

\lstinputlisting[language=,lastline=5]{example_4_travel/example_4_travel.graph}

\subsubsection{Problem Solution}

To obtain all optimal answer sets of the above program,
and display only the cycle predicate (which contains the solution)
execute the following command.

\leftaligned{\texttt{\$ dlvhex2 example\_4\_travel.hex --filter=cycle \textbackslash \\
\hphantom{\quad \$ dlvhex2 }--pythonplugin=example\_4\_travel.py}}

\noindent
The \dlvhex\ solver gives a single optimal answer set as output.
\begin{align*}
\{ & cycle(austin,boston), cycle(boston,memphis),cycle(detroit,austin), \\
   & cycle(chicago,detroit), cycle(memphis,fresno),cycle(fresno,chicago) \} \\
   & <[11:1]>.
\end{align*}
Note that only the $\mi{cycle}$ predicate is visible
due to the {\tt --filter} commandline option.
This makes the answer set easier to read.
The cheapest route which satisfies all given constraints is:
\smallskip

\centerline{%
Austin $\rightarrow$ Boston $\rightarrow$ Memphis $\rightarrow$ Fresno $\rightarrow$ Chicago $\rightarrow$ Detroit $\rightarrow$ Austin%
}
\smallskip

\noindent
with the minimum cost of 11. 

\subsection{Pathfinding Example}
\label{sec:pathfinding}
The last example is from the group of planning problems
and it considers pathfinding for multiple agents.
 
\subsubsection{Problem}
Pathfinding for a single agent is the problem of planning a 
route from an initial
location to a goal location in an environment, going around 
obstacles. 
Pathfinding for multiple agents also aims to plan such 
routes for each agent, 
subject to different constraints, such as restrictions on 
the length of each path 
or on the total length of paths, no self-intersecting 
paths, no intersection of 
paths/plans, no crossing/meeting each other.  It also has 
variations for finding optimal solutions, e.g., with 
respect 
to the maximum path length, or the sum of plan lengths. 
These problems are important
for many real-life applications, such as motion planning, 
vehicle routing, environmental monitoring, patrolling, 
computer games \cite{ekos2013}.
An ASP formulation for this problem
where multiple agents need to find paths 
from their respective starting locations to their goal 
locations, ensuring that 
paths do not collide with static obstacles and that no two 
agents collide with 
each other was described in \cite{ekos2013}.
We extend this formulation by importing the graph
using an external atom to consider only parts of a 
(potentially very large) graph.

The full source code for this example
is available at \examplelink{example_4_pathfind}
(\exampledownloadlink{example_4_pathfind/example_4_pathfind.hex}{example\_4\_pathfind.hex},
\exampledownloadlink{example_4_pathfind/example_4_pathfind.py}{example\_4\_pathfind.py},
and
\exampledownloadlink{example_4_pathfind/example_4_pathfind.graph}{example\_4\_pathfind.graph}).

\subsubsection{Encoding}
We can encode this problem
in the following \hex-program.
\begin{align*}
\rowprefix{r_1} & \mi{startingNode}(one). \\
\rowprefix{r_2} & \mi{nodeOfDegree}(P,0,P) \leftimpl \mi{startingNode}(P).  \\
\rowprefix{r_3} & \mi{nodeOfDegree}(F1, DegPlus, F2)
    \leftimpl \mi{nodeOfDegree}(\_, Deg, F1), \\
  & \qquad \ext{edges}{F1}{F2}, DegPlus=Deg+1, \#int(DegPlus).  \\
\rowprefix{r_4} & node(Y) \leftimpl \mi{nodeOfDegree}(X, V, Y).  \\
\rowprefix{r_5} & edge(X,Y) \leftimpl \mi{nodeOfDegree}(X,V,Y).\\[1ex]
\rowprefix{r_6} & \mathit{agent(1). } \ \mathit{agent(2).}\\
\rowprefix{r_7} & \mathit{start(1,one).} \ \mathit{start(2,four).} \\
\rowprefix{r_8} & \mathit{goal(1,ten).} \ \mathit{goal(2,eleven).} \\[1ex]
\rowprefix{r_9} & clear(V) \leftimpl
  \mathit{node(V)}, V \noteq \mathit{three} \\[1ex]
\rowprefix{r_{10}} & \mi{path}(I,0,V) \leftimpl start(I,V). \\
\rowprefix{r_{11}} & \{ \mi{path(I,TP,U)} \colon \mi{edge(U,V)} \}
  \leftimpl \\
  &\qquad \mathit{agent(I)}, \mathit{path(I,T,V)},
    \mathit{TP=T+1}, \mathit{\#int(TP)}. \\
\rowprefix{r_{12}} &
  \leftimpl \mathit{agent(I)}, \mathit{\#int(T)},
    1 < \mathit{\#count\{ U \colon \mi{path}(I, T, U) \}}. \\[1ex]
\rowprefix{r_{13}} & visit(I, V) \leftimpl \mi{path}(I,T,V). \\[1ex]
\rowprefix{r_{14}} &
  \leftimpl goal(I, V), \nott \thinspace  \mathit{visit(I, V).} \\
\rowprefix{r_{15}} &
  \leftimpl \mi{path}(I, T, V), \mi{path}(IP,T,V), X \lesseq XP. \\
\rowprefix{r_{16}} &
  \leftimpl \mi{path}(I,T,V), \nott \thinspace  \mathit{clear(V).}\\[1ex]
\rowprefix{r_{17}} & \leftimpl \mi{path(I,T,V)}, \mi{path(I,TP,U)},
  \mi{TP=T+1}, \nott \ext{check}{I,U,V}{}.
\end{align*}
%
In $\row{r_2}$--$\row{r_5}$ we load part of the graph using 
the $\&edges$ external atom
which discovers nodes and edges from the external file,
limited by the maximum integer value.
%
In $\row{r_6}$--$\row{r_8}$
we represent agents and their start and goal positions.
%
Rule $\row{r_9}$ represents that all vertices
except \enquote{$three$} are obstacle-free.

Rules $\row{r_{10}}$ and $\row{r_{11}}$
guess a path for each agent,
where the agent can visit a new node using an edge,
or do nothing.
%
Constraint $\row{r_{12}}$ eliminates all answer set candidates
in which there is more than one vertex visited by a single agent at one time
(no agent can be at two different locations at the same time).
%
Rule $\row{r_{13}}$ defines which nodes are visited, using the path.
Constraint $\row{r_{14}}$ ensures that
each agent reaches its destination node. We ensure that 
agents do not collide with each other using constraint 
$\row{r_{15}}$. We also ensure that agents do not go through 
obstacles using constraint $\row{r_{16}}$. 

Constraint $\row{r_{17}}$
represents an external check of the form $\mi{\&check[I,U,V]()}$ which checks
if agent $I$ is able to move from node $U$ to node $V$.
The external atom decides whether that move is valid or invalid,
for example because in the abstract representation of the graph
certain combinations of properties of agents and edges
(that can prevent successful movement)
are not represented,
e.g., narrow corners, or doors that are too small for certain agents.

Note that by using an external check we
can make the planning problem more abstract
by creating a sound (efficient) encoding
and making it complete using the external check.

\subsubsection{Plugin} 

The external atoms $\&edge$ and $\&check$ are realized in Python as follows.

\lstinputlisting{example_4_pathfind/example_4_pathfind.py}

\noindent
See Section~\ref{sec:travelplugin}
for an explanation of a similar plugin
and Section~\ref{sec:externalInterfaces} for the Python API.

\subsubsection{Problem Solution} 

\begin{figure}
\begin{center}
\begin{tikzpicture}[yscale=0.5]
\tikzset{vertex/.style = {shape=circle,draw,minimum size=3.5em}}
\tikzset{edge/.style = {->,> = latex'}}
% vertices
\node[vertex] (a) at  (0,3) {$\mathit{one}$};
\node[vertex] (b) at  (2,6) {$\mathit{two}$};
\node[vertex] (c) at  (2,3) {$\mathit{three}$};
\node[vertex] (d) at  (2,0) {$\mathit{four}$};
\node[vertex] (e) at  (4,6) {$\mathit{five}$};
\node[vertex] (f) at  (4,3) {$\mathit{six}$};
\node[vertex] (g) at  (4,0) {$\mathit{seven}$};
\node[vertex] (i) at  (6,6) {$\mathit{eight}$};
\node[vertex] (j) at  (6,3) {$\mathit{nine}$};
\node[vertex] (k) at  (8,6) {$\mathit{ten}$};
\node[vertex] (l) at  (8,3) {$\mathit{eleven}$};
%edges
\draw[edge] (a) to (b);
\draw[edge] (a) to (c);
\draw[edge] (a) to (d);
\draw[edge] (b) to (e);
\draw[edge] (c) to (f);
\draw[edge] (d) to (g);
\draw[edge] (e) to (i);
\draw[edge] (f) to (j);
\draw[edge] (g) to (j);
\draw[edge] (i) to (k);
\draw[edge] (j) to (l);
\draw[edge] (j) to (k);
\end{tikzpicture}
\end{center}
\caption{Simulation of the environment used by agents}
\label{fig:pathfinding}
\end{figure}

Assume we solve the problem using the graph in Figure~\ref{fig:pathfinding}.
The graph is again loaded from the external file and not 
specified as a set of facts.
We know that there is an obstacle at node $\mathit{three}$, so any answer set with node 
$\mathit{three}$ in the path is removed.

To obtain all answer sets of the above program,
and display only the path predicate (which contains the solution)
execute the following command.

\leftaligned{\texttt{\$ dlvhex2 example\_4\_pathfind.hex --filter=path --maxint=4 \textbackslash \\
\hphantom{\quad \$ dlvhex2 }--pythonplugin=example\_4\_pathfind.py --heuristics=old}}

\noindent
Note that here we also specify the maximum integer number.
If we do not do this, \dlvhex{} uses the largest integer in the program
which is in this case $2$, hence without {\tt --maxint} no solution is found.
We also specify an evaluation heuristics for performance reasons.
% TODO PS check why this is so slow with default heuristics

The answer sets of this program are as follows:
\begin{align*}
 \{ & path(1,0,one),path(2,0,four),path(1,1,four),path(2,1,seven), \\
 & path(1,2,seven),path(2,2,nine),path(1,3,nine),path(2,3,eleven), \\
 & path(1,4,ten) \}
\end{align*} 
This means that agent $1$ follows the path
\smallskip

\centerline{%
  one $\rightarrow$ four $\rightarrow$ seven
  $\rightarrow$ nine $\rightarrow$ ten}
\smallskip
  
\noindent
and at each time agent $2$ follows
\smallskip

\centerline{%
  four $\rightarrow$ seven
  $\rightarrow$ nine $\rightarrow$ eleven}
\smallskip

\noindent
and does not perform a last step.

As the external check excludes the path via $two$
and the internal knowledge exludes paths via $three$
there is only one answer set.

\section{External Interfaces}
\label{sec:externalInterfaces}
This section discusses the implementation of external sources. One important design principle was to provide a 
mechanism to easily add further external atoms, as introduced in Section~\ref{extatoms}, without 
having to recompile the main application.
 
Formally, an external atom is defined to evaluate to true
or false, depending on a number of parameters:
\begin{compactitem}
\item An interpretation (a set of atoms)
\item A list of input constants
\item A list of output constants
\end{compactitem}  
However, it is more intuitive and convenient to think of an 
external atom not as being boolean, but rather functional:
depending on a given interpretation and a list of input 
constants, it returns output tuples for which it is true. For instance, the 
external atom to import triples from RDF files has the 
form:
\mycenterline{$\ext{rdf}{\mi{Uri}}{X,Y,Z}$} 
\noindent
where $\mathit{Uri}$ stands for a string denoting the RDF-source and X, Y, and Z are variables that represent an RDF-triple $(X,Y,Z)$ from the specified source.

\subsection{Information Flow}
The interface that is used by \dlvhex{} to access a plugin 
follows very closely the previously described ``function'' semantics.
For each predicate (e.g., for $\amp{rdf}$),
a retrieval function has to be implemented.
This function receives a query object and returns an answer object.
The function is always called with ground input parameters.
The query object carries the ground input parameters
and the input interpretation, 
while the answer object is a container for the ground output 
tuples.

\subsection{Types of Input Parameters}
\label{inputparamtypes}

Previously we said that the semantic function of an external atom
may use the complete interpretation for its computation.
For practial and for efficiency reasons,
often only small parts of the interpretation are used.

This leads to three types of input parameters: 
\begin{compactitem}
\item Constant parameters
\item Predicate parameters
\item Tuples
\end{compactitem}

A parameter of type \emph{constant} is not related to the 
interpretation at all, like in the previous example of the 
RDF-atom where we have a string as a constant input to the external atom. 

A parameter is of type \emph{predicate} indicates that 
all atoms with this predicate in the interpretation are 
relevant for the semantic evaluation of the external atom.
%
%
As an example, assume an external 
atom that calculates the overall price of a number of books 
given by their ISBN number:
\mycenterline{$\ext{overallbookprice}{isbn}{X}$}
The single input parameter of this atom would be of type 
\emph{predicate}, meaning that not the constant itself is 
used by the atom's function,
but all atoms $\mi{isbn}(Y) \in I$ with this predicate.
Assume the current answer set candidate $I$ is
\mycenterline{$I = \{ \mi{isbn}(\textit{``0-19-82183-6''})$,
  $\mi{isbn}(\textit{``0-201-99954-4''})$, $p(a)$, $q(b) \dots\}$}
\noindent
then the function implementing $\amp{overallbookprice}$
will be called with the following filtered interpretation:
\mycenterline{$I = \{ \mi{isbn}(\textit{``0-19-82183-6''})$,
  $\mi{isbn}(\textit{``0-201-99954-4''}) \}$}
\noindent
where only atoms with predicate $\mi{isbn}$ remain.

A parameter of type \emph{tuple} stands for
an arbitrary number of constant input parameters.
This is, e.g., useful for string operations like concatenation
\mycenterline{$\ext{concat}{string1, string2, string3, \dots}{Out}$}
\noindent
where the atom is true for the output constant
which is the concatenation of all input strings.
(Note that for this functionality the interpretation is irrelevant
and the function implementing $\amp{concat}$ will receive $I=\emptyset$.)

Specifying the type of input parameters not only helps to 
single out the relevant part of the interpretation, but 
also supports \dlvhex{} in calculating the dependencies 
within a \hex-program. Plugins can be implemented either in Python or C++, as shown in the following two subsections.

\subsection{Implementing External Atoms in Python}
With \dlvhex{} version 2.4.0, a Python plugin interface was 
introduced, which supports Python scripts that provide 
functions to realise custom external atoms.

A Python plugin is a script that starts with
\verb|import dlvhex| and contains the following functions:
\begin{compactitem}
\item
  a \verb|register| function
  that registers all external atoms, and
\item
  for each external atom an evaluation function
  that has the same name as the atom.
\end{compactitem}

\subsubsection{Registering External Atoms}
\label{registerExtAtom}
%
The \verb+register+ function has the following form:
%
\begin{lstlisting} 
def register():
  dlvhex.addAtom("Atom_Name",(Input_Parameters),Output_Arity) 
\end{lstlisting}
%
It contains a call of \verb+addAtom+ for each external atom.
Each call specifies three parameters:
%
\begin{compactitem}
\item
  \verb+Atom_Name+ is the name of the external predicate;
\item
  \verb+(Input_Parameters)+ is a tuple of
  arbitrarily many input parameter \emph{types}.
  Each type is one of \verb+dlvhex.CONSTANT+, \verb+dlvhex.PREDICATE+, or 
  \verb+dlvhex.TUPLE+,
  corresponding to the concepts introduced in the previous section;
\item
  \verb+Output_Arity+ is an integer value
  representing the output arity of an atom.
\end{compactitem}
%
Consider the $\mathit{\&concat}$ external atom
introduced in the previous section.
It takes an arbitrary number of strings as input
and outputs their concatenation.
Hence the input type is \verb|dlvhex.TUPLE|
and the register function is as follows.%
\footnote{Note the extra ``,'': the Python syntax for creating a tuple
with a single element is \texttt{(a,)}.}
\begin{lstlisting}
def register():
  dlvhex.addAtom("concat", (dlvhex.TUPLE,), 1)  
\end{lstlisting}
If we assume that $\amp{concat}$ only accepts two strings,
the register function would be as follows.
\begin{lstlisting}
def register():
  dlvhex.addAtom("concat", (dlvhex.CONSTANT, dlvhex.CONSTANT), 1)  
\end{lstlisting}

\subsubsection{Implementing Semantics of External Atoms}
Once an external atom is registered,
it has to be implemented in the form of another Python function 
with an appropriate number of input parameters and output parameters.
\paragraph{Parameter Values (Input)}
As introduced in Section~\ref{inputparamtypes}
\dlvhex{} supports three different input types
(constant, predicate, and tuple).
The Python function implementing the external atom
requires one parameter for each element of the tuple given in \verb|addAtom|.
In general an external atom implementation looks as follows.
\begin{lstlisting}
def Atom_Name(Input_Parameter_1, Input_Parameter_2,...):
  Implementation ...
\end{lstlisting}
Each of the input parameter types is accessed in different way: 
\begin{compactitem}
\item
  To access data for input parameters of type \verb+CONSTANT+,
  if the parameter variable is called \verb+var+
  one obtains its value by writing \verb+var.value()+.
  %
  Example~\ref{constantAsInput} shows how to use a \verb+CONSTANT+ parameter.
\item
  To access data for input parameters of type \verb+PREDICATE+,
  if the parameter variable is \verb+var+
  then \verb+var.value()+ will just give the predicate given as argument.
  Method \verb+dlvhex.getTrueInputAtoms()+ provides a collection
  of all atoms of relevant predicates that are true in the current candidate.
  Using \verb+for atm in dlvhex.getTrueInputAtoms():+
  it is possible to enumerate these atoms.
  An atom \verb+atm+, for example $\mi{edge}(\mi{one},\mi{four})$
  corresponds to a tuple $(\mi{edge},\mi{one},\mi{four})$
  that can be obtained via \verb+atm.tuple()+.
  In this tuple, the value of each element again can be obtained
  using the method \verb+.value()+.
  %
  Example~\ref{ex:swimplugin} shows how to use a \verb+PREDICATE+ parameter.
\item
  To access data for input parameters of type \verb+TUPLE+,
  if the parameter variable is \verb+var+ then
  this variable will obtain a tuple corresponding with the ground input tuple.
  For each member \verb+x+ of that tuple \verb+var+
  we obtain its value using \verb+x.value()+.
  %
  Example~\ref{tupleAsInput} shows an implementation for \verb|&concat|
  using a \verb+TUPLE+ parameter.
\end{compactitem}
%
The object returned by the \verb+.value()+ method
is of type \verb|int| or \verb|str|.%
\footnote{The class providing the method \texttt{.value()}
  is of type \texttt{dlvhex.ID}, which is a data structure
  that holds the internal ID of an atom/constant/term within \dlvhex.}

\paragraph{Creating Output Tuples}
An external atom returns output tuples corresponding to the arity
specified in the register function (cf. Section~\ref{registerExtAtom}).
The \dlvhex{} command used for output looks as follows: 
\begin{lstlisting}
dlvhex.output((Output_Parameter_1, Output_Parameter_2,...))
\end{lstlisting}
Command to output a tuple containing a single value
stored in variable \verb|item| looks as follows.
\begin{lstlisting}
dlvhex.output( (item,) )
\end{lstlisting}
The output command above returns a constant in a tuple of size one
(cf. Example~\ref{constantAsInput}). 
If we want for instance to return a tuple of size two
containing an integer as second element,
the output command will be as follows.
\begin{lstlisting}
dlvhex.output( (node, int(j)) )
\end{lstlisting}
See also the example in Section~\ref{sec:traveling}.
Note that the output type of the first element
can be integer, constant, or string,
depending on what is stored in \verb|node|.
% PS TODO perhaps we should explain these types (42 vs 'foo' vs '"foo"') and their problems/features/error messages, e.g., 'Foo' will make an error as it cannot be stored as constant, on the contrary '"Foo"' will be stored as string. Also '42' cannot be stored as constant, we either need to use integer 42 or string '"42"'.

\subsubsection{Examples}
In the following we provide three examples,
corresponding to the previously explained input parameter types.

\begin{exmp}[\exampledownloadlink%
  {example_5_1/example_5_1.py}{download example\_5\_1.py}]
\label{constantAsInput}
This Example uses a constant (string) input parameter.
This plugin is used in Example~\ref{faceQuery}
to query all direct friends of the person of interest.

\lstinputlisting[numbers=left]{example_5_1/example_5_1.py}

The complete source code for this example is available at
\examplelink{example_5_1}.
% TODO PS there is only python code here, where is the usage of this plugin? we should also put some .hex file there or just point to another example if this plugin source code is also present in another example directory.

Lines 1--2 import two libraries:
every \dlvhex{}-plugin must import \verb+dlvhex+;
and the \verb+networkx+ library is needed in this particular example
for comfortable graph operations 
(loading a graph from a file, getting successors of a node). 

Lines 8--17 implement the external atom \verb+&friendsOf+ 
which receives the name of a person as string,
loads a graph from disk in line 11,
and returns all direct friends of the person in the graph in line 17.

Lines 20--23 register \verb+&friendsOf+
with a single constant input parameter and a single output parameter,
and a futher parameter \verb+prop+
which provides meta-information about the atom (required for liberal safety).%
\footnote{Advanced Topic:
in this case we provide the meta-information that only finitely many friends
can be discovered this way, i.e., that the graph is finite.}
\end{exmp}

\begin{exmp}[\exampledownloadlink%
  {example_4_swim/example_4_swim.py}{download example\_4\_swim.py}]
\label{ex:swimplugin}
This example shows the Python plugin for external atom $\&rq$
from the Swimming Example.
See Section~\ref{sec:swimming} for details of the corresponding program
how to run it.

The source code of the plugin is as follows.

\lstinputlisting[numbers=left]{example_4_swim/example_4_swim.py}

This example uses a predicate input parameter
for the external atom \verb+&rq+.
This external atom checks requirements
for a selected swimming location.
In the \hex{} program the external atom is of the form 

\mycenterline{$\ext{\mathit{rq}}{\mathit{location\_choice}}
{\mathit{required\_resource}}$}

\noindent
which intuitively evaluates 
to true whenever a given $\mi{location\_choice}$ requires a certain 
$\mi{required\_resource}$.
%and represents such resources and their 
%origin (inoutd, or loc) using predicate $\mathit{need}$. 

From line 7--12 we implement the \verb+rq+ function.
Line 9 extracts the location from the atom,
line 10 checks if the predicate of the current input atom
is equivalent to the value of \texttt{location\_choice}
(which specifies the predicate of interest),
line 11 checks if we know some requirement
and if so line 12 returns that requirements.
Lines 15--16 register the external atom \verb+&rq+.

For example, if $\mi{goto}(\mi{amalB})$ is true
in the answer set candidate,
then one of the \verb|for| loop iterations will contain
in \verb|x| the ID of the atom $\mi{goto}(\mi{amalB})$.
Then \verb|x.tuple()| is a tuple
of IDs of constants $\mi{goto}$ and $\mi{amalB}$.
Using the method \verb|.value()|
we obtain the strings of these IDs:
\verb|x.tuple()[0].value() = 'goto'|
and \verb|inp = x.tuple()[1].value() = 'amalB'|.
Accordingly the \verb|if| condition in line 10 is true
and line 12 returns \verb|('goggles',)|.
This means that the external atom
$\ext{rq}{goto}{\mi{goggles}}$ is true.
\end{exmp}

\begin{exmp}[\exampledownloadlink%
  {example_5_3/example_5_3.py}{download example\_5\_3.py}]
\label{tupleAsInput}
The third example demonstrates parameter type \verb|dlvhex.TUPLE|
which stands for an arbitrary number of constant input parameters.
As an example where this is useful we show string concatenation.
\lstinputlisting[numbers=left]{example_5_3/example_5_3.py}
The complete source code for this example is available at \examplelink{example_5_3}.
% TODO PS there is only python code here, where is the usage of this plugin? we should also put some .hex file there or just point to another example if this plugin source code is also present in another example directory.
% TODO perhaps eliminate example_5_3 and explain example_3_stringset instead

This external atom receives a tuple of strings,
concatenates them and outputs them as a single string value.
Line 7 initializes an empty string variable \verb|ret|,
the loop appends input strings to \verb|ret|
and line 12 outputs one tuple with the result.
\end{exmp}

\subsubsection{Learning additional constraints}

\tobewritten

\subsubsection{Further Information}

More information about methods in the \dlvhex{}
Python API is available online at
\url{http://www.kr.tuwien.ac.at/research/systems/dlvhex/doc2x/group__pythonpluginframework.html}.

\subsection{C++}

\tobewritten

\section{Command Line options}
\label{sec:commandline}
In this section, we briefly describe the meaning of the command line options supported by \dlvhex{}. 
Calling \dlvhex{} without any arguments will show all 
command line options available.
For each option, we indicate whether it requires an argument, and if so, we also describe it.
An abstract invocation of \dlvhex{} looks as follows:

\leftaligned{\texttt{\$ dlvhex2 [OPTION] FILENAME [FILENAME ...]}}
\noindent
or for reading the program from standard input
\leftaligned{\texttt{\$ dlvhex2 [OPTION] --}}

The following set of commands is related with Input, Output and  Reasoning options.
% and they directly affect the result.
% Sets column space
%\def\arraystretch{2}\tabrowsep=50pt
% Sets row space
\renewcommand{\arraystretch}{1.4}
\begin{longtable}{ p{2.0em} p{2.2cm} p{0.6cm} p{8.0cm} } 
 & \texttt{--}& & Parse from standard input. \\ 
\texttt{-s} & \texttt{--silent}&& Do not display anything than the actual result \\ 
\texttt{-f} & \texttt{--filter=foo[,bar[,...]]} && \\
& & & Only display instances of the specified predicate(s).\\
& \texttt{--nofacts} && Do not output EDB facts. EDB facts are the facts of the program.  \\
\texttt{-n} & \texttt{--number=<num>} && Limit number of displayed models to $\langle$\texttt{num}$\rangle$, Default value is 0, which means to display all models.\\ 
\texttt{-N} & \texttt{--maxint=<num>} && Set maximum integer (\# \texttt{maxint} in the program takes precedence). \\
 & \texttt{--weaksafety} && Skip strong safety check.\\
 & \texttt{--strongsafety} && Applies traditional strong safety criteria. \\
  & \texttt{--liberalsafety} && Uses more liberal safety condition than strong safety. \\
  &\texttt{--mlp}&& Use \dlvhex{}$+$mlp solver (modular nonmonotonic logic programs).\\
  & \texttt{--forget} && Forget previous instantiations that are not involved in current computation (mlp setting). \\
  & \texttt{--split} &&Use instantiation splitting techniques.\\
  & \texttt{--noeval} && Parse the program, but do not evaluate it (only useful with \texttt{--verbose}). \\
  & \texttt{--keepnsprefix} && Keep specified namespace-prefixes in the result. \\
  & \texttt{--keepauxpreds} && Keep auxiliary predicates in answer sets. \\
\end{longtable}
\bigskip
\subsection{Plugin Options}
\begin{longtable}{ p{2.0em} p{2.2cm} p{0.6cm} p{8.0cm} } 
 \texttt{-p}&\texttt{--plugindir=DIR}&&Specify additional directory where to look for plugin libraries (additionally to the installation plugin-dir and \texttt{\$HOME/.dlvhex/plugins}). Start with \texttt{!} to reset the preset plugin paths, e.g., ``\texttt{!:/lib}'' will use only \texttt{/lib/}.
 \\
\end{longtable}

\subsection{Performance Tuning Options}
\begin{longtable}{ p{2.0em} p{2.2cm} p{0.6cm} p{8.0cm} } 
%--EXTLEARN
\multicolumn{4}{p{6cm}}{\texttt{--extlearn[=none,iobehavior,monotonicity,functionality,}} \\[-1.5ex]
\multicolumn{4}{p{6cm}}{\texttt{\hphantom{--extlearn[}linearity,neg,user,generalize]}} \\

& & & Learn nogoods from external atom evaluation (only useful with \texttt{--solver=genuineii} or \texttt{--solver=genuinegi)}.\\
&\texttt{none}:& & Deactivate external learning. \\
&\texttt{iobehaviour}:& &Apply generic rules to learn input-output behaviour. \\
&\texttt{monotonicity}:& &Apply special rules for monotonic and antimonotonic external atoms.\\
&\texttt{functionality}:& &Apply special rules for external atoms which are linear in all predicate parameters.\\
&\texttt{linearity}:& &Apply special rules for external atoms which are linear in all predicate parameters.\\
&\texttt{neg}:& &Learn negative information\\
&\texttt{user}:& &Apply user-defined rules for nogood learning\\
&\texttt{generalize}:& &Generalize learned ground nogoods to ground nogoods.\\
& & & By default all options above except ``\texttt{generalize}'' are enabled.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--supportsets}} &
  Exploits support sets for evaluation.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--evalall}} &
  Evaluate all external atoms in every compatibility check, even if previous external atoms already failed.  This makes nogood learning more independent of the sequence of external atom checks. Only useful with \texttt{--extlearn}.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--nongroundnogoods}} &
Automatically instantiate learned nonground nogoods.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--flpcheck=[explicit,ufs,ufsm,aufs,aufsm,none]}} \\
%  Sets the strategy used to check if a candidate is a subset-minimal model of the reduct.\\
&\texttt{explicit}:&&Compute the reduct and compare its models with the candidate\\
&\texttt{ufs}:&&Use unfounded sets for minimality checking
\\
&\texttt{ufsm}:&&Use unfounded sets for minimality checking, do not decompose the program for UFS checking.\\
&\texttt{aufs}:&&Use unfounded sets for minimality checking by exploiting assumptions (default).\\
&\texttt{aufsm}:&&Use unfounded sets for minimality checking by exploiting assumptions. Do not decompose the program for UFS checking.\\
&\texttt{none}:&&Disable the check.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--flpcriterion=[all,head,e,none]}}\\
& & & Defines the kind of cycles whose absence is exploited for skipping minimality checks.\\
&\texttt{all (default)}:&&Exploit head- and e-cycles for skipping minimality checks\\
&\texttt{head}:&& Exploit head-cycles for skipping minimality checks\\
&\texttt{e}:&&Exploit e-cycles for skipping minimality checks\\
&\texttt{none}:&& Do not exploit head- or e-cycles for skipping minimality checks\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--noflpcriterion}} &
  Do no apply decision criterion to skip the FLP check. (equivalent to \texttt{--flpcriterion=none)}\\
\multicolumn{4}{l}{\texttt{--ufslearn=[none,reduct,ufs]}} \\
&&&Enable learning from UFS checks (only useful with \texttt{--flpcheck=[a]ufs[m]}).\\
&\texttt{none}:&&No learning\\
&\texttt{reduct}:&&Learning is based on the FLP-reduct\\
&\texttt{ufs (default)}:&&Learning is based on the unfounded set\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--eaevalheuristics=[always,periodic,inputcomplete,}}\\
\multicolumn{4}{l}{\texttt{\hphantom{--eaevalheuristics=[}eacomplete,post,never]}}\\
& & & Selects the heuristic for external atom evaluation.\\
&\texttt{always}:&&Evaluate whenever possible.\\
&\texttt{periodic}:&&Evaluate in regular intervals.\\
&\texttt{incomplete}:&&Evaluate whenever the input to the external atom is complete.\\
&\texttt{eacomplete}:&& Evaluate whenever all atoms relevant for the external atom are assigned.\\
&\texttt{post}:&&Only evaluate at the end (default).\\
&\texttt{never}:&&Only evaluate at the end and also ignore custom heuristics provided by plugins.\\
&&&Except for heuristics "never", custom heuristics provided by external atoms overrule the global heuristics for the particular external atom.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--ufscheckheuristic=[post,max,periodic]}}\\
& & & Specifies the frequency of unfounded set checks (only useful with \texttt{--flpcheck=[a]ufs[m])}.\\
&\texttt{post}:&&Do UFS check only over complete interpretations (default).\\
&\texttt{max}:&&Do UFS check as frequent as possible and over maximal subprograms.\\
&\texttt{periodic}:&&Do UFS check in periodic intervals.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--modelqueuesize=N}} &
  Size of the model queue, i.e. number of models which can be computed in parallel. Default value is 5. The option is only useful for clasp solver.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--solver=S}} &
  Use S as ASP engine, where S is one of \dlv{}, \dlvdb{}, \libdlv{}, \libclingo{}, \genuineii{}, \genuinegi{}, \genuineic{}, \genuinegc{} (\texttt{genuineii}=(i)nternal grounder and (i)nternal solver; \texttt{genuinegi}=(g)ringo grounder and (i)nternal solver \texttt{genuineic}=(i)nternal grounder and (c)lasp solver; \texttt{genuinegc}=(g)ringo grounder and (c)lasp solver).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--claspconfig=C}} &
  If clasp is used, configure it with \texttt{C} where \texttt{C} is parsed by clasp config parser, or \texttt{C} is one of the predefined strings frumpy, jumpy, handy, crafty, or trendy.\\
%%%%%%%%%%%%%%%%%%%
\texttt{-e}& \multicolumn{2}{l}{\texttt{--heuristics=H}} &
Use \texttt{H} as evaluation heuristics, where \texttt{H} is one of\\
&\texttt{old}:&&Old dlvhex behavior\\
&\texttt{trivial}:&&Use component graph as eval graph (much overhead)\\
&\texttt{easy}:&&Simple heuristics, used for LPNMR2011\\
&\texttt{greedy (default)}:&& Heuristics with advantages for external behaviour learning\\
&\texttt{monolithic}:&& Put entire program into one unit\\
&\texttt{manual:<file>:} &&  Read ``collapse'' $\langle$ idxs $\rangle$ share $\langle$idxs$\rangle$ commands from $\langle$file$\rangle$ where component indices $\langle$idx$\rangle$ are from \texttt{--graphviz=comp}\\
&\texttt{asp:<script>}:&&Use asp program $\langle$\texttt{script}$\rangle$ as eval heuristic\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--forcegc}} &
  Always use the guess and check model generator.\\
%%%%%%%%%%%%%%%%%%%
\texttt{-m}& \multicolumn{3}{l}{\texttt{--modelbuilder=M}} \\
&&& Use \texttt{M} as model builder, where \texttt{M} is one of (online,offline).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{2}{l}{\texttt{--nocache}} &&
  Do not cache queries to and answers from external atoms.\\
%%%%%%%%%%%%%%%%%%
\multicolumn{2}{l}{\texttt{--iauxinaux}} &&
  Keep auxiliary input predicates in auxiliary external atom predicates (can increase or decrease efficiency).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{2}{l}{\texttt{--constspace}} &&
  Free partial models immediately after using them. This may cause some models to be computed multiple times. (Not with monolithic.)
\end{longtable}

\subsection{Debugging and General Options}

\begin{longtable}{ p{2.0em} p{2.2cm} p{0.6cm} p{8.0cm} } 
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--dumpevalplan=F}} &
  Dump evaluation plan (usable as manual heuristics) to file \texttt{F}.\\
%%%%%%%%%%%%%%%%%%%
\texttt{-v}& \multicolumn{2}{l}{\texttt{--verbose[=N]}} &
  Specify verbose category (if option is used without [\texttt{=N}] then default is 1):\\
&\texttt{1}:&& Program analysis informations (including dot-file)\\
&\texttt{2}:&& Program modifications by plugins\\
&\texttt{4}:&& Intermediate model generation info\\
&\texttt{8}:&& Timing information (only if configured with \texttt{\texttt{--enable-benchmark}})\\
&&&Values are checked bitwise (sum up values for multiple categories).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--dumpstats}} &
  Dump certain benchmarking results and statistics in CSV format. (Only if configured with --enable-benchmark.)\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--graphviz=G}} &
  Specify comma separated list of graph types to export as .dot files. Default is none, graph types are:\\
&\texttt{dep}:&& Dependency Graph (once per program)\\
&\texttt{cycinp}:&& Graph for analysis cyclic predicate inputs (once per G\&C-eval unit)\\
&\texttt{comp}:&& Component Graph (once per program)\\
&\texttt{eval}:&& Evaluation Graph (once per program)\\
&\texttt{model}:&& Model Graph (once per program, after end of computation)\\
&\texttt{imodel}:&& Individual Model Graph (once per model)\\
&\texttt{attr}:&& Attribute dependency graph (once per program)\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--version}} &
  Shows version information.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-manualevalheuristicsplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--manualevalheuristics-enable}}\\
& & & Enable parsing and processing of ``\texttt{\#evalunit(...)}'' instructions.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-manualevalheuristicsplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--query-enable=[true,false]}}\\
& & & Enable or disable the querying plugin (default is disabled).\\
\multicolumn{3}{l}{\texttt{--query-brave}} &
  Do brave reasoning.\\
\multicolumn{3}{l}{\texttt{--query-all}} &
  Give all witnesses when doing ground reasoning. \\
\multicolumn{3}{l}{\texttt{--query-cautious}} &
  Do cautious reasoning.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-aggregateplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--aggregate-enable[=true,false]}}\\
& & & Enable aggregate plugin (default is enabled).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--aggregate-mode=[native,ext]}}\\
& & & Enable aggregate plugin (default is enabled).\\
&\texttt{native (default)}:&& Keep aggregates (but simplify them to some basic types).\\
&\texttt{ext}:&& Rewrite aggregates to an external atoms.\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{\texttt{--aggregate-allowaggextcycles}}\\
& & & Allows cycles which involve both aggregates and external atoms. If the option is not specified, such cycles lead to abortion; if specified, only a warning is printed but the models might be not minimal. With \texttt{--aggregate-mode=ext}, the option is irrelevant as aggregates are replaced by external atoms (models will be minimal in that case). See examples/aggextcycle1.hex..\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-strongnegationplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--strongnegation-enable[=true,false]}}\\
& & & Enable or disable strong negation plugin (default is enabled).\\ 
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-weakconstraintplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--weak-enable[=true,false]}}\\
& & & Enable or disable weak constraint plugin (default is enabled). \texttt{--weak-allmodels} Display all models also under weak constraints.\\ 
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-functionplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--function-maxarity=<N>}}\\
& & & Maximum number of output terms in functionDecompose.\\ 
%%%%%%%%%%%%%%%%%%%
\multicolumn{3}{l}{\texttt{--function-rewrite}} &
  Rewrite function symbols to external atoms.\\ 
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-choicePlugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--choice-enable[=true,false]}}\\
& & & Enable choice rules (default is enabled).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-conditionalLiteralPlugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--conditinal-enable[=true,false]}}\\
& & & Enable conditional literals (default is enabled).\\
%%%%%%%%%%%%%%%%%%%
\multicolumn{4}{l}{Plugin help for dlvhex-pythonplugin[internal]:}\\
\multicolumn{4}{l}{\texttt{--python-plugin=[PATH]}}\\
& & & Add Python script "PATH" as new plugin.\\
\multicolumn{3}{l}{\texttt{--python-main=PATH}} &
   Call method "main" in the specified Python script (with dlvhex support) instead of evaluating a program.\\
\multicolumn{3}{l}{\texttt{--python-arg=ARG}} &
  Passes arguments to Python (sys.argv) (can be used multiple times).\\
\end{longtable}

\section{Input-related warnings and errors}
\label{sec:inputRelatedWarnings}
This section explains the most frequent errors, warnings, and info messages related
to inappropriate inputs or command line options. All messages are printed to the
standard error stream.

Warning and error messages are prefixed with a number
that indicates the verbosity level of the message
(see \verb|--verbose| commandline option),
this is intended to allow for filtering
using \verb|grep| and similar tools.

\subsection{Syntax Errors}
In this section we consider errors emitted during the parsing and checking of logic programs.
These errors include information to ease finding and fixing the problem. Each of the error messages shows a line in which the error appears, followed by the type of the error and a short description.
\begin{align*}
 & \texttt{8 unparsed "go $\leftimpl$ goto(X)" }\\
 & \texttt{8 ----------\^{}} \\
 & \texttt{8 GeneralError:~Syntax Error:~Could not parse complete input!}
\end{align*}
%
To correct this error, investigate the indicated location and make sure the input conforms to the grammar in Section~\ref{sec:inputLang} (e.g., check for missing periods, unmatched parentheses).

\subsection{Plugin-related errors}
In this section we explain exceptions and errors 
which may occur while working with external atoms 
or plugins in which we have implemented desired external atom functionality (e.g. Python or C++ plugin). 

The following exception occurs whenever we try to
load a plugin from a nonexisting file, either from the Python or C++ file.
\begin{align*}
\texttt{Exception:~nonexisting\_file\_name.py:~no such file}
\end{align*}
$\texttt{nonexisting\_file\_name.py}$ does not exist in the current directory and should be replaced with
the right file which contains implementation for the external atom(s) used in \hex{}-program.

The following error occurs if we do not provide an external atom specification and implementation 
in the source file but we use it in the \hex{}-program. The error looks as below:
\begin{align*}
& \texttt{GeneralError:~Fatal:~did not find plugin atom for predicate}\\ 
& \texttt{"ext\_atom"}
\end{align*}  
From the description above we can see that there is no plugin atom for the predicate \texttt{ext\_atom}
in the source file which is passed as parameter from the command line.
%Implementation for the predicate \texttt{ext\_atom} should be added to the plugin source file.

Another error occurs if the output arity (i.e., the number of arguments in square or round brackes) of an external atom does not 
match its specification in the source file. The error is given below:
\begin{align*}
& \texttt{GeneralError:~External Atom \&rq[ind](C,A) has a wrong} \\
& \texttt{output arity (should be 1)}
\end{align*}  

\subsection{Safety Checking}
\label{safetyCheck}
If any of the variables used in the \hex{}-program
does not satisfy safety conditions listed below,
the program is not safe and an error occurs.
We use some examples and explanations 
from \cite{brfwilvpg2009} in the following. 

\subsubsection{Regular Safety}
\dlvhex{} imposes a safety condition on variables in rules. 
This guarantees that a rule has only finitely many ground instances.

\paragraph{Standard, Arithmetic and Comparative Predicates}
A variable $X$ in an aggregate-free rule is safe if at least one 
of the following conditions is satisfied:
\begin{itemize}
\item $X$ occurs in a positive standard predicate in the 
body of the rule
\item $X$ occurs in a strong negated standard predicate in 
the body of the rule
\item $X$ occurs in the last argument of an arithmetic 
predicate $A$ and all other arguments of $A$ are safe.
\end{itemize}
A rule is safe if all its variables are safe.
\begin{exmp} \textbf{Safe rules and Constraints}
\begin{align*}
a(X)& \leftimpl not \ b(X), c(X). \\
a(X)& \leftimpl X \geeq Y, node(X), node(Y).\\
a(Y)& \leftimpl number(X), \#precc(X,Y). \\
a(Z)& \leftimpl number(X), \#succ(X,Y),Z=X+Y.\\
    &\leftimpl number(X), number(Y), \#mod(X,Y,2).\\
    &\leftimpl a(Y), not \ b(Y), not \ c(Y). 
\end{align*}
\end{exmp}

\begin{exmp} \textbf{Unsafe Rules and Constraints}
\begin{align*}
a(X)  & \leftimpl b(Y).\\
a(X) &\vee \clasneg a(X). \\
a(X)&\leftimpl not \ b(X). \\
a(X)&\leftimpl number(Y), X=Y+Z. \\
a(X)&\leftimpl number(Y), \#succ(X,Y). \\
    & \leftimpl \nott \thinspace number(X), \#succ(X,Y). \\
    & \leftimpl \nott \thinspace b(Y).\\
    & \leftimpl X \geeq Y, node(X). 
\end{align*}
\end{exmp}

\paragraph{Aggregates}
A variable $X$ appearing in the symbolic set of an aggregate is safe if it does not appear elsewhere outside the aggregate atom and at least one of the following conditions is satisfied:
\begin{itemize}
\item $X$ occurs in a positive standard predicate in the symbolic set
\item $X$ occurs in a true negated standard predicate in the symbolic set
\item $X$ occurs in the last argument of an arithmetic predicate A in the symbolic set and all other arguments of A are safe
\end{itemize}
All other variables (including guards) appearing in an aggregate atom have to be made safe by some other literal of the body.
\begin{exmp} \textbf{Safe Rules and Constraints with Aggregates}
\begin{align*}
a(X) & \leftimpl node(X), \#count\{ V \colon edge(V,X)\} \geeq 0. \\
a(X) & \leftimpl node(X), \nott \#count\{ V \colon edge(V,X)\} = 0\\
& \leftimpl \#count\{V \colon edge(V,Y), \nott edge(Y,V)\}=X, X\geq2.\\
& \leftimpl \nott node(X), \#count\{ V \colon edge(V,Y)\}=X\\
\end{align*}
\end{exmp}

\begin{exmp} \textbf{Unsafe Rules and Constraints with Aggregates}
\begin{align*}
a(X) & \leftimpl \nott node(X), \#count\{V \colon edge(V,X)\} \geeq 0. \\
a(X) & \leftimpl node(X), \#count\{V \colon edge(V,X)\} \geeq Z. \\
a(X) & \leftimpl node(X), \#count\{V \colon edge(V,Y), \nott edge(V,Y)\} \geeq 0. \\
& \leftimpl \#count\{ V \colon edge(V,Y)\} \geeq 0, X > Y. \\
& \leftimpl \nott node(X), \#count\{V \colon edge(V,Y)\} > X. 
\end{align*}
\end{exmp}

\paragraph{Arithmetic predicates}
By evaluating a program with arithmetic predicates it is possible to derive new numeric constants, different from those already occurring in the program. In case of arithmetic rules, this could cause the non-termination of the evaluation so an error message is issued in this case.
\begin{exmp} \textbf{Non finite domain program}
\begin{align*}
& d(0). \\
& d(Y) \leftimpl d(X), Y=X+1.
\end{align*}
\end{exmp}
To safely evaluate this kind of programs an upper integer limit N has to be specified either on the command-line (cf. Section~\ref{sec:commandline}) or in the program using
\begin{align*}
  \texttt{\#maxint=N.}
\end{align*}


\paragraph{Complex Terms}
Evaluation of a program might not terminate if a complex term occurs in the head of a recursive rule.
\begin{exmp} \textbf{Non finite domain program}
\begin{align*}
p(0).&\\
p(f(X)) & \leftimpl q(X).\\
q(X) & \leftimpl p(X).
\end{align*}
\end{exmp}
Some programs can be safely evaluated even if there are complex terms appearing in the head of a rule. This is the case when all arguments of a functional term are restricted to range over a finite domain thanks to the presence of some other atoms in the body.
\begin{exmp} \textbf{Finite domain program}
\begin{align*}
p(0). & \quad r(0). \\
p(f(X)) & \leftimpl r(X), q(X). \\
q(X) & \leftimpl p(X).
\end{align*}
\end{exmp}
When a program is not recognized to have a finite domain and termination thus cannot be guaranteed, an error is issued. 

\subsubsection{Strong Safety}
By evaluating a program with external atoms
it is possible to derive new numeric constants,
different from those already occurring in the program.
Moreover it is possible to generate a cycle 
over such a value-inventing external atom.
Such a cycle can cause the non-termination
of the evaluation by generating (inventing)
more and more new constant terms.
In such programs the strong safety condition is violated.

An atom $b=\ext{g}{X}{Y}$ in a rule r of the program is \emph{strongly safe} if either there is no cyclic dependency over $b$   or every variable in $Y$ occurs also in a positive ordinary atom not depending on $b$. A program is safe, if every external atom in a rule is strongly safe. 


\begin{exmp} \textbf{Consider the following program:}
\label{strongSafetyExmp}
\begin{align*}
& \rowprefix{r_1} p(a). \\
& \rowprefix{r_2} q(aa). \\
& \rowprefix{r_3} s(Y) \leftimpl p(X), \ext{concat}{X,a}{Y}. \\
& \rowprefix{r_4} p(X) \leftimpl s(X), q(X).
\end{align*}
\end{exmp}
It is not \emph{strongly safe} because Y in the cyclic external atom $\ext{concat}{X,a}{Y}$ in $\row{r_3}$ does not occur in an
ordinary body atom that does not depend on $\ext{concat}{X,a}{Y}$.
When we run the above program with commandline option 
\texttt{--strongsafety} enabled
(cf. Section~\ref{sec:commandline}),
the following error is generated:
\begin{align*}
& \texttt{GeneralError:~Syntax Error:~[Rule] is not strongly safe!}  \\
& \texttt{Variable [Var] fails strong safety check in rule [Rule].}
\end{align*}
% PS: TODO does [Rule] and [Var] stand for the concrete rule and variable?
To make $\row{r_3}$ strongly safe we could add an ordinary atom in order to break the cycle. $\row{r_3}$ could be modified as follows:\mycenterline{$s(Y) \leftimpl p(X), \ext{concat}{X,a}{Y},q(Y).$} Adding atom $q(Y)$ makes program strongly safe since $Y$ appears in the body atom which does not depend on $\ext{concat}{X,a}{Y}$.
 
Along with the error message, the affected \texttt{[Rule]} and a list of all unsafe variable occurrences \texttt{[Var]} are reported. 
The first action to take usually consists of checking whether variable \texttt{[Var]} is actually in the scope of any atom (in the positive body of \texttt{[Rule]}) that can bind it. It can also be helpful to check for variables that occur in aggregate elements (cf. Section~\ref{aggregates}) or conditional literals (cf. Section~\ref{conditions}),
it might be necessary to constraint them
using additional positive atoms in conditions. 


\subsubsection{Liberal Safety}
Strong domain-expansion safety is overly restrictive, as it also excludes programs that are clearly finitely groundable.
To overcome unnecessary restrictions of strong safety, liberal domain-expansion safety (lde-safety)
has been introduced \cite{eite-etal-14a}, which incorporates both syntactic and semantic properties of a program. All lde-safe programs have finite groundings with the same answer sets.

Unlike strong safety, liberal de-safety is not a property of entire atoms but of argument positions of atoms which we call attributes.
Intuitively, an attribute is lde-safe, if the number of different terms in
an answer-set preserving grounding (i.e. a grounding which has the same answer sets if restricted to the
positive atoms as the original program) is finite. A program is lde-safe, if all its attributes are lde-safe \cite{efikrs2015}.

Since the program from Example~\ref{strongSafetyExmp} is finitely restrictable, the cycle is ``broken'' by $\mathit{q(X)}$ in $\row{r_4}$, it is also \emph{liberally safe}.
The program can be evaluated successfully while option \texttt{--liberalsafety} is enabled (cf. Section~\ref{sec:commandline}). The output is as follows.
\begin{align*}
\{ & 
\texttt{p(a),q(aa),p(aa),s(aa),s(aaa)}
\}
\end{align*}
For more details about liberal safety we refer to \cite{eite-etal-14a}.

%\newpage
\bibliographystyle{amsplain}
\bibliography{Manual}
\end{document}