(module yices-interface mzscheme 
  
  (require (prefix srfi13: (lib "13.ss" "srfi"))
           "proc-utils.scm")
  
  (provide yices
           yices-path)
  
  (define yices-path (make-parameter (string->path "/home/pmatos/solvers/yices-1.0.9/bin/yices")))
  
  ;; 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 (yices file)
    (let* ([current-time (current-inexact-milliseconds)]
           [subprocess-result (with-input-from-subprocess 
                               (λ ()
                                 (let ([status (string->symbol (read-line))])
                                   (cons status
                                         (if (eqv? status 'sat)
                                             (map (λ (n) (string->number n)) (srfi13:string-tokenize (read-line)))
                                             #f))))
                               (yices-path) "-d" "-e" file)]
           [final-time (current-inexact-milliseconds)])
      (values (- final-time current-time) (car subprocess-result) (cdr subprocess-result))))
                  
  )