BDD

Overview

Package

Class

Use

Deprecated

Index

Home >> All >> org >> sf >> [ javabdd overview ]

PREV CLASS NEXT CLASS

SUMMARY:

JAVADOC |

SOURCE |

DOWNLOAD | NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

org.sf.javabdd
Class BDD

java.lang.Object
  org.sf.javabdd.BDD

Direct Known Subclasses:: BuDDyFactory.BuDDyBDD, CUDDFactory.CUDDBDD, JavaFactory.bdd, TestBDDFactory.TestBDD, TypedBDDFactory.TypedBDD

public abstract class BDD
extends java.lang.Object

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.

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

Nested Class Summary

static class BDD.BDDToString
          BDDToString is used to specify the printing behavior of BDDs with domains.

(package private) static class BDD.OutputBuffer


Constructor Summary

protected BDD()
          Protected constructor.

Method Summary

abstract java.util.List 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, BDD 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, BDD 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, BDD 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.

private static void bdd_printset_rec(BDDFactory f, java.lang.StringBuffer sb, BDD r, int[] set)


BDD biimp(BDD that)
          Returns the logical 'bi-implication' of two BDDs.

BDD biimpWith(BDD that)
          Makes this BDD be the logical 'bi-implication' 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(java.lang.Object o)
          Determine whether this Object is semantically equal to another Object.

abstract BDD exist(BDD var)
          Existential quantification of variables.

(package private) static void fdd_printset_helper(BDD.OutputBuffer sb, long value, int i, int[] set, int[] var, int maxSkip)


(package private) static void fdd_printset_rec(BDDFactory bdd, java.lang.StringBuffer sb, BDD.BDDToString ts, BDD r, int[] set)


(package private) static boolean[] fdddec2bin(BDDFactory bdd, int var, long val)


abstract BDD forAll(BDD 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()
          Get a value that represents this Object, as uniquely as possible within the confines of an int.

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.

abstract boolean isZero()
          Returns true if this BDD is the zero (false) BDD.

abstract BDD ite(BDD thenBDD, BDD elseBDD)
          if-then-else operator.

int level()
          Gets the level of this BDD.

double logSatCount()
          Calculates the log.

double logSatCount(BDD varset)
          Calculates the log.

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 zero-terminal with references to the one-terminal and vice-versa.

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.

(package private) int printdot_rec(java.io.PrintStream out, int current, boolean[] visited, java.util.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.

abstract BDD relprod(BDD that, BDD 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(BDD 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(BDD var, BDD pol)
          Finds one satisfying variable assignment.

long[] scanAllVar()
          Finds one satisfying assignment in this BDD of all the defined FDD variables.

int[] scanSet()
          Scans this BDD to find all occurrences of FDD variables and returns an array that contains the indices of the possible found FDD variables.

int[] scanSetDomains()
          Scans this BDD and copies the stored variables into a integer array of variable numbers.

long scanVar(BDDDomain d)
          Finds one satisfying assignment of the domain d in this BDD and returns that value.

abstract BDD simplify(BDD d)
          Coudert and Madre's restrict function.

abstract BDD support()
          Returns the variable support of this BDD.

java.lang.String toString()
          Convert this Object to a human-readable String.

java.lang.String toStringWithDomains()
          Returns a string representation of this BDD using the defined domains.

java.lang.String toStringWithDomains(BDD.BDDToString ts)
          Returns a string representation of this BDD on the defined domains, using the given BDDToString converter.

abstract BDD unique(BDD 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

BDD

protected BDD()

Protected constructor.

Method Detail

getFactory

public abstract BDDFactory getFactory()

Returns the factory that created this BDD.

isZero

public abstract boolean isZero()

Returns true if this BDD is the zero (false) BDD.

isOne

public abstract boolean isOne()

Returns true if this BDD is the one (true) BDD.

var

public abstract int var()

Gets the variable labeling the BDD.

Compare to bdd_var.

level

public int level()

Gets the level of this BDD.

Compare to LEVEL() macro.

high

public abstract BDD high()

Gets the true branch of this BDD.

Compare to bdd_high.

low

public abstract BDD low()

Gets the false branch of this BDD.

Compare to bdd_low.

id

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.

not

public abstract BDD not()

Negates this BDD by exchanging all references to the zero-terminal with references to the one-terminal and vice-versa.

Compare to bdd_not.

and

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.

andWith

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.

or

public 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.

orWith

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.

xor

public 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.

xorWith

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.

imp

public 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.

impWith

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.

biimp

public BDD biimp(BDD that)

Returns the logical 'bi-implication' of two BDDs. This is a shortcut for calling "apply" with the "biimp" operator.

Compare to bdd_biimp.

biimpWith

public BDD biimpWith(BDD that)

Makes this BDD be the logical 'bi-implication' 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.

ite

public abstract BDD ite(BDD thenBDD,
                        BDD elseBDD)

if-then-else operator.

Compare to bdd_ite.

relprod

public abstract BDD relprod(BDD that,
                            BDD 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.

compose

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.

veccompose

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.

constrain

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.

exist

public abstract BDD exist(BDD var)

Existential quantification of variables. Removes all occurrences of this BDD in variables in the set var by existential quantification.

Compare to bdd_exist.

forAll

public abstract BDD forAll(BDD var)

Universal quantification of variables. Removes all occurrences of this BDD in variables in the set var by universal quantification.

Compare to bdd_forall.

unique

public abstract BDD unique(BDD 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.

restrict

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.

Compare to bdd_restrict.

restrictWith

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.

Compare to bdd_restrict and bdd_delref.

simplify

public abstract BDD simplify(BDD 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.

support

public abstract BDD support()

Returns the variable support of this BDD. The support is all the variables that this BDD depends on.

Compare to bdd_support.

apply

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.

applyWith

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.

applyAll

public abstract BDD applyAll(BDD that,
                             BDDFactory.BDDOp opr,
                             BDD 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.

applyEx

public abstract BDD applyEx(BDD that,
                            BDDFactory.BDDOp opr,
                            BDD 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.

applyUni

public abstract BDD applyUni(BDD that,
                             BDDFactory.BDDOp opr,
                             BDD 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.

satOne

public abstract BDD satOne()

Finds one satisfying variable assignment. Finds a BDD with at most one variable at each levels. The new BDD implies this BDD and is not false unless this BDD is false.

Compare to bdd_satone.

fullSatOne

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.

satOne

public abstract BDD satOne(BDD var,
                           BDD 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 the false BDD then all variables will be in negative form, and otherwise they will be in positive form.

Compare to bdd_satoneset.

allsat

public abstract java.util.List allsat()

Finds all satisfying variable assignments.

Compare to bdd_allsat.

scanSet

public int[] scanSet()

Scans this BDD to find all occurrences of FDD variables and returns an array that contains the indices of the possible found FDD variables.

Compare to bdd_scanset.

scanSetDomains

public int[] scanSetDomains()

Scans this BDD and copies the stored variables into a integer array of variable numbers. The numbers returned are guaranteed to be in ascending order.

Compare to fdd_scanset.

scanVar

public long scanVar(BDDDomain d)

Finds one satisfying assignment of the domain d in this BDD and returns that value.

Compare to fdd_scanvar.

scanAllVar

public long[] scanAllVar()

Finds one satisfying assignment in this BDD of all the defined FDD variables. Each value is stored in an array which is returned. The size of this array is exactly the number of FDD variables defined.

Compare to fdd_scanallvar.

replace

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.

replaceWith

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.

printSet

public void printSet()

Prints the set of truth assignments specified by this BDD.

Compare to bdd_printset.

printSetWithDomains

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.

printDot

public void printDot()

Prints this BDD in dot graph notation.

Compare to bdd_printdot.

printdot_rec

int printdot_rec(java.io.PrintStream out,
                 int current,
                 boolean[] visited,
                 java.util.HashMap map)

nodeCount

public abstract int nodeCount()

Counts the number of distinct nodes used for this BDD.

Compare to bdd_nodecount.

pathCount

public abstract double pathCount()

Counts the number of paths leading to the true terminal.

Compare to bdd_pathcount.

satCount

public abstract double satCount()

Calculates the number of satisfying variable assignments.

Compare to bdd_satcount.

satCount

public double satCount(BDD varset)

Calculates the number of satisfying variable assignments to the variables in the given varset.

Compare to bdd_satcountset.

logSatCount

public double logSatCount()

Calculates the log. number of satisfying variable assignments.

Compare to bdd_satcount.

logSatCount

public double logSatCount(BDD varset)

Calculates the log. number of satisfying variable assignments to the variables in the given varset.

Compare to bdd_satcountset.

varProfile

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.

equals

public abstract boolean equals(BDD that)

Returns true if this BDD equals that BDD, false otherwise.

equals

public boolean equals(java.lang.Object o)

Description copied from class: java.lang.Object

Determine whether this Object is semantically equal to another Object.

There are some fairly strict requirements on this method which subclasses must follow:

It must be transitive. If a.equals(b) and b.equals(c), then a.equals(c) must be true as well.
It must be symmetric. a.equals(b) and b.equals(a) must have the same value.
It must be reflexive. a.equals(a) must always be true.
It must be consistent. Whichever value a.equals(b) returns on the first invocation must be the value returned on all later invocations.
a.equals(null) must be false.
It must be consistent with hashCode(). That is, a.equals(b) must imply a.hashCode() == b.hashCode(). The reverse is not true; two objects that are not equal may have the same hashcode, but that has the potential to harm hashing performance.

This is typically overridden to throw a java.lang.ClassCastException if the argument is not comparable to the class performing the comparison, but that is not a requirement. It is legal for a.equals(b) to be true even though a.getClass() != b.getClass(). Also, it is typical to never cause a java.lang.NullPointerException.

In general, the Collections API (java.util) use the equals method rather than the == operator to compare objects. However, java.util.IdentityHashMap is an exception to this rule, for its own good reasons.

The default implementation returns this == o.

hashCode

public abstract int hashCode()

Description copied from class: java.lang.Object

Get a value that represents this Object, as uniquely as possible within the confines of an int.

There are some requirements on this method which subclasses must follow:

Semantic equality implies identical hashcodes. In other words, if a.equals(b) is true, then a.hashCode() == b.hashCode() must be as well. However, the reverse is not necessarily true, and two objects may have the same hashcode without being equal.
It must be consistent. Whichever value o.hashCode() returns on the first invocation must be the value returned on all later invocations as long as the object exists. Notice, however, that the result of hashCode may change between separate executions of a Virtual Machine, because it is not invoked on the same object.

Notice that since hashCode is used in java.util.Hashtable and other hashing classes, a poor implementation will degrade the performance of hashing (so don't blindly implement it as returning a constant!). Also, if calculating the hash is time-consuming, a class may consider caching the results.

The default implementation returns System.identityHashCode(this)

toString

public java.lang.String toString()

Description copied from class: java.lang.Object

Convert this Object to a human-readable String. There are no limits placed on how long this String should be or what it should contain. We suggest you make it as intuitive as possible to be able to place it into System.out.println() 55 and such.

It is typical, but not required, to ensure that this method never completes abruptly with a java.lang.RuntimeException.

This method will be called when performing string concatenation with this object. If the result is null, string concatenation will instead use "null".

The default implementation returns getClass().getName() + "@" + Integer.toHexString(hashCode()).

bdd_printset_rec

private static void bdd_printset_rec(BDDFactory f,
                                     java.lang.StringBuffer sb,
                                     BDD r,
                                     int[] set)

toStringWithDomains

public java.lang.String toStringWithDomains()

Returns a string representation of this BDD using the defined domains.

toStringWithDomains

public java.lang.String toStringWithDomains(BDD.BDDToString ts)

Returns a string representation of this BDD on the defined domains, using the given BDDToString converter.

fdd_printset_helper

static void fdd_printset_helper(BDD.OutputBuffer sb,
                                long value,
                                int i,
                                int[] set,
                                int[] var,
                                int maxSkip)

fdd_printset_rec

static void fdd_printset_rec(BDDFactory bdd,
                             java.lang.StringBuffer sb,
                             BDD.BDDToString ts,
                             BDD r,
                             int[] set)

fdddec2bin

static boolean[] fdddec2bin(BDDFactory bdd,
                            int var,
                            long val)

free

public abstract void free()

Frees this BDD. Further use of this BDD will result in an exception being thrown.

Overview

Package

Class

Use

Deprecated

Index

Home >> All >> org >> sf >> [ javabdd overview ]

PREV CLASS NEXT CLASS

SUMMARY:

JAVADOC |

SOURCE |

DOWNLOAD | NESTED | FIELD | CONSTR | METHOD

DETAIL: FIELD | CONSTR | METHOD

Nested Class Summary
`static class`	`BDD.BDDToString` BDDToString is used to specify the printing behavior of BDDs with domains.
`(package private) static class`	`BDD.OutputBuffer`

Constructor Summary
`protected`	`BDD()` Protected constructor.

Method Summary
`abstract java.util.List`	`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, BDD 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, BDD 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, BDD 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.
`private static void`	`bdd_printset_rec(BDDFactory f, java.lang.StringBuffer sb, BDD r, int[] set)`
`BDD`	`biimp(BDD that)` Returns the logical 'bi-implication' of two BDDs.
`BDD`	`biimpWith(BDD that)` Makes this BDD be the logical 'bi-implication' 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(java.lang.Object o)` Determine whether this Object is semantically equal to another Object.
`abstract BDD`	`exist(BDD var)` Existential quantification of variables.
`(package private) static void`	`fdd_printset_helper(BDD.OutputBuffer sb, long value, int i, int[] set, int[] var, int maxSkip)`
`(package private) static void`	`fdd_printset_rec(BDDFactory bdd, java.lang.StringBuffer sb, BDD.BDDToString ts, BDD r, int[] set)`
`(package private) static boolean[]`	`fdddec2bin(BDDFactory bdd, int var, long val)`
`abstract BDD`	`forAll(BDD 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()` Get a value that represents this Object, as uniquely as possible within the confines of an int.
`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.
`abstract boolean`	`isZero()` Returns true if this BDD is the zero (false) BDD.
`abstract BDD`	`ite(BDD thenBDD, BDD elseBDD)` if-then-else operator.
`int`	`level()` Gets the level of this BDD.
`double`	`logSatCount()` Calculates the log.
`double`	`logSatCount(BDD varset)` Calculates the log.
`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 zero-terminal with references to the one-terminal and vice-versa.
`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.
`(package private) int`	`printdot_rec(java.io.PrintStream out, int current, boolean[] visited, java.util.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.
`abstract BDD`	`relprod(BDD that, BDD 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(BDD 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(BDD var, BDD pol)` Finds one satisfying variable assignment.
`long[]`	`scanAllVar()` Finds one satisfying assignment in this BDD of all the defined FDD variables.
`int[]`	`scanSet()` Scans this BDD to find all occurrences of FDD variables and returns an array that contains the indices of the possible found FDD variables.
`int[]`	`scanSetDomains()` Scans this BDD and copies the stored variables into a integer array of variable numbers.
`long`	`scanVar(BDDDomain d)` Finds one satisfying assignment of the domain d in this BDD and returns that value.
`abstract BDD`	`simplify(BDD d)` Coudert and Madre's restrict function.
`abstract BDD`	`support()` Returns the variable support of this BDD.
`java.lang.String`	`toString()` Convert this Object to a human-readable String.
`java.lang.String`	`toStringWithDomains()` Returns a string representation of this BDD using the defined domains.
`java.lang.String`	`toStringWithDomains(BDD.BDDToString ts)` Returns a string representation of this BDD on the defined domains, using the given BDDToString converter.
`abstract BDD`	`unique(BDD 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.

org.sf.javabdd Class BDD

BDD

getFactory

isZero

isOne

var

level

high

low

id

not

and

andWith

or

orWith

xor

xorWith

imp

impWith

biimp

biimpWith

ite

relprod

compose

veccompose

constrain

exist

forAll

unique

restrict

restrictWith

simplify

support

apply

applyWith

applyAll

applyEx

applyUni

satOne

fullSatOne

satOne

allsat

scanSet

scanSetDomains

scanVar

scanAllVar

replace

replaceWith

printSet

printSetWithDomains

printDot

printdot_rec

nodeCount

pathCount

satCount

satCount

logSatCount

logSatCount

varProfile

equals

equals

hashCode

toString

bdd_printset_rec

toStringWithDomains

toStringWithDomains

fdd_printset_helper

fdd_printset_rec

fdddec2bin

free

org.sf.javabdd
Class BDD