sdd

Class SDDTrees

java.lang.Object

sdd.SDDTrees

public class SDDTrees
extends java.lang.Object

The static methods for SDDTree.

Constructor Summary

Constructors

Constructor and Description
SDDTrees()

Method Summary

Methods

Modifier and Type	Method and Description
static SDDTree	and(SDDTree tr1, SDDTree tr2, SDDMemory mem) Computes the conjunction of the two specified SDD trees.
static SDDTree	ban_and(SDDTree tr1, SDDTree tr2, SDDMemory mem) Computes the conjunction of the two specified SDD trees.
static SDDTree	ban_exists(SDDTree sdd, Variable var, SDDMemory mem, VtreePath path) Computes the result of the exists operation on the specified sdd for the specified variable.
static SDDTree	ban_forall(SDDTree sdd, Variable var, SDDMemory mem, VtreePath path) Computes the result of the forall operation on the specified sdd for the specified variable.
static SDDTree	ban_not(SDDTree sdd, SDDMemory mem) Computes the negation of the specified SDD tree.
static SDDTree	ban_or(SDDTree tr1, SDDTree tr2, SDDMemory mem) Computes the disjunction of the two specified SDD trees.
static SDDTree	buildSimpleSDDNode(SDDTree prime, SDDTree sub, SDDMemory mem)
static int	compare(SDDTree t1, SDDTree t2) Gives a total order on the SDD tree.
static SDDTree	exists(SDDTree sdd, Variable var, SDDMemory mem, VtreePath path) Computes the result of the exists operation on the specified sdd for the specified variable.
static SDDTree	forall(SDDTree sdd, Variable var, SDDMemory mem, VtreePath path) Computes the result of the forall operation on the specified sdd for the specified variable.
static SDDTree	not(SDDTree sdd, SDDMemory mem) Computes the negation of the specified SDD tree.
static SDDTree	or(SDDTree tr1, SDDTree tr2, SDDMemory mem) Computes the disjunction of the two specified SDD trees.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

SDDTrees

public SDDTrees()

Method Detail

and

public static SDDTree and(SDDTree tr1,
          SDDTree tr2,
          SDDMemory mem)

Computes the conjunction of the two specified SDD trees.

Parameters:

tr1 - the first SDD tree.

tr2 - the second SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the conjunction of tr1 and tr2.

ban_and

public static SDDTree ban_and(SDDTree tr1,
              SDDTree tr2,
              SDDMemory mem)

Computes the conjunction of the two specified SDD trees.

Parameters:

tr1 - the first SDD tree.

tr2 - the second SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the conjunction of tr1 and tr2.

or

public static SDDTree or(SDDTree tr1,
         SDDTree tr2,
         SDDMemory mem)

Computes the disjunction of the two specified SDD trees.

Parameters:

tr1 - the first SDD tree.

tr2 - the second SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the disjunction of tr1 and tr2.

ban_or

public static SDDTree ban_or(SDDTree tr1,
             SDDTree tr2,
             SDDMemory mem)

Computes the disjunction of the two specified SDD trees.

Parameters:

tr1 - the first SDD tree.

tr2 - the second SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the disjunction of tr1 and tr2.

not

public static SDDTree not(SDDTree sdd,
          SDDMemory mem)

Computes the negation of the specified SDD tree.

Parameters:

sdd - the SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the negation of sdd.

ban_not

public static SDDTree ban_not(SDDTree sdd,
              SDDMemory mem)

Computes the negation of the specified SDD tree.

Parameters:

sdd - the SDD tree.

mem - the SDD memory used to record already computed objects.

Returns:

an SDDTree corresponding to the negation of sdd.

exists

public static SDDTree exists(SDDTree sdd,
             Variable var,
             SDDMemory mem,
             VtreePath path)

Computes the result of the exists operation on the specified sdd for the specified variable.

Parameters:

sdd - the SDD tree.

var - the variable for which the existentiality is computed.

mem - the SDD memory used to record already computed objects.

path - the path from the root of the vtree to the variable.

Returns:

an SDDTree corresponding to the existence of a value for var.

ban_exists

public static SDDTree ban_exists(SDDTree sdd,
                 Variable var,
                 SDDMemory mem,
                 VtreePath path)

Computes the result of the exists operation on the specified sdd for the specified variable.

Parameters:

sdd - the SDD tree.

var - the variable for which the existentiality is computed.

mem - the SDD memory used to record already computed objects.

path - the path from the root of the vtree to the variable.

Returns:

an SDDTree corresponding to the existence of a value for var.

forall

public static SDDTree forall(SDDTree sdd,
             Variable var,
             SDDMemory mem,
             VtreePath path)

Computes the result of the forall operation on the specified sdd for the specified variable.

Parameters:

sdd - the SDD tree.

var - the variable for which the forall is computed.

mem - the SDD memory used to record already computed objects.

path - the path from the root of the vtree to the variable.

Returns:

an SDDTree corresponding to the universality of a value for var.

ban_forall

public static SDDTree ban_forall(SDDTree sdd,
                 Variable var,
                 SDDMemory mem,
                 VtreePath path)

Computes the result of the forall operation on the specified sdd for the specified variable.

Parameters:

sdd - the SDD tree.

var - the variable for which the forall is computed.

mem - the SDD memory used to record already computed objects.

path - the path from the root of the vtree to the variable.

Returns:

an SDDTree corresponding to the universality of a value for var.

buildSimpleSDDNode

public static SDDTree buildSimpleSDDNode(SDDTree prime,
                         SDDTree sub,
                         SDDMemory mem)

compare

public static int compare(SDDTree t1,
          SDDTree t2)

Gives a total order on the SDD tree.

Parameters:

t1 - the first SDD tree.

t2 - the second SDD tree.

Returns:

-1 if t1 < t2, 1 if t1 > t2, 0 if t1 == t2.