Package org.jreliability.bdd

Interface BDD<T>

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

    Modifier and Type
    Method
    Description
    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(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(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.
    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 BDDs.
    void
    impWith(BDD<T> that)
    Returns the logical implication of two BDDs.
    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 BDDs.
    void
    orWith(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 BDDs.
    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 Details

    • allsat

      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(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(Object that)
      TODO Returns true if this BDD equals that BDD.
      Overrides:
      equals in class 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(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

      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.