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
  17
  18 (cl:in-package :swig-macros)
  19
  20 (cl:defun swig-lispify (name flag cl:&optional (package (find-package :cuddapi)))
  21       (cl:labels ((helper (lst last rest cl:&aux (c (cl:car lst)))
  22                     (cl:cond
  23                       ((cl:null lst)
  24                        rest)
  25                       ((cl:upper-case-p c)
  26                        (helper (cl:cdr lst) 'upper
  27                                (cl:case last
  28                                  ((lower digit) (cl:list* c #\- rest))
  29                                  (cl:t (cl:cons c rest)))))
  30                       ((cl:lower-case-p c)
  31                        (helper (cl:cdr lst) 'lower (cl:cons (cl:char-upcase c) rest)))
  32                       ((cl:digit-char-p c)
  33                        (helper (cl:cdr lst) 'digit
  34                                (cl:case last
  35                                  ((upper lower) (cl:list* c #\- rest))
  36                                  (cl:t (cl:cons c rest)))))
  37                       ((cl:char-equal c #\_)
  38                        (helper (cl:cdr lst) '_ (cl:cons #\- rest)))
  39                       ((cl:char-equal c #\-)
  40                        (helper (cl:cdr lst) '- (cl:cons #\- rest)))
  41                       (cl:t
  42                        (cl:error "Invalid character: ~A" c)))))
  43         (cl:let ((fix (cl:case flag
  44                         ((constant enumvalue) "+")
  45                         (variable "*")
  46                         (cl:t ""))))
  47           (cl:intern
  48            (cl:concatenate
  49             'cl:string
  50             fix
  51             (cl:nreverse (helper (cl:concatenate 'cl:list name) cl:nil cl:nil))
  52             fix)
  53            package))))
  54
  55
  56 %}
  57
  58 %{
  59
  60 /* includes that SWIG needs to see to parse the cudd.h file go here */
  61
  62 %}
  63
  64 %insert ("swiglisp") %{
  65
  66
  67 (cl:in-package :cuddapi)
  68 %}
  69 %insert ("swiglisp") %{
  70 ;; foreign type definitions to hide pointer values
  71 (defclass wrapped-pointer ()
  72   ((ptrval :reader get-ptrval :initarg :ptrval)
  73    (ctype  :reader get-ctype :initarg :ctype))
  74   (:documentation "A wrapped pointer"))
  75
  76 (defmethod print-object ((p wrapped-pointer) stream)
  77   (print-unreadable-object (p stream :type nil :identity nil)
  78     (format stream "wrapper around `~A' @0x~16R" (get-ctype p) (get-ptrval p))))
  79
  80 (define-condition foreign-null-pointer-condition (error)
  81   ((type :initarg :type
  82          :reader foreign-null-pointer-condition-type))
  83   (:report (lambda (condition stream)
  84              (format stream "The foreign pointer of type ~A was NULL"
  85                      (foreign-null-pointer-condition-type condition)))))
  86
  87 %}
  88
  89 %define TYPEMAP_WRAPPED_POINTER(PTRTYPE,LISPCLASS)
  90
  91 %insert ("swiglisp") %{
  92 (define-foreign-type LISPCLASS ()
  93   ()
  94   (:actual-type :pointer)
  95   (:documentation "cffi wrapper type around PTRTYPE."))
  96
  97 (define-parse-method LISPCLASS ()
  98   (make-instance 'LISPCLASS))
  99
 100 (defmethod translate-from-foreign (value (type LISPCLASS))
 101   "Wrap PTRTYPE, signaling a null-pointer-exception if value is NULL."
 102   (if (cffi:null-pointer-p value)
 103       (error 'foreign-null-pointer-condition :type type)
 104       (make-instance 'wrapped-pointer :ptrval value :ctype "PTRTYPE")))
 105
 106 (defmethod translate-to-foreign ((g wrapped-pointer) (type LISPCLASS))
 107   "Unwrap PTRTYPE"
 108   (get-ptrval g))
 109
 110 %}
 111 %typemap (cin) PTRTYPE "LISPCLASS"
 112 %typemap (cout) PTRTYPE "LISPCLASS"
 113 %enddef
 114
 115 TYPEMAP_WRAPPED_POINTER(DdManager *, cudd-manager)
 116 TYPEMAP_WRAPPED_POINTER(DdNode *, cudd-node)
 117
 118 %typemap (cin)  DdManager * "cudd-manager"
 119 %typemap (cout) DdManager * "cudd-manager"
 120 %typemap (cin)  DdNode * "cudd-node"
 121 %typemap (cout) DdNode * "cudd-node"
 122
 123 /* Now parse and wrap the API header */
 124 %insert ("swiglisp") %{
 125 (eval-when (:compile-toplevel :load-toplevel)
 126   ;; Muffle compiler-notes globally
 127   #+sbcl (declaim (sb-ext:muffle-conditions sb-ext:defconstant-uneql))
 128
 129 %}
 130
 131 %include "cudd/cudd.h"
 132 %insert ("swiglisp") %{
 133 ) ;; end of eval-when to avoid top-level export
 134 %}
 135
 136 %insert ("swiglisp") %{
 137 ;; (defmethod translate-from-foreign :around (manager (type cudd-manager))
 138 ;;   (let ((cudd-manager (call-next-method)))
 139 ;;     (when manager
 140 ;;       (trivial-garbage:finalize cudd-manager #'(lambda ()
 141 ;;                                               ;; (break "finalize manager #x~x~%" manager)
 142 ;;                                                                                            ;; (format T "kill mgmr ~A~%" manager) (force-output)
 143
 144
 145
 146 ;;                                               (format T "~D nodes unfreed in manager ~A" (cuddapi:cudd-check-zero-ref manager) manager)
 147 ;;                                               ;;                                              (cuddapi:cudd-quit manager)
 148 ;; ;;                                                                                         (format T "killed mgmr ~A~%" manager) (force-output)
 149 ;;                                               )))
 150
 151 ;;     cudd-manager))
 152 %}
 153 %insert ("swiglisp") %{
 154 ;; (defmethod translate-from-foreign :around (node (type cudd-node))
 155 ;;   (let ((cudd-node (call-next-method)))
 156 ;;     (when node
 157 ;;       (trivial-garbage:finalize cudd-node #'(lambda ()
 158 ;;                                            ;; (format T "finalize node #x~x~%" node)
 159 ;;                                            ;; (format T "kill node ~A" node) (force-output)
 160
 161 ;; ;;                                         (format T "~&killed ~A~%" node)
 162 ;;                                            ;;                                              (format T "killed node ~A~%" node) (force-output)
 163 ;;                                            )))
 164 ;;     cudd-node))
 165 %}
 166
 167
 168 \f
 169
 170 %insert ("swiglisp") %{
 171
 172
 173 (cl:in-package :cudd)
 174
 175 \f
 176 ;; for garbage collection purposes we wrap a reference to the manager with each
 177 ;; variable object
 178 (defvar *bdd-env* nil
 179   "A special variable holding the current BDD Environment.")
 180
 181 (deftype wrapped-bdd ()
 182   `(simple-vector 2))
 183
 184 (defmacro wrap-bdd (bdd env)
 185   "Build a lisp object object around the cudd-node v."
 186   `(the wrapped-bdd
 187      (make-array 2 :adjustable NIL :fill-pointer NIL
 188                  :initial-contents
 189                  (list ,bdd ,env)))
 190   )
 191
 192 (defmacro unwrap-bdd (bdd)
 193   "Extract the cudd-node object from bdd."
 194   `(svref (the wrapped-bdd ,bdd) 0)
 195   )
 196
 197 \f
 198 (defun make-cudd-manager (&key
 199                           (initial-num-vars 0)
 200                           (initial-num-slots 256) ;; #.(cuddapi:CUDD-UNIQUE-SLOTS)
 201                           (cache-size 262144) ;; #.(cuddapi:CUDD-CACHE-SLOTS)
 202                           (max-memory 0))
 203   (cuddapi:cudd-init initial-num-vars
 204                      0  ;; num-zvars
 205                      initial-num-slots
 206                      cache-size
 207                      max-memory))
 208
 209 (defstruct (bdd-environment (:constructor construct-bdd-environment))
 210   "A wrapper object describing a CUDD-based BDD environment."
 211   (manager )
 212   (name "" :type string)
 213   ;; caching of the T and F objects of this manager to save FF overhead
 214   (true)
 215   (false)
 216   ;; mapping VARs to foreign IDs
 217   (var->id (make-hash-table :test #'eq) :type hash-table)
 218   (nextvar 0 :type (integer 0 #.(expt 2 (* 8 (- (cffi:foreign-type-size :int) 1))))))
 219
 220 (defmethod print-object ((e bdd-environment) stream)
 221   (print-unreadable-object (e stream :type T)
 222     (format stream "~A (manager @#x~X, ~D vars)"
 223             (bdd-environment-name e)
 224             (cuddapi::get-ptrval (bdd-environment-manager e))
 225             (bdd-environment-nextvar e))))
 226
 227 (defun make-bdd-environment (&key
 228                              (manager (make-cudd-manager))
 229                              (name (format nil "BDD Environment ~A" (gensym "BDDE"))))
 230   (let ((res (construct-bdd-environment :manager manager :name name)))
 231     (setf (bdd-environment-true res)
 232           (wrap-bdd (cuddapi:cudd-read-one manager) res))
 233     (setf (bdd-environment-false res)
 234           (wrap-bdd (cuddapi:cudd-read-logic-zero manager) res))
 235     ;; these need no finalization:
 236     (trivial-garbage:cancel-finalization (unwrap-bdd (bdd-environment-false res)))
 237     (trivial-garbage:cancel-finalization (unwrap-bdd (bdd-environment-true res)))
 238
 239
 240     (let ((vartab (bdd-environment-var->id res)))
 241       (trivial-garbage:finalize res
 242                                 #'(lambda ()
 243                                     (format T "~&killing ~D vars in ~A~%"
 244                                             (hash-table-size vartab)
 245                                             manager)
 246                                     (maphash #'(lambda (key val)
 247                                                  (declare (ignore val))
 248                                                  (cuddapi:cudd-recursive-deref
 249                                                   manager
 250                                                   (unwrap-bdd key)))
 251                                              vartab))))
 252     res))
 253
 254 (eval-when (:load-toplevel)
 255   (setf *bdd-env* (or *bdd-env*
 256                       (make-bdd-environment :name "The global BDD Environment."))))
 257
 258 (defmacro with-bdd-environment (env &body body)
 259   "Execute BODY within the bdd environment ENV."
 260   `(let ((*bdd-env* ,env))
 261      ,@body))
 262 \f
 263 ;;; utility functions for the environment
 264 (defun var->id (var &optional (env *bdd-env*))
 265   "Return the ID for VAR in ENV (which defaults to *bdd-env*)."
 266   (gethash var (bdd-environment-var->id env)))
 267
 268 (defsetf var->id (var &optional (env *bdd-env*)) (id)
 269   `(setf (gethash ,var (bdd-environment-var->id ,env)) ,id))
 270
 271 (defun id->var (id &optional (env *bdd-env*))
 272   "Return the VAR for ID  in ENV (which defaults to *bdd-env*)."
 273   (wrap-bdd (cuddapi:cudd-bdd-ith-var (bdd-environment-manager env) id) env))
 274
 275 \f
 276 (defun bdd-true ()
 277   (bdd-environment-true *bdd-env*))
 278
 279 (defun bdd-false ()
 280   (bdd-environment-false *bdd-env*))
 281
 282 (defun bdd-new-variable ()
 283   (handler-case
 284       (let ((v (wrap-bdd
 285                 (cuddapi:cudd-bdd-new-var (bdd-environment-manager *bdd-env*))
 286                 *bdd-env*))
 287             (id (bdd-environment-nextvar *bdd-env*)))
 288         (progn
 289           (incf (bdd-environment-nextvar *bdd-env*))
 290           (setf (var->id v *bdd-env*) id)
 291           v))
 292     (cuddapi::foreign-null-pointer-condition (c)
 293       (declare (ignore c))
 294       ;; FIXME: maybe try a garbage collection here
 295       (error "CUDD failed to allocate a variable ~D:~%BDD environment ~A full."
 296              (bdd-environment-nextvar *bdd-env*)
 297              *bdd-env*))))
 298
 299 (defun bdd-restrict (var val bdd)
 300   (wrap-bdd
 301    (cuddapi:cudd-bdd-restrict (bdd-environment-manager *bdd-env*)
 302                               (unwrap-bdd bdd)
 303                               (unwrap-bdd (if val var (bdd-not var))))
 304    *bdd-env*))
 305
 306 (defun bdd-and (x y)
 307   (wrap-bdd
 308    (cuddapi:cudd-bdd-and (bdd-environment-manager *bdd-env*)
 309                          (unwrap-bdd x) (unwrap-bdd y))
 310    *bdd-env*))
 311
 312 (defun bdd-or (x y)
 313   (wrap-bdd
 314    (cuddapi:cudd-bdd-or (bdd-environment-manager *bdd-env*)
 315                         (unwrap-bdd x) (unwrap-bdd y))
 316    *bdd-env*))
 317
 318 (defun bdd-not (x)
 319   ;; FIXME: cudd-not is a macro and hence not swig'ed, but would probably
 320   ;; perform be better
 321   (wrap-bdd
 322    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 323                           (unwrap-bdd x)
 324                           (unwrap-bdd x))
 325    *bdd-env*))
 326
 327 (defun bdd-xor (x y)
 328   (wrap-bdd
 329    (cuddapi:cudd-bdd-xor (bdd-environment-manager *bdd-env*)
 330                          (unwrap-bdd x)
 331                          (unwrap-bdd y))
 332    *bdd-env*))
 333
 334 (defun bdd-nand (x y)
 335   (wrap-bdd
 336    (cuddapi:cudd-bdd-nand (bdd-environment-manager *bdd-env*)
 337                           (unwrap-bdd x)
 338                           (unwrap-bdd y))
 339    *bdd-env*))
 340
 341 (defun bdd-nor (x y)
 342   (wrap-bdd
 343    (cuddapi:cudd-bdd-nor (bdd-environment-manager *bdd-env*)
 344                          (unwrap-bdd x)
 345                          (unwrap-bdd y))
 346    *bdd-env*))
 347
 348 (defun bdd-and-not (bdd1 bdd2)
 349   (bdd-and bdd1 (bdd-not bdd2)))
 350
 351 (defun bdd-or-not (bdd1 bdd2)
 352   (bdd-or bdd1 (bdd-not bdd2)))
 353
 354 (defun bdd-implies (bdd1 bdd2)
 355   (bdd-or-not bdd1 bdd2))
 356
 357 (defun bdd-iff (bdd1 bdd2)
 358   (bdd-and (bdd-implies bdd1 bdd2)
 359            (bdd-implies bdd2 bdd1)))
 360
 361 (defun bdd-equal (bdd1 bdd2)
 362   "Check whether BDD1 and BDD2 are equal."
 363   (let ((b1 (unwrap-bdd bdd1))
 364         (b2 (unwrap-bdd bdd2)))
 365     (and (= 1 (cuddapi:cudd-bdd-leq (bdd-environment-manager *bdd-env*) b1 b2))
 366          (= 1 (cuddapi:cudd-bdd-leq (bdd-environment-manager *bdd-env*) b2 b1)))))
 367
 368 (defun bdd-tautologyp (bdd &optional (fixings '()))
 369   "Check whether BDD is tautologic, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
 370   (if fixings
 371       (bdd-tautologyp (bdd-restrict (caar fixings) (cadr fixings) bdd)
 372                       (cdr fixings))
 373       (bdd-equal bdd (bdd-true))))
 374
 375 (defun bdd-satisfiablep (bdd &optional (fixings '()))
 376   "Check whether BDD is satisfiable, possibly under a given fixing in FIXINGS, a list of pairs (bddvar . value), value being T or NIL. "
 377   (if fixings
 378       (bdd-satisfiablep (bdd-restrict (caar fixings) (cadr fixings) bdd)
 379                         (cdr fixings))
 380       (not (bdd-equal bdd (bdd-false)))))
 381
 382 (defun bdd-var-fixed0 (bdd var)
 383   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 384                                             bdd
 385                                             (var->id var *bdd-env*)
 386                                             0)
 387     (1 T)
 388     (0 NIL)))
 389
 390 (defun bdd-var-fixed1 (bdd var)
 391   (ecase (cuddapi:cudd-bdd-is-var-essential (bdd-environment-manager *bdd-env*)
 392                                             bdd
 393                                             (var->id var)
 394                                             1)
 395     (1 T)
 396     (0 NIL)))
 397
 398 (defgeneric deserialize-bdd (source)
 399   (:documentation "Parse a textual representation of a BDD from SOURCE within the current BDD environment."))
 400
 401 (defmethod deserialize-bdd ((s string))
 402   (with-input-from-string (f s)
 403     (deserialize-bdd f)))
 404
 405 (defmethod deserialize-bdd ((s pathname))
 406   (with-open-file (f s :direction :input)
 407     (deserialize-bdd f)))
 408
 409 (defmethod deserialize-bdd ((l list))
 410   (with-input-from-string (f (format nil "~W" l))
 411     (deserialize-bdd f)))
 412
 413 (defmethod deserialize-bdd ((s stream))
 414   "Read a textual external representation of a bdd from STREAM.
 415 New variables are allocated in the current bdd environment.
 416 Returns two values: the bdd structure and an alist mapping variable numbers to the
 417 variable names specified in the bdd file."
 418   (labels ((parse-bddfile (s)
 419              (let* ((bddblock (read s))
 420                     (data (member "BDD" bddblock :test #'string-equal) )
 421                     (tree nil)
 422                     (nodenames nil))
 423                (unless data
 424                  (error "Could not find BDD block in ~A" data))
 425                (setf data (cdr data))
 426                (setf tree (assoc "DAG" data :test #'string-equal))
 427                (unless tree
 428                  (error "Could not find BDD DAG in ~A" data))
 429                (setf tree (cadr tree))
 430                (setf nodenames (assoc "VARNAMES" data :test #'string-equal))
 431                (unless nodenames
 432                  (error "Could not find node name mapping in ~A" data))
 433                (setf nodenames (cadr nodenames))
 434                (values tree nodenames)))
 435            (max-varnum (tree)
 436              ;; we depend on having consecutive variable numbers in the bdd file
 437              ;; starting above 0
 438              ;; Deducing maxvarnum from tree instead of varnames is safer because some
 439              ;; variable may be missing a name. In that case we fail softly: the tree will be
 440              ;; fine, but the mapping returned to the caller will be defective in the same way
 441              ;; that the user messed it up when calling serialize-bdd with an incomplete name map.
 442              (if (consp tree)
 443                  (max (second tree)
 444                       (max-varnum (third tree))
 445                       (max-varnum (fourth tree)))
 446                  0)))
 447     (multiple-value-bind (tree nodenames)
 448         (parse-bddfile s)
 449       (let* ((maxvar (max-varnum tree))
 450              (mapping (make-hash-table :size maxvar :test #'eql)))
 451         ;; fetch new variables
 452         (loop :for i :from 2 :upto maxvar
 453            :do (setf (gethash i mapping) (bdd-new-variable)))
 454         (labels ((walk (bddtext)
 455                    (cond
 456                      ((eq bddtext NIL)
 457                       (bdd-false))
 458                      ((eq bddtext T)
 459                       (bdd-true))
 460                      (T
 461                       (let ((thisvar (gethash (second bddtext) mapping))
 462                             (t-child (walk (third bddtext)))
 463                             (nil-child (walk (fourth bddtext))))
 464                         (bdd-or (bdd-and thisvar t-child)
 465                                 (bdd-and (bdd-not thisvar) nil-child)))))))
 466           (values
 467            (walk tree)
 468            (loop :for pair :in nodenames
 469               :as oldnum := (car pair)
 470               :do (setf (car pair)
 471                         (gethash oldnum mapping))
 472               :finally (return nodenames))))))))
 473
 474
 475 %}