(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")))
  
  ;; Given the path to the cnf file calls yices
  ;; and returns three values, the time taken, a symbol 'sat or 'unsat
  ;; and #f if 'unsat or a list of literals if 'sat
  (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))))))
                  
  )