Package com.github.javabdd

Class BDD.BDDIterator

  • All Implemented Interfaces:
    Iterator<BDD>
    Enclosing class:
    BDD
    public static class BDD.BDDIterator
extends Object
implements Iterator<BDD>
    BDDIterator is used to iterate through the satisfying assignments of a BDD. It includes the ability to check if bits are dont-cares and skip them.

    • Constructor Detail

      • BDDIterator

        public BDDIterator​(BDD bdd,
                   BDDVarSet var)
        Construct a new BDDIterator on the given BDD. The var argument is the set of variables that will be mentioned in the result.
        Parameters:
        bdd - BDD to iterate over
        var - variable set to mention in result

    • Method Detail

      • gotoNext

        protected void gotoNext()

      • gotoNextA

        protected boolean gotoNextA()

      • nextTuple

        public BigInteger[] nextTuple()
        Return the next tuple of domain values in the iteration.
        Returns:
        the next tuple of domain values in the iteration.

      • nextTuple2

        public BigInteger[] nextTuple2()
        An alternate implementation of nextTuple(). This may be slightly faster than the default if there are many domains.
        Returns:
        the next tuple of domain values in the iteration.

      • nextSat

        public boolean[] nextSat()
        Return the next single satisfying assignment in the iteration.
        Returns:
        the next single satisfying assignment in the iteration.

      • nextBDD

        public BDD nextBDD()
        Return the next BDD in the iteration.
        Returns:
        the next BDD in the iteration

      • isDontCare

        public boolean isDontCare​(int var)
        Returns true if the given BDD variable number is a dont-care. var must be a variable in the iteration set.
        Parameters:
        var - variable number to check
        Returns:
        if the given variable is a dont-care

      • isDontCare

        public boolean isDontCare​(BDDDomain d)
        Returns true if the BDD variables in the given BDD domain are all dont-care's.
        Parameters:
        d - domain to check
        Returns:
        if the variables are all dont-cares
        Throws:
        BDDException - if d is not in the iteration set

      • fastForward

        public void fastForward​(int var)
        Fast-forward the iteration such that the given variable number is true.
        Parameters:
        var - number of variable

      • fastForward

        public void fastForward​(int[] vars)
        Fast-forward the iteration such that the given set of variables are true.
        Parameters:
        vars - set of variable indices

      • skipDontCare

        public void skipDontCare​(BDDDomain d)
        Assuming d is a dont-care, skip to the end of the iteration for d.
        Parameters:
        d - BDD domain to fast-forward past