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                                                   (unwrap-bdd key)))
 272                                              vartab))))
 273     res))
 274
 275 (eval-when (:load-toplevel)
 276   (setf *bdd-env* (or *bdd-env*
 277                       (make-bdd-environment :name "The global BDD Environment."))))
 278
 279 (defmacro with-bdd-environment (env &body body)
 280   "Execute BODY within the bdd environment ENV."
 281   `(let ((*bdd-env* ,env))
 282      ,@body))
 283 \f
 284 ;;; utility functions for the environment
 285 (defun var->id (var &optional (env *bdd-env*))
 286   "Return the ID for VAR in ENV (which defaults to *bdd-env*)."
 287   (gethash var (bdd-environment-var->id env)))
 288
 289 (defsetf var->id (var &optional (env *bdd-env*)) (id)
 290   `(setf (gethash ,var (bdd-environment-var->id ,env)) ,id))
 291
 292 (defun id->var (id &optional (env *bdd-env*))
 293   "Return the VAR for ID  in ENV (which defaults to *bdd-env*)."
 294   (wrap-bdd (cuddapi:cudd-bdd-ith-var (bdd-environment-manager env) id) env))
 295
 296 \f
 297 (defun bdd-true ()
 298   (bdd-environment-true *bdd-env*))
 299
 300 (defun bdd-false ()
 301   (bdd-environment-false *bdd-env*))
 302
 303 (defun bdd-new-variable ()
 304   (handler-case
 305       (let ((v (wrap-bdd
 306                 (cuddapi:cudd-bdd-new-var (bdd-environment-manager *bdd-env*))
 307                 *bdd-env*))
 308             (id (bdd-environment-nextvar *bdd-env*)))
 309         (progn
 310           (incf (bdd-environment-nextvar *bdd-env*))
 311           (setf (var->id v *bdd-env*) id)
 312           v))
 313     (cuddapi::foreign-null-pointer-condition (c)
 314       (declare (ignore c))
 315       ;; FIXME: maybe try a garbage collection here
 316       (error "CUDD failed to allocate a variable ~D:~%BDD environment ~A full."
 317              (bdd-environment-nextvar *bdd-env*)
 318              *bdd-env*))))
 319
 320 (defun bdd-restrict (var val bdd)
 321   (wrap-bdd
 322    (cuddapi:cudd-bdd-restrict (bdd-environment-manager *bdd-env*)
 323                               (unwrap-bdd bdd)
 324                               (unwrap-bdd (if val var (bdd-not var))))
 325    *bdd-env*))
 326
 327 (defun bdd-and (x y)
 328   (wrap-bdd
 329    (cuddapi:cudd-bdd-and (bdd-environment-manager *bdd-env*)
 330                          (unwrap-bdd x) (unwrap-bdd y))
 331    *bdd-env*))
 332
 333 (defun bdd-or (x y)
 334   (wrap-bdd
 335    (cuddapi:cudd-bdd-or (bdd-environment-manager *bdd-env*)
 336                         (unwrap-bdd x) (unwrap-bdd y))
 337    *bdd-env*))
 338
 339 (defun bdd-not (x)
 340   ;; FIXME: cudd-not is a macro and hence not swig'ed, but would probably
 341   ;; perform be better
 342   (wrap-bdd
 343    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 344                           (unwrap-bdd x)
 345                           (unwrap-bdd x))
 346    *bdd-env*))
 347
 348 (defun bdd-xor (x y)
 349   (wrap-bdd
 350    (cuddapi:cudd-bdd-xor (bdd-environment-manager *bdd-env*)
 351                          (unwrap-bdd x)
 352                          (unwrap-bdd y))
 353    *bdd-env*))
 354
 355 (defun bdd-nand (x y)
 356   (wrap-bdd
 357    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 358                           (unwrap-bdd x)
 359                           (unwrap-bdd y))
 360    *bdd-env*))
 361
 362 (defun bdd-nor (x y)
 363   (wrap-bdd
 364    (cuddapi:cudd-bdd-nor (bdd-environment-manager *bdd-env*)
 365                          (unwrap-bdd x)
 366                          (unwrap-bdd y))
 367    *bdd-env*))
 368
 369 (defun bdd-and-not (bdd1 bdd2)
 370   (bdd-and bdd1 (bdd-not bdd2)))
 371
 372 (defun bdd-or-not (bdd1 bdd2)
 373   (bdd-or bdd1 (bdd-not bdd2)))
 374
 375 (defun bdd-implies (bdd1 bdd2)
 376   (bdd-or-not bdd1 bdd2))
 377
 378 (defun bdd-iff (bdd1 bdd2)
 379   (bdd-and (bdd-implies bdd1 bdd2)
 380            (bdd-implies bdd2 bdd1)))
 381
 382 (defun bdd-equal (bdd1 bdd2)
 383   "Check whether BDD1 and BDD2 are equal."
 384   (let ((b1 (unwrap-bdd bdd1))
 385         (b2 (unwrap-bdd bdd2)))
 386     (and (= 1 (cuddapi:cudd-bdd-leq (bdd-environment-manager *bdd-env*) b1 b2))
 387          (= 1 (cuddapi:cudd-bdd-leq (bdd-environment-manager *bdd-env*) b2 b1)))))
 388
 389 (defun bdd-tautologyp (bdd &optional (fixings '()))
 390   "Check whether BDD is tautologic, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
 391   (if fixings
 392       (bdd-tautologyp (bdd-restrict (caar fixings) (cadr fixings) bdd)
 393                       (cdr fixings))
 394       (bdd-equal bdd (bdd-true))))
 395
 396 (defun bdd-satisfiablep (bdd &optional (fixings '()))
 397   "Check whether BDD is satisfiable, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
 398   (if fixings
 399       (bdd-satisfiablep (bdd-restrict (caar fixings) (cadr fixings) bdd)
 400                         (cdr fixings))
 401       (not (bdd-equal bdd (bdd-false)))))
 402
 403 (defun bdd-var-fixed0 (bdd var)
 404   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 405                                             bdd
 406                                             (var->id var *bdd-env*)
 407                                             0)
 408     (1 T)
 409     (0 NIL)))
 410
 411 (defun bdd-var-fixed1 (bdd var)
 412   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 413                                             bdd
 414                                             (var->id var)
 415                                             1)
 416     (1 T)
 417     (0 NIL)))
 418
 419 (defgeneric deserialize-bdd (source)
 420   (:documentation "Parse a textual representation of a BDD from SOURCE within the current BDD environment."))
 421
 422 (defmethod deserialize-bdd ((s string))
 423   (with-input-from-string (f s)
 424     (deserialize-bdd f)))
 425
 426 (defmethod deserialize-bdd ((s pathname))
 427   (with-open-file (f s :direction :input)
 428     (deserialize-bdd f)))
 429
 430 (defmethod deserialize-bdd ((l list))
 431   (with-input-from-string (f (format nil "~W" l))
 432     (deserialize-bdd f)))
 433
 434 (defmethod deserialize-bdd ((s stream))
 435   "Read a textual external representation of a bdd from STREAM.
 436 New variables are allocated in the current bdd environment.
 437 Returns two values: the bdd structure and an alist mapping variable numbers to the
 438 variable names specified in the bdd file."
 439   (labels ((parse-bddfile (s)
 440              (let* ((bddblock (read s))
 441                     (data (member "BDD" bddblock :test #'string-equal) )
 442                     (tree nil)
 443                     (nodenames nil))
 444                (unless data
 445                  (error "Could not find BDD block in ~A" data))
 446                (setf data (cdr data))
 447                (setf tree (assoc "DAG" data :test #'string-equal))
 448                (unless tree
 449                  (error "Could not find BDD DAG in ~A" data))
 450                (setf tree (cadr tree))
 451                (setf nodenames (assoc "VARNAMES" data :test #'string-equal))
 452                (unless nodenames
 453                  (error "Could not find node name mapping in ~A" data))
 454                (setf nodenames (cadr nodenames))
 455                (values tree nodenames)))
 456            (max-varnum (tree)
 457              ;; we depend on having consecutive variable numbers in the bdd file
 458              ;; starting above 0
 459              ;; Deducing maxvarnum from tree instead of varnames is safer because some
 460              ;; variable may be missing a name. In that case we fail softly: the tree will be
 461              ;; fine, but the mapping returned to the caller will be defective in the same way
 462              ;; that the user messed it up when calling serialize-bdd with an incomplete name map.
 463              (if (consp tree)
 464                  (max (second tree)
 465                       (max-varnum (third tree))
 466                       (max-varnum (fourth tree)))
 467                  0)))
 468     (multiple-value-bind (tree nodenames)
 469         (parse-bddfile s)
 470       (let* ((maxvar (max-varnum tree))
 471              (mapping (make-hash-table :size maxvar :test #'eql)))
 472         ;; fetch new variables
 473         (loop :for i :from 2 :upto maxvar
 474            :do (setf (gethash i mapping) (bdd-new-variable)))
 475         (labels ((walk (bddtext)
 476                    (cond
 477                      ((eq bddtext NIL)
 478                       (bdd-false))
 479                      ((eq bddtext T)
 480                       (bdd-true))
 481                      (T
 482                       (let ((thisvar (gethash (second bddtext) mapping))
 483                             (t-child (walk (third bddtext)))
 484                             (nil-child (walk (fourth bddtext))))
 485                         (bdd-or (bdd-and thisvar t-child)
 486                                 (bdd-and (bdd-not thisvar) nil-child)))))))
 487           (values
 488            (walk tree)
 489            (loop :for pair :in nodenames
 490               :as oldnum := (car pair)
 491               :do (setf (car pair)
 492                         (gethash oldnum mapping))
 493               :finally (return nodenames))))))))
 494
 495
 496 %}