

PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 
java.lang.Object net.sf.javabdd.BDD
public abstract class BDD
Binary Decision Diagrams (BDDs) are used for efficient computation of many common problems. This is done by giving a compact representation and a set of efficient operations on boolean functions f: {0,1}^n > {0,1}.
Use an implementation of BDDFactory to create BDD objects.
BDDFactory
,
BDDDomain.set()
Nested Class Summary  

static class 
BDD.AllSatIterator
Iterator that returns all satisfying assignments as byte arrays. 
static class 
BDD.BDDIterator
BDDIterator is used to iterate through the satisfying assignments of a BDD. 
static class 
BDD.BDDToString
BDDToString is used to specify the printing behavior of BDDs with domains. 
Constructor Summary  

protected 
BDD()
Protected constructor. 
Method Summary  

BDD.AllSatIterator 
allsat()
Finds all satisfying variable assignments. 
BDD 
and(BDD that)
Returns the logical 'and' of two BDDs. 
BDD 
andWith(BDD that)
Makes this BDD be the logical 'and' of two BDDs. 
abstract BDD 
apply(BDD that,
BDDFactory.BDDOp opr)
Returns the result of applying the binary operator opr to the two BDDs. 
abstract BDD 
applyAll(BDD that,
BDDFactory.BDDOp opr,
BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs a universal quantification of the variables from the variable set var. 
abstract BDD 
applyEx(BDD that,
BDDFactory.BDDOp opr,
BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs an existential quantification of the variables from the variable set var. 
abstract BDD 
applyUni(BDD that,
BDDFactory.BDDOp opr,
BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs a unique quantification of the variables from the variable set var. 
abstract BDD 
applyWith(BDD that,
BDDFactory.BDDOp opr)
Makes this BDD be the result of the binary operator opr of two BDDs. 
BDD 
biimp(BDD that)
Returns the logical 'biimplication' of two BDDs. 
BDD 
biimpWith(BDD that)
Makes this BDD be the logical 'biimplication' of two BDDs. 
abstract BDD 
compose(BDD g,
int var)
Functional composition. 
abstract BDD 
constrain(BDD that)
Generalized cofactor. 
abstract boolean 
equals(BDD that)
Returns true if this BDD equals that BDD, false otherwise. 
boolean 
equals(Object o)

abstract BDD 
exist(BDDVarSet var)
Existential quantification of variables. 
abstract BDD 
forAll(BDDVarSet var)
Universal quantification of variables. 
abstract void 
free()
Frees this BDD. 
abstract BDD 
fullSatOne()
Finds one satisfying variable assignment. 
abstract BDDFactory 
getFactory()
Returns the factory that created this BDD. 
abstract int 
hashCode()

abstract BDD 
high()
Gets the true branch of this BDD. 
abstract BDD 
id()
Identity function. 
BDD 
imp(BDD that)
Returns the logical 'implication' of two BDDs. 
BDD 
impWith(BDD that)
Makes this BDD be the logical 'implication' of two BDDs. 
abstract boolean 
isOne()
Returns true if this BDD is the one (true) BDD. 
boolean 
isUniverse()
Returns true if this BDD is the universe BDD. 
abstract boolean 
isZero()
Returns true if this BDD is the zero (false) BDD. 
abstract BDD 
ite(BDD thenBDD,
BDD elseBDD)
ifthenelse operator. 
BDD.BDDIterator 
iterator(BDDVarSet var)
Returns an iteration of the satisfying assignments of this BDD. 
int 
level()
Gets the level of this BDD. 
double 
logSatCount()
Calculates the logarithm of the number of satisfying variable assignments. 
double 
logSatCount(BDDVarSet varset)
Calculates the logarithm of the number of satisfying variable assignments to the variables in the given varset. 
abstract BDD 
low()
Gets the false branch of this BDD. 
abstract int 
nodeCount()
Counts the number of distinct nodes used for this BDD. 
abstract BDD 
not()
Negates this BDD by exchanging all references to the zeroterminal with references to the oneterminal and viceversa. 
BDD 
or(BDD that)
Returns the logical 'or' of two BDDs. 
BDD 
orWith(BDD that)
Makes this BDD be the logical 'or' of two BDDs. 
abstract double 
pathCount()
Counts the number of paths leading to the true terminal. 
protected int 
printdot_rec(PrintStream out,
int current,
boolean[] visited,
HashMap map)

void 
printDot()
Prints this BDD in dot graph notation. 
void 
printSet()
Prints the set of truth assignments specified by this BDD. 
void 
printSetWithDomains()
Prints this BDD using a set notation as in printSet() but with the index of the finite domain blocks included instead of the BDD variables. 
BDD 
relprod(BDD that,
BDDVarSet var)
Relational product. 
abstract BDD 
replace(BDDPairing pair)
Returns a BDD where all variables are replaced with the variables defined by pair. 
abstract BDD 
replaceWith(BDDPairing pair)
Replaces all variables in this BDD with the variables defined by pair. 
abstract BDD 
restrict(BDD var)
Restrict a set of variables to constant values. 
abstract BDD 
restrictWith(BDD var)
Mutates this BDD to restrict a set of variables to constant values. 
abstract double 
satCount()
Calculates the number of satisfying variable assignments. 
double 
satCount(BDDVarSet varset)
Calculates the number of satisfying variable assignments to the variables in the given varset. 
abstract BDD 
satOne()
Finds one satisfying variable assignment. 
abstract BDD 
satOne(BDDVarSet var,
boolean pol)
Finds one satisfying variable assignment. 
BigInteger[] 
scanAllVar()
Finds one satisfying assignment in this BDD of all the defined BDDDomain's. 
BigInteger 
scanVar(BDDDomain d)
Finds one satisfying assignment of the domain d in this BDD and returns that value. 
abstract BDD 
simplify(BDDVarSet d)
Coudert and Madre's restrict function. 
abstract BDDVarSet 
support()
Returns the variable support of this BDD. 
String 
toString()

String 
toStringWithDomains()
Returns a string representation of this BDD using the defined domains. 
String 
toStringWithDomains(BDD.BDDToString ts)
Returns a string representation of this BDD on the defined domains, using the given BDDToString converter. 
BDDVarSet 
toVarSet()
Converts this BDD to a new BDDVarSet. 
abstract BDD 
unique(BDDVarSet var)
Unique quantification of variables. 
abstract int 
var()
Gets the variable labeling the BDD. 
abstract int[] 
varProfile()
Counts the number of times each variable occurs in this BDD. 
abstract BDD 
veccompose(BDDPairing pair)
Simultaneous functional composition. 
BDD 
xor(BDD that)
Returns the logical 'xor' of two BDDs. 
BDD 
xorWith(BDD that)
Makes this BDD be the logical 'xor' of two BDDs. 
Methods inherited from class java.lang.Object 

clone, finalize, getClass, notify, notifyAll, wait, wait, wait 
Constructor Detail 

protected BDD()
Protected constructor.
Method Detail 

public abstract BDDFactory getFactory()
Returns the factory that created this BDD.
public abstract boolean isZero()
Returns true if this BDD is the zero (false) BDD.
public abstract boolean isOne()
Returns true if this BDD is the one (true) BDD.
public boolean isUniverse()
Returns true if this BDD is the universe BDD. The universal BDD differs from the one BDD in ZDD mode.
public BDDVarSet toVarSet()
Converts this BDD to a new BDDVarSet.
This BDD must be a boolean function that represents the alltrue minterm of the BDD variables of interest.
public abstract int var()
Gets the variable labeling the BDD.
Compare to bdd_var.
public int level()
Gets the level of this BDD.
Compare to LEVEL() macro.
public abstract BDD high()
Gets the true branch of this BDD.
Compare to bdd_high.
public abstract BDD low()
Gets the false branch of this BDD.
Compare to bdd_low.
public abstract BDD id()
Identity function. Returns a copy of this BDD. Use as the argument to the "xxxWith" style operators when you do not want to have the argument consumed.
Compare to bdd_addref.
public abstract BDD not()
Negates this BDD by exchanging all references to the zeroterminal with references to the oneterminal and viceversa.
Compare to bdd_not.
public BDD and(BDD that)
Returns the logical 'and' of two BDDs. This is a shortcut for calling "apply" with the "and" operator.
Compare to bdd_and.
that
 BDD to 'and' with
public BDD andWith(BDD that)
Makes this BDD be the logical 'and' of two BDDs. The "that" BDD is consumed, and can no longer be used. This is a shortcut for calling "applyWith" with the "and" operator.
Compare to bdd_and and bdd_delref.
that
 the BDD to 'and' withpublic BDD or(BDD that)
Returns the logical 'or' of two BDDs. This is a shortcut for calling "apply" with the "or" operator.
Compare to bdd_or.
that
 the BDD to 'or' with
public BDD orWith(BDD that)
Makes this BDD be the logical 'or' of two BDDs. The "that" BDD is consumed, and can no longer be used. This is a shortcut for calling "applyWith" with the "or" operator.
Compare to bdd_or and bdd_delref.
that
 the BDD to 'or' withpublic BDD xor(BDD that)
Returns the logical 'xor' of two BDDs. This is a shortcut for calling "apply" with the "xor" operator.
Compare to bdd_xor.
that
 the BDD to 'xor' with
public BDD xorWith(BDD that)
Makes this BDD be the logical 'xor' of two BDDs. The "that" BDD is consumed, and can no longer be used. This is a shortcut for calling "applyWith" with the "xor" operator.
Compare to bdd_xor and bdd_delref.
that
 the BDD to 'xor' withpublic BDD imp(BDD that)
Returns the logical 'implication' of two BDDs. This is a shortcut for calling "apply" with the "imp" operator.
Compare to bdd_imp.
that
 the BDD to 'implication' with
public BDD impWith(BDD that)
Makes this BDD be the logical 'implication' of two BDDs. The "that" BDD is consumed, and can no longer be used. This is a shortcut for calling "applyWith" with the "imp" operator.
Compare to bdd_imp and bdd_delref.
that
 the BDD to 'implication' withpublic BDD biimp(BDD that)
Returns the logical 'biimplication' of two BDDs. This is a shortcut for calling "apply" with the "biimp" operator.
Compare to bdd_biimp.
that
 the BDD to 'biimplication' with
public BDD biimpWith(BDD that)
Makes this BDD be the logical 'biimplication' of two BDDs. The "that" BDD is consumed, and can no longer be used. This is a shortcut for calling "applyWith" with the "biimp" operator.
Compare to bdd_biimp and bdd_delref.
that
 the BDD to 'biimplication' withpublic abstract BDD ite(BDD thenBDD, BDD elseBDD)
ifthenelse operator.
Compare to bdd_ite.
thenBDD
 the 'then' BDDelseBDD
 the 'else' BDD
public BDD relprod(BDD that, BDDVarSet var)
Relational product. Calculates the relational product of the two BDDs as this AND that with the variables in var quantified out afterwards. Identical to applyEx(that, and, var).
Compare to bdd_relprod.
that
 the BDD to 'and' withvar
 the BDDVarSet to existentially quantify with
BDDDomain.set()
public abstract BDD compose(BDD g, int var)
Functional composition. Substitutes the variable var with the BDD that in this BDD: result = f[g/var].
Compare to bdd_compose.
g
 the function to use to replacevar
 the variable number to replace
public abstract BDD veccompose(BDDPairing pair)
Simultaneous functional composition. Uses the pairs of variables and BDDs in pair to make the simultaneous substitution: f [g1/V1, ... gn/Vn]. In this way one or more BDDs may be substituted in one step. The BDDs in pair may depend on the variables they are substituting. BDD.compose() may be used instead of BDD.replace() but is not as efficient when gi is a single variable, the same applies to BDD.restrict(). Note that simultaneous substitution is not necessarily the same as repeated substitution.
Compare to bdd_veccompose.
pair
 the pairing of variables to functions
public abstract BDD constrain(BDD that)
Generalized cofactor. Computes the generalized cofactor of this BDD with respect to the given BDD.
Compare to bdd_constrain.
that
 the BDD with which to compute the generalized cofactor
public abstract BDD exist(BDDVarSet var)
Existential quantification of variables. Removes all occurrences of this BDD in variables in the set var by existential quantification.
Compare to bdd_exist.
var
 BDDVarSet containing the variables to be existentially quantified
BDDDomain.set()
public abstract BDD forAll(BDDVarSet var)
Universal quantification of variables. Removes all occurrences of this BDD in variables in the set var by universal quantification.
Compare to bdd_forall.
var
 BDDVarSet containing the variables to be universally quantified
BDDDomain.set()
public abstract BDD unique(BDDVarSet var)
Unique quantification of variables. This type of quantification uses a XOR operator instead of an OR operator as in the existential quantification.
Compare to bdd_unique.
var
 BDDVarSet containing the variables to be uniquely quantified
BDDDomain.set()
public abstract BDD restrict(BDD var)
Restrict a set of variables to constant values. Restricts the variables in this BDD to constant true if they are included in their positive form in var, and constant false if they are included in their negative form.
Note that this is quite different than Coudert and Madre's restrict function.
Compare to bdd_restrict.
var
 BDD containing the variables to be restricted
net.sf.javabdd.BDD#simplify(BDD)
public abstract BDD restrictWith(BDD var)
Mutates this BDD to restrict a set of variables to constant values. Restricts the variables in this BDD to constant true if they are included in their positive form in var, and constant false if they are included in their negative form. The "that" BDD is consumed, and can no longer be used.
Note that this is quite different than Coudert and Madre's restrict function.
Compare to bdd_restrict and bdd_delref.
var
 BDD containing the variables to be restrictedBDDDomain.set()
public abstract BDD simplify(BDDVarSet d)
Coudert and Madre's restrict function. Tries to simplify the BDD f by restricting it to the domain covered by d. No checks are done to see if the result is actually smaller than the input. This can be done by the user with a call to nodeCount().
Compare to bdd_simplify.
d
 BDDVarSet containing the variables in the domain
public abstract BDDVarSet support()
Returns the variable support of this BDD. The support is all the variables that this BDD depends on.
Compare to bdd_support.
public abstract BDD apply(BDD that, BDDFactory.BDDOp opr)
Returns the result of applying the binary operator opr to the two BDDs.
Compare to bdd_apply.
that
 the BDD to apply the operator onopr
 the operator to apply
public abstract BDD applyWith(BDD that, BDDFactory.BDDOp opr)
Makes this BDD be the result of the binary operator opr of two BDDs. The "that" BDD is consumed, and can no longer be used. Attempting to use the passed in BDD again will result in an exception being thrown.
Compare to bdd_apply and bdd_delref.
that
 the BDD to apply the operator onopr
 the operator to applypublic abstract BDD applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs a universal quantification of the variables from the variable set var.
Compare to bdd_appall.
that
 the BDD to apply the operator onopr
 the operator to applyvar
 BDDVarSet containing the variables to quantify
BDDDomain.set()
public abstract BDD applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs an existential quantification of the variables from the variable set var.
Compare to bdd_appex.
that
 the BDD to apply the operator onopr
 the operator to applyvar
 BDDVarSet containing the variables to quantify
BDDDomain.set()
public abstract BDD applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
Applies the binary operator opr to two BDDs and then performs a unique quantification of the variables from the variable set var.
Compare to bdd_appuni.
that
 the BDD to apply the operator onopr
 the operator to applyvar
 BDDVarSet containing the variables to quantify
BDDDomain.set()
public abstract BDD satOne()
Finds one satisfying variable assignment. Finds a BDD with at most one variable at each level. The new BDD implies this BDD and is not false unless this BDD is false.
Compare to bdd_satone.
public abstract BDD fullSatOne()
Finds one satisfying variable assignment. Finds a BDD with exactly one variable at all levels. The new BDD implies this BDD and is not false unless this BDD is false.
Compare to bdd_fullsatone.
public abstract BDD satOne(BDDVarSet var, boolean pol)
Finds one satisfying variable assignment. Finds a minterm in this BDD. The var argument is a set of variables that must be mentioned in the result. The polarity of these variables in the result  in case they are undefined in this BDD  are defined by the pol parameter. If pol is false, then all variables will be in negative form. Otherwise they will be in positive form.
Compare to bdd_satoneset.
var
 BDDVarSet containing the set of variables that must be mentioned in the resultpol
 the polarity of the result
BDDDomain.set()
public BDD.AllSatIterator allsat()
Finds all satisfying variable assignments.
Compare to bdd_allsat.
public BigInteger scanVar(BDDDomain d)
Finds one satisfying assignment of the domain d in this BDD and returns that value.
Compare to fdd_scanvar.
d
 domain to scan
public BigInteger[] scanAllVar()
Finds one satisfying assignment in this BDD of all the defined BDDDomain's. Each value is stored in an array which is returned. The size of this array is exactly the number of BDDDomain's defined.
Compare to fdd_scanallvar.
public BDD.BDDIterator iterator(BDDVarSet var)
Returns an iteration of the satisfying assignments of this BDD. Returns an iteration of minterms. The var argument is the set of variables that will be mentioned in the result.
var
 set of variables to mention in result
BDDDomain.set()
public abstract BDD replace(BDDPairing pair)
Returns a BDD where all variables are replaced with the variables defined by pair. Each entry in pair consists of a old and a new variable. Whenever the old variable is found in this BDD then a new node with the new variable is inserted instead.
Compare to bdd_replace.
pair
 pairing of variables to the BDDs that replace those variables
public abstract BDD replaceWith(BDDPairing pair)
Replaces all variables in this BDD with the variables defined by pair. Each entry in pair consists of a old and a new variable. Whenever the old variable is found in this BDD then a new node with the new variable is inserted instead. Mutates the current BDD.
Compare to bdd_replace and bdd_delref.
pair
 pairing of variables to the BDDs that replace those variablespublic void printSet()
Prints the set of truth assignments specified by this BDD.
Compare to bdd_printset.
public void printSetWithDomains()
Prints this BDD using a set notation as in printSet() but with the index of the finite domain blocks included instead of the BDD variables.
Compare to fdd_printset.
public void printDot()
Prints this BDD in dot graph notation.
Compare to bdd_printdot.
protected int printdot_rec(PrintStream out, int current, boolean[] visited, HashMap map)
public abstract int nodeCount()
Counts the number of distinct nodes used for this BDD.
Compare to bdd_nodecount.
public abstract double pathCount()
Counts the number of paths leading to the true terminal.
Compare to bdd_pathcount.
public abstract double satCount()
Calculates the number of satisfying variable assignments.
Compare to bdd_satcount.
public double satCount(BDDVarSet varset)
Calculates the number of satisfying variable assignments to the variables in the given varset. ASSUMES THAT THE BDD DOES NOT HAVE ANY ASSIGNMENTS TO VARIABLES THAT ARE NOT IN VARSET. You will need to quantify out the other variables first.
Compare to bdd_satcountset.
public double logSatCount()
Calculates the logarithm of the number of satisfying variable assignments.
Compare to bdd_satcount.
public double logSatCount(BDDVarSet varset)
Calculates the logarithm of the number of satisfying variable assignments to the variables in the given varset.
Compare to bdd_satcountset.
public abstract int[] varProfile()
Counts the number of times each variable occurs in this BDD. The result is stored and returned in an integer array where the i'th position stores the number of times the i'th printing variable occurred in the BDD.
Compare to bdd_varprofile.
public abstract boolean equals(BDD that)
Returns true if this BDD equals that BDD, false otherwise.
that
 the BDD to compare with
public boolean equals(Object o)
equals
in class Object
public abstract int hashCode()
hashCode
in class Object
public String toString()
toString
in class Object
public String toStringWithDomains()
Returns a string representation of this BDD using the defined domains.
public String toStringWithDomains(BDD.BDDToString ts)
Returns a string representation of this BDD on the defined domains, using the given BDDToString converter.
BDD.BDDToString
public abstract void free()
Frees this BDD. Further use of this BDD will result in an exception being thrown.


PREV CLASS NEXT CLASS  FRAMES NO FRAMES  
SUMMARY: NESTED  FIELD  CONSTR  METHOD  DETAIL: FIELD  CONSTR  METHOD 