1 files changed, 42 insertions, 17 deletions
diff --git a/guile/sat/solver.scm b/guile/sat/solver.scm
index 24eb7b1..f633c31 100644
--- a/guile/sat/solver.scm
+++ b/guile/sat/solver.scm
@@ -3,17 +3,16 @@
   #: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 #f))
-(define sat-clauses (make-parameter #f))
+(define last-variable (make-parameter 0))
+(define sat-clauses (make-parameter '()))
 
 
 (define (make-sat-variable)
-  (unless (last-variable)
-    (error "make-variable used outside solve-sat"))
   (last-variable (1+ (last-variable)))
   (last-variable))
 
@@ -22,28 +21,54 @@
   (sat-clauses (cons clause (sat-clauses))))
 
 
-(define (write-dimacs n-variables 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"
-              n-variables
-              (length clauses))
+              (last-variable)
+              (length (sat-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)))))
+                (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 solve-sat
+(define-syntax sat-context
   (syntax-rules ()
     ((_ body ...)
      (parameterize ((last-variable 0)
                     (sat-clauses '()))
-       body ...
-       (write-dimacs (last-variable)
-                     (sat-clauses))))))
+       body ...))))