| Modifier and Type | Class and Description |
|---|---|
class |
BDDFactoryIntImpl.IntBDD |
class |
BDDFactoryIntImpl.IntBDDWithFinalizer |
class |
TypedBDDFactory.TypedBDD
A BDD with types (domains) attached to it.
|
| Modifier and Type | Field and Description |
|---|---|
protected BDD |
BDDVarSet.DefaultImpl.b
BDD representation of the set of variables.
|
protected BDD[] |
BDDBitVector.bitvec |
| Modifier and Type | Method and 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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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 |
TypedBDDFactory.TypedBDD.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 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) |
BDD |
TypedBDDFactory.TypedBDD.compose(BDD g,
int var) |
abstract BDD |
BDD.constrain(BDD that)
Generalized cofactor.
|
BDD |
BDDFactoryIntImpl.IntBDD.constrain(BDD that) |
BDD |
TypedBDDFactory.TypedBDD.constrain(BDD that) |
BDD |
JFactory.copyNode(BDD that)
Use this function to translate BDD's from a JavaFactory into its clone.
|
BDD |
MicroFactory.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) |
BDD |
TypedBDDFactory.TypedBDD.exist(BDDVarSet var) |
abstract BDD |
BDD.forAll(BDDVarSet var)
Universal quantification of variables.
|
BDD |
BDDFactoryIntImpl.IntBDD.forAll(BDDVarSet var) |
BDD |
TypedBDDFactory.TypedBDD.forAll(BDDVarSet var) |
abstract BDD |
BDD.fullSatOne()
Finds one satisfying variable assignment.
|
BDD |
BDDFactoryIntImpl.IntBDD.fullSatOne() |
BDD |
TypedBDDFactory.TypedBDD.fullSatOne() |
BDD |
BDDBitVector.getBit(int n) |
abstract BDD |
BDD.high()
Gets the true branch of this BDD.
|
BDD |
BDDFactoryIntImpl.IntBDD.high() |
BDD |
TypedBDDFactory.TypedBDD.high() |
abstract BDD |
BDD.id()
Identity function.
|
BDD |
BDDFactoryIntImpl.IntBDD.id() |
BDD |
TypedBDDFactory.TypedBDD.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 |
TypedBDDFactory.TypedBDD.ite(BDD thenBDD,
BDD elseBDD) |
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 |
TestBDDFactory.ithVar(int var) |
BDD |
TypedBDDFactory.ithVar(int var) |
BDD |
BDDDomain.ithVar(long val)
Returns the BDD that defines the given value for this finite domain
block.
|
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 |
JFactory.load(BufferedReader in,
int[] translate) |
BDD |
MicroFactory.load(BufferedReader in,
int[] translate) |
BDD |
UberMicroFactory.load(BufferedReader in,
int[] translate) |
BDD |
BDDFactory.load(String filename)
Loads a BDD from a file.
|
BDD |
TestBDDFactory.load(String filename) |
BDD |
TypedBDDFactory.load(String filename) |
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 |
TypedBDDFactory.TypedBDD.low() |
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) |
BDD |
TestBDDFactory.nithVar(int var) |
BDD |
TypedBDDFactory.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() |
BDD |
TypedBDDFactory.TypedBDD.not() |
abstract BDD |
BDDFactory.one()
Get the constant true BDD.
|
BDD |
BDDFactoryIntImpl.one() |
BDD |
TestBDDFactory.one() |
BDD |
TypedBDDFactory.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.
|
BDD |
BDD.relprod(BDD that,
BDDVarSet var)
Relational product.
|
BDD |
TypedBDDFactory.TypedBDD.relprod(BDD that,
BDDVarSet var) |
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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.replaceWith(BDDPairing pair) |
abstract BDD |
BDD.restrict(BDD var)
Restrict a set of variables to constant values.
|
BDD |
BDDFactoryIntImpl.IntBDD.restrict(BDD var) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.restrictWith(BDD var) |
abstract BDD |
BDD.satOne()
Finds one satisfying variable assignment.
|
BDD |
BDDFactoryIntImpl.IntBDD.satOne() |
BDD |
TypedBDDFactory.TypedBDD.satOne() |
abstract BDD |
BDD.satOne(BDDVarSet var,
boolean pol)
Finds one satisfying variable assignment.
|
BDD |
BDDFactoryIntImpl.IntBDD.satOne(BDDVarSet var,
boolean pol) |
BDD |
TypedBDDFactory.TypedBDD.satOne(BDDVarSet var,
boolean pol) |
abstract BDD |
BDD.simplify(BDD d)
Coudert and Madre's restrict function.
|
BDD |
BDDFactoryIntImpl.IntBDD.simplify(BDD d) |
BDD |
TypedBDDFactory.TypedBDD.simplify(BDD d) |
BDD |
BDDFactoryIntImpl.IntBDDVarSet.toBDD() |
abstract BDD |
BDDVarSet.toBDD() |
BDD |
BDDVarSet.DefaultImpl.toBDD() |
BDD |
TypedBDDFactory.TypedBDDVarSet.toBDD() |
abstract BDD |
BDD.unique(BDDVarSet var)
Unique quantification of variables.
|
BDD |
BDDFactoryIntImpl.IntBDD.unique(BDDVarSet var) |
BDD |
TypedBDDFactory.TypedBDD.unique(BDDVarSet var) |
BDD |
BDDFactory.universe()
Get the constant universe BDD.
|
BDD |
BDDFactoryIntImpl.universe() |
BDD |
TestBDDFactory.universe() |
BDD |
BDDDomain.varRange(BigInteger lo,
BigInteger hi) |
BDD |
BDDDomain.varRange(long lo,
long hi)
Returns the BDD that defines the given range of values, inclusive,
for this finite domain block.
|
abstract BDD |
BDD.veccompose(BDDPairing pair)
Simultaneous functional composition.
|
BDD |
BDDFactoryIntImpl.IntBDD.veccompose(BDDPairing pair) |
BDD |
TypedBDDFactory.TypedBDD.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() |
BDD |
TestBDDFactory.zero() |
BDD |
TypedBDDFactory.zero() |
| Modifier and Type | Method and 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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.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 |
TypedBDDFactory.TypedBDD.applyWith(BDD that,
BDDFactory.BDDOp opr) |
static void |
TestBDDFactory.assertSame(BDD b1,
BDD b2,
String s) |
static void |
TestBDDFactory.assertSame(boolean b,
BDD b1,
BDD b2,
String s) |
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) |
BDD |
TypedBDDFactory.TypedBDD.compose(BDD g,
int var) |
abstract BDD |
BDD.constrain(BDD that)
Generalized cofactor.
|
BDD |
BDDFactoryIntImpl.IntBDD.constrain(BDD that) |
BDD |
TypedBDDFactory.TypedBDD.constrain(BDD that) |
BDD |
JFactory.copyNode(BDD that)
Use this function to translate BDD's from a JavaFactory into its clone.
|
BDD |
MicroFactory.copyNode(BDD that)
Use this function to translate BDD's from a JavaFactory into its clone.
|
abstract boolean |
BDD.equals(BDD that)
Returns true if this BDD equals that BDD, false otherwise.
|
boolean |
BDDFactoryIntImpl.IntBDD.equals(BDD that) |
boolean |
TypedBDDFactory.TypedBDD.equals(BDD that) |
BigInteger[] |
BDDDomain.getVarIndices(BDD bdd)
Convert a BDD that to a list of indices of this domain.
|
BigInteger[] |
BDDDomain.getVarIndices(BDD bdd,
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 |
TryVarOrder.init(BDD b1,
BDD b2,
BDD dom,
BDDFactory.BDDOp op)
Initialize for a new trial.
|
void |
FindBestOrder.init(BDD b1,
BDD b2,
BDDVarSet dom,
BDDFactory.BDDOp op) |
abstract BDD |
BDD.ite(BDD thenBDD,
BDD elseBDD)
if-then-else operator.
|
BDD |
BDDFactoryIntImpl.IntBDD.ite(BDD thenBDD,
BDD elseBDD) |
BDD |
TypedBDDFactory.TypedBDD.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) |
void |
TestBDDFactory.printTable(BDD b) |
void |
TypedBDDFactory.printTable(BDD b) |
BDD |
BDD.relprod(BDD that,
BDDVarSet var)
Relational product.
|
BDD |
TypedBDDFactory.TypedBDD.relprod(BDD that,
BDDVarSet var) |
abstract BDD |
BDD.restrict(BDD var)
Restrict a set of variables to constant values.
|
BDD |
BDDFactoryIntImpl.IntBDD.restrict(BDD var) |
BDD |
TypedBDDFactory.TypedBDD.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) |
BDD |
TypedBDDFactory.TypedBDD.restrictWith(BDD var) |
protected int |
BDDFactory.save_rec_original(BufferedWriter out,
Map visited,
BDD root)
Helper function for save().
|
protected int |
BDDFactory.save_rec(BufferedWriter out,
BitSet visited,
BDD root)
Helper function for save().
|
void |
BDDFactory.save(BufferedWriter out,
BDD r)
Saves a BDD to an output writer.
|
void |
JFactory.save(BufferedWriter out,
BDD b) |
void |
MicroFactory.save(BufferedWriter out,
BDD b) |
void |
UberMicroFactory.save(BufferedWriter out,
BDD b) |
void |
BDDFactory.save(String filename,
BDD var)
Saves a BDD to a file.
|
void |
TestBDDFactory.save(String filename,
BDD var) |
void |
TypedBDDFactory.save(String filename,
BDD var) |
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) |
BDD |
TypedBDDFactory.TypedBDD.simplify(BDD d) |
protected static int |
BDDFactoryIntImpl.unwrap(BDD b) |
void |
JFactory.validateBDD(BDD b) |
void |
MicroFactory.validateBDD(BDD b) |
void |
UberMicroFactory.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.
|
| Constructor and 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.
|
TypedBDD(BDD bdd,
Set dom) |
Copyright © 2020. All rights reserved.