To do			-*- Outline -*-
-----

- properly implement substitution/grouping
  - use the BDD's built-in substitution manager for this + ForeignPtrs
    for garbage collection.
  - DONE, but because it uses ints for association id's, we can't use
    ForeignPtrs naturally (see email to Manuel for details).
  - as it is, it generates lots of warnings from the C compiler about
    (int *) <-> (int) conversions without casts. This might not work on
    some platforms GHC supports...

- bind more profiling functions
  - figure out what's useful (bdd_size, bdd_size_multiple, ...)

- get the binding mapping var id's -> names, especially in hbdd_print.
  - CString: lifetimes of objects?
    - how do i free them after calling bdd_print_bdd? (keep a list of them?)

Remove use of newConcForeignPtr, replace with standard FFI op.

* CUDD

FIXME verify garbage collection behaviour

* Implementation notes:

** Laziness

Laziness really bites.

Specifically, all functions using associations need to be conscious of the
evaluation state of all of their BDD arguments. Why? Well, consider the
"forall" function:

> forall :: QBF b => [b] -> b -> b
> forall vars bdd = unsafePerformIO $ ...
>             do {#call unsafe bdd_temp_assoc#} bdd_manager (castPtr assoc) 0
>                bddp <- {#call unsafe bdd_forall#} bdd_manager bdd
>                ...

If the construction of "bdd" involves using an association, then there is a
window between calling "bdd_temp_assoc" and "bdd_forall" where a lazily
evaluated BDD can reset the association to something else. Specifically,
this may happen if "bdd" is first demanded at the actual call to
"bdd_forall", and so we must arrange for "f" to be demanded *before* the
call to "bdd_temp_assoc".

Yes, yes, this is an unsafePerformIO-related problem.

*** Adopt John Meacham's `seq` idiom:

[H]ere is a pure Haskell 98 version that will work the way you want

newtype BDD = BDD (ForeignPtr Int)

exists :: Group BDD -> BDD -> BDD
exists group bdd = unsafePerformIO $
seq bdd $ withGroup group $ \ gid ->
  do bdd_assoc bdd_manager gid
     withBDD bdd ({#call unsafe bdd_exists#} bdd_manager) >>=
addBDDfinalizer

Notice we are seqing bdd not with the value returned, but the second
argument is an 'IO a' itself. so evaluating the second argument doesn't
actually mean running the IO action, it just means deciding on which IO
action will be run. sort of like the following with the Maybe monad.

f x y = x `seq` Just y

this function is strict in x but not in y, because it is the container
(Maybe a) that it is strict in, not a itself.