Uses of Class
com.github.javabdd.BDDVarSet
-
Uses of BDDVarSet in com.github.javabdd
Subclasses of BDDVarSet in com.github.javabddModifier and TypeClassDescriptionclassclassclassclassstatic classDefault implementation of BDDVarSet based on BDDs.Fields in com.github.javabdd declared as BDDVarSetMethods in com.github.javabdd that return BDDVarSetModifier and TypeMethodDescriptionBDDFactory.emptySet()Get an empty BDDVarSet.BDDFactoryIntImpl.emptySet()BDDFactoryIntImpl.IntBDDVarSet.id()BDDVarSet.DefaultImpl.id()abstract BDDVarSetBDDVarSet.id()abstract BDDVarSetReturns a new BDDVarSet that is the union of the current BDDVarSet and the given BDDVarSet.BDDFactoryIntImpl.IntBDDVarSet.intersectWith(BDDVarSet b) BDDVarSet.DefaultImpl.intersectWith(BDDVarSet s) abstract BDDVarSetBDDVarSet.intersectWith(BDDVarSet b) Modifies this BDDVarSet to include all of the vars in the given set.BDDFactory.makeSet(int[] varset) Builds a BDD variable set from an integer array.Returns a BDD defining all the variable sets used to define the variable blocks in the given array.BDDDomain.set()Returns the variable set that contains the variables used to define this finite domain block.abstract BDDVarSetBDD.support()Returns the variable support of this BDD.BDDFactoryIntImpl.IntBDD.support()BDD.toVarSet()Converts this BDD to a new BDDVarSet.BDDFactoryIntImpl.IntBDD.toVarSet()BDDFactoryIntImpl.IntBDDVarSet.union(int var) BDDVarSet.DefaultImpl.union(int var) abstract BDDVarSetBDDVarSet.union(int var) Returns a new BDDVarSet that is the union of the current BDDVarSet and the given variable.abstract BDDVarSetReturns a new BDDVarSet that is the union of the current BDDVarSet and the given BDDVarSet.BDDFactoryIntImpl.IntBDDVarSet.unionWith(int var) BDDVarSet.DefaultImpl.unionWith(int var) abstract BDDVarSetBDDVarSet.unionWith(int var) Modifies this BDDVarSet to include the given variable.abstract BDDVarSetModifies this BDDVarSet to include all of the vars in the given set.Methods in com.github.javabdd with parameters of type BDDVarSetModifier and TypeMethodDescriptionvoidBDDFactory.addVarBlock(BDDVarSet var, boolean fixed) Adds a new variable block for reordering.abstract BDDBDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) Applies the binary operatoroprto two BDDs and then performs a universal quantification of the variables from the variable setvar.BDDFactoryIntImpl.IntBDD.applyAll(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) abstract BDDBDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) Applies the binary operatoroprto two BDDs and then performs an existential quantification of the variables from the variable setvar.BDDFactoryIntImpl.IntBDD.applyEx(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) abstract BDDBDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) Applies the binary operatoroprto two BDDs and then performs a unique quantification of the variables from the variable setvar.BDDFactoryIntImpl.IntBDD.applyUni(BDD that, BDDFactory.BDDOp opr, BDDVarSet var) booleanBDDFactoryIntImpl.IntBDDVarSet.equalsBDDVarSet(BDDVarSet that) booleanBDDVarSet.DefaultImpl.equalsBDDVarSet(BDDVarSet s) abstract booleanBDDVarSet.equalsBDDVarSet(BDDVarSet that) Returns true if the sets are equal.abstract BDDExistential quantification of variables.abstract BDDUniversal quantification of variables.voidFindBestOrder.init(BDD b1, BDD b2, BDDVarSet dom, BDDFactory.BDDOp op) abstract BDDVarSetReturns a new BDDVarSet that is the union of the current BDDVarSet and the given BDDVarSet.BDDFactoryIntImpl.IntBDDVarSet.intersectWith(BDDVarSet b) BDDVarSet.DefaultImpl.intersectWith(BDDVarSet s) abstract BDDVarSetBDDVarSet.intersectWith(BDDVarSet b) Modifies this BDDVarSet to include all of the vars in the given set.Returns an iteration of the satisfying assignments of this BDD.doubleBDD.logSatCount(BDDVarSet varset) Calculates the logarithm of the number of satisfying variable assignments to the variables in the given varset.abstract BDDComputes the BDD that represents the set of successor states fromstates, i.e., the ones reachable by taking one forward step from states instates, where this BDD is the (partial) transition relation to consider.abstract BDDBDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars) Computesand(relnext(states, vars), restriction)as a single BDD operation.BDDFactoryIntImpl.IntBDD.relnextIntersection(BDD states, BDD restriction, BDDVarSet vars) abstract BDDBDD.relnextUnion(BDD states, BDD union, BDDVarSet vars) Computesor(relnext(states, vars), union)as a single BDD operation.BDD.relnextUnion(BDD states, BDDVarSet vars) Computesor(relnext(states, vars), states)as a single BDD operation.BDDFactoryIntImpl.IntBDD.relnextUnion(BDD states, BDD union, BDDVarSet vars) abstract BDDComputes the BDD that represents the set of predecessor states fromstates, i.e., the ones reachable by taking one backward step from states instates, where this BDD is the (partial) transition relation to consider.abstract BDDBDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars) Computesand(relprev(states, vars), restriction)as a single BDD operation.BDDFactoryIntImpl.IntBDD.relprevIntersection(BDD states, BDD restriction, BDDVarSet vars) abstract BDDBDD.relprevUnion(BDD states, BDD union, BDDVarSet vars) Computesor(relprev(states, vars), union)as a single BDD operation.BDD.relprevUnion(BDD states, BDDVarSet vars) Computesor(relprev(states, vars), states)as a single BDD operation.BDDFactoryIntImpl.IntBDD.relprevUnion(BDD states, BDD union, BDDVarSet vars) Relational product.Calculates the number of satisfying variable assignments to the variables in the given varset.abstract BDDFinds one satisfying variable assignment.abstract BDDVarSetReturns a new BDDVarSet that is the union of the current BDDVarSet and the given BDDVarSet.abstract BDDVarSetModifies this BDDVarSet to include all of the vars in the given set.abstract BDDUnique quantification of variables.protected static final intConstructors in com.github.javabdd with parameters of type BDDVarSetModifierConstructorDescriptionBDDIterator(BDD bdd, BDDVarSet var) Construct a new BDDIterator on the given BDD.