(module minisat-interface mzscheme
(require (prefix srfi13: (lib "13.ss" "srfi"))
(lib "file.ss")
(lib "port.ss")
(lib "process.ss"))
(provide minisat
minisat-path)
(define minisat-path (make-parameter (string->path "/home/pmatos/solvers/minisat2/minisat/core/minisat")))
(define (minisat file)
(let* ([current-time (current-inexact-milliseconds)]
[tmp-file (path->string (make-temporary-file))])
(printf "MiniSAT outputting to temp file ~a~n" tmp-file)
(let-values ([(stdout stdin pid stderr proc) (apply values (process*/ports (open-output-nowhere) (open-input-file "/dev/null") (open-output-nowhere)
(minisat-path) "-verbosity=0" file tmp-file))])
(proc 'wait)
(let* ([result (with-input-from-file tmp-file
(λ ()
(let ([status (string->symbol (srfi13:string-downcase (read-line)))])
(cons status
(if (eqv? status 'sat)
(map (λ (n) (string->number n)) (srfi13:string-tokenize (srfi13:string-drop-right (read-line) 1)))
#f)))))]
[final-time (current-inexact-milliseconds)])
(values (- final-time current-time) (car result) (cdr result))))))
)