buddy-users — Using the BuDDy library and BDDs in general

Re: [Buddy-users] bdd_disable_reorder() in bdd_support() misplaced?

[Nikos G. <nik...@gm...>]

Hi Karel,

On 05/02/14 12:28, Karel Heyse wrote:
> Is it possible that the bdd_disable_reorder() in bdd_support() in
> bddop.c should happen before support_rec()?
> Because, support_rec stores the levels of all the variables of the bdd
> in supportSet. And it's probably bad if those levels change before the
> support BDD is constructed.

Reordering can be triggered while performing BDD operations.  There is 
nothing in support_rec (nor in bdd_support before the call to 
bdd_disable_reorder) that calls a BDD operation, so no reordering should 
happen before that call.

Regards,
Nikos

[Buddy-users] bdd_disable_reorder() in bdd_support() misplaced?

[Karel H. <vor...@gm...>]

Hi,

Is it possible that the bdd_disable_reorder() in bdd_support() in bddop.c should happen before support_rec()?
Because, support_rec stores the levels of all the variables of the bdd in supportSet. And it's probably bad if those levels change before the support BDD is constructed.

Extract:
   support_rec(r, supportSet);
   bdd_unmark(r);

   bdd_disable_reorder();

   for (n=supportMax ; n>=supportMin ; --n)
      if (supportSet[n] == supportID)
      {
	 register BDD tmp;
	 bdd_addref(res);
	 tmp = bdd_makenode(n, 0, res);
	 bdd_delref(res);
	 res = tmp;
      }
   
   bdd_enable_reorder();

   return res;
}

Kind regards
Karel

[Buddy-users] Mohammed Al Saleh

[Mohammed Al S. <moh...@ya...>]

wer    
http://en.termabania.pl/jqrifzmg/ucqqfsxexzt/iygkll/ygttxhdfahl.php    Mohammed Al Saleh

[Buddy-users] BDD creation of a boolean function which is there in some file

[harish s. <har...@gm...>]

hi all,
           i started using Buddy library .
where i can easily create a  bdd for   f= a | b ^ c Boolean function .

but when i want to read this boolean funciton from  a file . while
assigning this Boolean function string to bdd variable it gives error :
type mismatch . one is bdd and other is string.

kindly help me . Thanks in advance
Regards
Harish

[Buddy-users] Buddy on Multi-Threaded Process

[Faisal N. K. <fn...@gm...>]

Hi

I am working on multi-threaded program where multiple threads utilize
buddy package. The program keeps crashing with error

BDD error: Unknown variable.

After a bit of debugging, it appears to me that the bdd variables are
being cleared by garbage collection in one thread that were supposed
to be used by other thread. As such, I am wondering how to use Buddy
in a multi-threaded environment, especially since the package does not
allow multiple instances of initializations.

Any help would be very much appreciated.

Thank you
Faisal Khan

[Buddy-users] BuDDy and VC++

[Ryan L. <le...@mc...>]

Hello,

I have an exiting application that is primarily used in Linux, but also compiles fine under MS Visual C++ environment (some of my developers prefer to use VC++).

I am adding some new algs that use BuDDy  which is fine for Linux, but I wish to still be able to compile in VC++.


The question is how to compile BuDDy under VC++?  I hyave heard it has been done, but I have not been able to find any documentation on how to do this.

Can anyone point me in the right direction?

Ryan
	

[Buddy-users] Use of bdd_veccompose

[Jimmy <jim...@an...>]

Hi,

I've recently come across a problem where I'd like to replace some BDD
variables with some formulae (for example, replace variable 0 with "1 OR
2" and variable 2 with "4 OR 7"), and it looks like bdd_veccompose is
the function I want to use. However I can't seem to work out how to use
it.

It takes a bddPair, and from what I can understand a bddPair is strictly
from variables to variables, not from variables to arbitrary BDDs. I
tried playing around with a trivial example to see if I could ignore
this, and add a pair entry from bdd_ithvar(0) to
bdd_or(bdd_ithvar(1),bdd_ithvar(2)), but this complains about unknown
variables. The documentation of bdd_setpairs also seems unclear to me,
taking integers (rather than BDDs) for arguments, but the description
indicating that the arrays can contain BDDs.

Am I on the right track, and if not, what should I be using instead? The
alternative that comes to mind would be replacing the variables with
fresh ones and then doing a series of bdd_compose calls, but this
doesn't sound particularly good.

Thanks,

Jimmy

[Buddy-users] Memory / time efficiency at small numbers of variables

[Jimmy <u43...@an...>]

Hi, I'm a new user of BuDDy, and I've found that with as few as 70 BDD
variables, I'm tending towards using several gigabytes of memory,
millions of nodes (as reported by the GC), and a nontrivial amount of
time to and- together some 25 relatively small (3 or 4 variable nodes
when printed) formulae.

Is this common behaviour? Is there a better way to calculate the
conjunction of a collection of formulae? Could this be somehow due to me
using the OCaml bindings, rather than C/++?

I am implementing my own version of someone else's algorithm as a
prelude to modifying it, and I know that their implementation can handle
the particular instance I am trying within 20 seconds, while my version
is taking several minutes and more memory. However I don't know whether
they use another BDD package which may be better, or whether they use
other tricks and tweaks to improve performance which I'm not aware of.

Thanks,

Jimmy

[Buddy-users] Multiple instances of bdd

[Mohammed Al S. <moh...@ya...>]

Dear All,

I am using buddy, and I'd like to have like more than one instance of bdd. i.e. 
I want to initialize the two instances separately, something like

buddy instance1;
instance1.bdd_init();

buddy instance2;
instance2.bdd_init();

like this each one will be initialize with bdd_init() separately. Is that 
possible in buddy?

Regards.

[Buddy-users] Building buddy dll

[masoud k. <mas...@ya...>]

Dear all;

How I can configure buddy in order to output .dll file after build (when 
compiling with Cygwin)?

Thanks



      

[Buddy-users] BuDDy Out-of-Range error

[Hasan Q. <ha...@gm...>]

Dear All,

I am a new user of Buddy. I am using JavaBDD which is an inteface to BuDDy.

The following lines of code

bddFactory_ = BDDFactory.init(7000000, 1000000); // these numbers are
subject to change
	System.out.println(elementNumberInP_ * 10 );
	bddFactory_.setVarNum(elementNumberInP_ * 10) ;

Give me the following output:

2380
Exception in thread "main" net.sf.javabdd.BDDException: Value out of range
	at net.sf.javabdd.BuDDyFactory.setVarNum0(Native Method)
	at net.sf.javabdd.BuDDyFactory.setVarNum(BuDDyFactory.java:312)

I would highly appreciate it if you could explain to me what went
wrong. What is the range? How to change it?

Thanks,

Hasan

Re: [Buddy-users] bdd_setvarorder !!!

[Pietro A. <Pie...@pp...>]

Hi again.

I'm trying to debug this problem of mine ... it seems that the culprit is in
the function mark_roots in reorder.c . In particular the second loop takes
forever. I'm not quite sure if I understand what is happening here. If I read
the complexity of this function is O(bddnodesize * bddvarnum^2) ... that is
quite a lot !

Can anybody explain to me why this loops is soooooo slow even on an empty bdd ?

I'm sure I'm missing something here and I'd love a bit of help.

regards,
pietro

for reference :

-----------------------

static void addDependencies(char *dep)
{
   int n,m;

   for (n=0 ; n<bddvarnum ; n++)
   {
      for (m=n ; m<bddvarnum ; m++)
      {
   if (dep[n]  &&  dep[m])
   {
      imatrixSet(iactmtx, n,m);
      imatrixSet(iactmtx, m,n);
   }
      }
   }
}

/* Make sure all nodes are recursively reference counted and store info about
   nodes that are refcou. externally. This info is used at last to revert
   to the standard GBC mode.
 */
static int mark_roots(void)
{
   char *dep = NEW(char,bddvarnum);
   int n;

   for (n=2,extrootsize=0 ; n<bddnodesize ; n++)
   {
         /* This is where we go from .level to .var!
    * - Do NOT use the LEVEL macro here. */
      bddnodes[n].level = bddlevel2var[bddnodes[n].level];

      if (bddnodes[n].refcou > 0)
      {
   SETMARK(n);
   extrootsize++;
      }
   }

   if ((extroots=(int*)(malloc(sizeof(int)*extrootsize))) == NULL)
      return bdd_error(BDD_MEMORY);

   iactmtx = imatrixNew(bddvarnum);

   for (n=2,extrootsize=0 ; n<bddnodesize ; n++)
   {
      BddNode *node = &bddnodes[n];

      if (MARKEDp(node))
      {
   UNMARKp(node);
   extroots[extrootsize++] = n;

   memset(dep,0,bddvarnum);
   dep[VARp(node)] = 1;
   levels[VARp(node)].nodenum++;

   addref_rec(LOWp(node), dep);
   addref_rec(HIGHp(node), dep);

   addDependencies(dep);
      }

      /* Make sure the hash field is empty. This saves a loop in the
   initial GBC */
      node->hash = 0;
   }

   bddnodes[0].hash = 0;
   bddnodes[1].hash = 0;

   free(dep);
   return 0;
}


On Thu, May 27, 2010 at 10:49:51AM +0200, Pietro Abate wrote:
> Hi !
> 
> I did before sending the message, but I didn't find any example with
> bdd_setvarorder (you mean the directory example...). 
> 
> I've just noticed that I wrote orange for apples... My problem is with
> setvarorder (not num) ...
> 
> this is a revised example. it does not print the order ... but it works
> (does not hang) if I use 25 variables instead of 25000 ... Is 25000
> variables to much for buddy bdd to handle ?
> 
> ------------
> #include <bdd.h>
> 
> main(void)
> {
>   int max = 25000;
>   bdd_init(max*2,max*10);
>   bdd_setvarnum(max);
>   int a[max];
>   int i;
>   for(i = 0; i < max ;i++){
>     a[i] = i;
>   }
>   printf("before\n");
> //  bdd_disable_reorder();
>   bdd_printorder();
>   bdd_reorder_verbose(2);
>   bdd_setvarorder(a);
>   bdd_printorder();
>   printf("after\n");
>   return;
> }
> --------------
> 
> a little hint ?
> 
> thanks.
> 
> 
> On Wed, May 26, 2010 at 07:33:09PM -0400, Haim Cohen wrote:
> >    check the unit tests directory for examples.
> > 
> >    On Wed, May 26, 2010 at 4:27 AM, Pietro Abate
> >    <[1]Pie...@pp...> wrote:
> > 
> >      hello.
> > 
> >      I've a problem with bdd_setvarnum ...
> > 
> >      ----------
> >      #include <bdd.h>
> > 
> >      main(void)
> >      {
> >       int max = 25000;
> >       bdd_init(100000,1000000);
> >       bdd_setvarnum(max);
> >       int a[max];
> >       int i;
> >       for(i = 0; i < max ;i++){
> >         a[i] = i;
> >       }
> >       bdd_setvarorder(a);
> >       return;
> >      }
> >      --------------------
> > 
> >      why this piece of code hangs ? I haven't build a bdd yet, so I don't
> >      understand what is doing. In the bdd_setvarorder function there is
> >      a while loop that tries to reorder the bdd, but in this case I it should
> >      just record the variable order ...
> > 
> >      Maybe I misunderstood its use. My goal is to fix a initial static
> >      variable ordering that is will then be used to build the bdd. What am I
> >      doing wrong ?
> > 
> >      Alternatively, can anybody point me to a piece of code that use the
> >      buddy library so I can try to figure out the problem myself by example ?
> > 
> >      thanks.
> >      p
> > 
> >      --
> >      ----
> >      [2]http://en.wikipedia.org/wiki/Posting_style
> > 
> >      ------------------------------------------------------------------------------
> > 
> >      _______________________________________________
> >      Buddy-users mailing list
> >      [3]Bud...@li...
> >      [4]https://lists.sourceforge.net/lists/listinfo/buddy-users
> > 
> >    --
> > 
> >    ---
> >    Haim Cohen / (212) 289 5405
> > 
> > References
> > 
> >    Visible links
> >    1. mailto:Pie...@pp...
> >    2. http://en.wikipedia.org/wiki/Posting_style
> >    3. mailto:Bud...@li...
> >    4. https://lists.sourceforge.net/lists/listinfo/buddy-users
> 
> -- 
> ----
> http://en.wikipedia.org/wiki/Posting_style
> 
> ------------------------------------------------------------------------------
> 
> _______________________________________________
> Buddy-users mailing list
> Bud...@li...
> https://lists.sourceforge.net/lists/listinfo/buddy-users

-- 
----
http://en.wikipedia.org/wiki/Posting_style

[Buddy-users] bdd_setvarorder (not num) !!! Re: bdd_setvarnum problem

[Pietro A. <Pie...@pp...>]

Hi !

I did before sending the message, but I didn't find any example with
bdd_setvarorder (you mean the directory example...). 

I've just noticed that I wrote orange for apples... My problem is with
setvarorder (not num) ...

this is a revised example. it does not print the order ... but it works
(does not hang) if I use 25 variables instead of 25000 ... Is 25000
variables to much for buddy bdd to handle ?

------------
#include <bdd.h>

main(void)
{
  int max = 25000;
  bdd_init(max*2,max*10);
  bdd_setvarnum(max);
  int a[max];
  int i;
  for(i = 0; i < max ;i++){
    a[i] = i;
  }
  printf("before\n");
//  bdd_disable_reorder();
  bdd_printorder();
  bdd_reorder_verbose(2);
  bdd_setvarorder(a);
  bdd_printorder();
  printf("after\n");
  return;
}
--------------

a little hint ?

thanks.


On Wed, May 26, 2010 at 07:33:09PM -0400, Haim Cohen wrote:
>    check the unit tests directory for examples.
> 
>    On Wed, May 26, 2010 at 4:27 AM, Pietro Abate
>    <[1]Pie...@pp...> wrote:
> 
>      hello.
> 
>      I've a problem with bdd_setvarnum ...
> 
>      ----------
>      #include <bdd.h>
> 
>      main(void)
>      {
>       int max = 25000;
>       bdd_init(100000,1000000);
>       bdd_setvarnum(max);
>       int a[max];
>       int i;
>       for(i = 0; i < max ;i++){
>         a[i] = i;
>       }
>       bdd_setvarorder(a);
>       return;
>      }
>      --------------------
> 
>      why this piece of code hangs ? I haven't build a bdd yet, so I don't
>      understand what is doing. In the bdd_setvarorder function there is
>      a while loop that tries to reorder the bdd, but in this case I it should
>      just record the variable order ...
> 
>      Maybe I misunderstood its use. My goal is to fix a initial static
>      variable ordering that is will then be used to build the bdd. What am I
>      doing wrong ?
> 
>      Alternatively, can anybody point me to a piece of code that use the
>      buddy library so I can try to figure out the problem myself by example ?
> 
>      thanks.
>      p
> 
>      --
>      ----
>      [2]http://en.wikipedia.org/wiki/Posting_style
> 
>      ------------------------------------------------------------------------------
> 
>      _______________________________________________
>      Buddy-users mailing list
>      [3]Bud...@li...
>      [4]https://lists.sourceforge.net/lists/listinfo/buddy-users
> 
>    --
> 
>    ---
>    Haim Cohen / (212) 289 5405
> 
> References
> 
>    Visible links
>    1. mailto:Pie...@pp...
>    2. http://en.wikipedia.org/wiki/Posting_style
>    3. mailto:Bud...@li...
>    4. https://lists.sourceforge.net/lists/listinfo/buddy-users

-- 
----
http://en.wikipedia.org/wiki/Posting_style

[Buddy-users] bdd_setvarnum problem

[Pietro A. <Pie...@pp...>]

hello.

I've a problem with bdd_setvarnum ...

----------
#include <bdd.h>

main(void)
{
  int max = 25000;
  bdd_init(100000,1000000);
  bdd_setvarnum(max);
  int a[max];
  int i;
  for(i = 0; i < max ;i++){
    a[i] = i;
  }
  bdd_setvarorder(a);
  return;
}
--------------------

why this piece of code hangs ? I haven't build a bdd yet, so I don't
understand what is doing. In the bdd_setvarorder function there is
a while loop that tries to reorder the bdd, but in this case I it should
just record the variable order ... 

Maybe I misunderstood its use. My goal is to fix a initial static
variable ordering that is will then be used to build the bdd. What am I
doing wrong ? 

Alternatively, can anybody point me to a piece of code that use the
buddy library so I can try to figure out the problem myself by example ?

thanks.
p	      

-- 
----
http://en.wikipedia.org/wiki/Posting_style

[Buddy-users] Buddy make check error

[Vlad S. <vs...@cc...>]

Hello,

I've configured buddy-2.4, I did make and make install. Now I'm trying to do 'make check', but this fails with the error:

Making check in src
make[1]: Entering directory `/home/vlad/BDD/buddy-2.4/src'
make  bddtest
make[2]: Entering directory `/home/vlad/BDD/buddy-2.4/src'
if g++ -DHAVE_CONFIG_H   -I..   -g -O2 -MT bddtest.o -MD -MP -MF ".deps/bddtest.Tpo" -c -o bddtest.o bddtest.cxx; \
	then mv -f ".deps/bddtest.Tpo" ".deps/bddtest.Po"; else rm -f ".deps/bddtest.Tpo"; exit 1; fi
bddtest.cxx: In function ���void fail(std::string, const char*, int)���:
bddtest.cxx:42: error: ���exit��� was not declared in this scope
make[2]: *** [bddtest.o] Error 1
make[2]: Leaving directory `/home/vlad/BDD/buddy-2.4/src'
make[1]: *** [check-am] Error 2
make[1]: Leaving directory `/home/vlad/BDD/buddy-2.4/src'
make: *** [check-recursive] Error 1

The machine I'm running on is an AMD Opteron running 64-bit linux 2.6.31 . The g++ version is 4.4.1 .

Does anyone know what can I do to fix the error?

Thank you,

Vlad

[Buddy-users] Win32 Problem

[Octavio M. P. <omu...@gd...>]

Hi, I’ve been trying to compile buddy in windows but I just get this error
in the part of make install

 c:\MinGW\bin\ranlib.exe: '/usr/local/lib/libbdd.a': No such file

make[2]: *** [install-libLTLIBRARIES] Error 1

make[1]: *** [install-am] Error 2

make: *** [install-recursive] Error 1

 

Configure and make seem to work just fine. I have the MinGW 3.4.5 compiler
and the last version of CYGWIN, I’m working in windows vista home premium
sp1. Can you help me with a tutorial about how to compile the library in
windows or can you give me a compiled library so I can start using buddy on
windows???.

 

Thanks in advance

 

Regards.

 

 

[Buddy-users] some prolbems

[cx_xidian <cx_...@12...>]

 hello,
     i am studying about Buddy,recently i find a question .
    for examples,
  #include "bdd.h"
  #include "fdd.h"

  void main(){
   bdd_init(1000,100);
   int mydomain[]={1,4,7,8,2 };
   fdd_extdomain(mydomain,5);
   bdd_addvarblock(fdd_ithset(0),1);
   
   bdd_printorder();
   bdd_done();
  }
when variable 0 is added into bdd_addbarblock() ,there is a problem in bdd_done().From the debug , i find the bug is in fuction bddtree_del() when variable 0 is in free(t->seq).
And when i replace  bdd_addvarblock(fdd_ithset(0),1) with  bdd_addvarblock(fdd_ithset(i),1) which i is between 1 and 4 ,there is no problem here.
untill now i have not found the problem.
 

Re: [Buddy-users] Un-restrict

[John W. <joe...@gm...>]

Hi,

The restrict() operation returns a new BDD that has the variable(s)
assigned.  You can just use the old BDD to get the unrestricted BDD.

b =3D a.restrict(...);
System.out.println("This is the restricted BDD: "+b.toString());
System.out.println("This is the unrestricted BDD: "+a.toString());

-John


On 4/2/06, Islam Elkabani <iel...@cs...> wrote:
>
>
>
> Hi,
>
> I am a new buddy user and I want to use buddy's ROBDDs in some research
> project. In this project I need to use the restrict function to assign a
> value to an ordered variable in the BDD and also I need something to
> un-restrict or in other words to backtrack from restricting the variable
> (returning the BDD to its state before restricting some variable in it). =
Is
> that possible in Buddy? if not, do you beleive that I could implement thi=
s
> feature in Buddy and how?
> I would really appreciate your help.
>
> Thanks,
>
> Islam Elkabani.

[Buddy-users] Un-restrict

[Islam E. <iel...@cs...>]

Hi,

I am a new buddy user and I want to use buddy's ROBDDs in some research =
project. In this project I need to use the restrict function to assign a =
value to an ordered variable in the BDD and also I need something to =
un-restrict or in other words to backtrack from restricting the variable =
(returning the BDD to its state before restricting some variable in it). =
Is that possible in Buddy? if not, do you beleive that I could implement =
this feature in Buddy and how?=20
I would really appreciate your help.

Thanks,

Islam Elkabani. 

[Buddy-users] Equivalent to CUDD's FindEssential

[Werner M. <wer...@o2...>]

Hi,

I could not find a BuDDy function which calculates the essential cube of
a given BDD. CUDD has a function called Cudd_FindEssential which does
this. Is there a (simple) way to get the same information for a BuDDy BDD?

Werner


CUDD Documentation for Cudd_FindEssential:

Returns the cube of the essential variables. A positive
literal means that the variable must be set to 1 for the function to be
1. A negative literal means that the variable must be set to 0 for the
function to be 1. Returns a pointer to the cube BDD if successful;
NULL otherwise.

[Buddy-users] BuDDy2.4: fdd_printset to slow

[<bud...@fr...>]

Hello,=0A=0AI'm using BuDDy2.4 for Points-To analysis. BuDDy works fine, fo=
r bigsets too. But when I want to put out my Points-To set with fdd_printse=
tor fdd_fprintset, it takes very long time for big sets. For example:with 1=
00.000  bdd nodes takes solving only a few seconds andfdd_printset takes ab=
out 30-45 minutes!=0A=0AIs it so, or do I anything wrong?=0ACan I use anoth=
er function to put my  fdd variables out faster?=0A=0AThanks=0A=0AAlex=0A=
=0AIhr Traumpartner ist nur einen Klick entfernt. 1 Million Singles warten =
auf Sie in=0ADeutschlands beliebtester Partnerboerse:=0Ahttp://singles.free=
net.de/index.html?pid=3D11512=0A

[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
>
> 

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

[Alexandre Duret-L. <ad...@sr...>]

>>> "QY" == Qin Yang <qin...@ya...> writes:

 QY> Dear Haim Cohen,
 QY> I am a new user of BuDDy. To find all the satisfying
 QY> assignments of a bdd, I find that "bdd_allsat()" is
 QY> not enough for me. For example, 
 QY> bdd a = bdd_ithvar(0);
 QY> bdd b = bdd_ithvar(1);
 QY> bdd c = bdd_ithvar(2);

 QY> bdd x = a & !b & c;
 QY> x |= a & !b & !c;

You can always extract one assignment using bdd_satoneset(), NAND
it out of x, and iterate until x is false.

 bdd varset = a & b & c;
 while (x != bddfalse)
 {
   bdd one = bdd_satoneset(x, varset, bddtrue);
   x -= one;
   // ... do what you want with `one' ...
 }

Surely that must be less effective that a bdd_allsat()-style
interface: bdd_satoneset() and -= will both recurse into the BDD,
on each iteration, while I assume bdd_allsat() does it only once.
-- 
Alexandre Duret-Lutz

[Buddy-users] A simple question about BuDDy

[Qin Y. <qin...@ya...>]

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 
 

[Buddy-users] bug in buddy library: reordering

[John W. <jw...@st...>]

I have tracked down a tricky bug involving garbage collection and variable
reordering.  When calling setvarorder(), some BDDs are not getting
reordered, leading to invalid BDDs because the levels are no longer
monotonically increasing.  This bug affects all BDD reordering (swapvar,
dynamic reordering, etc.)

This is a serious bug because it will cause the library to silently give
incorrect results to BDD operations.

The problem seems to be in the construction of the dependency imatrix.
mark_roots() is supposed to mark the externally-accessible BDD references
and mark which variables depend on each other in the imatrix.

mark_roots() calls addref_rec(), which is supposed to recurse down the BDD,
adding variable dependencies.  mark_roots() uses "REF(r) == 0" to test
whether or not it has already visited and therefore computed the
dependencies for a BDD node.

Herein lies the problem. If an internal BDD node has an external reference,
its refcount will not be zero, and mark_roots() will assume it has computed
the imatrix dependencies when it has not.

The whole mark_roots() process seems to assume that it can use the refcount
field as a marker for BDD nodes.  This is wrong and we should think about
the right way to do this. We may need to use an external table instead.

Coming up with a test case that exhibits the bug is nontrivial because the
BDDs must be allocated in a non-sequential order.  For this to happen, there
must have been a garbage collection in the past where nodes were reclaimed
and new nodes were given numbers before old nodes.  Thus, all of the test
cases that exhibit the bug are rather large.

-John