public class RavenBDDDomain extends Object
RavenBDDFactory
,
RavenBDD
,
RavenBDDPairing
Modifier and Type | Method and Description |
---|---|
static RavenBDDDomain |
createDomain(int length)
Creates a new BDD Domain with
length bits. |
static RavenBDDDomain[] |
createDomains(int amount,
int length)
Creates
amount new BDD Domains with length bits. |
RavenBDD |
getBDDForInteger(int number,
int bitLength)
Returns a BDD representing a (non-negative) integer value
number as binary encoding
of length bitLength . |
RavenBDD |
getDomainBDD()
Returns a BDD encoding all variables used by this BDD Domain
|
static int |
getInteger(RavenBDD bdd)
Returns the integer which is encoded (as bit string) by the BDD
bdd . |
RavenBDD |
getIthBDD(int i)
Returns a BDD representing the
i -th variable of the BDD-Domain. |
int |
getLength()
Returns the number of bits used to define this BDD domain.
|
int[] |
getVars()
Return all variables of this domain.
|
static RavenBDD |
one()
Returns the One-BDD.
|
static RavenBDD |
zero()
Returns the Zero-BDD.
|
public static RavenBDDDomain createDomain(int length)
length
bits.length
- the length of the BDD Domain (in bits)public static RavenBDDDomain[] createDomains(int amount, int length)
amount
new BDD Domains with length
bits.amount
- the number of new BDD Domainslength
- the length of the BDD Domain (in bits)public static RavenBDD one()
public static RavenBDD zero()
public static int getInteger(RavenBDD bdd)
bdd
.
If the bdd is not a singleton set, i.e. the number of satisfying assignments
is not equal to one, -1
is returned.bdd
- the singleton set containing the encoded number (as bit string)-1
if the bdd does not
encode a singleton setpublic int getLength()
public RavenBDD getDomainBDD()
public int[] getVars()
public RavenBDD getIthBDD(int i)
i
-th variable of the BDD-Domain.i
- index of the BDD-variablepublic RavenBDD getBDDForInteger(int number, int bitLength)
number
as binary encoding
of length bitLength
.number
- number) to be representedbitLength
- length of the binary encoding