cudd-cffi.i

   1 /* swig interface wrapper file for cffi binding generation -*- lisp -*- */
   2 /* swig -cffi interface for CUDD */
   3 /* (c) 2009 Utz-Uwe Haus */
   4
   5 %module "cuddapi"
   6
   7 %feature("intern_function","1");   // use swig-lispify
   8 %feature("export");                // export wrapped things
   9
  10 %insert("lisphead")%{
  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))))
  15
  16 (cl:defpackage :swig-macros
  17   (:use :cl :cffi)
  18   (:documentation "Package containing utility functions for SWIG cffi interface generation")
  19   (:export #:swig-lispify #:defanonenum))
  20
  21 (cl:in-package :swig-macros)
  22
  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)))
  25                     (cl:cond
  26                       ((cl:null lst)
  27                        rest)
  28                       ((cl:upper-case-p c)
  29                        (helper (cl:cdr lst) 'upper
  30                                (cl:case last
  31                                  ((lower digit) (cl:list* c #\- rest))
  32                                  (cl:t (cl:cons c rest)))))
  33                       ((cl:lower-case-p c)
  34                        (helper (cl:cdr lst) 'lower (cl:cons (cl:char-upcase c) rest)))
  35                       ((cl:digit-char-p c)
  36                        (helper (cl:cdr lst) 'digit
  37                                (cl:case last
  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)))
  44                       (cl:t
  45                        (cl:error "Invalid character: ~A" c)))))
  46         (cl:let ((fix (cl:case flag
  47                         ((constant enumvalue) "+")
  48                         (variable "*")
  49                         (cl:t ""))))
  50           (cl:intern
  51            (cl:concatenate
  52             'cl:string
  53             fix
  54             (cl:nreverse (helper (cl:concatenate 'cl:list name) cl:nil cl:nil))
  55             fix)
  56            package))))
  57
  58
  59 %}
  60
  61 %{
  62
  63 /* includes that SWIG needs to see to parse the cudd.h file go here */
  64
  65 %}
  66
  67 %insert ("swiglisp") %{
  68
  69 (cl:defpackage #:cuddapi
  70   (:use :cl :cffi :swig-macros)
  71   (:export #:cudd-manager #:cudd-node)
  72   ;; other exports done by swig
  73   )
  74 (cl:in-package :cuddapi)
  75 %}
  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"))
  82
  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))))
  86
  87 (define-condition foreign-null-pointer-condition (error)
  88   ((type :initarg :type
  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)))))
  93
  94 %}
  95
  96 %define TYPEMAP_WRAPPED_POINTER(PTRTYPE,LISPCLASS)
  97
  98 %insert ("swiglisp") %{
  99 (define-foreign-type LISPCLASS ()
 100   ()
 101   (:actual-type :pointer)
 102   (:documentation "cffi wrapper type around PTRTYPE."))
 103
 104 (define-parse-method LISPCLASS ()
 105   (make-instance 'LISPCLASS))
 106
 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")))
 112
 113 (defmethod translate-to-foreign ((g wrapped-pointer) (type LISPCLASS))
 114   "Unwrap PTRTYPE"
 115   (get-ptrval g))
 116
 117 %}
 118 %typemap (cin) PTRTYPE "LISPCLASS"
 119 %typemap (cout) PTRTYPE "LISPCLASS"
 120 %enddef
 121
 122 TYPEMAP_WRAPPED_POINTER(DdManager *, cudd-manager)
 123 TYPEMAP_WRAPPED_POINTER(DdNode *, cudd-node)
 124
 125 %typemap (cin)  DdManager * "cudd-manager"
 126 %typemap (cout) DdManager * "cudd-manager"
 127 %typemap (cin)  DdNode * "cudd-node"
 128 %typemap (cout) DdNode * "cudd-node"
 129
 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))
 135
 136 %}
 137
 138 %include "cudd/cudd.h"
 139 %insert ("swiglisp") %{
 140 ) ;; end of eval-when to avoid top-level export
 141 %}
 142
 143 %insert ("swiglisp") %{
 144 ;; (defmethod translate-from-foreign :around (manager (type cudd-manager))
 145 ;;   (let ((cudd-manager (call-next-method)))
 146 ;;     (when manager
 147 ;;       (trivial-garbage:finalize cudd-manager #'(lambda ()
 148 ;;                                               ;; (break "finalize manager #x~x~%" manager)
 149 ;;                                                                                            ;; (format T "kill mgmr ~A~%" manager) (force-output)
 150
 151
 152
 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)
 156 ;;                                               )))
 157
 158 ;;     cudd-manager))
 159 %}
 160 %insert ("swiglisp") %{
 161 ;; (defmethod translate-from-foreign :around (node (type cudd-node))
 162 ;;   (let ((cudd-node (call-next-method)))
 163 ;;     (when node
 164 ;;       (trivial-garbage:finalize cudd-node #'(lambda ()
 165 ;;                                            ;; (format T "finalize node #x~x~%" node)
 166 ;;                                            ;; (format T "kill node ~A" node) (force-output)
 167
 168 ;; ;;                                         (format T "~&killed ~A~%" node)
 169 ;;                                            ;;                                              (format T "killed node ~A~%" node) (force-output)
 170 ;;                                            )))
 171 ;;     cudd-node))
 172 %}
 173
 174
 175 \f
 176
 177 %insert ("swiglisp") %{
 178 ;;; Higher-level interface similar to de.uuhaus.bdd
 179 (defpackage #:cudd
 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))
 194
 195 (cl:in-package :cudd)
 196
 197 \f
 198 ;; for garbage collection purposes we wrap a reference to the manager with each
 199 ;; variable object
 200 (defvar *bdd-env* nil
 201   "A special variable holding the current BDD Environment.")
 202
 203 (deftype wrapped-bdd ()
 204   `(simple-vector 2))
 205
 206 (defmacro wrap-bdd (bdd env)
 207   "Build a lisp object object around the cudd-node v."
 208   `(the wrapped-bdd
 209      (make-array 2 :adjustable NIL :fill-pointer NIL
 210                  :initial-contents
 211                  (list ,bdd ,env)))
 212   )
 213
 214 (defmacro unwrap-bdd (bdd)
 215   "Extract the cudd-node object from bdd."
 216   `(svref (the wrapped-bdd ,bdd) 0)
 217   )
 218
 219 \f
 220 (defun make-cudd-manager (&key
 221                           (initial-num-vars 0)
 222                           (initial-num-slots 256) ;; #.(cuddapi:CUDD-UNIQUE-SLOTS)
 223                           (cache-size 262144) ;; #.(cuddapi:CUDD-CACHE-SLOTS)
 224                           (max-memory 0))
 225   (cuddapi:cudd-init initial-num-vars
 226                      0  ;; num-zvars
 227                      initial-num-slots
 228                      cache-size
 229                      max-memory))
 230
 231 (defstruct (bdd-environment (:constructor construct-bdd-environment))
 232   "A wrapper object describing a CUDD-based BDD environment."
 233   (manager )
 234   (name "" :type string)
 235   ;; caching of the T and F objects of this manager to save FF overhead
 236   (true)
 237   (false)
 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))))))
 241
 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))))
 248
 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)))
 260
 261
 262     (let ((vartab (bdd-environment-var->id res)))
 263       (trivial-garbage:finalize res
 264                                 #'(lambda ()
 265                                     (format T "~&killing ~D vars in ~A~%"
 266                                             (hash-table-size vartab)
 267                                             manager)
 268                                     (maphash #'(lambda (key val)
 269                                                  (declare (ignore val))
 270                                                  (cuddapi:cudd-recursive-deref
 271                                                   manager
 272                                                   (unwrap-bdd key)))
 273                                              vartab))))
 274     res))
 275
 276 (eval-when (:load-toplevel)
 277   (setf *bdd-env* (or *bdd-env*
 278                       (make-bdd-environment :name "The global BDD Environment."))))
 279
 280 (defmacro with-bdd-environment (env &body body)
 281   "Execute BODY within the bdd environment ENV."
 282   `(let ((*bdd-env* ,env))
 283      ,@body))
 284 \f
 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)))
 289
 290 (defsetf var->id (var &optional (env *bdd-env*)) (id)
 291   `(setf (gethash ,var (bdd-environment-var->id ,env)) ,id))
 292
 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))
 296
 297 \f
 298 (defun bdd-true ()
 299   (bdd-environment-true *bdd-env*))
 300
 301 (defun bdd-false ()
 302   (bdd-environment-false *bdd-env*))
 303
 304 (defun bdd-new-variable ()
 305   (handler-case
 306       (let ((v (wrap-bdd
 307                 (cuddapi:cudd-bdd-new-var (bdd-environment-manager *bdd-env*))
 308                 *bdd-env*))
 309             (id (bdd-environment-nextvar *bdd-env*)))
 310         (progn
 311           (incf (bdd-environment-nextvar *bdd-env*))
 312           (setf (var->id v *bdd-env*) id)
 313           v))
 314     (cuddapi::foreign-null-pointer-condition (c)
 315       (declare (ignore 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*)
 319              *bdd-env*))))
 320
 321 (defun bdd-restrict (var val bdd)
 322   (wrap-bdd
 323    (cuddapi:cudd-bdd-restrict (bdd-environment-manager *bdd-env*)
 324                               (unwrap-bdd bdd)
 325                               (unwrap-bdd (if val var (bdd-not var))))
 326    *bdd-env*))
 327
 328 (defun bdd-and (x y)
 329   (wrap-bdd
 330    (cuddapi:cudd-bdd-and (bdd-environment-manager *bdd-env*)
 331                          (unwrap-bdd x) (unwrap-bdd y))
 332    *bdd-env*))
 333
 334 (defun bdd-or (x y)
 335   (wrap-bdd
 336    (cuddapi:cudd-bdd-or (bdd-environment-manager *bdd-env*)
 337                         (unwrap-bdd x) (unwrap-bdd y))
 338    *bdd-env*))
 339
 340 (defun bdd-not (x)
 341   ;; FIXME: cudd-not is a macro and hence not swig'ed, but would probably
 342   ;; perform be better
 343   (wrap-bdd
 344    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 345                           (unwrap-bdd x)
 346                           (unwrap-bdd x))
 347    *bdd-env*))
 348
 349 (defun bdd-xor (x y)
 350   (wrap-bdd
 351    (cuddapi:cudd-bdd-xor (bdd-environment-manager *bdd-env*)
 352                          (unwrap-bdd x)
 353                          (unwrap-bdd y))
 354    *bdd-env*))
 355
 356 (defun bdd-nand (x y)
 357   (wrap-bdd
 358    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 359                           (unwrap-bdd x)
 360                           (unwrap-bdd y))
 361    *bdd-env*))
 362
 363 (defun bdd-nor (x y)
 364   (wrap-bdd
 365    (cuddapi:cudd-bdd-nor (bdd-environment-manager *bdd-env*)
 366                          (unwrap-bdd x)
 367                          (unwrap-bdd y))
 368    *bdd-env*))
 369
 370 (defun bdd-and-not (bdd1 bdd2)
 371   (bdd-and bdd1 (bdd-not bdd2)))
 372
 373 (defun bdd-or-not (bdd1 bdd2)
 374   (bdd-or bdd1 (bdd-not bdd2)))
 375
 376 (defun bdd-implies (bdd1 bdd2)
 377   (bdd-or-not bdd1 bdd2))
 378
 379 (defun bdd-iff (bdd1 bdd2)
 380   (bdd-and (bdd-implies bdd1 bdd2)
 381            (bdd-implies bdd2 bdd1)))
 382
 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)))))
 389
 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. "
 392   (if fixings
 393       (bdd-tautologyp (bdd-restrict (caar fixings) (cadr fixings) bdd)
 394                       (cdr fixings))
 395       (bdd-equal bdd (bdd-true))))
 396
 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. "
 399   (if fixings
 400       (bdd-satisfiablep (bdd-restrict (caar fixings) (cadr fixings) bdd)
 401                         (cdr fixings))
 402       (not (bdd-equal bdd (bdd-false)))))
 403
 404 (defun bdd-var-fixed0 (bdd var)
 405   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 406                                             bdd
 407                                             (var->id var *bdd-env*)
 408                                             0)
 409     (1 T)
 410     (0 NIL)))
 411
 412 (defun bdd-var-fixed1 (bdd var)
 413   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 414                                             bdd
 415                                             (var->id var)
 416                                             1)
 417     (1 T)
 418     (0 NIL)))
 419
 420 (defgeneric deserialize-bdd (source)
 421   (:documentation "Parse a textual representation of a BDD from SOURCE within the current BDD environment."))
 422
 423 (defmethod deserialize-bdd ((s string))
 424   (with-input-from-string (f s)
 425     (deserialize-bdd f)))
 426
 427 (defmethod deserialize-bdd ((s pathname))
 428   (with-open-file (f s :direction :input)
 429     (deserialize-bdd f)))
 430
 431 (defmethod deserialize-bdd ((l list))
 432   (with-input-from-string (f (format nil "~W" l))
 433     (deserialize-bdd f)))
 434
 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) )
 443                     (tree nil)
 444                     (nodenames nil))
 445                (unless data
 446                  (error "Could not find BDD block in ~A" data))
 447                (setf data (cdr data))
 448                (setf tree (assoc "DAG" data :test #'string-equal))
 449                (unless tree
 450                  (error "Could not find BDD DAG in ~A" data))
 451                (setf tree (cadr tree))
 452                (setf nodenames (assoc "VARNAMES" data :test #'string-equal))
 453                (unless nodenames
 454                  (error "Could not find node name mapping in ~A" data))
 455                (setf nodenames (cadr nodenames))
 456                (values tree nodenames)))
 457            (max-varnum (tree)
 458              ;; we depend on having consecutive variable numbers in the bdd file
 459              ;; starting above 0
 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.
 464              (if (consp tree)
 465                  (max (second tree)
 466                       (max-varnum (third tree))
 467                       (max-varnum (fourth tree)))
 468                  0)))
 469     (multiple-value-bind (tree nodenames)
 470         (parse-bddfile s)
 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)
 477                    (cond
 478                      ((eq bddtext NIL)
 479                       (bdd-false))
 480                      ((eq bddtext T)
 481                       (bdd-true))
 482                      (T
 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)))))))
 488           (values
 489            (walk tree)
 490            (loop :for pair :in nodenames
 491               :as oldnum := (car pair)
 492               :do (setf (car pair)
 493                         (gethash oldnum mapping))
 494               :finally (return nodenames))))))))
 495
 496
 497 %}