|
|||||||||
| 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 BDDFactory
java.lang.Objectorg.sf.javabdd.BDDFactory
- Direct Known Subclasses:
- BuDDyFactory, CUDDFactory, JavaFactory, TestBDDFactory, TypedBDDFactory
- public abstract class BDDFactory
- extends java.lang.Object
Interface for the creation and manipulation of BDDs.
- Version:
- $Id: BDDFactory.java,v 1.16 2003/11/01 00:45:43 joewhaley Exp $
| Nested Class Summary | |
static class |
BDDFactory.BDDOp
Enumeration class for binary operations on BDDs. |
static class |
BDDFactory.ReorderMethod
Enumeration class for method reordering techniques. |
| Field Summary | |
static BDDFactory.BDDOp |
and
Logical 'and'. |
static BDDFactory.BDDOp |
biimp
Logical 'bi-implication'. |
static BDDFactory.BDDOp |
diff
Set difference. |
protected BDDDomain[] |
domain
FINITE DOMAINS |
protected int |
fdvarnum
|
protected int |
firstbddvar
|
static BDDFactory.BDDOp |
imp
Logical 'implication'. |
static BDDFactory.BDDOp |
invimp
Inverse implication. |
static BDDFactory.BDDOp |
less
Less than. |
static BDDFactory.BDDOp |
nand
Logical 'nand'. |
static BDDFactory.BDDOp |
nor
Logical 'nor'. |
static BDDFactory.BDDOp |
or
Logical 'or'. |
static BDDFactory.ReorderMethod |
REORDER_NONE
No reordering. |
static BDDFactory.ReorderMethod |
REORDER_RANDOM
Selects a random position for each variable. |
static BDDFactory.ReorderMethod |
REORDER_SIFT
Reordering where each block is moved through all possible positions. |
static BDDFactory.ReorderMethod |
REORDER_SIFTITE
Same as REORDER_SIFT, but the process is repeated until no further progress is done. |
static BDDFactory.ReorderMethod |
REORDER_WIN2
Reordering using a sliding window of 2. |
static BDDFactory.ReorderMethod |
REORDER_WIN2ITE
Reordering using a sliding window of 2, iterating until no further progress. |
static BDDFactory.ReorderMethod |
REORDER_WIN3
Reordering using a sliding window of 3. |
static BDDFactory.ReorderMethod |
REORDER_WIN3ITE
Reordering using a sliding window of 3, iterating until no further progress. |
static BDDFactory.BDDOp |
xor
Logical 'xor'. |
| Constructor Summary | |
protected |
BDDFactory()
|
| Method Summary | |
abstract void |
addVarBlock(BDD var,
boolean fixed)
Adds a new variable block for reordering. |
abstract void |
addVarBlock(int first,
int last,
boolean fixed)
Adds a new variable block for reordering. |
abstract void |
autoReorder(BDDFactory.ReorderMethod method)
Enables automatic reordering. |
abstract void |
autoReorder(BDDFactory.ReorderMethod method,
int max)
Enables automatic reordering with the given (maximum) number of reorderings. |
BDD |
buildCube(int value,
int[] variables)
Build a cube from an array of variables. |
BDD |
buildCube(int value,
java.util.List variables)
Build a cube from an array of variables. |
BDDBitVector |
buildVector(BDDDomain d)
|
BDDBitVector |
buildVector(int[] var)
|
BDDBitVector |
buildVector(int bitnum,
boolean b)
|
BDDBitVector |
buildVector(int bitnum,
int offset,
int step)
|
void |
clearAllDomains()
Clear all allocated finite domain blocks that were defined by extDomain() or overlapDomain(). |
abstract void |
clearVarBlocks()
Clears all the variable blocks that have been defined by calls to addVarBlock. |
BDDBitVector |
constantVector(int bitnum,
int val)
|
BDDBitVector |
constantVector(int bitnum,
long val)
|
protected abstract BDDBitVector |
createBitVector(int a)
|
protected abstract BDDDomain |
createDomain(int a,
long b)
Implementors must implement this factory method to create BDDDomain objects of the correct type. |
abstract void |
disableReorder()
Disable automatic reordering until enableReorder is called. |
abstract void |
done()
Resets the BDD package. |
abstract void |
enableReorder()
Enable automatic reordering after a call to disableReorder. |
BDDDomain[] |
extDomain(int[] dom)
Extends the set of finite domain blocks with domains of the given sizes. |
BDDDomain[] |
extDomain(long[] domainSizes)
|
int |
extVarNum(int num)
Add extra BDD variables. |
(package private) static int |
fillInVarIndices(BDDDomain[] doms,
int domainIndex,
int numDomains,
int[][] localOrders,
int bitIndex,
int[] varorder)
|
protected void |
finalize()
Called on an object by the Virtual Machine at most once, at some point after the Object is determined unreachable but before it is destroyed. |
abstract int |
getAllocNum()
Get the number of allocated nodes. |
BDDDomain |
getDomain(int i)
Returns the ith finite domain block, as defined by calls to extDomain(). |
abstract int |
getNodeNum()
Get the number of active nodes in use. |
abstract BDDFactory.ReorderMethod |
getReorderMethod()
Returns the current reorder method as defined by autoReorder. |
abstract int |
getReorderTimes()
Returns the number of allowed reorderings left. |
static BDDFactory |
init(int nodenum,
int cachesize)
Initializes a BDD factory with the given initial node table size and operation cache size. |
static BDDFactory |
init(java.lang.String bddpackage,
int nodenum,
int cachesize)
Initializes a BDD factory of the given type with the given initial node table size and operation cache size. |
protected abstract void |
initialize(int nodenum,
int cachesize)
Compare to bdd_init. |
abstract boolean |
isInitialized()
Compare to bdd_isrunning. |
abstract BDD |
ithVar(int var)
Returns a BDD representing the I'th variable. |
abstract int |
level2Var(int level)
Compare to bdd_level2var. |
abstract BDD |
load(java.lang.String filename)
Loads a BDD from a file. |
abstract BDDPairing |
makePair()
Compare to bdd_newpair. |
BDDPairing |
makePair(BDDDomain oldvar,
BDDDomain newvar)
|
BDDPairing |
makePair(int oldvar,
BDD newvar)
|
BDDPairing |
makePair(int oldvar,
int newvar)
|
BDD |
makeSet(BDDDomain[] v)
Returns a BDD defining all the variable sets used to define the variable blocks in the given array. |
BDD |
makeSet(int[] varset)
Builds a BDD variable set from an integer array. |
int[] |
makeVarOrdering(boolean reverseLocal,
java.lang.String ordering)
|
abstract BDD |
nithVar(int var)
Returns a BDD representing the negation of the I'th variable. |
abstract int |
nodeCount(java.util.Collection r)
Counts the number of shared nodes in a collection of BDDs. |
int |
numberOfDomains()
Returns the number of finite domain blocks defined by calls to extDomain(). |
abstract BDD |
one()
Get the constant true BDD. |
BDDDomain |
overlapDomain(BDDDomain d1,
BDDDomain d2)
This function takes two finit blocks and merges them into a new one, such that the new one is encoded using both sets of BDD variables. |
abstract void |
printAll()
Prints all used entries in the node table. |
abstract void |
printOrder()
Prints an indented list of the variable blocks. |
abstract void |
printStat()
Print cache statistics. |
abstract void |
printTable(BDD b)
Prints the node table entries used by a BDD. |
abstract void |
reorder(BDDFactory.ReorderMethod m)
Compare to bdd_reorder. |
abstract int |
reorderGain()
Calculate the gain in size after a reordering. |
abstract int |
reorderVerbose(int v)
Enables verbose information about reordering. |
abstract void |
save(java.lang.String filename,
BDD var)
Saves a BDD to a file. |
abstract int |
setCacheRatio(int x)
Sets the cache ratio for the operator caches. |
abstract int |
setMaxIncrease(int x)
Set maximum number of nodes used to increase node table. |
abstract int |
setMaxNodeNum(int size)
Set the maximum available number of BDD nodes. |
abstract void |
setMinFreeNodes(int x)
Set minimum number of nodes to be reclaimed after a garbage collection. |
abstract int |
setVarNum(int num)
Set the number of used BDD variables. |
abstract void |
setVarOrder(int[] neworder)
This function sets the current variable order to be the one defined by neworder. |
abstract void |
swapVar(int v1,
int v2)
Compare to bdd_swapvar. |
abstract int |
var2Level(int var)
Compare to bdd_var2level. |
abstract void |
varBlockAll()
Add a variable block for all variables. |
abstract int |
varNum()
Returns the number of defined variables. |
abstract BDD |
zero()
Get the constant false BDD. |
| Methods inherited from class java.lang.Object |
clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
| Field Detail |
and
public static final BDDFactory.BDDOp and
- Logical 'and'.
xor
public static final BDDFactory.BDDOp xor
- Logical 'xor'.
or
public static final BDDFactory.BDDOp or
- Logical 'or'.
nand
public static final BDDFactory.BDDOp nand
- Logical 'nand'.
nor
public static final BDDFactory.BDDOp nor
- Logical 'nor'.
imp
public static final BDDFactory.BDDOp imp
- Logical 'implication'.
biimp
public static final BDDFactory.BDDOp biimp
- Logical 'bi-implication'.
diff
public static final BDDFactory.BDDOp diff
- Set difference.
less
public static final BDDFactory.BDDOp less
- Less than.
invimp
public static final BDDFactory.BDDOp invimp
- Inverse implication.
domain
protected BDDDomain[] domain
- FINITE DOMAINS
fdvarnum
protected int fdvarnum
firstbddvar
protected int firstbddvar
REORDER_NONE
public static final BDDFactory.ReorderMethod REORDER_NONE
- No reordering.
REORDER_WIN2
public static final BDDFactory.ReorderMethod REORDER_WIN2
- Reordering using a sliding window of 2.
REORDER_WIN2ITE
public static final BDDFactory.ReorderMethod REORDER_WIN2ITE
- Reordering using a sliding window of 2, iterating until no further
progress.
REORDER_WIN3
public static final BDDFactory.ReorderMethod REORDER_WIN3
- Reordering using a sliding window of 3.
REORDER_WIN3ITE
public static final BDDFactory.ReorderMethod REORDER_WIN3ITE
- Reordering using a sliding window of 3, iterating until no further
progress.
REORDER_SIFT
public static final BDDFactory.ReorderMethod REORDER_SIFT
- Reordering where each block is moved through all possible positions. The
best of these is then used as the new position. Potentially a very slow
but good method.
REORDER_SIFTITE
public static final BDDFactory.ReorderMethod REORDER_SIFTITE
- Same as REORDER_SIFT, but the process is repeated until no further
progress is done. Can be extremely slow.
REORDER_RANDOM
public static final BDDFactory.ReorderMethod REORDER_RANDOM
- Selects a random position for each variable. Mostly used for debugging
purposes.
| Constructor Detail |
BDDFactory
protected BDDFactory()
| Method Detail |
init
public static BDDFactory init(int nodenum, int cachesize)
- 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.
init
public static BDDFactory init(java.lang.String bddpackage, int nodenum, int cachesize)
- Initializes a BDD factory of the given type with the given initial
node table size and operation cache size. The type is a string that
can be "buddy", "cudd", "java", "test", or a name of a class that
has an init() method that returns a BDDFactory. If it fails, it
falls back to the "java" factory.
zero
public abstract BDD zero()
- Get the constant false BDD.
Compare to bdd_false.
one
public abstract BDD one()
- Get the constant true BDD.
Compare to bdd_true.
buildCube
public BDD buildCube(int value, java.util.List variables)
- Build a cube from an array of variables.
Compare to bdd_buildcube.
buildCube
public BDD buildCube(int value, int[] variables)
- Build a cube from an array of variables.
Compare to bdd_ibuildcube.
makeSet
public BDD makeSet(int[] varset)
- 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.
initialize
protected abstract void initialize(int nodenum,
int cachesize)
- Compare to bdd_init.
isInitialized
public abstract boolean isInitialized()
- Compare to bdd_isrunning.
done
public abstract void done()
- 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.
setMaxNodeNum
public abstract int setMaxNodeNum(int size)
- Set the maximum available number of BDD nodes.
Compare to bdd_setmaxnodenum.
setMinFreeNodes
public abstract void setMinFreeNodes(int x)
- 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.
setMaxIncrease
public abstract int setMaxIncrease(int x)
- Set maximum number of nodes used to increase node table.
Compare to bdd_setmaxincrease.
setCacheRatio
public abstract int setCacheRatio(int x)
- Sets the cache ratio for the operator caches.
Compare to bdd_setcacheratio.
varNum
public abstract int varNum()
- Returns the number of defined variables.
Compare to bdd_varnum.
setVarNum
public abstract int setVarNum(int num)
- 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.
extVarNum
public int extVarNum(int num)
- Add extra BDD variables. Extends the current number of allocated BDD
variables with num extra variables.
Compare to bdd_extvarnum.
ithVar
public abstract BDD ithVar(int var)
- 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.
nithVar
public abstract BDD nithVar(int var)
- 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.
printAll
public abstract void printAll()
- Prints all used entries in the node table.
Compare to bdd_printall.
printTable
public abstract void printTable(BDD b)
- Prints the node table entries used by a BDD.
Compare to bdd_printtable.
load
public abstract BDD load(java.lang.String filename) throws java.io.IOException
- Loads a BDD from a file.
Compare to bdd_load.
save
public abstract void save(java.lang.String filename, BDD var) throws java.io.IOException
- Saves a BDD to a file.
Compare to bdd_save.
level2Var
public abstract int level2Var(int level)
- Compare to bdd_level2var.
var2Level
public abstract int var2Level(int var)
- Compare to bdd_var2level.
reorder
public abstract void reorder(BDDFactory.ReorderMethod m)
- Compare to bdd_reorder.
autoReorder
public abstract void autoReorder(BDDFactory.ReorderMethod method)
- Enables automatic reordering. If method is REORDER_NONE then automatic
reordering is disabled.
Compare to bdd_autoreorder.
autoReorder
public abstract void autoReorder(BDDFactory.ReorderMethod method, int max)
- 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.
getReorderMethod
public abstract BDDFactory.ReorderMethod getReorderMethod()
- Returns the current reorder method as defined by autoReorder.
Compare to bdd_getreorder_method.
getReorderTimes
public abstract int getReorderTimes()
- Returns the number of allowed reorderings left. This value can be
defined by autoReorder.
Compare to bdd_getreorder_times.
disableReorder
public abstract void disableReorder()
- 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.
enableReorder
public abstract void enableReorder()
- Enable automatic reordering after a call to disableReorder.
Compare to bdd_enable_reorder
reorderVerbose
public abstract int reorderVerbose(int v)
- Enables verbose information about reordering. A value of zero means no
information, one means some information and greater than one means lots
of information.
setVarOrder
public abstract void setVarOrder(int[] neworder)
- 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
addVarBlock
public abstract void addVarBlock(BDD var, boolean fixed)
- 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.
addVarBlock
public abstract void addVarBlock(int first,
int last,
boolean fixed)
- 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.
varBlockAll
public abstract void varBlockAll()
- 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.
clearVarBlocks
public abstract void clearVarBlocks()
- Clears all the variable blocks that have been defined by calls to
addVarBlock.
Compare to bdd_clrvarblocks.
printOrder
public abstract void printOrder()
- Prints an indented list of the variable blocks.
Compare to bdd_printorder.
nodeCount
public abstract int nodeCount(java.util.Collection r)
- 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.
getAllocNum
public abstract int getAllocNum()
- Get the number of allocated nodes. This includes both dead and active
nodes.
Compare to bdd_getallocnum.
getNodeNum
public abstract int getNodeNum()
- 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
reorderGain
public abstract int reorderGain()
- 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.
printStat
public abstract void printStat()
- Print cache statistics.
Compare to bdd_printstat.
makePair
public abstract BDDPairing makePair()
- Compare to bdd_newpair.
makePair
public BDDPairing makePair(int oldvar, int newvar)
makePair
public BDDPairing makePair(int oldvar, BDD newvar)
makePair
public BDDPairing makePair(BDDDomain oldvar, BDDDomain newvar)
swapVar
public abstract void swapVar(int v1,
int v2)
- Compare to bdd_swapvar.
createDomain
protected abstract BDDDomain createDomain(int a, long b)
- Implementors must implement this factory method to create BDDDomain
objects of the correct type.
extDomain
public BDDDomain[] extDomain(int[] dom)
- Extends the set of finite domain blocks with domains of the given sizes.
Each entry in domainSizes is the size of a new finite domain which later
on can be used for finite state machine traversal and other operations on
finite domains. Each domain allocates log 2 (|domainSizes[i]|) BDD
variables to be used later. The ordering is interleaved for the domains
defined in each call to extDomain. This means that assuming domain D0
needs 2 BDD variables x1 and x2 , and another domain D1 needs 4 BDD
variables y1, y2, y3 and y4, then the order then will be x1, y1, x2, y2,
y3, y4. The new domains are returned in order. The BDD variables needed
to encode the domain are created for the purpose and do not interfere
with the BDD variables already in use.
Compare to fdd_extdomain.
extDomain
public BDDDomain[] extDomain(long[] domainSizes)
overlapDomain
public BDDDomain overlapDomain(BDDDomain d1, BDDDomain d2)
- This function takes two finit blocks and merges them into a new one, such
that the new one is encoded using both sets of BDD variables.
Compare to fdd_overlapdomain.
makeSet
public BDD makeSet(BDDDomain[] v)
- Returns a BDD defining all the variable sets used to define the variable
blocks in the given array.
Compare to fdd_makeset.
clearAllDomains
public void clearAllDomains()
- Clear all allocated finite domain blocks that were defined by extDomain()
or overlapDomain().
Compare to fdd_clearall.
numberOfDomains
public int numberOfDomains()
- Returns the number of finite domain blocks defined by calls to
extDomain().
Compare to fdd_domainnum.
getDomain
public BDDDomain getDomain(int i)
- Returns the ith finite domain block, as defined by calls to
extDomain().
makeVarOrdering
public int[] makeVarOrdering(boolean reverseLocal,
java.lang.String ordering)
fillInVarIndices
static int fillInVarIndices(BDDDomain[] doms, int domainIndex, int numDomains, int[][] localOrders, int bitIndex, int[] varorder)
finalize
protected void finalize()
throws java.lang.Throwable
- Description copied from class:
java.lang.Object - Called on an object by the Virtual Machine at most once,
at some point after the Object is determined unreachable
but before it is destroyed. You would think that this
means it eventually is called on every Object, but this is
not necessarily the case. If execution terminates
abnormally, garbage collection does not always happen.
Thus you cannot rely on this method to always work.
For finer control over garbage collection, use references
from the
java.lang.refpackage.Virtual Machines are free to not call this method if they can determine that it does nothing important; for example, if your class extends Object and overrides finalize to do simply
super.finalize().finalize() will be called by a java.lang.Thread that has no locks on any Objects, and may be called concurrently. There are no guarantees on the order in which multiple objects are finalized. This means that finalize() is usually unsuited for performing actions that must be thread-safe, and that your implementation must be use defensive programming if it is to always work.
If an Exception is thrown from finalize() during garbage collection, it will be patently ignored and the Object will still be destroyed.
It is allowed, although not typical, for user code to call finalize() directly. User invocation does not affect whether automatic invocation will occur. It is also permitted, although not recommended, for a finalize() method to "revive" an object by making it reachable from normal code again.
Unlike constructors, finalize() does not get called for an object's superclass unless the implementation specifically calls
super.finalize().The default implementation does nothing.
createBitVector
protected abstract BDDBitVector createBitVector(int a)
buildVector
public BDDBitVector buildVector(int bitnum, boolean b)
constantVector
public BDDBitVector constantVector(int bitnum, int val)
constantVector
public BDDBitVector constantVector(int bitnum, long val)
buildVector
public BDDBitVector buildVector(int bitnum, int offset, int step)
buildVector
public BDDBitVector buildVector(BDDDomain d)
buildVector
public BDDBitVector buildVector(int[] var)
|
|||||||||
| Home >> All >> org >> sf >> [ javabdd overview ] | PREV CLASS NEXT CLASS | ||||||||
|
SUMMARY: JAVADOC | SOURCE | DOWNLOAD | NESTED | FIELD | CONSTR | METHOD |
DETAIL: FIELD | CONSTR | METHOD | ||||||||