Uses of Class
com.github.javabdd.BDD

Uses of BDD in com.github.javabdd

Subclasses of BDD in com.github.javabdd

Modifier and Type	Class	Description
class	BDDFactoryIntImpl.IntBDD
class	BDDFactoryIntImpl.IntBDDWithFinalizer

Fields in com.github.javabdd declared as BDD

Modifier and Type	Field	Description
protected BDD	BDDVarSet.DefaultImpl.b	BDD representation of the set of variables.
protected BDD[]	BDDBitVector.bitvec

Fields in com.github.javabdd with type parameters of type BDD

Modifier and Type	Field	Description
protected LinkedList<BDD>	BDD.AllSatIterator.hiStack
protected LinkedList<BDD>	BDD.AllSatIterator.loStack

Methods in com.github.javabdd that return BDD

Modifier and Type	Method	Description
BDD	BDD.and(BDD that)	Returns the logical 'and' of two BDDs.
BDD	BDD.andWith(BDD that)	Makes this BDD be the logical 'and' of two BDDs.
abstract BDD	BDD.apply(BDD that, BDDFactory.BDDOp opr)	Returns the result of applying the binary operator opr to the two BDDs.
BDD	BDDFactoryIntImpl.IntBDD.apply(BDD that, BDDFactory.BDDOp opr)
abstract BDD	BDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs a universal quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs an existential quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs a unique quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyWith(BDD that, BDDFactory.BDDOp opr)	Makes this BDD be the result of the binary operator opr of two BDDs.
BDD	BDDFactoryIntImpl.IntBDD.applyWith(BDD that, BDDFactory.BDDOp opr)
BDD	BDD.biimp(BDD that)	Returns the logical 'bi-implication' of two BDDs.
BDD	BDD.biimpWith(BDD that)	Makes this BDD be the logical 'bi-implication' of two BDDs.
BDD	BDDDomain.buildAdd(BDDDomain that, int bits, long value)
BDD	BDDDomain.buildAdd(BDDDomain that, long value)
BDD	BDDFactory.buildCube(int value, int[] variables)	Build a cube from an array of variables.
BDD	BDDFactory.buildCube(int value, List<BDD> variables)	Build a cube from an array of variables.
BDD	BDDDomain.buildEquals(BDDDomain that)	Builds a BDD which is true for all the possible assignments to the variable blocks that makes the blocks equal.
abstract BDD	BDD.compose(BDD g, int var)	Functional composition.
BDD	BDDFactoryIntImpl.IntBDD.compose(BDD g, int var)
abstract BDD	BDD.constrain(BDD that)	Generalized cofactor.
BDD	BDDFactoryIntImpl.IntBDD.constrain(BDD that)
BDD	JFactory.copyNode(BDD that)	Use this function to translate BDD's from a JavaFactory into its clone.
BDD	BDDDomain.domain()	Returns what corresponds to a disjunction of all possible values of this domain.
abstract BDD	BDD.exist(BDDVarSet var)	Existential quantification of variables.
BDD	BDDFactoryIntImpl.IntBDD.exist(BDDVarSet var)
abstract BDD	BDD.forAll(BDDVarSet var)	Universal quantification of variables.
BDD	BDDFactoryIntImpl.IntBDD.forAll(BDDVarSet var)
abstract BDD	BDD.fullSatOne()	Finds one satisfying variable assignment.
BDD	BDDFactoryIntImpl.IntBDD.fullSatOne()
BDD	BDDBitVector.getBit(int n)
abstract BDD	BDD.high()	Gets the true branch of this BDD.
BDD	BDDFactoryIntImpl.IntBDD.high()
abstract BDD	BDD.id()	Identity function.
BDD	BDDFactoryIntImpl.IntBDD.id()
BDD	BDD.imp(BDD that)	Returns the logical 'implication' of two BDDs.
BDD	BDD.impWith(BDD that)	Makes this BDD be the logical 'implication' of two BDDs.
abstract BDD	BDD.ite(BDD thenBDD, BDD elseBDD)	if-then-else operator.
BDD	BDDFactoryIntImpl.IntBDD.ite(BDD thenBDD, BDD elseBDD)
BDD	BDDDomain.ithVar(long val)	Returns the BDD that defines the given value for this finite domain block.
BDD	BDDDomain.ithVar(BigInteger val)
abstract BDD	BDDFactory.ithVar(int var)	Returns a BDD representing the I'th variable.
BDD	BDDFactoryIntImpl.ithVar(int var)
BDD	BDDFactory.load(BufferedReader ifile)	Loads a BDD from the given input.
BDD	BDDFactory.load(BufferedReader ifile, int[] translate)	Loads a BDD from the given input, translating BDD variables according to the given map.
BDD	BDDFactory.load(String filename)	Loads a BDD from a file.
BDD	JFactory.load(BufferedReader in, int[] translate)
protected BDD	BDDFactory.loadhash_get(BDDFactory.LoadHash[] lh_table, int lh_nodenum, int key)	Gets a BDD from the load hash table.
abstract BDD	BDD.low()	Gets the false branch of this BDD.
BDD	BDDFactoryIntImpl.IntBDD.low()
BDD	BDD.BDDIterator.next()
BDD	BDD.BDDIterator.nextBDD()	Return the next BDD in the iteration.
abstract BDD	BDDFactory.nithVar(int var)	Returns a BDD representing the negation of the I'th variable.
BDD	BDDFactoryIntImpl.nithVar(int var)
abstract BDD	BDD.not()	Negates this BDD by exchanging all references to the zero-terminal with references to the one-terminal and vice-versa.
BDD	BDDFactoryIntImpl.IntBDD.not()
abstract BDD	BDDFactory.one()	Get the constant true BDD.
BDD	BDDFactoryIntImpl.one()
BDD	BDD.or(BDD that)	Returns the logical 'or' of two BDDs.
BDD	BDD.orWith(BDD that)	Makes this BDD be the logical 'or' of two BDDs.
abstract BDD	BDD.relnext(BDD states, BDDVarSet vars)	Computes the BDD that represents the set of successor states from states, i.e., the ones reachable by taking one forward step from states in states, where this BDD is the (partial) transition relation to consider.
BDD	BDDFactoryIntImpl.IntBDD.relnext(BDD states, BDDVarSet vars)
abstract BDD	BDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars)	Computes and(relnext(states, vars), restriction) as a single BDD operation.
BDD	BDDFactoryIntImpl.IntBDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars)
abstract BDD	BDD.relprev(BDD states, BDDVarSet vars)	Computes the BDD that represents the set of predecessor states from states, i.e., the ones reachable by taking one backward step from states in states, where this BDD is the (partial) transition relation to consider.
BDD	BDDFactoryIntImpl.IntBDD.relprev(BDD states, BDDVarSet vars)
abstract BDD	BDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars)	Computes and(relprev(states, vars), restriction) as a single BDD operation.
BDD	BDDFactoryIntImpl.IntBDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars)
BDD	BDD.relprod(BDD that, BDDVarSet var)	Relational product.
abstract BDD	BDD.replace(BDDPairing pair)	Returns a BDD where all variables are replaced with the variables defined by pair.
BDD	BDDFactoryIntImpl.IntBDD.replace(BDDPairing pair)
abstract BDD	BDD.replaceWith(BDDPairing pair)	Replaces all variables in this BDD with the variables defined by pair.
BDD	BDDFactoryIntImpl.IntBDD.replaceWith(BDDPairing pair)
abstract BDD	BDD.restrict(BDD var)	Restrict a set of variables to constant values.
BDD	BDDFactoryIntImpl.IntBDD.restrict(BDD var)
abstract BDD	BDD.restrictWith(BDD var)	Mutates this BDD to restrict a set of variables to constant values.
BDD	BDDFactoryIntImpl.IntBDD.restrictWith(BDD that)
abstract BDD	BDD.satOne()	Finds one satisfying variable assignment.
abstract BDD	BDD.satOne(BDDVarSet var, boolean pol)	Finds one satisfying variable assignment.
BDD	BDDFactoryIntImpl.IntBDD.satOne()
BDD	BDDFactoryIntImpl.IntBDD.satOne(BDDVarSet var, boolean pol)
abstract BDD	BDD.simplify(BDD d)	Coudert and Madre's restrict function.
BDD	BDDFactoryIntImpl.IntBDD.simplify(BDD d)
BDD	BDDFactoryIntImpl.IntBDDVarSet.toBDD()
BDD	BDDVarSet.DefaultImpl.toBDD()
abstract BDD	BDDVarSet.toBDD()
abstract BDD	BDD.unique(BDDVarSet var)	Unique quantification of variables.
BDD	BDDFactoryIntImpl.IntBDD.unique(BDDVarSet var)
BDD	BDDFactory.universe()	Get the constant universe BDD.
BDD	BDDFactoryIntImpl.universe()
BDD	BDDDomain.varRange(long lo, long hi)	Returns the BDD that defines the given range of values, inclusive, for this finite domain block.
BDD	BDDDomain.varRange(BigInteger lo, BigInteger hi)
abstract BDD	BDD.veccompose(BDDPairing pair)	Simultaneous functional composition.
BDD	BDDFactoryIntImpl.IntBDD.veccompose(BDDPairing pair)
BDD	BDD.xor(BDD that)	Returns the logical 'xor' of two BDDs.
BDD	BDD.xorWith(BDD that)	Makes this BDD be the logical 'xor' of two BDDs.
abstract BDD	BDDFactory.zero()	Get the constant false BDD.
BDD	BDDFactoryIntImpl.zero()

Methods in com.github.javabdd with parameters of type BDD

Modifier and Type	Method	Description
BDD	BDD.and(BDD that)	Returns the logical 'and' of two BDDs.
BDD	BDD.andWith(BDD that)	Makes this BDD be the logical 'and' of two BDDs.
abstract BDD	BDD.apply(BDD that, BDDFactory.BDDOp opr)	Returns the result of applying the binary operator opr to the two BDDs.
BDD	BDDFactoryIntImpl.IntBDD.apply(BDD that, BDDFactory.BDDOp opr)
abstract BDD	BDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs a universal quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs an existential quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)	Applies the binary operator opr to two BDDs and then performs a unique quantification of the variables from the variable set var.
BDD	BDDFactoryIntImpl.IntBDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var)
abstract BDD	BDD.applyWith(BDD that, BDDFactory.BDDOp opr)	Makes this BDD be the result of the binary operator opr of two BDDs.
BDD	BDDFactoryIntImpl.IntBDD.applyWith(BDD that, BDDFactory.BDDOp opr)
BDD	BDD.biimp(BDD that)	Returns the logical 'bi-implication' of two BDDs.
BDD	BDD.biimpWith(BDD that)	Makes this BDD be the logical 'bi-implication' of two BDDs.
abstract BDD	BDD.compose(BDD g, int var)	Functional composition.
BDD	BDDFactoryIntImpl.IntBDD.compose(BDD g, int var)
abstract BDD	BDD.constrain(BDD that)	Generalized cofactor.
BDD	BDDFactoryIntImpl.IntBDD.constrain(BDD that)
BDD	JFactory.copyNode(BDD that)	Use this function to translate BDD's from a JavaFactory into its clone.
abstract boolean	BDD.equalsBDD(BDD that)	Returns true if this BDD equals that BDD, false otherwise.
boolean	BDDFactoryIntImpl.IntBDD.equalsBDD(BDD that)
BigInteger[]	BDDDomain.getVarIndices(BDD that)	Convert a BDD that to a list of indices of this domain.
BigInteger[]	BDDDomain.getVarIndices(BDD that, int max)	Convert a BDD that to a list of indices of this domain.
BDD	BDD.imp(BDD that)	Returns the logical 'implication' of two BDDs.
BDD	BDD.impWith(BDD that)	Makes this BDD be the logical 'implication' of two BDDs.
void	FindBestOrder.init(BDD b1, BDD b2, BDDVarSet dom, BDDFactory.BDDOp op)
void	TryVarOrder.init(BDD b1, BDD b2, BDD dom, BDDFactory.BDDOp op)	Initialize for a new trial.
abstract BDD	BDD.ite(BDD thenBDD, BDD elseBDD)	if-then-else operator.
BDD	BDDFactoryIntImpl.IntBDD.ite(BDD thenBDD, BDD elseBDD)
BDDPairing	BDDFactory.makePair(int oldvar, BDD newvar)	Make a new pairing that maps from one variable to another BDD.
BDD	BDD.or(BDD that)	Returns the logical 'or' of two BDDs.
BDD	BDD.orWith(BDD that)	Makes this BDD be the logical 'or' of two BDDs.
abstract void	BDDFactory.printTable(BDD b)	Prints the node table entries used by a BDD.
void	BDDFactoryIntImpl.printTable(BDD b)
abstract BDD	BDD.relnext(BDD states, BDDVarSet vars)	Computes the BDD that represents the set of successor states from states, i.e., the ones reachable by taking one forward step from states in states, where this BDD is the (partial) transition relation to consider.
BDD	BDDFactoryIntImpl.IntBDD.relnext(BDD states, BDDVarSet vars)
abstract BDD	BDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars)	Computes and(relnext(states, vars), restriction) as a single BDD operation.
BDD	BDDFactoryIntImpl.IntBDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars)
abstract BDD	BDD.relprev(BDD states, BDDVarSet vars)	Computes the BDD that represents the set of predecessor states from states, i.e., the ones reachable by taking one backward step from states in states, where this BDD is the (partial) transition relation to consider.
BDD	BDDFactoryIntImpl.IntBDD.relprev(BDD states, BDDVarSet vars)
abstract BDD	BDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars)	Computes and(relprev(states, vars), restriction) as a single BDD operation.
BDD	BDDFactoryIntImpl.IntBDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars)
BDD	BDD.relprod(BDD that, BDDVarSet var)	Relational product.
abstract BDD	BDD.restrict(BDD var)	Restrict a set of variables to constant values.
BDD	BDDFactoryIntImpl.IntBDD.restrict(BDD var)
abstract BDD	BDD.restrictWith(BDD var)	Mutates this BDD to restrict a set of variables to constant values.
BDD	BDDFactoryIntImpl.IntBDD.restrictWith(BDD that)
void	BDDFactory.save(BufferedWriter out, BDD r)	Saves a BDD to an output writer.
void	BDDFactory.save(String filename, BDD var)	Saves a BDD to a file.
void	JFactory.save(BufferedWriter out, BDD b)
protected int	BDDFactory.save_rec(BufferedWriter out, BitSet visited, BDD root)	Helper function for save().
void	BDDPairing.set(int[] oldvar, BDD[] newvar)	Like set(), but with a whole list of pairs.
abstract void	BDDPairing.set(int oldvar, BDD newvar)	Adds the pair (oldvar, newvar) to this table of pairs.
BDDBitVector	BDDBitVector.shl(int pos, BDD c)
abstract BDD	BDD.simplify(BDD d)	Coudert and Madre's restrict function.
BDD	BDDFactoryIntImpl.IntBDD.simplify(BDD d)
protected static final int	BDDFactoryIntImpl.unwrap(BDD b)
void	JFactory.validateBDD(BDD b)
BDD	BDD.xor(BDD that)	Returns the logical 'xor' of two BDDs.
BDD	BDD.xorWith(BDD that)	Makes this BDD be the logical 'xor' of two BDDs.

Method parameters in com.github.javabdd with type arguments of type BDD

Modifier and Type	Method	Description
BDD	BDDFactory.buildCube(int value, List<BDD> variables)	Build a cube from an array of variables.
abstract int	BDDFactory.nodeCount(Collection<BDD> r)	Counts the number of shared nodes in a collection of BDDs.
int	BDDFactoryIntImpl.nodeCount(Collection<BDD> r)
protected int	BDD.printdot_rec(PrintStream out, int current, boolean[] visited, HashMap<BDD,Integer> map)
protected static final int[]	BDDFactoryIntImpl.unwrap(Collection<BDD> c)

Constructors in com.github.javabdd with parameters of type BDD

Modifier	Constructor	Description
	AllSatIterator(BDD r)	Constructs a satisfying-assignment iterator on the given BDD.
	AllSatIterator(BDD r, boolean lev)	Constructs a satisfying-assignment iterator on the given BDD.
	BDDIterator(BDD bdd, BDDVarSet var)	Construct a new BDDIterator on the given BDD.
	DefaultImpl(BDD b)	Construct a BDDVarSet backed by the given BDD.