-
Notifications
You must be signed in to change notification settings - Fork 0
/
JOURNAL.txt
467 lines (345 loc) · 20.5 KB
/
JOURNAL.txt
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
******************************************************************************
******************************************************************************
**************** ****************
**************** PICAT SETLOG JOURNAL ****************
**************** ****************
******************************************************************************
******************************************************************************
Luca Parolari <luca.parolari23@gmail.com>
This document, apart from headers, is intentionally in italian. The headers
represents a summary of what were done in the specified date.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 11 Genuary -
------------------------------------------------------------------------------
- The beginning -
------------------------------------------------------------------------------
L'idea è nata dalla volonta di voler conoscere un linguaggio funzionale ed
il suo funzionamento, applicando la programmazione per vincoli CLP.
Sono stato coinvolto con la proposta di sviluppare sostanzialmente un
risolutore di formule per il linguaggio {log}, basato su insiemi.
Il linguaggio L_BR (di {log}) è un linguaggio a vincoli che fornisce insiemi
estensionali finiti e relazioni binarie su operazioni base come entità
primitive del linguaggio.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 February/March -
------------------------------------------------------------------------------
- Some learnings -
------------------------------------------------------------------------------
Proof of concepts per picat, lettura manuali, documenti e raccolta
informazioni necessarie per procedere con il lavoro.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 mid-March -
------------------------------------------------------------------------------
- Utils and first setlog solver -
------------------------------------------------------------------------------
Aggiunte alcune funzioni di utilità in picat, abbozzata la prima struttura
del solver, risoluzione dei problemi comuni e apprendimento del funzionamento
di Picat.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 March-April -
------------------------------------------------------------------------------
- More on setlog solver -
------------------------------------------------------------------------------
Aggiunta una struttura più consistente per il risolutore setlog grazie al
file di prova in prolog del prof. Primi risultati.
Inizio risooluzioni dei primi problemi ed adeguamento del codice alle
necessità ed a Picat stesso.
Particolare difficoltà nella riproduzione delle funzioni dai predicati,
trasformati grazie all'uso del "fail" e della programmazione logica.
Trasformato il risolutore, ove possibile, in uno il più possibile imperativo
per facile comprensione altrui.
Aggiunte funzioni di utilità come logger, e trasformatore di predicati in
funzioni.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 11 April -
------------------------------------------------------------------------------
- Global variables and tmp file helper -
------------------------------------------------------------------------------
Aggiunto un helper per le variabili globali che scrive su get_global_map(),
possibilità:
- get_heap_map()
Created on the heap after the thread is created
Changes are undone when backtracking
- get_global_map()
Created in the global area when Picat is started
Changes are not undone when backtracking
- get_table_map()
Created in the table area when Picat is started
Keys and values are hash-consed
Changes are not undone when backtracking
fonte: http://picat-lang.org/download/picat_tutorial.pdf
Aggiunto un helper per file temporanei che dia la possibilità di leggere e
scrivere sullo stesso file senza trattare i nomi ed in modo semplice ed
efficace.
Questi helper serviranno per l'implementazione della conversione variabili
picat a variabili reali per quanto riguarda i nomi.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 13-14 April -
------------------------------------------------------------------------------
- First set, in and notin constraint tests -
------------------------------------------------------------------------------
Aggiunte le prime prove per l'implementazione di set e dei vincoli in e
notin nel solver. E' stato necessario implementare una funzione smember
per verificare l'esistenza di un elemento (anche variabile) nel set
sfruttando il nondeterminismo. Complicanze nell'utilizzo del nondeterminismo
"inline" con picat.
Note:
- implementazione naive in (ok)
- implementazione naive notin (ovvero, `not rule($in(...))`) non
funzionante.
Aggiunti modulo per l'interazione con utente (user input).
Project refactor (moved modules to setlog folder).
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 15 April -
------------------------------------------------------------------------------
- Picat problems -
------------------------------------------------------------------------------
Riscontrati una buona dose di problemi con picat:
(1) chiudere di seguito due stream read e write comporta il troncamenteo del
file (motivi ignoti);
(2) la read_term di picat quando incontra il $ trasforma la clausola in
qualcosa tipo _$_term_construct, e tenta di costruire una struct.
Questo non va per nulla bene nell'implementazione della traduzione
da "picat names a real names", che sbarella non appena prende uno di
questi e fallisce miseramente la traduzione.
**Soluzione**: non mi sembra una soluzione l'aggiunta di casi eccezionali
tipo
se: _$_term_construct allora non fare nulla
altrimenti: fai come solito
...;
(3) pattern matching è notevolmente problematico per il problemi di chiudere
al punto (2), obbliga a scrivere cose come [$eq(X,1)] da passare alla
rule(eq(X,Y)) ma sempre per la traduzione da "picat names a real
names" è un problema.
**Soluzione**: manipolazione di stringhe toglie tutti i dollari (MAH).
Fix and bugs setlog e mie implementazioni:
(1) modulo temp:
- chiusura file demandata all'utente.
Questa implementazione
X = tmp_w(Key), X.close()
Y = tmp_r(Key), Y.close()
causa il troncamento del file con conseguente perdita di informazione.
- eliminazione file possibile (a quanto pare) senza chiusura degli
stream.
(2) modulo read_term_sl:
- aggiunto ignore delle variabili duplicate e utilizzato il modulo
temp.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 17 April -
------------------------------------------------------------------------------
- Some fixes -
------------------------------------------------------------------------------
Fix del modulo read_term_sl
Update temp module: removed del files.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 29 April -
------------------------------------------------------------------------------
- A new setlog intepreter -
------------------------------------------------------------------------------
Nuova implementazione dell'interprete setlog sfruttando la potenza dei
predicati. Le regole di risoluzione sono state separate dall'interpretazione
della sintassi delle formule, ed offerte come delle api di programmazione.
Es: rule(eq(T1, T2), R) => eq(T1, T2, R).
in cui la rule richiama l'api per la risoluzione delle equality constraints.
Tentata la segmentazione delle regole di risoluzione, ma data la dipendenza
di alcune regole da altre regole è stato impossibile segmentare tutto.
Implementata la modifica dinamica della debug mode da variabili globali.
Implementazione di uno scheletro per il testing delle regole di inferenza.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 08 May -
------------------------------------------------------------------------------
- More on rewrite rules -
------------------------------------------------------------------------------
Incontro con il prof sull'interprete inviato ad inizio di maggio.
E' emerso che:
(1) il nondeterminismo del predicato solve è quello che probabilmente porta
l'interprete a chiedere più volte se si vuole un'altra soluzione o meno.
(2) bisogna verificare l'esistenza di un predicato functor fornito da Picat
per estrarre da una variabile il nome del funtore e la sua arità.
Questo può essere sfruttato per l'implementazione delle regole eq_6,
eq_9, neq_6, neq_7.
Dal manuale si evince che esitono dei predicati per estrarre nome ed arità
dalle struct.
(3) bisogna verificare come implementare l'or nelle regole del neq,
specialmente neq_7 e scegliere se implementarle tramite il nondeterminismo
della regola in se o se usare l'API or/2, nel caso bisognerebbe trovare un
modo per scrivere gli or annidati come
or(x_1, or(x2, or(..., xn)))
che sarebbero processati come
x_1 \/ x_2 \/ ... \/ x_n.
(4) potrebbe essere introdotto l'uso di variabili globali per verificare
che il constraint store sia stato modificato o meno e rendere più
efficiente la solve/2.
Inoltre, le globali potrebbero essere usate anche per mantenere i nomi
delle variabili lette da linea di comando.
Inoltre sono state discusse le regole di riscrittura per insiemi.
In particolare, nella eq_8
{x|A} = {y|B} -->
x = y /\ A = B (caso base)
x = y /\ {x|A} = B (verifica un caso particolare)
x = y /\ A = {y|B} (verifica un altro caso particolare)
A = {y|N} /\ {x|N} = B (**1)
**1: A è uguale all'insieme {y|N} (y resto N) e B è uguale a {x|N}, dove
è da notare che la N (resto) è la stessa in entrambi.
Le regole "duali" valgono per il neq.
Nota: per quanto riguarda la neq_4, si intende dire che *t* è un termine
composto, esempio una lista e quindi
X neq [X]
elimina il vincolo di neq perché è sempre vero
Non si applica nel caso di insiemi e non si applica nel caso di funtori
perché quella regola è dopo.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 13,14 May -
------------------------------------------------------------------------------
- Implementing some rewrite rules -
------------------------------------------------------------------------------
Implementate le regole eq_1, eq_6, eq_8, eq_9.
Implementate le regole neq_3, neq_4
Implementato l'or su lista.
Dai test è emerso che (vedere demos.txt) dall'interprete setlog possono
essere richiesti goal in cui tutto si scrive senza $ di struct.
Eesempio:
neq(f(1,2), g(1,2))
sia neq che esiste come predicate che f e g che invece non esistono possono
essere scritti senza $
neq($f(1,2), $g(1,2))
invece genera un errore in neq perchè controlla i nomi delle struct e
diventano _$_term_construct
Da linea di comando picat invece (NON SO PERCHÉ), neq($f(1,2), $g(1,2))
funziona, mentre `neq(f(1,2), g(1,2))` no. Nella seconda vorrebbe trovare
le funzioni f e g da eseguire, ma non esisono. La prima invece non so come
caspita possa funzionare!
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 21 May -
------------------------------------------------------------------------------
- Working on lset -
------------------------------------------------------------------------------
Aggiornato il readme.
Problemi con la gestione degli insiemi nella struttura dati stabilita:
set([...]).
Ho quindi implementato una sorta di classe lset per la gestione degli insiemi
che gestisca la creazione di nuove istanze, la testa ed il resto degli
insiemi. (Vedere lset.pi)
Riscrittura del modulo setlog con la nuova implementazione di set.
Nell'incontro con il prof di domani (22/05/2019) andranno definite:
- una sorta di roadmap;
- come proseguire con l'implementazione delle regole;
- come TESTARE ciò che faccio per capire se è corretto o meno (anche da use
cases della tesi di vetere per esempio);
- a quale obiettivo arrivare;
- dettagli logistici come
- come, dove e quando vederci;
- come e quando iniziare a scrivere la tesi, che struttura dare.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 22 May -
------------------------------------------------------------------------------
- Goal direction -
------------------------------------------------------------------------------
Dall'incotro sono emerse delle novità.
(1) i test case possono essere riassunti nei seguenti:
- {} // empty set
- X // var
- {X, Y} // closed set
- {X | R} // open set
da attribuire ad entrambe le parti delle relazioni binarie, generando almeno
16 casi.
(2) nall risluzione dei vincoli non bisogna essere greedy, i vincoli non vanno
risolti subito, fatta eccezione delle eq constraints. I neq non vanno
assolutamente risolti subito, i nuovi vincoli vanno inseriti nel constraint
e risolti al giro dopo.
(3) la rappresentazione insiemistica con lset va bene; da sperimentare.
(4) il goal ultimo è l'implementazione di clp(set)
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 23/24 May -
------------------------------------------------------------------------------
- It's time of CLI -
------------------------------------------------------------------------------
E' stata implementata una CLI degna di tale nome, che segua il principio di
"separation of concerns" tale per cui la CLI viene separata dal solver vero
e proprio.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 26 May -
------------------------------------------------------------------------------
- The end of eq/neq/in rules? -
------------------------------------------------------------------------------
Implmentazione di tutte le regole dell'equality constraints, seguendo paro
paro le regole di riscrittura (vari fix, soprattutto eq_7).
Tutte le neq sono state riscritte di modo che non siano risolte in maniera
greedy, ma siano solo riscritte e passate al solver per essere sistemate
alla passata successiva.
Riscritte le regole per "in" con la nuova impl. di lset.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 27 May -
------------------------------------------------------------------------------
- The union constraints -
------------------------------------------------------------------------------
Aggiornao il solver con alcuni commenti e minor fix.
Tentata la riscrittura delle variabili ma non funziona mettendo la mappa
nelle globali, mistero...
Aggiunte alcune union rules.
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 29 May -
------------------------------------------------------------------------------
- The "union" meeting -
------------------------------------------------------------------------------
Domande:
- come implemento il notin?
Vedere documento capitolo 7.
- nelle regole della union, {t u A}, t è un termine o è l'insieme dei
termini?
E' un singolo termine, la ricorsione va effettuata su tutti i termini!
E' emerso che mostrare i risultati "nice" si fa solo alla fine, non anche
durante la traccia parziale. Questo però potrebbe essere fatto rifacendo il
parsing della stringa e unificando quello che ho letto con le variabili
calcolate.
Provare ad introdurre delle regole "side" che permettano l'espansione del
solver sfruttando le altre regole.
Introdurre un "constraint not found" se la rule fallisce.
Altri appunti:
- l'inversione in neq `t != x --> x != t` va in ciclo se si specifica
solamente che t deve essere nonvar, perché se le gira e anche l'altro è
nonvar continua all'infinito.
Soluzione: nonvar(T1), var(T2)
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 30 May -
------------------------------------------------------------------------------
- Verification and check up -
------------------------------------------------------------------------------
Domande:
- cosa succede nella eq7 se l'insieme ha zero elementi e solo il resto?
Questo caso è intercettato da regole precedenti.
Vedere file test8.pi in setlog-temp, implementare tutto così.
Cambiare implementazione ad lset!!
------------------------------------------------------------------------------
------------------------------------------------------------------------------
- 2019 O2 June -
------------------------------------------------------------------------------
- New Lset implementation made it works!! -
------------------------------------------------------------------------------
Modificata la rappresentazione interna di lset con l'utilizzo delle liste
non chiuse: le eq constraints funzionano:
Esempio
- [eq([1,2,3|X],[4,5,6|X])]
Vars: (map)[X = [1,2,3,4,5,6|_171a0]]
Constraints: []
- [eq([1,X],[1,Y])]
Vars: (map)[Y = _7458,X = _7458]
Constraints: []