SableJBDD.bdd
Class JBDD

java.lang.Object
  extended bySableJBDD.bdd.JBDD

public class JBDD
extends java.lang.Object

A BDD object represents a bdd function. It has a root node and a manager, and supports basic bdd operations.


Method Summary
 JBDD and(JBDD other)
          AND operation.
 void andWith(JBDD other)
          In-node AND operation in place.
 JBDD biimply(JBDD other)
          BIIMPLY operation.
 JBDD copy()
          Returns a copy of current BDD with the same manager and same root node.
 JBDD diff(JBDD other)
          DIFF operation.
 boolean equals(java.lang.Object other)
           
 JBDD exist(JBDD vars)
          Apply existential quantification on this bdd function.
 JBDD forall(JBDD vars)
          Apply universal quantification on this bdd function.
 int hashCode()
           
 JBDD imply(JBDD other)
          IMPLY operation.
 JBDD invimp(JBDD other)
          Inverse imply operation.
 boolean isOne()
          Checks if this BDD is ONE
 boolean isRootOf(JBddVariable var)
          Checks if the root is a particular variable
 boolean isZero()
          Checks if this BDD is ZERO
 JBDD less(JBDD other)
          LESS operation.
 JBDD nand(JBDD other)
          NAND operations, it is more efficient than AND followed by NOT.
 void nandWith(JBDD other)
          In-node NAND operation.
 JBDD nor(JBDD other)
          NOR operation, it is more efficient than OR followed by NOT.
 void norWith(JBDD other)
          In-node NOR operation.
 JBDD not()
          NOT operation.
 JBDD or(JBDD other)
          OR operation.
 void orWith(JBDD other)
          In-node OR operation.
 JBDD replace(java.util.Map varmap)
          Replaces a set of variables in this bdd to another set of variables.
 int size()
          Counts the size of this bdd function (the number of internal nodes), excluding two sink nodes.
 void toDotGraph(java.io.PrintStream out, java.lang.String graphname)
          Dumps this bdd to a DOT format graph.
 java.lang.String toString()
           
 JBDD unique(JBDD vars)
          Apply unique quantification on this bdd function.
 JBDD xor(JBDD other)
          XOR operation.
 void xorWith(JBDD other)
          In-node XOR operation.
 
Methods inherited from class java.lang.Object
getClass, notify, notifyAll, wait, wait, wait
 

Method Detail

copy

public JBDD copy()
Returns a copy of current BDD with the same manager and same root node.


and

public JBDD and(JBDD other)
AND operation.

Parameters:
other - the second bdd function.
Returns:
this & other

andWith

public void andWith(JBDD other)
In-node AND operation in place.

Parameters:
other - the second bdd function

or

public JBDD or(JBDD other)
OR operation.

Parameters:
other - the second bdd function.
Returns:
this | other

orWith

public void orWith(JBDD other)
In-node OR operation.

Parameters:
other - the second bdd function

not

public JBDD not()
NOT operation.

Returns:
! this

xor

public JBDD xor(JBDD other)
XOR operation.

Parameters:
other - the second bdd function.
Returns:
this (+) other

xorWith

public void xorWith(JBDD other)
In-node XOR operation.

Parameters:
other - the second bdd function.

nand

public JBDD nand(JBDD other)
NAND operations, it is more efficient than AND followed by NOT.

Parameters:
other - the second bdd function.
Returns:
! (this & other)

nandWith

public void nandWith(JBDD other)
In-node NAND operation.

Parameters:
other - the second bdd function.

nor

public JBDD nor(JBDD other)
NOR operation, it is more efficient than OR followed by NOT.

Parameters:
other - the second bdd function.
Returns:
! (this | other)

norWith

public void norWith(JBDD other)
In-node NOR operation.

Parameters:
other - the second bdd function.

imply

public JBDD imply(JBDD other)
IMPLY operation.

Parameters:
other - the second bdd function.
Returns:
this -> other

biimply

public JBDD biimply(JBDD other)
BIIMPLY operation.

Parameters:
other - the second bdd function.
Returns:
this <-> other

diff

public JBDD diff(JBDD other)
DIFF operation.

Parameters:
other - the second bdd function.
Returns:
this / other

less

public JBDD less(JBDD other)
LESS operation.

Parameters:
other - the second bdd function.
Returns:
this < other

invimp

public JBDD invimp(JBDD other)
Inverse imply operation.

Parameters:
other - the second bdd function.
Returns:
this <- other

replace

public JBDD replace(java.util.Map varmap)
Replaces a set of variables in this bdd to another set of variables.

Parameters:
varmap - a map from a set of variables to another set of variables, where the variables of the first set in this bdd will be replaced by the variables of the second set.
Returns:
the new bdd after replacement This method may fail if this bdd contains nodes of variables of replacing targets.

exist

public JBDD exist(JBDD vars)
Apply existential quantification on this bdd function.

Parameters:
vars - a bdd which is the conjunction of several variables' positive form.
Returns:
the resulted bdd function

forall

public JBDD forall(JBDD vars)
Apply universal quantification on this bdd function.

Parameters:
vars - a bdd which is the conjunction of several variables' positive form.
Returns:
the resulted bdd function

unique

public JBDD unique(JBDD vars)
Apply unique quantification on this bdd function.

Parameters:
vars - a bdd which is the conjunction of several variables' positive form.
Returns:
the resulted bdd function.

isZero

public boolean isZero()
Checks if this BDD is ZERO

Returns:
true if this is zero

isOne

public boolean isOne()
Checks if this BDD is ONE

Returns:
true if this is one

isRootOf

public boolean isRootOf(JBddVariable var)
Checks if the root is a particular variable

Returns:
true if it is

size

public int size()
Counts the size of this bdd function (the number of internal nodes), excluding two sink nodes.

Returns:
the size of this bdd function.

toDotGraph

public void toDotGraph(java.io.PrintStream out,
                       java.lang.String graphname)
Dumps this bdd to a DOT format graph.

Parameters:
out - the output stream
graphname - the name in DOT graph

hashCode

public int hashCode()

equals

public boolean equals(java.lang.Object other)

toString

public java.lang.String toString()