Fork me on GitHub
#clojure-italy
<
2019-04-29
>
manuel07:04:45

buon lunedì, gente :rain_cloud:

reborg09:04:36

gionno ☀️

reborg09:04:55

Allora @bronsa te lo sei scordato del tutto Clojure e ci bazzichi ancora? :)

bronsa09:04:23

ancora qualcosina me lo ricordo ;) a breve inizio a scrivere tools.sat

reborg09:04:13

wat? cos’e’ sat?

bronsa09:04:27

sat solver

reborg09:04:07

oh oh, stiamo facendo la stesse cose… io sono in FOL ed SMT solving

bronsa09:04:34

SMT e` un po' piu` complicato da scrivere, vediamo come va

nilrecurring10:04:46

Interessante, sto lavorando anche io a roba SAT e CDCL 😄

reborg10:04:38

comunque, dopo un po’ di transformazioni per approssimare FOL a proprositional logic, arriva ad usare gli stessi algoritmi

bronsa10:04:09

eh non proprio

bronsa10:04:32

cioe`, puoi pensarla cosi`

bronsa10:04:38

ma i SMT solver moderni non funzionano cosi`

reborg10:04:43

ci sono quintalate di teoria e di libri, tutto e’ possibile, dipende, etc.

bronsa10:04:38

e` una buona visione dall'altissimo di come funziona il loop in un SMT solver

reborg10:04:32

Clojure (perche’ e’ lispy) e’ fantastico per lavorare simbolicamente su queste cose

reborg10:04:07

Comunque non vedo l’ora di usare il tuo tool.sat

bronsa10:04:40

mah non aspettarti chissache`, e` piu` per imparare a scrivere un CDCL solver che per altro

bronsa10:04:20

mi aspetto sara` da 2 a 3 ordini di grandezza piu` lento di comuni SAT solver

reborg10:04:31

Hai bisogno di trasformare la logica prima di partire con CDCL?

bronsa10:04:58

no, CDCL e` puramente SAT

reborg10:04:02

chiedevo perche’ DPLL prevede CNF e vedevo l’ispirazione viene da li

bronsa10:04:37

ah, trasformare in quel senso, si`, essendo CDCL un'"estensione" di DPLL, lavora in CNF anche lui

bronsa10:04:28

penso sia standard su qualsiasi tecnica di SAT solving lavorare su una formula CNF

reborg10:04:08

qui al lavoro sono piu’ interessato alle transformazioni che altro, ed abbiamo obiettivi diversi da smt solving o ATP. Quindi parto da basi simili poi divergo.

bronsa10:04:02

trasformazioni in che senso?

reborg10:04:09

trasformazioni della logica in input in modo che risponda a certi requisiti (forme normali che non sono CNF ma altro)

reborg10:04:57

@nilrecurring anche tu per lavoro o per diletto?

bronsa10:04:28

io per diletto questo comunque, non mi serve per lavoro

nilrecurring10:04:05

Diletto anche per me 🙂

reborg10:04:18

sono il privilegiato allora :)

reborg10:04:37

(dipende dai punti di vista)

😄 4
Andrea Imparato11:04:49

domandina del lunedì: E’ possibile secondo voi riscrivere questa funzione usando recur anzichè la chiamata ricorsiva:

(defn walk [s sea-level valleys]
    (if (seq s)
        (let [step (first s)
              new-sea-level (+ step sea-level)]
            (if (and (= new-sea-level 0) (= step 1))
                (walk (rest s) new-sea-level (inc valleys))
                (walk (rest s) new-sea-level valleys)))
        valleys))

reborg11:04:13

Parrebbe di si’:

(defn walk [s sea-level valleys]
    (if (seq s)
        (let [step (first s)
              new-sea-level (+ step sea-level)]
            (if (and (= new-sea-level 0) (= step 1))
                (recur (rest s) new-sea-level (inc valleys))
                (recur (rest s) new-sea-level valleys)))
        valleys))

Andrea Imparato11:04:34

hmm recur non deve essere sempre l’ “ultima istruzione”? :thinking_face:

reborg11:04:22

Lo e’ :) non ti far confondere dagli if. Quello che importa e’ che se si arriva ad un recur, in quel momento nel codice, non c’e’ altra istruzione da eseguire nello stack corrente dopo il salto ricorsivo. Il risultato di recur puo’ essere “sostituito” nell stack corrente con il valore ritornato.

Andrea Imparato11:04:17

ok ok e come la mettiamo con il return di valleys alla fine? non è un’istruzione che viene dopo il recur?

reborg11:04:59

sintatticamente si’, ma logicamente no. Per arrivare a ritornare “valleys” nello stack corrente, non devi passare per un recur

reborg11:04:10

fortunatamente, recur ti dice se sei in tail-call o no. Quindi la cosa piu’ semplice a volte e’ metterlo e vedere se tira un’eccezione

Andrea Imparato11:04:46

sìsì è che ero così convinto di non poterlo usare che non ci avevo neanche provato 😄

reborg12:04:58

dubbio valido, specialmente con “walk” vari a volte non si puo’ andare di recur