net.sf.javabdd.BDDFactory
net.sf.javabdd.BDDFactoryIntImpl
net.sf.javabdd.MicroFactory
|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||
java.lang.Object
public class MicroFactory
BDD factory where each node only takes 16 bytes. This is accomplished by tightly packing the bits and limiting the maximum number of BDD variables to 2^10 = 1024.
Because of the extra computation required for packing/unpacking, this BDD factory is a little slower than JFactory, but it also uses 20% less memory.
| Nested Class Summary | |
|---|---|
static class |
MicroFactory.PairOfInts
|
static class |
MicroFactory.QuadOfInts
|
static class |
MicroFactory.TripleOfInts
|
| Nested classes/interfaces inherited from class net.sf.javabdd.BDDFactoryIntImpl |
|---|
BDDFactoryIntImpl.IntBDD, BDDFactoryIntImpl.IntBDDBitVector, BDDFactoryIntImpl.IntBDDVarSet, BDDFactoryIntImpl.IntBDDVarSetWithFinalizer, BDDFactoryIntImpl.IntBDDWithFinalizer, BDDFactoryIntImpl.IntZDDVarSet, BDDFactoryIntImpl.IntZDDVarSetWithFinalizer |
| Nested classes/interfaces inherited from class net.sf.javabdd.BDDFactory |
|---|
BDDFactory.BDDOp, BDDFactory.CacheStats, BDDFactory.GCStats, BDDFactory.ReorderMethod, BDDFactory.ReorderStats |
| Field Summary | |
|---|---|
static boolean |
FLUSH_CACHE_ON_GC
|
static String |
REVISION
|
| Fields inherited from class net.sf.javabdd.BDDFactoryIntImpl |
|---|
to_free, to_free_length |
| 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 |
| Method Summary | |
|---|---|
protected void |
addref_impl(int v)
|
void |
addVarBlock(int first,
int last,
boolean fixed)
Adds a new variable block for reordering. |
protected int |
apply_impl(int v1,
int v2,
BDDFactory.BDDOp opr)
|
protected int |
applyAll_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
|
protected int |
applyEx_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
|
protected int |
applyUni_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
|
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. |
MicroFactory |
cloneFactory()
|
protected int |
compose_impl(int v1,
int v2,
int var)
|
protected int |
constrain_impl(int v1,
int v2)
|
BDD |
copyNode(BDD that)
Use this function to translate BDD's from a JavaFactory into its clone. |
protected void |
delref_impl(int v)
|
void |
disableReorder()
Disable automatic reordering until enableReorder is called. |
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. |
protected int |
exist_impl(int v1,
int v2)
|
protected int |
forAll_impl(int v1,
int v2)
|
protected int |
fullSatOne_impl(int v)
|
int |
getCacheSize()
Get the current size of the cache, in entries. |
BDDFactory.CacheStats |
getCacheStats()
Return the current cache statistics for this BDD factory. |
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. |
protected int |
high_impl(int v)
|
static BDDFactory |
init(int nodenum,
int cachesize)
|
protected void |
initialize(int initnodesize,
int cs)
Compare to bdd_init. |
protected int |
invalid_bdd_impl()
|
boolean |
isInitialized()
Returns true if this BDD factory is initialized, false otherwise. |
protected int |
ite_impl(int v1,
int v2,
int v3)
|
protected int |
ithVar_impl(int var)
|
protected int |
level_impl(int v)
|
int |
level2Var(int level)
Convert from a BDD level to a BDD variable. |
BDD |
load(BufferedReader in,
int[] translate)
Loads a BDD from the given input, translating BDD variables according to the given map. |
protected int |
low_impl(int v)
|
protected int |
makenode_impl(int lev,
int lo,
int hi)
|
BDDPairing |
makePair()
Make a new BDDPairing object. |
protected int |
nithVar_impl(int var)
|
protected int |
nodeCount_impl(int v)
|
protected int |
nodeCount_impl2(int[] v)
|
protected int |
not_impl(int v1)
|
protected int |
one_impl()
|
protected double |
pathCount_impl(int v)
|
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. |
protected void |
printTable_impl(int v)
|
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. |
protected int |
replace_impl(int v,
BDDPairing p)
|
protected int |
restrict_impl(int v1,
int v2)
|
protected double |
satCount_impl(int v)
|
protected int |
satOne_impl(int v)
|
protected int |
satOne_impl2(int v1,
int v2,
boolean pol)
|
void |
save(BufferedWriter out,
BDD b)
Saves a BDD to an output writer. |
double |
setCacheRatio(double x)
Sets the cache ratio for the operator caches. |
int |
setCacheSize(int v)
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. |
protected int |
simplify_impl(int v1,
int v2)
|
protected int |
support_impl(int v)
|
void |
swapVar(int v1,
int v2)
Swap two variables. |
protected int |
unique_impl(int v1,
int v2)
|
void |
validateAll()
|
void |
validateBDD(BDD b)
|
protected int |
var_impl(int v)
|
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. |
protected int[] |
varProfile_impl(int v)
|
protected int |
veccompose_impl(int v,
BDDPairing p)
|
protected int |
zero_impl()
|
| Methods inherited from class net.sf.javabdd.BDDFactoryIntImpl |
|---|
deferredFree, emptySet, finalize, handleDeferredFree, ithVar, makeBDD, makeBDDVarSet, nithVar, nodeCount, one, printTable, universe_impl, universe, unwrap, unwrap, unwrap, zero |
| Methods inherited from class java.lang.Object |
|---|
clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
| Field Detail |
|---|
public static boolean FLUSH_CACHE_ON_GC
public static final String REVISION
| Method Detail |
|---|
public String getVersion()
BDDFactory
getVersion in class BDDFactory
public static BDDFactory init(int nodenum,
int cachesize)
public BDDPairing makePair()
BDDFactoryMake a new BDDPairing object.
Compare to bdd_newpair.
makePair in class BDDFactoryprotected void addref_impl(int v)
addref_impl in class BDDFactoryIntImplprotected void delref_impl(int v)
delref_impl in class BDDFactoryIntImplprotected int zero_impl()
zero_impl in class BDDFactoryIntImplprotected int one_impl()
one_impl in class BDDFactoryIntImplprotected int invalid_bdd_impl()
invalid_bdd_impl in class BDDFactoryIntImplprotected int var_impl(int v)
var_impl in class BDDFactoryIntImplprotected int level_impl(int v)
level_impl in class BDDFactoryIntImplprotected int low_impl(int v)
low_impl in class BDDFactoryIntImplprotected int high_impl(int v)
high_impl in class BDDFactoryIntImplprotected int ithVar_impl(int var)
ithVar_impl in class BDDFactoryIntImplprotected int nithVar_impl(int var)
nithVar_impl in class BDDFactoryIntImpl
protected int makenode_impl(int lev,
int lo,
int hi)
makenode_impl in class BDDFactoryIntImpl
protected int ite_impl(int v1,
int v2,
int v3)
ite_impl in class BDDFactoryIntImpl
protected int apply_impl(int v1,
int v2,
BDDFactory.BDDOp opr)
apply_impl in class BDDFactoryIntImplprotected int not_impl(int v1)
not_impl in class BDDFactoryIntImpl
protected int applyAll_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
applyAll_impl in class BDDFactoryIntImpl
protected int applyEx_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
applyEx_impl in class BDDFactoryIntImpl
protected int applyUni_impl(int v1,
int v2,
BDDFactory.BDDOp opr,
int v3)
applyUni_impl in class BDDFactoryIntImpl
protected int compose_impl(int v1,
int v2,
int var)
compose_impl in class BDDFactoryIntImpl
protected int constrain_impl(int v1,
int v2)
constrain_impl in class BDDFactoryIntImpl
protected int restrict_impl(int v1,
int v2)
restrict_impl in class BDDFactoryIntImpl
protected int simplify_impl(int v1,
int v2)
simplify_impl in class BDDFactoryIntImplprotected int support_impl(int v)
support_impl in class BDDFactoryIntImpl
protected int exist_impl(int v1,
int v2)
exist_impl in class BDDFactoryIntImpl
protected int forAll_impl(int v1,
int v2)
forAll_impl in class BDDFactoryIntImpl
protected int unique_impl(int v1,
int v2)
unique_impl in class BDDFactoryIntImplprotected int fullSatOne_impl(int v)
fullSatOne_impl in class BDDFactoryIntImpl
protected int replace_impl(int v,
BDDPairing p)
replace_impl in class BDDFactoryIntImpl
protected int veccompose_impl(int v,
BDDPairing p)
veccompose_impl in class BDDFactoryIntImplprotected int nodeCount_impl(int v)
nodeCount_impl in class BDDFactoryIntImplprotected double pathCount_impl(int v)
pathCount_impl in class BDDFactoryIntImplprotected double satCount_impl(int v)
satCount_impl in class BDDFactoryIntImplprotected int satOne_impl(int v)
satOne_impl in class BDDFactoryIntImpl
protected int satOne_impl2(int v1,
int v2,
boolean pol)
satOne_impl2 in class BDDFactoryIntImplprotected int nodeCount_impl2(int[] v)
nodeCount_impl2 in class BDDFactoryIntImplprotected int[] varProfile_impl(int v)
varProfile_impl in class BDDFactoryIntImplprotected void printTable_impl(int v)
printTable_impl in class BDDFactoryIntImpl
protected void initialize(int initnodesize,
int cs)
BDDFactoryCompare to bdd_init.
initialize in class BDDFactoryinitnodesize - the initial number of BDD nodescs - the size of caches used by the BDD operators
public void addVarBlock(int first,
int last,
boolean fixed)
BDDFactoryAdds 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 BDDFactorypublic void varBlockAll()
BDDFactoryAdd 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 BDDFactorypublic void clearVarBlocks()
BDDFactoryClears all the variable blocks that have been defined by calls to addVarBlock.
Compare to bdd_clrvarblocks.
clearVarBlocks in class BDDFactorypublic void printOrder()
BDDFactoryPrints an indented list of the variable blocks.
Compare to bdd_printorder.
printOrder in class BDDFactorypublic int getNodeTableSize()
BDDFactoryGet the number of allocated nodes. This includes both dead and active nodes.
Compare to bdd_getallocnum.
getNodeTableSize in class BDDFactorypublic int setNodeTableSize(int size)
BDDFactorySets the node table size.
setNodeTableSize in class BDDFactorysize - new size of table
public int setCacheSize(int v)
BDDFactorySets cache size.
setCacheSize in class BDDFactorypublic boolean isInitialized()
BDDFactoryReturns true if this BDD factory is initialized, false otherwise.
Compare to bdd_isrunning.
isInitialized in class BDDFactorypublic void done()
BDDFactoryThis 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 BDDFactoryIntImplpublic void setError(int code)
BDDFactorySets the error condition. This will cause the BDD package to throw an exception at the next garbage collection.
setError in class BDDFactorycode - the error code to setpublic void clearError()
BDDFactoryClears any outstanding error condition.
clearError in class BDDFactorypublic int setMaxNodeNum(int size)
BDDFactorySet the maximum available number of BDD nodes.
Compare to bdd_setmaxnodenum.
setMaxNodeNum in class BDDFactorysize - maximum number of nodes
public double setMinFreeNodes(double x)
BDDFactorySet 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 BDDFactoryx - number from 0 to 1
public int setMaxIncrease(int x)
BDDFactorySet maximum number of nodes by which to increase node table after a garbage collection.
Compare to bdd_setmaxincrease.
setMaxIncrease in class BDDFactoryx - maximum number of nodes by which to increase node table
public double setIncreaseFactor(double x)
BDDFactorySet factor by which to increase node table after a garbage collection. The amount of growth is still limited by setMaxIncrease().
setIncreaseFactor in class BDDFactoryx - factor by which to increase node table after GC
public int getNodeNum()
BDDFactoryGet 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 BDDFactorypublic int getCacheSize()
BDDFactoryGet the current size of the cache, in entries.
getCacheSize in class BDDFactorypublic int reorderGain()
BDDFactoryCalculate 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 BDDFactorypublic void printStat()
BDDFactoryPrint cache statistics.
Compare to bdd_printstat.
printStat in class BDDFactorypublic double setCacheRatio(double x)
BDDFactorySets 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 BDDFactoryx - cache ratiopublic int varNum()
BDDFactoryReturns the number of defined variables.
Compare to bdd_varnum.
varNum in class BDDFactorypublic int setVarNum(int num)
BDDFactorySet 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 BDDFactorynum - new number of BDD variables
public void printAll()
BDDFactoryPrints all used entries in the node table.
Compare to bdd_printall.
printAll in class BDDFactory
public BDD load(BufferedReader in,
int[] translate)
throws IOException
BDDFactoryLoads a BDD from the given input, translating BDD variables according to the given map.
Compare to bdd_load.
load in class BDDFactoryin - readertranslate - variable translation map
IOException
public void save(BufferedWriter out,
BDD b)
throws IOException
BDDFactorySaves a BDD to an output writer.
Compare to bdd_save.
save in class BDDFactoryIOExceptionpublic void setVarOrder(int[] neworder)
BDDFactoryThis 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 int level2Var(int level)
BDDFactoryConvert from a BDD level to a BDD variable.
Compare to bdd_level2var.
level2Var in class BDDFactorypublic int var2Level(int var)
BDDFactoryConvert from a BDD variable to a BDD level.
Compare to bdd_var2level.
var2Level in class BDDFactorypublic int getReorderTimes()
BDDFactoryReturns the number of allowed reorderings left. This value can be defined by autoReorder.
Compare to bdd_getreorder_times.
getReorderTimes in class BDDFactorypublic void disableReorder()
BDDFactoryDisable 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 BDDFactorypublic void enableReorder()
BDDFactoryEnable automatic reordering after a call to disableReorder.
Compare to bdd_enable_reorder.
enableReorder in class BDDFactorypublic int reorderVerbose(int v)
BDDFactoryEnables 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 BDDFactoryv - the new verbose level
public void reorder(BDDFactory.ReorderMethod m)
BDDFactoryReorder the BDD with the given method.
Compare to bdd_reorder.
reorder in class BDDFactorypublic void autoReorder(BDDFactory.ReorderMethod method)
BDDFactoryEnables 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)
BDDFactoryEnables 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 void swapVar(int v1,
int v2)
BDDFactorySwap two variables.
Compare to bdd_swapvar.
swapVar in class BDDFactorypublic BDDFactory.ReorderMethod getReorderMethod()
BDDFactoryReturns the current reorder method as defined by autoReorder.
Compare to bdd_getreorder_method.
getReorderMethod in class BDDFactorypublic void validateAll()
public void validateBDD(BDD b)
public MicroFactory cloneFactory()
public BDD copyNode(BDD that)
that - BDD in old factory
public BDDFactory.CacheStats getCacheStats()
BDDFactoryReturn the current cache statistics for this BDD factory.
getCacheStats in class BDDFactory
|
|||||||||
| PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
| SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD | ||||||||