SddNode

class pysdd.sdd.SddNode
bit
condition
conjoin
copy

Returns a copy of an SDD, with respect to a new manager dest manager.

The destination manager, and the manager associated with the SDD to be copied, must have copies of the same vtree.

count

Returns the node count of an SDD (rooted at node).

deref

Dereferences an SDD node if it is not a terminal node.

Returns the node. The number of dereferences to a node cannot be larger than the number of its references (except for terminal SDD nodes, for which referencing and dereferencing has no effect).

disjoin
dot
elements

Returns an array containing the elements of an SDD node.

Returns:A list of pairs [(prime, sub)]

Internal working: If the node has m elements, the array will be of size 2m, with primes appearing at locations 0, 2, … , 2m − 2 and their corresponding subs appearing at locations 1, 3, … , 2m − 1. Assumes that sdd node is decision(node) returns 1. Moreover, the returned array should not be freed.

equiv
garbage_collected

Returns true if the SDD node with the given ID has been garbage collected; returns false otherwise.

This function may be helpful for debugging.

global_model_count
id

Unique id of the SDD node.

Every SDD node has an ID. When an SDD node is garbage collected, its structure is not freed but inserted into a gc-list. Moreover, this structure may be reused later by another, newly created SDD node, which will have its own new ID.

Returns:id
is_decision

The node is a decision node.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_false

The node is a node representing false.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_literal

The node is a literal.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

is_true

The node is a node representing true.

A functions that is useful for navigating the structure of an SDD (i.e., visiting all its nodes).

literal

Returns the signed integer (i.e., variable index or the negation of a variable index) of an SDD node representing a literal. Assumes that sdd node is literal(node) returns 1.

model_count
models

A generator for the models of an SDD.

negate
node_size

Returns the size of an SDD node (the number of its elements).

Recall that the size is zero for terminal nodes (i.e., non-decision nodes).

print_ptr
ref

References an SDD node if it is not a terminal node.

Returns the node.

ref_count

Returns the reference count of an SDD node.

The reference count of a terminal SDD is 0 (terminal SDDs are always live).

save
save_as_dot
set_bit
size

Returns the size of an SDD (rooted at node).

vtree

Returns the vtree of an SDD node.

vtree2

Returns the vtree of an SDD node.

vtree_next
wmc

Create a WmcManager to perform Weighted Model Counting with this node as root.

Parameters:log_mode – Perform the computations in log mode or not (default = True)