-
Notifications
You must be signed in to change notification settings - Fork 0
/
thesis.tex
3571 lines (2961 loc) · 122 KB
/
thesis.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
% !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 \\