net.sf.javabdd
Class TypedBDDFactory.TypedBDD

java.lang.Object
  extended by net.sf.javabdd.BDD
      extended by net.sf.javabdd.TypedBDDFactory.TypedBDD
Enclosing class:
TypedBDDFactory

public class TypedBDDFactory.TypedBDD
extends BDD

A BDD with types (domains) attached to it.

Version:
$Id: TypedBDDFactory.java 456 2006-07-17 05:19:54Z joewhaley $
Author:
jwhaley

Nested Class Summary
 
Nested classes/interfaces inherited from class net.sf.javabdd.BDD
BDD.AllSatIterator, BDD.BDDIterator, BDD.BDDToString
 
Constructor Summary
TypedBDDFactory.TypedBDD(BDD bdd, Set dom)
           
 
Method Summary
 BDD.AllSatIterator 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, BDDVarSet 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, BDDVarSet 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, BDDVarSet 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(BDDVarSet var)
          Existential quantification of variables.
 BDD forAll(BDDVarSet var)
          Universal quantification of variables.
 void free()
          Frees this BDD.
 BDD fullSatOne()
          Finds one satisfying variable assignment.
 Set getDomainSet()
          Returns the set of domains that this BDD uses.
 BDDFactory getFactory()
          Returns the factory that created this BDD.
 int hashCode()
           
 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.BDDIterator iterator()
           
 BDD.BDDIterator iterator(BDDVarSet var)
          Returns an iteration of the satisfying assignments of this BDD.
 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, BDDVarSet 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 var)
          Mutates this BDD to restrict a set of variables to constant values.
 double satCount()
          Calculates the number of satisfying variable assignments.
 double satCount(BDDVarSet set)
          Calculates the number of satisfying variable assignments to the variables in the given varset.
 BDD satOne()
          Finds one satisfying variable assignment.
 BDD satOne(BDDVarSet var, boolean pol)
          Finds one satisfying variable assignment.
 void setDomains(BDDDomain d)
          Changes this BDD's domain to be the given domain.
 void setDomains(BDDDomain d1, BDDDomain d2)
          Changes this BDD's domains to be the given domains.
 void setDomains(BDDDomain d1, BDDDomain d2, BDDDomain d3)
          Changes this BDD's domains to be the given domains.
 void setDomains(BDDDomain d1, BDDDomain d2, BDDDomain d3, BDDDomain d4)
          Changes this BDD's domains to be the given domains.
 void setDomains(BDDDomain d1, BDDDomain d2, BDDDomain d3, BDDDomain d4, BDDDomain d5)
          Changes this BDD's domains to be the given domains.
 void setDomains(Set d)
          Changes this BDD's domains to be the given set.
 BDD simplify(BDDVarSet d)
          Coudert and Madre's restrict function.
 BDDVarSet support()
          Returns the variable support of this BDD.
 BDDVarSet toVarSet()
          Converts this BDD to a new BDDVarSet.
 BDD unique(BDDVarSet 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 net.sf.javabdd.BDD
and, andWith, biimp, biimpWith, equals, imp, impWith, isUniverse, level, logSatCount, logSatCount, or, orWith, printdot_rec, printDot, printSet, printSetWithDomains, scanAllVar, scanVar, toString, toStringWithDomains, toStringWithDomains, xor, xorWith
 
Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
 

Constructor Detail

TypedBDDFactory.TypedBDD

public TypedBDDFactory.TypedBDD(BDD bdd,
                                Set dom)
Method Detail

toVarSet

public BDDVarSet toVarSet()
Description copied from class: BDD

Converts this BDD to a new BDDVarSet.

This BDD must be a boolean function that represents the all-true minterm of the BDD variables of interest.

Overrides:
toVarSet in class BDD
Returns:
the contents of this BDD as a new BDDVarSet

getDomainSet

public Set getDomainSet()
Returns the set of domains that this BDD uses.


setDomains

public void setDomains(Set d)
Changes this BDD's domains to be the given set.


setDomains

public void setDomains(BDDDomain d)
Changes this BDD's domain to be the given domain.


setDomains

public void setDomains(BDDDomain d1,
                       BDDDomain d2)
Changes this BDD's domains to be the given domains.


setDomains

public void setDomains(BDDDomain d1,
                       BDDDomain d2,
                       BDDDomain d3)
Changes this BDD's domains to be the given domains.


setDomains

public void setDomains(BDDDomain d1,
                       BDDDomain d2,
                       BDDDomain d3,
                       BDDDomain d4)
Changes this BDD's domains to be the given domains.


setDomains

public void setDomains(BDDDomain d1,
                       BDDDomain d2,
                       BDDDomain d3,
                       BDDDomain d4,
                       BDDDomain d5)
Changes this BDD's domains to be the given domains.


getFactory

public BDDFactory getFactory()
Description copied from class: BDD

Returns the factory that created this BDD.

Specified by:
getFactory in class BDD
Returns:
factory that created this 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
Returns:
true if this BDD is the zero (false) 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
Returns:
true if this BDD is the one (true) 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
Returns:
the index of the variable labeling the 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
Returns:
true branch of this 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
Returns:
false branch of this 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
Returns:
copy of this 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
Returns:
the negated 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
Parameters:
thenBDD - the 'then' BDD
elseBDD - the 'else' BDD
Returns:
the result of the if-then-else operator on the three BDDs

relprod

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

Overrides:
relprod in class BDD
Parameters:
that - the BDD to 'and' with
var - the BDDVarSet to existentially quantify with
Returns:
the result of the relational product
See Also:
BDDDomain.set()

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
Parameters:
g - the function to use to replace
var - the variable number to replace
Returns:
the result of the functional composition

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
Parameters:
pair - the pairing of variables to functions
Returns:
BDD the result of the simultaneous functional composition

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
Parameters:
that - the BDD with which to compute the generalized cofactor
Returns:
the result of the generalized cofactor

exist

public BDD exist(BDDVarSet 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
Parameters:
var - BDDVarSet containing the variables to be existentially quantified
Returns:
the result of the existential quantification
See Also:
BDDDomain.set()

forAll

public BDD forAll(BDDVarSet 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
Parameters:
var - BDDVarSet containing the variables to be universally quantified
Returns:
the result of the universal quantification
See Also:
BDDDomain.set()

unique

public BDD unique(BDDVarSet 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
Parameters:
var - BDDVarSet containing the variables to be uniquely quantified
Returns:
the result of the unique quantification
See Also:
BDDDomain.set()

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.

Note that this is quite different than Coudert and Madre's restrict function.

Compare to bdd_restrict.

Specified by:
restrict in class BDD
Parameters:
var - BDD containing the variables to be restricted
Returns:
the result of the restrict operation
See Also:
net.sf.javabdd.BDD#simplify(BDD)

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.

Note that this is quite different than Coudert and Madre's restrict function.

Compare to bdd_restrict and bdd_delref.

Specified by:
restrictWith in class BDD
Parameters:
var - BDD containing the variables to be restricted
See Also:
BDDDomain.set()

simplify

public BDD simplify(BDDVarSet 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
Parameters:
d - BDDVarSet containing the variables in the domain
Returns:
the result of the simplify operation

support

public BDDVarSet 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
Returns:
the variable support of this 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
Parameters:
that - the BDD to apply the operator on
opr - the operator to apply
Returns:
the result of applying the operator

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
Parameters:
that - the BDD to apply the operator on
opr - the operator to apply

applyAll

public BDD applyAll(BDD that,
                    BDDFactory.BDDOp opr,
                    BDDVarSet 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
Parameters:
that - the BDD to apply the operator on
opr - the operator to apply
var - BDDVarSet containing the variables to quantify
Returns:
the result
See Also:
BDDDomain.set()

applyEx

public BDD applyEx(BDD that,
                   BDDFactory.BDDOp opr,
                   BDDVarSet 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
Parameters:
that - the BDD to apply the operator on
opr - the operator to apply
var - BDDVarSet containing the variables to quantify
Returns:
the result
See Also:
BDDDomain.set()

applyUni

public BDD applyUni(BDD that,
                    BDDFactory.BDDOp opr,
                    BDDVarSet 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
Parameters:
that - the BDD to apply the operator on
opr - the operator to apply
var - BDDVarSet containing the variables to quantify
Returns:
the result
See Also:
BDDDomain.set()

satOne

public BDD satOne()
Description copied from class: BDD

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.

Specified by:
satOne in class BDD
Returns:
one satisfying variable assignment

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
Returns:
one satisfying variable assignment

satOne

public BDD satOne(BDDVarSet var,
                  boolean 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 false, then all variables will be in negative form. Otherwise they will be in positive form.

Compare to bdd_satoneset.

Specified by:
satOne in class BDD
Parameters:
var - BDDVarSet containing the set of variables that must be mentioned in the result
pol - the polarity of the result
Returns:
one satisfying variable assignment
See Also:
BDDDomain.set()

allsat

public BDD.AllSatIterator allsat()
Description copied from class: BDD

Finds all satisfying variable assignments.

Compare to bdd_allsat.

Overrides:
allsat in class BDD
Returns:
all satisfying variable assignments

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
Parameters:
pair - pairing of variables to the BDDs that replace those variables
Returns:
result of replace

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
Parameters:
pair - pairing of variables to the BDDs that replace those variables

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
Returns:
the number of distinct nodes used for this 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
Returns:
the number of paths leading to the true terminal

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
Returns:
the number of satisfying variable assignments

satCount

public double satCount(BDDVarSet set)
Description copied from class: BDD

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.

Overrides:
satCount in class BDD
Returns:
the number of satisfying variable assignments

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
Parameters:
that - the BDD to compare with
Returns:
true iff the two BDDs are equal

hashCode

public int hashCode()
Specified by:
hashCode in class BDD

iterator

public BDD.BDDIterator iterator(BDDVarSet var)
Description copied from class: BDD

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.

Overrides:
iterator in class BDD
Parameters:
var - set of variables to mention in result
Returns:
an iteration of minterms
See Also:
BDDDomain.set()

iterator

public BDD.BDDIterator iterator()

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


Copyright © 2003-2007 John Whaley. All Rights Reserved.