Docjar: A Java Source and Docuemnt Enginecom.*    java.*    javax.*    org.*    all    new    plug-in

Quick Search    Search Deep
Overview  Package   Class  Use  Deprecated  Index 
Home >> All >> org >> sf >> [ javabdd overview ]  PREV CLASS  NEXT CLASS
SUMMARY: JavaDoc of org.sf.javabdd.JavaFactory JAVADOC | Sourc code of org.sf.javabdd.JavaFactory SOURCE | Download org.sf.javabdd.JavaFactory DOWNLOAD | NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.sf.javabdd
Class JavaFactory.bdd  view JavaFactory.bdd download JavaFactory.bdd.java

java.lang.Object
  extended byorg.sf.javabdd.BDD
      extended byorg.sf.javabdd.JavaFactory.bdd
Enclosing class:
JavaFactory
class JavaFactory.bdd
extends BDD

Wrapper for the BDD index number used internally in the representation.

Nested Class Summary
 
Nested classes inherited from class org.sf.javabdd.BDD
BDD.BDDToString, BDD.OutputBuffer
 
Field Summary
(package private)  int _index
           
(package private) static int INVALID_BDD
           
(package private) static boolean USE_FINALIZER
           
 
Constructor Summary
(package private) JavaFactory.bdd(int index)
           
 
Method Summary
 java.util.List allsat()
          Finds all satisfying variable assignments.
 BDD apply(BDD that, BDDFactory.BDDOp opr)
          Returns the result of applying the binary operator opr to the two BDDs.
 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.
 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.
 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.
 BDD applyWith(BDD that, BDDFactory.BDDOp opr)
          Makes this BDD be the result of the binary operator opr of two BDDs.
 BDD compose(BDD g, int var)
          Functional composition.
 BDD constrain(BDD that)
          Generalized cofactor.
 boolean equals(BDD that)
          Returns true if this BDD equals that BDD, false otherwise.
 BDD exist(BDD var)
          Existential quantification of variables.
 BDD forAll(BDD var)
          Universal quantification of variables.
 void free()
          Frees this BDD.
 BDD fullSatOne()
          Finds one satisfying variable assignment.
 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.
 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.
 BDD low()
          Gets the false branch of this BDD.
 int nodeCount()
          Counts the number of distinct nodes used for this BDD.
 BDD not()
          Negates this BDD by exchanging all references to the zero-terminal with references to the one-terminal and vice-versa.
 double pathCount()
          Counts the number of paths leading to the true terminal.
 BDD relprod(BDD that, BDD var)
          Relational product.
 BDD replace(BDDPairing pair)
          Returns a BDD where all variables are replaced with the variables defined by pair.
 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.
 BDD restrictWith(BDD that)
          Mutates this BDD to restrict a set of variables to constant values.
 double satCount()
          Calculates the number of satisfying variable assignments.
 BDD satOne()
          Finds one satisfying variable assignment.
 BDD satOne(BDD var, BDD pol)
          Finds one satisfying variable assignment.
 BDD simplify(BDD d)
          Coudert and Madre's restrict function.
 BDD support()
          Returns the variable support of this BDD.
 BDD unique(BDD var)
          Unique quantification of variables.
 int var()
          Gets the variable labeling the BDD.
 int[] varProfile()
          Counts the number of times each variable occurs in this BDD.
 BDD veccompose(BDDPairing pair)
          Simultaneous functional composition.
 
Methods inherited from class org.sf.javabdd.BDD
and, andWith, biimp, biimpWith, equals, fdd_printset_helper, fdd_printset_rec, fdddec2bin, imp, impWith, level, logSatCount, logSatCount, or, orWith, printdot_rec, printDot, printSet, printSetWithDomains, satCount, 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

_index

int _index

INVALID_BDD

static final int INVALID_BDD
See Also:
Constant Field Values

USE_FINALIZER

static final boolean USE_FINALIZER
See Also:
Constant Field Values
Constructor Detail

JavaFactory.bdd

JavaFactory.bdd(int index)
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

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

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

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

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

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

compose

public BDD compose(BDD g,
                   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

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

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

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

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

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

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

restrictWith

public BDD restrictWith(BDD that)
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
Overview  Package   Class  Use  Deprecated  Index 
Home >> All >> org >> sf >> [ javabdd overview ]  PREV CLASS  NEXT CLASS
SUMMARY: JavaDoc of org.sf.javabdd.JavaFactory JAVADOC | Sourc code of org.sf.javabdd.JavaFactory SOURCE | Download org.sf.javabdd.JavaFactory DOWNLOAD | NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD