Type Parameters:

T - the type of the variables

All Known Implementing Classes:

JBDD
```
public interface BDD<T>
```
The BDD is an interface containing the very basic functionality of a BDD. Thus, it is used as a front end for the various available BDD packages.

Method Summary

All Methods Instance Methods Abstract Methods
Modifier and Type	Method	Description
`java.util.Iterator<BDD<T>>`	`allsat()`	Returns a `BDD` `Iterator` containing all satisfying variable assignments.
`BDD<T>`	`and(BDD<T> that)`	Returns the logical `and` of two BDDs.
`void`	`andWith(java.util.Collection<T> that)`	Makes this BDD the logical `and` of this and `that` variables.
`void`	`andWith(BDD<T> that)`	Makes this BDD the logical `and` of this and `that` `BDD`.
`void`	`andWith(T that)`	Makes this BDD the logical `and` of this and `that` variable.
`BDD<T>`	`copy()`	Returns a copy of this `BDD`.
`boolean`	`equals(java.lang.Object that)`	TODO Returns `true` if this BDD equals `that` BDD.
`BDD<T>`	`exist(T variable)`	Returns this `BDD` after an existential quantification of the specified variable.
`BDD<T>`	`forAll(T variable)`	Returns this `BDD` after a universal quantification of the specified variable.
`void`	`free()`	Destroys this `BDD`.
`BDDProvider<T>`	`getProvider()`	Returns the used `BDDProvider`.
`java.util.Set<T>`	`getVariables()`	Returns the set of variables that are used in this `BDD`.
`BDD<T>`	`high()`	Returns the `true` or `1` branch of this BDD.
`BDD<T>`	`imp(BDD<T> that)`	Returns the logical implication of two `BDD`s.
`void`	`impWith(BDD<T> that)`	Returns the logical implication of two `BDD`s.
`void`	`impWith(T that)`	Makes this BDD the logical implication of this and `that` variable.
`boolean`	`isOne()`	Returns `true` if this BDD is the `one` BDD.
`boolean`	`isZero()`	Returns `true` if this BDD is the `zero` BDD.
`BDD<T>`	`ite(BDD<T> thenBDD, BDD<T> elseBDD)`	Returns the if-then-else} `BDD` with this `BDD` being the if, the `thenBDD` being the then and `elseBDD` being the else statement.
`int`	`level()`	Returns the level of this `BDD`.
`BDD<T>`	`low()`	Returns the `false` or `0` branch of this `BDD`.
`int`	`nodeCount()`	Returns the number of node in this `BDD`.
`BDD<T>`	`not()`	Returns a `BDD` that is the negation of this `BDD`.
`BDD<T>`	`or(BDD<T> that)`	Returns the logical or of two `BDD`s.
`void`	`orWith(java.util.Collection<T> that)`	Makes this `BDD` the logical or of this and `that` variables.
`void`	`orWith(BDD<T> that)`	Makes this BDD the logical or of this and `that` `BDD`.
`void`	`orWith(T that)`	Makes this BDD the logical or of this and `that` variable.
`BDD<T>`	`replace(T variable1, T variable2)`	Returns a `BDD` where the variable for `variable1` is replaced with the variable of `variable2`.
`void`	`replaceWith(T variable1, T variable2)`	Replaces the variable for `variable1` with the variable of `variable2` in this `BDD`.
`BDD<T>`	`restrict(BDD<T> that)`	Returns a `BDD` where the variables of `that` `BDD` are set to constant reliabilityFunctions in this BDD.
`void`	`restrictWith(BDD<T> that)`	Restricts the variables of `that` to constant reliabilityFunctions in this BDD.
`BDD<T>`	`sat()`	Returns one satisfying variable assignment as a `BDD`.
`T`	`var()`	Returns the variable labeling the `BDD`.
`BDD<T>`	`xor(BDD<T> that)`	Returns the logical xor of two `BDD`s.
`void`	`xorWith(BDD<T> that)`	Makes this `BDD` the logical xor of this and `that` BDD.
`void`	`xorWith(T that)`	Makes this `BDD` the logical xor of this and `that` variable.

- Method Detail
  - allsat
```
java.util.Iterator<BDD<T>> allsat()
```
    Returns a BDD Iterator containing all satisfying variable assignments.
    
    Returns:
    
    all satisfying variable assignments
  - and
```
BDD<T> and(BDD<T> that)
```
    Returns the logical and of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
    
    Parameters:
    
    that - the BDD to and with this BDD
    
    Returns:
    
    the logical and of the two BDDs
  - andWith
```
void andWith(BDD<T> that)
```
    Makes this BDD the logical and of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
    
    Parameters:
    
    that - the BDD to and with this BDD
  - andWith
```
void andWith(java.util.Collection<T> that)
```
    Makes this BDD the logical and of this and that variables.
    
    Parameters:
    
    that - the variables to and with this BDD
  - andWith
```
void andWith(T that)
```
    Makes this BDD the logical and of this and that variable.
    
    Parameters:
    
    that - the variable to and with this BDD
  - equals
```
boolean equals(java.lang.Object that)
```
    TODO Returns true if this BDD equals that BDD.
    
    Overrides:
    
    equals in class java.lang.Object
    
    Parameters:
    
    that - the BDD to compare with this BDD
    
    Returns:
    
    true if this BDD equals that BDD
  - exist
```
BDD<T> exist(T variable)
```
    Returns this BDD after an existential quantification of the specified variable.
    
    Parameters:
    
    variable - the variable for the existential quantification
    
    Returns:
    
    this BDD after an existential quantification of the specified variables
  - forAll
```
BDD<T> forAll(T variable)
```
    Returns this BDD after a universal quantification of the specified variable.
    
    Parameters:
    
    variable - the variable for the universal quantification
    
    Returns:
    
    this BDD after a universal quantification of the specified variables
  - sat
```
BDD<T> sat()
```
    Returns one satisfying variable assignment as a BDD.
    
    Returns:
    
    one satisfying variable assignment as a BDD
  - high
```
BDD<T> high()
```
    Returns the true or 1 branch of this BDD.
    
    Returns:
    
    the true or 1 branch of this BDD
  - getProvider
```
BDDProvider<T> getProvider()
```
    Returns the used BDDProvider.
    
    Returns:
    
    the used bdd provider
  - isOne
```
boolean isOne()
```
    Returns true if this BDD is the one BDD.
    
    Returns:
    
    true if this BDD is the one BDD
  - isZero
```
boolean isZero()
```
    Returns true if this BDD is the zero BDD.
    
    Returns:
    
    true if this BDD is the zero BDD
  - ite
```
BDD<T> ite(BDD<T> thenBDD,
           BDD<T> elseBDD)
```
    Returns the if-then-else} BDD with this BDD being the if, the thenBDD being the then and elseBDD being the else statement.
    
    Parameters:
    
    thenBDD - the BDD for the then statement
    
    elseBDD - the BDD for the else statement
    
    Returns:
    
    the if-then-else BDD
  - level
```
int level()
```
    Returns the level of this BDD.
    
    Returns:
    
    the level of this BDD
  - low
```
BDD<T> low()
```
    Returns the false or 0 branch of this BDD.
    
    Returns:
    
    the false or 0 branch of this BDD
  - not
```
BDD<T> not()
```
    Returns a BDD that is the negation of this BDD.
    
    Returns:
    
    a BDD that is the negation of this BDD
  - nodeCount
```
int nodeCount()
```
    Returns the number of node in this BDD.
    
    Returns:
    
    the number of nodes in this bdd
  - or
```
BDD<T> or(BDD<T> that)
```
    Returns the logical or of two BDDs. Note: Both BDDs remain unchanged after this or-operation.
    
    Parameters:
    
    that - the BDD to or with this BDD
    
    Returns:
    
    the logical or of the two BDDs
  - orWith
```
void orWith(BDD<T> that)
```
    Makes this BDD the logical or of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
    
    Parameters:
    
    that - the BDD to or with this BDD
  - orWith
```
void orWith(java.util.Collection<T> that)
```
    Makes this BDD the logical or of this and that variables.
    
    Parameters:
    
    that - the variables to or with this BDD
  - orWith
```
void orWith(T that)
```
    Makes this BDD the logical or of this and that variable.
    
    Parameters:
    
    that - the variable to or with this BDD
  - replace
```
BDD<T> replace(T variable1,
               T variable2)
```
    Returns a BDD where the variable for variable1 is replaced with the variable of variable2.
    
    Parameters:
    
    variable1 - the first variable
    
    variable2 - the second variable
    
    Returns:
    
    a BDD where the variable for variable1 is replaced with the variable of variable2
  - replaceWith
```
void replaceWith(T variable1,
                 T variable2)
```
    Replaces the variable for variable1 with the variable of variable2 in this BDD.
    
    Parameters:
    
    variable1 - the first variable
    
    variable2 - the second variable
  - restrict
```
BDD<T> restrict(BDD<T> that)
```
    Returns a BDD where the variables of that BDD are set to constant reliabilityFunctions in this BDD. Note: Both BDDs remain unchanged after this or-operation.
    
    Parameters:
    
    that - the BDD to restrict this BDD with
    
    Returns:
    
    a new BDD representing this BDD restricted with that BDD
  - restrictWith
```
void restrictWith(BDD<T> that)
```
    Restricts the variables of that to constant reliabilityFunctions in this BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
    
    Parameters:
    
    that - the BDD to restrict this BDD with
  - var
```
T var()
```
    Returns the variable labeling the BDD.
    
    Returns:
    
    the variable labeling the BDD
  - xor
```
BDD<T> xor(BDD<T> that)
```
    Returns the logical xor of two BDDs. Note: Both BDDs remain unchanged after this xor-operation.
    
    Parameters:
    
    that - the BDD to xor with this BDD
    
    Returns:
    
    the logical xor of the two BDDs
  - xorWith
```
void xorWith(BDD<T> that)
```
    Makes this BDD the logical xor of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
    
    Parameters:
    
    that - the BDD to xor with this BDD
  - xorWith
```
void xorWith(T that)
```
    Makes this BDD the logical xor of this and that variable.
    
    Parameters:
    
    that - the variable to or with this BDD
  - imp
```
BDD<T> imp(BDD<T> that)
```
    Returns the logical implication of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
    
    Parameters:
    
    that - the BDD to implicate with this BDD
    
    Returns:
    
    the logical implication of the two BDDs
  - impWith
```
void impWith(BDD<T> that)
```
    Returns the logical implication of two BDDs. Note: That BDD is consumed(!) within this operation and invalid afterwards.
    
    Parameters:
    
    that - the BDD to implicate with this BDD
  - impWith
```
void impWith(T that)
```
    Makes this BDD the logical implication of this and that variable.
    
    Parameters:
    
    that - the variable to implicate with this BDD
  - copy
```
BDD<T> copy()
```
    Returns a copy of this BDD.
    
    Returns:
    
    a copy of this object
  - getVariables
```
java.util.Set<T> getVariables()
```
    Returns the set of variables that are used in this BDD.
    
    Returns:
    
    the set of variables that are used in this bdd
  - free
```
void free()
```
    Destroys this BDD.

Interface BDD<T>

Method Summary

Method Detail

allsat

and

andWith

andWith

andWith

equals

exist

forAll

sat

high

getProvider

isOne

isZero

ite

level

low

not

nodeCount

or

orWith

orWith

orWith

replace

replaceWith

restrict

restrictWith

var

xor

xorWith

xorWith

imp

impWith

impWith

copy

getVariables

free