javabdd-devel — General developer's list.

[Javabdd-devel] Appling filters to variable values

[Sergio <ser...@te...>]

Hi,

 

I am interested in setting values to variables after applying dependencies
to them. I will show what I mean with an example:

 

1.	Create variables

 

BDD x=B.ithVar(0);

BDD y=B.ithVar(1);

...

 

2.	Apply dependencies:

 

x.andWith(y);

..

 

3.	Set some variables values to true or false and obtaining a
satisfying variable assignment with that restriction or filter

 

 

For instance, I would like to get a satisfying variable assignment in which
variables x, y, z, etc. is always true.

 

I have try with x=B.one() but it does not work.

 

Any help?

 

Sincerely,

 

Sergio 

RE: [Javabdd-devel] Memory usage??

[Sergio <ser...@ly...>]

Thank you very much for your quick answer John.

=20

According to de API documentation the method setMaxIncrease(int x) =
receives
as parameter the NUMBER of nodes by which to increase node table after a
garbage collection but it doesn=B4t work with memory.=20

How do you set it to 1 MB then? Do I have an old JaCoP version?


setMaxIncrease

public abstract int setMaxIncrease(int x)

Set maximum number of nodes by which to increase node table after a =
garbage
collection.

Compare to bdd_setmaxincrease.

Parameters:=20

x - maximum number of nodes by which to increase node table=20

Returns:=20

old value

=20

Sincerely,

=20

Sergio

=20

  _____ =20

De: John Whaley [mailto:joe...@gm...]=20
Enviado el: domingo, 22 de enero de 2006 20:39
Para: Sergio
Asunto: Re: [Javabdd-devel] Memory usage??

=20


Hello,

Thanks for the email.

=20

=20
How do we set the maximum table size increase to 1MB?


See BDDFactory.setMaxIncrease().

=20

How do we allow the table to grow only if the node table is more than =
99%
full after a garbage collection?


See BDDFactory.setMinFreeNodes().

Let me know if you have any more questions.=20


-John

=20

[Javabdd-devel] Memory usage??

[Sergio <ser...@ly...>]

Hello,

 

I am trying to get the memory usage of a BDD in java (JFactory).

I have read the paper "Cloning-Based Context-Sensitive Pointer Alias
Analysis Using Binary Decision Diagrams" (John Whaley, Monica S Lam) 

in which is explained a method to get it, however, I am finding really
difficult implementing it :

 

"The memory numbers reported are the sizes of the peak number of live BDD
nodes during the course of the algorithm. 

We measured peak BDD memory usage by setting the initial table size and
maximum table size increase to 1MB,

and only allowed the table to grow if the node table was more than 99% full
after a garbage collection." 

(Cloning-Based Context-Sensitive Pointer Alias Analysis Using Binary
Decision Diagrams , John Whaley, Monica S Lam)

 

How do we set the maximum table size increase to 1MB?

How do we allow the table to grow only if the node table is more than 99%
full after a garbage collection?

Any idea?

Any example?

 

Sincerely,

 

Sergio (Spain)

 

[Javabdd-devel] JFactory use of JavaBDD

[Clint K. <cli...@gm...>]

Hello.  I have a question about using the pure-Java implementation of
JavaBDD with the JFactory class.  From looking at the source code, it
appears to me that every time I say something like:

BDD x =3D foo.and(bar);

(where x, foo, and bar are BDDs)

x will be a new BDD object, even if there is already another BDD
object somewhere that is logically equivalent.  I assume that this is
why I need to use the .equals() method to compare two BDDs instead of
just doing a pointer comparison (=3D=3D).

Is there any way to get around this?  I thought that one of the
advantages of using BDDs was that you don't need to create new BDD
nodes if you aren't creating a node that corresponds to a unique truth
table.  This method in JFactory seems to use a lot of extra memory and
be slower.  Would I be better off using one of the BDDFactories that
uses the C implementations?

Any help will be greatly appreciated!

Clinton Kelly, Ph.D.
Vice President, Advanced Research
Achronix Semiconductor Corporation
http://www.achronix.com

[Javabdd-devel] JavaBDD : BDDPairing

[<jea...@ce...>]

Hello,
can I get some example code with the use of the BDDPairing class with 
the method veccompose of the BDD class.
(the API doc mentions BDDPairing as an abstract class and veccompose as 
an abstract method : do I need to implement them
to use them ? )

Yours faithfully

JF Molderez

[Javabdd-devel] 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