diff options
Diffstat (limited to 'guile/sat/solver.scm')
-rw-r--r-- | guile/sat/solver.scm | 59 |
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 ...)))) |