net.sf.javabdd
Class BDDFactoryIntImpl

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

Direct Known Subclasses:

BuDDyFactory, JDDFactory, JFactory, MicroFactory, UberMicroFactory

public abstract class BDDFactoryIntImpl
extends BDDFactory

A shared superclass for BDD factories that refer to BDDs as ints.

Version:

$Id$

Author:

jwhaley

Nested Class Summary

class	BDDFactoryIntImpl.IntBDD
class	BDDFactoryIntImpl.IntBDDBitVector
class	BDDFactoryIntImpl.IntBDDVarSet
class	BDDFactoryIntImpl.IntBDDVarSetWithFinalizer
class	BDDFactoryIntImpl.IntBDDWithFinalizer
class	BDDFactoryIntImpl.IntZDDVarSet
class	BDDFactoryIntImpl.IntZDDVarSetWithFinalizer

Nested classes/interfaces inherited from class net.sf.javabdd.BDDFactory

BDDFactory.BDDOp, BDDFactory.CacheStats, BDDFactory.GCStats, BDDFactory.LoadHash, BDDFactory.ReorderMethod, BDDFactory.ReorderStats

Field Summary

protected int[]	to_free
protected int	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

Constructor Summary

BDDFactoryIntImpl()

Method Summary

protected abstract void	addref_impl(int v)
protected abstract int	apply_impl(int v1, int v2, BDDFactory.BDDOp opr)
protected abstract int	applyAll_impl(int v1, int v2, BDDFactory.BDDOp opr, int v3)
protected abstract int	applyEx_impl(int v1, int v2, BDDFactory.BDDOp opr, int v3)
protected abstract int	applyUni_impl(int v1, int v2, BDDFactory.BDDOp opr, int v3)
protected abstract int	compose_impl(int v1, int v2, int var)
protected abstract int	constrain_impl(int v1, int v2)
void	deferredFree(int v)
protected abstract void	delref_impl(int v)
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.
protected abstract int	exist_impl(int v1, int v2)
protected void	finalize()
protected abstract int	forAll_impl(int v1, int v2)
protected abstract int	fullSatOne_impl(int v)
void	handleDeferredFree()
protected abstract int	high_impl(int v)
protected abstract int	invalid_bdd_impl()
protected abstract int	ite_impl(int v1, int v2, int v3)
protected abstract int	ithVar_impl(int var)
BDD	ithVar(int var) Returns a BDD representing the I'th variable.
protected abstract int	level_impl(int v)
protected abstract int	low_impl(int v)
protected BDDFactoryIntImpl.IntBDD	makeBDD(int v)
protected BDDFactoryIntImpl.IntBDDVarSet	makeBDDVarSet(int v)
protected abstract int	makenode_impl(int lev, int lo, int hi)
protected abstract int	nithVar_impl(int var)
BDD	nithVar(int var) Returns a BDD representing the negation of the I'th variable.
protected abstract int	nodeCount_impl(int v)
protected abstract int	nodeCount_impl2(int[] v)
int	nodeCount(Collection r) Counts the number of shared nodes in a collection of BDDs.
protected abstract int	not_impl(int v1)
protected abstract int	one_impl()
BDD	one() Get the constant true BDD.
protected abstract double	pathCount_impl(int v)
protected abstract void	printTable_impl(int v)
void	printTable(BDD b) Prints the node table entries used by a BDD.
protected abstract int	replace_impl(int v, BDDPairing p)
protected abstract int	restrict_impl(int v1, int v2)
protected abstract double	satCount_impl(int v)
protected abstract int	satOne_impl(int v)
protected abstract int	satOne_impl2(int v1, int v2, boolean pol)
protected abstract int	simplify_impl(int v1, int v2)
protected abstract int	support_impl(int v)
protected abstract int	unique_impl(int v1, int v2)
protected int	universe_impl()
BDD	universe() Get the constant universe BDD.
protected static int	unwrap(BDD b)
protected static int	unwrap(BDDVarSet b)
protected static int[]	unwrap(Collection c)
protected abstract int	var_impl(int v)
protected abstract int[]	varProfile_impl(int v)
protected abstract int	veccompose_impl(int v, BDDPairing p)
protected abstract int	zero_impl()
BDD	zero() Get the constant false BDD.

Methods inherited from class net.sf.javabdd.BDDFactory

addVarBlock, addVarBlock, autoReorder, autoReorder, bdd_default_gbchandler, bdd_default_reohandler, bdd_default_reshandler, buildCube, buildCube, buildVector, buildVector, buildVector, buildVector, clearAllDomains, clearError, clearVarBlocks, constantVector, constantVector, createBitVector, createDomain, disableReorder, doCallbacks, enableReorder, extDomain, extDomain, extDomain, extDomain, extDomain, extVarNum, gbc_handler, getCacheSize, getCacheStats, getDomain, getGCStats, getNodeNum, getNodeTableSize, getProperty, getReorderMethod, getReorderStats, getReorderTimes, getVarOrder, getVersion, init, init, initialize, isInitialized, isZDD, level2Var, load, load, load, loadhash_get, makePair, makePair, makePair, makePair, makeSet, makeSet, makeVarOrdering, numberOfDomains, overlapDomain, printAll, printOrder, printStat, readNext, registerCallback, registerGCCallback, registerReorderCallback, registerResizeCallback, reorder, reorderGain, reorderVerbose, reset, resize_handler, save_rec_original, save_rec, save, save, setCacheRatio, setCacheSize, setError, setIncreaseFactor, setMaxIncrease, setMaxNodeNum, setMinFreeNodes, setNodeTableSize, setVarNum, setVarOrder, swapVar, unregisterCallback, unregisterGCCallback, unregisterReorderCallback, unregisterResizeCallback, var2Level, varBlockAll, varNum

Methods inherited from class java.lang.Object

clone, equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

to_free

protected int[] to_free

to_free_length

protected int to_free_length

Constructor Detail

BDDFactoryIntImpl

public BDDFactoryIntImpl()

Method Detail

addref_impl

protected abstract void addref_impl(int v)

delref_impl

protected abstract void delref_impl(int v)

zero_impl

protected abstract int zero_impl()

one_impl

protected abstract int one_impl()

universe_impl

protected int universe_impl()

invalid_bdd_impl

protected abstract int invalid_bdd_impl()

var_impl

protected abstract int var_impl(int v)

level_impl

protected abstract int level_impl(int v)

low_impl

protected abstract int low_impl(int v)

high_impl

protected abstract int high_impl(int v)

ithVar_impl

protected abstract int ithVar_impl(int var)

nithVar_impl

protected abstract int nithVar_impl(int var)

makenode_impl

protected abstract int makenode_impl(int lev,
                                     int lo,
                                     int hi)

ite_impl

protected abstract int ite_impl(int v1,
                                int v2,
                                int v3)

apply_impl

protected abstract int apply_impl(int v1,
                                  int v2,
                                  BDDFactory.BDDOp opr)

not_impl

protected abstract int not_impl(int v1)

applyAll_impl

protected abstract int applyAll_impl(int v1,
                                     int v2,
                                     BDDFactory.BDDOp opr,
                                     int v3)

applyEx_impl

protected abstract int applyEx_impl(int v1,
                                    int v2,
                                    BDDFactory.BDDOp opr,
                                    int v3)

applyUni_impl

protected abstract int applyUni_impl(int v1,
                                     int v2,
                                     BDDFactory.BDDOp opr,
                                     int v3)

compose_impl

protected abstract int compose_impl(int v1,
                                    int v2,
                                    int var)

constrain_impl

protected abstract int constrain_impl(int v1,
                                      int v2)

restrict_impl

protected abstract int restrict_impl(int v1,
                                     int v2)

simplify_impl

protected abstract int simplify_impl(int v1,
                                     int v2)

support_impl

protected abstract int support_impl(int v)

exist_impl

protected abstract int exist_impl(int v1,
                                  int v2)

forAll_impl

protected abstract int forAll_impl(int v1,
                                   int v2)

unique_impl

protected abstract int unique_impl(int v1,
                                   int v2)

fullSatOne_impl

protected abstract int fullSatOne_impl(int v)

replace_impl

protected abstract int replace_impl(int v,
                                    BDDPairing p)

veccompose_impl

protected abstract int veccompose_impl(int v,
                                       BDDPairing p)

nodeCount_impl

protected abstract int nodeCount_impl(int v)

pathCount_impl

protected abstract double pathCount_impl(int v)

satCount_impl

protected abstract double satCount_impl(int v)

satOne_impl

protected abstract int satOne_impl(int v)

satOne_impl2

protected abstract int satOne_impl2(int v1,
                                    int v2,
                                    boolean pol)

nodeCount_impl2

protected abstract int nodeCount_impl2(int[] v)

varProfile_impl

protected abstract int[] varProfile_impl(int v)

printTable_impl

protected abstract void printTable_impl(int v)

makeBDD

protected BDDFactoryIntImpl.IntBDD makeBDD(int v)

unwrap

protected static final int unwrap(BDD b)

unwrap

protected static final int[] unwrap(Collection c)

makeBDDVarSet

protected BDDFactoryIntImpl.IntBDDVarSet makeBDDVarSet(int v)

unwrap

protected static final int unwrap(BDDVarSet b)

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

Parameters:

var - the variable number

Returns:

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

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

Parameters:

var - the variable number

Returns:

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

nodeCount

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

one

public BDD one()

Description copied from class: BDDFactory

Get the constant true BDD.

Compare to bdd_true.

Specified by:

one in class BDDFactory

universe

public BDD universe()

Description copied from class: BDDFactory

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

Compare to bdd_true.

Overrides:

universe in class BDDFactory

emptySet

public BDDVarSet emptySet()

Description copied from class: BDDFactory

Get an empty BDDVarSet.

Compare to bdd_true.

Overrides:

emptySet 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

zero

public BDD zero()

Description copied from class: BDDFactory

Get the constant false BDD.

Compare to bdd_false.

Specified by:

zero in class BDDFactory

done

public void done()

Description copied from class: 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.

Specified by:

done in class BDDFactory

finalize

protected void finalize()
                 throws Throwable

Overrides:

finalize in class Object

Throws:

Throwable

deferredFree

public void deferredFree(int v)

handleDeferredFree

public void handleDeferredFree()