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 BuDDyFactory.BuDDyBDD  

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

Enclosing class:

BuDDyFactory

---

static class BuDDyFactory.BuDDyBDD

extends BDD

---

Nested Class Summary

 

Nested classes inherited from class org.sf.javabdd.BDD

BDD.BDDToString, BDD.OutputBuffer

 

Field Summary
private  int	_id           The value used by the BDD library.
(package private) static int	INVALID_BDD           An invalid id, for use in invalidating BDDs.
(package private) static boolean	USE_FINALIZER

 

Constructor Summary
private	BuDDyFactory.BuDDyBDD(int id)

 

Method Summary
private static void	addRef(int b)
java.util.List	allsat()           Finds all satisfying variable assignments.
private static byte[][]	allsat0(int b)
BDD	apply(BDD that, BDDFactory.BDDOp opr)           Returns the result of applying the binary operator opr to the two BDDs.
private static int	apply0(int b, int c, int opr)
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.
private static int	applyAll0(int b, int c, int opr, int d)
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.
private static int	applyEx0(int b, int c, int opr, int d)
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.
private static int	applyUni0(int b, int c, int opr, int d)
BDD	applyWith(BDD that, BDDFactory.BDDOp opr)           Makes this BDD be the result of the binary operator opr of two BDDs.
BDD	compose(BDD that, int var)           Functional composition.
private static int	compose0(int b, int c, int var)
BDD	constrain(BDD that)           Generalized cofactor.
private static int	constrain0(int b, int c)
private static void	delRef(int b)
boolean	equals(BDD that)           Returns true if this BDD equals that BDD, false otherwise.
BDD	exist(BDD var)           Existential quantification of variables.
private static int	exist0(int b, int var)
BDD	forAll(BDD var)           Universal quantification of variables.
private static int	forAll0(int b, int var)
void	free()           Frees this BDD.
BDD	fullSatOne()           Finds one satisfying variable assignment.
private static int	fullSatOne0(int b)
BDDFactory	getFactory()           Returns the factory that created this BDD.
int	hashCode()           Get a value that represents this Object, as uniquely as possible within the confines of an int.
BDD	high()           Gets the true branch of this BDD.
private static int	high0(int b)
BDD	id()           Identity function.
boolean	isOne()           Returns true if this BDD is the one (true) BDD.
boolean	isZero()           Returns true if this BDD is the zero (false) BDD.
BDD	ite(BDD thenBDD, BDD elseBDD)           if-then-else operator.
private static int	ite0(int b, int c, int d)
double	logSatCount()           Calculates the log.
double	logSatCount(BDD varset)           Calculates the log.
private static double	logSatCount0(int b)
private static double	logSatCount1(int b, int c)
BDD	low()           Gets the false branch of this BDD.
private static int	low0(int b)
int	nodeCount()           Counts the number of distinct nodes used for this BDD.
private static int	nodeCount0(int b)
BDD	not()           Negates this BDD by exchanging all references to the zero-terminal with references to the one-terminal and vice-versa.
private static int	not0(int b)
double	pathCount()           Counts the number of paths leading to the true terminal.
private static double	pathCount0(int b)
void	printDot()           Prints this BDD in dot graph notation.
private static void	printDot0(int b)
void	printSet()           Prints the set of truth assignments specified by this BDD.
private static void	printSet0(int b)
BDD	relprod(BDD that, BDD var)           Relational product.
private static int	relprod0(int b, int c, int d)
BDD	replace(BDDPairing pair)           Returns a BDD where all variables are replaced with the variables defined by pair.
private static int	replace0(int b, long p)
BDD	replaceWith(BDDPairing pair)           Replaces all variables in this BDD with the variables defined by pair.
BDD	restrict(BDD var)           Restrict a set of variables to constant values.
private static int	restrict0(int b, int var)
BDD	restrictWith(BDD var)           Mutates this BDD to restrict a set of variables to constant values.
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.
private static double	satCount0(int b)
private static double	satCount1(int b, int c)
BDD	satOne()           Finds one satisfying variable assignment.
BDD	satOne(BDD var, BDD pol)           Finds one satisfying variable assignment.
private static int	satOne0(int b)
private static int	satOne1(int b, int c, int d)
BDD	simplify(BDD d)           Coudert and Madre's restrict function.
private static int	simplify0(int b, int d)
BDD	support()           Returns the variable support of this BDD.
private static int	support0(int b)
BDD	unique(BDD var)           Unique quantification of variables.
private static int	unique0(int b, int var)
int	var()           Gets the variable labeling the BDD.
private static int	var0(int b)
int[]	varProfile()           Counts the number of times each variable occurs in this BDD.
private static int[]	varProfile0(int b)
BDD	veccompose(BDDPairing pair)           Simultaneous functional composition.
private static int	veccompose0(int b, long p)

 

Methods inherited from class org.sf.javabdd.BDD

and, andWith, biimp, biimpWith, equals, fdd_printset_helper, fdd_printset_rec, fdddec2bin, imp, impWith, level, or, orWith, printdot_rec, printSetWithDomains, scanAllVar, scanSet, scanSetDomains, scanVar, toString, toStringWithDomains, toStringWithDomains, xor, xorWith

 

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

_id

private int _id

The value used by the BDD library.

---

INVALID_BDD

static final int INVALID_BDD

An invalid id, for use in invalidating BDDs.

See Also:

Constant Field Values

---

USE_FINALIZER

static final boolean USE_FINALIZER

See Also:

Constant Field Values

Constructor Detail

BuDDyFactory.BuDDyBDD

private BuDDyFactory.BuDDyBDD(int id)

Method Detail

getFactory

public BDDFactory getFactory()

Description copied from class: BDD

Returns the factory that created this BDD.

Specified by:

getFactory in class BDD

---

isZero

public boolean isZero()

Description copied from class: BDD

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

Specified by:

isZero in class BDD

---

isOne

public boolean isOne()

Description copied from class: BDD

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

Specified by:

isOne in class BDD

---

var

public int var()

Description copied from class: BDD

Gets the variable labeling the BDD.

Compare to bdd_var.

Specified by:

var in class BDD

---

var0

private static int var0(int b)

---

high

public BDD high()

Description copied from class: BDD

Gets the true branch of this BDD.

Compare to bdd_high.

Specified by:

high in class BDD

---

high0

private static int high0(int b)

---

low

public BDD low()

Description copied from class: BDD

Gets the false branch of this BDD.

Compare to bdd_low.

Specified by:

low in class BDD

---

low0

private static int low0(int b)

---

id

public BDD id()

Description copied from class: BDD

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.

Specified by:

id in class BDD

---

not

public BDD not()

Description copied from class: BDD

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

Compare to bdd_not.

Specified by:

not in class BDD

---

not0

private static int not0(int b)

---

ite

public BDD ite(BDD thenBDD,
               BDD elseBDD)

Description copied from class: BDD

if-then-else operator.

Compare to bdd_ite.

Specified by:

ite in class BDD

---

ite0

private static int ite0(int b,
                        int c,
                        int d)

---

relprod

public BDD relprod(BDD that,
                   BDD var)

Description copied from class: BDD

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.

Specified by:

relprod in class BDD

---

relprod0

private static int relprod0(int b,
                            int c,
                            int d)

---

compose

public BDD compose(BDD that,
                   int var)

Description copied from class: BDD

Functional composition. Substitutes the variable var with the BDD that in this BDD: result = f[g/var].

Compare to bdd_compose.

Specified by:

compose in class BDD

---

compose0

private static int compose0(int b,
                            int c,
                            int var)

---

constrain

public BDD constrain(BDD that)

Description copied from class: BDD

Generalized cofactor. Computes the generalized cofactor of this BDD with respect to the given BDD.

Compare to bdd_constrain.

Specified by:

constrain in class BDD

---

constrain0

private static int constrain0(int b,
                              int c)

---

exist

public BDD exist(BDD var)

Description copied from class: BDD

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

Compare to bdd_exist.

Specified by:

exist in class BDD

---

exist0

private static int exist0(int b,
                          int var)

---

forAll

public BDD forAll(BDD var)

Description copied from class: BDD

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

Compare to bdd_forall.

Specified by:

forAll in class BDD

---

forAll0

private static int forAll0(int b,
                           int var)

---

unique

public BDD unique(BDD var)

Description copied from class: BDD

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.

Specified by:

unique in class BDD

---

unique0

private static int unique0(int b,
                           int var)

---

restrict

public BDD restrict(BDD var)

Description copied from class: BDD

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.

Specified by:

restrict in class BDD

---

restrict0

private static int restrict0(int b,
                             int var)

---

restrictWith

public BDD restrictWith(BDD var)

Description copied from class: BDD

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.

Specified by:

restrictWith in class BDD

---

simplify

public BDD simplify(BDD d)

Description copied from class: BDD

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.

Specified by:

simplify in class BDD

---

simplify0

private static int simplify0(int b,
                             int d)

---

support

public BDD support()

Description copied from class: BDD

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

Compare to bdd_support.

Specified by:

support in class BDD

---

support0

private static int support0(int b)

---

apply

public BDD apply(BDD that,
                 BDDFactory.BDDOp opr)

Description copied from class: BDD

Returns the result of applying the binary operator opr to the two BDDs.

Compare to bdd_apply.

Specified by:

apply in class BDD

---

apply0

private static int apply0(int b,
                          int c,
                          int opr)

---

applyWith

public BDD applyWith(BDD that,
                     BDDFactory.BDDOp opr)

Description copied from class: BDD

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.

Specified by:

applyWith in class BDD

---

applyAll

public BDD applyAll(BDD that,
                    BDDFactory.BDDOp opr,
                    BDD var)

Description copied from class: BDD

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.

Specified by:

applyAll in class BDD

---

applyAll0

private static int applyAll0(int b,
                             int c,
                             int opr,
                             int d)

---

applyEx

public BDD applyEx(BDD that,
                   BDDFactory.BDDOp opr,
                   BDD var)

Description copied from class: BDD

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.

Specified by:

applyEx in class BDD

---

applyEx0

private static int applyEx0(int b,
                            int c,
                            int opr,
                            int d)

---

applyUni

public BDD applyUni(BDD that,
                    BDDFactory.BDDOp opr,
                    BDD var)

Description copied from class: BDD

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.

Specified by:

applyUni in class BDD

---

applyUni0

private static int applyUni0(int b,
                             int c,
                             int opr,
                             int d)

---

satOne

public BDD satOne()

Description copied from class: BDD

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.

Specified by:

satOne in class BDD

---

satOne0

private static int satOne0(int b)

---

fullSatOne

public BDD fullSatOne()

Description copied from class: BDD

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.

Specified by:

fullSatOne in class BDD

---

fullSatOne0

private static int fullSatOne0(int b)

---

satOne

public BDD satOne(BDD var,
                  BDD pol)

Description copied from class: BDD

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.

Specified by:

satOne in class BDD

---

satOne1

private static int satOne1(int b,
                           int c,
                           int d)

---

allsat

public java.util.List allsat()

Description copied from class: BDD

Finds all satisfying variable assignments.

Compare to bdd_allsat.

Specified by:

allsat in class BDD

---

allsat0

private static byte[][] allsat0(int b)

---

printSet

public void printSet()

Description copied from class: BDD

Prints the set of truth assignments specified by this BDD.

Compare to bdd_printset.

Overrides:

printSet in class BDD

---

printSet0

private static void printSet0(int b)

---

printDot

public void printDot()

Description copied from class: BDD

Prints this BDD in dot graph notation.

Compare to bdd_printdot.

Overrides:

printDot in class BDD

---

printDot0

private static void printDot0(int b)

---

nodeCount

public int nodeCount()

Description copied from class: BDD

Counts the number of distinct nodes used for this BDD.

Compare to bdd_nodecount.

Specified by:

nodeCount in class BDD

---

nodeCount0

private static int nodeCount0(int b)

---

pathCount

public double pathCount()

Description copied from class: BDD

Counts the number of paths leading to the true terminal.

Compare to bdd_pathcount.

Specified by:

pathCount in class BDD

---

pathCount0

private static double pathCount0(int b)

---

satCount

public double satCount()

Description copied from class: BDD

Calculates the number of satisfying variable assignments.

Compare to bdd_satcount.

Specified by:

satCount in class BDD

---

satCount0

private static double satCount0(int b)

---

satCount

public double satCount(BDD varset)

Description copied from class: BDD

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

Compare to bdd_satcountset.

Overrides:

satCount in class BDD

---

satCount1

private static double satCount1(int b,
                                int c)

---

logSatCount

public double logSatCount()

Description copied from class: BDD

Calculates the log. number of satisfying variable assignments.

Compare to bdd_satcount.

Overrides:

logSatCount in class BDD

---

logSatCount0

private static double logSatCount0(int b)

---

logSatCount

public double logSatCount(BDD varset)

Description copied from class: BDD

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

Compare to bdd_satcountset.

Overrides:

logSatCount in class BDD

---

logSatCount1

private static double logSatCount1(int b,
                                   int c)

---

varProfile

public int[] varProfile()

Description copied from class: BDD

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.

Specified by:

varProfile in class BDD

---

varProfile0

private static int[] varProfile0(int b)

---

addRef

private static void addRef(int b)

---

delRef

private static void delRef(int b)

---

free

public void free()

Description copied from class: BDD

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

Specified by:

free in class BDD

---

veccompose

public BDD veccompose(BDDPairing pair)

Description copied from class: BDD

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.

Specified by:

veccompose in class BDD

---

veccompose0

private static int veccompose0(int b,
                               long p)

---

replace

public BDD replace(BDDPairing pair)

Description copied from class: BDD

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.

Specified by:

replace in class BDD

---

replace0

private static int replace0(int b,
                            long p)

---

replaceWith

public BDD replaceWith(BDDPairing pair)

Description copied from class: BDD

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.

Specified by:

replaceWith in class BDD

---

equals

public boolean equals(BDD that)

Description copied from class: BDD

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

Specified by:

equals in class BDD

---

hashCode

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

Specified by:

hashCode in class 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

---