1 files changed, 49 insertions, 0 deletions
diff --git a/guile/sat/solver.scm b/guile/sat/solver.scm
new file mode 100644
index 0000000..24eb7b1
--- /dev/null
+++ b/guile/sat/solver.scm
@@ -0,0 +1,49 @@
+(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))))))