Proper garbage collection of foreign objects using trivial-garbage.
[cl-satwrap.git] / dimacs.lisp
blob98f91dc9369170f6339073ac530d63f875606369
1 ;;; -*- Mode: Lisp; Syntax: ANSI-Common-Lisp; Base: 10; -*-
2 ;;;
3 ;;; dimacs.lisp --- DIMACS read/write procedures
5 ;; Copyright (C) 2010 Utz-Uwe Haus <lisp@uuhaus.de>
6 ;; $Id:$
7 ;; This code is free software; you can redistribute it and/or modify
8 ;; it under the terms of the version 3 of the GNU General
9 ;; Public License as published by the Free Software Foundation, as
10 ;; clarified by the prequel found in LICENSE.Lisp-GPL-Preface.
12 ;; This code is distributed in the hope that it will be useful, but
13 ;; without any warranty; without even the implied warranty of
14 ;; merchantability or fitness for a particular purpose. See the GNU
15 ;; Lesser General Public License for more details.
17 ;; Version 3 of the GNU General Public License is in the file
18 ;; LICENSE.GPL that was distributed with this file. If it is not
19 ;; present, you can access it from
20 ;; http://www.gnu.org/copyleft/gpl.txt (until superseded by a
21 ;; newer version) or write to the Free Software Foundation, Inc., 59
22 ;; Temple Place, Suite 330, Boston, MA 02111-1307 USA
24 ;; Commentary:
26 ;;
28 ;;; Code:
32 (in-package #:satwrap)
34 (defun split-delimited-string (string char)
35 "Return a list of the substrings of STRING that are separated by CHAR. Without CHAR."
36 (declare (type string string)
37 (type character char))
38 (let ((next-separator (position char string :test #'char=)))
39 (if next-separator
40 (cons (subseq string 0 next-separator)
41 (split-delimited-string (subseq string (1+ next-separator))
42 char))
43 `(,string))))
45 (defgeneric read-dimacs (solver source)
46 (:documentation "Read DIMACS-style sat problem from SOURCE into SOLVER.")
47 (:method ((solver sat-solver) (source pathname))
48 (with-open-file (f source :direction :input)
49 (loop :as line := (read-line f nil nil nil)
50 :as pieces := (split-delimited-string line #\Space)
51 :while line
52 :when (string= "p" (first pieces))
53 ;; format specification:
54 :do (destructuring-bind (p format m n)
55 pieces
56 (declare (ignore p))
57 (unless (string= "cnf" format)
58 (error "Dimacs file not in CNF format: ~A" line))
59 (setf (sat-solver-numvars solver) (parse-integer m))
60 (loop
61 :with clause := '()
62 :as var := (read f nil nil nil)
63 :while var
64 :if (= 0 var)
65 :do (progn
66 (add-clause solver (nreverse clause))
67 (setf clause '()))
68 :else
69 :collect (push var clause))
70 (unless (= (parse-integer n) (sat-solver-numclauses solver))
71 (error "Dimacs file ends prematurely: parsed ~D clauses, expected ~A"
72 (sat-solver-numclauses solver)
73 n)))))
74 (setf (sat-solver-clauses solver) (nreverse (sat-solver-clauses solver)))
75 solver))
77 (defun make-sat-solver-for-dimacs-instance (source)
78 (read-dimacs (make-instance 'sat-solver) source))