(define-module (sat solver)
  #:use-module (ice-9 popen)
  #:use-module (ice-9 rdelim)
  #:use-module (ice-9 format)
  #:export (solve-sat
             make-sat-variable
             add-clause))


(define last-variable (make-parameter #f))
(define sat-clauses (make-parameter #f))


(define (make-sat-variable)
  (unless (last-variable)
    (error "make-variable used outside solve-sat"))
  (last-variable (1+ (last-variable)))
  (last-variable))


(define (add-clause clause)
  (sat-clauses (cons clause (sat-clauses))))


(define (write-dimacs n-variables clauses)
  (with-output-to-file
    "dimacs.cnf"
    (lambda ()
      (format #t "p cnf ~a ~a\n"
              n-variables
              (length clauses))
      (for-each (lambda (clause)
                  (format #t "~{~d ~}0\n" clause))
                clauses)))
  (let loop ((port (open-pipe* OPEN_READ "kissat" "dimacs.cnf")))
    (let ((line (read-line port)))
      (unless (eof-object? line)
        (format #t "Line '~a'\n" line)
        (loop port)))))


(define-syntax solve-sat
  (syntax-rules ()
    ((_ body ...)
     (parameterize ((last-variable 0)
                    (sat-clauses '()))
       body ...
       (write-dimacs (last-variable)
                     (sat-clauses))))))