net.sf.javabdd
Class BDDFactory

java.lang.Object
  net.sf.javabdd.BDDFactory

Direct Known Subclasses:

BDDFactoryIntImpl, CALFactory, CUDDFactory, TestBDDFactory, TypedBDDFactory

public abstract class BDDFactory
extends Object

Interface for the creation and manipulation of BDDs.

Version:

$Id: BDDFactory.java 476 2007-03-06 06:08:40Z joewhaley $

Author:

John Whaley

See Also:

BDD

Nested Class Summary

static class	BDDFactory.BDDOp Enumeration class for binary operations on BDDs.
static class	BDDFactory.CacheStats Stores statistics about the operator cache.
static class	BDDFactory.GCStats Stores statistics about garbage collections.
protected static class	BDDFactory.LoadHash LoadHash is used to hash during loading.
static class	BDDFactory.ReorderMethod Enumeration class for method reordering techniques.
static class	BDDFactory.ReorderStats Stores statistics about reordering.

Field Summary

static BDDFactory.BDDOp	and Logical 'and'.
static BDDFactory.BDDOp	biimp Logical 'bi-implication'.
protected BDDFactory.CacheStats	cachestats Singleton object for cache statistics.
static BDDFactory.BDDOp	diff Set difference.
protected BDDDomain[]	domain FINITE DOMAINS
protected int	fdvarnum
protected int	firstbddvar
protected List	gc_callbacks CALLBACKS
protected BDDFactory.GCStats	gcstats Singleton object for GC statistics.
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'.
protected List	reorder_callbacks CALLBACKS
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.
protected BDDFactory.ReorderStats	reorderstats Singleton object for reorder statistics.
protected List	resize_callbacks CALLBACKS
protected StringTokenizer	tokenizer Used for tokenization during loading.
static BDDFactory.BDDOp	xor Logical 'xor'.

Constructor Summary

protected

BDDFactory() Construct a new BDDFactory.

Method Summary

void	addVarBlock(BDDVarSet 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.
protected static void	bdd_default_gbchandler(boolean pre, BDDFactory.GCStats s)
protected void	bdd_default_reohandler(boolean prestate, BDDFactory.ReorderStats s)
protected static void	bdd_default_reshandler(int oldsize, int newsize)
BDD	buildCube(int value, int[] variables) Build a cube from an array of variables.
BDD	buildCube(int value, List variables) Build a cube from an array of variables.
BDDBitVector	buildVector(BDDDomain d) Build a bit vector using variables from the given BDD domain.
BDDBitVector	buildVector(int[] var) Build a bit vector using the given variables.
BDDBitVector	buildVector(int bitnum, boolean b) Build a bit vector that is constant true or constant false.
BDDBitVector	buildVector(int bitnum, int offset, int step) Build a bit vector using variables offset, offset+step, offset+2*step, ...
void	clearAllDomains() Clear all allocated finite domain blocks that were defined by extDomain() or overlapDomain().
abstract void	clearError() Clears any outstanding error condition.
abstract void	clearVarBlocks() Clears all the variable blocks that have been defined by calls to addVarBlock.
BDDBitVector	constantVector(int bitnum, BigInteger val)
BDDBitVector	constantVector(int bitnum, long val) Build a bit vector that corresponds to a constant value.
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.
abstract void	disableReorder() Disable automatic reordering until enableReorder is called.
protected void	doCallbacks(List callbacks, Object arg1, Object arg2)
abstract void	done() This function frees all memory used by the BDD package and resets the package to its uninitialized state.
BDDVarSet	emptySet() Get an empty BDDVarSet.
abstract void	enableReorder() Enable automatic reordering after a call to disableReorder.
BDDDomain	extDomain(BigInteger domainSize)
BDDDomain[]	extDomain(BigInteger[] domainSizes)
BDDDomain[]	extDomain(int[] dom) Extends the set of finite domain blocks with domains of the given sizes.
BDDDomain	extDomain(long domainSize) Creates a new finite domain block of the given size.
BDDDomain[]	extDomain(long[] dom)
int	extVarNum(int num) Add extra BDD variables.
protected void	gbc_handler(boolean pre, BDDFactory.GCStats s)
abstract int	getCacheSize() Get the current size of the cache, in entries.
BDDFactory.CacheStats	getCacheStats() Return the current cache statistics for this BDD factory.
BDDDomain	getDomain(int i) Returns the ith finite domain block, as defined by calls to extDomain().
BDDFactory.GCStats	getGCStats() Return the current GC statistics for this BDD factory.
abstract int	getNodeNum() Get the number of active nodes in use.
abstract int	getNodeTableSize() Get the number of allocated nodes.
static String	getProperty(String key, String def)
abstract BDDFactory.ReorderMethod	getReorderMethod() Returns the current reorder method as defined by autoReorder.
BDDFactory.ReorderStats	getReorderStats() Return the current reordering statistics for this BDD factory.
abstract int	getReorderTimes() Returns the number of allowed reorderings left.
int[]	getVarOrder() Gets the current variable order.
abstract String	getVersion() Get the BDD library version.
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(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() Returns true if this BDD factory is initialized, false otherwise.
boolean	isZDD() Returns true if this is a ZDD factory, false otherwise.
abstract BDD	ithVar(int var) Returns a BDD representing the I'th variable.
abstract int	level2Var(int level) Convert from a BDD level to a BDD variable.
BDD	load(BufferedReader ifile) Loads a BDD from the given input.
BDD	load(BufferedReader ifile, int[] translate) Loads a BDD from the given input, translating BDD variables according to the given map.
BDD	load(String filename) Loads a BDD from a file.
protected BDD	loadhash_get(BDDFactory.LoadHash[] lh_table, int lh_nodenum, int key) Gets a BDD from the load hash table.
abstract BDDPairing	makePair() Make a new BDDPairing object.
BDDPairing	makePair(BDDDomain oldvar, BDDDomain newvar) Make a new pairing that maps from one BDD domain to another.
BDDPairing	makePair(int oldvar, BDD newvar) Make a new pairing that maps from one variable to another BDD.
BDDPairing	makePair(int oldvar, int newvar) Make a new pairing that maps from one variable to another.
BDDVarSet	makeSet(BDDDomain[] v) Returns a BDD defining all the variable sets used to define the variable blocks in the given array.
BDDVarSet	makeSet(int[] varset) Builds a BDD variable set from an integer array.
int[]	makeVarOrdering(boolean reverseLocal, String ordering) Creates a variable ordering from a string.
abstract BDD	nithVar(int var) Returns a BDD representing the negation of the I'th variable.
abstract int	nodeCount(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 finite domain 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.
protected String	readNext(BufferedReader ifile) Read the next token from the file.
protected void	registerCallback(List callbacks, Object o, Method m)
void	registerGCCallback(Object o, Method m) Register a callback that is called when garbage collection is about to occur.
void	registerReorderCallback(Object o, Method m) Register a callback that is called when reordering is about to occur.
void	registerResizeCallback(Object o, Method m) Register a callback that is called when node table resizing is about to occur.
abstract void	reorder(BDDFactory.ReorderMethod m) Reorder the BDD with the given method.
abstract int	reorderGain() Calculate the gain in size after a reordering.
abstract int	reorderVerbose(int v) Enables verbose information about reordering.
void	reset() Reset the BDD factory to its initial state.
protected void	resize_handler(int oldsize, int newsize)
protected int	save_rec_original(BufferedWriter out, Map visited, BDD root) Helper function for save().
protected int	save_rec(BufferedWriter out, BitSet visited, BDD root) Helper function for save().
void	save(BufferedWriter out, BDD r) Saves a BDD to an output writer.
void	save(String filename, BDD var) Saves a BDD to a file.
abstract double	setCacheRatio(double x) Sets the cache ratio for the operator caches.
abstract int	setCacheSize(int n) Sets cache size.
abstract void	setError(int code) Sets the error condition.
abstract double	setIncreaseFactor(double x) Set factor by which to increase node table after a garbage collection.
abstract int	setMaxIncrease(int x) Set maximum number of nodes by which to increase node table after a garbage collection.
abstract int	setMaxNodeNum(int size) Set the maximum available number of BDD nodes.
abstract double	setMinFreeNodes(double x) Set minimum percentage of nodes to be reclaimed after a garbage collection.
abstract int	setNodeTableSize(int n) Sets the node table size.
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) Swap two variables.
BDD	universe() Get the constant universe BDD.
protected boolean	unregisterCallback(List callbacks, Object o, Method m)
void	unregisterGCCallback(Object o, Method m) Unregister a garbage collection callback that was previously registered.
void	unregisterReorderCallback(Object o, Method m) Unregister a reorder callback that was previously registered.
void	unregisterResizeCallback(Object o, Method m) Unregister a reorder callback that was previously registered.
abstract int	var2Level(int var) Convert from a BDD variable to a BDD level.
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, finalize, 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.

tokenizer

protected StringTokenizer tokenizer

Used for tokenization during loading.

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.

gcstats

protected BDDFactory.GCStats gcstats

Singleton object for GC statistics.

reorderstats

protected BDDFactory.ReorderStats reorderstats

Singleton object for reorder statistics.

cachestats

protected BDDFactory.CacheStats cachestats

Singleton object for cache statistics.

domain

protected BDDDomain[] domain

FINITE DOMAINS

fdvarnum

protected int fdvarnum

firstbddvar

protected int firstbddvar

gc_callbacks

protected List gc_callbacks

CALLBACKS

reorder_callbacks

protected List reorder_callbacks

CALLBACKS

resize_callbacks

protected List resize_callbacks

CALLBACKS

Constructor Detail

BDDFactory

protected BDDFactory()

Construct a new BDDFactory.

Method Detail

getProperty

public static final String getProperty(String key,
                                       String def)

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.

Parameters:

nodenum - initial node table size

cachesize - operation cache size

Returns:

BDD factory object

init

public static BDDFactory init(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", "cal", "j", "java", "jdd", "test", "typed", 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.

Parameters:

bddpackage - BDD package string identifier

nodenum - initial node table size

cachesize - operation cache size

Returns:

BDD factory object

isZDD

public boolean isZDD()

Returns true if this is a ZDD factory, false otherwise.

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.

universe

public BDD universe()

Get the constant universe BDD. (The universe BDD differs from the one BDD in ZDD mode.)

Compare to bdd_true.

emptySet

public BDDVarSet emptySet()

Get an empty BDDVarSet.

Compare to bdd_true.

buildCube

public BDD buildCube(int value,
                     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./p>

makeSet

public BDDVarSet makeSet(int[] varset)

Builds a BDD variable set from an integer array. The integer array varset 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.

Parameters:

nodenum - the initial number of BDD nodes

cachesize - the size of caches used by the BDD operators

isInitialized

public abstract boolean isInitialized()

Returns true if this BDD factory is initialized, false otherwise.

Compare to bdd_isrunning.

Returns:

true if this BDD factory is initialized

reset

public void reset()

Reset the BDD factory to its initial state. Everything is reallocated from scratch. This is like calling done() followed by initialize().

done

public abstract void done()

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.

setError

public abstract void setError(int code)

Sets the error condition. This will cause the BDD package to throw an exception at the next garbage collection.

Parameters:

code - the error code to set

clearError

public abstract void clearError()

Clears any outstanding error condition.

setMaxNodeNum

public abstract int setMaxNodeNum(int size)

Set the maximum available number of BDD nodes.

Compare to bdd_setmaxnodenum.

Parameters:

size - maximum number of nodes

Returns:

old value

setMinFreeNodes

public abstract double setMinFreeNodes(double x)

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.

Parameters:

x - number from 0 to 1

Returns:

old value

setMaxIncrease

public abstract int setMaxIncrease(int x)

Set maximum number of nodes by which to increase node table after a garbage collection.

Compare to bdd_setmaxincrease.

Parameters:

x - maximum number of nodes by which to increase node table

Returns:

old value

setIncreaseFactor

public abstract double setIncreaseFactor(double x)

Set factor by which to increase node table after a garbage collection. The amount of growth is still limited by setMaxIncrease().

Parameters:

x - factor by which to increase node table after GC

Returns:

old value

setCacheRatio

public abstract double setCacheRatio(double x)

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.

Parameters:

x - cache ratio

setNodeTableSize

public abstract int setNodeTableSize(int n)

Sets the node table size.

Parameters:

n - new size of table

Returns:

old size of table

setCacheSize

public abstract int setCacheSize(int n)

Sets cache size.

Returns:

old cache size

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.

Parameters:

num - new number of BDD variables

Returns:

old number of BDD variables

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.

Parameters:

num - number of BDD variables to add

Returns:

old number of BDD variables

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.

Parameters:

var - the variable number

Returns:

the I'th variable on success, otherwise the constant false BDD

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.

Parameters:

var - the variable number

Returns:

the negated I'th variable on success, otherwise the constant false BDD

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 BDD load(String filename)
         throws IOException

Loads a BDD from a file.

Compare to bdd_load.

Throws:

IOException

load

public BDD load(BufferedReader ifile)
         throws IOException

Loads a BDD from the given input.

Compare to bdd_load.

Parameters:

ifile - reader

Returns:

BDD

Throws:

IOException

load

public BDD load(BufferedReader ifile,
                int[] translate)
         throws IOException

Loads a BDD from the given input, translating BDD variables according to the given map.

Compare to bdd_load.

Parameters:

ifile - reader

translate - variable translation map

Returns:

BDD

Throws:

IOException

readNext

protected String readNext(BufferedReader ifile)
                   throws IOException

Read the next token from the file.

Parameters:

ifile - reader

Returns:

next string token

Throws:

IOException

loadhash_get

protected BDD loadhash_get(BDDFactory.LoadHash[] lh_table,
                           int lh_nodenum,
                           int key)

Gets a BDD from the load hash table.

save

public void save(String filename,
                 BDD var)
          throws IOException

Saves a BDD to a file.

Compare to bdd_save.

Throws:

IOException

save

public void save(BufferedWriter out,
                 BDD r)
          throws IOException

Saves a BDD to an output writer.

Compare to bdd_save.

Throws:

IOException

save_rec_original

protected int save_rec_original(BufferedWriter out,
                                Map visited,
                                BDD root)
                         throws IOException

Helper function for save().

Throws:

IOException

save_rec

protected int save_rec(BufferedWriter out,
                       BitSet visited,
                       BDD root)
                throws IOException

Helper function for save().

Throws:

IOException

level2Var

public abstract int level2Var(int level)

Convert from a BDD level to a BDD variable.

Compare to bdd_level2var.

var2Level

public abstract int var2Level(int var)

Convert from a BDD variable to a BDD level.

Compare to bdd_var2level.

reorder

public abstract void reorder(BDDFactory.ReorderMethod m)

Reorder the BDD with the given method.

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.

Returns:

ReorderMethod

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.

Parameters:

v - the new verbose level

Returns:

the old verbose level

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

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.

Parameters:

neworder - new variable order

getVarOrder

public int[] getVarOrder()

Gets the current variable order.

Returns:

variable order

makePair

public abstract BDDPairing makePair()

Make a new BDDPairing object.

Compare to bdd_newpair.

makePair

public BDDPairing makePair(int oldvar,
                           int newvar)

Make a new pairing that maps from one variable to another.

Parameters:

oldvar - old variable

newvar - new variable

Returns:

BDD pairing

makePair

public BDDPairing makePair(int oldvar,
                           BDD newvar)

Make a new pairing that maps from one variable to another BDD.

Parameters:

oldvar - old variable

newvar - new BDD

Returns:

BDD pairing

makePair

public BDDPairing makePair(BDDDomain oldvar,
                           BDDDomain newvar)

Make a new pairing that maps from one BDD domain to another.

Parameters:

oldvar - old BDD domain

newvar - new BDD domain

Returns:

BDD pairing

swapVar

public abstract void swapVar(int v1,
                             int v2)

Swap two variables.

Compare to bdd_swapvar.

addVarBlock

public void addVarBlock(BDDVarSet 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.

getVersion

public abstract String getVersion()

Get the BDD library version.

Returns:

version string

nodeCount

public abstract int nodeCount(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.

getNodeTableSize

public abstract int getNodeTableSize()

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.

getCacheSize

public abstract int getCacheSize()

Get the current size of the cache, in entries.

Returns:

size of cache

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.

getGCStats

public BDDFactory.GCStats getGCStats()

Return the current GC statistics for this BDD factory.

Returns:

GC statistics

getReorderStats

public BDDFactory.ReorderStats getReorderStats()

Return the current reordering statistics for this BDD factory.

Returns:

reorder statistics

getCacheStats

public BDDFactory.CacheStats getCacheStats()

Return the current cache statistics for this BDD factory.

Returns:

cache statistics

createDomain

protected BDDDomain createDomain(int a,
                                 BigInteger b)

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

extDomain

public BDDDomain extDomain(long domainSize)

Creates a new finite domain block of the given size. Allocates log 2 (|domainSize|) BDD variables for the domain.

extDomain

public BDDDomain extDomain(BigInteger domainSize)

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[] dom)

extDomain

public BDDDomain[] extDomain(BigInteger[] domainSizes)

overlapDomain

public BDDDomain overlapDomain(BDDDomain d1,
                               BDDDomain d2)

This function takes two finite domain 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 BDDVarSet 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,
                             String ordering)

Creates a variable ordering from a string. The resulting order can be passed into setVarOrder(). Example: in the order "A_BxC_DxExF", the bits for A are first, followed by the bits for B and C interleaved, followed by the bits for D, E, and F interleaved.

Obviously, domain names cannot contain the 'x' or '_' characters.

Parameters:

reverseLocal - whether to reverse the bits of each domain

ordering - string representation of ordering

Returns:

int[] of ordering

See Also:

setVarOrder(int[])

createBitVector

protected BDDBitVector createBitVector(int a)

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

buildVector

public BDDBitVector buildVector(int bitnum,
                                boolean b)

Build a bit vector that is constant true or constant false.

Compare to bvec_true, bvec_false.

constantVector

public BDDBitVector constantVector(int bitnum,
                                   long val)

Build a bit vector that corresponds to a constant value.

Compare to bvec_con.

constantVector

public BDDBitVector constantVector(int bitnum,
                                   BigInteger val)

buildVector

public BDDBitVector buildVector(int bitnum,
                                int offset,
                                int step)

Build a bit vector using variables offset, offset+step, offset+2*step, ... , offset+(bitnum-1)*step.

Compare to bvec_var.

buildVector

public BDDBitVector buildVector(BDDDomain d)

Build a bit vector using variables from the given BDD domain.

Compare to bvec_varfdd.

buildVector

public BDDBitVector buildVector(int[] var)

Build a bit vector using the given variables.

compare to bvec_varvec.

registerGCCallback

public void registerGCCallback(Object o,
                               Method m)

Register a callback that is called when garbage collection is about to occur.

Parameters:

o - base object

m - method

unregisterGCCallback

public void unregisterGCCallback(Object o,
                                 Method m)

Unregister a garbage collection callback that was previously registered.

Parameters:

o - base object

m - method

registerReorderCallback

public void registerReorderCallback(Object o,
                                    Method m)

Register a callback that is called when reordering is about to occur.

Parameters:

o - base object

m - method

unregisterReorderCallback

public void unregisterReorderCallback(Object o,
                                      Method m)

Unregister a reorder callback that was previously registered.

Parameters:

o - base object

m - method

registerResizeCallback

public void registerResizeCallback(Object o,
                                   Method m)

Register a callback that is called when node table resizing is about to occur.

Parameters:

o - base object

m - method

unregisterResizeCallback

public void unregisterResizeCallback(Object o,
                                     Method m)

Unregister a reorder callback that was previously registered.

Parameters:

o - base object

m - method

gbc_handler

protected void gbc_handler(boolean pre,
                           BDDFactory.GCStats s)

bdd_default_gbchandler

protected static void bdd_default_gbchandler(boolean pre,
                                             BDDFactory.GCStats s)

bdd_default_reohandler

protected void bdd_default_reohandler(boolean prestate,
                                      BDDFactory.ReorderStats s)

resize_handler

protected void resize_handler(int oldsize,
                              int newsize)

bdd_default_reshandler

protected static void bdd_default_reshandler(int oldsize,
                                             int newsize)

registerCallback

protected void registerCallback(List callbacks,
                                Object o,
                                Method m)

unregisterCallback

protected boolean unregisterCallback(List callbacks,
                                     Object o,
                                     Method m)

doCallbacks

protected void doCallbacks(List callbacks,
                           Object arg1,
                           Object arg2)