[Buddy-users] Re: A simple question about BuDDy

[Haim C. <hai...@ho...>]

I recall I had to do something similar to get all the assignments...
However, if you have many assignments and you need to get them all, I would 
say that you should reconsider your design.
The whole idea of BDDs is that they are a compact representation of Boolean 
function.
In your application, try to defer the processing of the assignment as long 
as you can, and always favor BDD operations on other data structures.

Haim

----- Original Message ----- 
From: "Qin Yang" <qin...@ya...>
To: <hai...@us...>
Cc: <bud...@li...>
Sent: Friday, August 05, 2005 19:27
Subject: A simple question about BuDDy


> Dear Haim Cohen,
>
> I am a new user of BuDDy. To find all the satisfying
> assignments of a bdd, I find that "bdd_allsat()" is
> not enough for me. For example,
>    bdd a = bdd_ithvar(0);
>    bdd b = bdd_ithvar(1);
>    bdd c = bdd_ithvar(2);
>
>    bdd x = a & !b & c;
>    x |= a & !b & !c;
> The satisfying assignments of x are [1,0,1] and
> [1,0,0]. However, "allsatHandler()" provides the
> assignment of [1,0,X] ('X' means notcare). Could you
> tell me if there is any interface that I can use to
> obtain all the unique assignments (not including 'X')
> similarly?
>
> Thanks a lot!
>
> Best Regards,
> Qin
>
>
>
> ____________________________________________________
> Start your day with Yahoo! - make it your home page
> http://www.yahoo.com/r/hs
>
>