Overview  Package   Class  Use  Deprecated  Index
Home >> All >> org >> sf >> [ javabdd overview ]	PREV CLASS  NEXT CLASS
SUMMARY:  JAVADOC |  SOURCE |  DOWNLOAD | NESTED | FIELD | CONSTR | METHOD	DETAIL: FIELD | CONSTR | METHOD

---

org.sf.javabdd
Class BuDDyFactory  

java.lang.Object
  org.sf.javabdd.BDDFactory
      org.sf.javabdd.BuDDyFactory

---

public class BuDDyFactory

extends BDDFactory

An implementation of BDDFactory that relies on the BuDDy library through a native interface. You can use this by calling the "BuDDyFactory.init()" method with the desired arguments. This will return you an instance of the BDDFactory class that you can use. Call "done()" on that instance when you are finished.

This class (and the BuDDy library) do NOT support multithreading. Furthermore, there can be only one instance active at a time. You can only call "init()" again after you have called "done()" on the original instance. It is not recommended to call "init()" again after calling "done()" unless you are _completely_ sure that all BDD objects that reference the old factory have been freed.

If you really need multiple BDD factories, consider using the JavaFactory class for the additional BDD factories --- JavaFactory can have multiple factory instances active at a time.

Version:

$Id: BuDDyFactory.java,v 1.32 2003/11/01 05:16:33 joewhaley Exp $

---

Nested Class Summary
(package private) static class	BuDDyFactory.BuDDyBDD
(package private) static class	BuDDyFactory.BuDDyBDDBitVector
(package private) static class	BuDDyFactory.BuDDyBDDDomain
(package private) static class	BuDDyFactory.BuDDyBDDPairing

 

Nested classes inherited from class org.sf.javabdd.BDDFactory

BDDFactory.BDDOp, BDDFactory.ReorderMethod

 

Field Summary
private static BuDDyFactory	INSTANCE

 

Fields inherited from class org.sf.javabdd.BDDFactory

and, biimp, diff, domain, fdvarnum, firstbddvar, imp, invimp, less, nand, nor, or, REORDER_NONE, REORDER_RANDOM, REORDER_SIFT, REORDER_SIFTITE, REORDER_WIN2, REORDER_WIN2ITE, REORDER_WIN3, REORDER_WIN3ITE, xor

 

Constructor Summary
private	BuDDyFactory()

 

Method Summary
void	addVarBlock(BDD var, boolean fixed)           Adds a new variable block for reordering.
void	addVarBlock(int first, int last, boolean fixed)           Adds a new variable block for reordering.
private static void	addVarBlock0(int var, boolean fixed)
private static void	addVarBlock1(int first, int last, boolean fixed)
void	autoReorder(BDDFactory.ReorderMethod method)           Enables automatic reordering.
void	autoReorder(BDDFactory.ReorderMethod method, int max)           Enables automatic reordering with the given (maximum) number of reorderings.
private static void	autoReorder0(int method)
private static void	autoReorder1(int method, int max)
BDD	buildCube(int value, int[] var)           Build a cube from an array of variables.
BDD	buildCube(int value, java.util.List var)           Build a cube from an array of variables.
private static int	buildCube0(int value, int[] var)
private static int	buildCube1(int value, int[] var)
void	clearVarBlocks()           Clears all the variable blocks that have been defined by calls to addVarBlock.
private static void	clearVarBlocks0()
protected  BDDBitVector	createBitVector(int a)
protected  BDDDomain	createDomain(int a, long b)           Implementors must implement this factory method to create BDDDomain objects of the correct type.
void	disableReorder()           Disable automatic reordering until enableReorder is called.
private static void	disableReorder0()
void	done()           Resets the BDD package.
private static void	done0()
void	enableReorder()           Enable automatic reordering after a call to disableReorder.
private static void	enableReorder0()
int	extVarNum(int num)           Add extra BDD variables.
private static int	extVarNum0(int num)
int	getAllocNum()           Get the number of allocated nodes.
private static int	getAllocNum0()
int	getNodeNum()           Get the number of active nodes in use.
private static int	getNodeNum0()
BDDFactory.ReorderMethod	getReorderMethod()           Returns the current reorder method as defined by autoReorder.
private static int	getReorderMethod0()
int	getReorderTimes()           Returns the number of allowed reorderings left.
private static int	getReorderTimes0()
static BDDFactory	init(int nodenum, int cachesize)           Initializes a BDD factory with the given initial node table size and operation cache size.
protected  void	initialize(int nodenum, int cachesize)           Compare to bdd_init.
private static void	initialize0(int nodenum, int cachesize)
boolean	isInitialized()           Compare to bdd_isrunning.
private static boolean	isInitialized0()
BDD	ithVar(int var)           Returns a BDD representing the I'th variable.
private static int	ithVar0(int var)
int	level2Var(int level)           Compare to bdd_level2var.
private static int	level2Var0(int level)
BDD	load(java.lang.String filename)           Loads a BDD from a file.
private static int	load0(java.lang.String filename)
static void	main(java.lang.String[] args)
BDDPairing	makePair()           Compare to bdd_newpair.
private static long	makePair0()
BDD	makeSet(int[] v)           Builds a BDD variable set from an integer array.
private static int	makeSet0(int[] var)
BDD	nithVar(int var)           Returns a BDD representing the negation of the I'th variable.
private static int	nithVar0(int var)
int	nodeCount(java.util.Collection r)           Counts the number of shared nodes in a collection of BDDs.
private static int	nodeCount0(int[] a)
BDD	one()           Get the constant true BDD.
void	printAll()           Prints all used entries in the node table.
private static void	printAll0()
void	printOrder()           Prints an indented list of the variable blocks.
private static void	printOrder0()
void	printStat()           Print cache statistics.
private static void	printStat0()
void	printTable(BDD b)           Prints the node table entries used by a BDD.
private static void	printTable0(int b)
private static void	registerNatives()
void	reorder(BDDFactory.ReorderMethod method)           Compare to bdd_reorder.
private static void	reorder0(int method)
int	reorderGain()           Calculate the gain in size after a reordering.
private static int	reorderGain0()
int	reorderVerbose(int v)           Enables verbose information about reordering.
private static int	reorderVerbose0(int v)
void	save(java.lang.String filename, BDD b)           Saves a BDD to a file.
private static void	save0(java.lang.String filename, int b)
int	setCacheRatio(int x)           Sets the cache ratio for the operator caches.
private static int	setCacheRatio0(int x)
int	setMaxIncrease(int x)           Set maximum number of nodes used to increase node table.
private static int	setMaxIncrease0(int x)
int	setMaxNodeNum(int size)           Set the maximum available number of BDD nodes.
private static int	setMaxNodeNum0(int size)
void	setMinFreeNodes(int x)           Set minimum number of nodes to be reclaimed after a garbage collection.
private static void	setMinFreeNodes0(int x)
int	setVarNum(int num)           Set the number of used BDD variables.
private static int	setVarNum0(int num)
void	setVarOrder(int[] neworder)           This function sets the current variable order to be the one defined by neworder.
private static void	setVarOrder0(int[] neworder)
void	swapVar(int v1, int v2)           Compare to bdd_swapvar.
private static void	swapVar0(int v1, int v2)
private static int[]	toBuDDyArray(java.util.Collection c)           Converts collection of BuDDyBDD's into an int array, for passing to native code.
int	var2Level(int var)           Compare to bdd_var2level.
private static int	var2Level0(int var)
void	varBlockAll()           Add a variable block for all variables.
private static void	varBlockAll0()
int	varNum()           Returns the number of defined variables.
private static int	varNum0()
BDD	zero()           Get the constant false BDD.

 

Methods inherited from class org.sf.javabdd.BDDFactory

buildVector, buildVector, buildVector, buildVector, clearAllDomains, constantVector, constantVector, extDomain, extDomain, fillInVarIndices, finalize, getDomain, init, makePair, makePair, makePair, makeSet, makeVarOrdering, numberOfDomains, overlapDomain

 

Methods inherited from class java.lang.Object

clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

 

Field Detail

INSTANCE

private static BuDDyFactory INSTANCE

Constructor Detail

BuDDyFactory

private BuDDyFactory()

Method Detail

init

public static BDDFactory init(int nodenum,
                              int cachesize)

Description copied from class: BDDFactory

Initializes a BDD factory with the given initial node table size and operation cache size. Tries to use the "buddy" native library; if it fails, it falls back to the "java" library.

---

registerNatives

private static void registerNatives()

---

zero

public BDD zero()

Description copied from class: BDDFactory

Get the constant false BDD. Compare to bdd_false.

Specified by:

zero in class BDDFactory

---

one

public BDD one()

Description copied from class: BDDFactory

Get the constant true BDD. Compare to bdd_true.

Specified by:

one in class BDDFactory

---

toBuDDyArray

private static int[] toBuDDyArray(java.util.Collection c)

Converts collection of BuDDyBDD's into an int array, for passing to native code.

---

buildCube

public BDD buildCube(int value,
                     java.util.List var)

Description copied from class: BDDFactory

Build a cube from an array of variables. Compare to bdd_buildcube.

Overrides:

buildCube in class BDDFactory

---

buildCube0

private static int buildCube0(int value,
                              int[] var)

---

buildCube

public BDD buildCube(int value,
                     int[] var)

Description copied from class: BDDFactory

Build a cube from an array of variables. Compare to bdd_ibuildcube.

Overrides:

buildCube in class BDDFactory

---

buildCube1

private static int buildCube1(int value,
                              int[] var)

---

makeSet

public BDD makeSet(int[] v)

Description copied from class: BDDFactory

Builds a BDD variable set from an integer array. The integer array v holds the variable numbers. The BDD variable set is represented by a conjunction of all the variables in their positive form. Compare to bdd_makeset.

Overrides:

makeSet in class BDDFactory

---

makeSet0

private static int makeSet0(int[] var)

---

initialize

protected void initialize(int nodenum,
                          int cachesize)

Description copied from class: BDDFactory

Compare to bdd_init.

Specified by:

initialize in class BDDFactory

---

initialize0

private static void initialize0(int nodenum,
                                int cachesize)

---

isInitialized

public boolean isInitialized()

Description copied from class: BDDFactory

Compare to bdd_isrunning.

Specified by:

isInitialized in class BDDFactory

---

isInitialized0

private static boolean isInitialized0()

---

done

public void done()

Description copied from class: BDDFactory

Resets the BDD package. This function frees all memory used by the BDD package and resets the package to its initial state. Compare to bdd_done.

Specified by:

done in class BDDFactory

---

done0

private static void done0()

---

setMaxNodeNum

public int setMaxNodeNum(int size)

Description copied from class: BDDFactory

Set the maximum available number of BDD nodes. Compare to bdd_setmaxnodenum.

Specified by:

setMaxNodeNum in class BDDFactory

---

setMaxNodeNum0

private static int setMaxNodeNum0(int size)

---

setMinFreeNodes

public void setMinFreeNodes(int x)

Description copied from class: BDDFactory

Set minimum number of nodes to be reclaimed after a garbage collection. The range of x is 0..100. The default is 20. Compare to bdd_setminfreenodes.

Specified by:

setMinFreeNodes in class BDDFactory

---

setMinFreeNodes0

private static void setMinFreeNodes0(int x)

---

setMaxIncrease

public int setMaxIncrease(int x)

Description copied from class: BDDFactory

Set maximum number of nodes used to increase node table. Compare to bdd_setmaxincrease.

Specified by:

setMaxIncrease in class BDDFactory

---

setMaxIncrease0

private static int setMaxIncrease0(int x)

---

setCacheRatio

public int setCacheRatio(int x)

Description copied from class: BDDFactory

Sets the cache ratio for the operator caches. Compare to bdd_setcacheratio.

Specified by:

setCacheRatio in class BDDFactory

---

setCacheRatio0

private static int setCacheRatio0(int x)

---

varNum

public int varNum()

Description copied from class: BDDFactory

Returns the number of defined variables. Compare to bdd_varnum.

Specified by:

varNum in class BDDFactory

---

varNum0

private static int varNum0()

---

setVarNum

public int setVarNum(int num)

Description copied from class: BDDFactory

Set the number of used BDD variables. It can be called more than one time, but only to increase the number of variables. Compare to bdd_setvarnum.

Specified by:

setVarNum in class BDDFactory

---

setVarNum0

private static int setVarNum0(int num)

---

extVarNum

public int extVarNum(int num)

Description copied from class: BDDFactory

Add extra BDD variables. Extends the current number of allocated BDD variables with num extra variables. Compare to bdd_extvarnum.

Overrides:

extVarNum in class BDDFactory

---

extVarNum0

private static int extVarNum0(int num)

---

ithVar

public BDD ithVar(int var)

Description copied from class: BDDFactory

Returns a BDD representing the I'th variable. (One node with the children true and false). The requested variable must be in the (zero-indexed) range defined by setVarNum. Compare to bdd_ithvar.

Specified by:

ithVar in class BDDFactory

---

ithVar0

private static int ithVar0(int var)

---

nithVar

public BDD nithVar(int var)

Description copied from class: BDDFactory

Returns a BDD representing the negation of the I'th variable. (One node with the children false and true). The requested variable must be in the (zero- indexed) range defined by setVarNum. Compare to bdd_nithvar.

Specified by:

nithVar in class BDDFactory

---

nithVar0

private static int nithVar0(int var)

---

swapVar

public void swapVar(int v1,
                    int v2)

Description copied from class: BDDFactory

Compare to bdd_swapvar.

Specified by:

swapVar in class BDDFactory

---

swapVar0

private static void swapVar0(int v1,
                             int v2)

---

makePair

public BDDPairing makePair()

Description copied from class: BDDFactory

Compare to bdd_newpair.

Specified by:

makePair in class BDDFactory

---

makePair0

private static long makePair0()

---

printAll

public void printAll()

Description copied from class: BDDFactory

Prints all used entries in the node table. Compare to bdd_printall.

Specified by:

printAll in class BDDFactory

---

printAll0

private static void printAll0()

---

printTable

public void printTable(BDD b)

Description copied from class: BDDFactory

Prints the node table entries used by a BDD. Compare to bdd_printtable.

Specified by:

printTable in class BDDFactory

---

printTable0

private static void printTable0(int b)

---

load

public BDD load(java.lang.String filename)

Description copied from class: BDDFactory

Loads a BDD from a file. Compare to bdd_load.

Specified by:

load in class BDDFactory

---

load0

private static int load0(java.lang.String filename)

---

save

public void save(java.lang.String filename,
                 BDD b)

Description copied from class: BDDFactory

Saves a BDD to a file. Compare to bdd_save.

Specified by:

save in class BDDFactory

---

save0

private static void save0(java.lang.String filename,
                          int b)

---

level2Var

public int level2Var(int level)

Description copied from class: BDDFactory

Compare to bdd_level2var.

Specified by:

level2Var in class BDDFactory

---

level2Var0

private static int level2Var0(int level)

---

var2Level

public int var2Level(int var)

Description copied from class: BDDFactory

Compare to bdd_var2level.

Specified by:

var2Level in class BDDFactory

---

var2Level0

private static int var2Level0(int var)

---

reorder

public void reorder(BDDFactory.ReorderMethod method)

Description copied from class: BDDFactory

Compare to bdd_reorder.

Specified by:

reorder in class BDDFactory

---

reorder0

private static void reorder0(int method)

---

autoReorder

public void autoReorder(BDDFactory.ReorderMethod method)

Description copied from class: BDDFactory

Enables automatic reordering. If method is REORDER_NONE then automatic reordering is disabled. Compare to bdd_autoreorder.

Specified by:

autoReorder in class BDDFactory

---

autoReorder0

private static void autoReorder0(int method)

---

autoReorder

public void autoReorder(BDDFactory.ReorderMethod method,
                        int max)

Description copied from class: BDDFactory

Enables automatic reordering with the given (maximum) number of reorderings. If method is REORDER_NONE then automatic reordering is disabled. Compare to bdd_autoreorder_times.

Specified by:

autoReorder in class BDDFactory

---

autoReorder1

private static void autoReorder1(int method,
                                 int max)

---

getReorderMethod

public BDDFactory.ReorderMethod getReorderMethod()

Description copied from class: BDDFactory

Returns the current reorder method as defined by autoReorder. Compare to bdd_getreorder_method.

Specified by:

getReorderMethod in class BDDFactory

---

getReorderMethod0

private static int getReorderMethod0()

---

getReorderTimes

public int getReorderTimes()

Description copied from class: BDDFactory

Returns the number of allowed reorderings left. This value can be defined by autoReorder. Compare to bdd_getreorder_times.

Specified by:

getReorderTimes in class BDDFactory

---

getReorderTimes0

private static int getReorderTimes0()

---

disableReorder

public void disableReorder()

Description copied from class: BDDFactory

Disable automatic reordering until enableReorder is called. Reordering is enabled by default as soon as any variable blocks have been defined. Compare to bdd_disable_reorder.

Specified by:

disableReorder in class BDDFactory

---

disableReorder0

private static void disableReorder0()

---

enableReorder

public void enableReorder()

Description copied from class: BDDFactory

Enable automatic reordering after a call to disableReorder. Compare to bdd_enable_reorder

Specified by:

enableReorder in class BDDFactory

---

enableReorder0

private static void enableReorder0()

---

reorderVerbose

public int reorderVerbose(int v)

Description copied from class: BDDFactory

Enables verbose information about reordering. A value of zero means no information, one means some information and greater than one means lots of information.

Specified by:

reorderVerbose in class BDDFactory

---

reorderVerbose0

private static int reorderVerbose0(int v)

---

setVarOrder

public void setVarOrder(int[] neworder)

Description copied from class: BDDFactory

This function sets the current variable order to be the one defined by neworder. The variable parameter neworder is interpreted as a sequence of variable indices and the new variable order is exactly this sequence. The array must contain all the variables defined so far. If, for instance the current number of variables is 3 and neworder contains [1; 0; 2] then the new variable order is v1

Specified by:

setVarOrder in class BDDFactory

---

setVarOrder0

private static void setVarOrder0(int[] neworder)

---

addVarBlock

public void addVarBlock(BDD var,
                        boolean fixed)

Description copied from class: BDDFactory

Adds a new variable block for reordering. Creates a new variable block with the variables in the variable set var. The variables in var must be contiguous. The fixed parameter sets the block to be fixed (no reordering of its child blocks is allowed) or free, Compare to bdd_addvarblock.

Specified by:

addVarBlock in class BDDFactory

---

addVarBlock0

private static void addVarBlock0(int var,
                                 boolean fixed)

---

addVarBlock

public void addVarBlock(int first,
                        int last,
                        boolean fixed)

Description copied from class: BDDFactory

Adds a new variable block for reordering. Creates a new variable block with the variables numbered first through last, inclusive. The fixed parameter sets the block to be fixed (no reordering of its child blocks is allowed) or free, Compare to bdd_intaddvarblock.

Specified by:

addVarBlock in class BDDFactory

---

addVarBlock1

private static void addVarBlock1(int first,
                                 int last,
                                 boolean fixed)

---

varBlockAll

public void varBlockAll()

Description copied from class: BDDFactory

Add a variable block for all variables. Adds a variable block for all BDD variables declared so far. Each block contains one variable only. More variable blocks can be added later with the use of addVarBlock -- in this case the tree of variable blocks will have the blocks of single variables as the leafs. Compare to bdd_varblockall.

Specified by:

varBlockAll in class BDDFactory

---

varBlockAll0

private static void varBlockAll0()

---

clearVarBlocks

public void clearVarBlocks()

Description copied from class: BDDFactory

Clears all the variable blocks that have been defined by calls to addVarBlock. Compare to bdd_clrvarblocks.

Specified by:

clearVarBlocks in class BDDFactory

---

clearVarBlocks0

private static void clearVarBlocks0()

---

printOrder

public void printOrder()

Description copied from class: BDDFactory

Prints an indented list of the variable blocks. Compare to bdd_printorder.

Specified by:

printOrder in class BDDFactory

---

printOrder0

private static void printOrder0()

---

nodeCount

public int nodeCount(java.util.Collection r)

Description copied from class: BDDFactory

Counts the number of shared nodes in a collection of BDDs. Counts all distinct nodes that are used in the BDDs -- if a node is used in more than one BDD then it only counts once. Compare to bdd_anodecount.

Specified by:

nodeCount in class BDDFactory

---

nodeCount0

private static int nodeCount0(int[] a)

---

getAllocNum

public int getAllocNum()

Description copied from class: BDDFactory

Get the number of allocated nodes. This includes both dead and active nodes. Compare to bdd_getallocnum.

Specified by:

getAllocNum in class BDDFactory

---

getAllocNum0

private static int getAllocNum0()

---

getNodeNum

public int getNodeNum()

Description copied from class: BDDFactory

Get the number of active nodes in use. Note that dead nodes that have not been reclaimed yet by a garbage collection are counted as active. Compare to bdd_getnodenum

Specified by:

getNodeNum in class BDDFactory

---

getNodeNum0

private static int getNodeNum0()

---

reorderGain

public int reorderGain()

Description copied from class: BDDFactory

Calculate the gain in size after a reordering. The value returned is (100*(A-B))/A, where A is previous number of used nodes and B is current number of used nodes. Compare to bdd_reorder_gain.

Specified by:

reorderGain in class BDDFactory

---

reorderGain0

private static int reorderGain0()

---

printStat

public void printStat()

Description copied from class: BDDFactory

Print cache statistics. Compare to bdd_printstat.

Specified by:

printStat in class BDDFactory

---

printStat0

private static void printStat0()

---

createDomain

protected BDDDomain createDomain(int a,
                                 long b)

Description copied from class: BDDFactory

Implementors must implement this factory method to create BDDDomain objects of the correct type.

Specified by:

createDomain in class BDDFactory

---

createBitVector

protected BDDBitVector createBitVector(int a)

Specified by:

createBitVector in class BDDFactory

---

main

public static void main(java.lang.String[] args)

---

Overview  Package   Class  Use  Deprecated  Index
Home >> All >> org >> sf >> [ javabdd overview ]	PREV CLASS  NEXT CLASS
SUMMARY:  JAVADOC |  SOURCE |  DOWNLOAD | NESTED | FIELD | CONSTR | METHOD	DETAIL: FIELD | CONSTR | METHOD

---