5f26bbe7eab3

--- a/.ffignore	Thu Oct 27 14:38:18 2016 +0000
+++ b/.ffignore	Thu Oct 27 15:45:42 2016 +0000
@@ -1,1 +1,2 @@
 docs/build
+build

--- a/Makefile	Thu Oct 27 14:38:18 2016 +0000
+++ b/Makefile	Thu Oct 27 15:45:42 2016 +0000
@@ -18,7 +18,10 @@
 	cd build/cudd-3.0.0 && ./configure --enable-shared && make
 	cp build/cudd-3.0.0/cudd/.libs/libcudd-*.dylib build/libcudd.dylib
 
-cudd: build/libcudd.dylib
+src/cudd.lisp: build/cudd-3.0.0 src/cudd.i
+	swig -cffi src/cudd.i
+
+cudd: build/libcudd.dylib src/cudd.lisp
 
 # Misc ------------------------------------------------------------------------
 clean:

--- a/scully.asd	Thu Oct 27 14:38:18 2016 +0000
+++ b/scully.asd	Thu Oct 27 15:45:42 2016 +0000
@@ -27,6 +27,7 @@
                (:module "src" :serial t
                 :components ((:file "gdl")
                              (:file "rule-trees")
+                             (:file "cudd")
                              (:file "zdd")
                              (:module "reasoners" :serial t
                               :components ((:file "prolog")))

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/cudd.i	Thu Oct 27 15:45:42 2016 +0000
@@ -0,0 +1,24 @@
+%module cudd
+
+%feature("intern_function","1");
+%feature("export");
+
+%insert("lisphead")%{
+
+(cl:defpackage :scully.cudd)
+(cl:in-package :scully.cudd)
+
+(cffi:define-foreign-library scully.zdd::cudd
+  (:darwin "./build/libcudd.dylib"))
+
+(cffi:use-foreign-library scully.zdd::cudd)
+
+%}
+
+%inline %{
+
+typedef unsigned int size_t;
+
+%}
+
+%include "build/cudd-3.0.0/cudd/cudd.h"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/cudd.lisp	Thu Oct 27 15:45:42 2016 +0000
@@ -0,0 +1,3241 @@
+;;; This file was automatically generated by SWIG (http://www.swig.org).
+;;; Version 3.0.10
+;;;
+;;; Do not make changes to this file unless you know what you are doing--modify
+;;; the SWIG interface file instead.
+
+
+(cl:when (cl:not (cl:find-package :scully.cudd))
+  (cl:defpackage :scully.cudd))
+
+(cl:defpackage :scully.cudd)
+(cl:in-package :scully.cudd)
+
+(cffi:define-foreign-library scully.zdd::cudd
+  (:darwin "./build/libcudd.dylib"))
+
+(cffi:use-foreign-library scully.zdd::cudd)
+
+
+
+
+;;;SWIG wrapper code starts here
+
+(cl:defmacro defanonenum (cl:&body enums)
+   "Converts anonymous enums to defconstants."
+  `(cl:progn ,@(cl:loop for value in enums
+                        for index = 0 then (cl:1+ index)
+                        when (cl:listp value) do (cl:setf index (cl:second value)
+                                                          value (cl:first value))
+                        collect `(cl:defconstant ,value ,index))))
+
+(cl:eval-when (:compile-toplevel :load-toplevel)
+  (cl:unless (cl:fboundp 'swig-lispify)
+    (cl:defun swig-lispify (name flag cl:&optional (package cl:*package*))
+      (cl:labels ((helper (lst last rest cl:&aux (c (cl:car lst)))
+                    (cl:cond
+                      ((cl:null lst)
+                       rest)
+                      ((cl:upper-case-p c)
+                       (helper (cl:cdr lst) 'upper
+                               (cl:case last
+                                 ((lower digit) (cl:list* c #\- rest))
+                                 (cl:t (cl:cons c rest)))))
+                      ((cl:lower-case-p c)
+                       (helper (cl:cdr lst) 'lower (cl:cons (cl:char-upcase c) rest)))
+                      ((cl:digit-char-p c)
+                       (helper (cl:cdr lst) 'digit 
+                               (cl:case last
+                                 ((upper lower) (cl:list* c #\- rest))
+                                 (cl:t (cl:cons c rest)))))
+                      ((cl:char-equal c #\_)
+                       (helper (cl:cdr lst) '_ (cl:cons #\- rest)))
+                      (cl:t
+                       (cl:error "Invalid character: ~A" c)))))
+        (cl:let ((fix (cl:case flag
+                        ((constant enumvalue) "+")
+                        (variable "*")
+                        (cl:t ""))))
+          (cl:intern
+           (cl:concatenate
+            'cl:string
+            fix
+            (cl:nreverse (helper (cl:concatenate 'cl:list name) cl:nil cl:nil))
+            fix)
+           package))))))
+
+;;;SWIG wrapper code ends here
+
+
+(cl:defconstant #.(swig-lispify "CUDD_TRUE" 'constant) 1)
+
+(cl:export '#.(swig-lispify "CUDD_TRUE" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_FALSE" 'constant) 0)
+
+(cl:export '#.(swig-lispify "CUDD_FALSE" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_OUT_OF_MEM" 'constant) -1)
+
+(cl:export '#.(swig-lispify "CUDD_OUT_OF_MEM" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_UNIQUE_SLOTS" 'constant) 256)
+
+(cl:export '#.(swig-lispify "CUDD_UNIQUE_SLOTS" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_CACHE_SLOTS" 'constant) 262144)
+
+(cl:export '#.(swig-lispify "CUDD_CACHE_SLOTS" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_RESIDUE_DEFAULT" 'constant) 0)
+
+(cl:export '#.(swig-lispify "CUDD_RESIDUE_DEFAULT" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_RESIDUE_MSB" 'constant) 1)
+
+(cl:export '#.(swig-lispify "CUDD_RESIDUE_MSB" 'constant))
+
+(cl:defconstant #.(swig-lispify "CUDD_RESIDUE_TC" 'constant) 2)
+
+(cl:export '#.(swig-lispify "CUDD_RESIDUE_TC" 'constant))
+
+(cffi:defcenum #.(swig-lispify "Cudd_ReorderingType" 'enumname)
+	#.(swig-lispify "CUDD_REORDER_SAME" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_NONE" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_RANDOM" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_RANDOM_PIVOT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_SIFT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_SIFT_CONVERGE" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_SYMM_SIFT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_SYMM_SIFT_CONV" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW2" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW3" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW4" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW2_CONV" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW3_CONV" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_WINDOW4_CONV" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_GROUP_SIFT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_GROUP_SIFT_CONV" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_ANNEALING" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_GENETIC" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_LINEAR" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_LINEAR_CONVERGE" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_LAZY_SIFT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_REORDER_EXACT" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_ReorderingType" 'enumname))
+
+(cffi:defcenum #.(swig-lispify "Cudd_AggregationType" 'enumname)
+	#.(swig-lispify "CUDD_NO_CHECK" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK2" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK3" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK4" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK5" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK6" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK7" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK8" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_GROUP_CHECK9" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_AggregationType" 'enumname))
+
+(cffi:defcenum #.(swig-lispify "Cudd_HookType" 'enumname)
+	#.(swig-lispify "CUDD_PRE_GC_HOOK" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_POST_GC_HOOK" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_PRE_REORDERING_HOOK" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_POST_REORDERING_HOOK" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_HookType" 'enumname))
+
+(cffi:defcenum #.(swig-lispify "Cudd_ErrorType" 'enumname)
+	#.(swig-lispify "CUDD_NO_ERROR" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_MEMORY_OUT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_TOO_MANY_NODES" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_MAX_MEM_EXCEEDED" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_TIMEOUT_EXPIRED" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_TERMINATION" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_INVALID_ARG" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_INTERNAL_ERROR" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_ErrorType" 'enumname))
+
+(cffi:defcenum #.(swig-lispify "Cudd_LazyGroupType" 'enumname)
+	#.(swig-lispify "CUDD_LAZY_NONE" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_LAZY_SOFT_GROUP" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_LAZY_HARD_GROUP" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_LAZY_UNGROUP" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_LazyGroupType" 'enumname))
+
+(cffi:defcenum #.(swig-lispify "Cudd_VariableType" 'enumname)
+	#.(swig-lispify "CUDD_VAR_PRIMARY_INPUT" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_VAR_PRESENT_STATE" 'enumvalue :keyword)
+	#.(swig-lispify "CUDD_VAR_NEXT_STATE" 'enumvalue :keyword))
+
+(cl:export '#.(swig-lispify "Cudd_VariableType" 'enumname))
+
+(cffi:defcfun ("Cudd_addNewVar" #.(swig-lispify "Cudd_addNewVar" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addNewVar" 'function))
+
+(cffi:defcfun ("Cudd_addNewVarAtLevel" #.(swig-lispify "Cudd_addNewVarAtLevel" 'function)) :pointer
+  (dd :pointer)
+  (level :int))
+
+(cl:export '#.(swig-lispify "Cudd_addNewVarAtLevel" 'function))
+
+(cffi:defcfun ("Cudd_bddNewVar" #.(swig-lispify "Cudd_bddNewVar" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddNewVar" 'function))
+
+(cffi:defcfun ("Cudd_bddNewVarAtLevel" #.(swig-lispify "Cudd_bddNewVarAtLevel" 'function)) :pointer
+  (dd :pointer)
+  (level :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddNewVarAtLevel" 'function))
+
+(cffi:defcfun ("Cudd_bddIsVar" #.(swig-lispify "Cudd_bddIsVar" 'function)) :int
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsVar" 'function))
+
+(cffi:defcfun ("Cudd_addIthVar" #.(swig-lispify "Cudd_addIthVar" 'function)) :pointer
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_addIthVar" 'function))
+
+(cffi:defcfun ("Cudd_bddIthVar" #.(swig-lispify "Cudd_bddIthVar" 'function)) :pointer
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIthVar" 'function))
+
+(cffi:defcfun ("Cudd_zddIthVar" #.(swig-lispify "Cudd_zddIthVar" 'function)) :pointer
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddIthVar" 'function))
+
+(cffi:defcfun ("Cudd_zddVarsFromBddVars" #.(swig-lispify "Cudd_zddVarsFromBddVars" 'function)) :int
+  (dd :pointer)
+  (multiplicity :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddVarsFromBddVars" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxIndex" #.(swig-lispify "Cudd_ReadMaxIndex" 'function)) :unsigned-int)
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxIndex" 'function))
+
+(cffi:defcfun ("Cudd_addConst" #.(swig-lispify "Cudd_addConst" 'function)) :pointer
+  (dd :pointer)
+  (c :double))
+
+(cl:export '#.(swig-lispify "Cudd_addConst" 'function))
+
+(cffi:defcfun ("Cudd_IsConstant" #.(swig-lispify "Cudd_IsConstant" 'function)) :int
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_IsConstant" 'function))
+
+(cffi:defcfun ("Cudd_IsNonConstant" #.(swig-lispify "Cudd_IsNonConstant" 'function)) :int
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_IsNonConstant" 'function))
+
+(cffi:defcfun ("Cudd_T" #.(swig-lispify "Cudd_T" 'function)) :pointer
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_T" 'function))
+
+(cffi:defcfun ("Cudd_E" #.(swig-lispify "Cudd_E" 'function)) :pointer
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_E" 'function))
+
+(cffi:defcfun ("Cudd_V" #.(swig-lispify "Cudd_V" 'function)) :double
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_V" 'function))
+
+(cffi:defcfun ("Cudd_ReadStartTime" #.(swig-lispify "Cudd_ReadStartTime" 'function)) :unsigned-long
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadStartTime" 'function))
+
+(cffi:defcfun ("Cudd_ReadElapsedTime" #.(swig-lispify "Cudd_ReadElapsedTime" 'function)) :unsigned-long
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadElapsedTime" 'function))
+
+(cffi:defcfun ("Cudd_SetStartTime" #.(swig-lispify "Cudd_SetStartTime" 'function)) :void
+  (unique :pointer)
+  (st :unsigned-long))
+
+(cl:export '#.(swig-lispify "Cudd_SetStartTime" 'function))
+
+(cffi:defcfun ("Cudd_ResetStartTime" #.(swig-lispify "Cudd_ResetStartTime" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ResetStartTime" 'function))
+
+(cffi:defcfun ("Cudd_ReadTimeLimit" #.(swig-lispify "Cudd_ReadTimeLimit" 'function)) :unsigned-long
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadTimeLimit" 'function))
+
+(cffi:defcfun ("Cudd_SetTimeLimit" #.(swig-lispify "Cudd_SetTimeLimit" 'function)) :unsigned-long
+  (unique :pointer)
+  (tl :unsigned-long))
+
+(cl:export '#.(swig-lispify "Cudd_SetTimeLimit" 'function))
+
+(cffi:defcfun ("Cudd_UpdateTimeLimit" #.(swig-lispify "Cudd_UpdateTimeLimit" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_UpdateTimeLimit" 'function))
+
+(cffi:defcfun ("Cudd_IncreaseTimeLimit" #.(swig-lispify "Cudd_IncreaseTimeLimit" 'function)) :void
+  (unique :pointer)
+  (increase :unsigned-long))
+
+(cl:export '#.(swig-lispify "Cudd_IncreaseTimeLimit" 'function))
+
+(cffi:defcfun ("Cudd_UnsetTimeLimit" #.(swig-lispify "Cudd_UnsetTimeLimit" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_UnsetTimeLimit" 'function))
+
+(cffi:defcfun ("Cudd_TimeLimited" #.(swig-lispify "Cudd_TimeLimited" 'function)) :int
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_TimeLimited" 'function))
+
+(cffi:defcfun ("Cudd_RegisterTerminationCallback" #.(swig-lispify "Cudd_RegisterTerminationCallback" 'function)) :void
+  (unique :pointer)
+  (callback :pointer)
+  (callback_arg :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_RegisterTerminationCallback" 'function))
+
+(cffi:defcfun ("Cudd_UnregisterTerminationCallback" #.(swig-lispify "Cudd_UnregisterTerminationCallback" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_UnregisterTerminationCallback" 'function))
+
+(cffi:defcfun ("Cudd_RegisterOutOfMemoryCallback" #.(swig-lispify "Cudd_RegisterOutOfMemoryCallback" 'function)) :pointer
+  (unique :pointer)
+  (callback :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_RegisterOutOfMemoryCallback" 'function))
+
+(cffi:defcfun ("Cudd_UnregisterOutOfMemoryCallback" #.(swig-lispify "Cudd_UnregisterOutOfMemoryCallback" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_UnregisterOutOfMemoryCallback" 'function))
+
+(cffi:defcfun ("Cudd_RegisterTimeoutHandler" #.(swig-lispify "Cudd_RegisterTimeoutHandler" 'function)) :void
+  (unique :pointer)
+  (handler :pointer)
+  (arg :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_RegisterTimeoutHandler" 'function))
+
+(cffi:defcfun ("Cudd_ReadTimeoutHandler" #.(swig-lispify "Cudd_ReadTimeoutHandler" 'function)) :pointer
+  (unique :pointer)
+  (argp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadTimeoutHandler" 'function))
+
+(cffi:defcfun ("Cudd_AutodynEnable" #.(swig-lispify "Cudd_AutodynEnable" 'function)) :void
+  (unique :pointer)
+  (method #.(swig-lispify "Cudd_ReorderingType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_AutodynEnable" 'function))
+
+(cffi:defcfun ("Cudd_AutodynDisable" #.(swig-lispify "Cudd_AutodynDisable" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_AutodynDisable" 'function))
+
+(cffi:defcfun ("Cudd_ReorderingStatus" #.(swig-lispify "Cudd_ReorderingStatus" 'function)) :int
+  (unique :pointer)
+  (method :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReorderingStatus" 'function))
+
+(cffi:defcfun ("Cudd_AutodynEnableZdd" #.(swig-lispify "Cudd_AutodynEnableZdd" 'function)) :void
+  (unique :pointer)
+  (method #.(swig-lispify "Cudd_ReorderingType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_AutodynEnableZdd" 'function))
+
+(cffi:defcfun ("Cudd_AutodynDisableZdd" #.(swig-lispify "Cudd_AutodynDisableZdd" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_AutodynDisableZdd" 'function))
+
+(cffi:defcfun ("Cudd_ReorderingStatusZdd" #.(swig-lispify "Cudd_ReorderingStatusZdd" 'function)) :int
+  (unique :pointer)
+  (method :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReorderingStatusZdd" 'function))
+
+(cffi:defcfun ("Cudd_zddRealignmentEnabled" #.(swig-lispify "Cudd_zddRealignmentEnabled" 'function)) :int
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddRealignmentEnabled" 'function))
+
+(cffi:defcfun ("Cudd_zddRealignEnable" #.(swig-lispify "Cudd_zddRealignEnable" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddRealignEnable" 'function))
+
+(cffi:defcfun ("Cudd_zddRealignDisable" #.(swig-lispify "Cudd_zddRealignDisable" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddRealignDisable" 'function))
+
+(cffi:defcfun ("Cudd_bddRealignmentEnabled" #.(swig-lispify "Cudd_bddRealignmentEnabled" 'function)) :int
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddRealignmentEnabled" 'function))
+
+(cffi:defcfun ("Cudd_bddRealignEnable" #.(swig-lispify "Cudd_bddRealignEnable" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddRealignEnable" 'function))
+
+(cffi:defcfun ("Cudd_bddRealignDisable" #.(swig-lispify "Cudd_bddRealignDisable" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddRealignDisable" 'function))
+
+(cffi:defcfun ("Cudd_ReadOne" #.(swig-lispify "Cudd_ReadOne" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadOne" 'function))
+
+(cffi:defcfun ("Cudd_ReadZddOne" #.(swig-lispify "Cudd_ReadZddOne" 'function)) :pointer
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadZddOne" 'function))
+
+(cffi:defcfun ("Cudd_ReadZero" #.(swig-lispify "Cudd_ReadZero" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadZero" 'function))
+
+(cffi:defcfun ("Cudd_ReadLogicZero" #.(swig-lispify "Cudd_ReadLogicZero" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadLogicZero" 'function))
+
+(cffi:defcfun ("Cudd_ReadPlusInfinity" #.(swig-lispify "Cudd_ReadPlusInfinity" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPlusInfinity" 'function))
+
+(cffi:defcfun ("Cudd_ReadMinusInfinity" #.(swig-lispify "Cudd_ReadMinusInfinity" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMinusInfinity" 'function))
+
+(cffi:defcfun ("Cudd_ReadBackground" #.(swig-lispify "Cudd_ReadBackground" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadBackground" 'function))
+
+(cffi:defcfun ("Cudd_SetBackground" #.(swig-lispify "Cudd_SetBackground" 'function)) :void
+  (dd :pointer)
+  (bck :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SetBackground" 'function))
+
+(cffi:defcfun ("Cudd_ReadCacheSlots" #.(swig-lispify "Cudd_ReadCacheSlots" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadCacheSlots" 'function))
+
+(cffi:defcfun ("Cudd_ReadCacheUsedSlots" #.(swig-lispify "Cudd_ReadCacheUsedSlots" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadCacheUsedSlots" 'function))
+
+(cffi:defcfun ("Cudd_ReadCacheLookUps" #.(swig-lispify "Cudd_ReadCacheLookUps" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadCacheLookUps" 'function))
+
+(cffi:defcfun ("Cudd_ReadCacheHits" #.(swig-lispify "Cudd_ReadCacheHits" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadCacheHits" 'function))
+
+(cffi:defcfun ("Cudd_ReadRecursiveCalls" #.(swig-lispify "Cudd_ReadRecursiveCalls" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadRecursiveCalls" 'function))
+
+(cffi:defcfun ("Cudd_ReadMinHit" #.(swig-lispify "Cudd_ReadMinHit" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMinHit" 'function))
+
+(cffi:defcfun ("Cudd_SetMinHit" #.(swig-lispify "Cudd_SetMinHit" 'function)) :void
+  (dd :pointer)
+  (hr :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetMinHit" 'function))
+
+(cffi:defcfun ("Cudd_ReadLooseUpTo" #.(swig-lispify "Cudd_ReadLooseUpTo" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadLooseUpTo" 'function))
+
+(cffi:defcfun ("Cudd_SetLooseUpTo" #.(swig-lispify "Cudd_SetLooseUpTo" 'function)) :void
+  (dd :pointer)
+  (lut :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetLooseUpTo" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxCache" #.(swig-lispify "Cudd_ReadMaxCache" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxCache" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxCacheHard" #.(swig-lispify "Cudd_ReadMaxCacheHard" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxCacheHard" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxCacheHard" #.(swig-lispify "Cudd_SetMaxCacheHard" 'function)) :void
+  (dd :pointer)
+  (mc :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxCacheHard" 'function))
+
+(cffi:defcfun ("Cudd_ReadSize" #.(swig-lispify "Cudd_ReadSize" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSize" 'function))
+
+(cffi:defcfun ("Cudd_ReadZddSize" #.(swig-lispify "Cudd_ReadZddSize" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadZddSize" 'function))
+
+(cffi:defcfun ("Cudd_ReadSlots" #.(swig-lispify "Cudd_ReadSlots" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSlots" 'function))
+
+(cffi:defcfun ("Cudd_ReadUsedSlots" #.(swig-lispify "Cudd_ReadUsedSlots" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadUsedSlots" 'function))
+
+(cffi:defcfun ("Cudd_ExpectedUsedSlots" #.(swig-lispify "Cudd_ExpectedUsedSlots" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ExpectedUsedSlots" 'function))
+
+(cffi:defcfun ("Cudd_ReadKeys" #.(swig-lispify "Cudd_ReadKeys" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadKeys" 'function))
+
+(cffi:defcfun ("Cudd_ReadDead" #.(swig-lispify "Cudd_ReadDead" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadDead" 'function))
+
+(cffi:defcfun ("Cudd_ReadMinDead" #.(swig-lispify "Cudd_ReadMinDead" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMinDead" 'function))
+
+(cffi:defcfun ("Cudd_ReadReorderings" #.(swig-lispify "Cudd_ReadReorderings" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadReorderings" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxReorderings" #.(swig-lispify "Cudd_ReadMaxReorderings" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxReorderings" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxReorderings" #.(swig-lispify "Cudd_SetMaxReorderings" 'function)) :void
+  (dd :pointer)
+  (mr :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxReorderings" 'function))
+
+(cffi:defcfun ("Cudd_ReadReorderingTime" #.(swig-lispify "Cudd_ReadReorderingTime" 'function)) :long
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadReorderingTime" 'function))
+
+(cffi:defcfun ("Cudd_ReadGarbageCollections" #.(swig-lispify "Cudd_ReadGarbageCollections" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadGarbageCollections" 'function))
+
+(cffi:defcfun ("Cudd_ReadGarbageCollectionTime" #.(swig-lispify "Cudd_ReadGarbageCollectionTime" 'function)) :long
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadGarbageCollectionTime" 'function))
+
+(cffi:defcfun ("Cudd_ReadNodesFreed" #.(swig-lispify "Cudd_ReadNodesFreed" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadNodesFreed" 'function))
+
+(cffi:defcfun ("Cudd_ReadNodesDropped" #.(swig-lispify "Cudd_ReadNodesDropped" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadNodesDropped" 'function))
+
+(cffi:defcfun ("Cudd_ReadUniqueLookUps" #.(swig-lispify "Cudd_ReadUniqueLookUps" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadUniqueLookUps" 'function))
+
+(cffi:defcfun ("Cudd_ReadUniqueLinks" #.(swig-lispify "Cudd_ReadUniqueLinks" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadUniqueLinks" 'function))
+
+(cffi:defcfun ("Cudd_ReadSiftMaxVar" #.(swig-lispify "Cudd_ReadSiftMaxVar" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSiftMaxVar" 'function))
+
+(cffi:defcfun ("Cudd_SetSiftMaxVar" #.(swig-lispify "Cudd_SetSiftMaxVar" 'function)) :void
+  (dd :pointer)
+  (smv :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetSiftMaxVar" 'function))
+
+(cffi:defcfun ("Cudd_ReadSiftMaxSwap" #.(swig-lispify "Cudd_ReadSiftMaxSwap" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSiftMaxSwap" 'function))
+
+(cffi:defcfun ("Cudd_SetSiftMaxSwap" #.(swig-lispify "Cudd_SetSiftMaxSwap" 'function)) :void
+  (dd :pointer)
+  (sms :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetSiftMaxSwap" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxGrowth" #.(swig-lispify "Cudd_ReadMaxGrowth" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxGrowth" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxGrowth" #.(swig-lispify "Cudd_SetMaxGrowth" 'function)) :void
+  (dd :pointer)
+  (mg :double))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxGrowth" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxGrowthAlternate" #.(swig-lispify "Cudd_ReadMaxGrowthAlternate" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxGrowthAlternate" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxGrowthAlternate" #.(swig-lispify "Cudd_SetMaxGrowthAlternate" 'function)) :void
+  (dd :pointer)
+  (mg :double))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxGrowthAlternate" 'function))
+
+(cffi:defcfun ("Cudd_ReadReorderingCycle" #.(swig-lispify "Cudd_ReadReorderingCycle" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadReorderingCycle" 'function))
+
+(cffi:defcfun ("Cudd_SetReorderingCycle" #.(swig-lispify "Cudd_SetReorderingCycle" 'function)) :void
+  (dd :pointer)
+  (cycle :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetReorderingCycle" 'function))
+
+(cffi:defcfun ("Cudd_NodeReadIndex" #.(swig-lispify "Cudd_NodeReadIndex" 'function)) :unsigned-int
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_NodeReadIndex" 'function))
+
+(cffi:defcfun ("Cudd_ReadPerm" #.(swig-lispify "Cudd_ReadPerm" 'function)) :int
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPerm" 'function))
+
+(cffi:defcfun ("Cudd_ReadPermZdd" #.(swig-lispify "Cudd_ReadPermZdd" 'function)) :int
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPermZdd" 'function))
+
+(cffi:defcfun ("Cudd_ReadInvPerm" #.(swig-lispify "Cudd_ReadInvPerm" 'function)) :int
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadInvPerm" 'function))
+
+(cffi:defcfun ("Cudd_ReadInvPermZdd" #.(swig-lispify "Cudd_ReadInvPermZdd" 'function)) :int
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadInvPermZdd" 'function))
+
+(cffi:defcfun ("Cudd_ReadVars" #.(swig-lispify "Cudd_ReadVars" 'function)) :pointer
+  (dd :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadVars" 'function))
+
+(cffi:defcfun ("Cudd_ReadEpsilon" #.(swig-lispify "Cudd_ReadEpsilon" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadEpsilon" 'function))
+
+(cffi:defcfun ("Cudd_SetEpsilon" #.(swig-lispify "Cudd_SetEpsilon" 'function)) :void
+  (dd :pointer)
+  (ep :double))
+
+(cl:export '#.(swig-lispify "Cudd_SetEpsilon" 'function))
+
+(cffi:defcfun ("Cudd_ReadGroupcheck" #.(swig-lispify "Cudd_ReadGroupcheck" 'function)) #.(swig-lispify "Cudd_AggregationType" 'enumname)
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadGroupcheck" 'function))
+
+(cffi:defcfun ("Cudd_SetGroupcheck" #.(swig-lispify "Cudd_SetGroupcheck" 'function)) :void
+  (dd :pointer)
+  (gc #.(swig-lispify "Cudd_AggregationType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_SetGroupcheck" 'function))
+
+(cffi:defcfun ("Cudd_GarbageCollectionEnabled" #.(swig-lispify "Cudd_GarbageCollectionEnabled" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_GarbageCollectionEnabled" 'function))
+
+(cffi:defcfun ("Cudd_EnableGarbageCollection" #.(swig-lispify "Cudd_EnableGarbageCollection" 'function)) :void
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_EnableGarbageCollection" 'function))
+
+(cffi:defcfun ("Cudd_DisableGarbageCollection" #.(swig-lispify "Cudd_DisableGarbageCollection" 'function)) :void
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DisableGarbageCollection" 'function))
+
+(cffi:defcfun ("Cudd_DeadAreCounted" #.(swig-lispify "Cudd_DeadAreCounted" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DeadAreCounted" 'function))
+
+(cffi:defcfun ("Cudd_TurnOnCountDead" #.(swig-lispify "Cudd_TurnOnCountDead" 'function)) :void
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_TurnOnCountDead" 'function))
+
+(cffi:defcfun ("Cudd_TurnOffCountDead" #.(swig-lispify "Cudd_TurnOffCountDead" 'function)) :void
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_TurnOffCountDead" 'function))
+
+(cffi:defcfun ("Cudd_ReadRecomb" #.(swig-lispify "Cudd_ReadRecomb" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadRecomb" 'function))
+
+(cffi:defcfun ("Cudd_SetRecomb" #.(swig-lispify "Cudd_SetRecomb" 'function)) :void
+  (dd :pointer)
+  (recomb :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetRecomb" 'function))
+
+(cffi:defcfun ("Cudd_ReadSymmviolation" #.(swig-lispify "Cudd_ReadSymmviolation" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSymmviolation" 'function))
+
+(cffi:defcfun ("Cudd_SetSymmviolation" #.(swig-lispify "Cudd_SetSymmviolation" 'function)) :void
+  (dd :pointer)
+  (symmviolation :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetSymmviolation" 'function))
+
+(cffi:defcfun ("Cudd_ReadArcviolation" #.(swig-lispify "Cudd_ReadArcviolation" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadArcviolation" 'function))
+
+(cffi:defcfun ("Cudd_SetArcviolation" #.(swig-lispify "Cudd_SetArcviolation" 'function)) :void
+  (dd :pointer)
+  (arcviolation :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetArcviolation" 'function))
+
+(cffi:defcfun ("Cudd_ReadPopulationSize" #.(swig-lispify "Cudd_ReadPopulationSize" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPopulationSize" 'function))
+
+(cffi:defcfun ("Cudd_SetPopulationSize" #.(swig-lispify "Cudd_SetPopulationSize" 'function)) :void
+  (dd :pointer)
+  (populationSize :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetPopulationSize" 'function))
+
+(cffi:defcfun ("Cudd_ReadNumberXovers" #.(swig-lispify "Cudd_ReadNumberXovers" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadNumberXovers" 'function))
+
+(cffi:defcfun ("Cudd_SetNumberXovers" #.(swig-lispify "Cudd_SetNumberXovers" 'function)) :void
+  (dd :pointer)
+  (numberXovers :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetNumberXovers" 'function))
+
+(cffi:defcfun ("Cudd_ReadOrderRandomization" #.(swig-lispify "Cudd_ReadOrderRandomization" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadOrderRandomization" 'function))
+
+(cffi:defcfun ("Cudd_SetOrderRandomization" #.(swig-lispify "Cudd_SetOrderRandomization" 'function)) :void
+  (dd :pointer)
+  (factor :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetOrderRandomization" 'function))
+
+(cffi:defcfun ("Cudd_ReadMemoryInUse" #.(swig-lispify "Cudd_ReadMemoryInUse" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMemoryInUse" 'function))
+
+(cffi:defcfun ("Cudd_PrintInfo" #.(swig-lispify "Cudd_PrintInfo" 'function)) :int
+  (dd :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintInfo" 'function))
+
+(cffi:defcfun ("Cudd_ReadPeakNodeCount" #.(swig-lispify "Cudd_ReadPeakNodeCount" 'function)) :long
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPeakNodeCount" 'function))
+
+(cffi:defcfun ("Cudd_ReadPeakLiveNodeCount" #.(swig-lispify "Cudd_ReadPeakLiveNodeCount" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadPeakLiveNodeCount" 'function))
+
+(cffi:defcfun ("Cudd_ReadNodeCount" #.(swig-lispify "Cudd_ReadNodeCount" 'function)) :long
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadNodeCount" 'function))
+
+(cffi:defcfun ("Cudd_zddReadNodeCount" #.(swig-lispify "Cudd_zddReadNodeCount" 'function)) :long
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddReadNodeCount" 'function))
+
+(cffi:defcfun ("Cudd_AddHook" #.(swig-lispify "Cudd_AddHook" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (where #.(swig-lispify "Cudd_HookType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_AddHook" 'function))
+
+(cffi:defcfun ("Cudd_RemoveHook" #.(swig-lispify "Cudd_RemoveHook" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (where #.(swig-lispify "Cudd_HookType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_RemoveHook" 'function))
+
+(cffi:defcfun ("Cudd_IsInHook" #.(swig-lispify "Cudd_IsInHook" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (where #.(swig-lispify "Cudd_HookType" 'enumname)))
+
+(cl:export '#.(swig-lispify "Cudd_IsInHook" 'function))
+
+(cffi:defcfun ("Cudd_StdPreReordHook" #.(swig-lispify "Cudd_StdPreReordHook" 'function)) :int
+  (dd :pointer)
+  (str :string)
+  (data :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_StdPreReordHook" 'function))
+
+(cffi:defcfun ("Cudd_StdPostReordHook" #.(swig-lispify "Cudd_StdPostReordHook" 'function)) :int
+  (dd :pointer)
+  (str :string)
+  (data :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_StdPostReordHook" 'function))
+
+(cffi:defcfun ("Cudd_EnableReorderingReporting" #.(swig-lispify "Cudd_EnableReorderingReporting" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_EnableReorderingReporting" 'function))
+
+(cffi:defcfun ("Cudd_DisableReorderingReporting" #.(swig-lispify "Cudd_DisableReorderingReporting" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DisableReorderingReporting" 'function))
+
+(cffi:defcfun ("Cudd_ReorderingReporting" #.(swig-lispify "Cudd_ReorderingReporting" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReorderingReporting" 'function))
+
+(cffi:defcfun ("Cudd_PrintGroupedOrder" #.(swig-lispify "Cudd_PrintGroupedOrder" 'function)) :int
+  (dd :pointer)
+  (str :string)
+  (data :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintGroupedOrder" 'function))
+
+(cffi:defcfun ("Cudd_EnableOrderingMonitoring" #.(swig-lispify "Cudd_EnableOrderingMonitoring" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_EnableOrderingMonitoring" 'function))
+
+(cffi:defcfun ("Cudd_DisableOrderingMonitoring" #.(swig-lispify "Cudd_DisableOrderingMonitoring" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DisableOrderingMonitoring" 'function))
+
+(cffi:defcfun ("Cudd_OrderingMonitoring" #.(swig-lispify "Cudd_OrderingMonitoring" 'function)) :int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_OrderingMonitoring" 'function))
+
+(cffi:defcfun ("Cudd_SetApplicationHook" #.(swig-lispify "Cudd_SetApplicationHook" 'function)) :void
+  (dd :pointer)
+  (value :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SetApplicationHook" 'function))
+
+(cffi:defcfun ("Cudd_ReadApplicationHook" #.(swig-lispify "Cudd_ReadApplicationHook" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadApplicationHook" 'function))
+
+(cffi:defcfun ("Cudd_ReadErrorCode" #.(swig-lispify "Cudd_ReadErrorCode" 'function)) #.(swig-lispify "Cudd_ErrorType" 'enumname)
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadErrorCode" 'function))
+
+(cffi:defcfun ("Cudd_ClearErrorCode" #.(swig-lispify "Cudd_ClearErrorCode" 'function)) :void
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ClearErrorCode" 'function))
+
+(cffi:defcfun ("Cudd_InstallOutOfMemoryHandler" #.(swig-lispify "Cudd_InstallOutOfMemoryHandler" 'function)) :pointer
+  (newHandler :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_InstallOutOfMemoryHandler" 'function))
+
+(cffi:defcfun ("Cudd_ReadStdout" #.(swig-lispify "Cudd_ReadStdout" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadStdout" 'function))
+
+(cffi:defcfun ("Cudd_SetStdout" #.(swig-lispify "Cudd_SetStdout" 'function)) :void
+  (dd :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SetStdout" 'function))
+
+(cffi:defcfun ("Cudd_ReadStderr" #.(swig-lispify "Cudd_ReadStderr" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadStderr" 'function))
+
+(cffi:defcfun ("Cudd_SetStderr" #.(swig-lispify "Cudd_SetStderr" 'function)) :void
+  (dd :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SetStderr" 'function))
+
+(cffi:defcfun ("Cudd_ReadNextReordering" #.(swig-lispify "Cudd_ReadNextReordering" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadNextReordering" 'function))
+
+(cffi:defcfun ("Cudd_SetNextReordering" #.(swig-lispify "Cudd_SetNextReordering" 'function)) :void
+  (dd :pointer)
+  (next :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetNextReordering" 'function))
+
+(cffi:defcfun ("Cudd_ReadSwapSteps" #.(swig-lispify "Cudd_ReadSwapSteps" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadSwapSteps" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxLive" #.(swig-lispify "Cudd_ReadMaxLive" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxLive" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxLive" #.(swig-lispify "Cudd_SetMaxLive" 'function)) :void
+  (dd :pointer)
+  (maxLive :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxLive" 'function))
+
+(cffi:defcfun ("Cudd_ReadMaxMemory" #.(swig-lispify "Cudd_ReadMaxMemory" 'function)) :unsigned-int
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadMaxMemory" 'function))
+
+(cffi:defcfun ("Cudd_SetMaxMemory" #.(swig-lispify "Cudd_SetMaxMemory" 'function)) :unsigned-int
+  (dd :pointer)
+  (maxMemory :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_SetMaxMemory" 'function))
+
+(cffi:defcfun ("Cudd_bddBindVar" #.(swig-lispify "Cudd_bddBindVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddBindVar" 'function))
+
+(cffi:defcfun ("Cudd_bddUnbindVar" #.(swig-lispify "Cudd_bddUnbindVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddUnbindVar" 'function))
+
+(cffi:defcfun ("Cudd_bddVarIsBound" #.(swig-lispify "Cudd_bddVarIsBound" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddVarIsBound" 'function))
+
+(cffi:defcfun ("Cudd_addExistAbstract" #.(swig-lispify "Cudd_addExistAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addExistAbstract" 'function))
+
+(cffi:defcfun ("Cudd_addUnivAbstract" #.(swig-lispify "Cudd_addUnivAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addUnivAbstract" 'function))
+
+(cffi:defcfun ("Cudd_addOrAbstract" #.(swig-lispify "Cudd_addOrAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addOrAbstract" 'function))
+
+(cffi:defcfun ("Cudd_addApply" #.(swig-lispify "Cudd_addApply" 'function)) :pointer
+  (dd :pointer)
+  (op :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addApply" 'function))
+
+(cffi:defcfun ("Cudd_addPlus" #.(swig-lispify "Cudd_addPlus" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addPlus" 'function))
+
+(cffi:defcfun ("Cudd_addTimes" #.(swig-lispify "Cudd_addTimes" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addTimes" 'function))
+
+(cffi:defcfun ("Cudd_addThreshold" #.(swig-lispify "Cudd_addThreshold" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addThreshold" 'function))
+
+(cffi:defcfun ("Cudd_addSetNZ" #.(swig-lispify "Cudd_addSetNZ" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addSetNZ" 'function))
+
+(cffi:defcfun ("Cudd_addDivide" #.(swig-lispify "Cudd_addDivide" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addDivide" 'function))
+
+(cffi:defcfun ("Cudd_addMinus" #.(swig-lispify "Cudd_addMinus" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addMinus" 'function))
+
+(cffi:defcfun ("Cudd_addMinimum" #.(swig-lispify "Cudd_addMinimum" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addMinimum" 'function))
+
+(cffi:defcfun ("Cudd_addMaximum" #.(swig-lispify "Cudd_addMaximum" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addMaximum" 'function))
+
+(cffi:defcfun ("Cudd_addOneZeroMaximum" #.(swig-lispify "Cudd_addOneZeroMaximum" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addOneZeroMaximum" 'function))
+
+(cffi:defcfun ("Cudd_addDiff" #.(swig-lispify "Cudd_addDiff" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addDiff" 'function))
+
+(cffi:defcfun ("Cudd_addAgreement" #.(swig-lispify "Cudd_addAgreement" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addAgreement" 'function))
+
+(cffi:defcfun ("Cudd_addOr" #.(swig-lispify "Cudd_addOr" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addOr" 'function))
+
+(cffi:defcfun ("Cudd_addNand" #.(swig-lispify "Cudd_addNand" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addNand" 'function))
+
+(cffi:defcfun ("Cudd_addNor" #.(swig-lispify "Cudd_addNor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addNor" 'function))
+
+(cffi:defcfun ("Cudd_addXor" #.(swig-lispify "Cudd_addXor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addXor" 'function))
+
+(cffi:defcfun ("Cudd_addXnor" #.(swig-lispify "Cudd_addXnor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addXnor" 'function))
+
+(cffi:defcfun ("Cudd_addMonadicApply" #.(swig-lispify "Cudd_addMonadicApply" 'function)) :pointer
+  (dd :pointer)
+  (op :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addMonadicApply" 'function))
+
+(cffi:defcfun ("Cudd_addLog" #.(swig-lispify "Cudd_addLog" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addLog" 'function))
+
+(cffi:defcfun ("Cudd_addFindMax" #.(swig-lispify "Cudd_addFindMax" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addFindMax" 'function))
+
+(cffi:defcfun ("Cudd_addFindMin" #.(swig-lispify "Cudd_addFindMin" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addFindMin" 'function))
+
+(cffi:defcfun ("Cudd_addIthBit" #.(swig-lispify "Cudd_addIthBit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (bit :int))
+
+(cl:export '#.(swig-lispify "Cudd_addIthBit" 'function))
+
+(cffi:defcfun ("Cudd_addScalarInverse" #.(swig-lispify "Cudd_addScalarInverse" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (epsilon :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addScalarInverse" 'function))
+
+(cffi:defcfun ("Cudd_addIte" #.(swig-lispify "Cudd_addIte" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addIte" 'function))
+
+(cffi:defcfun ("Cudd_addIteConstant" #.(swig-lispify "Cudd_addIteConstant" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addIteConstant" 'function))
+
+(cffi:defcfun ("Cudd_addEvalConst" #.(swig-lispify "Cudd_addEvalConst" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addEvalConst" 'function))
+
+(cffi:defcfun ("Cudd_addLeq" #.(swig-lispify "Cudd_addLeq" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addLeq" 'function))
+
+(cffi:defcfun ("Cudd_addCmpl" #.(swig-lispify "Cudd_addCmpl" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addCmpl" 'function))
+
+(cffi:defcfun ("Cudd_addNegate" #.(swig-lispify "Cudd_addNegate" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addNegate" 'function))
+
+(cffi:defcfun ("Cudd_addRoundOff" #.(swig-lispify "Cudd_addRoundOff" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (N :int))
+
+(cl:export '#.(swig-lispify "Cudd_addRoundOff" 'function))
+
+(cffi:defcfun ("Cudd_addWalsh" #.(swig-lispify "Cudd_addWalsh" 'function)) :pointer
+  (dd :pointer)
+  (x :pointer)
+  (y :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_addWalsh" 'function))
+
+(cffi:defcfun ("Cudd_addResidue" #.(swig-lispify "Cudd_addResidue" 'function)) :pointer
+  (dd :pointer)
+  (n :int)
+  (m :int)
+  (options :int)
+  (top :int))
+
+(cl:export '#.(swig-lispify "Cudd_addResidue" 'function))
+
+(cffi:defcfun ("Cudd_bddAndAbstract" #.(swig-lispify "Cudd_bddAndAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (g :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddAndAbstract" 'function))
+
+(cffi:defcfun ("Cudd_bddAndAbstractLimit" #.(swig-lispify "Cudd_bddAndAbstractLimit" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (g :pointer)
+  (cube :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddAndAbstractLimit" 'function))
+
+(cffi:defcfun ("Cudd_ApaNumberOfDigits" #.(swig-lispify "Cudd_ApaNumberOfDigits" 'function)) :int
+  (binaryDigits :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaNumberOfDigits" 'function))
+
+(cffi:defcfun ("Cudd_NewApaNumber" #.(swig-lispify "Cudd_NewApaNumber" 'function)) :pointer
+  (digits :int))
+
+(cl:export '#.(swig-lispify "Cudd_NewApaNumber" 'function))
+
+(cffi:defcfun ("Cudd_FreeApaNumber" #.(swig-lispify "Cudd_FreeApaNumber" 'function)) :void
+  (number :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FreeApaNumber" 'function))
+
+(cffi:defcfun ("Cudd_ApaCopy" #.(swig-lispify "Cudd_ApaCopy" 'function)) :void
+  (digits :int)
+  (source :pointer)
+  (dest :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaCopy" 'function))
+
+(cffi:defcfun ("Cudd_ApaAdd" #.(swig-lispify "Cudd_ApaAdd" 'function)) :pointer
+  (digits :int)
+  (a :pointer)
+  (b :pointer)
+  (sum :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaAdd" 'function))
+
+(cffi:defcfun ("Cudd_ApaSubtract" #.(swig-lispify "Cudd_ApaSubtract" 'function)) :pointer
+  (digits :int)
+  (a :pointer)
+  (b :pointer)
+  (diff :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaSubtract" 'function))
+
+(cffi:defcfun ("Cudd_ApaShortDivision" #.(swig-lispify "Cudd_ApaShortDivision" 'function)) :pointer
+  (digits :int)
+  (dividend :pointer)
+  (divisor :pointer)
+  (quotient :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaShortDivision" 'function))
+
+(cffi:defcfun ("Cudd_ApaIntDivision" #.(swig-lispify "Cudd_ApaIntDivision" 'function)) :unsigned-int
+  (digits :int)
+  (dividend :pointer)
+  (divisor :unsigned-int)
+  (quotient :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaIntDivision" 'function))
+
+(cffi:defcfun ("Cudd_ApaShiftRight" #.(swig-lispify "Cudd_ApaShiftRight" 'function)) :void
+  (digits :int)
+  (in :pointer)
+  (a :pointer)
+  (b :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaShiftRight" 'function))
+
+(cffi:defcfun ("Cudd_ApaSetToLiteral" #.(swig-lispify "Cudd_ApaSetToLiteral" 'function)) :void
+  (digits :int)
+  (number :pointer)
+  (literal :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaSetToLiteral" 'function))
+
+(cffi:defcfun ("Cudd_ApaPowerOfTwo" #.(swig-lispify "Cudd_ApaPowerOfTwo" 'function)) :void
+  (digits :int)
+  (number :pointer)
+  (power :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPowerOfTwo" 'function))
+
+(cffi:defcfun ("Cudd_ApaCompare" #.(swig-lispify "Cudd_ApaCompare" 'function)) :int
+  (digitsFirst :int)
+  (first :pointer)
+  (digitsSecond :int)
+  (second :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaCompare" 'function))
+
+(cffi:defcfun ("Cudd_ApaCompareRatios" #.(swig-lispify "Cudd_ApaCompareRatios" 'function)) :int
+  (digitsFirst :int)
+  (firstNum :pointer)
+  (firstDen :unsigned-int)
+  (digitsSecond :int)
+  (secondNum :pointer)
+  (secondDen :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaCompareRatios" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintHex" #.(swig-lispify "Cudd_ApaPrintHex" 'function)) :int
+  (fp :pointer)
+  (digits :int)
+  (number :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintHex" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintDecimal" #.(swig-lispify "Cudd_ApaPrintDecimal" 'function)) :int
+  (fp :pointer)
+  (digits :int)
+  (number :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintDecimal" 'function))
+
+(cffi:defcfun ("Cudd_ApaStringDecimal" #.(swig-lispify "Cudd_ApaStringDecimal" 'function)) :string
+  (digits :int)
+  (number :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaStringDecimal" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintExponential" #.(swig-lispify "Cudd_ApaPrintExponential" 'function)) :int
+  (fp :pointer)
+  (digits :int)
+  (number :pointer)
+  (precision :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintExponential" 'function))
+
+(cffi:defcfun ("Cudd_ApaCountMinterm" #.(swig-lispify "Cudd_ApaCountMinterm" 'function)) :pointer
+  (manager :pointer)
+  (node :pointer)
+  (nvars :int)
+  (digits :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ApaCountMinterm" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintMinterm" #.(swig-lispify "Cudd_ApaPrintMinterm" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (node :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintMinterm" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintMintermExp" #.(swig-lispify "Cudd_ApaPrintMintermExp" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (node :pointer)
+  (nvars :int)
+  (precision :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintMintermExp" 'function))
+
+(cffi:defcfun ("Cudd_ApaPrintDensity" #.(swig-lispify "Cudd_ApaPrintDensity" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (node :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_ApaPrintDensity" 'function))
+
+(cffi:defcfun ("Cudd_UnderApprox" #.(swig-lispify "Cudd_UnderApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (safe :int)
+  (quality :double))
+
+(cl:export '#.(swig-lispify "Cudd_UnderApprox" 'function))
+
+(cffi:defcfun ("Cudd_OverApprox" #.(swig-lispify "Cudd_OverApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (safe :int)
+  (quality :double))
+
+(cl:export '#.(swig-lispify "Cudd_OverApprox" 'function))
+
+(cffi:defcfun ("Cudd_RemapUnderApprox" #.(swig-lispify "Cudd_RemapUnderApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (quality :double))
+
+(cl:export '#.(swig-lispify "Cudd_RemapUnderApprox" 'function))
+
+(cffi:defcfun ("Cudd_RemapOverApprox" #.(swig-lispify "Cudd_RemapOverApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (quality :double))
+
+(cl:export '#.(swig-lispify "Cudd_RemapOverApprox" 'function))
+
+(cffi:defcfun ("Cudd_BiasedUnderApprox" #.(swig-lispify "Cudd_BiasedUnderApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (b :pointer)
+  (numVars :int)
+  (threshold :int)
+  (quality1 :double)
+  (quality0 :double))
+
+(cl:export '#.(swig-lispify "Cudd_BiasedUnderApprox" 'function))
+
+(cffi:defcfun ("Cudd_BiasedOverApprox" #.(swig-lispify "Cudd_BiasedOverApprox" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (b :pointer)
+  (numVars :int)
+  (threshold :int)
+  (quality1 :double)
+  (quality0 :double))
+
+(cl:export '#.(swig-lispify "Cudd_BiasedOverApprox" 'function))
+
+(cffi:defcfun ("Cudd_bddExistAbstract" #.(swig-lispify "Cudd_bddExistAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddExistAbstract" 'function))
+
+(cffi:defcfun ("Cudd_bddExistAbstractLimit" #.(swig-lispify "Cudd_bddExistAbstractLimit" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddExistAbstractLimit" 'function))
+
+(cffi:defcfun ("Cudd_bddXorExistAbstract" #.(swig-lispify "Cudd_bddXorExistAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (g :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddXorExistAbstract" 'function))
+
+(cffi:defcfun ("Cudd_bddUnivAbstract" #.(swig-lispify "Cudd_bddUnivAbstract" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddUnivAbstract" 'function))
+
+(cffi:defcfun ("Cudd_bddBooleanDiff" #.(swig-lispify "Cudd_bddBooleanDiff" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (x :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddBooleanDiff" 'function))
+
+(cffi:defcfun ("Cudd_bddVarIsDependent" #.(swig-lispify "Cudd_bddVarIsDependent" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (var :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddVarIsDependent" 'function))
+
+(cffi:defcfun ("Cudd_bddCorrelation" #.(swig-lispify "Cudd_bddCorrelation" 'function)) :double
+  (manager :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddCorrelation" 'function))
+
+(cffi:defcfun ("Cudd_bddCorrelationWeights" #.(swig-lispify "Cudd_bddCorrelationWeights" 'function)) :double
+  (manager :pointer)
+  (f :pointer)
+  (g :pointer)
+  (prob :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddCorrelationWeights" 'function))
+
+(cffi:defcfun ("Cudd_bddIte" #.(swig-lispify "Cudd_bddIte" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIte" 'function))
+
+(cffi:defcfun ("Cudd_bddIteLimit" #.(swig-lispify "Cudd_bddIteLimit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIteLimit" 'function))
+
+(cffi:defcfun ("Cudd_bddIteConstant" #.(swig-lispify "Cudd_bddIteConstant" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIteConstant" 'function))
+
+(cffi:defcfun ("Cudd_bddIntersect" #.(swig-lispify "Cudd_bddIntersect" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIntersect" 'function))
+
+(cffi:defcfun ("Cudd_bddAnd" #.(swig-lispify "Cudd_bddAnd" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddAnd" 'function))
+
+(cffi:defcfun ("Cudd_bddAndLimit" #.(swig-lispify "Cudd_bddAndLimit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddAndLimit" 'function))
+
+(cffi:defcfun ("Cudd_bddOr" #.(swig-lispify "Cudd_bddOr" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddOr" 'function))
+
+(cffi:defcfun ("Cudd_bddOrLimit" #.(swig-lispify "Cudd_bddOrLimit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddOrLimit" 'function))
+
+(cffi:defcfun ("Cudd_bddNand" #.(swig-lispify "Cudd_bddNand" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddNand" 'function))
+
+(cffi:defcfun ("Cudd_bddNor" #.(swig-lispify "Cudd_bddNor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddNor" 'function))
+
+(cffi:defcfun ("Cudd_bddXor" #.(swig-lispify "Cudd_bddXor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddXor" 'function))
+
+(cffi:defcfun ("Cudd_bddXnor" #.(swig-lispify "Cudd_bddXnor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddXnor" 'function))
+
+(cffi:defcfun ("Cudd_bddXnorLimit" #.(swig-lispify "Cudd_bddXnorLimit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (limit :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddXnorLimit" 'function))
+
+(cffi:defcfun ("Cudd_bddLeq" #.(swig-lispify "Cudd_bddLeq" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddLeq" 'function))
+
+(cffi:defcfun ("Cudd_addBddThreshold" #.(swig-lispify "Cudd_addBddThreshold" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (value :double))
+
+(cl:export '#.(swig-lispify "Cudd_addBddThreshold" 'function))
+
+(cffi:defcfun ("Cudd_addBddStrictThreshold" #.(swig-lispify "Cudd_addBddStrictThreshold" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (value :double))
+
+(cl:export '#.(swig-lispify "Cudd_addBddStrictThreshold" 'function))
+
+(cffi:defcfun ("Cudd_addBddInterval" #.(swig-lispify "Cudd_addBddInterval" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (lower :double)
+  (upper :double))
+
+(cl:export '#.(swig-lispify "Cudd_addBddInterval" 'function))
+
+(cffi:defcfun ("Cudd_addBddIthBit" #.(swig-lispify "Cudd_addBddIthBit" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (bit :int))
+
+(cl:export '#.(swig-lispify "Cudd_addBddIthBit" 'function))
+
+(cffi:defcfun ("Cudd_BddToAdd" #.(swig-lispify "Cudd_BddToAdd" 'function)) :pointer
+  (dd :pointer)
+  (B :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_BddToAdd" 'function))
+
+(cffi:defcfun ("Cudd_addBddPattern" #.(swig-lispify "Cudd_addBddPattern" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addBddPattern" 'function))
+
+(cffi:defcfun ("Cudd_bddTransfer" #.(swig-lispify "Cudd_bddTransfer" 'function)) :pointer
+  (ddSource :pointer)
+  (ddDestination :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddTransfer" 'function))
+
+(cffi:defcfun ("Cudd_DebugCheck" #.(swig-lispify "Cudd_DebugCheck" 'function)) :int
+  (table :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DebugCheck" 'function))
+
+(cffi:defcfun ("Cudd_CheckKeys" #.(swig-lispify "Cudd_CheckKeys" 'function)) :int
+  (table :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CheckKeys" 'function))
+
+(cffi:defcfun ("Cudd_bddClippingAnd" #.(swig-lispify "Cudd_bddClippingAnd" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (maxDepth :int)
+  (direction :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddClippingAnd" 'function))
+
+(cffi:defcfun ("Cudd_bddClippingAndAbstract" #.(swig-lispify "Cudd_bddClippingAndAbstract" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (cube :pointer)
+  (maxDepth :int)
+  (direction :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddClippingAndAbstract" 'function))
+
+(cffi:defcfun ("Cudd_Cofactor" #.(swig-lispify "Cudd_Cofactor" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Cofactor" 'function))
+
+(cffi:defcfun ("Cudd_CheckCube" #.(swig-lispify "Cudd_CheckCube" 'function)) :int
+  (dd :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CheckCube" 'function))
+
+(cffi:defcfun ("Cudd_VarsAreSymmetric" #.(swig-lispify "Cudd_VarsAreSymmetric" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (index1 :int)
+  (index2 :int))
+
+(cl:export '#.(swig-lispify "Cudd_VarsAreSymmetric" 'function))
+
+(cffi:defcfun ("Cudd_bddCompose" #.(swig-lispify "Cudd_bddCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (v :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddCompose" 'function))
+
+(cffi:defcfun ("Cudd_addCompose" #.(swig-lispify "Cudd_addCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (v :int))
+
+(cl:export '#.(swig-lispify "Cudd_addCompose" 'function))
+
+(cffi:defcfun ("Cudd_addPermute" #.(swig-lispify "Cudd_addPermute" 'function)) :pointer
+  (manager :pointer)
+  (node :pointer)
+  (permut :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addPermute" 'function))
+
+(cffi:defcfun ("Cudd_addSwapVariables" #.(swig-lispify "Cudd_addSwapVariables" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (x :pointer)
+  (y :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_addSwapVariables" 'function))
+
+(cffi:defcfun ("Cudd_bddPermute" #.(swig-lispify "Cudd_bddPermute" 'function)) :pointer
+  (manager :pointer)
+  (node :pointer)
+  (permut :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddPermute" 'function))
+
+(cffi:defcfun ("Cudd_bddVarMap" #.(swig-lispify "Cudd_bddVarMap" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddVarMap" 'function))
+
+(cffi:defcfun ("Cudd_SetVarMap" #.(swig-lispify "Cudd_SetVarMap" 'function)) :int
+  (manager :pointer)
+  (x :pointer)
+  (y :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_SetVarMap" 'function))
+
+(cffi:defcfun ("Cudd_bddSwapVariables" #.(swig-lispify "Cudd_bddSwapVariables" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (x :pointer)
+  (y :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSwapVariables" 'function))
+
+(cffi:defcfun ("Cudd_bddAdjPermuteX" #.(swig-lispify "Cudd_bddAdjPermuteX" 'function)) :pointer
+  (dd :pointer)
+  (B :pointer)
+  (x :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddAdjPermuteX" 'function))
+
+(cffi:defcfun ("Cudd_addVectorCompose" #.(swig-lispify "Cudd_addVectorCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vector :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addVectorCompose" 'function))
+
+(cffi:defcfun ("Cudd_addGeneralVectorCompose" #.(swig-lispify "Cudd_addGeneralVectorCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vectorOn :pointer)
+  (vectorOff :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addGeneralVectorCompose" 'function))
+
+(cffi:defcfun ("Cudd_addNonSimCompose" #.(swig-lispify "Cudd_addNonSimCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vector :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addNonSimCompose" 'function))
+
+(cffi:defcfun ("Cudd_bddVectorCompose" #.(swig-lispify "Cudd_bddVectorCompose" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vector :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddVectorCompose" 'function))
+
+(cffi:defcfun ("Cudd_bddApproxConjDecomp" #.(swig-lispify "Cudd_bddApproxConjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (conjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddApproxConjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddApproxDisjDecomp" #.(swig-lispify "Cudd_bddApproxDisjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (disjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddApproxDisjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddIterConjDecomp" #.(swig-lispify "Cudd_bddIterConjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (conjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIterConjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddIterDisjDecomp" #.(swig-lispify "Cudd_bddIterDisjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (disjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIterDisjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddGenConjDecomp" #.(swig-lispify "Cudd_bddGenConjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (conjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddGenConjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddGenDisjDecomp" #.(swig-lispify "Cudd_bddGenDisjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (disjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddGenDisjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddVarConjDecomp" #.(swig-lispify "Cudd_bddVarConjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (conjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddVarConjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_bddVarDisjDecomp" #.(swig-lispify "Cudd_bddVarDisjDecomp" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (disjuncts :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddVarDisjDecomp" 'function))
+
+(cffi:defcfun ("Cudd_FindEssential" #.(swig-lispify "Cudd_FindEssential" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FindEssential" 'function))
+
+(cffi:defcfun ("Cudd_bddIsVarEssential" #.(swig-lispify "Cudd_bddIsVarEssential" 'function)) :int
+  (manager :pointer)
+  (f :pointer)
+  (id :int)
+  (phase :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsVarEssential" 'function))
+
+(cffi:defcfun ("Cudd_FindTwoLiteralClauses" #.(swig-lispify "Cudd_FindTwoLiteralClauses" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FindTwoLiteralClauses" 'function))
+
+(cffi:defcfun ("Cudd_PrintTwoLiteralClauses" #.(swig-lispify "Cudd_PrintTwoLiteralClauses" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (names :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintTwoLiteralClauses" 'function))
+
+(cffi:defcfun ("Cudd_ReadIthClause" #.(swig-lispify "Cudd_ReadIthClause" 'function)) :int
+  (tlc :pointer)
+  (i :int)
+  (var1 :pointer)
+  (var2 :pointer)
+  (phase1 :pointer)
+  (phase2 :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ReadIthClause" 'function))
+
+(cffi:defcfun ("Cudd_tlcInfoFree" #.(swig-lispify "Cudd_tlcInfoFree" 'function)) :void
+  (t_arg0 :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_tlcInfoFree" 'function))
+
+(cffi:defcfun ("Cudd_DumpBlif" #.(swig-lispify "Cudd_DumpBlif" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (mname :string)
+  (fp :pointer)
+  (mv :int))
+
+(cl:export '#.(swig-lispify "Cudd_DumpBlif" 'function))
+
+(cffi:defcfun ("Cudd_DumpBlifBody" #.(swig-lispify "Cudd_DumpBlifBody" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer)
+  (mv :int))
+
+(cl:export '#.(swig-lispify "Cudd_DumpBlifBody" 'function))
+
+(cffi:defcfun ("Cudd_DumpDot" #.(swig-lispify "Cudd_DumpDot" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DumpDot" 'function))
+
+(cffi:defcfun ("Cudd_DumpDaVinci" #.(swig-lispify "Cudd_DumpDaVinci" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DumpDaVinci" 'function))
+
+(cffi:defcfun ("Cudd_DumpDDcal" #.(swig-lispify "Cudd_DumpDDcal" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DumpDDcal" 'function))
+
+(cffi:defcfun ("Cudd_DumpFactoredForm" #.(swig-lispify "Cudd_DumpFactoredForm" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DumpFactoredForm" 'function))
+
+(cffi:defcfun ("Cudd_FactoredFormString" #.(swig-lispify "Cudd_FactoredFormString" 'function)) :string
+  (dd :pointer)
+  (f :pointer)
+  (inames :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FactoredFormString" 'function))
+
+(cffi:defcfun ("Cudd_bddConstrain" #.(swig-lispify "Cudd_bddConstrain" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddConstrain" 'function))
+
+(cffi:defcfun ("Cudd_bddRestrict" #.(swig-lispify "Cudd_bddRestrict" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddRestrict" 'function))
+
+(cffi:defcfun ("Cudd_bddNPAnd" #.(swig-lispify "Cudd_bddNPAnd" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddNPAnd" 'function))
+
+(cffi:defcfun ("Cudd_addConstrain" #.(swig-lispify "Cudd_addConstrain" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addConstrain" 'function))
+
+(cffi:defcfun ("Cudd_bddConstrainDecomp" #.(swig-lispify "Cudd_bddConstrainDecomp" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddConstrainDecomp" 'function))
+
+(cffi:defcfun ("Cudd_addRestrict" #.(swig-lispify "Cudd_addRestrict" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addRestrict" 'function))
+
+(cffi:defcfun ("Cudd_bddCharToVect" #.(swig-lispify "Cudd_bddCharToVect" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddCharToVect" 'function))
+
+(cffi:defcfun ("Cudd_bddLICompaction" #.(swig-lispify "Cudd_bddLICompaction" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddLICompaction" 'function))
+
+(cffi:defcfun ("Cudd_bddSqueeze" #.(swig-lispify "Cudd_bddSqueeze" 'function)) :pointer
+  (dd :pointer)
+  (l :pointer)
+  (u :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddSqueeze" 'function))
+
+(cffi:defcfun ("Cudd_bddInterpolate" #.(swig-lispify "Cudd_bddInterpolate" 'function)) :pointer
+  (dd :pointer)
+  (l :pointer)
+  (u :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddInterpolate" 'function))
+
+(cffi:defcfun ("Cudd_bddMinimize" #.(swig-lispify "Cudd_bddMinimize" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddMinimize" 'function))
+
+(cffi:defcfun ("Cudd_SubsetCompress" #.(swig-lispify "Cudd_SubsetCompress" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (nvars :int)
+  (threshold :int))
+
+(cl:export '#.(swig-lispify "Cudd_SubsetCompress" 'function))
+
+(cffi:defcfun ("Cudd_SupersetCompress" #.(swig-lispify "Cudd_SupersetCompress" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (nvars :int)
+  (threshold :int))
+
+(cl:export '#.(swig-lispify "Cudd_SupersetCompress" 'function))
+
+(cffi:defcfun ("Cudd_addHarwell" #.(swig-lispify "Cudd_addHarwell" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (E :pointer)
+  (x :pointer)
+  (y :pointer)
+  (xn :pointer)
+  (yn_ :pointer)
+  (nx :pointer)
+  (ny :pointer)
+  (m :pointer)
+  (n :pointer)
+  (bx :int)
+  (sx :int)
+  (by :int)
+  (sy :int)
+  (pr :int))
+
+(cl:export '#.(swig-lispify "Cudd_addHarwell" 'function))
+
+(cffi:defcfun ("Cudd_Init" #.(swig-lispify "Cudd_Init" 'function)) :pointer
+  (numVars :unsigned-int)
+  (numVarsZ :unsigned-int)
+  (numSlots :unsigned-int)
+  (cacheSize :unsigned-int)
+  (maxMemory :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_Init" 'function))
+
+(cffi:defcfun ("Cudd_Quit" #.(swig-lispify "Cudd_Quit" 'function)) :void
+  (unique :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Quit" 'function))
+
+(cffi:defcfun ("Cudd_PrintLinear" #.(swig-lispify "Cudd_PrintLinear" 'function)) :int
+  (table :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintLinear" 'function))
+
+(cffi:defcfun ("Cudd_ReadLinear" #.(swig-lispify "Cudd_ReadLinear" 'function)) :int
+  (table :pointer)
+  (x :int)
+  (y :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReadLinear" 'function))
+
+(cffi:defcfun ("Cudd_bddLiteralSetIntersection" #.(swig-lispify "Cudd_bddLiteralSetIntersection" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddLiteralSetIntersection" 'function))
+
+(cffi:defcfun ("Cudd_addMatrixMultiply" #.(swig-lispify "Cudd_addMatrixMultiply" 'function)) :pointer
+  (dd :pointer)
+  (A :pointer)
+  (B :pointer)
+  (z :pointer)
+  (nz :int))
+
+(cl:export '#.(swig-lispify "Cudd_addMatrixMultiply" 'function))
+
+(cffi:defcfun ("Cudd_addTimesPlus" #.(swig-lispify "Cudd_addTimesPlus" 'function)) :pointer
+  (dd :pointer)
+  (A :pointer)
+  (B :pointer)
+  (z :pointer)
+  (nz :int))
+
+(cl:export '#.(swig-lispify "Cudd_addTimesPlus" 'function))
+
+(cffi:defcfun ("Cudd_addTriangle" #.(swig-lispify "Cudd_addTriangle" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (z :pointer)
+  (nz :int))
+
+(cl:export '#.(swig-lispify "Cudd_addTriangle" 'function))
+
+(cffi:defcfun ("Cudd_addOuterSum" #.(swig-lispify "Cudd_addOuterSum" 'function)) :pointer
+  (dd :pointer)
+  (M :pointer)
+  (r :pointer)
+  (c :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addOuterSum" 'function))
+
+(cffi:defcfun ("Cudd_PrioritySelect" #.(swig-lispify "Cudd_PrioritySelect" 'function)) :pointer
+  (dd :pointer)
+  (R :pointer)
+  (x :pointer)
+  (y :pointer)
+  (z :pointer)
+  (Pi :pointer)
+  (n :int)
+  (PiFunc :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrioritySelect" 'function))
+
+(cffi:defcfun ("Cudd_Xgty" #.(swig-lispify "Cudd_Xgty" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (z :pointer)
+  (x :pointer)
+  (y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Xgty" 'function))
+
+(cffi:defcfun ("Cudd_Xeqy" #.(swig-lispify "Cudd_Xeqy" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (x :pointer)
+  (y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Xeqy" 'function))
+
+(cffi:defcfun ("Cudd_addXeqy" #.(swig-lispify "Cudd_addXeqy" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (x :pointer)
+  (y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_addXeqy" 'function))
+
+(cffi:defcfun ("Cudd_Dxygtdxz" #.(swig-lispify "Cudd_Dxygtdxz" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (x :pointer)
+  (y :pointer)
+  (z :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Dxygtdxz" 'function))
+
+(cffi:defcfun ("Cudd_Dxygtdyz" #.(swig-lispify "Cudd_Dxygtdyz" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (x :pointer)
+  (y :pointer)
+  (z :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Dxygtdyz" 'function))
+
+(cffi:defcfun ("Cudd_Inequality" #.(swig-lispify "Cudd_Inequality" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (c :int)
+  (x :pointer)
+  (y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Inequality" 'function))
+
+(cffi:defcfun ("Cudd_Disequality" #.(swig-lispify "Cudd_Disequality" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (c :int)
+  (x :pointer)
+  (y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Disequality" 'function))
+
+(cffi:defcfun ("Cudd_bddInterval" #.(swig-lispify "Cudd_bddInterval" 'function)) :pointer
+  (dd :pointer)
+  (N :int)
+  (x :pointer)
+  (lowerB :unsigned-int)
+  (upperB :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_bddInterval" 'function))
+
+(cffi:defcfun ("Cudd_CProjection" #.(swig-lispify "Cudd_CProjection" 'function)) :pointer
+  (dd :pointer)
+  (R :pointer)
+  (Y :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CProjection" 'function))
+
+(cffi:defcfun ("Cudd_addHamming" #.(swig-lispify "Cudd_addHamming" 'function)) :pointer
+  (dd :pointer)
+  (xVars :pointer)
+  (yVars :pointer)
+  (nVars :int))
+
+(cl:export '#.(swig-lispify "Cudd_addHamming" 'function))
+
+(cffi:defcfun ("Cudd_MinHammingDist" #.(swig-lispify "Cudd_MinHammingDist" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (minterm :pointer)
+  (upperBound :int))
+
+(cl:export '#.(swig-lispify "Cudd_MinHammingDist" 'function))
+
+(cffi:defcfun ("Cudd_bddClosestCube" #.(swig-lispify "Cudd_bddClosestCube" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (distance :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddClosestCube" 'function))
+
+(cffi:defcfun ("Cudd_addRead" #.(swig-lispify "Cudd_addRead" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (E :pointer)
+  (x :pointer)
+  (y :pointer)
+  (xn :pointer)
+  (yn_ :pointer)
+  (nx :pointer)
+  (ny :pointer)
+  (m :pointer)
+  (n :pointer)
+  (bx :int)
+  (sx :int)
+  (by :int)
+  (sy :int))
+
+(cl:export '#.(swig-lispify "Cudd_addRead" 'function))
+
+(cffi:defcfun ("Cudd_bddRead" #.(swig-lispify "Cudd_bddRead" 'function)) :int
+  (fp :pointer)
+  (dd :pointer)
+  (E :pointer)
+  (x :pointer)
+  (y :pointer)
+  (nx :pointer)
+  (ny :pointer)
+  (m :pointer)
+  (n :pointer)
+  (bx :int)
+  (sx :int)
+  (by :int)
+  (sy :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddRead" 'function))
+
+(cffi:defcfun ("Cudd_Ref" #.(swig-lispify "Cudd_Ref" 'function)) :void
+  (n :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Ref" 'function))
+
+(cffi:defcfun ("Cudd_RecursiveDeref" #.(swig-lispify "Cudd_RecursiveDeref" 'function)) :void
+  (table :pointer)
+  (n :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_RecursiveDeref" 'function))
+
+(cffi:defcfun ("Cudd_IterDerefBdd" #.(swig-lispify "Cudd_IterDerefBdd" 'function)) :void
+  (table :pointer)
+  (n :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_IterDerefBdd" 'function))
+
+(cffi:defcfun ("Cudd_DelayedDerefBdd" #.(swig-lispify "Cudd_DelayedDerefBdd" 'function)) :void
+  (table :pointer)
+  (n :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DelayedDerefBdd" 'function))
+
+(cffi:defcfun ("Cudd_RecursiveDerefZdd" #.(swig-lispify "Cudd_RecursiveDerefZdd" 'function)) :void
+  (table :pointer)
+  (n :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_RecursiveDerefZdd" 'function))
+
+(cffi:defcfun ("Cudd_Deref" #.(swig-lispify "Cudd_Deref" 'function)) :void
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Deref" 'function))
+
+(cffi:defcfun ("Cudd_CheckZeroRef" #.(swig-lispify "Cudd_CheckZeroRef" 'function)) :int
+  (manager :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CheckZeroRef" 'function))
+
+(cffi:defcfun ("Cudd_ReduceHeap" #.(swig-lispify "Cudd_ReduceHeap" 'function)) :int
+  (table :pointer)
+  (heuristic #.(swig-lispify "Cudd_ReorderingType" 'enumname))
+  (minsize :int))
+
+(cl:export '#.(swig-lispify "Cudd_ReduceHeap" 'function))
+
+(cffi:defcfun ("Cudd_ShuffleHeap" #.(swig-lispify "Cudd_ShuffleHeap" 'function)) :int
+  (table :pointer)
+  (permutation :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ShuffleHeap" 'function))
+
+(cffi:defcfun ("Cudd_Eval" #.(swig-lispify "Cudd_Eval" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (inputs :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Eval" 'function))
+
+(cffi:defcfun ("Cudd_ShortestPath" #.(swig-lispify "Cudd_ShortestPath" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (weight :pointer)
+  (support :pointer)
+  (length :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ShortestPath" 'function))
+
+(cffi:defcfun ("Cudd_LargestCube" #.(swig-lispify "Cudd_LargestCube" 'function)) :pointer
+  (manager :pointer)
+  (f :pointer)
+  (length :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_LargestCube" 'function))
+
+(cffi:defcfun ("Cudd_ShortestLength" #.(swig-lispify "Cudd_ShortestLength" 'function)) :int
+  (manager :pointer)
+  (f :pointer)
+  (weight :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ShortestLength" 'function))
+
+(cffi:defcfun ("Cudd_Decreasing" #.(swig-lispify "Cudd_Decreasing" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_Decreasing" 'function))
+
+(cffi:defcfun ("Cudd_Increasing" #.(swig-lispify "Cudd_Increasing" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_Increasing" 'function))
+
+(cffi:defcfun ("Cudd_EquivDC" #.(swig-lispify "Cudd_EquivDC" 'function)) :int
+  (dd :pointer)
+  (F :pointer)
+  (G :pointer)
+  (D :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_EquivDC" 'function))
+
+(cffi:defcfun ("Cudd_bddLeqUnless" #.(swig-lispify "Cudd_bddLeqUnless" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (D :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddLeqUnless" 'function))
+
+(cffi:defcfun ("Cudd_EqualSupNorm" #.(swig-lispify "Cudd_EqualSupNorm" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (tolerance :double)
+  (pr :int))
+
+(cl:export '#.(swig-lispify "Cudd_EqualSupNorm" 'function))
+
+(cffi:defcfun ("Cudd_bddMakePrime" #.(swig-lispify "Cudd_bddMakePrime" 'function)) :pointer
+  (dd :pointer)
+  (cube :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddMakePrime" 'function))
+
+(cffi:defcfun ("Cudd_bddMaximallyExpand" #.(swig-lispify "Cudd_bddMaximallyExpand" 'function)) :pointer
+  (dd :pointer)
+  (lb :pointer)
+  (ub :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddMaximallyExpand" 'function))
+
+(cffi:defcfun ("Cudd_bddLargestPrimeUnate" #.(swig-lispify "Cudd_bddLargestPrimeUnate" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (phaseBdd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddLargestPrimeUnate" 'function))
+
+(cffi:defcfun ("Cudd_CofMinterm" #.(swig-lispify "Cudd_CofMinterm" 'function)) :pointer
+  (dd :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CofMinterm" 'function))
+
+(cffi:defcfun ("Cudd_SolveEqn" #.(swig-lispify "Cudd_SolveEqn" 'function)) :pointer
+  (bdd :pointer)
+  (F :pointer)
+  (Y :pointer)
+  (G :pointer)
+  (yIndex :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_SolveEqn" 'function))
+
+(cffi:defcfun ("Cudd_VerifySol" #.(swig-lispify "Cudd_VerifySol" 'function)) :pointer
+  (bdd :pointer)
+  (F :pointer)
+  (G :pointer)
+  (yIndex :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_VerifySol" 'function))
+
+(cffi:defcfun ("Cudd_SplitSet" #.(swig-lispify "Cudd_SplitSet" 'function)) :pointer
+  (manager :pointer)
+  (S :pointer)
+  (xVars :pointer)
+  (n :int)
+  (m :double))
+
+(cl:export '#.(swig-lispify "Cudd_SplitSet" 'function))
+
+(cffi:defcfun ("Cudd_SubsetHeavyBranch" #.(swig-lispify "Cudd_SubsetHeavyBranch" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int))
+
+(cl:export '#.(swig-lispify "Cudd_SubsetHeavyBranch" 'function))
+
+(cffi:defcfun ("Cudd_SupersetHeavyBranch" #.(swig-lispify "Cudd_SupersetHeavyBranch" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int))
+
+(cl:export '#.(swig-lispify "Cudd_SupersetHeavyBranch" 'function))
+
+(cffi:defcfun ("Cudd_SubsetShortPaths" #.(swig-lispify "Cudd_SubsetShortPaths" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (hardlimit :int))
+
+(cl:export '#.(swig-lispify "Cudd_SubsetShortPaths" 'function))
+
+(cffi:defcfun ("Cudd_SupersetShortPaths" #.(swig-lispify "Cudd_SupersetShortPaths" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (numVars :int)
+  (threshold :int)
+  (hardlimit :int))
+
+(cl:export '#.(swig-lispify "Cudd_SupersetShortPaths" 'function))
+
+(cffi:defcfun ("Cudd_SymmProfile" #.(swig-lispify "Cudd_SymmProfile" 'function)) :void
+  (table :pointer)
+  (lower :int)
+  (upper :int))
+
+(cl:export '#.(swig-lispify "Cudd_SymmProfile" 'function))
+
+(cffi:defcfun ("Cudd_Prime" #.(swig-lispify "Cudd_Prime" 'function)) :unsigned-int
+  (p :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_Prime" 'function))
+
+(cffi:defcfun ("Cudd_Reserve" #.(swig-lispify "Cudd_Reserve" 'function)) :int
+  (manager :pointer)
+  (amount :int))
+
+(cl:export '#.(swig-lispify "Cudd_Reserve" 'function))
+
+(cffi:defcfun ("Cudd_PrintMinterm" #.(swig-lispify "Cudd_PrintMinterm" 'function)) :int
+  (manager :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintMinterm" 'function))
+
+(cffi:defcfun ("Cudd_bddPrintCover" #.(swig-lispify "Cudd_bddPrintCover" 'function)) :int
+  (dd :pointer)
+  (l :pointer)
+  (u :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddPrintCover" 'function))
+
+(cffi:defcfun ("Cudd_PrintDebug" #.(swig-lispify "Cudd_PrintDebug" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (n :int)
+  (pr :int))
+
+(cl:export '#.(swig-lispify "Cudd_PrintDebug" 'function))
+
+(cffi:defcfun ("Cudd_PrintSummary" #.(swig-lispify "Cudd_PrintSummary" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (n :int)
+  (mode :int))
+
+(cl:export '#.(swig-lispify "Cudd_PrintSummary" 'function))
+
+(cffi:defcfun ("Cudd_DagSize" #.(swig-lispify "Cudd_DagSize" 'function)) :int
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_DagSize" 'function))
+
+(cffi:defcfun ("Cudd_EstimateCofactor" #.(swig-lispify "Cudd_EstimateCofactor" 'function)) :int
+  (dd :pointer)
+  (node :pointer)
+  (i :int)
+  (phase :int))
+
+(cl:export '#.(swig-lispify "Cudd_EstimateCofactor" 'function))
+
+(cffi:defcfun ("Cudd_EstimateCofactorSimple" #.(swig-lispify "Cudd_EstimateCofactorSimple" 'function)) :int
+  (node :pointer)
+  (i :int))
+
+(cl:export '#.(swig-lispify "Cudd_EstimateCofactorSimple" 'function))
+
+(cffi:defcfun ("Cudd_SharingSize" #.(swig-lispify "Cudd_SharingSize" 'function)) :int
+  (nodeArray :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_SharingSize" 'function))
+
+(cffi:defcfun ("Cudd_CountMinterm" #.(swig-lispify "Cudd_CountMinterm" 'function)) :double
+  (manager :pointer)
+  (node :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_CountMinterm" 'function))
+
+(cffi:defcfun ("Cudd_LdblCountMinterm" #.(swig-lispify "Cudd_LdblCountMinterm" 'function)) :pointer
+  (manager :pointer)
+  (node :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_LdblCountMinterm" 'function))
+
+(cffi:defcfun ("Cudd_EpdPrintMinterm" #.(swig-lispify "Cudd_EpdPrintMinterm" 'function)) :int
+  (dd :pointer)
+  (node :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_EpdPrintMinterm" 'function))
+
+(cffi:defcfun ("Cudd_CountPath" #.(swig-lispify "Cudd_CountPath" 'function)) :double
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CountPath" 'function))
+
+(cffi:defcfun ("Cudd_CountPathsToNonZero" #.(swig-lispify "Cudd_CountPathsToNonZero" 'function)) :double
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CountPathsToNonZero" 'function))
+
+(cffi:defcfun ("Cudd_SupportIndices" #.(swig-lispify "Cudd_SupportIndices" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (indices :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SupportIndices" 'function))
+
+(cffi:defcfun ("Cudd_Support" #.(swig-lispify "Cudd_Support" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Support" 'function))
+
+(cffi:defcfun ("Cudd_SupportIndex" #.(swig-lispify "Cudd_SupportIndex" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SupportIndex" 'function))
+
+(cffi:defcfun ("Cudd_SupportSize" #.(swig-lispify "Cudd_SupportSize" 'function)) :int
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_SupportSize" 'function))
+
+(cffi:defcfun ("Cudd_VectorSupportIndices" #.(swig-lispify "Cudd_VectorSupportIndices" 'function)) :int
+  (dd :pointer)
+  (F :pointer)
+  (n :int)
+  (indices :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_VectorSupportIndices" 'function))
+
+(cffi:defcfun ("Cudd_VectorSupport" #.(swig-lispify "Cudd_VectorSupport" 'function)) :pointer
+  (dd :pointer)
+  (F :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_VectorSupport" 'function))
+
+(cffi:defcfun ("Cudd_VectorSupportIndex" #.(swig-lispify "Cudd_VectorSupportIndex" 'function)) :pointer
+  (dd :pointer)
+  (F :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_VectorSupportIndex" 'function))
+
+(cffi:defcfun ("Cudd_VectorSupportSize" #.(swig-lispify "Cudd_VectorSupportSize" 'function)) :int
+  (dd :pointer)
+  (F :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_VectorSupportSize" 'function))
+
+(cffi:defcfun ("Cudd_ClassifySupport" #.(swig-lispify "Cudd_ClassifySupport" 'function)) :int
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (common :pointer)
+  (onlyF :pointer)
+  (onlyG :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_ClassifySupport" 'function))
+
+(cffi:defcfun ("Cudd_CountLeaves" #.(swig-lispify "Cudd_CountLeaves" 'function)) :int
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CountLeaves" 'function))
+
+(cffi:defcfun ("Cudd_bddPickOneCube" #.(swig-lispify "Cudd_bddPickOneCube" 'function)) :int
+  (ddm :pointer)
+  (node :pointer)
+  (string :string))
+
+(cl:export '#.(swig-lispify "Cudd_bddPickOneCube" 'function))
+
+(cffi:defcfun ("Cudd_bddPickOneMinterm" #.(swig-lispify "Cudd_bddPickOneMinterm" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vars :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddPickOneMinterm" 'function))
+
+(cffi:defcfun ("Cudd_bddPickArbitraryMinterms" #.(swig-lispify "Cudd_bddPickArbitraryMinterms" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vars :pointer)
+  (n :int)
+  (k :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddPickArbitraryMinterms" 'function))
+
+(cffi:defcfun ("Cudd_SubsetWithMaskVars" #.(swig-lispify "Cudd_SubsetWithMaskVars" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (vars :pointer)
+  (nvars :int)
+  (maskVars :pointer)
+  (mvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_SubsetWithMaskVars" 'function))
+
+(cffi:defcfun ("Cudd_FirstCube" #.(swig-lispify "Cudd_FirstCube" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (cube :pointer)
+  (value :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FirstCube" 'function))
+
+(cffi:defcfun ("Cudd_NextCube" #.(swig-lispify "Cudd_NextCube" 'function)) :int
+  (gen :pointer)
+  (cube :pointer)
+  (value :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_NextCube" 'function))
+
+(cffi:defcfun ("Cudd_FirstPrime" #.(swig-lispify "Cudd_FirstPrime" 'function)) :pointer
+  (dd :pointer)
+  (l :pointer)
+  (u :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FirstPrime" 'function))
+
+(cffi:defcfun ("Cudd_NextPrime" #.(swig-lispify "Cudd_NextPrime" 'function)) :int
+  (gen :pointer)
+  (cube :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_NextPrime" 'function))
+
+(cffi:defcfun ("Cudd_bddComputeCube" #.(swig-lispify "Cudd_bddComputeCube" 'function)) :pointer
+  (dd :pointer)
+  (vars :pointer)
+  (phase :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddComputeCube" 'function))
+
+(cffi:defcfun ("Cudd_addComputeCube" #.(swig-lispify "Cudd_addComputeCube" 'function)) :pointer
+  (dd :pointer)
+  (vars :pointer)
+  (phase :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_addComputeCube" 'function))
+
+(cffi:defcfun ("Cudd_CubeArrayToBdd" #.(swig-lispify "Cudd_CubeArrayToBdd" 'function)) :pointer
+  (dd :pointer)
+  (array :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_CubeArrayToBdd" 'function))
+
+(cffi:defcfun ("Cudd_BddToCubeArray" #.(swig-lispify "Cudd_BddToCubeArray" 'function)) :int
+  (dd :pointer)
+  (cube :pointer)
+  (array :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_BddToCubeArray" 'function))
+
+(cffi:defcfun ("Cudd_FirstNode" #.(swig-lispify "Cudd_FirstNode" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_FirstNode" 'function))
+
+(cffi:defcfun ("Cudd_NextNode" #.(swig-lispify "Cudd_NextNode" 'function)) :int
+  (gen :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_NextNode" 'function))
+
+(cffi:defcfun ("Cudd_GenFree" #.(swig-lispify "Cudd_GenFree" 'function)) :int
+  (gen :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_GenFree" 'function))
+
+(cffi:defcfun ("Cudd_IsGenEmpty" #.(swig-lispify "Cudd_IsGenEmpty" 'function)) :int
+  (gen :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_IsGenEmpty" 'function))
+
+(cffi:defcfun ("Cudd_IndicesToCube" #.(swig-lispify "Cudd_IndicesToCube" 'function)) :pointer
+  (dd :pointer)
+  (array :pointer)
+  (n :int))
+
+(cl:export '#.(swig-lispify "Cudd_IndicesToCube" 'function))
+
+(cffi:defcfun ("Cudd_PrintVersion" #.(swig-lispify "Cudd_PrintVersion" 'function)) :void
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_PrintVersion" 'function))
+
+(cffi:defcfun ("Cudd_AverageDistance" #.(swig-lispify "Cudd_AverageDistance" 'function)) :double
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_AverageDistance" 'function))
+
+(cffi:defcfun ("Cudd_Random" #.(swig-lispify "Cudd_Random" 'function)) :pointer
+  (dd :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Random" 'function))
+
+(cffi:defcfun ("Cudd_Srandom" #.(swig-lispify "Cudd_Srandom" 'function)) :void
+  (dd :pointer)
+  (seed :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_Srandom" 'function))
+
+(cffi:defcfun ("Cudd_Density" #.(swig-lispify "Cudd_Density" 'function)) :double
+  (dd :pointer)
+  (f :pointer)
+  (nvars :int))
+
+(cl:export '#.(swig-lispify "Cudd_Density" 'function))
+
+(cffi:defcfun ("Cudd_OutOfMem" #.(swig-lispify "Cudd_OutOfMem" 'function)) :void
+  (size :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_OutOfMem" 'function))
+
+(cffi:defcfun ("Cudd_OutOfMemSilent" #.(swig-lispify "Cudd_OutOfMemSilent" 'function)) :void
+  (size :unsigned-int))
+
+(cl:export '#.(swig-lispify "Cudd_OutOfMemSilent" 'function))
+
+(cffi:defcfun ("Cudd_zddCount" #.(swig-lispify "Cudd_zddCount" 'function)) :int
+  (zdd :pointer)
+  (P :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddCount" 'function))
+
+(cffi:defcfun ("Cudd_zddCountDouble" #.(swig-lispify "Cudd_zddCountDouble" 'function)) :double
+  (zdd :pointer)
+  (P :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddCountDouble" 'function))
+
+(cffi:defcfun ("Cudd_zddProduct" #.(swig-lispify "Cudd_zddProduct" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddProduct" 'function))
+
+(cffi:defcfun ("Cudd_zddUnateProduct" #.(swig-lispify "Cudd_zddUnateProduct" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddUnateProduct" 'function))
+
+(cffi:defcfun ("Cudd_zddWeakDiv" #.(swig-lispify "Cudd_zddWeakDiv" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddWeakDiv" 'function))
+
+(cffi:defcfun ("Cudd_zddDivide" #.(swig-lispify "Cudd_zddDivide" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDivide" 'function))
+
+(cffi:defcfun ("Cudd_zddWeakDivF" #.(swig-lispify "Cudd_zddWeakDivF" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddWeakDivF" 'function))
+
+(cffi:defcfun ("Cudd_zddDivideF" #.(swig-lispify "Cudd_zddDivideF" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDivideF" 'function))
+
+(cffi:defcfun ("Cudd_zddComplement" #.(swig-lispify "Cudd_zddComplement" 'function)) :pointer
+  (dd :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddComplement" 'function))
+
+(cffi:defcfun ("Cudd_zddIsop" #.(swig-lispify "Cudd_zddIsop" 'function)) :pointer
+  (dd :pointer)
+  (L :pointer)
+  (U :pointer)
+  (zdd_I :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddIsop" 'function))
+
+(cffi:defcfun ("Cudd_bddIsop" #.(swig-lispify "Cudd_bddIsop" 'function)) :pointer
+  (dd :pointer)
+  (L :pointer)
+  (U :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsop" 'function))
+
+(cffi:defcfun ("Cudd_MakeBddFromZddCover" #.(swig-lispify "Cudd_MakeBddFromZddCover" 'function)) :pointer
+  (dd :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_MakeBddFromZddCover" 'function))
+
+(cffi:defcfun ("Cudd_zddDagSize" #.(swig-lispify "Cudd_zddDagSize" 'function)) :int
+  (p_node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDagSize" 'function))
+
+(cffi:defcfun ("Cudd_zddCountMinterm" #.(swig-lispify "Cudd_zddCountMinterm" 'function)) :double
+  (zdd :pointer)
+  (node :pointer)
+  (path :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddCountMinterm" 'function))
+
+(cffi:defcfun ("Cudd_zddPrintSubtable" #.(swig-lispify "Cudd_zddPrintSubtable" 'function)) :void
+  (table :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddPrintSubtable" 'function))
+
+(cffi:defcfun ("Cudd_zddPortFromBdd" #.(swig-lispify "Cudd_zddPortFromBdd" 'function)) :pointer
+  (dd :pointer)
+  (B :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddPortFromBdd" 'function))
+
+(cffi:defcfun ("Cudd_zddPortToBdd" #.(swig-lispify "Cudd_zddPortToBdd" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddPortToBdd" 'function))
+
+(cffi:defcfun ("Cudd_zddReduceHeap" #.(swig-lispify "Cudd_zddReduceHeap" 'function)) :int
+  (table :pointer)
+  (heuristic #.(swig-lispify "Cudd_ReorderingType" 'enumname))
+  (minsize :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddReduceHeap" 'function))
+
+(cffi:defcfun ("Cudd_zddShuffleHeap" #.(swig-lispify "Cudd_zddShuffleHeap" 'function)) :int
+  (table :pointer)
+  (permutation :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddShuffleHeap" 'function))
+
+(cffi:defcfun ("Cudd_zddIte" #.(swig-lispify "Cudd_zddIte" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer)
+  (g :pointer)
+  (h :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddIte" 'function))
+
+(cffi:defcfun ("Cudd_zddUnion" #.(swig-lispify "Cudd_zddUnion" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (Q :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddUnion" 'function))
+
+(cffi:defcfun ("Cudd_zddIntersect" #.(swig-lispify "Cudd_zddIntersect" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (Q :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddIntersect" 'function))
+
+(cffi:defcfun ("Cudd_zddDiff" #.(swig-lispify "Cudd_zddDiff" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (Q :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDiff" 'function))
+
+(cffi:defcfun ("Cudd_zddDiffConst" #.(swig-lispify "Cudd_zddDiffConst" 'function)) :pointer
+  (zdd :pointer)
+  (P :pointer)
+  (Q :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDiffConst" 'function))
+
+(cffi:defcfun ("Cudd_zddSubset1" #.(swig-lispify "Cudd_zddSubset1" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (var :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddSubset1" 'function))
+
+(cffi:defcfun ("Cudd_zddSubset0" #.(swig-lispify "Cudd_zddSubset0" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (var :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddSubset0" 'function))
+
+(cffi:defcfun ("Cudd_zddChange" #.(swig-lispify "Cudd_zddChange" 'function)) :pointer
+  (dd :pointer)
+  (P :pointer)
+  (var :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddChange" 'function))
+
+(cffi:defcfun ("Cudd_zddSymmProfile" #.(swig-lispify "Cudd_zddSymmProfile" 'function)) :void
+  (table :pointer)
+  (lower :int)
+  (upper :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddSymmProfile" 'function))
+
+(cffi:defcfun ("Cudd_zddPrintMinterm" #.(swig-lispify "Cudd_zddPrintMinterm" 'function)) :int
+  (zdd :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddPrintMinterm" 'function))
+
+(cffi:defcfun ("Cudd_zddPrintCover" #.(swig-lispify "Cudd_zddPrintCover" 'function)) :int
+  (zdd :pointer)
+  (node :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddPrintCover" 'function))
+
+(cffi:defcfun ("Cudd_zddPrintDebug" #.(swig-lispify "Cudd_zddPrintDebug" 'function)) :int
+  (zdd :pointer)
+  (f :pointer)
+  (n :int)
+  (pr :int))
+
+(cl:export '#.(swig-lispify "Cudd_zddPrintDebug" 'function))
+
+(cffi:defcfun ("Cudd_zddFirstPath" #.(swig-lispify "Cudd_zddFirstPath" 'function)) :pointer
+  (zdd :pointer)
+  (f :pointer)
+  (path :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddFirstPath" 'function))
+
+(cffi:defcfun ("Cudd_zddNextPath" #.(swig-lispify "Cudd_zddNextPath" 'function)) :int
+  (gen :pointer)
+  (path :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddNextPath" 'function))
+
+(cffi:defcfun ("Cudd_zddCoverPathToString" #.(swig-lispify "Cudd_zddCoverPathToString" 'function)) :string
+  (zdd :pointer)
+  (path :pointer)
+  (str :string))
+
+(cl:export '#.(swig-lispify "Cudd_zddCoverPathToString" 'function))
+
+(cffi:defcfun ("Cudd_zddSupport" #.(swig-lispify "Cudd_zddSupport" 'function)) :pointer
+  (dd :pointer)
+  (f :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddSupport" 'function))
+
+(cffi:defcfun ("Cudd_zddDumpDot" #.(swig-lispify "Cudd_zddDumpDot" 'function)) :int
+  (dd :pointer)
+  (n :int)
+  (f :pointer)
+  (inames :pointer)
+  (onames :pointer)
+  (fp :pointer))
+
+(cl:export '#.(swig-lispify "Cudd_zddDumpDot" 'function))
+
+(cffi:defcfun ("Cudd_bddSetPiVar" #.(swig-lispify "Cudd_bddSetPiVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetPiVar" 'function))
+
+(cffi:defcfun ("Cudd_bddSetPsVar" #.(swig-lispify "Cudd_bddSetPsVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetPsVar" 'function))
+
+(cffi:defcfun ("Cudd_bddSetNsVar" #.(swig-lispify "Cudd_bddSetNsVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetNsVar" 'function))
+
+(cffi:defcfun ("Cudd_bddIsPiVar" #.(swig-lispify "Cudd_bddIsPiVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsPiVar" 'function))
+
+(cffi:defcfun ("Cudd_bddIsPsVar" #.(swig-lispify "Cudd_bddIsPsVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsPsVar" 'function))
+
+(cffi:defcfun ("Cudd_bddIsNsVar" #.(swig-lispify "Cudd_bddIsNsVar" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsNsVar" 'function))
+
+(cffi:defcfun ("Cudd_bddSetPairIndex" #.(swig-lispify "Cudd_bddSetPairIndex" 'function)) :int
+  (dd :pointer)
+  (index :int)
+  (pairIndex :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetPairIndex" 'function))
+
+(cffi:defcfun ("Cudd_bddReadPairIndex" #.(swig-lispify "Cudd_bddReadPairIndex" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddReadPairIndex" 'function))
+
+(cffi:defcfun ("Cudd_bddSetVarToBeGrouped" #.(swig-lispify "Cudd_bddSetVarToBeGrouped" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetVarToBeGrouped" 'function))
+
+(cffi:defcfun ("Cudd_bddSetVarHardGroup" #.(swig-lispify "Cudd_bddSetVarHardGroup" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetVarHardGroup" 'function))
+
+(cffi:defcfun ("Cudd_bddResetVarToBeGrouped" #.(swig-lispify "Cudd_bddResetVarToBeGrouped" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddResetVarToBeGrouped" 'function))
+
+(cffi:defcfun ("Cudd_bddIsVarToBeGrouped" #.(swig-lispify "Cudd_bddIsVarToBeGrouped" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsVarToBeGrouped" 'function))
+
+(cffi:defcfun ("Cudd_bddSetVarToBeUngrouped" #.(swig-lispify "Cudd_bddSetVarToBeUngrouped" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddSetVarToBeUngrouped" 'function))
+
+(cffi:defcfun ("Cudd_bddIsVarToBeUngrouped" #.(swig-lispify "Cudd_bddIsVarToBeUngrouped" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsVarToBeUngrouped" 'function))
+
+(cffi:defcfun ("Cudd_bddIsVarHardGroup" #.(swig-lispify "Cudd_bddIsVarHardGroup" 'function)) :int
+  (dd :pointer)
+  (index :int))
+
+(cl:export '#.(swig-lispify "Cudd_bddIsVarHardGroup" 'function))
+
+

--- a/src/zdd.lisp	Thu Oct 27 14:38:18 2016 +0000
+++ b/src/zdd.lisp	Thu Oct 27 15:45:42 2016 +0000
@@ -1,9 +1,10 @@
 (in-package :scully.zdd)
 
-;;;; Library ------------------------------------------------------------------
-(define-foreign-library cudd
-  (:darwin "./build/libcudd.dylib"))
 
-(use-foreign-library cudd)
+(defparameter *cudd-manager*
+  (scully.cudd:cudd-init 0
+                         0
+                         scully.cudd:+cudd-unique-slots+
+                         scully.cudd:+cudd-cache-slots+
+                         0))
 
-