1 /* SWIG wrapper generation for minisat library
-*- lisp
-*- */
2 /* (c
) 2010 Utz-Uwe Haus
*/
4 %module
"satwrap.minisat"
6 %feature
("intern_function","1"); // use swig-lispify
7 %feature
("export"); // export wrapped things
10 ;;; Auto-generated
-*- lisp
-*- file
11 ;;; generated from $Id
:$
12 (eval-when
(:compile-toplevel
:load-toplevel
)
13 (declaim
(optimize
(speed
3) (debug
0) (safety
1))))
15 (cl
:defpackage
:satwrap.minisat
16 (:use
:cl
:cffi
:satwrap.backend
)
17 (:documentation
"Package containing minisat-backend")
18 ;; other exports done by swig
19 (:export #
:minisat-backend #
:satisiablep #
:solution #
:add-clause #
:numvars
))
20 (cl
:in-package
:satwrap.minisat
)
21 (eval-when
(:compile-toplevel
:load-toplevel
:execute
)
22 (cl
:defun swig-lispify
(name flag cl
:&optional (package (find-package :satwrap.minisat)))
23 (cl
:labels
((helper
(lst last rest cl
:&aux (c (cl:car lst)))
28 (helper
(cl
:cdr lst
) 'upper
30 ((lower digit
) (cl
:list
* c #\
- rest
))
31 (cl
:t
(cl
:cons c rest
)))))
33 (helper
(cl
:cdr lst
) 'lower
(cl
:cons
(cl
:char-upcase c
) rest
)))
35 (helper
(cl
:cdr lst
) 'digit
37 ((upper lower
) (cl
:list
* c #\
- rest
))
38 (cl
:t
(cl
:cons c rest
)))))
39 ((cl
:char-equal c #\_
)
40 (helper
(cl
:cdr lst
) '_
(cl
:cons #\
- rest
)))
41 ((cl
:char-equal c #\
-)
42 (helper
(cl
:cdr lst
) '
- (cl
:cons #\
- rest
)))
44 (cl
:error
"Invalid character: ~A" c
)))))
45 (cl
:let
((fix
(cl
:case flag
46 ((constant enumvalue
) "+")
53 (cl
:nreverse
(helper
(cl
:concatenate 'cl
:list name
) cl
:nil cl
:nil
))
59 %insert
("swiglisp") %{
64 %insert
("swiglisp") %{
65 ;; foreign type definitions to hide pointer values
66 (defclass wrapped-pointer
()
67 ((ptrval
:reader get-ptrval
:initarg
:ptrval
)
68 (ctype
:reader get-ctype
:initarg
:ctype
))
69 (:documentation
"A wrapped pointer"))
71 (defmethod print-object
((p wrapped-pointer
) stream
)
72 (print-unreadable-object
(p stream
:type nil
:identity nil
)
73 (format stream
"wrapper around `~A' @0x~16R" (get-ctype p
) (get-ptrval p
))))
75 (define-condition foreign-null-pointer-condition
(error
)
77 :reader foreign-null-pointer-condition-type
))
78 (:report
(lambda
(condition stream
)
79 (format stream
"The foreign pointer of type ~A was NULL"
80 (foreign-null-pointer-condition-type condition
)))))
84 %define TYPEMAP_WRAPPED_POINTER
(PTRTYPE
,LISPCLASS
)
86 %insert
("swiglisp") %{
87 (define-foreign-type LISPCLASS
()
89 (:actual-type
:pointer
)
90 (:documentation
"cffi wrapper type around PTRTYPE."))
92 (define-parse-method LISPCLASS
()
93 (make-instance 'LISPCLASS
))
95 (defmethod translate-from-foreign
(value
(type LISPCLASS
))
96 "Wrap PTRTYPE, signaling a null-pointer-exception if value is NULL."
97 (if
(cffi
:null-pointer-p value
)
98 (error 'foreign-null-pointer-condition
:type type
)
99 (make-instance 'wrapped-pointer
:ptrval value
:ctype
"PTRTYPE")))
101 (defmethod translate-to-foreign
((g wrapped-pointer
) (type LISPCLASS
))
106 %typemap
(cin
) PTRTYPE
"LISPCLASS"
107 %typemap
(cout
) PTRTYPE
"LISPCLASS"
110 TYPEMAP_WRAPPED_POINTER
(struct minisat_solver
*, minisat-solver
)
112 %typemap
(cin
) struct minisat_solver
* "minisat-solver"
113 %typemap
(cout
) struct minisat_solver
* "minisat-solver"
115 /* Now parse and wrap the API header
*/
116 %insert
("swiglisp") %{
117 (eval-when
(:compile-toplevel
:load-toplevel
)
118 ;; Muffle compiler-notes globally
119 #
+sbcl
(declaim
(sb-ext
:muffle-conditions sb-ext
:defconstant-uneql
))
123 %include
"minisat_wrap.h"
124 %insert
("swiglisp") %{
126 ;; implementation of a satwrap backend using minisat
:
127 (defclass minisat-backend
(satwrap-backend
)
128 ((solver
:initarg
:solver
:accessor minisat-backend-solver
)
129 (solved
:initform NIL
:accessor minisat-backend-solvedp
))
131 (:default-initargs
:name
"MiniSAT" :version
"2-070721"
132 :solver
(alloc-minisat-solver
))
133 (:documentation
"MiniSAT solver backend"))
134 ) ;; end of eval-when to avoid top-level export
136 (defmethod initialize-instance
:after
((instance minisat-backend
) &rest initargs)
137 (let
((solver
(minisat-backend-solver instance
)))
138 (tg
:finalize instance #'
(lambda
()
139 ;; (format T
"Finalizing ~X." solver
)
140 (free-minisat-solver solver
)))))
142 ;; (defmethod reinitialize-instance
((instance minisat-backend
) &rest initargs &key &allow-other-keys)
143 ;; (apply #'call-next-method initargs
))
147 (defmethod
(setf numvars
) ((numvars fixnum
) (backend minisat-backend
)) ;; arguments reversed for setf methods...
148 (minisat-set-numvars
(minisat-backend-solver backend
) numvars
))
150 (defmethod add-clause
((backend minisat-backend
) (clause list
))
151 (assert
(not
(member
0 clause
:test #'
=)))
153 (loop
:with solver
:= (minisat-backend-solver backend
)
154 :for v
:of-type fixnum
:in clause
155 :do
(minisat-add-var-to-clause solver v
)
157 (minisat-add-var-to-clause solver
0)
158 (setf
(minisat-backend-solvedp backend
) NIL
))))
160 (defmacro with-assumptions
((solver assumptions
) &body body)
161 (let
((i
(gensym
"i"))
162 (s
(gensym
"solver"))
163 (a
(gensym
"assumptions")))
168 (minisat-clear-assumptions
,s
)
170 (list
(dolist
(,i
,a
)
171 (minisat-add-assumption
,s
,i
)))
172 (vector
(loop
:for
,i
:across
,a
173 :do
(minisat-add-assumption
,s
,i
))))
175 (minisat-clear-assumptions
,s
)))))
177 (defmethod satisfiablep
((backend minisat-backend
) (assumptions sequence
))
178 (ecase
(let
((be
(minisat-backend-solver backend
)))
179 (with-assumptions
(be assumptions
)
182 (setf
(minisat-backend-solvedp backend
) T
)
184 (:+MINISAT-UNSAT
+ NIL
)))
186 (defmethod solution
((backend minisat-backend
) (interesting-vars list
))
187 (if
(not
(minisat-backend-solvedp backend
))
188 (error
"Problem still unsolved or UNSAT")
189 (loop
:with be
:= (minisat-backend-solver backend
)
190 :for i
:of-type fixnum
:in interesting-vars
191 :collect
(minisat-sol-val be i
))))
193 (defmethod synchronize-backend
((backend minisat-backend
)
196 (deleted-clauses
(eql '
()))
198 "Adding clauses is easy with minisat."
199 (declare
(ignore numvars
))
200 (dolist
(c new-clauses
)
201 (add-clause backend c
)))