blob: 24eb7b1e21e2fc1782e7b9c18599a79ef50ea2bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
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))))))
|
