sdd

Class SDDMemory

java.lang.Object

sdd.SDDMemory

public class SDDMemory
extends java.lang.Object

An SDD memory is an object that remembers the computed SDDTree, i.e., the results of the and, or, not, exists, forall, and tree-based (e.g., left rotation) operations. The set of variables is assumed to be constant for the existence and universal operators and the tree operations are supposed to be the same as well.

Constructor Summary

Constructors

Constructor and Description
SDDMemory() Creates an empty memory.

Method Summary

Methods

Modifier and Type	Method and Description
void	addAnd(SDDTreeDisjunction c1, SDDTreeDisjunction c2, SDDTree c) Stores the specified result of the conjunction of the two specified SDDTree.
void	addExists(SDDTreeDisjunction t, SDDTreeDisjunction e) Stores the specified result of the existence operation on the specified SDDTree.
void	addForall(SDDTreeDisjunction t, SDDTreeDisjunction f) Stores the specified result of the universal operation on the specified SDDTree.
void	addNot(SDDTreeDisjunction t, SDDTreeDisjunction n) Stores the specified result of the negation of the specified SDDTree.
void	addOr(SDDTreeDisjunction d1, SDDTreeDisjunction d2, SDDTree d) Stores the specified result of the disjunction of the two specified SDDTree.
void	addTree(SDDTreeDisjunction t, SDDTreeDisjunction f) Stores the specified result of the tree-based operation on the specified SDDTree.
SDDTree	and(SDDTreeDisjunction t1, SDDTreeDisjunction t2) Returns the result of the AND operation between the two specified SDDTreeDisjunction if this result is known, null otherwise.
void	empty() Empties the memory.
SDDTree	exists(SDDTreeDisjunction t) Returns the result of the EXISTS operation on the specified SDDTreeDisjunction if this result is known, null otherwise.
SDDTree	forall(SDDTreeDisjunction t) Returns the result of the FORALL operation on the specified SDDTreeDisjunction if this result is known, null otherwise.
SDDTree	not(SDDTreeDisjunction t) Returns the result of the NOT operation on the specified SDDTreeDisjunction if this result is known, null otherwise.
SDDTree	or(SDDTreeDisjunction t1, SDDTreeDisjunction t2) Returns the result of the OR operation between the two specified SDDTreeDisjunction if this result is known, null otherwise.
SDDTree	tree(SDDTreeDisjunction t) Returns the result of the tree-based operation on the specified SDDTreeDisjunction if this result is known, null otherwise.

Methods inherited from class java.lang.Object

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

Constructor Detail

SDDMemory

public SDDMemory()

Creates an empty memory.

Method Detail

and

public SDDTree and(SDDTreeDisjunction t1,
          SDDTreeDisjunction t2)

Returns the result of the AND operation between the two specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t1 - the first conjunct.

t2 - the second conjunct.

Returns:

the conjunction of t1 and t2 if known.

addAnd

public void addAnd(SDDTreeDisjunction c1,
          SDDTreeDisjunction c2,
          SDDTree c)

Stores the specified result of the conjunction of the two specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

c1 - the first conjunct.

c2 - the second conjunct.

c - the conjunction.

or

public SDDTree or(SDDTreeDisjunction t1,
         SDDTreeDisjunction t2)

Returns the result of the OR operation between the two specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t1 - the first disjunct.

t2 - the second disjunct.

Returns:

the disjunction of t1 and t2 if known.

addOr

public void addOr(SDDTreeDisjunction d1,
         SDDTreeDisjunction d2,
         SDDTree d)

Stores the specified result of the disjunction of the two specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

d1 - the first disjunct.

d2 - the second disjunct.

d - the conjunction.

not

public SDDTree not(SDDTreeDisjunction t)

Returns the result of the NOT operation on the specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t - the negated tree.

Returns:

the negation of t.

addNot

public void addNot(SDDTreeDisjunction t,
          SDDTreeDisjunction n)

Stores the specified result of the negation of the specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

t - the tree.

n - the negation of t.

exists

public SDDTree exists(SDDTreeDisjunction t)

Returns the result of the EXISTS operation on the specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t - the tree.

Returns:

the tree obtained after the existence operation on t.

addExists

public void addExists(SDDTreeDisjunction t,
             SDDTreeDisjunction e)

Stores the specified result of the existence operation on the specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

t - the tree.

e - the result of existence operation on t.

forall

public SDDTree forall(SDDTreeDisjunction t)

Returns the result of the FORALL operation on the specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t - the tree.

Returns:

the tree obtained after the universal operation on t.

addForall

public void addForall(SDDTreeDisjunction t,
             SDDTreeDisjunction f)

Stores the specified result of the universal operation on the specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

t - the tree.

f - the result of universal operation on t.

tree

public SDDTree tree(SDDTreeDisjunction t)

Returns the result of the tree-based operation on the specified SDDTreeDisjunction if this result is known, null otherwise. As a consequence, a watch operation is performed on the returned SDDTree.

Parameters:

t - the tree.

Returns:

the tree obtained after the tree-based operation on t.

addTree

public void addTree(SDDTreeDisjunction t,
           SDDTreeDisjunction f)

Stores the specified result of the tree-based operation on the specified SDDTree. As a consequence, all elements are watched (the empty() method should be called to clean this).

Parameters:

t - the tree.

f - the result of tree-based operation on t.

empty

public void empty()

Empties the memory. As a consequence, all watched elements are unwatched. This method should be called every time the SDDMemory is no longer necessary.