|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object net.sf.javabdd.BDDFactory net.sf.javabdd.TypedBDDFactory
public class TypedBDDFactory
This BDD factory keeps track of what domains each BDD uses, and complains if you try to do an operation where the domains do not match.
BDDFactory
Nested Class Summary | |
---|---|
class |
TypedBDDFactory.TypedBDD
A BDD with types (domains) attached to it. |
class |
TypedBDDFactory.TypedBDDVarSet
|
Nested classes/interfaces inherited from class net.sf.javabdd.BDDFactory |
---|
BDDFactory.BDDOp, BDDFactory.CacheStats, BDDFactory.GCStats, BDDFactory.LoadHash, BDDFactory.ReorderMethod, BDDFactory.ReorderStats |
Field Summary | |
---|---|
static Comparator |
domain_comparator
|
static String |
REVISION
|
Fields inherited from class net.sf.javabdd.BDDFactory |
---|
and, biimp, cachestats, diff, domain, fdvarnum, firstbddvar, gc_callbacks, gcstats, imp, invimp, less, nand, nor, or, reorder_callbacks, REORDER_NONE, REORDER_RANDOM, REORDER_SIFT, REORDER_SIFTITE, REORDER_WIN2, REORDER_WIN2ITE, REORDER_WIN3, REORDER_WIN3ITE, reorderstats, resize_callbacks, tokenizer, xor |
Constructor Summary | |
---|---|
TypedBDDFactory(BDDFactory f)
|
Method Summary | |
---|---|
void |
addVarBlock(int first,
int last,
boolean fixed)
Adds a new variable block for reordering. |
Set |
allDomains()
|
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. |
void |
clearError()
Clears any outstanding error condition. |
void |
clearVarBlocks()
Clears all the variable blocks that have been defined by calls to addVarBlock. |
protected BDDBitVector |
createBitVector(int a)
Implementors must implement this factory method to create BDDBitVector objects of the correct type. |
protected BDDDomain |
createDomain(int a,
BigInteger b)
Implementors must implement this factory method to create BDDDomain objects of the correct type. |
void |
disableReorder()
Disable automatic reordering until enableReorder is called. |
static String |
domainNames(Set dom)
|
void |
done()
This function frees all memory used by the BDD package and resets the package to its uninitialized state. |
void |
enableReorder()
Enable automatic reordering after a call to disableReorder. |
BDDDomain[] |
extDomain(long[] domainSizes)
|
int |
getCacheSize()
Get the current size of the cache, in entries. |
int |
getNodeNum()
Get the number of active nodes in use. |
int |
getNodeTableSize()
Get the number of allocated nodes. |
BDDFactory.ReorderMethod |
getReorderMethod()
Returns the current reorder method as defined by autoReorder. |
int |
getReorderTimes()
Returns the number of allowed reorderings left. |
String |
getVersion()
Get the BDD library version. |
static BDDFactory |
init(int nodenum,
int cachesize)
|
protected void |
initialize(int nodenum,
int cachesize)
Compare to bdd_init. |
boolean |
isInitialized()
Returns true if this BDD factory is initialized, false otherwise. |
BDD |
ithVar(int var)
Returns a BDD representing the I'th variable. |
int |
level2Var(int level)
Convert from a BDD level to a BDD variable. |
BDD |
load(String filename)
Loads a BDD from a file. |
static Map |
makeMap()
|
BDDPairing |
makePair()
Make a new BDDPairing object. |
static Set |
makeSet()
|
static Set |
makeSet(Set s)
|
BDD |
nithVar(int var)
Returns a BDD representing the negation of the I'th variable. |
int |
nodeCount(Collection r)
Counts the number of shared nodes in a collection of BDDs. |
BDD |
one()
Get the constant true BDD. |
void |
printAll()
Prints all used entries in the node table. |
void |
printOrder()
Prints an indented list of the variable blocks. |
void |
printStat()
Print cache statistics. |
void |
printTable(BDD b)
Prints the node table entries used by a BDD. |
void |
reorder(BDDFactory.ReorderMethod m)
Reorder the BDD with the given method. |
int |
reorderGain()
Calculate the gain in size after a reordering. |
int |
reorderVerbose(int v)
Enables verbose information about reordering. |
void |
save(String filename,
BDD var)
Saves a BDD to a file. |
double |
setCacheRatio(double x)
Sets the cache ratio for the operator caches. |
int |
setCacheSize(int size)
Sets cache size. |
void |
setError(int code)
Sets the error condition. |
double |
setIncreaseFactor(double x)
Set factor by which to increase node table after a garbage collection. |
int |
setMaxIncrease(int x)
Set maximum number of nodes by which to increase node table after a garbage collection. |
int |
setMaxNodeNum(int size)
Set the maximum available number of BDD nodes. |
double |
setMinFreeNodes(double x)
Set minimum percentage of nodes to be reclaimed after a garbage collection. |
int |
setNodeTableSize(int size)
Sets the node table size. |
int |
setVarNum(int num)
Set the number of used BDD variables. |
void |
setVarOrder(int[] neworder)
This function sets the current variable order to be the one defined by neworder. |
void |
swapVar(int v1,
int v2)
Swap two variables. |
int |
var2Level(int var)
Convert from a BDD variable to a BDD level. |
void |
varBlockAll()
Add a variable block for all variables. |
int |
varNum()
Returns the number of defined variables. |
BDDDomain |
whichDomain(int var)
|
BDD |
zero()
Get the constant false BDD. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
public static final Comparator domain_comparator
public static final String REVISION
Constructor Detail |
---|
public TypedBDDFactory(BDDFactory f)
Method Detail |
---|
public static BDDFactory init(int nodenum, int cachesize)
public BDD zero()
BDDFactory
Get the constant false BDD.
Compare to bdd_false.
zero
in class BDDFactory
public BDD one()
BDDFactory
Get the constant true BDD.
Compare to bdd_true.
one
in class BDDFactory
protected void initialize(int nodenum, int cachesize)
BDDFactory
Compare to bdd_init.
initialize
in class BDDFactory
nodenum
- the initial number of BDD nodescachesize
- the size of caches used by the BDD operatorspublic boolean isInitialized()
BDDFactory
Returns true if this BDD factory is initialized, false otherwise.
Compare to bdd_isrunning.
isInitialized
in class BDDFactory
public void done()
BDDFactory
This function frees all memory used by the BDD package and resets the package to its uninitialized state. The BDD package is no longer usable after this call.
Compare to bdd_done.
done
in class BDDFactory
public void setError(int code)
BDDFactory
Sets the error condition. This will cause the BDD package to throw an exception at the next garbage collection.
setError
in class BDDFactory
code
- the error code to setpublic void clearError()
BDDFactory
Clears any outstanding error condition.
clearError
in class BDDFactory
public int setMaxNodeNum(int size)
BDDFactory
Set the maximum available number of BDD nodes.
Compare to bdd_setmaxnodenum.
setMaxNodeNum
in class BDDFactory
size
- maximum number of nodes
public int setNodeTableSize(int size)
BDDFactory
Sets the node table size.
setNodeTableSize
in class BDDFactory
size
- new size of table
public int setCacheSize(int size)
BDDFactory
Sets cache size.
setCacheSize
in class BDDFactory
public double setMinFreeNodes(double x)
BDDFactory
Set minimum percentage of nodes to be reclaimed after a garbage collection. If this percentage is not reclaimed, the node table will be grown. The range of x is 0..1. The default is .20.
Compare to bdd_setminfreenodes.
setMinFreeNodes
in class BDDFactory
x
- number from 0 to 1
public double setIncreaseFactor(double x)
BDDFactory
Set factor by which to increase node table after a garbage collection. The amount of growth is still limited by setMaxIncrease().
setIncreaseFactor
in class BDDFactory
x
- factor by which to increase node table after GC
public int setMaxIncrease(int x)
BDDFactory
Set maximum number of nodes by which to increase node table after a garbage collection.
Compare to bdd_setmaxincrease.
setMaxIncrease
in class BDDFactory
x
- maximum number of nodes by which to increase node table
public double setCacheRatio(double x)
BDDFactory
Sets the cache ratio for the operator caches. When the node table grows, operator caches will also grow to maintain the ratio.
Compare to bdd_setcacheratio.
setCacheRatio
in class BDDFactory
x
- cache ratiopublic int varNum()
BDDFactory
Returns the number of defined variables.
Compare to bdd_varnum.
varNum
in class BDDFactory
public int setVarNum(int num)
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.
setVarNum
in class BDDFactory
num
- new number of BDD variables
public BDDDomain whichDomain(int var)
public BDD ithVar(int var)
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.
ithVar
in class BDDFactory
var
- the variable number
public BDD nithVar(int var)
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.
nithVar
in class BDDFactory
var
- the variable number
public void printAll()
BDDFactory
Prints all used entries in the node table.
Compare to bdd_printall.
printAll
in class BDDFactory
public void printTable(BDD b)
BDDFactory
Prints the node table entries used by a BDD.
Compare to bdd_printtable.
printTable
in class BDDFactory
public BDD load(String filename) throws IOException
BDDFactory
Loads a BDD from a file.
Compare to bdd_load.
load
in class BDDFactory
IOException
public void save(String filename, BDD var) throws IOException
BDDFactory
Saves a BDD to a file.
Compare to bdd_save.
save
in class BDDFactory
IOException
public int level2Var(int level)
BDDFactory
Convert from a BDD level to a BDD variable.
Compare to bdd_level2var.
level2Var
in class BDDFactory
public int var2Level(int var)
BDDFactory
Convert from a BDD variable to a BDD level.
Compare to bdd_var2level.
var2Level
in class BDDFactory
public void reorder(BDDFactory.ReorderMethod m)
BDDFactory
Reorder the BDD with the given method.
Compare to bdd_reorder.
reorder
in class BDDFactory
public void autoReorder(BDDFactory.ReorderMethod method)
BDDFactory
Enables automatic reordering. If method is REORDER_NONE then automatic reordering is disabled.
Compare to bdd_autoreorder.
autoReorder
in class BDDFactory
public void autoReorder(BDDFactory.ReorderMethod method, int max)
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.
autoReorder
in class BDDFactory
public BDDFactory.ReorderMethod getReorderMethod()
BDDFactory
Returns the current reorder method as defined by autoReorder.
Compare to bdd_getreorder_method.
getReorderMethod
in class BDDFactory
public int getReorderTimes()
BDDFactory
Returns the number of allowed reorderings left. This value can be defined by autoReorder.
Compare to bdd_getreorder_times.
getReorderTimes
in class BDDFactory
public void disableReorder()
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.
disableReorder
in class BDDFactory
public void enableReorder()
BDDFactory
Enable automatic reordering after a call to disableReorder.
Compare to bdd_enable_reorder.
enableReorder
in class BDDFactory
public int reorderVerbose(int v)
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.
reorderVerbose
in class BDDFactory
v
- the new verbose level
public void setVarOrder(int[] neworder)
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 Note that this operation must walk through the node table many times,
and therefore it is much more efficient to call this when the node table
is small.
setVarOrder
in class BDDFactory
neworder
- new variable order
public void addVarBlock(int first, int last, boolean fixed)
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.
addVarBlock
in class BDDFactory
public void varBlockAll()
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.
varBlockAll
in class BDDFactory
public void clearVarBlocks()
BDDFactory
Clears all the variable blocks that have been defined by calls to addVarBlock.
Compare to bdd_clrvarblocks.
clearVarBlocks
in class BDDFactory
public void printOrder()
BDDFactory
Prints an indented list of the variable blocks.
Compare to bdd_printorder.
printOrder
in class BDDFactory
public int nodeCount(Collection r)
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.
nodeCount
in class BDDFactory
public int getNodeTableSize()
BDDFactory
Get the number of allocated nodes. This includes both dead and active nodes.
Compare to bdd_getallocnum.
getNodeTableSize
in class BDDFactory
public int getNodeNum()
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.
getNodeNum
in class BDDFactory
public int getCacheSize()
BDDFactory
Get the current size of the cache, in entries.
getCacheSize
in class BDDFactory
public int reorderGain()
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.
reorderGain
in class BDDFactory
public void printStat()
BDDFactory
Print cache statistics.
Compare to bdd_printstat.
printStat
in class BDDFactory
public BDDPairing makePair()
BDDFactory
Make a new BDDPairing object.
Compare to bdd_newpair.
makePair
in class BDDFactory
public void swapVar(int v1, int v2)
BDDFactory
Swap two variables.
Compare to bdd_swapvar.
swapVar
in class BDDFactory
protected BDDDomain createDomain(int a, BigInteger b)
BDDFactory
Implementors must implement this factory method to create BDDDomain objects of the correct type.
createDomain
in class BDDFactory
protected BDDBitVector createBitVector(int a)
BDDFactory
Implementors must implement this factory method to create BDDBitVector objects of the correct type.
createBitVector
in class BDDFactory
public BDDDomain[] extDomain(long[] domainSizes)
extDomain
in class BDDFactory
public static Set makeSet()
public static Set makeSet(Set s)
public Set allDomains()
public static Map makeMap()
public static String domainNames(Set dom)
public String getVersion()
BDDFactory
getVersion
in class BDDFactory
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |