public class SDDMemory
extends java.lang.Object
| Constructor and Description |
|---|
SDDMemory()
Creates an empty memory.
|
| 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.
|
public SDDTree and(SDDTreeDisjunction t1, SDDTreeDisjunction t2)
t1 - the first conjunct.t2 - the second conjunct.public void addAnd(SDDTreeDisjunction c1, SDDTreeDisjunction c2, SDDTree c)
c1 - the first conjunct.c2 - the second conjunct.c - the conjunction.public SDDTree or(SDDTreeDisjunction t1, SDDTreeDisjunction t2)
t1 - the first disjunct.t2 - the second disjunct.public void addOr(SDDTreeDisjunction d1, SDDTreeDisjunction d2, SDDTree d)
d1 - the first disjunct.d2 - the second disjunct.d - the conjunction.public SDDTree not(SDDTreeDisjunction t)
t - the negated tree.public void addNot(SDDTreeDisjunction t, SDDTreeDisjunction n)
t - the tree.n - the negation of t.public SDDTree exists(SDDTreeDisjunction t)
t - the tree.public void addExists(SDDTreeDisjunction t, SDDTreeDisjunction e)
t - the tree.e - the result of existence operation on t.public SDDTree forall(SDDTreeDisjunction t)
t - the tree.public void addForall(SDDTreeDisjunction t, SDDTreeDisjunction f)
t - the tree.f - the result of universal operation on t.public SDDTree tree(SDDTreeDisjunction t)
t - the tree.public void addTree(SDDTreeDisjunction t, SDDTreeDisjunction f)
t - the tree.f - the result of tree-based operation on t.public void empty()