thesis.tex

% !TeX spellcheck = it_IT
\documentclass[12pt,a4paper,openright]{book}  % oneside  % openright

% ****************************************************************
%   PACKAGES
\usepackage{lmodern}         % font package.
\usepackage[T1]{fontenc}     % define T1 charset for out files.
\usepackage[italian]{babel}  % italian latex typo conventions.
\usepackage[utf8]{inputenc}  % italian symbols.
\usepackage{csquotes}        % needed by babel.
\usepackage{amsmath}         % math features.
\usepackage{amsthm}          % math theorems.
\usepackage{amssymb}         % math symbols.
\usepackage{amsbsy}			 % math bold.
\usepackage{listings}        % embed programming language in latex.
\usepackage{stmaryrd}        % symbols for theoretical computer science.
\usepackage{hhline}          % better horizontal lines in tabulars and arrays.
%%\usepackage{vmargin}         % various page dimensions.
\usepackage{hyperref}        % hypertext support.
\usepackage{makeidx}         % for creating indexes.
\usepackage{nicefrac}        % inline fractions.
\usepackage{marginnote}      % notes in the margin, even where \marginpar fails.
\usepackage{xr}              % references to other latex documents.
\usepackage{subfiles}        % multifile support.
\usepackage{geometry}        % interface for document dimension.
\usepackage{graphicx}        % enhanced support for graphics.
\usepackage{fancyhdr}        % extensive control of page headers and footers.
\usepackage{lipsum}          % generate dummy text.
\usepackage[
	backend=biber,
	style=numeric,
	citestyle=numeric  % numeric, alphabetic
]{biblatex}                  % bib management. %bibtex
\usepackage{minitoc}         % table of contents per chapter.
\usepackage{listings}        % code sections, http://ctan.org/pkg/listings
\usepackage{titlesec}        % change titles size.
\usepackage{algorithm}       % algorithm block.
\usepackage{algcompatible}
\usepackage{algpseudocode}   % style for (autoimported) package algorithmicx.
\usepackage{float}           % float management.
\usepackage[toc,page]{appendix}  % appendix.
\usepackage{tcolorbox}
%\usepackage{minted}
\usepackage{tikz}            % flow chart.
\usepackage{tocvsec2}        % numbering chapter fix.
\usepackage{enumitem}        % enums.
%\usepackage{subcaption}      % needed by nested figures.
%\usepackage{showframe}      % DEBUG: shows page frames.

% ****************************************************************
%   CONFIGS
%\hypersetup{                                  % hyperlinks color
%  colorlinks=true,
%  urlcolor=blue,
%  linkcolor=blue
%}
\dominitoc                                    % minitoc setup
\lstset{                                      % listing setup
  basicstyle=\ttfamily,
  mathescape,
  columns=fullflexible,
  keepspaces=true
}
\addto{\captionsitalian}{%                    % custom translations
  \renewcommand{\mtctitle}{Sommario}%
  \renewcommand{\appendixtocname}{Appendice}%
  \renewcommand{\appendixpagename}{Appendice}%
}
\renewcommand{\listalgorithmname}{Elenco degli algoritmi}
\floatname{algorithm}{Algoritmo}
\newenvironment{dedication}                   % dedication setup
  {%\clearpage           % we want a new page          %% I commented this
   \thispagestyle{empty}% no header and footer
   \vspace*{\stretch{1}}% some space at the top
   \itshape             % the text is in italics
   \raggedleft          % flush to the right margin
  }
  {\par % end the paragraph
   \vspace{\stretch{3}} % space at bottom is three times that at the top
   \clearpage           % finish off the page
  }
\titleformat*{\subsubsection}{               % subsubsection size
  \large\bfseries
}
\usetikzlibrary{calc,trees,positioning,arrows,chains,shapes.geometric,%
	decorations.pathreplacing,decorations.pathmorphing,shapes,%
	matrix,shapes.symbols}
\tikzset{
                                   % flow chart
>=stealth',
punktchain/.style={
	rectangle,
	rounded corners,
	% fill=black!10,
	draw=black, very thick,
	text width=10em,
	minimum height=3em,
	text centered,
	on chain},
line/.style={draw, thick, <-},
element/.style={
	tape,
	top color=white,
	bottom color=blue!50!black!60!,
	minimum width=8em,
	draw=blue!40!black!90, very thick,
	text width=10em,
	minimum height=3.5em,
	text centered,
	on chain},
every join/.style={->, thick,shorten >=1pt},
decoration={brace},
tuborg/.style={decorate},
tubnode/.style={midway, right=2pt},
}

% ****************************************************************
%   RESOURCES
\subfile{prooftree}
\input{macros.tex}
\addbibresource{biblio.bib}



% ****************************************************************
% @@@@@@                     DOCUMENT                       @@@@@@
% ****************************************************************
\begin{document}

%%% *******************************************************
%%% Opening page   ****************************************
\begin{titlepage}
    \begin{center}
        \includegraphics[width=0.4\textwidth]{img/logo_unipr.png}

		\vspace{0.5cm}

		% *** university details
		\Large
        \textsc{Dipartimento di Scienze Matematiche,\\
        Fisiche e Informatiche}

        \vspace{0.5cm}

        \Large
        \textsc{Corso di Laurea in Informatica}

		\vspace{1.1cm}
		%\noindent\hrulefill

 		% *** title
        \Huge
        \textbf{Progettazione e implementazione in Picat di un
          risolutore per vincoli insiemistici}

 		% *** subtitle
        \vspace{1cm}
        \LARGE
        Design and Implementation in Picat of a Set Constraint Solver

		\vspace{1.3cm}
		%\noindent\hrulefill

 		% *** authors
		%\large Candidato: \Large Luca \textsc{Parolari}\\
		%\large Relatore: \Large Gianfranco \textsc{Rossi}

		\begin{minipage}{0.4\textwidth}
			\begin{flushleft}
				\large
				\textit{Relatore}\\
				Prof. Gianfranco \textsc{Rossi}
			\end{flushleft}
		\end{minipage}
		\begin{minipage}{0.4\textwidth}
			\begin{flushright}
				\large
				\textit{Candidato}\\
				Luca \textsc{Parolari}
			\end{flushright}
		\end{minipage}

        \vfill

 		\large
        Anno Accademico 2018/2019

    \end{center}
\end{titlepage}



%%% *******************************************************
%%% Dedica   **********************************************
\thispagestyle{empty}
\cleardoublepage

\begin{dedication}
A mio nonno, Luigi.
\end{dedication}

\thispagestyle{empty}



%%% *******************************************************
%%% Table of contents   ***********************************
\tableofcontents



%%% *******************************************************
%%% Introduzione   ****************************************
\setsecnumdepth{none}
\chapter{Introduzione}
\resetsecnumdepth

\label{ch:intro}

L'ambito dei linguaggi basati su insiemi è da sempre un ambito
affascinante nonché di particolare rilevanza per la risoluzione di
certe classi di problemi. Avere strumenti in grado di trattare in modo
automatico operazioni su insiemi (incluse relazioni binarie e funzioni
parziali, che sono comunque un tipo particolare di insiemi) è di ovvio
interesse in vari settori: dalla dimostrazione di teoremi alla
programmazione con vincoli.

Una proposta in tal senso è quella di \clpset{} \cite{Dovier00}, con
il suo linguaggio a vincoli basato su insiemi \lset{}. \clpset{}
fornisce all'utente una forma molto generale di insiemi, detti
\emph{untyped hereditarily finite hybrid sets} (letteralmente, insiemi
ibridi ereditariamente finiti non tipizzati). \clpset{} è dotato di un
solver (denominato \satset{}) che implementa una procedura decisionale
in grado di risolvere le formule del primo ordine senza quantificatori
su un universo di insiemi ereditariamente finiti. Lavori successivi
hanno mostrato come estendere \clpset{} in modo tale che relazioni e
funzioni parziali siano entità primitive del linguaggio. Il linguaggio
che ne è risultato, denominato \lbr{}, offre insiemi, relazioni
binarie e funzioni parziali, con le relative operazioni di base su
essi \cite{Rossi18}.

Attualmente \lset{} , con le sue estensioni introdotte in \lbr{}, è
implementato in Prolog, all'interno dello strumento di programmazione
logica \setlog{} \cite{SetLog}.

L'obiettivo di questo lavoro di tesi è la realizzazione del solver
\satset{} per \lset{}, utilizzando il linguaggio di programmazione
Picat.

Picat \cite{PicatLang} è un linguaggio logico piuttosto innovativo che
ricalca nel core il funzionamento di un linguaggio logico, ma possiede
alcune caratteristiche che lo rendono un candidato ideale per
sperimentare l'implementazione del solver per \lset{}.

\bigskip

\noindent Il resto di questo elaborato di tesi è strutturato come
segue.
\begin{itemize}
	\item Il capitolo \ref{ch:clpbasedlang} presenta la sintassi e
          la semantica del linguaggio \lset{}, con la procedura di
          risoluzione del solver \satset{}. A corredo viene data una
          panoramica generale del CLP (Constraint Logic
          Programming). Successivamente si descrivono le regole di
          riscrittura, utilizzate dal solver per la risoluzione dei
          vincoli di \lset{}.
	\item Il capitolo \ref{ch:picat} descrive Picat in forma
          generale: sono trattate le sue caratteristiche e
          funzionalità (di base e avanzate), finendo con una
          descrizione delle differenze tra Picat e Prolog, il più
          diffuso linguaggio logico.
	\item Il capitolo \ref{ch:lsetpicat} descrive la realizzazione
          del solver in Picat, trattando aspetti progettuali, problemi
          riscontrati e caratteristiche implementative.
	\item Nel capitolo \ref{ch:impl} viene data una descrizione
          più dettagliata dell'implementazione delle regole di
          riscrittura utilizzate dal solver, mostrando come la
          descrizione astratta di \lset{} venga tradotta in un
          programma Picat.
	\item Il capitolo \ref{ch:use} mostra come è possibile
          utilizzare il solver realizzato: tramite modalità
          interattiva o tramite API.
	\item Il capitolo \ref{ch:conclusion} fornisce una panoramica
          del lavoro svolto e accenna a possibili lavori futuri.
\end{itemize}

\thispagestyle{fancy}
\renewcommand{\headrulewidth}{0pt}
\lhead{\thepage}
\rhead{INTRODUZIONE}
\cfoot{}



%%% *******************************************************
% Linguaggi a vincoli basati su insiemi   *****************
\chapter{Linguaggio a vincoli basato su insiemi}
\label{ch:clpbasedlang}

%\minitoc

In questo capitolo viene presentato e contestualizzato un linguaggio
orientato alla risoluzione di formule insiemistiche denominato
\lset{}. \lset{} è un linguaggio logico definito come parte del
linguaggio di programmazione logica a vincoli (o Constraint Logic
Programming, abbreviato CLP) \clpset{} \cite{Dovier00}.

\clpset{} (e quindi il suo linguaggio a vincoli \lset{}) è stato
implementato in Prolog nello strumento \setlog{} \cite{SetLog};
inoltre \lset{} è stato implementato in Java come parte della libreria
\jsetl{} \cite{JSetL}. Obiettivo principale di questo lavoro di tesi è
quello di dare un'implementazione di \lset{} utilizzando il linguaggio
di programmazione Picat \cite{PicatLang}.

Nella sezione \ref{sec:clpbasedlang_clp} è descritto il paradigma di
programmazione logico a vincoli in forma molto discorsiva e
introduttiva, mentre in \ref{sec:clpbasedlang_lset} si dà una
presentazione di \lset{}: sintassi, semantica, solver e regole di
riscrittura.

\section{Constraint Logic Programming}
\label{sec:clpbasedlang_clp}

Nel campo dell'informatica la logica trova molteplici applicazioni, in
particolare nell'ambito dell'intelligenza artificiale. La logica
classica si può suddividere in due classi principali: la \emph{logica
  proposizionale} e la \emph{logica dei predicati}.  I più comuni
linguaggi logici sono basati su un sottoinsieme della logica dei
predicati del primo ordine, che permette di garantire la correttezza
delle soluzioni ma non la terminazione del programma. Entrambe,
comunque, permettono di esprimere proposizioni (frasi) e relazioni tra
posizioni. La principale differenza tra le due è l'espressività. Ciò
che può essere espresso nella logica dei predicati può essere espresso
nella logica proposizionale, ma non viceversa. La logica dei predicati
consente di utilizzare \textbf{variabili} e quantificazioni su di
esse, mentre nella logica proposizionale non è possibile.

La logica dei predicati, sotto opportune ipotesi, può diventare un
vero e proprio linguaggio di programmazione, prendendo appunto il nome
di Logic Programming (abbreviato LP) (per approfondire i concetti di
programmazione logica si veda ad esempio \cite{Console97}).

Il Logic Programming è un paradigma di programmazione dove gli
statements del programma rappresentano fatti o regole, espressi
tramite qualche logica formale, di un problema. La logica viene
utilizzata come meccanismo formale per analizzare le inferenze in
termini di operazioni su espressioni simboliche, dedurre conseguenze
da un insieme di premesse, studiare la verità (o falsità) di un
insieme di proposizioni, data la verità (o falsità) di altre
proposizioni e dimostrare la validità di una teoria.

Spesso i linguaggi di programmazione di questo tipo adottano un
approccio dichiarativo, descrivendo solamente la forma della soluzione
e non la procedura per ottenerla (e.g., il Datalog). Per i linguaggi
come il Prolog o Picat invece l'approccio può essere ibrido: il
paradigma dichiarativo, imperativo e procedurale si intersecano
lasciando al programmatore la scelta del paradigma da utilizzare.

La programmazione logica a vincoli (CLP) estende la programmazione
logica introducendo il concetto di \emph{vincolo}. Un programma CLP
contiene fatti e regole come un programma LP, con la differenza che
nel programma CLP il corpo delle clausole può presentare vincoli. Per
i CLP il risultato di una dimostrazione è quindi un insieme di vincoli
(contraint store) e/o un valore letterale valido in quell'insieme di
vincoli.

La programmazione logica a vincoli può essere utilizzata per risolvere
\emph{Contraint Satisfaction Problem} (spesso abbreviato in
\emph{CSP}). Un problema di soddisfacimento di vincoli è una tripla
composta da
\begin{itemize}
	\item un insieme $X$ di variabili ${X_1, \ldots, X_n}$;
	\item un insieme $D$ di domini ${D_1, \ldots, D_n}$, uno per
          variabile;
	\item un insieme $C$ di vincoli che specificano le
          combinazioni di valori possibili per le variabili.
\end{itemize}

Ogni dominio $D_i$ specifica un insieme di valori possibili per la
variabile $X_i$. Dato che i CSP sono parametrici rispetto al dominio
dei vincoli, anche il supporto alla risolzuione lo diventa: da qui il
nome \clpset{}. Si utilizzerà per la loro risoluzione un'opportuna
istanza dello schema generale CLP. Ad esempio se il dominio è quello
degli insiemi allora si potrebbe utilizzare \clpset{}.

\section{Il linguaggio logico a vincoli \lset{}}
\label{sec:clpbasedlang_lset}

\lset{} è un linguaggio logico per la gestione di vincoli su
insiemi. \lset{} è stato inizialmente introdotto come parte del
linguaggio \clpset{} \cite{Dovier00}. Da un punto di vista più
generale \clpset{} è un istanza dei CLP sopra descritti, dove il
dominio di applicazione dei vincoli è quello insiemistico.

Uno degli obiettivi primari di \clpset{} è di essere molto flessibile
e fornire forme generali per la manipolazione di insiemi e relative
operazioni, in quanto la nozione di \emph{set} è una componente comune
nella progettazione di programmi, ma sono pochi i linguaggi che
forniscono gli insiemi come struttura dati elementare.  Sempre in
\cite{Dovier00} vengono menzionate alcune eccezioni di linguaggi che
si basano su insiemi: SETL, B e il linguaggio Z, utilizzato per
descrivere la specifica formale di programmi. Qualche eccezione esiste
anche nel campo dei \emph{database deduttivi} e, più recentemente,
anche come \emph{general purpose programming language}. Ad ogni modo,
questi linguaggi impongono dei limiti sul tipo di insiemi esprimibili
o sulle capacità computazionali degli stessi. Ad esempio, in molti
ambiti, si richiede che gli insiemi siano totalmente specificati: non
sono ammesse \emph{variabili} libere.

In \lset{} gli insiemi sono visti come un tipo di dato primitivo del
linguaggio, ovvero termini della logica del primo ordine. I predicati
predefiniti invece sono visti come vincoli predefiniti del linguaggio,
gestiti con procedure di risoluzione di vincoli. La classe di insiemi
considerata vuole essere molto generale: gli insiemi possono essere
annidati e/o parzialmente specificati. Gli insiemi parzialmente
specificati possono contenere variabili come elementi dell'insieme o
come parte dell'insieme stesso.

Di seguito si forniscono le specifiche di \lset{} definendone prima la
sintassi (\ref{subsec:clpbasedlang_lset_sintax}) e poi la semantica
informale (\ref{subsec:clpbasedlang_lset_semantics}). In
\ref{subsec:clpbasedlang_lset_solver} viene descritto il funzionamento
in termini astratti del risolutore di formule per questo linguaggio,
implementato in questo lavoro di tesi, mentre in
\ref{subsec:clpbasedlang_lset_rewriteeq},
\ref{subsec:clpbasedlang_lset_rewriteset} e
\ref{subsec:clpbasedlang_lset_rewriteneg} sono trattate
rispettivamente le regole di riscrittura per vincoli di uguaglianza,
vincoli su insiemi e vincoli negativi.

\subsection{Sintassi}
\label{subsec:clpbasedlang_lset_sintax}

La sintassi del linguaggio \lset{} si basa sui seguenti insiemi di
simboli:

\begin{itemize}
	\item $\calF$ è un insieme di costanti e simboli di funzione
          definito da:
	\begin{itemize}
		\item $\emptyset \in \calF$,
		\item $\{ \cdot \mid \cdot \} \in \calF$ e $int \in
                  \calF$, simboli relazione binaria,
		\item $\calF_0 \subset \calF$, dove $\calF_0$ è un
                  insieme di costanti e simboli di funzione non
                  interpretati;
	\end{itemize}
	\item $\prod_C = \{ =, in, un, disj, set \}$, insieme di
          simboli di predicato;
	\item $\calV$ è un insieme numerabile di simboli di variabile.
\end{itemize}

I \calset{}-\textit{termini} sono termini costruiti a partire dai
simboli di $\calF$ e $\calV$ nel modo usuale. Ad esempio, i seguenti,
sono termini insiemistici ($set-terms$):
\begin{itemize}
	\item $\{1 \mid \emptyset \} \equiv \{1\}$
	\item $\{1 \mid \{2 \mid \emptyset \} \} \equiv \{1,2\}$
	\item $\{1 \mid \{2 \mid X \} \} \equiv \{1,2 \mid X \}$
\end{itemize}

I \calset{}-\textit{constraint} atomici (o primitivi) sono predicati
atomici costruiti a partire dai simboli di $\prod_C$ nel modo
usuale. Ad esempio, i seguenti, sono \calset{}-\textit{constraint}
primitivi:
\begin{itemize}
	\item $X = 1$
	\item $un(\{1\}, \emptyset, R)$
\end{itemize}

Le \calset{}-\textit{formule} (o \calset{}-\textit{constraint}
composti) sono combinazioni $\wedge$ (and) e $\vee$ (or) di
\calset{}-\textit{constraint} primitivi. Le seguenti formule sono
esempi di \calset{}-\textit{constraint} composti:
\begin{itemize}
	\item $1\ in\ R \land 1\ nin\ S \land un(R,S,T) \land T = \{X\}$
	\item $(X\ in\ S \land X\ neq\ 1) \lor (X\ nin\ S \land X = 1)$
\end{itemize}

\subsection{Semantica informale}
\label{subsec:clpbasedlang_lset_semantics}

La semantica intuitiva dei vari simboli in $\sum_{\mathcal{SET}}$ è la
seguente:

\begin{itemize}
	\item $\emptyset$ rappresenta l'insieme vuoto;
	\item $\{\cdot\mid\cdot\}$ rappresenta il costruttore di
          insiemi definito come $\{t\mid s\} = \{t\}\ \cup s$;
	\item il predicato $=$ rappresenta la relazione di
          uguaglianza;
	\item il predicato \textit{in} rappresenta la relazione di
          appartenenza;
	\item il predicato \textit{un} rappresenta la relazione di
          unione insiemistica definita come $un(r,s,t) = true
          \Longleftrightarrow t = r \cup s$;
	\item il predicato \textit{disj} rappresenta la relazione di
          disgiunzione insiemistica definita come $disj(r,s) = true
          \Longleftrightarrow r \cap s = \emptyset$;
	\item il predicato \textit{set} controlla che il termine sia
          un insieme.
\end{itemize}
%\subsubsection{Vincoli}

\subsection{Il solver \satset{}}
\label{subsec:clpbasedlang_lset_solver}

La procedura \satset{} risolve i vincoli e rappresenta il solver del
linguaggio \lset{}. Il seguente algoritmo ne descrive la struttura.

\begin{algorithm}
	\caption{Procedura \satset{}}
	\begin{algorithmic}[1]
		\Procedure{\satset{$(C)$}}{}
		\State $C \gets $ \texttt{sort\_infer($C$)};
		\Repeat
		\State $C'$ $\gets C;$
		\Repeat
		\State $C'' \gets C;$
		\State $C \gets $ \texttt{STEP($C$)};
		\Until {$C$ = $C''$;}
		\State $C \gets $ \texttt{remove\_neq($C$)};
		\Until {$C'$ = $C$;}
		\State
		\State\Return $C$;
		\EndProcedure
	\end{algorithmic}
	\label{alg:pseudo_satset}
\end{algorithm}

Essenzialmente \satset{$(C)$} utilizza tre procedure:

\begin{itemize}
	\item \textbf{\texttt{sort\_infer}}: aggiunge alla
          \calset{}-\textit{formula} $C$ i vincoli \textbf{set} e
          \textbf{integer} per assicurare che gli oggetti utilizzati
          nei vincoli siano del tipo corretto.

	\item \textbf{\texttt{STEP}}: applica speciali \textit{regole
          di riscrittura} alla formula $C$ corrente e ritorna
          \textit{false} oppure la formula modificata. L'esecuzione di
          $STEP$ viene iterata fino ad arrivare a ottenere una
          formula in forma irriducibile. Notare che $STEP$ ritorna
          $false$ se almeno uno dei vincoli in $C$ viene riscritto a
          $false$. Anche $STEP(false)$ ritorna $false$.

	\item \textbf{\texttt{remove\_neq}}: tratta l'eliminazione dei
          $\neq-constraints$ nel caso in cui coinvolgano variabili
          insiemistiche che appaiono anche in vincoli di unione in
          forma risolta.
\end{itemize}

Quando la computazione non-deterministica di $\satset{}(C)$ termina,
se il risultato è $false$ allora si può concludere che $C$ non è
soddisfacibile; al contrario, se nessuno dei vincoli in $C$ viene
riscritto a $false$ allora ogni soluzione generata da \satset{} è una
soluzione per $C$ e viceversa.

\subsection{Regole di riscrittura per vincoli di uguaglianza}
\label{subsec:clpbasedlang_lset_rewriteeq}

Nelle sezioni successive sono riportate le regole di riscrittura
descritte in \cite{Rossi18}, trattate durante la realizzazione del
solver.

L'implementazione di queste regole in Picat è riportata nel capitolo
\ref{ch:impl}.

\subsubsection{Il vincolo eq}

\textit{Sintassi:} $t_1 = t_2$.\\
\noindent\textit{Semantica informale:} $t_1$ e $t_2$ sono uguali.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:eq_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{=\textsubscript{\arabic{equation}}}

		If $x, y, t, t_i, u_i: \text{U}; A,B: \text{Set}$ then:

		\begin{equation}
		\dotx = \dotx \to true
		\end{equation}
		\begin{equation}
		\text{If } t \not\in \calV, t = \dotx \to \\ \dotx = t
		\end{equation}
		\begin{equation}
		\text{If} \dotA \not\in vars(t_1, \ldots, t_n), \dotA = \{ t_1, \ldots, t_n \} \to \dotA = \{ t_1, \ldots, t_n \sqcup N \}
		\end{equation}
		\begin{equation}
		\text{If} \dotx \in vars(t), \dotx = t \to false
		\end{equation}
		\begin{equation}
		\dotx = t \to \text{substitute $\dotx$ by $t$ in all others literals of the input formula}
		\end{equation}
		\begin{equation}
		\text{If} f \not\equiv g, f(t_1, \ldots, t_n) = g(t_1, \ldots, t_m) \to false
		\end{equation}
		\begin{equation}
		\begin{split}
		\{ t_1, & \ldots, t_m \sqcup \dotA \} = \{u_1, \ldots, u_n \sqcup \dotA \} \to \\
		& t_1 = u_j \land \{ t_2, \ldots, t_m \sqcup \dotA \} = \{ u_1, \ldots, u_{j_1}, u_{j+1}, \ldots, u_n \sqcup \dotA \} \\
		& \lor t_1 = u_j \land \{ t_1, \ldots, t_m \sqcup \dotA \} = \{ u_1, \ldots, u_{j_1}, u_{j+1}, \ldots, u_n \sqcup \dotA \} \\
		& \lor t_1 = u_j \land \{ t_2, \ldots, t_m \sqcup \dotA \} = \{ u_1, \ldots u_n \sqcup \dotA \} \\
		& \lor \dotA = \{ t_1 \sqcup N \} \land \{ t_2, \ldots, t_m \sqcup N \} = \{ u_1, \ldots, u_n \sqcup N \}
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		\{ x \sqcup & A \} = \{ y \sqcup B \} \to \\
		& x = y \land A = B \\
		& \lor x = y \land \{ x \sqcup A \} = B \\
		& \lor x = y \land A = \{ y \sqcup B \} \\
		& \lor A = \{ y \sqcup N \} \land \{ x \sqcup N \} = B
		\end{split}
		\end{equation}
		\begin{equation}
		f(t_1, \ldots, t_n) = f(u_1, \ldots, u_n) \to t_1 = u_1 \land \ldots \land t_1 = u_n
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di uguaglianza}
	\label{fig:eq_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $\dotx = t$ e $\dotx$ non è contenuto ne in $t$ ne in
          altri letterali della formula.
\end{itemize}

\paragraph{Implementazione}
Algoritmo \ref{alg:eq_constraints}

\paragraph{Esempio}
Esempio di riscrittura del vincolo composto $\{1,2\} = \{X,Y\} \land X \neq 1$.
Di seguito sono riportate le riscritture compiute per giungere al risultato.

\begin{itemize}
	\item Viene applicata la regola $eq_8$\\ 
	  \[
	  \begin{split}
	    \{ 1, 2 \} &= \{ X, Y \} \land X \neq 1 \to \\
	      & (1 = X \land 2 = Y \\
	      & \lor 1 = X \land \{ 1,2 \} = Y \\
	      & \lor 1 = X \land 2 = \{ X,Y \} \\
	      & \lor 2 = \{ X \sqcup N \} \land \{ 1 \sqcup N \} = Y)  \land X \neq 1
	  \end{split}
	  \]
	  che può essere semplificata in 
	  \[
	    \begin{split}
	      \{ 1, 2 \} &= \{ X, Y \} \land X \neq 1 \to \\
	  	    & \{2\} = \{ X \sqcup N \} \land \{ 1 \sqcup N \} = \{Y\}  \land X \neq 1
        \end{split}
	  \]
	  per il primo termine, mentre il secondo ($X \neq 1$) è irriducibile e viene mantenuto nel constraint store.
	\item Per il primo e secondo termine viene applicata la regola $eq_8$, mentre il terzo è irriducibile
	  \[
	    \begin{split}
	      \{2\} &= \{ X \sqcup N \} \land \{ 1 \sqcup N \} = \{Y\}  \land X \neq 1 \to \\
	        & (2=X \land \emptyset=\{N\} \\
	        & \lor 2=X \land \{2\}=\{N\} \\
	        & \lor 2=X \land \emptyset = \{ X \sqcup N \} \\
	        & \lor \emptyset = \{X \sqcup N'\} \land \{ 2 \sqcup N'\} = \{ N\}) \\
	        & \land \\
	        & (1=Y \land \{N\} = \emptyset \\
	        & \lor 1=Y \land \{1 \sqcup N\} = \emptyset \\
	        & \lor 1=Y \land \{N\} = \{Y\} \\
	        & \lor \emptyset = \{Y \sqcup N'' \} \land \{1 \sqcup N''\} = \emptyset) \\
	        & \land \\ 
	        & X \neq 1
	    \end{split}
	  \]
	  tramite la quale otteniamo subito un risultato ponendo $X=2$, $Y=1$ e $N=\emptyset$
\end{itemize}

\subsubsection{Il vincolo neq}

\textit{Sintassi:} $t_1 \neq t_2$.\\
\noindent\textit{Semantica informale:} $t_1$ è diverso da $t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:neq_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{$\neq$\textsubscript{\arabic{equation}}}

		If $t, t_i: \text{U}; A,B: \text{Set}$ then:

		\begin{equation}
		\text{If } t \text{ is a constant or } t \in \calV, t \neq t \to false
		\end{equation}
		\begin{equation}
		\text{If } t \not\in \calV, t \neq \dotx \to \dotx \neq t
		\end{equation}
		\begin{equation}
		\text{If} \dotx \not\in vars(t_1, \ldots, t_n), \dotx \neq \{ t_1, \ldots, t_n \sqcup \dotx \} \to t_1 \not\in \dotx \lor \ldots \lor t_n \not\in \dotx
		\end{equation}
		\begin{equation}
		\text{If} \dotx \in vars(t), \dotx \neq t \to true
		\end{equation}
		\begin{equation}
		\begin{split}
		\{ t_1 \sqcup & A \} = \{ t_2 \sqcup B \} \to \\
		& N \in \{ t_1 \sqcup A \} \land N \not\in \{ t_2 \sqcup B \} \\
		& N \not\in \{ t_1 \sqcup A \} \land N \in \{ t_2 \sqcup B \}
		\end{split}
		\end{equation}
		\begin{equation}
		f(t_1, \ldots, t_n) \neq g(u_1, \ldots, u_m) \to true
		\end{equation}
		\begin{equation}
		f(t_1, \ldots, t_n) = f(u_1, \ldots, u_n) \to t_1 \neq u_1 \land \ldots \land t_1 \neq u_n
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di disuguaglianza}
	\label{fig:neq_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $\dotx \neq t$ e $\dotx$ non compare ne in $t$ ne come
          argomento di qualunque predicato $p(\ldots)$, $p \in \{ un,
          id, inv, comp \}$.
\end{itemize}

\paragraph{Implementazione}
Algoritmo \ref{alg:neq_constraints}

\subsection{Regole di riscrittura per vincoli (positivi) su insiemi}
\label{subsec:clpbasedlang_lset_rewriteset}

\subsubsection{Il vincolo in}

\textit{Sintassi:} $t_1 \in t_2$.\\
\noindent\textit{Semantica informale:} se $t_2$ è un insieme, $t_1$ è un membro di $t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:in_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{$\in$\textsubscript{\arabic{equation}}}

		If $x, y: \text{U}; A: \text{Set}$ then:

		\begin{equation}
		x \in \emptyset \to false
		\end{equation}
		\begin{equation}
		x \in \{ y \sqcup A \} \to x = y \lor x \in A
		\end{equation}
		\begin{equation}
		x \in \dotA \to \dotA = \{ x \sqcup N \}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di appartenenza}
	\label{fig:in_constraints}
\end{figure}

\paragraph{Forme irriducibili} Nessuna.

\paragraph{Implementazione}
Algoritmo \ref{alg:in_constraints}

\paragraph{Esempio}
Esempio di riscrittura del vincolo composto $1 \in X \land 1 \not\in
X$. Di seguito sono riportate le riscritture compiute per giungere al
risultato.

\begin{itemize}
	\item Viene applicata la regola $\in_3$ e la regola
          ``irriducibile'' per $\not\in$.\\
	  \[
	  \begin{split}
	    1 \in X &\land 1 \not\in X \to \\ & X = \{ 1 \sqcup N \}
              \\ & \land 1 \not\in X
	  \end{split}
	  \]
	\item Viene applicata la regola $eq_5$ e $X$ viene unificato a
          $\{ 1 \sqcup N\}$, quindi
	  \[
	    \begin{split}
	      X = \{ 1 \sqcup N \} \land 1 \not\in X \to 1 \not\in \{1 \sqcup N\}
	    \end{split}
	  \]
	\item Viene applicata la regola $in_5$
	  \[
	    1 \not\in \{1 \sqcup N\} \to 1 \neq 1 \land 1 \not\in N
	  \]
	\item $1 \neq 1$, provoca il fallimento: la formula non è
          soddisfacibile.
\end{itemize}

\subsubsection{Il vincolo union}

\textit{Sintassi:} $un(t_1, t_2, t_3)$.\\
\noindent\textit{Semantica informale:} se $t_1, t_2$ e $t_3$ sono insiemi,  allora $t_3 = t_1 \cup t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:un_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{$\cup$\textsubscript{\arabic{equation}}}

		If $t: \text{U}; A, B, C: \text{Set}$ then:

		\begin{equation}
		un(A,A,B) \to A = B
		\end{equation}
		\begin{equation}
		un(A,B,\emptyset) \to A = \emptyset \land B = \emptyset
		\end{equation}
		\begin{equation}
		un(\emptyset,A,\dotB) \to \dotB = A
		\end{equation}
		\begin{equation}
		un(A,\emptyset,\dotB) \to \dotB = A
		\end{equation}
		\begin{equation}
		\begin{split}
		un & (\{ t \sqcup C \}, A, \dotB) \to \\
		& (t \not\in A \land un(N_1, A, N) \\
		& \lor A = \{ t_1 \sqcup N_2 \} \land un(N_1, N_2, N) ) \\
		& \land \{ t\sqcup C \} = \{ t \sqcup N_1 \} \land \dotB = \{ t\sqcup N \}
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		un & (A, \{ t \sqcup C \}, \dotB) \to \\
		& (t \not\in A \land un(N_1, A, N) \\
		& \lor A = \{ t_1 \sqcup N_2 \} \land un(N_1, N_2, N) ) \\
		& \land \{ t\sqcup C \} = \{ t \sqcup N_1 \} \land \dotB = \{ t\sqcup N \}
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		un & (A, B, \{ t \sqcup C \}) \to \\
		& (A = \{t \sqcup N_1 \} \land un(N_1, N_2, N) \\
		& \lor B = \{ t \sqcup N_1 \} \land un(A, N_1, N) \\
		& \lor A = \{ t \sqcup N_1 \} \land B = \{ t \sqcup N_2 \} \land un(N_1, N_2, N) ) \\
		& \land \{ t \sqcup C \} = \{ t \sqcup N \}
		\end{split}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di appartenenza}
	\label{fig:un_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $un(\dotA, \dotB, \dotC)$, $\dotA$ e $\dotB$ variabili distinte.
\end{itemize}

\paragraph{Implementazione}
Algoritmo \ref{alg:un_constraints}

\subsubsection{Il vincolo disj}

\textit{Sintassi:} $t_1 \mid\mid t_2$.\\
\noindent\textit{Semantica informale:} se $t_1$ e $t_2$ sono insiemi, allora $t_1 \cap t_2 = \emptyset$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:disj_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{$\mid\mid$\textsubscript{\arabic{equation}}}

		If $t, t_i: \text{U}; A, B: \text{Set}$ then:

		\begin{equation}
		\emptyset \mid\mid A \to true
		\end{equation}
		\begin{equation}
		A \mid\mid \emptyset \to true
		\end{equation}
		\begin{equation}
		\dotA \mid\mid \dotA \to \dotA = \emptyset
		\end{equation}
		\begin{equation}
		\{ t \sqcup B \} \mid\mid \dotA \to t \not\in \dotA \land \dotA \mid\mid B
		\end{equation}
		\begin{equation}
		\dotA \mid\mid \{ t \sqcup B \} \to t \not\in \dotA \land \dotA \mid\mid B
		\end{equation}
		\begin{equation}
		\{ t_1 \sqcup A \} \mid\mid \{ t_2 \sqcup B \} \to t_1 \neq t_2 \land t_1 \not\in B \land t_2 \not\in A \land A \mid\mid B
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di disgiunzione}
	\label{fig:disj_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $\dotA \mid\mid \dotB$, $\dotA$ e $\dotB$ variabili distinte.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:disj_constraints}

\subsubsection{Il vincolo subset}

\textit{Sintassi:} $t_1 \subseteq t_2$.\\
\noindent\textit{Semantica informale:} se $t_1$ e $t_2$ sono insiemi, allora $t_1$ è un sottoinsieme di $t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:subset_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{\textsubscript{\arabic{equation}}}

		If $x, y: \text{U}; A, B: \text{Set}$ then:

		\begin{equation}
		\dotA \subseteq \dotA \to true
		\end{equation}
		\begin{equation}
		\emptyset \subseteq A \to true
		\end{equation}
		\begin{equation}
		\dotA \subseteq \emptyset \to \dotA = \emptyset
		\end{equation}
		\begin{equation}
		\{ t \sqcup A \} \subseteq \emptyset \to false
		\end{equation}
		\begin{equation}
		\begin{split}
		\{ x \sqcup A \} & \subseteq \dotB \to \\
		& \dotB = \{ x \sqcup N \} \land A \subseteq \{ x \sqcup N \}
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		\{ x \sqcup A \} & \subseteq \{ y \sqcup B \} \to \\
		& x = y \land A \subseteq \{ y \sqcup B \} \\
		& \lor x \neq y \land x \in B \land A \subseteq \{ x \sqcup B \}
		\end{split}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di sottoinsieme}
	\label{fig:subset_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $\dotA \subseteq \dotB$, $\dotA$ e $\dotB$ variabili distinte;
	\item $\dotA \subseteq \{ y | B \}$.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:subset_constraints}

\subsubsection{Il vincolo inters}

\textit{Sintassi:} $inters(t_1,t_2,t_3)$.\\
\noindent\textit{Semantica informale:} se $t_1, t_2$ e $t_3$ sono insiemi, allora $t_3 = t_1 \cap t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:intersect_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{7}
		\renewcommand{\theequation}{$\cup$\textsubscript{\arabic{equation}}}

		If $x: \text{U}; A, B, C: \text{Set}$ then:

		\begin{equation}
		inters(\dotA, \dotA, B) \to A = B
		\end{equation}
		\begin{equation}
		inters(\emptyset, \dotA, C) \to C = \emptyset
		\end{equation}
		\begin{equation}
		inters(\dotA, \emptyset, C) \to C = \emptyset
		\end{equation}
		\begin{equation}
		inters(A,B,\emptyset) \to A \mid\mid B
		\end{equation}
		\begin{equation}
		\begin{split}
		inters & (A,B,\dotC) \to \\
		& A = \{ x \sqcup N_1 \} \\
		& \lor B = \{ x \sqcup N_2 \} \land \dotC = \{ x \sqcup N_3 \} \land inters(N_1, N_2, N_3)
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		inters & (A,B,\dotC) \to \\
		& A = \{ x \sqcup N_1 \} \land B = \{ x \sqcup N_2 \} \land inters(N_1, N_2, C)
		\end{split}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di intersezione}
	\label{fig:intersect_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $inters(\dotA, B, \dotC)$, $\dotA$ e $B$ non sono la stessa variabile;
	\item $inters(A, \dotB, \dotC)$, $A$ e $\dotB$ non sono la stessa variabile.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:inters_constraints}

\subsubsection{Il vincolo diff}

\textit{Sintassi:} $diff(t_1,t_2,t_3)$.\\
\noindent\textit{Semantica informale:} se $t_1, t_2$ e $t_3$ sono insiemi, allora $t_3 = t_1 \setminus t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:difference_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{\textsubscript{\arabic{equation}}}

		If $A, B, C: \text{Set}$ then:

		\begin{equation}
		diff(A,B,C) \to un(C,A,A) \land un(B,C,N) \land un(A,N,N)
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di differenza}
	\label{fig:difference_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item Nessuna.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:diff_constraints}

\subsection{Regole di riscrittura per vincoli negativi su insiemi}
\label{subsec:clpbasedlang_lset_rewriteneg}

I vincoli negativi su insiemi in \lset{} non sono dati dalla comune
negazione, bensì sono introdotti come vincoli derivati. La negazione
classica viene eliminata e per ogni predicato $\neg p(t_1, \ldots,
t_n)$ si ottiene una forma positiva del predicato $p'(t_1, \ldots,
t_n)$ che ne rappresenta la negazione.

\subsubsection{Il vincolo not in}

\textit{Sintassi:} $t_1 \not\in t_2$.\\
\noindent\textit{Semantica informale:} se $t_2$ è un insieme, allora $t_1$ non è un membro di $t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:notin_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{3}
		\renewcommand{\theequation}{$\in$\textsubscript{\arabic{equation}}}

		If $x, y: \text{U}; A, B, C: \text{Set}$ then:

		\begin{equation}
		x \not\in \emptyset \to true
		\end{equation}
		\begin{equation}
		x \not\in \{ y \sqcup A \} \to x \neq y \land x \not\in A
		\end{equation}
		\begin{equation}
		\text{If } \dotA \in vars(x), x \not\in \dotA \to true
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di non appartenenza}
	\label{fig:notin_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item $t \not\in \dotA$, e $\dotA$ non occorre in $t$.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:notin_constraints}

\subsubsection{Il vincolo not union}

\textit{Sintassi:} $nun(t_1,t_2,t_3)$.\\
\noindent\textit{Semantica informale:} se $t_1, t_2$ e $t_3$ sono insiemi, allora $t_3 \neq t_1 \cup t_2$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:notun_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{13}
		\renewcommand{\theequation}{$\cup$\textsubscript{\arabic{equation}}}

		If $A, B, C: \text{Set}$ then:

		\begin{equation}
		\begin{split}
		nun(& A,B,C) \to \\
		  & N \in C \land N \not\in A N \not\in B \\
		  & \lor N \in A \land N \not\in C \\
		  & \lor N \in B \land N \not\in C
		\end{split}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli non unione}
	\label{fig:notun_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item Nessuna.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:notun_constraints}

\subsubsection{Il vincolo not disjoint}

\textit{Sintassi:} $t_1 \not\mid\mid t_2$.\\
\noindent\textit{Semantica informale:} se $t_1$ e $t_2$ sono insiemi, allora $t_1 \cap t_2 \neq \emptyset$.\\
\noindent\textit{Regole di riscrittura:} Figura \ref{fig:notdisj_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{6}
		\renewcommand{\theequation}{$\mid\mid$\textsubscript{\arabic{equation}}}

		If $A, B: \text{Set}$ then:

		\begin{equation}
		A \not\mid\mid B \to N \in A \land N \in B
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per vincoli di non disgiunzione}
	\label{fig:notdisj_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item Nessuna.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:notdisj_constraints}

\subsubsection{Altri vincoli negativi}

\noindent\textit{Regole di riscrittura:} Figura \ref{fig:othernegatives_constraints}.

\begin{figure}
	\begin{tcolorbox}[colframe=black, colback=white, sharp corners]
		\setcounter{equation}{0}
		\renewcommand{\theequation}{\arabic{equation}}

		If $R, S, T, A, B, C: \text{Set}$ then:

		\begin{equation}
		nsubset(A,B) \to n \in A \land n \not\in B
		\end{equation}
		\begin{equation}
		\begin{split}
		ninters& (A,B,C) \to \\
		  & n \in C \land ( n \not\in A \lor n \in C \land n \not\in B ) \\
		  & \lor n \not\in C \land n \in A \land n \not\in B
		\end{split}
		\end{equation}
		\begin{equation}
		\begin{split}
		ndiff& (A,B,C) \to \\
		  & n \in C \land n \not\in A \lor n \in C \land n \in B \\
		  & \lor n \not\in C \land n \in A \land n \not\in B
		\end{split}
		\end{equation}

	\end{tcolorbox}

	\caption{Regole di riscrittura per altri vincoli negativi}
	\label{fig:othernegatives_constraints}
\end{figure}

\paragraph{Forme irriducibili}
\begin{itemize}
	\item Nessuna.
\end{itemize}

%\paragraph{Implementazione}
%Algoritmo \ref{alg:othernegatives_constraints}



%%% *******************************************************
%%% Picat   ***********************************************
\chapter{Picat}
\label{ch:picat}

%\minitoc

In questo capitolo viene presentato Picat, un linguaggio di
programmazione multiparadigma basato sulla logica dei predicati del
prim'ordine. Picat è per certi versi molto simile al Prolog, ma
dispone di molte funzionalità che modificano radicalmente l'utilizzo
comune sia di un linguaggio imperativo che logico.

Nella sezione \ref{sec:picat_features} si descrivono le
caratteristiche di Picat, mentre in \ref{sec:picat_base} e
\ref{sec:picat_advanced} se ne espongono le funzionalità fornendo
esempi esplicativi.

I numerosi dettagli tralasciati per ovvi motivi in questa
presentazione possono essere approfonditi sul manuale di Picat
\cite{PicatGuide}. Si avvisa inoltre che al tempo in cui si sta
scrivendo, la guida di Picat è in versione 2.6.

\section{Caratteristiche}
\label{sec:picat_features}

Picat incorpora le principali funzionalità dei linguaggi logici,
funzionali e di scripting. Le caratteristiche di Picat sono riassunte
dalle lettere del suo nome:
\begin{itemize}
\item \textbf{P}attern-matching. Un \emph{predicato} definisce una
  relazione e può avere zero, una o più soluzioni. Picat è un
  linguaggio basato su regole. I predicati e le funzioni sono definiti
  tramite pattern-matching.
\item \textbf{I}ntuitive. Picat fornisce comandi come l'assegnamento
  e i loop, che vengono comunemente usati nei linguaggi imperativi,
  rendendo di fatto più semplice la scrittura di programmi non logici.
\item \textbf{C}onstraints. Picat supporta nativamente la programmazione con
  vincoli. Nasce infatti con quattro moduli per la risoluzione di
  vincoli: \verb|cp|, \verb|sat|, \verb|smt| e \verb|mip|.
\item \textbf{A}ctors. Viene fornito il supporto a chiamate
  event-driven tramite \emph{action rules}, utilizzate per descrivere
  il comportamento degli attori event-driven.
\item \textbf{T}abling. Il tabling è utilizzato per memorizzare la
  soluzione di un calcolo in memoria, permettendo quindi una rapida
  consultazione del risultato senza ricalcolo. Per questo motivo, il
  modulo \verb|planner| di Picat ne fa largo uso.
\end{itemize}

Inoltre, Picat supporta le principali caratteristiche dei linguaggi
logici, obbligando però il programmatore a usarle in modo esplicito,
come per il caso dell'unificazione, del non determinismo, del tabling
e dei vincoli.

\section{Funzionalità di base}
\label{sec:picat_base}

\subsection{Il sistema Picat}
\label{subsec:picat_base_system}

Picat è un linguaggio interpretato. I programmi Picat però, prima di
essere eseguiti, sono compilati in \textbf{byte-code}. Il compilatore
non trasforma i sorgenti in codice macchina, ma depura il programma da
tutto quello che non è necessario per l'esecuzione, compie vari
controlli statici e riscrive alcuni costrutti sintatticamente (e.g., i
cicli).

Tramite l'interprete Picat è possibile caricare, compilare ed eseguire
programmi, eventualmente anche modalità debug.

\paragraph{Esempio}\
\begin{verbatim}
$ picat 

Picat> compile(hello_world)
Compiling::hello_world.pi
hello_world.pi compiled in 1 milliseconds

yes

Picat> load(hello_world)
loading...hello_world.qi

yes

Picat> main
Hello, World!

yes
\end{verbatim}

Dall'esempio riportato sopra è possibile notare che la compilazione
del file sorgente \texttt{.pi} produce un file compilato in byte-code
con estensione \texttt{.qi}, che viene poi caricato dall'interprete
Picat al comando \texttt{load}. Picat mette a disposizione anche il
comando \texttt{cl($\cdot$)} (compile and load), che permette di
eseguire compilazione e caricamento in modo rapido e senza la
generazione di file intermedi (il byte-code generato è caricato
istantaneamente dall'interprete, senza bisogno di essere salvato su
memoria persistente).

\subsection{Tipi di dato}
\label{subsec:picat_base_datatype}

Picat è un linguaggio \textbf{dinamicamente tipato}: il controllo dei
tipi avviene a runtime. Le variabili in Picat possono avere o non
avere un valore. Una variabile è libera fintanto che non viene
vincolata a un valore (operazione di bounding), e può avere degli
attributi rappresentati come mappa chiave-valore.\footnote{Gli
  attributi di una variabile sono spesso utilizzati dai risolutori di
  vincoli integrati nei moduli predefiniti di Picat per memorizzare
  informazioni riguardanti vincoli su variabili.}

I tipi primitivi di Picat sono il numero intero, reale e l'atomo. Un
atomo è un nome iniziante con lettera minuscola o una stringa quotata
da apici singoli.

I tipi composti invece sono le liste $[t_1, \ldots,
t_n]$ e le strutture $\$s(t_1, \ldots, t_n)$, dove
$s$ è il nome della struct, ed $n$ è l'arità. Il dollaro viene
impiegato per distinguere una chiamata di funzione da una
struct. Picat inoltre mette a disposizione tipi composti speciali come
\emph{strings}, \emph{arrays}, \emph{maps}, \emph{sets} e
\emph{heaps}.

\paragraph{Esempio}\
\begin{verbatim}
Picat> V1 = X1, V2 = _ab, V3 = _       % variabili

Picat> N1 = 12, N2 = 0xf3, N3 = 1.0e8  % numeri

Picat> A1 = x1, A2 = '_AB', A3 = ''    % atomi

Picat> L = [a,b,c,d]                   % liste

Picat> write("hello"++"picat")
[h,e,l,l,o,p,i,c,a,t]                  % stringhe

Picat> print("hello"++"picat")
hellopicat

Picat> writef("%s","hello"++"picat")
hellopicat                             % write con formato

Picat> writef("%-5d %5.2f",2,2.0)
2
2.00                                   % write con formato

Picat> S = $point(1.0,2.0)             % struttura

Picat> S = new_struct(point,3)
S = point(_3b0,_3b4,_3b8)              % creazione di una struttura
                                       % con arità 3

Picat> A = {a,b,c,d}                   % array

Picat> A = new_array(3)
A = {_3b0,_3b4,_3b8}                   % creazione di un array 
                                       % di 3 elementi

Picat> M = new_map([one=1,two=2])
M = (map)[two = 2,one = 1]             % creazione di una mappa

Picat> M = new_set([one,two,three])
M = (map)[two,one,three]               % creazione di un insieme

Picat> X = 1..2..10
X = [1,3,5,7,9]                        % ranges

Picat> X = 1..5
X = [1,2,3,4,5]
\end{verbatim}

Picat possiede una ricca libreria di funzioni di utilità sui tipi di
dato che permettono, tra le altre cose, di verificare qual è il tipo
di una variabile, convertire tipi ad altri tipi e aggiungere o
rimuovere elementi da una struttura dati.

\subsection{Predicati}
\label{subsec:picat_base_pred}

I predicati sono una componente fondamentale di Picat: essi
definiscono una relazione che può avere zero, una o più soluzioni,
terminando in modo positivo o negativo, a meno di eccezioni.

In Picat i predicati sono definiti con regole di pattern-matching. Le
regole utilizzabili per la definizione di un predicato sono 
\[ Head, Cond => Body \]
e
\[Head, Cond\ ?=> Body \] che rappresentano
rispettivamente la regola \emph{non-backtrackable} e
\emph{backtrackable}. La testa $Head$ del predicato è $p(t_1, \ldots,
t_n)$ con $p$ il nome del predicato e $n$ l'arità. Le condizioni
$Cond$ sono goal opzionali che specificano l'applicabilità della
regola. $Body$ è li corpo del predicato.  Quando una chiamata $C$ è
applicabile, Picat riscrive $C$ in $Body$. Se la regola usata è
\emph{non-backtrackable} allora la riscrittura è permanente,
altrimenti il programma farà backtracking su $C$ se $Body$ fallisce e
verrà provata la regola successiva.

Un predicato è detto essere \emph{deterministico} se è definito
solamente da regole non-backtrackable, \emph{non-deterministico}
invece se nella definizione del predicato compare almeno una regola
backtrackable. Inoltre, si dice \emph{globalmente deterministico} un
predicato deterministico che in $Body$ contiene solo chiamate a
predicati globalmente deterministici. Per questo motivo, un
predicato deterministico può avere più di una soluzione, mentre
uno globalmente deterministico al massimo una.

\paragraph{Esempio} Regola non backtrackable.
\begin{verbatim}
membchk(X,[X|_]) => true.
membchk(X,[_|L]) => membchk(X,L)

Picat> membchk(X,[1,2,3]).
no
\end{verbatim}

\paragraph{Esempio} Regola backtrackable.
\begin{verbatim}
member(X,[Y|_]) ?=> X=Y.
member(X,[_|L]) => member(X,L).

Picat> member(X,[1,2,3])
X = 1;
X = 2;
X = 3;
no
\end{verbatim}

Picat inoltre permette la definizione di \emph{fatti} della forma
$p(t_1, \ldots, t_n)$ nelle definizioni di predicati. I fatti sono
tradotti in regole di pattern-matching prima della compilazione. Una
definizione di predicato costituita da fatti può essere preceduta da
una \emph{index declaration} della forma $index (M_{11}, \ldots,
M_{1n}) \ldots (M_{m1}, \ldots, M_{mn})$ dove ogni $M_{ij}$ può essere
o $+$ (indicizzato) o $-$ (non indicizzato). Per ogni pattern
indicizzato $(M_{i1}, \ldots, M_{in})$, il compilatore genera una
versione del predicato che indicizza tutti gli argomenti
contrassegnati da $+$. Ciò è fatto per ragioni di efficienza.

\paragraph{Esempio}

Supponendo di voler rappresentare la seguente figura tramite fatti in
Picat
\begin{center}
\begin {tikzpicture}[-latex ,auto ,node distance =4 cm and 5cm ,on grid ,
semithick ,
state/.style ={ circle ,top color =white , bottom color = white ,
	draw, black , text=black , minimum width =1 cm}]
\node[state] (A) {a};
\node[state] (B) [right=of A] {b};
\node[state] (C) [below =of A] {c};
\path (A) edge (B);
\path (A) edge (C);
\path (C) edge [bend left =15] (B);
\path (B) edge [bend left =15] (C);
\end{tikzpicture}
\end{center}
la rappresentazione potrebbe essere
\begin{verbatim}
index (+,-) (-,+)
spigolo(a,b).
spigolo(a,c).
spigolo(b,c).
spigolo(c,b).
\end{verbatim}
che grazie all'indicizzazione vengono poi tradotti nelle regole che
seguono
\begin{verbatim}
spigolo(a,Y) ?=> Y=b.
spigolo(a,Y) =>  Y=c.
spigolo(b,Y) =>  Y=c.
spigolo(c,Y) =>  Y=b.
spigolo(X,b) ?=> X=a.
spigolo(X,c) ?=> X=a.
spigolo(X,c) =>  X=b.
spigolo(X,b) =>  X=c.
\end{verbatim}

\subsection{Funzioni}
\label{subsec:picat_base_func}

Picat permette di definire delle funzioni, ovvero oggetti che hanno
sempre esito positivo e che ritornano un solo valore. La sintassi di
una funzione è
\[
  Head, Cond = Result => Body
\]
Le funzioni in Picat
sono uno zucchero sintattico per un predicato così formato:
$HeadResult, Cond => Body$ dove $HeadResult = p(t_1, \ldots, t_n, r)$.

\paragraph{Esempio}
\begin{verbatim}
fib(0)=F => F=1.
fib(1)=F => F=1.
fib(N)=F,N>1 => F=fib(N-1)+fib(N-2).

Picat> X = fib(8)
X = 21
yes
\end{verbatim}

\subsection{Assegnamenti e Cicli}
\label{subsec:picat_base_asscycle}

Picat cerca di agevolare notevolmente i programmatori abituati alla
programmazione con linguaggi imperativi. Per questo motivo offre
funzionalità come l'assegnamento, tipicamente non disponibile in un
linguaggio logico, e cicli, che nei linguaggi logici si realizzano con
la ricorsione.

\subsubsection{Assegnamento}

Anche l'assegnamento, come altri comandi, è uno zucchero
sintattico. Un assegnamento in Picat $X := Y$ viene gestito a tempo di
compilazione creando nuovi nomi di variabile. Le nuove variabili
conterranno il nuovo valore dopo l'assegnamento e verranno usate nella
porzione di programma successiva all'assegnamento al posto della
vecchia variabile.

\paragraph{Esempio}
\begin{verbatim}
test => X=0, X:=X+1, X:=X+1, write(X).
\end{verbatim}
ha come output $2$, e con la compilazione viene riscritto in
\begin{verbatim}
test => X=0, X1=X+1, X2=X1+1, write(X2).
\end{verbatim}
avente anch'esso output $2$.

\subsubsection{Cicli}

Picat supporta tre tipi di cicli: \verb|foreach|, \verb|while| e
\verb|do-while|. Il \verb|foreach| viene anche impiegato per
implementare un particolare tipo di ciclo su liste denominato
\emph{list comprehension}.

\paragraph{Esempio}\
\begin{lstlisting}
% esempio di foreach
L = [2, 3, 5, 10],
foreach(I in L, J in 1 .. 10, J mod I != 0)
	printf("%d is not a multiple of %d%n", J, I)
end.

% esempio di while
I = 1,
while (I <= 9)
	println(I),
	I := I + 2
end.

% esempio di do while
J = 6,
do
	println(J),
	J := J + 1
while (J <= 5).
\end{lstlisting}

Mentre per i tipi di cicli più comuni la semantica è piuttosto ovvia,
per le list comprehension la cosa è più interessante. Le list
comprehension sono funzioni che servono a costruire una lista iterando
valori di altre list. La sintassi per esprimerle è la seguente
\begin{lstlisting}
[T : $E_1$ in $D_1$, $Cond_1$ , $\ldots$, $E_n$ in $D_n$ , $Cond_n$]
\end{lstlisting}

\paragraph{Esempio}\
\begin{lstlisting}
picat> L = [(A, I) : A in [a, b], I in 1 .. 2].
L = [(a , 1),(a , 2),(b , 1),(b , 2)]
\end{lstlisting}

\section{Funzionalità avanzate}
\label{sec:picat_advanced}

In questa sezione si dà una panoramica delle funzionalità avanzate di
Picat come il tabling, i moduli, le eccezioni, le high-order calls, le
action rules e le mappe globali. Questi strumenti rendono Picat un
linguaggio veramente ricco e unico nel suo genere. Eventuali
approfondimenti si possono trovare in \cite{PicatGuide}.

\subsection{Tabling}
\label{subsec:picat_advanced_tabling}

Il tabling è un meccanismo di caching che permette di memorizzare la
chiamata a un predicato e relativo risultato per evitare cicli
infiniti o per ridurre il costo computazione dovuto alla grossa
ridondanza dei calcoli.

\paragraph{Esempio}\
\begin{lstlisting}
table
fib(0) = 0.
fib(1) = 1.
fib(N) = fib(N-1)+fib(N-2).
\end{lstlisting}
Senza tabling \verb|fib(N)| ha costo esponenziale in \verb|N|, con il
tabling invece il costo è lineare in quanto non vi è la necessità del
ricalcolo di risultati intermedi.

Il tabling è abilitato usando la keyword \verb|table| prima della
definizione del predicato.

\subsection{Moduli}
\label{subsec:picat_advanced_modules}

I moduli sono una funzionalità molto utile di Picat e permettono al
programmatore un'organizzazione comoda del codice sorgente, suddivisa
su più file (moduli, appunto).

Un modulo è un file sorgente con estensione \texttt{.pi}, e
inizia con la dichiarazione di se stesso nella forma 
\[
\texttt{module}\ Name.
\]
dove $Name$ corrisponde al nome del file. Se il modulo non inizia con
la dichiarazione del modulo stesso, esso è assunto appartenere al
modulo globale e tutte le funzioni e predicati dichiarati sono resi
visibili a tutti gli altri moduli, nonchè all'interprete Picat.

Picat fornisce un sistema molto semplice di import, consentendo così
di accedere a funzionalità di altri file sorgente. La sintassi per
l'import è
\[
\texttt{import}\ Name_1, \ldots, Name_n.
\]

Un predicato pubblico può essere acceduto anche specificandone
completamente il nome tramite \texttt{m.p()}, dove \texttt{m} è il
nome del modulo e \texttt{p} è il nome del predicato. Il modulo va
comunque importato. E' consentito modificare la visibilità di un
predicato ai moduli esterni (poibendone quindi l'utilizzo)
semplicemente antecedendo la keyword \texttt{private} alla definizione
del predicato.

\paragraph{Esempio}

\begin{verbatim}
%%% file somma.pi
module somma.

somma(L)=Sum =>
    somma_aux(L,0,Sum).
private
somma_aux([],Sum0,Sum) => Sum=Sum0.
somma_aux([X|L],Sum0,Sum) => sum_aux(L,X+Sum0,Sum).

%%% file test_somma.pi
module test_somma.
import somma.

go =>
    writeln(somma([1,2,3,4])).
\end{verbatim}

\subsection{Eccezioni}
\label{subsec:picat_advanced_exceptions}

Picat fornisce un semplice sistema di gestione delle eccezioni, con
cui è possibile gestire eventi eccezionali ed errori non previsti.

La sintassi per il lancio delle eccezioni è
\begin{lstlisting}
throw Exception
\end{lstlisting}
mentre la cattura e la gestione dell'eccezione si effettua tramite
\begin{lstlisting}
catch(Goal, Exception, Handler)
\end{lstlisting}
con ovvia semantica: $Goal$ è il predicato dal quale si catturano le
eccezioni; $Exception$ è l'eccezione che si vuole catturare, da
unificare con l'eccezione lanciata ($Exception$ può essere anche una
variabile libera); mentre $Handler$ è il predicato che si esegue una
volta catturata l'eccezione.

Si noti che il predicato \texttt{catch} è di ordine superiore in
quanto prende come primo e terzo parametro un altro predicato.

\paragraph{Esempio}

\begin{verbatim}
%%% file pericolo.pi
pericolo => X = 5 // 0.   % divisione per zero, solleva
                          % eccezione zero_divisor

main =>
    catch(
        pericolo, 
        Exception, 
        (print("Eccezione catturata: "), println(Exception)).

$ picat pericolo.pi
Eccezione catturata: error(zero_divisor,/ / 2)
\end{verbatim}

\subsection{Higher-Order Calls}
\label{subsec:picat_advanced_hoc}

Un predicato o una funzione è di ordine superiore se riceve funzioni
come argomenti. Alcuni predicati di ordine superiore \emph{built-in}
del linguaggio sono \verb|call|, \verb|apply| e \verb|find_all|. I
predicati \verb|call| e \verb|apply| prendono in input un nome di
funzione e lo eseguono con gli argomenti dati; \verb|apply| può
ritornare un valore. Il predicato \verb|find_all| invece trova tutte
le soluzioni della chiamata per la funzione in input.

Picat fornisce altri predicati di ordine superiore per la gestione
delle eccezioni, l'esecuzione e altre utilità.

\paragraph{Esempio}
\begin{verbatim}
Picat> S=$member(X), call(S,[1,2,3])
X = 1;
X = 2;
X = 3;
no

Picat> L=findall(X,member(X,[1,2,3])).
L = [1,2,3]

Picat> Z=apply('+',1,2)
Z = 3
\end{verbatim}

\subsection{Action Rules}
\label{subsec:picat_advanced_actionrules}

Picat fornisce \emph{Action Rules} per descrivere attori
event-driven. Un attore è un chiamata a un predicato che può essere
differita rispetto alla normale esecuzione ed è attivabile da
eventi. Queste regole hanno sintassi 
\[ Head, Cond, \{Event\} => Body \]
dove $Event$ è un insieme non vuoto di eventi separati da virgola.

Gli attori possono essere assegnati a canali sui quali sono notificati
gli eventi. Un canale è una variabile con degli attributi in grado di
notificare eventi e può avere diverse porte, che specificano
la visibilità dell'evento per quel canale.

\subsection{Mappe Globali}
\label{subsec:picat_advanced_globalmaps}

Picat fornisce tre tipi diversi di mappe utilizzabili durante
l'esecuzione: mappe \emph{heap}, mappe \emph{globali} e
\emph{tabelle}.

Queste mappe sono create non appena il sistema Picat si avvia. 
Possono essere consultate e modificate richiedendone un riferimento
al sistema, specificando tipologia e codice identificativo.
Le tre mappe differiscono per la modalità di memorizzazione
degli elementi e per il numero di mappe che possono essere richieste.

Queste mappe sono accessibili durante tutta l'esecuzione e sono quindi
molto utili per memorizzare variabili globali.

\section{Picat vs. Prolog}
\label{sec:picat_picatvsprolog}

Sebbene Picat sia un linguaggio multi paradigma, esso è profondamente
legato ai concetti di programmazione logica includendo \emph{variabili
  logiche}, \emph{unificazione} e \emph{backtracking}.  Come in
Prolog, le variabili di Picat sono etichette a valori. Una variabile
logica può essere legata a qualunque termine, includendo altre
variabili logiche (una volta sola).

\begin{description}
\item[Unificazione e pattern-matching.] L'unificazione è l'operazione
  di base sia in Picat che in Prolog per effettuare il bound delle
  variabili a termini. Ma mentre in Prolog l'unificazione viene
  utilizzata anche nella risoluzione delle regole, in Picat viene
  impiegato il pattern-matching per decidere se una regola è
  applicabile o meno. Ciò comporta alcune divergenze tra l'esecuzione
  della stessa regola in Prolog e in Picat.  Inoltre, in termini di
  efficienza, l'operazione di pattern-matching sulle regole è molto
  più leggera rispetto all'unificazione.
\item[Backtracking.] Anche Picat supporta nativamente il
  backtracking. In Prolog però ogni regola è implicitamente
  \emph{backtrackable} e si usa l'operatore \emph{cut} (\texttt{!}) 
  per controllarne il comportamento. In Picat invece una regola è
  \emph{backtrackable} solo se esplicitamente dichiarato. Ciò permette
  al programmatore di capire a colpo d'occhio l'intenzione di una
  regola.
\item[Predicati dinamici.] Picat non supporta i predicati dinamici,
  mentre in Prolog è possibile asserire un predicato durante
  l'esecuzione, dando di fatto più flessibilità al linguaggio.
\item[Operatori definiti da utente.] In Picat non è possibile definire
  nessun operatore, mentre in Prolog è possibile estendere il set di
  operatore aggiungendone di nuovi. Questa caratteristica è stata
  particolarmente sfruttata nello strumento \setlog per dare un senso
  di naturalezza e vicinanza alla rappresentazione matematica delle
  formule.
\item[Costrutti.] Una delle differenze più evidenti tra i due
  linguaggi sono i costrutti. Picat infatti fornisce molti costrutti
  per svolgere operazioni comuni quali assegnamenti, cicli e salti
  condizionali. Non mancano inoltre un buon numero di tipi di dato
  predefiniti con relative operazioni, che per attività di scripting e
  modellazione rendono Picat più conveniente rispetto al Prolog. In
  Prolog è fornita solo qualche struttura elementare come l'\emph{if}
  con una sintassi particolare, spesso difficile da leggere e capire
  durante la manutenzione del codice.
\end{description}



%%% *******************************************************
%%% Solver CLP(SET) in Picat   ****************************
\chapter{\lset{} in Picat}
\label{ch:lsetpicat}

%\minitoc

In questo capitolo si descrive la realizzazione del constraint solver
e del suo sistema Picat, trattando aspetti progettuali e relative
scelte, problemi e difficoltà riscontrate sia di design che in fase di
realizzazione e qualche caratteristica implementativa del solver.

In particolare, nella sezione \ref{sec:lsetpicat_project} si dà una
breve panoramica sull'organizzazione del progetto e delle scelte
effettuate per strutturarne il codice, nonché qualche accenno alle
notazioni e convenzioni adottate. In \ref{sec:lsetpicat_system} si
fornisce una descrizione del sistema dal punto di vista generale,
includendo l'ingegnerizzazione e la suddivisione in moduli delle
funzionalità. Inoltre si fornisce una veloce rassegna per ogni modulo
e se ne descrive l'interfaccia esposta. Nella sezione
\ref{sec:lsetpicat_solver} viene approfondito il solver, il suo
funzionamento e i predicati implementati. La sezione
\ref{sec:lsetpicat_or} approfondisce i problemi affrontati e relative
soluzioni nell'implementazione del vincolo \texttt{or} con Picat. In
\ref{sec:lsetpicat_solutions} si analizza il problema
dell'enumerazione delle soluzioni in Picat. In
\ref{sec:lsetpicat_testing} si affronta il problema del testing: un
processo necessario e piuttosto complicato da effettuare durante la la
stesura dell'implementazione di un solver.

\section{Organizzazione del progetto}
\label{sec:lsetpicat_project}

L'organizzazione del progetto e dei file sorgente è di particolare
rilevanza: permette una miglior stesura del codice, facilità
di lettura e manutenzione, creazione dei test e consente a futuri
collaboratori di lavorare sul software in modo ordinato e preciso.
Soprattutto nell'ambito dei linguaggi logici esistono
poche linee guida e strutture convenzionali per l'organizzazione dei
sorgenti. Ciò, unito alla complessità intrinseca dei linguaggi logici,
complica notevolmente la manutenibilità del software e lo rende molto
più soggetto a bug ed errori di progettazione.

Picat essendo un linguaggio logico ancora poco utilizzato, non
presenta convenzioni comunemente accettate e vincoli che forzino il
programmatore a seguire una struttura ben definita. Vi sono però dei
vantaggi da questo punto di vista nell'utilizzo di Picat:
\begin{itemize}
	\item è possibile organizzare logicamente la struttura del
          progetto tramite i moduli, semplificando la gestione delle
          funzionalità;
	\item è possibile seguire un approccio OOP con costruttori e
          funzioni, integrando il concetto di visibilità dei
          metodi. Ciò può essere di aiuto a garantire il corretto
          utilizzo delle interfacce di programmazione, progettate per
          svolgere compiti ben definiti;
	\item non è possibile scrivere del codice ``magico'' o che
          abbia comportamenti non attesi in quanto il backtracking è
          sempre esplicito e non è possibile asserire nuovi predicati
          che cambino il comportamento del programma.
\end{itemize}

Nell'organizzazione di questo progetto si adotta la convenzione più
comune della suddivisione in file sorgenti che realizzano le
funzionalità generali (cartella \texttt{src}) e i test (cartella
\texttt{tests}). Come convenzione interna inoltre si decide che le
funzionalità raggruppate in un singolo modulo debbano essere
\textit{tightly coupled}\footnote{Letteralmente, \textit{tightly
    coupled} significa strettamente accoppiati. \`E un concetto che
  riferito ai componenti di un sistema ne esprime la forte relazione
  e interconnessione.}, mentre le funzionalità \textit{loosely
  coupled} siano dipendenze da funzionalità di moduli diversi.

La struttura che ne risulta è elencata in figura
\ref{fig:proj_folder_structure}.

\begin{figure}[]
	\label{fig:proj_folder_structure}
	\begin{verbatim}
	.
	|-- JOURNAL.txt
	|-- LICENSE.txt
	|-- Makefile
	|-- README.md
	|-- src
	|   |-- assert.pi
	|   |-- commands.pi
	|   |-- global.pi
	|   |-- log_h.pi
	|   |-- lset.pi
	|   |-- main.pi
	|   |-- Makefile
	|   |-- prompt.pi
	|   `-- solver.pi
	`-- tests
	    |-- lset_test.pi
	    |-- Makefile
	    `-- solver_test.pi
	\end{verbatim}
	\caption{Organizzazione del progetto}
\end{figure}

Una descrizione sommaria del contenuto dei file e delle directory è
riportata di seguito:
\begin{itemize}
	\item \texttt{LICENSE.txt}, la licenza del codice sorgente.
	\item \texttt{README.md}, la descrizione del progetto:
          contenente note per l'installazione e l'utilizzo.
	\item \texttt{Makefile}, consente l'automatizzazione di task
          ricorrenti, evitando al programmatore l'esecuzione manuale
          degli stessi. Ad esempio, il \texttt{Makefile} nella
          cartella \texttt{tests} costruisce uno scipt che esegue un
          clone dei sorgenti ed esegue i test.
	\item \texttt{src}, la cartella contenente i file sorgenti. I
          moduli che compongono il sistema sono mostrati in
          \ref{subsec:lsetpicat_architecture}.
	\item \texttt{tests}, la cartella contenente i test dei
          componenti fondamentali.
\end{itemize}

Per quanto riguarda lo stile del codice sorgente, dei commenti e
dell'utilizzo del linguaggio logico si prende spunto da
\cite{Covington12}, al quale si rimanda per ulteriori informazioni. Le
convenzioni descritte in questo articolo, essendo basate sul Prolog,
non vengono seguite in modo rigido.

\section{Il sistema}
\label{sec:lsetpicat_system}

\subsection{Linguaggio (concreto) di input}
\label{subsec:lsetpicat_concretelang}

Il linguaggio definito in \lset{} per le formule non è realizzabile in
Picat senza elaborazioni sofisticate, che esulano dall'obiettivo di
questo lavoro di tesi. Definiremo pertanto un linguaggio concreto
ad-hoc per descrivere le formule di input per il solver, che risulti
il più vicino possibile al linguaggio di \lset{}, rimanendo facilmente
implementabile in Picat.

\subsubsection{Sintassi}

La notazione adottata per la rappresentazione delle formule è la
seguente:

\begin{table}[H]
	\center
	\begin{tabular}{ll}
		\textbf{Linguaggio} & \textbf{Notazione} \\
		\lset{} & $T_1 \land T_2 \land \ldots \land T_n$ \\
		Picat & \verb|[| $T_1, T_2, \ldots, T_n$\verb|]| \\
	\end{tabular}
\end{table}

Le operazioni primitive di \clpset{} sono spesso espresse tramite
simboli (e.g., $=, \neq, \ldots$). La notazione adottata è la
seguente:
\begin{table}[H]
	\center
	\begin{tabular}{l l}
		\textbf{Linguaggio} & \textbf{Notazione} \\
		\lset{} & $T_1 = T_2$ \\
		Picat & \verb|[eq(| $T_1, T_2$ \verb|)]| \\
	\end{tabular}
\end{table}
dove gli operatori binari di \lset{} hanno la ovvia traduzione in
forma scritta: $=$ diventa $eq(\cdot, \cdot)$, $\neq$ diventa
$neq(\cdot, \cdot)$, $\in$ diventa $in(\cdot, \cdot)$\footnote{Più
  precisamente, in Picat questo simbolo è stato
  trasformato in \texttt{insl}, in quanto il predicato \texttt{in} è presente
  nativamente in Picat e non può essere ridefinito. Per evitare
  ambiguità è stato definito il predicato \texttt{contains} che ha la
  stessa semantica di \texttt{in} con gli argomenti ``ribaltati''.},
$\not\in$ diventa $nin(\cdot, \cdot)$, e così via. La convenzione di
\lset{} prevede che la forma negata di questi operatori sia
rappresentata dal prefisso $n$ prima del nome. Ad esempio: $nunion$,
$ndisj$, eccetera.

Gli insiemi in \clpset{} sono rappresentati tramite la funzione $\{
\cdot \mid \cdot \}$.

\begin{table}[H]
	\center
	\begin{tabular}{l l}
		\textbf{Linguaggio} & \textbf{Notazione} \\
		\lset{} & $\{ T_1, T_2, \ldots, T_n \mid X \}$ \\
		Picat & \verb|[| $T_1, T_2, \ldots, T_n \mid X$ \verb|]| \\
	\end{tabular}
\end{table}

\subsection{Architettura}
\label{subsec:lsetpicat_architecture}

L'interprete realizzato per la gestione del sistema nel suo insieme è
suddiviso per funzionalità: grazie alle caratteristiche di Picat
queste funzionalità sono state raggruppate e separate in
\emph{moduli}. Ognuno di questi moduli cerca di essere il più coeso
possibile e fornisce funzionalità ad altri moduli, incrementando
quindi la riusabilità del codice.

I moduli identificati e realizzati sono descritti nel seguito.

\subsubsection{solver.pi}

Il modulo \texttt{solver} è il modulo principale che realizza la
risoluzione delle formule. Espone il predicato \verb|solve/2|,
utilizzabile da qualunque programma Picat per risolvere una formula di
\lset{}. Questo modulo viene ampiamente trattato in
\ref{sec:lsetpicat_solver}.

\subsubsection{lset.pi}

Il modulo \texttt{lset} contiene l'interfaccia e l'implementazione
degli insiemi nei termini di \lset{}. Consente di astrarre l'entità
insieme dalla sua implementazione reale. L'approccio OOP è
intenzionale: Picat, come detto in precedenza, favorisce l'utilizzo di
paradigmi diversi da quello logico.

L'adozione di questo meccanismo permette di sperimentare due
implementazioni differenti dell'insieme di \lset{}:

\begin{itemize}
	\item \textbf{Rappresentazione ``coppia''} La rappresentazione
          \emph{coppia} prevede la suddivisione dell'insieme in due
          elementi: il primo è una lista dei componenti dell'insieme
          completamente specificati, mentre il secondo rappresenta il
          resto dell'insieme (una variabile).
	\item \textbf{Rappresentazione ``lista-resto''} La
          rappresentazione \emph{lista-resto} prevede di trattare un
          insieme come una lista in cui gli elementi dell'insieme
          completamente specificati vengono elencati all'inizio della
          lista, e il resto dell'insieme corrisponde al resto della
          lista.
\end{itemize}

Entrambe le rappresentazioni riescono a descrivere semanticamente un
insieme di \lset{}, ma l'implementazione scelta è quella
\emph{lista-resto}. Questa infatti ha la particolarità di sfruttare
alcune caratteristiche delle regole di riscrittura che trattano gli
insiemi proprio come liste, consentendo quindi l'implementazione della
regola in modo del tutto analogo alla descrizione matematica.

\paragraph{Interfaccia}

L'interfaccia di questo modulo espone alcune funzioni
\begin{itemize}
	\item \texttt{new\textunderscore lset/0},
          \texttt{new\textunderscore lset/1},
          \texttt{new\textunderscore lset/2}, i costruttori,
          utilizzati rispettivamente per creare un insieme vuoto, un
          insieme a partire da una lista o un insieme partendo da
          testa e resto;
	\item \texttt{lset\textunderscore head/1}, un metodo per
          recuperare la testa dell'insieme;
	\item \texttt{lset\textunderscore rest/1}, un metodo per
          recuperare il resto dell'insieme
\end{itemize}

\paragraph{Esempio}

I metodi di questo modulo sono facilmente usabili come in un
linguaggio OOP:
\begin{verbatim}
Picat> X = new_lset()          % crea un insieme vuoto

% entrambi i costruttori creano un insieme costituito da
%  testa [1, 2] e resto A.
Picat> Y = new_lset([1,2|A])
Picat> Z = new_lset([1,2], A)


% restituisce in YHead il resto dell'insieme Y
Picat> YHead = Y.lset_head()
YHead = [1,2]

% restituisce in YRest il resto dell'insieme Y
Picat> YRest = Y.lset_rest()
YRest = A
\end{verbatim}


\subsubsection{commands.pi}

Il modulo \texttt{commands} gestisce l'interfaccia utente. Implementa
una CLI (Command Line Interface) orientata all'usabilità utente:
fornisce messaggi di aiuto, cerca di effettuare controlli 
sull'input e una sapiente gestione degli errori.

Di fatto questo modulo implementa un ciclo che non termina mai se non
quando il comando di uscita è ricevuto. Inoltre, il ciclo principale è
racchiuso nel predicato di ordine superiore \texttt{catch} (si veda
\ref{subsec:picat_advanced_hoc} per più informazioni sui predicati di
ordine superiore) che consente di catturare qualunque eccezione esca
dalla gestione dei comandi, per evitare spiacevoli crash e consentendo
all'utente di capire ciò che succede in caso di errore.

La CLI all'avvio svolge, in ordine, le seguenti operazioni:
\begin{enumerate}[label=\arabic*)]
	\item inizializza le variabili globali necessarie con i valori
          predefiniti;
	\item mostra un messaggio di introduzione contenente qualche
          piccola nota sulla garanzia, copyright e mostra i comandi di
          aiuto principali, nonché uno stato delle variabili
          inizializzate;
	\item si mette in attesa di un comando.
\end{enumerate}

La lettura dei comandi è effettuata tramite funzioni predefinite di
Picat per leggere l'input da uno \emph{stream} e funzioni di utilità
per la manipolazione di stringhe nel predicato
\texttt{readCommandLine/1}. La stringa letta è convertita in una lista
di atomi e ritornata al chiamante, il quale sa per certo che nella
lista risultato il primo elemento è sempre un comando e, se esistono,
sono presenti alcuni argomenti nel resto della lista.

Una volta letto il comando si controlla che esso sia un comando
consentito (esiste ed è stato implementato) e se ne effettua il
dispatching, consentendone l'esecuzione. Un'interessante proprietà di
questa CLI è la gestione dell'\textit{history}: per i comandi validi,
viene mantenuta una storia consultabile e rieseguibile di comandi (si
veda l'esempio \ref{fig:example_commandshistory}).

\begin{figure}
	\begin{verbatim}
	log> help
	...

	log> info
	Current log level: [v,vv,vvv]
	Quiet mode: false
	Log file: stdout

	log> log none

	log> info
	Current log level: []
	Quiet mode: false
	Log file: stdout

	log> up history
	3: [help]                   % primo comando eseguito
	2: [info]
	1: [log,none]
	0: [info]                   % ultimo comando eseguito

	log> up                     % esegue l'ultimo comando (come "up 0")
	Current log level: []
	Quiet mode: false
	Log file: stdout
	\end{verbatim}
	\caption{Esempio: history dei comandi}
	\label{fig:example_commandshistory}
\end{figure}

{\tolerance= 3000\relax
L'esecuzione di un comando valido viene attivata tramite il predicato
\texttt{doCommand/2} che riceve come primo argomento il comando e come
secondo argomento una lista (possibilmente vuota) di
argomenti. L'implementazione di questo predicato segue molto lo stile
di programmazione logico: il predicato distingue i casi a seconda del
primo argomento ed è implementato per svolgere funzioni diverse
appunto a seconda di quale sia il comando di input, per esempio:
\par}
\begin{verbatim}
doCommand(help, Args) => ...
doCommand(solve, Args) => ...
doCommand(...) => ...
\end{verbatim}
Questo ``\textit{swtich}'' potrebbe essere effettuato in modo più
imperativo sfruttando la presenza delle \textit{strutture di
  controllo} in Picat, ma si preferisce adottare questo pattern per
facilitare la lettura.

Questo modulo fornisce alcuni metodi di utilità per: la validazione
dell'input (\texttt{getKnownCommands/0} e
\texttt{getNoHistoryCommands/0}), la creazione di messaggi di errore
(\texttt{unknownCommand/1}, \texttt{wrongArgNumber/2} e
\texttt{wrongArgValues/2}), la gestione della \textit{history} dei
comandi (\texttt{push\textunderscore last\textunderscore command/2},
\texttt{get\textunderscore last\textunderscore command/0} e
\texttt{get\textunderscore last\textunderscore command/1}), la
gestione del solver (\texttt{doSolve/2}).

\subsubsection{global.pi}

Il modulo \texttt{global} gestisce le variabili globali. Aiuta il
programmatore a effettuare operazioni sulle variabili globali senza
conoscere il tipo di mappa globale utilizzata e senza effettuare
manipolazione diretta della mappa stessa.

\paragraph{Interfaccia}
Il modulo fornisce principalmente due metodi per creare e leggere
variabili globali.

\begin{itemize}
	\item \texttt{get\textunderscore global/1}, prende in input il
          nome della variabile globale (\emph{key}) e ne restituisce
          il valore associato. Se la chiave data in input non è
          associata a nessun valore l'eccezione
          \texttt{existence\textunderscore error/2} è sollevata.
	\item \texttt{set\textunderscore global/2}, prende in input
          una chiave \emph{key} e un valore \emph{value} e imposta in
          una mappa globale la variabile \emph{key} con valore
          \emph{value}.
\end{itemize}

L'implementazione corrente di questo modulo non consente la scelta
della mappa globale utilizzata per la memorizzazione delle variabili a
\emph{runtime}, ma ciò potrebbe essere oggetto di future migliorie.

\subsubsection{log\textunderscore h.pi}

Il modulo \texttt{log\textunderscore h} è pensato come un livello di
astrazione sull'I/O nativo di Picat, in grado di realizzare messaggi
di log con certe peculiarità.

Il modulo fornisce le seguenti caratteristiche.

\begin{itemize}
	\item \textbf{Livelli di log}. I livelli di log sono
          utilizzati per avere diverse granularità dei messaggi
          tracciati. I livelli integrati in questo modulo sono
	\begin{itemize}
		\item \texttt{none}, nessun log è effettuato;
		\item \texttt{v}, primo livello di verbosità. Mostra i
                  log con verbosità \texttt{v};
		\item \texttt{vv}, secondo livello di
                  verbosità. Mostra i log con verbosità \texttt{vv} e
                  \texttt{v};
		\item \texttt{vvv}, terzo livello di verbosità. Mostra
                  i log con verbosità \texttt{vvv}, \texttt{vv} e
                  \texttt{v};
		\item \texttt{all}, comprende tutti i livelli di
                  verbosità.
	\end{itemize}
	I tre livelli di verbosità predefiniti sono volutamente
        implementati con ereditarietà (e.g., il livello di verbosità
        \texttt{vvv} mostra i log anche dei livelli \texttt{vv} e
        \texttt{v} oltre ai propri). Comunque, il modulo permette di
        specificare altri livelli di verbosità qualora ve ne sia
        necessità e di darne un'implementazione ereditaria (vedere
        esempio \ref{fig:example_loglevel_noinheritance} e
        \ref{fig:example_loglevel_inheritance}).

	\item \textbf{Tipi di log}. I log possono avere tipi
          differenti: \texttt{debug}, \texttt{error} o \texttt{info},
          da utilizzare nel caso in cui il tipo del messaggio
          differisca. Il tipo non è determinante per il canale di
          output su cui il messaggio verrà loggato, ma è utilizzato
          per distinguere a colpo d'occhio il tipo dei log. A ogni
          messaggio di log viene aggiunto un prefisso, rispettivamente
          \texttt{D:}, \texttt{E:} o \texttt{I:}.

	\item \textbf{Canali di output}. I log possono essere
          tracciati su canali di output differenti. Di default vengono
          mostrati sullo standard output, ma tramite un file
          descriptor è possibile indicare il file sul quale scrivere i
          log.
\end{itemize}

\begin{figure}
	\begin{verbatim}
	log_mode(critical) => set_log_mode([critical]).

	test() =>
	    log_d("Critical message example", critical),
	    log_d("Warning message example", warning),
	    log_d("Notice message example", notice).

	% OUTPUT
	% D: Critical message example

	\end{verbatim}

	\caption{Esempio: livelli di log custom non ereditari}
	\label{fig:example_loglevel_noinheritance}
\end{figure}

\begin{figure}
	\begin{verbatim}
	log_mode(critical) => set_log_mode([critical, warning, notice]).

	test() =>
	    log_d("Critical message example", critical),
	    log_d("Warning message example", warning),
	    log_d("Notice message example", notice).

	% OUTPUT
	% D: Critical message example
	% D: Warning message example
	% D: Notice message example
	\end{verbatim}
	\caption{Esempio: livelli di log custom ereditari}
	\label{fig:example_loglevel_inheritance}
\end{figure}

\paragraph{Interfaccia}

L'interfaccia offerta da questo modulo consiste nei seguenti metodi
\begin{itemize}
	\item \texttt{log\textunderscore d/1},
          \texttt{log\textunderscore e/1}, \texttt{log\textunderscore
            i/1} attuano la scrittura vera e propria del messaggio di
          log sul file di destinazione con relativo tipo;
	\item \texttt{log\textunderscore d/2},
          \texttt{log\textunderscore e/2}, \texttt{log\textunderscore
            i/2} verificano che il secondo argomento (il livello di
          log) sia tra quelli impostati e in caso lanciano la
          scrittura del log;
	\item \texttt{log\textunderscore mode/1} imposta il log mode
          scegliendo tra una delle modalità implementate;
	\item \texttt{set\textunderscore log\textunderscore mode/1} e
          \texttt{get\textunderscore log\textunderscore mode/1}
          rispettivamente impostano un log mode arbitrario e ritornano
          il log mode impostato;
	\item \texttt{set\textunderscore log\textunderscore file/0 e
          get\textunderscore log\textunderscore file/0} impostano e
          ritornano rispettivamente il nome del file sul quale
          scrivere i log (di default questo valore è impostato a
          \texttt{stdout}).
\end{itemize}

\subsubsection{prompt.pi}

Il modulo \texttt{prompt} crea un livello di astrazione sopra l'I/O di
Picat, permettendo quindi una gestione più fine dell'input e
dell'output con formattazione e output condizionali, funzioni
predefinite per leggere valori booleani, stringhe, eccetera.

\paragraph{Interfaccia}

\begin{itemize}
	\item \texttt{prompt(Q) = A}. Mostra la domanda \texttt{Q} su
	      \texttt{stdout} all'utente e ne cattura una risposta arbitraria \texttt{A} da \texttt{stdin}.
	      Attualmente non implementato, solleva
          \texttt{not\textunderscore implemented\textunderscore
            exception} (predisposto nell'interfaccia per utilizzi
            futuri).
    \item \texttt{confirm(Q) = A}. Mostra la domanda \texttt{Q} su
          \texttt{stdout} all'utente e ne cattura la risposta
          \texttt{A} da \texttt{stdin} che deve essere uno tra i
          valori consentiti (y/n).
    \item \texttt{echo(P)}. Mostra la frase \texttt{P} su
          \texttt{stdout}, se la modalità \emph{quiet} non è
          impostata.
    \item \texttt{set\textunderscore quiet(B)} e
          \texttt{get\textunderscore quiet() = B} rispettivamente
          impostano e ritornano la quiet mode.
\end{itemize}

La \emph{quiet mode} viene utilizzata da tutto il modulo per gestire
l'I/O in modo condizionale. Per esempio, se la quiet mode è abilitata
allora gli echo non mostreranno nessun messaggio.

\subsubsection{assert.pi}

Il modulo \texttt{assert} implementa metodi di utilità per la gestione
degli \emph{unit tests}. In particolare è necessario avere una
batteria di test che sia in grado di notificare in modo semplice il
successo o il fallimento di un test.

Questo modulo implementa quindi delle funzioni di utilità che
gestiscono i test e sono in grado di confrontare i risultati attesi
con quelli attuali per decretare il successo (o fallimento) del test.

\paragraph{Interfaccia}
\begin{itemize}
	\item \texttt{new\textunderscore assert/1}. Il costruttore
          necessario per avere un oggetto di tipo assert tramite il
          quale identificare un test.
	\item \texttt{assert\textunderscore equal/2}. Confronta il
          risultato atteso (il primo parametro) con il risultato
          attuale (il secondo parametro) e verifica tramite
          l'uguaglianza di Picat (\texttt{==}\footnote{\`E necessario
            utilizzare il doppio uguale per non consentire a Picat di
            istanziare variabili \emph{unbound}: si vuole verificare
            l'identicità di due termini.}) che i due valori siano
          identici.
	\item \texttt{assert\textunderscore fail/0}. Asserisce un
          fallimento. Il meccanismo in questo caso è delicato: si
          rimanda all'esempio \ref{fig:example_unittest_assertfail}.
	\item \texttt{success/0} e \texttt{fail/0} forzano
          rispettivamente il successo o fallimento di un test.
\end{itemize}

\begin{figure}
	\begin{verbatim}
	% predicato che realizza il test di una certa funzionalità.

	test() ?=>

	    A = new_assert("test")

	    % solve è il predicato da testare, 
	    % di cui è atteso il fallimento.

	    solve(F, FF),

	    % se il controllo riesce a raggiungere questo punto della
	    % computazione significa che il predicato di cui era atteso
	    % il fallimento non è fallito, e ciò è da segnalare con un
	    % errore tramite A.fail()

	    A.fail().

	test() =>

	    A = new_assert("test"),

	    % se invece il predicato solve fallisce, il predicato
	    % test effettua il backtracking, scatenando la 
	    % computazione di questa regola.
	    % Ciò, a meno di fallimenti durante la creazione 
	    % dell'asserzione o all'esecuzione di metodi 
	    % dell'asserzione, ci garantisce che il test ha successo.

	    A.assert_fail().
	\end{verbatim}
 	\caption{Esempio: asserire un fallimento}
	\label{fig:example_unittest_assertfail}
\end{figure}

\section{Il solver}
\label{sec:lsetpicat_solver}

L'obiettivo principale del solver \lset{} è risolvere formule. Il
risultato può avere zero, una o più soluzioni e il solver deve essere
in grado di calcolarle tutte.

Il funzionamento del solver è quello descritto dallo pseudocodice in
\ref{subsec:clpbasedlang_lset_solver}. Per ricapitolare, il solver
svolge queste tre azioni:
\begin{itemize}
	\item rimpiazza i vincoli derivati con le corrispondenti
          formule \lset{};
	\item riduce la complessità sintattica dei vincoli primitivi
          applicando le regole di riscrittura corrette;
	\item elimina gli insiemi che coinvolgono disuguaglianze.
\end{itemize}
La formula finale ottenuta è semplificata, irriducibile ed equivalente alla forma originale.

\subsection{Predicato solve/2}
\label{subsec:lsetpicat_solver_solve2}

Il predicato \verb|solve/2| riceve in input una formula, e restituisce
in output la formula risolta. Questo predicato scandisce ogni termine
della formula congiuntiva data in input e cerca di ridurla generando
una nuova formula (eventualmente nulla) e un insieme di vincoli
(eventualmente vuoto).

\paragraph{Implementazione}

Il predicato \verb|solve/2| risolve la formula congiuntiva in input
$C$ e riscrive ogni termine in forma più semplice, creando un nuovo
constraint store $CN$. Se le riscritture applicate rendono il
constraint store uguale alla formula in input allora si è raggiunto un
\textbf{punto fisso} e si termina l'esecuzione con risultato $CC =
CN$, altrimenti si prosegue cercando di risolvere il nuovo constraint
store $solve(CN, CC)$.

\begin{verbatim}
%% solve(C, CC) is det

solve(C, CC) =>
    % nuovo constraint store
    CN = [],
    
    % ciclo su ogni termine della formula (congiunta)
    % Ad esempio per
    %   [ eq(X,1), eq(Y,2) ]
    % viene valutato prima il termine eq(X,1) e poi eq(Y,2)

    foreach (T in C)
        % procedura di risoluzione per il termine T,
        % C1 conterrà i nuovi vincoli generati
        sat(T, C1),

        % aggiungo i nuovi vincoli al constraint store
        CN := CN ++ C1,
    end,
    
    CN := CN.flatten(),

    if C == CN
    then CC = CN           % punto fisso
    else solve(CN, CC)     % continuo la risoluzione partendo da CN
    end.
\end{verbatim}

\paragraph{Utilizzo}
Il predicato \verb|solve/2| può essere usato come un API, esposta dal
modulo \emph{solver}. Il modulo \emph{commands} di fatto usa questo
predicato per risolvere una formula.
\begin{verbatim}
%% doSolve(+FormulaString) is semidet

doSolve(FormulaString) ?=>
    parse_term(FormulaString, Term, Vars),
    solve(Term, Res),
    println("Vars: " ++ Vars.to_string),
    println("Constraints: " ++ Res.to_string).
    nl,
    A = confirm("Another solution?"),
    if A == 1 then fail end.
doSolve(_) => println("no!").
\end{verbatim}

Il predicato \verb|solve/2| visto come API è utile anche
nell'effettuare gli \emph{unit tests}. L'esempio riportato, seppur poco
interessante dal punto di vista della formula, mostra l'utilizzo di
\verb|solve/2| per verificare la correttezza della risoluzione.
\begin{verbatim}
setlog_eq1_1_test ?=>
    A = new_assert("setlog_eq1_1_test"),
    F = [$eq(1, 1)],
    solve(F, FF),
    A.assert_equal([], FF).
setlog_eq1_1_test => A = new_assert("setlog_eq1_1_test"), A.fail().
\end{verbatim}

\subsection{Predicato sat/2}
\label{subsec:lsetpicat_solver_sat2}

Il predicato \verb|sat/2| combinato con \verb|rule/2| seleziona la
regola da applicare in base al termine dato, distinguendo se
l'operazione che si vuole compiere è $=, \neq, \in, \ldots$, e
applicando le giuste regole di riscrittura.

\paragraph{Implementazione}
\verb|sat/2| gestisce l'input, mentre \verb|rule/2| effettua il
dispatching della regola giusta. Notare come il predicato
\verb|rule/2| sia pensato per essere estendibile.
\begin{verbatim}
%% sat(F, FF) is det

sat(F, FF), F == [] => FR = [].
sat(F, FF) => rule(F, FF).

%% rule(F, R) is det

rule(eq(T1, T2), R)  => eq(T1, T2, R).
rule(neq(T1, T2), R) => neq(T1, T2, R).
rule(or(T1, T2), R)  => or(T1, T2, R).
rule(or(T), R)       => or(T, R).
rule(insl(X, S), R)  => insl(X, S, R).
rule(nin(X, S), R)   => nin(X, S, R).
rule(contains(S, X), R)    => contains(S, X, R).
rule(union(S1, S2, S3), R) => union(S1, S2, S3, R).
rule(disj(S1, S2), R)      => disj(S1, S2, R).
rule(subset(S1, S2), R)    => subset(S1, S2, R).
\end{verbatim}

Le regole implementate sono un sottoinsieme di quelle descritte in
\cite{Rossi18}.

\subsection{Vincoli integrati}
\label{subsec:lsetpicat_solver_rewriterules}

Nel modulo \emph{solver}, oltre ai predicati descritti in precedenza e
a qualche predicato ausiliario, sono presenti i predicati che
implementano le regole di riscrittura per i seguenti vincoli:
\begin{itemize}
\item \verb|eq/3| ($=$);
\item \verb|neq/3| ($\neq$)
\item \verb|insl/3| ($\in$)
\item \verb|contains/3| ($contains$);
\item \verb|union/3| ($\cup$);
\item \verb|disj/3| ($||$);
\item \verb|subset/3| ($\subset$);
\item \verb|inters/3| ($\cap$);
\item \verb|diff/3| ($\setminus$);
\end{itemize}

\section{Il vincolo or}
\label{sec:lsetpicat_or}

Molte regole di riscrittura integrate dal solver non contengono solo
clausole in congiunzione (legate da $\land$), ma anche clausole in
disgiunzione. Questa sottile differenza porta un grosso cambiamento
nella gestione del controllo durante la risoluzione di formule. Da un
punto di vista algoritmico, mentre le clausole congiunte si possono
risolvere una dopo l'altra catturando il primo fallimento per
interrompere la computazione, le clausole disgiunte non godono della
stessa proprietà. Di fatto, se una clausola in disgiunzione fallisce,
non è detto che le altre lo facciano, anzi, spesso non è così. Bisogna
quindi essere in grado di tornare al punto in cui si è scelta una
delle clausole in \emph{or} da risolvere, ripristinando lo stato del
programma, per poter proseguire con la successiva.

Per l'implementazione di questo meccanismo viene in aiuto il
\emph{backtracking}, che simula proprio il funzionamento in
questione. Il backtracking è un algoritmo generale che permette di
trovare tutte (o alcune) soluzioni a un certo problema
computazionale, che incrementalmente costruisce nuove soluzioni
abbandonando quelle che sono state decretate non essere una
soluzione. Durante la risoluzione di formule insiemistiche questo si
può verificare appunto prendendo una clausola in disgiunzione che non
soddisfa i vincoli e provoca il fallimento. Il backtracking in questo
caso scarta la soluzione, ripristina il programma al punto di scelta
(\emph{choice point}) e prosegue con un'altra delle clausole
non ancora esplorate.

L'implementazione del vincolo or nel solver è costruito in due modi:
\begin{itemize}
	\item tramite l'utilizzo di un vincolo ausiliario;
	\item sfruttando il backtracking sulla regola esatta che
          presenta clausole in disgiunzione.
\end{itemize}

Nel primo caso l'implementazione è simile a quella di una regola di
riscrittura
\begin{verbatim}
%% or(List, Result) is nondet
%
% @desc Rewrite rule for or constraints.

or([], []) => true.
or([T|_Tr], R) ?=> R = [T].
or([_T|Tr], R) => or(Tr, R).
\end{verbatim}
dove
\begin{itemize}
	\item la prima regola gestisce il caso in cui la lista di
          clausole in or sia vuota, e ha sempre successo;
	\item la seconda regola gestisce la prima riscrittura: estrae
          una clausola prendendola dalla testa della lista e la
          inserisce nel risultato;
	\item la terza regola gestisce il caso in cui la seconda
          regola fallisca (ovvero la clausola utilizzata non ha
          soddisfatto la formula) procedendo con un'altra clausola
          della lista.
\end{itemize}

\paragraph{Esempio}
\begin{verbatim}
{log} => [eq(X,1),or([eq(X,2),eq(X,1)])]
\end{verbatim}

\begin{itemize}

	\item[Step 1] Il risultato della prima riscrittura è
	\begin{verbatim}
	--- [eq(1,1),or([eq(1,2),eq(1,1)])]
	==> [eq(1,2)]
	\end{verbatim}
	e si può notare come il vincolo \verb|eq(1,1)| sia stato
        risolto e rimosso dal constraint store risultate, mentre il
        vincolo \verb|or([eq(X,2),eq(X,1)])| sia stato riscritto in
        \verb|eq(1,2)|.

	\item[Step 2] Il risultato della seconda riscrittura è
	\begin{verbatim}
	--- [eq(1,1),or([eq(1,2),eq(1,1)])]
	==> [eq(1,1)]
	\end{verbatim}
	da cui invece è evidente il fallimento nella risoluzione di
        \verb|eq(1,2)|, e la riscrittura del vincolo
        \verb|or([eq(X,2),eq(X,1)])| in \verb|eq(1,1)|.

	\item[Step 3] Il risultato della terza riscrittura è
	\begin{verbatim}
	--- [eq(1,1)]
	==> []
	\end{verbatim}
	da cui si nota la risoluzione dell'ultimo vincolo rimasto.

\end{itemize}

\section{Enumerazione delle soluzioni}
\label{sec:lsetpicat_solutions}

Il solver per ogni formula può trovare zero, una o più
soluzioni. L'enumerazione di queste soluzioni è di notevole importanza
per \lset{}. Per questo motivo il solver deve essere in grado di
cercare altre soluzioni qualora ve ne siano. Anche in questo caso si
ricorre al backtracking.

L'enumerazione di nuove soluzione è infatti implementata forzando un
fallimento: tramite il bakctracking si cercano di esplorare strade
alternative per la costruzione di altri risultati e se queste
alternative sono infinite allora anche questo processo è infinito.

\paragraph{Esempio}
\begin{verbatim}
{log} => [ union( [1|X], [1,2], [1,2] ) ]
\end{verbatim}
ha 4 soluzioni
\begin{itemize}
	\item \verb|X = []|;
	\item \verb|X = [1]|;
	\item \verb|X = [2]|;
	\item \verb|X = [1,2]|
\end{itemize}
che sono costruite dal solver una dopo l'altra, simulando il
non-determinismo.

\section{Testing}
\label{sec:lsetpicat_testing}

La stesura dei test per verificare la correttezza dell'implementazione
è un'operazione necessaria al fine di incrementare la qualità del
software prodotto. Per questo motivo sono stati realizzati predicati
che prendono in esame casi semplici ma cercano di esplorare i casi
limite.

I test realizzati fanno uso del modulo \verb|assert| che mette a
disposizione metodi di utilità come \verb|assert_equal/2|,
\verb|assert_fail/1|, \verb|fail/1|. Grazie a questi predicati è
possibile effettuare test con la seguente struttura
\begin{verbatim}
test1 ?=>
    A = new_assert(test1)
    solve(Formula, Result),
    A.assert_equal([], Result)
test1 =>
    A = new_assert(test1), A.fail().
\end{verbatim}
dove \verb|assert_equal/2| verifica che il valore attuale sia uguale
al valore previsto, e se non lo è fallisce attivando il predicato
\verb|fail/1| che registra il fallimento di quel test.



%%% *******************************************************
%%% Implementazione delle regole di riscrittura   *********
\chapter{Implementazione delle regole di riscrittura}
\label{ch:impl}

%\minitoc

In questo capitolo è riportata l'implementazione in Picat delle regole
di riscrittura descritte con notazione matematica in
\ref{subsec:clpbasedlang_lset_rewriteeq},
\ref{subsec:clpbasedlang_lset_rewriteset} e
\ref{subsec:clpbasedlang_lset_rewriteneg}. Si può notare che la
descrizione matematica delle regole in \cite{Rossi18} è molto vicina
all'implementazione. L'implementazione di queste regole è stata fatta
con un occhio di riguardo alla leggibilità e alla semplicità del
codice; esiste già un'implementazione del solver in un linguaggio
logico: \setlog{} in Prolog, che però risulta piuttosto complicata da
capire per chi non ha familiarità con il Prolog.

Le implementazioni riportate sono quelle per le regole di riscrittura
fondamentali. Gli altri vincoli sono stati implementati in modo del
tutto analogo.

\section{Il vincolo eq}

Il vincolo di uguaglianza è uno dei vincoli più importanti di \lset{}
in quanto tratta l'unificazione insiemistica, operazione complessa e
piuttosto delicata. Il vincolo $=$ è un vincolo binario e
nell'implementazione è rappresentato come un predicato con tre
argomenti: i primi due sono i due termini sui quali si applica il
vincolo mentre il terzo è il risultato e contiene la riscrittura del
vincolo.

Le regole elencate per questo predicato rappresentano una sorta di
``switch'': in base ai due termini di input viene selezionata la
riscrittura corretta da applicare. Ciò, sfruttando le regole di
pattern-matching di Picat, è effettuato tramite apposite condizioni
che specificano l'applicabilità dei predicati.

Il non determinismo è utilizzato solo per le regole con clausole in
disgiunzione, dove il fallimento della regola è contemplato, e non
determina il fallimento dell'intera riscrittura.

\begin{algorithm}[H]
	\caption{Regole di riscrittura per vincoli di uguaglianza}
	\label{alg:eq_constraints}
\end{algorithm}
\begin{verbatim}
eq(T1, T2, R),  T1 == T2 =>                                % 1
    R = [].

eq(T1, T2, R), nonvar(T1), var(T2) =>                      % 2
    R = [ $eq(T2, T1) ].

eq(T1, T2, R),
        var(T1), T2.is_lset(),
        not occur_check(T1, T2.lset_head()),
        T1 == T2.lset_rest() =>                            % 3
   	% costruzione di un nuovo insieme con la testa
   	%  di T2 e un nuovo resto N.
    YSetNew = new_lset(T2.lset_head(),_N),
    R = [ $eq(T1, YSetNew) ].

eq(T1, T2, _R),
        var(T1),
        occur_check(T1, T2) =>                             % 4
    fail.  % sic.

eq(T1, T2, R),
        var(T1) =>                                         % 5
    % si rimuove il vincolo e si effettua 
    % l'unificazione.
    R = [], 
    T1 = T2.

eq(T1, T2, _R),
        struct(T1), struct(T2),
        T1.name() !== T2.name() =>                         % 6
    % le funzioni di L_SET possono essere rappresentate
    % da struct: $f(1,2), $g(f, X), ...
    fail.  % sic.

eq(T1@[X|Xs], T2, R),
        T1.is_lset(), T2.is_lset(),
        T1.lset_rest() == T2.lset_rest() ?=>               % 7a
    % regola ri riscrittura 7 che implementa la prima
    % clausola in or.

    YH = T2.lset_head(),                   % head of T2.
    foreachnd_slice(YH, YElem, YSlice),    % get j-th elem nondet.
    YRest = T2.lset_rest(),                % rest of T2.
    YSetSliced = new_lset(YSlice, YRest),  % T2 without j-th elem.

    R1 = [ $eq(X, YElem) ],
    R2 = [ $eq(Xs, YSetSliced) ],

    R = R1 ++ R2.

eq(T1@[X|_], T2, R),
        T1.is_lset(), T2.is_lset(),
        T1.lset_rest() == T2.lset_rest() ?=>               % 7b
    % regola ri riscrittura 7 che implementa la seconda
    % clausola in or.

    YH = T2.lset_head(),                   % head of T2.
    foreachnd_slice(YH, YElem, YSlice),    % get j-th elem nondet.
    YRest = T2.lset_rest(),                % rest of T2.
    YSetSliced = new_lset(YSlice, YRest),  % T2 without j-th elem.

    R1 = [ $eq(X, YElem) ],
    R2 = [ $eq(T1, YSetSliced) ],

    R = R1 ++ R2.

eq(T1@[X|Xs], T2, R),
        T1.is_lset(), T2.is_lset(),
        T1.lset_rest() == T2.lset_rest() ?=>               % 7c
    % regola ri riscrittura 7 che implementa la terza
    % clausola in or.

    % no slice for T2, only Y elem.
    YH = lset_head(T2),              % head of T2.
    foreachnd_slice(YH, YElem, _),   % get j-th elem nondet.

    R1 = [ $eq(X, YElem) ],
    R2 = [ $eq(Xs, T2) ],

    R = R1 ++ R2.

eq(T1@[X|Xs], T2, R),
        T1.is_lset(), T2.is_lset(),
        T1.lset_rest() == T2.lset_rest() =>                % 7d
    % regola ri riscrittura 7 che implementa la quarta
    % clausola in or.

    XRest = lset_rest(T1),

    XHeadSlice = lset_head(Xs),
    XSetNew = new_lset(XHeadSlice, N),

    YHead = T2.lset_head(),
    YSetNew = new_lset(YHead, N),

    R1 = [ $eq(XRest, [X|N]) ],
    R2 = [ $eq(XSetNew, YSetNew) ],

    R = R1 ++ R2.

eq(T1@[X|Xs], T2@[Y|Ys], R),
        T1.is_lset(), T2.is_lset() ?=>                     % 8a
    R = [ 
        $eq(X,Y), 
        $eq(Xs, Ys) 
    ].

eq(T1@[X|_], T2@[Y|Ys], R),
        T1.is_lset(), T2.is_lset() ?=>                     % 8b
    R = [ 
        $eq(X,Y), 
        $eq(T1, Ys) 
    ].

eq(T1@[X|Xs], T2@[Y|_], R),
        T1.is_lset(), T2.is_lset() ?=>                     % 8c
    R = [ 
        $eq(X,Y), 
        $eq(Xs, T2) 
    ].

eq(T1@[X|Xs], T2@[Y|Ys], R),
        T1.is_lset(), T2.is_lset() =>                      % 8d
    R = [
        $eq( Xs,  [Y|N] ),
        $eq( [X|N],  Ys )
    ].

eq(T1, T2, R),
        T1.struct(), T2.struct(),
        T1.name() == T2.name(),
        T1.arity() == T2.arity() =>                        % 9
    RR = [],
    foreach(I in 1..T1.arity())
        RR := RR ++ [  $eq( T1[I], T2[I] )  ]
    end,
    R = RR.
\end{verbatim}

\section{Il vincolo neq}

Il vincolo $neq$ rappresenta la negazione del vincolo $eq$. La negazione classica in \lset{} viene evitata: si vuole avere a disposizione un predicato positivo che rappresenti la negazione di un altro predicato (si veda \ref{subsec:clpbasedlang_lset_rewriteneg} per approfondimenti). L'algoritmo \ref{alg:neq_constraints} implementa proprio questa funzionalità.

\begin{algorithm}[H]
	\caption{Regole di riscrittura per vincoli di non disuguaglianza}
	\label{alg:neq_constraints}
\end{algorithm}
\begin{verbatim}
neq(T1, T2, R),
        ground(T1), ground(T2),
        T1 !== T2 =>                                       % ground
    R = [].

neq(T1, T2, R),
        T1 == T2 =>                                        % 1
    log_d_vv("neq :: neq_1"),
    fail.  % sic.

neq(T, X, R),
       	nonvar(T), var(X) =>                               % 2
    R = [ $neq(X, T) ].

neq(X, S, R),
        S.is_lset(),
        X == S.lset_rest(),
        not occur(X, S.lset_head()) =>                     % 3
    RR = [],
    foreach (T in S.lset_head)
        RR := RR ++ [$nin(T, X)]
    end,
    R = [ $or(RR) ].

neq(X, T, R),
       	occur(X, T) =>                                     % 4
    R = [].

neq([T1|A], [T2|B], R) ?=>                                 % 5a
    log_d_vv("neq :: neq_5a"),
    R = [ 
        $inls(N, [T1|A], 
        $nin(N, [T2|B])) 
    ].

neq([T1|A], [T2|B], R) ?=>                                 % 5b
    log_d_vv("neq :: neq_5a"),
    R = [ 
        $nin(N, [T1|A]), 
        $insl(N, [T2|B]) 
    ].

neq(F, G, R),
        F.struct(), G.struct(),
        F.name() !== G.name() =>                           % 6
    log_d_vv("neq :: neq_6"),
    R = [].

neq(F, G, R),
        F.struct(), G.struct(),
        F.arity() !== G.arity() =>                         % 7
    log_d_vv("neq :: neq_7"),
    R = [].

neq(X, T, R),
        not occur(X, T) =>                                 % irr
    log_d_vv("neq :: neq_irr"),
    R = [ $neq(X, T) ].
\end{verbatim}

\section{Il vincolo in}

Il vincolo $in$ è uno dei vincoli fondamentali che lavora su
insiemi. Implementa in modo molto diretto l'appartenenza
insiemistica. Il predicato \texttt{insl/3} rappresenta il vincolo $in$
in quanto \texttt{in} è una keyword riservata di Picat. Per questo
motivo si è deciso di introdurre il vincolo $contains$, che ha la
stessa semantica del vincolo $in$, ma con gli argomenti invertiti. Il
predicato \texttt{contains/3} infatti implementa le stesse regole di
riscrittura del vincolo $in$, ma prendendo come primo argomento un
insieme e come secondo un termine anziché il contrario.

\begin{algorithm}[H]
	\caption{Regole di riscrittura per vincoli di appartenenza}
	\label{alg:in_constraints}
\end{algorithm}
\begin{verbatim}
insl(X, S, R) =>
    % si potrebbe anche riscrivere il vincolo piuttosto
    % che effettuare subito la chiamata al predicato che 
    % implementa il "contains". In questo caso, comunque,
    % il comportamento è il medesimo.
    contains(S, X, R).

contains(S, X, R),
        S.is_lset(),
        S.is_emptyset() =>                                 % 1
    fail.

contains(S@[Y|A], X, R),
        S.is_lset() ?=>                                    % 2a
    R = [ $eq(X, Y) ].

contains(S@[Y|A], X, R),
        S.is_lset() =>                                     % 2b
    R = [ $contains(A, X) ].

contains(A, X, R),
        var(A) =>                                          % 3
    YN = new_lset(X, N),
    R = [ $eq(A, YN) ].
\end{verbatim}

\section{Il vincolo union}

Il vincolo $union$ è uno dei vincoli più importanti di \lset{}: viene
impiegato per la realizzazione di vincoli derivati come \textit{diff}
(differenza insiemistica). E' un vincolo piuttosto complicato in
quanto molte delle sue regole utilizzano clausole in disgiunzione, le
quali complicano soprattutto il debugging. L'algoritmo
\ref{alg:in_constraints} ne riporta l'implementazione.

\begin{algorithm}[H]
	\caption{Regole di riscrittura per vincoli di appartenenza}
	\label{alg:un_constraints}
\end{algorithm}
\begin{verbatim}
union(S1, S2, S3, R),
        S1 == S2 =>                                        % 1
    R = [ $eq(S1, S3) ].

union(S1, S2, S3, R),
        S3.is_emptyset() =>                                % 2
    R = [
        $eq(S1, S3),
        $eq(S2, S3)
    ].

union(E, A, B, R),
        E.is_emptyset(),
        var(B) =>                                          % 3
    R = [ $eq(B, A) ].

union(A, E, B, R),
        E.is_emptyset(),
        var(B) =>                                          % 4
    R = [ $eq(B, A) ].

union(S@[T|C], A, B, R),
        S.is_lset(),
        var(B) ?=>                                         % 5a
    R = [
        $nin(T, A),
        $un(N1, A, N),
        $eq([T|C], [T|N1]),
        $eq(B, [T|N])
    ].

union(S@[T|C], A, B, R),
        S.is_lset(),
        var(B) =>                                          % 5b
    R = [
        $eq(A, [T|N2]),
        $un(N1, N2, N),
        $eq([T|C], [T|N1]),
        $eq(B, [T|N])
    ].

union(A, S@[T|C], B, R),
        S.is_lset(),
        var(B) ?=>                                         % 6a
    R = [
        $nin(T, A),
        $un(N1, A, N),
        $eq([T|C], [T|N1]),
        $eq(B, [T|N])
    ].

union(A, S@[T|C], B, R),
        S.is_lset(),
        var(B) =>                                          % 6b
    R = [
        $eq(A, [T|N2]),
        $un(N1, N2, N),
        $eq([T|C], [T|N1]),
        $eq(B, [T|N])
    ].

union(A, B, S@[T|C], R),
        S.is_lset() ?=>                                    % 7a
    R1 = [
        $eq(A, [T|N1]),
        $un(N1, B2, N)
    ],
    R4 = [ $eq([T|C], [T|N]) ],

    R = R1 ++ R4.

union(A, B, S@[T|C], R),
        S.is_lset() ?=>                                    % 7b
    R2 = [
        $eq(B, [T|N1]),
        $un(A, N1, N)
    ],
    R4 = [ $eq([T|C], [T|N]) ],

    R = R2 ++ R4.

union(A, B, S@[T|C], R),
        S.is_lset() =>                                     % 7c
    R3 = [
        $eq(A, [T|N1]),
        $eq(B, [T|N2]),
        $un(N1, N2, N)
    ],
    R4 = [ $eq([T|C], [T|N]) ],

    R = R3 ++ R4.

union(S1, S2, S3, R),
        var(S1), var(S2), var(S3),
        S1 !== S2 =>                                       % irr
    R = [ $un(S1, S2, S3) ].
\end{verbatim}



%%% *******************************************************
%%% *   Uso del solver   **********************************
\chapter{Uso del solver \lset{} da Picat}
\label{ch:use}

%\minitoc

In questo capitolo vengono dati degli esempi di utilizzo del solver per
casi d'uso comuni. Nella sezione \ref{sec:use_interactive} si mostra
l'utilizzo del risolutore tramite la modalità interattiva, mentre in
\ref{sec:use_api} si illustra l'utilizzo dello stesso tramite API.

\section{Modalità interattiva}
\label{sec:use_interactive}

La modalità interattiva consente l'uso del solver da CLI, tramite
interazione da linea di comando (possibili evoluzioni potrebbero
sostituire la CLI con una interfaccia utente più evoluta, come 
una GUI).
Questa modalità è utilizzata per scopi fine a se stessi, come il
testing del sistema e la risoluzione isolata di formule.

\subsection{Avvio dell'interprete}

L'interprete di \lset{} è avviato tramite alcuni semplici passi:
\begin{enumerate}
	\item avvio dell'interprete Picat;
	\item caricamento dei sorgenti di \lset{} (grazie al sistema
          di import è possibile caricare solamente il file che
          contiene la chiamata iniziale da eseguire);
	\item compilazione dei sorgenti caricati;
	\item esecuzione della procedura iniziale.
\end{enumerate}

Questi step nella pratica si traducono in
\begin{verbatim}
$ Picat
picat> load(main.pi)
picat> compile(main.pi)
picat> main.
\end{verbatim}
oppure, grazie a una forma più concisa, in 
\texttt{picat main.pi} (vedere
esempio \ref{fig:example_interpreterstart}).

\begin{figure}
	\begin{verbatim}
	$ picat main.pi

	This is the pure implementation of {log} in Picat.
	Copyright (C) 2019 Luca Parolari <luca.parolari23@gmail.com>
	This program is free software, covered by the MIT License
	There is ABSOLUTELY NO WARRANTY for this program.
	Type 'copying' to see the conditions
	Type 'warranty' for details.
	Type 'help' for advice, 'quit' to exit.

	Default settings follows.

	Current log level: [v,vv,vvv]
	Quiet mode: false
	Log file: stdout

	log>
	\end{verbatim}
	\caption{Esempio: avvio dell'interprete}
	\label{fig:example_interpreterstart}
\end{figure}

\subsection{Comandi disponibili}

La modalità interattiva permette all'utente di interagire con il
sistema tramite dei comandi. I comandi disponibili sono
\begin{itemize}
	\item \texttt{help}, mostra informazioni sull'utilizzo dei
          comandi e/o la documentazione degli stessi;
	\item \texttt{info}, mostra lo stato delle impostazioni del
          sistema;
	\item \texttt{up}, riesegue l'$n$-esimo comando o mostra la
          lista dei comandi eseguiti;
	\item \texttt{log}, imposta il log mode oppure il nome del
          file sul quale scrivere i log;
	\item \texttt{solve}, risolve una formula leggendola da
          diversi canali di input;
	\item \texttt{quiet}, imposta la modalità silenziosa per le
          interazioni utente.
\end{itemize}

Informazioni più dettagliate possono essere reperite eseguendo il
comando \texttt{help} (esempio in figura
\ref{fig:example_helpcommand}) che mostra i comandi offerti dalla CLI
e la loro descrizione.

\begin{figure}
\begin{verbatim}
log> help
Setlog provides you with the following commands:

help
help <what>
    Show help for <what>.
    The argument describes the topic to give help for.
    <what> can be one of [solve]

info
    Display the current interpreter status.

up history
    Print the whole commands history.
up <n>
    Redo the last <n> command issued.
    If <n> is empty the last command is issued,
    this is equivalent to `up 0`.

log <mode>
    Set the log mode to <mode>.
    Available log mode: [none,v,vv,vvv,all].
log file <file>
    Set log file to <file>.
    Default is `stdout`.

solve
solve <formula>
solve file <file>
    Solve the formula, respectively, typed in stdin,
    given as argument of this command, or read from the
    first line of file <file> using the setlog solver.

quiet <mode>
    Set the quit mode execution.
    Available mode: [true, false]. Default is true.
\end{verbatim}

	\caption{Esempio: comando help}
	\label{fig:example_helpcommand}
\end{figure}

\subsection{Configurazione}

La modalità interattiva permette una piccola configurazione del
sistema. In particolare l'utente può scegliere
\begin{itemize}
	\item il livello di log da visualizzare;
	\item il file su cui scrivere i log;
	\item di visualizzare o meno i messaggi del solver (ad esempio, 
	      i passaggi delle riscritture).
\end{itemize}

Configurazioni di basso livello sul sistema o sul solver
sono proibite o determinate a tempo di compilazione, all'utente
non è quindi permessa la modifica.

Un esempio di configurazione è mostrato in figura
\ref{fig:example_confcommands}.

\begin{figure}
	\begin{verbatim}
	log> info
	Current log level: [v,vv,vvv]
	Quiet mode: false
	Log file: stdout

	log> log none

	log> quiet true

	log> info
	Current log level: []
	Quiet mode: true
	Log file: stdout
	\end{verbatim}
	\caption{Esempio: comandi di configurazione}
	\label{fig:example_confcommands}
\end{figure}

\subsection{Risoluzione di formule}

La modalità interattiva offre tre procedure la risoluzione di formule,
che differiscono dal canale di input dal quale la formula viene letta.

Il comando \texttt{solve} svolge appunto questa funzione, e
\begin{itemize}
	\item se non viene specificato nessun argomento, la formula
          viene letta da \texttt{stdin};
	\item se il primo argomento è \texttt{file} la formula viene
          letta dalla prima riga del file indicato come secondo
          argomento;
	\item altrimenti gli argomenti vengono considerati una formula
          e ne viene effettuato il parsing (se possibile).
\end{itemize}

Si veda l'esempio in \ref{fig:example_solvecommands}

\begin{figure}
	\begin{verbatim}
	log> solve                       % formula da stdin
	{log} => [ eq(X,1) ]

	Vars: (map)[X = 1]
	Constraints: []

	Another solution? (y/n): y
	no!
	log>
	log> solve [ eq(X,1) ]           % formula come argomento
	                                 % del comando
	{log} => [eq(X,1)]
	Vars: (map)[X = 1]
	Constraints: []

	Another solution? (y/n): y
	no!
	log>
	log> solve file formula1.lset    % formula da file
	{log} => [ eq(X,1) ]
	Vars: (map)[X = 1]
	Constraints: []

	Another solution? (y/n): y
	no!
	log>
	\end{verbatim}
	\caption{Esempio: comando solve (e varianti) della modalità interattiva}
	\label{fig:example_solvecommands}
\end{figure}

\section{API}
\label{sec:use_api}

L'utilizzo vero e proprio del solver solitamente non è quello da linea
di comando, bensì da altri programmi che lavorano con formule e
necessitano di risolvere le stesse per poter combinare i risultati in
modelli teorici. E' questo il caso del linguaggio Z, utilizzato per
descrivere formalmente la specifica di programmi. Il linguaggio Z è
basato sui concetti e sulla sintassi della matematica, e in
particolare della teoria degli insiemi. Le specifiche Z sono
convertite in programmi eseguibili, scritti in linguaggi come il Java
(si veda \cite{DeSantis17}).

Per questo motivo anche l'implementazione di questo solver fornisce
API tramite le quali altri programmi possono interagire con il
solver. E' il caso del metodo \verb|solve/2| che come primo argomento
riceve una formula e nel secondo argomento restituisce la formula
risolta.

\paragraph{Esempio} (pseudocodice)
\begin{verbatim}
%%% my_program.pi

import solver.

my_predicate =>
    computazione arbitraria ...

    % risoluzione della formula F con il solver
    %  scritto in Picat
    solve(F, Result),

    utilizzo del risultato Result ...
\end{verbatim}



%%% *******************************************************
%%% *   Conclusione   *************************************
\chapter{Conclusione e lavori futuri}
\label{ch:conclusion}

Il risultato principale di questo lavoro di tesi è stata la
progettazione e implementazione in Picat di un constraint solver per
formule insiemistiche, basato sul lavoro descritto in
\cite{Dovier00}. Per ottenere questo risultato è stato necessario,
prima di tutto, di sperimentare e capire Picat, un linguaggio logico
nuovo e molto innovativo, che cerca di prendere di petto tutti i
problemi tradizionali dei linguaggi logici e risolverli, semplificando
il compito del programmatore. Di fatto Picat possiede un sistema molto
ricco e completo di funzionalità, che semplificano veramente alcuni
compiti ricorrenti durante la stesura di un programma logico: in
questo esperimento, la facilità di stesura dei moduli di corredo al
solver è stata veramente evidente. Ad esempio, per il modulo di
gestione della command line interface, si è riusciti a scrivere del
codice molto leggibile, chiaro e manutenibile, grazie all'utilizzo
combinato del paradigma imperativo e logico. La gestione dell'I/O,
notevolmente semplificata in Picat, ha reso evidente i vantaggi che
Picat può offrire quando il paradigma logico non è necessario. Il
discorso è differente invece per il solo paradigma logico.

Purtroppo
(o per foruna) Picat possiede delle nette differenze da altri
linguaggi logici come Prolog, per nominarne uno, che influiscono
pesantemente sulla progettazione e sul comportamento del sistema. (In
\ref{sec:picat_picatvsprolog} queste differenze sono trattate più
approfonditamente). Differenze così pesanti complicano, e non di poco,
l'utilizzo di Picat con il paradigma logico, che in alcuni casi si
rivela non del tutto appropriato a risolvere questo tipo di
problemi. Limitazioni sull'uso degli operatori e l'aggiunta di
operatori definiti da utente e sulla sintassi dei termini trattabili
da Picat hanno di nuovo influito sul risultato finale, forzando la
risoluzione di alcuni problemi con workaround.

Per questo lavoro di tesi si sono concentrati gli sforzi nella
realizzazione del risolutore di formule stesso, per arrivare ad avere
un'implementazione funzionante di \lset{} in Picat, e, di fatto, sono
stati tralasciati numerosi dettagli.  Uno dei dettagli non considerati
è stato la rappresentazione delle formule. Nell'implementazione Picat
di \lset{} non è stato possibile adottare la rappresentazione delle
formule di \lset{} adottata in \setlog{} a causa delle citate
limitazioni di Picat rispetto al Prolog sulla forma sintattica dei
termini.  Si è quindi utilizzato per il momento una sintassi
nettamente più vicina alla rappresentazione interna di Picat. La
soluzione a questo problema è riassumibile dallo schema seguente
\begin{figure}[H]
	\centering
	\begin{tikzpicture}
	[node distance=.8cm,start chain=going below,]
	\node[punktchain, join] (a) {Formule \lset{}\\ $X = \{1|Y\}$};
	\node[punktchain, join] (b) {Formule in rappresentazione Picat\\ \texttt{  [eq(X, [1|Y])]}};
	\node[punktchain, join] (c) {Solver};
	\end{tikzpicture}
\end{figure}
che aggiunge un livello: il parsing delle formule \lset{}.  In questo
modo il solver non ha bisogno di modifiche: le formule manipolate sono
sempre rappresentate con una sintassi vicina a quella di Picat, ma
l'utente (sia umano che non) può lavorare con formule \lset{}.  Così
facendo, inoltre, si può decidere di realizzare questo livello
intermedio in un linguaggio diverso da Picat. Possiamo citare Prolog,
ad esempio, con il modulo DCG \cite{MetalevelDCG} (Definite Clause
Grammar) che consente di effettuare il parsing di frasi dando la
grammatica a clausole definite.

Un altro aspetto sicuramente da migliorare riguarda la verifica della
correttezza sulla risoluzione delle formule. Il testing del solver non
era obiettivo di questo lavoro di tesi, ma si è reso necessario per
capire, almeno indicativamente, l'aderenza dell'implementazione alla
teoria. I casi esaminati non sono ovviamente esaustivi e non coprono
nemmeno tutti i casi limite che andrebbero verificati.

Una futura espansione al solver invece potrebbe prevedere
l'integrazione delle funzioni parziali, andando quindi a considerare
l'intero linguaggio attualmente supportato da \setlog{} e \jsetl{} e
non un suo sottoinsieme.



%%% *******************************************************
%%% *   Ringraziamenti   **********************************
\setsecnumdepth{none}
\chapter{Ringraziamenti}
\resetsecnumdepth

Vorrei spendere qualche parola per ringraziare tutti coloro che durante
questi tre duri anni mi hanno supportato e sostenuto, mi hanno spinto
a non mollare mai, a mettercela tutta per cercare di raggiungere
obiettivi degni di nota nel racconto di una vita.

\bigskip

Vorrei ringraziare per prima la mia famiglia, che dal primo giorno in
cui ho pensato intraprendere la carriera universitaria fino al giorno
della laurea ha creduto in me.

Ringrazio mia mamma, che con la sua umiltà mi ha insegnato a tirare
fuori sempre il meglio, rimanendo umile e modesto, senza la pretesa di
essere il migliore o più importante degli altri.

Mio papà, che con la sua franchezza e i suoi (strani) motti mi ha
sempre spronato.

I miei due fratellini, che con la loro leggerezza hanno saputo farmi
ridere anche nei momenti più bui.

Le mie nonne, con la loro cura e apprensione e mio nonno, con la sua
bontà che da lassù mi guarda ed è sempre con me.

\bigskip

Ringrazio anche Francesco che con la sua disponibilità e infinita
pazienza mi ha aiutato in moltissime situazioni.

\bigskip

Ringrazio Antonio e Silvio, per i loro preziosi consigli e
l'accompagnamento dal punto di vista professionale e lavorativo.

\bigskip

Ringrazio tutti quelli che in un modo o nell'altro mi hanno dedicato
un aiuto, un ``buona fortuna'' a un esame o una risata,
accompagnandomi in questo percorso.

\bigskip

Infine, un grazie speciale lo devo a Giulia che ha saputo sostenermi
in tutto e per tutto, donandomi la forza che mi è mancata. Ma per
questo forse servirebbe un'altra tesi.

\bigskip
\bigskip

\begin{flushright}
	Parma, 26 settembre 2019
\end{flushright}



%%% *******************************************************
%%% *   List of Figures/Algorithms   **********************
%\listoffigures
%\listofalgorithms



%%% *******************************************************
%%% *   Bibliograpy   *************************************
\printbibliography
\addcontentsline{toc}{chapter}{Bibliografia}



\end{document}