SDD

java.lang.Object
- buffer.CanonicalWatched
- - sdd.SDD

```
public class SDD
extends CanonicalWatched
```
An SDD is defined by a SDD tree and the vtree upon which the SDD tree is defined.

Method Summary

Methods
Modifier and Type	Method and Description
`SDD`	`and(SDD other)` Returns the SDD corresponding to the AND operation between this SDD and the specified SDD.
`<X> X`	`apply(SDDFunction<X> f)` Applies the specified SDD function on this SDD.
`static SDD`	`constant(boolean constant, Vtree tree)` Returns the SDD representing the specified constant.
`static SDD`	`create(SDDTree sdd, Vtree tree)` Creates an SDD defined as the specified SDD tree on the specified vtree.
`protected void`	`destroy()` Notifies this object that it is no longer referenced.
`protected boolean`	`equivalent(java.lang.Object obj)` Indicates whether the specified object is equivalent to this object.
`SDD`	`exists(Variable vr)` Computes the SDD resulting from the existantial operation over this SDD for the specified variable.
`SDD`	`forall(Variable vr)` Computes the SDD resulting from the universal operation over this SDD for the specified variable.
`java.util.List<Assignment>`	`getAssignments()` Returns the models of this SDD.
`protected java.util.Map<java.lang.Object,SDD>`	`getBuffer()` Returns the buffer that is used to decide the canonical objects.
`Assignment`	`getOneAssignment()` Returns one model of this SDD.
`SDDTree`	`getSDDTree()` Returns the SDDTree of this SDD.
`Vtree`	`getTree()` Returns the Vtree of this SDD.
`int`	`hashCode()`
`boolean`	`isConstant()` Indicates whether this SDD represents a constant (true or false).
`boolean`	`isSat()` Indicates whether this SDD is satisfiable, i.e., whether it is different from false.
`boolean`	`isValid()` Indicates whether this SDD is valid, i.e., whether it is equivalent to true.
`SDD`	`leftRotation(VtreeNode nodeWhereLeftRotationIsPerformed)` Performs a left rotation operation on the specified node of the vtree.
`SDD`	`leftRotationOnRoot()` Performs a left rotation operation on the root of this SDD.
`java.math.BigInteger`	`nbModels()` Returns the number of models of this SDD.
`SDD`	`neg()` Returns the SDD corresponding to the NOT operation on this SDD.
`SDD`	`or(SDD other)` Returns the SDD corresponding to the OR operation between this SDD and the specified SDD.
`static SDD`	`or(Vtree tree, SDD... sdds)` Performs an OR operation on the specified collection of SDD.
`static void`	`printBuffer(java.io.PrintStream out)` Prints the content of the SDD buffer, i.e., the list of SDD that are still being watched.
`static SDD`	`readCNF(Vtree vtree, java.util.List<SDD> vars, IntegerTokenizer tokizer)` Reads the CNF in the specified integer tokenizer with the specified list of sdds (representing the variables) and the specified vtree.
`SDD`	`replace(Variable var1, Variable var2)` Computes the SDD where every instance of the first specified variable is replaced in this SDD by an instance of the second variable.
`SDD`	`rightRotation(VtreeNode nodeWhereRightRotationIsPerformed)` Performs a right rotation operation on the specified node of the vtree.
`SDD`	`rightRotationOnRoot()` Performs a right rotation operation on the root of this SDD.
`int`	`size()` Returns the number of nodes used to represent this SDD.
`SDD`	`swapVnodeOnRoot()` Performs a swap operation on the root of this SDD.
`void`	`toDot()` Prints a DOT representation of this SDD in `System.out`.
`void`	`toDot(java.lang.String filename)` Prints a DOT representation of this SDD in the file at the specified address.
`static void`	`toDot(java.lang.String filename, SDD... sdds)` Print a DOT representation of the specified collection of SDDs in the file at the specified address.
`java.lang.String`	`toString()`
`static SDD`	`variable(Variable var, Vtree tree)` Creates the SDD associated with the specified variable (i.e., the positive literal associated with the variable) for a given vtree.

Methods inherited from class buffer.CanonicalWatched
equals, getCanonical, print, unwatch, unwatchAll, verifyValidity, watch

Methods inherited from class java.lang.Object
clone, finalize, getClass, notify, notifyAll, wait, wait, wait

- Method Detail
  - create
```
public static SDD create(SDDTree sdd,
         Vtree tree)
```
    Creates an SDD defined as the specified SDD tree on the specified vtree.
    
    Parameters:
    sdd - the SDD tree.
    tree - the vtree upon which the SDD tree is defined.
    
    Returns:
    the SDD corresponding to the data structure sdd defined on the vtree tree.
  - variable
```
public static SDD variable(Variable var,
           Vtree tree)
```
    Creates the SDD associated with the specified variable (i.e., the positive literal associated with the variable) for a given vtree.
    
    Parameters:
    var - the variable.
    tree - the vtree.
    
    Returns:
    the SDD associated with var.
  - constant
```
public static SDD constant(boolean constant,
           Vtree tree)
```
    Returns the SDD representing the specified constant.
    
    Parameters:
    constant - the constant (true or false) of the SDD.
    tree - the tree upon which the SDD is built.
    
    Returns:
    the SDD corresponding to constant.
  - hashCode
```
public int hashCode()
```
    Specified by:
    
    hashCode in class CanonicalWatched
  - equivalent
```
protected boolean equivalent(java.lang.Object obj)
```
    Description copied from class: CanonicalWatched
    
    Indicates whether the specified object is equivalent to this object. There should not be two equivalent objects, so this method is used at the creation of this type of object to verify whether the object create is truly original.
    
    Specified by:
    
    equivalent in class CanonicalWatched
    
    Parameters:
    obj - the object compared to this object.
    
    Returns:
    true if obj is equivalent to this.
  - getBuffer
```
protected java.util.Map<java.lang.Object,SDD> getBuffer()
```
    Description copied from class: CanonicalWatched
    
    Returns the buffer that is used to decide the canonical objects.
    
    Specified by:
    
    getBuffer in class CanonicalWatched
    
    Returns:
    a map that contains the canonical objects.
  - destroy
```
protected void destroy()
```
    Description copied from class: CanonicalWatched
    
    Notifies this object that it is no longer referenced. The object may have some cleaning up to do at this stage. The default implementation is that the object does nothing.
    
    Overrides:
    
    destroy in class CanonicalWatched
  - readCNF
```
public static SDD readCNF(Vtree vtree,
          java.util.List<SDD> vars,
          IntegerTokenizer tokizer)
```
    Reads the CNF in the specified integer tokenizer with the specified list of sdds (representing the variables) and the specified vtree.
    
    Parameters:
    vtree - the vtree.
    vars - the list of variables (vars.get(i) is the variable referred to as x in the integer tokenizer).
    tokizer - the integer tokenizer.
    
    Returns:
    the SDD corresponding to the CNF in the tokenizer.
  - getTree
```
public Vtree getTree()
```
    Returns the Vtree of this SDD.
    
    Returns:
    the tree upon which this SDD is built.
  - getSDDTree
```
public SDDTree getSDDTree()
```
    Returns the SDDTree of this SDD.
    
    Returns:
    the SDDTree of this SDD.
  - toString
```
public java.lang.String toString()
```
    Overrides:
    
    toString in class java.lang.Object
  - toDot
```
public void toDot()
```
    Prints a DOT representation of this SDD in System.out.
  - toDot
```
public void toDot(java.lang.String filename)
```
    Prints a DOT representation of this SDD in the file at the specified address.
    
    Parameters:
    filename - the address of the file where the dot file should be stored.
  - toDot
```
public static void toDot(java.lang.String filename,
         SDD... sdds)
```
    Print a DOT representation of the specified collection of SDDs in the file at the specified address.
    
    Parameters:
    filename - the address of the file where the dot file should be stored.
    sdds - the list of SDDs that should be printed together.
  - printBuffer
```
public static void printBuffer(java.io.PrintStream out)
```
    Prints the content of the SDD buffer, i.e., the list of SDD that are still being watched. This method is mainly for debugging.
    
    Parameters:
    out - the print stream where the buffer should be printed.
  - and
```
public SDD and(SDD other)
```
    Returns the SDD corresponding to the AND operation between this SDD and the specified SDD.
    
    Parameters:
    other - the SDD that is conjuncted with this SDD.
    
    Returns:
    the SDD whose models are the intersection of this SDD's model and other's.
  - or
```
public SDD or(SDD other)
```
    Returns the SDD corresponding to the OR operation between this SDD and the specified SDD.
    
    Parameters:
    other - the SDD that is disjuncted with this SDD.
    
    Returns:
    the SDD whose models are the union of this SDD's model and other's.
  - or
```
public static SDD or(Vtree tree,
     SDD... sdds)
```
    Performs an OR operation on the specified collection of SDD.
    
    Parameters:
    tree - the Vtree upon which the SDD is built.
    sdds - the collection of SDD whose disjunction is requested.
    
    Returns:
    the disjunction of the SDDs in sdds.
  - neg
```
public SDD neg()
```
    Returns the SDD corresponding to the NOT operation on this SDD.
    
    Returns:
    the SDD whose models are exactly those that are not models of this SDD.
  - exists
```
public SDD exists(Variable vr)
```
    Computes the SDD resulting from the existantial operation over this SDD for the specified variable.
    
    Parameters:
    vr - the variable whose value is ignored.
    
    Returns:
    the SDD representing the propositional formula of this SDD where the value of vr is ignored.
  - forall
```
public SDD forall(Variable vr)
```
    Computes the SDD resulting from the universal operation over this SDD for the specified variable.
    
    Parameters:
    vr - the variable whose value is ignored.
    
    Returns:
    the SDD representing the propositional formula of this SDD that should be consistent regardless the value of vr.
  - replace
```
public SDD replace(Variable var1,
          Variable var2)
```
    Computes the SDD where every instance of the first specified variable is replaced in this SDD by an instance of the second variable. This method assumes that the second variable is free in this SDD.
    
    Parameters:
    var1 - the variable that is replaced.
    var2 - the variable that replaces var1.
    
    Returns:
    this SDD where var1 has been replaced by var2.
  - rightRotationOnRoot
```
public SDD rightRotationOnRoot()
```
    Performs a right rotation operation on the root of this SDD.
    
    Returns:
    the right rotated version of this SDD.
  - rightRotation
```
public SDD rightRotation(VtreeNode nodeWhereRightRotationIsPerformed)
```
    Performs a right rotation operation on the specified node of the vtree.
    
    Parameters:
    nodeWhereRightRotationIsPerformed - the node of the vtree of this SDD where the right rotation is performed.
    
    Returns:
    the right rotated version of this SDD.
  - leftRotationOnRoot
```
public SDD leftRotationOnRoot()
```
    Performs a left rotation operation on the root of this SDD.
    
    Returns:
    the left rotated version of this SDD.
  - leftRotation
```
public SDD leftRotation(VtreeNode nodeWhereLeftRotationIsPerformed)
```
    Performs a left rotation operation on the specified node of the vtree.
    
    Parameters:
    nodeWhereLeftRotationIsPerformed - the node of the vtree of this SDD where the left rotation is performed.
    
    Returns:
    the left rotated version of this SDD.
  - swapVnodeOnRoot
```
public SDD swapVnodeOnRoot()
```
    Performs a swap operation on the root of this SDD.
    
    Returns:
    the swapped version of this SDD.
  - getAssignments
```
public java.util.List<Assignment> getAssignments()
```
    Returns the models of this SDD. The use of this method is not recommended in general as it might return a huge number of elements (easily well above 10**10).
    
    Returns:
    the list of assignments that are consistent with this SDD.
  - getOneAssignment
```
public Assignment getOneAssignment()
```
    Returns one model of this SDD.
    
    Returns:
    an assignment consistent with this SDD if any, null otherwise.
  - isConstant
```
public boolean isConstant()
```
    Indicates whether this SDD represents a constant (true or false).
    
    Returns:
    true if this SDD represents a constant, false otherwise.
  - size
```
public int size()
```
    Returns the number of nodes used to represent this SDD.
    
    Returns:
    the size of this SDD.
  - isValid
```
public boolean isValid()
```
    Indicates whether this SDD is valid, i.e., whether it is equivalent to true.
    
    Returns:
    true if this SDD is the representation of the logical statement true.
  - isSat
```
public boolean isSat()
```
    Indicates whether this SDD is satisfiable, i.e., whether it is different from false.
    
    Returns:
    false if this SDD is the representation of the logical statement false.
  - nbModels
```
public java.math.BigInteger nbModels()
```
    Returns the number of models of this SDD.
    
    Returns:
    a value equivalent to getAssignments().size().
  - apply
```
public <X> X apply(SDDFunction<X> f)
```
    Applies the specified SDD function on this SDD.
    
    Type Parameters:
    X - the type of object that the function computes.
    Parameters:
    f - the function to apply on this SDD.
    
    Returns:
    the result of f on this SDD.

Class SDD

Method Summary

Methods inherited from class buffer.CanonicalWatched

Methods inherited from class java.lang.Object

Method Detail

create

variable

constant

hashCode

equivalent

getBuffer

destroy

readCNF

getTree

getSDDTree

toString

toDot

toDot

toDot

printBuffer

and

or

or

neg

exists

forall

replace

rightRotationOnRoot

rightRotation

leftRotationOnRoot

leftRotation

swapVnodeOnRoot

getAssignments

getOneAssignment

isConstant

size

isValid

isSat

nbModels

apply