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

      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 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​(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 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 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
      • 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.