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


(define last-variable (make-parameter 0))
(define sat-clauses (make-parameter '()))


(define (make-sat-variable)
  (last-variable (1+ (last-variable)))
  (last-variable))


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


(define (vline->integers line)
  (cdr
    (map string->number
         (string-split line #\space))))


(define (set-values! value-array values)
  (for-each
    (lambda (val)
      ;; If exactly zero, don't set anything
      (cond
        ((> val 0)
         (array-set! value-array #t val))
        ((< val 0)
         (array-set! value-array #f (- val)))))
    values))


(define* (solve-sat #:key (solver "kissat"))

  ;; Prepare CNF input
  (with-output-to-file
    "dimacs.cnf"
    (lambda ()
      (format #t "p cnf ~a ~a\n"
              (last-variable)
              (length (sat-clauses)))
      (for-each (lambda (clause)
                  (format #t "~{~d ~}0\n" clause))
                (sat-clauses))))

  ;; Run the solver and parse output
  (let ((values (make-array 'none (list 0 (last-variable)))))
    (let loop ((port (open-pipe* OPEN_READ solver "dimacs.cnf")))
      (let ((line (read-line port)))
        (unless (eof-object? line)
          (cond
            ((char=? (string-ref line 0) #\v)
             (set-values! values (vline->integers line)))
            ((string=? line "s UNSATISFIABLE")
             (error "Unsatsfiable!")))
          (loop port))))
    values))


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