Class JBDD<T>

  • Type Parameters:
    T - the type of the variables
    All Implemented Interfaces:
    BDD<T>

    public class JBDD<T>
    extends java.lang.Object
    implements BDD<T>
    The JBDD is a BDD based on the JavaBDD standard java implementation.
    • Field Summary

      Fields 
      Modifier and Type Field Description
      protected net.sf.javabdd.BDD bdd  
      protected JBDDProvider<T> provider  
    • Method Summary

      All Methods Instance Methods Concrete 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.
      int hashCode()  
      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.
      java.lang.String toString()  
      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.
      • Methods inherited from class java.lang.Object

        clone, finalize, getClass, notify, notifyAll, wait, wait, wait
    • Field Detail

      • bdd

        protected net.sf.javabdd.BDD bdd
    • Method Detail

      • allsat

        public java.util.Iterator<BDD<T>> allsat()
        Description copied from interface: BDD
        Returns a BDD Iterator containing all satisfying variable assignments.
        Specified by:
        allsat in interface BDD<T>
        Returns:
        all satisfying variable assignments
      • and

        public BDD<T> and​(BDD<T> that)
        Description copied from interface: BDD
        Returns the logical and of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
        Specified by:
        and in interface BDD<T>
        Parameters:
        that - the BDD to and with this BDD
        Returns:
        the logical and of the two BDDs
      • andWith

        public void andWith​(BDD<T> that)
        Description copied from interface: BDD
        Makes this BDD the logical and of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
        Specified by:
        andWith in interface BDD<T>
        Parameters:
        that - the BDD to and with this BDD
      • equals

        public boolean equals​(java.lang.Object that)
        Description copied from interface: BDD
        TODO Returns true if this BDD equals that BDD.
        Specified by:
        equals in interface BDD<T>
        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

        public BDD<T> exist​(T variable)
        Description copied from interface: BDD
        Returns this BDD after an existential quantification of the specified variable.
        Specified by:
        exist in interface BDD<T>
        Parameters:
        variable - the variable for the existential quantification
        Returns:
        this BDD after an existential quantification of the specified variables
      • forAll

        public BDD<T> forAll​(T variable)
        Description copied from interface: BDD
        Returns this BDD after a universal quantification of the specified variable.
        Specified by:
        forAll in interface BDD<T>
        Parameters:
        variable - the variable for the universal quantification
        Returns:
        this BDD after a universal quantification of the specified variables
      • high

        public BDD<T> high()
        Description copied from interface: BDD
        Returns the true or 1 branch of this BDD.
        Specified by:
        high in interface BDD<T>
        Returns:
        the true or 1 branch of this BDD
      • isOne

        public boolean isOne()
        Description copied from interface: BDD
        Returns true if this BDD is the one BDD.
        Specified by:
        isOne in interface BDD<T>
        Returns:
        true if this BDD is the one BDD
      • isZero

        public boolean isZero()
        Description copied from interface: BDD
        Returns true if this BDD is the zero BDD.
        Specified by:
        isZero in interface BDD<T>
        Returns:
        true if this BDD is the zero BDD
      • ite

        public BDD<T> ite​(BDD<T> thenBDD,
                          BDD<T> elseBDD)
        Description copied from interface: BDD
        Returns the if-then-else} BDD with this BDD being the if, the thenBDD being the then and elseBDD being the else statement.
        Specified by:
        ite in interface BDD<T>
        Parameters:
        thenBDD - the BDD for the then statement
        elseBDD - the BDD for the else statement
        Returns:
        the if-then-else BDD
      • level

        public int level()
        Description copied from interface: BDD
        Returns the level of this BDD.
        Specified by:
        level in interface BDD<T>
        Returns:
        the level of this BDD
      • low

        public BDD<T> low()
        Description copied from interface: BDD
        Returns the false or 0 branch of this BDD.
        Specified by:
        low in interface BDD<T>
        Returns:
        the false or 0 branch of this BDD
      • not

        public BDD<T> not()
        Description copied from interface: BDD
        Returns a BDD that is the negation of this BDD.
        Specified by:
        not in interface BDD<T>
        Returns:
        a BDD that is the negation of this BDD
      • nodeCount

        public int nodeCount()
        Description copied from interface: BDD
        Returns the number of node in this BDD.
        Specified by:
        nodeCount in interface BDD<T>
        Returns:
        the number of nodes in this bdd
      • or

        public BDD<T> or​(BDD<T> that)
        Description copied from interface: BDD
        Returns the logical or of two BDDs. Note: Both BDDs remain unchanged after this or-operation.
        Specified by:
        or in interface BDD<T>
        Parameters:
        that - the BDD to or with this BDD
        Returns:
        the logical or of the two BDDs
      • orWith

        public void orWith​(BDD<T> that)
        Description copied from interface: BDD
        Makes this BDD the logical or of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
        Specified by:
        orWith in interface BDD<T>
        Parameters:
        that - the BDD to or with this BDD
      • replace

        public BDD<T> replace​(T variable1,
                              T variable2)
        Description copied from interface: BDD
        Returns a BDD where the variable for variable1 is replaced with the variable of variable2.
        Specified by:
        replace in interface BDD<T>
        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

        public void replaceWith​(T variable1,
                                T variable2)
        Description copied from interface: BDD
        Replaces the variable for variable1 with the variable of variable2 in this BDD.
        Specified by:
        replaceWith in interface BDD<T>
        Parameters:
        variable1 - the first variable
        variable2 - the second variable
      • restrict

        public BDD<T> restrict​(BDD<T> that)
        Description copied from interface: BDD
        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.
        Specified by:
        restrict in interface BDD<T>
        Parameters:
        that - the BDD to restrict this BDD with
        Returns:
        a new BDD representing this BDD restricted with that BDD
      • restrictWith

        public void restrictWith​(BDD<T> that)
        Description copied from interface: BDD
        Restricts the variables of that to constant reliabilityFunctions in this BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
        Specified by:
        restrictWith in interface BDD<T>
        Parameters:
        that - the BDD to restrict this BDD with
      • sat

        public BDD<T> sat()
        Description copied from interface: BDD
        Returns one satisfying variable assignment as a BDD.
        Specified by:
        sat in interface BDD<T>
        Returns:
        one satisfying variable assignment as a BDD
      • var

        public T var()
        Description copied from interface: BDD
        Returns the variable labeling the BDD.
        Specified by:
        var in interface BDD<T>
        Returns:
        the variable labeling the BDD
      • xor

        public BDD<T> xor​(BDD<T> that)
        Description copied from interface: BDD
        Returns the logical xor of two BDDs. Note: Both BDDs remain unchanged after this xor-operation.
        Specified by:
        xor in interface BDD<T>
        Parameters:
        that - the BDD to xor with this BDD
        Returns:
        the logical xor of the two BDDs
      • xorWith

        public void xorWith​(BDD<T> that)
        Description copied from interface: BDD
        Makes this BDD the logical xor of this and that BDD. Note: That BDD is consumed(!) within this operation and invalid afterwards.
        Specified by:
        xorWith in interface BDD<T>
        Parameters:
        that - the BDD to xor with this BDD
      • imp

        public BDD<T> imp​(BDD<T> that)
        Description copied from interface: BDD
        Returns the logical implication of two BDDs. Note: Both BDDs remain unchanged after this and-operation.
        Specified by:
        imp in interface BDD<T>
        Parameters:
        that - the BDD to implicate with this BDD
        Returns:
        the logical implication of the two BDDs
      • impWith

        public void impWith​(BDD<T> that)
        Description copied from interface: BDD
        Returns the logical implication of two BDDs. Note: That BDD is consumed(!) within this operation and invalid afterwards.
        Specified by:
        impWith in interface BDD<T>
        Parameters:
        that - the BDD to implicate with this BDD
      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object
      • hashCode

        public int hashCode()
        Overrides:
        hashCode in class java.lang.Object
      • andWith

        public void andWith​(java.util.Collection<T> that)
        Description copied from interface: BDD
        Makes this BDD the logical and of this and that variables.
        Specified by:
        andWith in interface BDD<T>
        Parameters:
        that - the variables to and with this BDD
      • andWith

        public void andWith​(T that)
        Description copied from interface: BDD
        Makes this BDD the logical and of this and that variable.
        Specified by:
        andWith in interface BDD<T>
        Parameters:
        that - the variable to and with this BDD
      • orWith

        public void orWith​(java.util.Collection<T> that)
        Description copied from interface: BDD
        Makes this BDD the logical or of this and that variables.
        Specified by:
        orWith in interface BDD<T>
        Parameters:
        that - the variables to or with this BDD
      • orWith

        public void orWith​(T that)
        Description copied from interface: BDD
        Makes this BDD the logical or of this and that variable.
        Specified by:
        orWith in interface BDD<T>
        Parameters:
        that - the variable to or with this BDD
      • impWith

        public void impWith​(T that)
        Description copied from interface: BDD
        Makes this BDD the logical implication of this and that variable.
        Specified by:
        impWith in interface BDD<T>
        Parameters:
        that - the variable to implicate with this BDD
      • xorWith

        public void xorWith​(T that)
        Description copied from interface: BDD
        Makes this BDD the logical xor of this and that variable.
        Specified by:
        xorWith in interface BDD<T>
        Parameters:
        that - the variable to or with this BDD
      • copy

        public BDD<T> copy()
        Description copied from interface: BDD
        Returns a copy of this BDD.
        Specified by:
        copy in interface BDD<T>
        Returns:
        a copy of this object
      • getVariables

        public java.util.Set<T> getVariables()
        Description copied from interface: BDD
        Returns the set of variables that are used in this BDD.
        Specified by:
        getVariables in interface BDD<T>
        Returns:
        the set of variables that are used in this bdd
      • free

        public void free()
        Description copied from interface: BDD
        Destroys this BDD.
        Specified by:
        free in interface BDD<T>