1 /* swig interface wrapper file for cffi binding generation
-*- lisp
-*- */
2 /* swig
-cffi interface for CUDD
*/
3 /* (c
) 2009 Utz-Uwe Haus
*/
7 %feature
("intern_function","1"); // use swig-lispify
8 %feature
("export"); // export wrapped things
11 ;;; Auto-generated
-*- lisp
-*- file
12 ;;; generated from $Id
:$
13 (eval-when
(:compile-toplevel
:load-toplevel
)
14 (declaim
(optimize
(speed
3) (debug
0) (safety
1))))
16 (cl
:defpackage
:swig-macros
18 (:documentation
"Package containing utility functions for SWIG cffi interface generation")
19 (:export #
:swig-lispify #
:defanonenum
))
21 (cl
:in-package
:swig-macros
)
23 (cl
:defun swig-lispify
(name flag cl
:&optional (package (find-package :cuddapi)))
24 (cl
:labels
((helper
(lst last rest cl
:&aux (c (cl:car lst)))
29 (helper
(cl
:cdr lst
) 'upper
31 ((lower digit
) (cl
:list
* c #\
- rest
))
32 (cl
:t
(cl
:cons c rest
)))))
34 (helper
(cl
:cdr lst
) 'lower
(cl
:cons
(cl
:char-upcase c
) rest
)))
36 (helper
(cl
:cdr lst
) 'digit
38 ((upper lower
) (cl
:list
* c #\
- rest
))
39 (cl
:t
(cl
:cons c rest
)))))
40 ((cl
:char-equal c #\_
)
41 (helper
(cl
:cdr lst
) '_
(cl
:cons #\
- rest
)))
42 ((cl
:char-equal c #\
-)
43 (helper
(cl
:cdr lst
) '
- (cl
:cons #\
- rest
)))
45 (cl
:error
"Invalid character: ~A" c
)))))
46 (cl
:let
((fix
(cl
:case flag
47 ((constant enumvalue
) "+")
54 (cl
:nreverse
(helper
(cl
:concatenate 'cl
:list name
) cl
:nil cl
:nil
))
63 /* includes that SWIG needs to see to parse the cudd.h file go here
*/
67 %insert
("swiglisp") %{
69 (cl
:defpackage #
:cuddapi
70 (:use
:cl
:cffi
:swig-macros
)
71 (:export #
:cudd-manager #
:cudd-node
)
72 ;; other exports done by swig
74 (cl
:in-package
:cuddapi
)
76 %insert
("swiglisp") %{
77 ;; foreign type definitions to hide pointer values
78 (defclass wrapped-pointer
()
79 ((ptrval
:reader get-ptrval
:initarg
:ptrval
)
80 (ctype
:reader get-ctype
:initarg
:ctype
))
81 (:documentation
"A wrapped pointer"))
83 (defmethod print-object
((p wrapped-pointer
) stream
)
84 (print-unreadable-object
(p stream
:type nil
:identity nil
)
85 (format stream
"wrapper around `~A' @0x~16R" (get-ctype p
) (get-ptrval p
))))
87 (define-condition foreign-null-pointer-condition
(error
)
89 :reader foreign-null-pointer-condition-type
))
90 (:report
(lambda
(condition stream
)
91 (format stream
"The foreign pointer of type ~A was NULL"
92 (foreign-null-pointer-condition-type condition
)))))
96 %define TYPEMAP_WRAPPED_POINTER
(PTRTYPE
,LISPCLASS
)
98 %insert
("swiglisp") %{
99 (define-foreign-type LISPCLASS
()
101 (:actual-type
:pointer
)
102 (:documentation
"cffi wrapper type around PTRTYPE."))
104 (define-parse-method LISPCLASS
()
105 (make-instance 'LISPCLASS
))
107 (defmethod translate-from-foreign
(value
(type LISPCLASS
))
108 "Wrap PTRTYPE, signaling a null-pointer-exception if value is NULL."
109 (if
(cffi
:null-pointer-p value
)
110 (error 'foreign-null-pointer-condition
:type type
)
111 (make-instance 'wrapped-pointer
:ptrval value
:ctype
"PTRTYPE")))
113 (defmethod translate-to-foreign
((g wrapped-pointer
) (type LISPCLASS
))
118 %typemap
(cin
) PTRTYPE
"LISPCLASS"
119 %typemap
(cout
) PTRTYPE
"LISPCLASS"
122 TYPEMAP_WRAPPED_POINTER
(DdManager
*, cudd-manager
)
123 TYPEMAP_WRAPPED_POINTER
(DdNode
*, cudd-node
)
125 %typemap
(cin
) DdManager
* "cudd-manager"
126 %typemap
(cout
) DdManager
* "cudd-manager"
127 %typemap
(cin
) DdNode
* "cudd-node"
128 %typemap
(cout
) DdNode
* "cudd-node"
130 /* Now parse and wrap the API header
*/
131 %insert
("swiglisp") %{
132 (eval-when
(:compile-toplevel
:load-toplevel
)
133 ;; Muffle compiler-notes globally
134 #
+sbcl
(declaim
(sb-ext
:muffle-conditions sb-ext
:defconstant-uneql
))
138 %include
"cudd/cudd.h"
139 %insert
("swiglisp") %{
140 ) ;; end of eval-when to avoid top-level export
143 %insert
("swiglisp") %{
144 ;; (defmethod translate-from-foreign
:around
(manager
(type cudd-manager
))
145 ;; (let
((cudd-manager
(call-next-method
)))
147 ;; (trivial-garbage
:finalize cudd-manager #'
(lambda
()
148 ;; ;; (break
"finalize manager #x~x~%" manager
)
149 ;; ;; (format T
"kill mgmr ~A~%" manager
) (force-output
)
153 ;; (format T
"~D nodes unfreed in manager ~A" (cuddapi
:cudd-check-zero-ref manager
) manager
)
154 ;; ;; (cuddapi
:cudd-quit manager
)
155 ;; ;; (format T
"killed mgmr ~A~%" manager
) (force-output
)
160 %insert
("swiglisp") %{
161 ;; (defmethod translate-from-foreign
:around
(node
(type cudd-node
))
162 ;; (let
((cudd-node
(call-next-method
)))
164 ;; (trivial-garbage
:finalize cudd-node #'
(lambda
()
165 ;; ;; (format T
"finalize node #x~x~%" node
)
166 ;; ;; (format T
"kill node ~A" node
) (force-output
)
168 ;; ;; (format T
"~&killed ~A~%" node
)
169 ;; ;; (format T
"killed node ~A~%" node
) (force-output
)
177 %insert
("swiglisp") %{
178 ;;; Higher-level interface similar to de.uuhaus.bdd
180 (:use #
:cuddapi #
:cl
)
181 (:export #
:bdd-environment
)
182 (:export #
:with-bdd-environment #
:make-bdd-environment
)
183 ; (:export #
:make-bdd
)
184 (:export #
:bdd-true #
:bdd-false
)
185 (:export #
:bdd-new-variable
)
186 (:export #
:bdd-and #
:bdd-or #
:bdd-not #
:bdd-xor #
:bdd-nand #
:bdd-nor
187 #
:bdd-and-not #
:bdd-or-not #
:bdd-implies
188 #
:bdd-iff #
:bdd-restrict
)
189 (:export #
:bdd-exists #
:bdd-forall
)
190 (:export #
:bdd-tautologyp #
:bdd-satisfiablep
)
191 (:export #
:bdd-var-min #
:bdd-var-max
)
192 (:export #
:bdd-var-fixed0 #
:bdd-var-fixed0
)
193 (:export #
:deserialize-bdd
))
195 (cl
:in-package
:cudd
)
198 ;; for garbage collection purposes we wrap a reference to the manager with each
200 (defvar
*bdd-env
* nil
201 "A special variable holding the current BDD Environment.")
203 (deftype wrapped-bdd
()
206 (defmacro wrap-bdd
(bdd env
)
207 "Build a lisp object object around the cudd-node v."
209 (make-array
2 :adjustable NIL
:fill-pointer NIL
214 (defmacro unwrap-bdd
(bdd
)
215 "Extract the cudd-node object from bdd."
216 `
(svref
(the wrapped-bdd
,bdd
) 0)
220 (defun make-cudd-manager
(&key
222 (initial-num-slots
256) ;; #.
(cuddapi
:CUDD-UNIQUE-SLOTS
)
223 (cache-size
262144) ;; #.
(cuddapi
:CUDD-CACHE-SLOTS
)
225 (cuddapi
:cudd-init initial-num-vars
231 (defstruct
(bdd-environment
(:constructor construct-bdd-environment
))
232 "A wrapper object describing a CUDD-based BDD environment."
234 (name
"" :type string
)
235 ;; caching of the T and F objects of this manager to save FF overhead
238 ;; mapping VARs to foreign IDs
239 (var-
>id
(make-hash-table
:test #'eq
) :type hash-table
)
240 (nextvar
0 :type
(integer
0 #.
(expt
2 (* 8 (- (cffi
:foreign-type-size
:int
) 1))))))
242 (defmethod print-object
((e bdd-environment
) stream
)
243 (print-unreadable-object
(e stream
:type T
)
244 (format stream
"~A (manager @#x~X, ~D vars)"
245 (bdd-environment-name e
)
246 (cuddapi
::get-ptrval
(bdd-environment-manager e
))
247 (bdd-environment-nextvar e
))))
249 (defun make-bdd-environment
(&key
250 (manager
(make-cudd-manager
))
251 (name
(format nil
"BDD Environment ~A" (gensym
"BDDE"))))
252 (let
((res
(construct-bdd-environment
:manager manager
:name name
)))
253 (setf
(bdd-environment-true res
)
254 (wrap-bdd
(cuddapi
:cudd-read-one manager
) res
))
255 (setf
(bdd-environment-false res
)
256 (wrap-bdd
(cuddapi
:cudd-read-logic-zero manager
) res
))
257 ;; these need no finalization
:
258 (trivial-garbage
:cancel-finalization
(unwrap-bdd
(bdd-environment-false res
)))
259 (trivial-garbage
:cancel-finalization
(unwrap-bdd
(bdd-environment-true res
)))
262 (let
((vartab
(bdd-environment-var-
>id res
)))
263 (trivial-garbage
:finalize res
265 (format T
"~&killing ~D vars in ~A~%"
266 (hash-table-size vartab
)
268 (maphash #'
(lambda
(key val
)
269 (declare
(ignore val
))
270 (cuddapi
:cudd-recursive-deref
276 (eval-when
(:load-toplevel
)
277 (setf
*bdd-env
* (or
*bdd-env
*
278 (make-bdd-environment
:name
"The global BDD Environment."))))
280 (defmacro with-bdd-environment
(env
&body body)
281 "Execute BODY within the bdd environment ENV."
282 `
(let
((*bdd-env
* ,env
))
285 ;;; utility functions for the environment
286 (defun var-
>id
(var
&optional (env *bdd-env*))
287 "Return the ID for VAR in ENV (which defaults to *bdd-env*)."
288 (gethash var
(bdd-environment-var-
>id env
)))
290 (defsetf var-
>id
(var
&optional (env *bdd-env*)) (id)
291 `
(setf
(gethash
,var
(bdd-environment-var-
>id
,env
)) ,id
))
293 (defun id-
>var
(id
&optional (env *bdd-env*))
294 "Return the VAR for ID in ENV (which defaults to *bdd-env*)."
295 (wrap-bdd
(cuddapi
:cudd-bdd-ith-var
(bdd-environment-manager env
) id
) env
))
299 (bdd-environment-true
*bdd-env
*))
302 (bdd-environment-false
*bdd-env
*))
304 (defun bdd-new-variable
()
307 (cuddapi
:cudd-bdd-new-var
(bdd-environment-manager
*bdd-env
*))
309 (id
(bdd-environment-nextvar
*bdd-env
*)))
311 (incf
(bdd-environment-nextvar
*bdd-env
*))
312 (setf
(var-
>id v
*bdd-env
*) id
)
314 (cuddapi
::foreign-null-pointer-condition
(c
)
316 ;; FIXME
: maybe try a garbage collection here
317 (error
"CUDD failed to allocate a variable ~D:~%BDD environment ~A full."
318 (bdd-environment-nextvar
*bdd-env
*)
321 (defun bdd-restrict
(var val bdd
)
323 (cuddapi
:cudd-bdd-restrict
(bdd-environment-manager
*bdd-env
*)
325 (unwrap-bdd
(if val var
(bdd-not var
))))
330 (cuddapi
:cudd-bdd-and
(bdd-environment-manager
*bdd-env
*)
331 (unwrap-bdd x
) (unwrap-bdd y
))
336 (cuddapi
:cudd-bdd-or
(bdd-environment-manager
*bdd-env
*)
337 (unwrap-bdd x
) (unwrap-bdd y
))
341 ;; FIXME
: cudd-not is a macro and hence not swig'ed
, but would probably
344 (cuddapi
:cudd-bdd-nand
(bdd-environment-manager
*bdd-env
*)
351 (cuddapi
:cudd-bdd-xor
(bdd-environment-manager
*bdd-env
*)
356 (defun bdd-nand
(x y
)
358 (cuddapi
:cudd-bdd-nand
(bdd-environment-manager
*bdd-env
*)
365 (cuddapi
:cudd-bdd-nor
(bdd-environment-manager
*bdd-env
*)
370 (defun bdd-and-not
(bdd1 bdd2
)
371 (bdd-and bdd1
(bdd-not bdd2
)))
373 (defun bdd-or-not
(bdd1 bdd2
)
374 (bdd-or bdd1
(bdd-not bdd2
)))
376 (defun bdd-implies
(bdd1 bdd2
)
377 (bdd-or-not bdd1 bdd2
))
379 (defun bdd-iff
(bdd1 bdd2
)
380 (bdd-and
(bdd-implies bdd1 bdd2
)
381 (bdd-implies bdd2 bdd1
)))
383 (defun bdd-equal
(bdd1 bdd2
)
384 "Check whether BDD1 and BDD2 are equal."
385 (let
((b1
(unwrap-bdd bdd1
))
386 (b2
(unwrap-bdd bdd2
)))
387 (and
(= 1 (cuddapi
:cudd-bdd-leq
(bdd-environment-manager
*bdd-env
*) b1 b2
))
388 (= 1 (cuddapi
:cudd-bdd-leq
(bdd-environment-manager
*bdd-env
*) b2 b1
)))))
390 (defun bdd-tautologyp
(bdd
&optional (fixings '()))
391 "Check whether BDD is tautologic, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
393 (bdd-tautologyp
(bdd-restrict
(caar fixings
) (cadr fixings
) bdd
)
395 (bdd-equal bdd
(bdd-true
))))
397 (defun bdd-satisfiablep
(bdd
&optional (fixings '()))
398 "Check whether BDD is satisfiable, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
400 (bdd-satisfiablep
(bdd-restrict
(caar fixings
) (cadr fixings
) bdd
)
402 (not
(bdd-equal bdd
(bdd-false
)))))
404 (defun bdd-var-fixed0
(bdd var
)
405 (ecase
(cuddapi
:cudd-bdd-is-var-essential
(bdd-environment-manager
*bdd-env
*)
407 (var-
>id var
*bdd-env
*)
412 (defun bdd-var-fixed1
(bdd var
)
413 (ecase
(cuddapi
:cudd-bdd-is-var-essential
(bdd-environment-manager
*bdd-env
*)
420 (defgeneric deserialize-bdd
(source
)
421 (:documentation
"Parse a textual representation of a BDD from SOURCE within the current BDD environment."))
423 (defmethod deserialize-bdd
((s string
))
424 (with-input-from-string
(f s
)
425 (deserialize-bdd f
)))
427 (defmethod deserialize-bdd
((s pathname
))
428 (with-open-file
(f s
:direction
:input
)
429 (deserialize-bdd f
)))
431 (defmethod deserialize-bdd
((l list
))
432 (with-input-from-string
(f
(format nil
"~W" l
))
433 (deserialize-bdd f
)))
435 (defmethod deserialize-bdd
((s stream
))
436 "Read a textual external representation of a bdd from STREAM.
437 New variables are allocated in the current bdd environment.
438 Returns two values: the bdd structure and an alist mapping variable numbers to the
439 variable names specified in the bdd file."
440 (labels
((parse-bddfile
(s
)
441 (let
* ((bddblock
(read s
))
442 (data
(member
"BDD" bddblock
:test #'string-equal
) )
446 (error
"Could not find BDD block in ~A" data
))
447 (setf data
(cdr data
))
448 (setf tree
(assoc
"DAG" data
:test #'string-equal
))
450 (error
"Could not find BDD DAG in ~A" data
))
451 (setf tree
(cadr tree
))
452 (setf nodenames
(assoc
"VARNAMES" data
:test #'string-equal
))
454 (error
"Could not find node name mapping in ~A" data
))
455 (setf nodenames
(cadr nodenames
))
456 (values tree nodenames
)))
458 ;; we depend on having consecutive variable numbers in the bdd file
460 ;; Deducing maxvarnum from tree instead of varnames is safer because some
461 ;; variable may be missing a name. In that case we fail softly
: the tree will be
462 ;; fine
, but the mapping returned to the caller will be defective in the same way
463 ;; that the user messed it up when calling serialize-bdd with an incomplete name map.
466 (max-varnum
(third tree
))
467 (max-varnum
(fourth tree
)))
469 (multiple-value-bind
(tree nodenames
)
471 (let
* ((maxvar
(max-varnum tree
))
472 (mapping
(make-hash-table
:size maxvar
:test #'eql
)))
473 ;; fetch new variables
474 (loop
:for i
:from
2 :upto maxvar
475 :do
(setf
(gethash i mapping
) (bdd-new-variable
)))
476 (labels
((walk
(bddtext
)
483 (let
((thisvar
(gethash
(second bddtext
) mapping
))
484 (t-child
(walk
(third bddtext
)))
485 (nil-child
(walk
(fourth bddtext
))))
486 (bdd-or
(bdd-and thisvar t-child
)
487 (bdd-and
(bdd-not thisvar
) nil-child
)))))))
490 (loop
:for pair
:in nodenames
491 :as oldnum
:= (car pair
)
493 (gethash oldnum mapping
))
494 :finally
(return nodenames
))))))))