net.sf.javabdd
Class BDDDomain

java.lang.Object
  net.sf.javabdd.BDDDomain

public abstract class BDDDomain
extends Object

Represents a domain of BDD variables. This is useful for finite state machines, among other things.

BDDDomains are called "finite domain blocks" in Section 2.9 of the buddy documentation. A BDDDomain is a block of BDD variables that can represent integer values as opposed to only true and false.

Use BDDFactory.extDomain() to create one or more domains with a specified list of sizes.

Version:

$Id: BDDDomain.java 468 2006-11-29 08:07:13Z joewhaley $

Author:

John Whaley

See Also:

BDDFactory.extDomain(int[])

Field Summary

protected int	index
protected int[]	ivar
protected String	name
protected BigInteger	realsize
protected BDDVarSet	var

Constructor Summary

protected

BDDDomain(int index, BigInteger range) Default constructor.

Method Summary

BDD	buildAdd(BDDDomain that, int bits, long value)
BDD	buildAdd(BDDDomain that, long value)
BDD	buildEquals(BDDDomain that) Builds a BDD which is true for all the possible assignments to the variable blocks that makes the blocks equal.
BDD	domain() Returns what corresponds to a disjunction of all possible values of this domain.
int	ensureCapacity(BigInteger range)
int	ensureCapacity(long range)
abstract BDDFactory	getFactory() Returns the factory that created this domain.
int	getIndex() Returns the index of this domain.
String	getName() Gets the name of this domain.
BigInteger[]	getVarIndices(BDD bdd) Convert a BDD that to a list of indices of this domain.
BigInteger[]	getVarIndices(BDD bdd, int max) Convert a BDD that to a list of indices of this domain.
BDD	ithVar(BigInteger val)
BDD	ithVar(long val) Returns the BDD that defines the given value for this finite domain block.
BDDVarSet	set() Returns the variable set that contains the variables used to define this finite domain block.
void	setName(String name) Sets the name of this domain.
BigInteger	size() Returns the size of the domain for this finite domain block.
String	toString()
int	varNum() Returns the number of BDD variables used for this finite domain block.
BDD	varRange(BigInteger lo, BigInteger hi)
BDD	varRange(long lo, long hi) Returns the BDD that defines the given range of values, inclusive, for this finite domain block.
int[]	vars() Returns an integer array containing the indices of the BDD variables used to define this finite domain.

Methods inherited from class java.lang.Object

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

Field Detail

name

protected String name

index

protected int index

realsize

protected BigInteger realsize

ivar

protected int[] ivar

var

protected BDDVarSet var

Constructor Detail

BDDDomain

protected BDDDomain(int index,
                    BigInteger range)

Default constructor.

Parameters:

index - index of this domain

range - size of this domain

Method Detail

getFactory

public abstract BDDFactory getFactory()

Returns the factory that created this domain.

setName

public void setName(String name)

Sets the name of this domain.

getName

public String getName()

Gets the name of this domain.

getIndex

public int getIndex()

Returns the index of this domain.

domain

public BDD domain()

Returns what corresponds to a disjunction of all possible values of this domain. This is more efficient than doing ithVar(0) OR ithVar(1) ... explicitly for all values in the domain.

Compare to fdd_domain.

size

public BigInteger size()

Returns the size of the domain for this finite domain block. Compare to fdd_domainsize.

buildAdd

public BDD buildAdd(BDDDomain that,
                    long value)

buildAdd

public BDD buildAdd(BDDDomain that,
                    int bits,
                    long value)

buildEquals

public BDD buildEquals(BDDDomain that)

Builds a BDD which is true for all the possible assignments to the variable blocks that makes the blocks equal. Compare to fdd_equals/fdd_equ.

Parameters:

that -

Returns:

BDD

set

public BDDVarSet set()

Returns the variable set that contains the variables used to define this finite domain block. Compare to fdd_ithset.

Returns:

BDDVarSet

ithVar

public BDD ithVar(long val)

Returns the BDD that defines the given value for this finite domain block. Compare to fdd_ithvar.

Returns:

BDD

ithVar

public BDD ithVar(BigInteger val)

varRange

public BDD varRange(long lo,
                    long hi)

Returns the BDD that defines the given range of values, inclusive, for this finite domain block.

Returns:

BDD

varRange

public BDD varRange(BigInteger lo,
                    BigInteger hi)

varNum

public int varNum()

Returns the number of BDD variables used for this finite domain block. Compare to fdd_varnum.

Returns:

int

vars

public int[] vars()

Returns an integer array containing the indices of the BDD variables used to define this finite domain. Compare to fdd_vars.

Returns:

int[]

ensureCapacity

public int ensureCapacity(long range)

ensureCapacity

public int ensureCapacity(BigInteger range)

toString

public String toString()

Overrides:

toString in class Object

getVarIndices

public BigInteger[] getVarIndices(BDD bdd)

Convert a BDD that to a list of indices of this domain. This method assumes that the BDD passed is a disjunction of ithVar(i_1) to ithVar(i_k). It returns an array of length 'k' with elements [i_1,...,i_k].

Be careful when using this method for BDDs with a large number of entries, as it allocates a BigInteger[] array of dimension k.

Parameters:

bdd - bdd that is the disjunction of domain indices

See Also:

getVarIndices(BDD,int), ithVar(BigInteger)

getVarIndices

public BigInteger[] getVarIndices(BDD bdd,
                                  int max)

Convert a BDD that to a list of indices of this domain. Same as getVarIndices(BDD), except only 'max' indices are extracted.

Parameters:

bdd - bdd that is the disjunction of domain indices

max - maximum number of entries to be returned

See Also:

ithVar(long)