Thursday, February 28, 2008

A SAT prover in 50 lines of Arc

Here is a very naïve implementation of a purely functional SAT prover written in Arc. Deals with unit clauses and can read CNF files.



(def rem-members (source lst) ; source - lst
(rem [mem _ lst] source))

(def has-members (source lst) ; inter (source, lst) != nil
(some [mem _ lst] source))

(def simplify (clauses (o model))
(withs
(anti-model (map - model)
not-t-clauses (keep [~has-members _ model] clauses)
simpl (map [rem-members _ anti-model] not-t-clauses))
(if (some nil simpl) ; At least one empty clause : UNSAT
'UNSAT
(aif (keep [is (len _) 1] simpl) ; if there are unit clauses...
(simplify (rem (car it) simpl) ; Remove the first one
(cons (caar it) model)) ; And unify its literal
(cons simpl model)))))

(def free-var (model) ; Chooses a non-unified var.
(with
(_abs (map abs model)
i 1)
(while (mem i _abs) (++ i))
i))

(def solve (clauses (o model))
(let simpl (simplify clauses model)
(if (is 'UNSAT simpl)
'UNSAT
(with
(c (car simpl)
m (cdr simpl))
(if (no c) ; We have no more clause : SAT
m
(withs
(var (free-var m)
unif-true (solve c (cons var m)))
(if (isnt unif-true 'UNSAT)
unif-true
(solve c (cons (- var) m)))))))))

(def read-pb (filename)
(let clauses '()
(w/infile f filename
(readline f) ; ignore first line
(whilet line (readline f)
(let lits (tokens line)
(if (and lits (~mem "c" lits)) ; Ignore empty lines and comments
(push (rem 0 (map [coerce _ 'int] lits)) clauses)))))
clauses))


Enjoy !

Thursday, February 14, 2008

Browse and recover files from a remote server

I needed a web app for people at my work to be able to browse and recover what they saved on a dedicated server when they break their own data. It needed a login/password system and the ability to compress and transfer files (that was the hard part). It had to use Apache at least as a proxy so as to enable SSL encryption. Something rather simple, but with a few tricky points.

Here is the code :


(= admin-ip* "XXX.XXX.XXX.XXX" ; The admin's machine IP address
apache-ip* "127.0.0.1" ; if used through Apache, that's the IP
rootdir* "/tmp/arc/"
threadlife* 300 ; threadlife extended for large archives
(ext-mimetypes* "tgz") "x-gzip")

; shortcut for "Run the following command and return the result in a string"
(= sys tostring:system:string)

; Shortcut for "Run sys function and return result as a list of strings, one per line"
(mac sys-lines args
`(tokens (sys ,@args) #\newline))


(def to-kill (filename) ; Removes a file after a period of time, depending on its size
(let duration (+ 600 (/ file-size.filename 102400)) ; Sleep 10mn, then 1s/100kb
(thread sleep.duration rmfile.filename)))


(def get-archive (path) ; Generate an archive from a given path
(withs (tgz (string (uniq) "-" (rand 100000) ".tgz") ; unique ID
http-tgz (string "/" tgz)
full-tgz (string rootdir* tgz))
(pr "Please wait... ")
(system:string "ssh -n xxx@xxx tar -zcf " full-tgz " '" path "'") ; Zip on file server
(pr "Almost finished... ")
(system:string "scp xxx@xxx:" full-tgz " " full-tgz) ; Transfer to the web server
(thread:system:string "ssh -n xxx@xxx rm " full-tgz) ; Remove zip from file server
(prs "Archive created : " (+ 1 (trunc (/ file-size.full-tgz 1024.0))) " kb ")
(link "[download]" http-tgz)
(to-kill full-tgz))) ; Just leave it available for a few minutes


(def show-dir (user path) ; Show a directory's content
(tag (p)
(prs "You are connected as " user " ")
(link "[logout]" "/logout"))
(tag (h3) (pr path))
(w/link (get-archive path) (pr "Recover that directory's content"))

(with (dirs (sys-lines "ssh -n xxx@xxx /usr/sbin/ls-dirs.pl dirs '" path "'")
files (sys-lines "ssh -n xxx@xxx /usr/sbin/ls-dirs.pl files '" path "'"))

(tag (h3) (pr "Directories"))
(tag (ul)
(map [tag (li) (w/link (show-dir user (string path "/" _)) (pr _))] dirs))

(tag (h3) (pr "Files"))
(tag (ul)
(map [tag (li) (w/link (get-archive:string path "/" _) (pr _))] files))))


; Secured defop : if not accessed through a given IP, deny access
(mac defsop (nom req ip . body)
`(defop ,nom ,req
(if (is (,req 'ip) ,ip)
(do ,@body)
(pr "Permission denied"))))


(defsop admin req admin-ip*
(login-page 'both "add a user..."
(fn (user ip) (whitepage (link "one more" "/admin")))))


(defsop voir req apache-ip*
(aif (get-user req)
(show-dir it (string "/home/" it))
(login-page 'login "Login, please..." login-ok)))


(def login-ok (user ip)
(whitepage
(prs "Welcome " user ", click ")
(link "here" "/voir")
(prs " to go on")))


(thread (asv))


There are a few thing to note.

First, I needed SSL encryption, which is not provided by the Arc server. So I use Apache as a proxy : users connect to https://mysite.fr which is an encrypted proxy to http://mysite.fr:8080. If users try to connect directly to the latter, they have a "permission denied denied message". It is done via the defsop macro : it is a secured defop which first checks that you are running it from a given IP. If you are coming from the proxy, your IP is 127.0.0.1. Else, you cannot go on.

Then, on the current version of the app, the web server is not on the same machine as the file server. So I use ssh a lot to list files and directories and to compress them. The code would be simpler if files were stored on the same machine.

Finally, once archives are created, they are available only for a limited amount of time, then they are deleted. A thread is in charge of that (on per archive). Not removing archives would rapidly fill the available space.

Feel free to use / criticize / ask questions about that code !

My Arc stuff

Hi, this weblog is about things I write with the Arc language. Some of them are tools I use at work.