SddNode

class pysdd.sdd.SddNode

bit(self)

condition(node, lit)

conjoin(self, SddNode other)

copy(self, SddManager manager=None)

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(self)

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

deref(self)

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(self, SddNode other)

dot(self)

elements(self)

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(left, SddNode right)

garbage_collected(self)

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(self)

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(self)

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(self)

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(self)

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(self)

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(self)

models(self, Vtree vtree=None)

A generator for the models of an SDD.

negate(self)

node_size(self)

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(self)

ref(self)

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

Returns the node.

ref_count(self)

Returns the reference count of an SDD node.

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

save(self, char *filename)

save_as_dot(self, char *filename)

set_bit(self, int bit)

size(self)

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

vtree(self)

Returns the vtree of an SDD node.

vtree2(self)

Returns the vtree of an SDD node.

vtree_next(self)

wmc(self, log_mode=True)

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)