public class RavenBDD extends Object implements Cloneable, Data
RavenBDDFactory
,
RavenBDDDomain
,
RavenBDDPairing
Modifier and Type | Class and Description |
---|---|
static class |
RavenBDD.Type
Enumeration of the different types of implemented BDDs.
|
Modifier and Type | Method and Description |
---|---|
List<byte[]> |
allSat()
Finds all satisfying variable assignments.
|
RavenBDD |
and(RavenBDD bdd)
Returns a BDD which is the logical AND of this BDD and the
BDD
bdd . |
RavenBDD |
applyAll(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an universal
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
applyEx(RavenBDD bdd,
RavenBDDFactory.BDDOperator operator,
RavenBDD variables)
Applies the operator
operator to this BDD and
the BDD bdd and afterwards performs an existential
quantification of the BDD nodes specified by the BDD
variables . |
RavenBDD |
biimp(RavenBDD bdd)
Returns a BDD which is the logical BIIMPLICATION of this BDD and the
BDD
bdd . |
RavenBDD |
clone() |
boolean |
equals(Object o) |
RavenBDD |
exists(RavenBDD bdd)
Performs an existential quantification of the BDD nodes
specified by the given BDD.
|
RavenBDD |
forAll(RavenBDD bdd)
Performs an universal quantification of the BDD nodes
specified by the given BDD.
|
void |
free()
Frees this BDD.
|
RavenBDD |
getOne()
Returns the One-BDD.
|
List<RavenBDD> |
getSatAssignments(RavenBDD var)
Returns a list of satisfying variable assignments (seen as BDDs) for the variables
var . |
RavenBDD.Type |
getType()
Returns the type of the data object.
|
int[] |
getVarProfile()
Returns the number of times each variable occurs in this BDD.
|
RavenBDD |
getZero()
Returns the Zero-BDD.
|
int |
hashCode() |
RavenBDD |
high()
Returns the high successor of this BDD.
|
RavenBDD |
imp(RavenBDD bdd)
Returns a BDD which is the logical IMPLICATION of the this BDD and the
BDD
bdd . |
boolean |
isOne()
Returns
true if and only if the BDD is the ONE-BDD. |
boolean |
isZero()
Returns
true if and only if the BDD is the ZERO-BDD. |
static RavenBDD |
loadBDD(InputStream is)
Loads a BDD from the input stream
is ; |
RavenBDD |
low()
Returns the low successor of this BDD.
|
int |
nodeCount()
Returns the number of nodes used to encode this BDD.
|
RavenBDD |
not()
Returns a BDD which is the logical NOT of this BDD.
|
RavenBDD |
or(RavenBDD bdd)
Returns a BDD which is the logical OR of this BDD and the
BDD
bdd . |
int |
pathCount()
Returns the number of paths leading to the true terminal.
|
void |
printDot(PrintStream out)
Prints this BDD in DOT syntax to the output stream
out . |
RavenBDD |
replace(RavenBDDPairing pairing)
Replaces the BDD nodes according to the given BDD pairing.
|
RavenBDD |
restrict(RavenBDD bdd)
Restricts the BDD according to the given BDD.
|
int |
satCount(RavenBDD vars)
Returns the number of satisfying assignments to this BDD.
|
static void |
saveBDD(RavenBDD ravenBDD,
ZipOutputStream zos,
String name)
Writes the BDD
ravenBDD to the stream zos and saves it to the zip file
named name . |
static String |
toBitString(byte[] assignment)
Converts the (satisfying) variable assignment (seen as byte array) to a bit string with
least significant bit left.
|
static int |
toInteger(byte[] assignment)
Converts the (satisfying) variable assignment (seen as byte array) to a n integer value
|
String |
toString() |
int |
var()
Returns the variable (in the root) of this BDD.
|
RavenBDD |
xor(RavenBDD bdd)
Returns a BDD which is the logical XOR of this BDD and the
BDD
bdd . |
public static int toInteger(byte[] assignment)
assignment
- the (satisfying) variable assignmentpublic static String toBitString(byte[] assignment)
assignment
- the (satisfying) variable assignmentpublic static void saveBDD(RavenBDD ravenBDD, ZipOutputStream zos, String name) throws IOException
ravenBDD
to the stream zos
and saves it to the zip file
named name
.ravenBDD
- the BDD to be savedzos
- the stream to the zip filename
- the name of the zip file entryIOException
- if an I/O error has occurredpublic static RavenBDD loadBDD(InputStream is) throws IOException
is
;is
- the input stream from which the BDD is readIOException
- if an I/O error has occurredpublic List<RavenBDD> getSatAssignments(RavenBDD var)
var
.var
- the variables for which a satisfying variable assignment is computedpublic void free()
public int var()
public RavenBDD low()
public RavenBDD high()
public RavenBDD and(RavenBDD bdd)
bdd
.bdd
- the BDD which will be applied to this BDDpublic RavenBDD biimp(RavenBDD bdd)
bdd
.bdd
- the BDD which will be applied to this BDDpublic RavenBDD imp(RavenBDD bdd)
bdd
.bdd
- the BDD which will be applied to this BDDpublic RavenBDD not()
public RavenBDD or(RavenBDD bdd)
bdd
.bdd
- the BDD which will be applied to this BDDpublic RavenBDD xor(RavenBDD bdd)
bdd
.bdd
- the BDD which will be applied to this BDDpublic RavenBDD forAll(RavenBDD bdd)
bdd
- the BDD to specify the BDD nodes to be quantifiedpublic RavenBDD applyAll(RavenBDD bdd, RavenBDDFactory.BDDOperator operator, RavenBDD variables)
operator
to this BDD and
the BDD bdd
and afterwards performs an universal
quantification of the BDD nodes specified by the BDD
variables
.bdd
- the BDD to be applied with this bddoperator
- the operator to be applied to both bddsvariables
- the BDD to specify the BDD nodes to be quantifiedpublic RavenBDD exists(RavenBDD bdd)
bdd
- the BDD to specify the BDD nodes to be quantifiedpublic RavenBDD applyEx(RavenBDD bdd, RavenBDDFactory.BDDOperator operator, RavenBDD variables)
operator
to this BDD and
the BDD bdd
and afterwards performs an existential
quantification of the BDD nodes specified by the BDD
variables
.bdd
- the BDD to be applied with this bddoperator
- the operator to be applied to both bddsvariables
- the BDD to specify the BDD nodes to be quantifiedpublic RavenBDD restrict(RavenBDD bdd)
bdd
- the BDD to be used for the restrictionpublic RavenBDD replace(RavenBDDPairing pairing)
pairing
- the BDD pairing to be used for the replacementpublic RavenBDD getOne()
public RavenBDD getZero()
public boolean isOne()
true
if and only if the BDD is the ONE-BDD.true
if the BDD is one, false
otherwisepublic boolean isZero()
true
if and only if the BDD is the ZERO-BDD.true
if the BDD is zero, false
otherwisepublic int nodeCount()
public int satCount(RavenBDD vars)
vars
- a BDD encoding the fixed variable assignmentspublic int pathCount()
public List<byte[]> allSat()
public int[] getVarProfile()
public void printDot(PrintStream out)
out
.out
- the output stream to be used as output
For further informations about the DOT syntax see GraphViz
(Dot Guide).public RavenBDD.Type getType()
Data