SableJBDD.fdd
Class FiniteDomain

java.lang.Object
  extended bySableJBDD.fdd.FiniteDomain

public class FiniteDomain
extends java.lang.Object

A finite domain provides constructions and operations of BDD functions on a finite set of variables.


Constructor Summary
FiniteDomain(JBddManager manager, java.lang.String name, int size)
          Defines a finite domain with a BDD manager, a domain name, and the domain capacity.
FiniteDomain(JBddManager manager, java.lang.String name, int[] varidxes)
          Defines a finite domain with a bdd manager and variables at specific levels.
FiniteDomain(JBddManager manager, java.lang.String name, int[] varidxes, boolean expandible)
          Defines a finite domain with a bdd manager, name, variables at specific levels, and a expandible flag.
FiniteDomain(JBddManager manager, java.lang.String name, int size, boolean expandible)
          Defines a finite domain with a BDD manager, a domain name, domain capacity, and a flag indicating whether the domain can be expanded automatically.
 
Method Summary
 JBDD domainRepresentation()
           
 JBDD exist(JBDD f)
          Applies existential quantification on variables of this domain.
 JBDD ith(int i)
          Gets a BDD function representing the ith element of this domain.
 JBDD replace(JBDD x, FiniteDomain other)
          Replaces domain variables in a BDD by variables in another domain.
 void reportOrdering(java.io.PrintStream out)
          Reports variable orderings in this domain, from low to high.
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

FiniteDomain

public FiniteDomain(JBddManager manager,
                    java.lang.String name,
                    int size)
Defines a finite domain with a BDD manager, a domain name, and the domain capacity.


FiniteDomain

public FiniteDomain(JBddManager manager,
                    java.lang.String name,
                    int size,
                    boolean expandible)
Defines a finite domain with a BDD manager, a domain name, domain capacity, and a flag indicating whether the domain can be expanded automatically.


FiniteDomain

public FiniteDomain(JBddManager manager,
                    java.lang.String name,
                    int[] varidxes)
Defines a finite domain with a bdd manager and variables at specific levels.


FiniteDomain

public FiniteDomain(JBddManager manager,
                    java.lang.String name,
                    int[] varidxes,
                    boolean expandible)
Defines a finite domain with a bdd manager, name, variables at specific levels, and a expandible flag.

Method Detail

ith

public JBDD ith(int i)
Gets a BDD function representing the ith element of this domain. Side effect: if i exceeds the capacity of this domain, the domain is expanded automatically by allocating new variables from the underlying BDD manager. It is user's reponsibility to ensure the right order and capacity of a domain.

Parameters:
i - an integer
Returns:
the BDD function for ith element

domainRepresentation

public JBDD domainRepresentation()
Returns:
a BDD function representing the conjunction of variables in this domain.

replace

public JBDD replace(JBDD x,
                    FiniteDomain other)
Replaces domain variables in a BDD by variables in another domain. Two domains must be compatible:

Parameters:
x - the bdd to be replace
other - the target domain
Returns:
the new BDD function after replacement

exist

public JBDD exist(JBDD f)
Applies existential quantification on variables of this domain.

Parameters:
f - the BDD function to be quantified
Returns:
the resulted BDD function

reportOrdering

public void reportOrdering(java.io.PrintStream out)
Reports variable orderings in this domain, from low to high.

Parameters:
out - the print stream