Docjar: A Java Source and Docuemnt Enginecom.*    java.*    javax.*    org.*    all    new    plug-in

Quick Search    Search Deep

org.sf.javabdd
Class TestBDDFactory  view TestBDDFactory download TestBDDFactory.java

java.lang.Object
  extended byorg.sf.javabdd.BDDFactory
      extended byorg.sf.javabdd.TestBDDFactory

public class TestBDDFactory
extends BDDFactory

This BDD factory is used to test other BDD factories. It is a wrapper around two BDD factories, and all operations are performed on both factories. It throws an exception if the results from the two implementations do not match.

Version:
$Id: TestBDDFactory.java,v 1.6 2003/11/01 00:45:43 joewhaley Exp $

Nested Class Summary
 class TestBDDFactory.TestBDD
           
 class TestBDDFactory.TestBDDBitVector
           
 class TestBDDFactory.TestBDDDomain
           
 class TestBDDFactory.TestBDDPairing
           
 
Nested classes inherited from class org.sf.javabdd.BDDFactory
BDDFactory.BDDOp, BDDFactory.ReorderMethod
 
Field Summary
(package private)  BDDFactory f1
           
(package private)  BDDFactory f2
           
 
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
(package private) TestBDDFactory(BDDFactory a, BDDFactory b)
           
 
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.
static void assertSame(BDD b1, BDD b2, java.lang.String s)
           
static void assertSame(boolean b, BDD b1, BDD b2, java.lang.String s)
           
static void assertSame(boolean b, java.lang.String s)
           
 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 clearVarBlocks()
          Clears all the variable blocks that have been defined by calls to addVarBlock.
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.
 void done()
          Resets the BDD package.
 void enableReorder()
          Enable automatic reordering after a call to disableReorder.
 int getAllocNum()
          Get the number of allocated nodes.
 int getNodeNum()
          Get the number of active nodes in use.
 BDDFactory.ReorderMethod getReorderMethod()
          Returns the current reorder method as defined by autoReorder.
 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.
protected  void initialize(int nodenum, int cachesize)
          Compare to bdd_init.
 boolean isInitialized()
          Compare to bdd_isrunning.
 BDD ithVar(int var)
          Returns a BDD representing the I'th variable.
 int level2Var(int level)
          Compare to bdd_level2var.
 BDD load(java.lang.String filename)
          Loads a BDD from a file.
 BDDPairing makePair()
          Compare to bdd_newpair.
 BDD nithVar(int var)
          Returns a BDD representing the negation of the I'th variable.
 int nodeCount(java.util.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)
          Compare to bdd_reorder.
 int reorderGain()
          Calculate the gain in size after a reordering.
 int reorderVerbose(int v)
          Enables verbose information about reordering.
 void save(java.lang.String filename, BDD var)
          Saves a BDD to a file.
 int setCacheRatio(int x)
          Sets the cache ratio for the operator caches.
 int setMaxIncrease(int x)
          Set maximum number of nodes used to increase node table.
 int setMaxNodeNum(int size)
          Set the maximum available number of BDD nodes.
 void setMinFreeNodes(int x)
          Set minimum number of nodes to be reclaimed after a garbage collection.
 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)
          Compare to bdd_swapvar.
 int var2Level(int var)
          Compare to bdd_var2level.
 void varBlockAll()
          Add a variable block for all variables.
 int varNum()
          Returns the number of defined variables.
 BDD zero()
          Get the constant false BDD.
 
Methods inherited from class org.sf.javabdd.BDDFactory
buildCube, buildCube, buildVector, buildVector, buildVector, buildVector, clearAllDomains, constantVector, constantVector, extDomain, extDomain, extVarNum, fillInVarIndices, finalize, getDomain, init, makePair, makePair, makePair, makeSet, makeSet, makeVarOrdering, numberOfDomains, overlapDomain
 
Methods inherited from class java.lang.Object
clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

f1

BDDFactory f1

f2

BDDFactory f2
Constructor Detail

TestBDDFactory

TestBDDFactory(BDDFactory a,
               BDDFactory b)
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.


assertSame

public static final void assertSame(boolean b,
                                    java.lang.String s)

assertSame

public static final void assertSame(BDD b1,
                                    BDD b2,
                                    java.lang.String s)

assertSame

public static final void assertSame(boolean b,
                                    BDD b1,
                                    BDD b2,
                                    java.lang.String s)

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

initialize

protected void initialize(int nodenum,
                          int cachesize)
Description copied from class: BDDFactory
Compare to bdd_init.

Specified by:
initialize in class BDDFactory

isInitialized

public boolean isInitialized()
Description copied from class: BDDFactory
Compare to bdd_isrunning.

Specified by:
isInitialized in class BDDFactory

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

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

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

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

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

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

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

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

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

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

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

load

public BDD load(java.lang.String filename)
         throws java.io.IOException
Description copied from class: BDDFactory
Loads a BDD from a file. Compare to bdd_load.

Specified by:
load in class BDDFactory

save

public void save(java.lang.String filename,
                 BDD var)
          throws java.io.IOException
Description copied from class: BDDFactory
Saves a BDD to a file. Compare to bdd_save.

Specified by:
save in class BDDFactory

level2Var

public int level2Var(int level)
Description copied from class: BDDFactory
Compare to bdd_level2var.

Specified by:
level2Var in class BDDFactory

var2Level

public int var2Level(int var)
Description copied from class: BDDFactory
Compare to bdd_var2level.

Specified by:
var2Level in class BDDFactory

reorder

public void reorder(BDDFactory.ReorderMethod m)
Description copied from class: BDDFactory
Compare to bdd_reorder.

Specified by:
reorder in class BDDFactory

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

printStat

public void printStat()
Description copied from class: BDDFactory
Print cache statistics. Compare to bdd_printstat.

Specified by:
printStat in class BDDFactory

makePair

public BDDPairing makePair()
Description copied from class: BDDFactory
Compare to bdd_newpair.

Specified by:
makePair in class BDDFactory

swapVar

public void swapVar(int v1,
                    int v2)
Description copied from class: BDDFactory
Compare to bdd_swapvar.

Specified by:
swapVar in class BDDFactory

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