(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")))
(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))))
)