Vtree

class pysdd.sdd.Vtree(var_count=None, var_order=None, vtree_type='balanced', filename=None, is_X_var=None)

Returns a vtree over a given number of variables.

Parameters:

• var_count – Number of variables
• vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”, “balanced”, or “random”.
• var_order – The left-to-right variable ordering is given in array var_order. The contents of array var_order must be a permutation of the integers from 1 to var count.
• is_X_var – The constrained variables X, specified as an array of size var_count+1. For variables i where 1 =< i =< var_count, if is_X_var[i] is 1 then i is an element of X, and if it is 0 then i is not an element of X.
• filename – The name of the file from which to create a vtree.

Returns:

A vtree

count(self)

count_at(self)

dead_count(self)

dead_count_at(self)

dead_size(self)

dead_size_at(self)

dot(self)

Vtree to Graphiv dot string.

static from_file(filename)

Create Vtree from file.

get_sdd_nodes(self, SddManager manager)

List of SDD nodes normalized for vtree.

Only two sdd nodes for leaf vtrees: first is positive literal, second is negative literal.

Parameters:manager – SddManager associated with this Vtree Returns:List of SddNodes

get_sdd_rootnodes(self, SddManager manager)

List of SDD nodes that are a root for the shared SDD.

Parameters:manager – SddManager associated with this Vtree Returns:List of SddNodes

init_vtree_size_limit(self, SddManager manager)

Declares the size s of current SDD for vtree as the reference size for the relative size limit l.

That is, a rotation or swap operation will fail if the SDD size grows to larger than s × l.

is_leaf(self)

Returns 1 if vtree is a leaf node, and 0 otherwise.

is_ref

is_ref: ‘bool’

static is_sub(Vtree vtree1, Vtree vtree2)

Returns 1 if vtree1 is a sub-vtree of vtree2 and 0 otherwise.

static lca(Vtree vtree1, Vtree vtree2, Vtree root)

Returns the lowest common ancestor (lca) of vtree nodes vtree1 and vtree2, assuming that root is a common ancestor of these two nodes.

left(self)

Returns the left child of a vtree node (returns NULL if the vtree is a leaf node).

live_count(self)

live_count_at(self)

live_size(self)

live_size_at(self)

location(self, SddManager manager)

Returns the location of the pointer to the vtree root.

This location can be used to access the new root of the vtree, which may have changed due to rotating some of the vtree nodes.

minimize(self, SddManager manager)

Performs local garbage collection on vtree and then tries to minimize the size of the SDD of vtree by searching for a different vtree. Returns the root of the resulting vtree.

static new_with_X_constrained(var_count, is_X_var, vtree_type)

Returns an X-constrained vtree over a given number of variables (var_count).

Parameters:

• var_count – Number of variables
• is_X_var – The constrained variables X, specified as an array of size var_count+1. For variables i where 1 =< i =< var_count, if is_X_var[i] is 1 then i is an element of X, and if it is 0 then i is not an element of X.
• vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”,

“balanced”, or “random”. :return: an X-constrained vTree

static new_with_var_order(var_count, var_order, vtree_type)

Returns a vtree over a given number of variables (var_count), whose left-to-right variable ordering is given in array var_order.

Parameters:

• var_count – Number of variables
• var_order – The left-to-right variable ordering. The contents of the array must be a permutation of the integers from 1 to var count.
• vtree_type – The type of a vtree may be “right” (right linear), “left” (left linear), “vertical”,

“balanced”, or “random” :return: a vtree ordered according to var_order

parent(self)

Returns the parent of a vtree node (return NULL if the vtree is a root node).

position(self)

Returns the position of a given vtree node in the vtree inorder.

Position indices start at 0.

read(self, char *filename)

Reads a vtree from file.

right(self)

Returns the right child of a vtree node (returns NULL if the vtree is a leaf node).

root(self)

rotate_left(self, SddManager sddmanager, int limited)

Rotates a vtree node left, given time and size limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

rotate_right(self, SddManager sddmanager, int limited)

Rotates a vtree node right, given time, size and cartesian-product limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

save(self, char *filename)

Saves a vtree to file.

save_as_dot(self, char *filename)

size(self)

size_at(self)

swap(self, SddManager sddmanager, int limited)

Swaps the children of a vtree node, given time, size and cartesian-product limits.

Time and size limits, among others, are enforced when limited is set to 1; if limited is set to 0, limits are deactivated. Returns 1 if the operation succeeds and 0 otherwise (i.e., limits exceeded). This operation assumes no dead SDD nodes inside or above vtree and does not introduce any new dead SDD nodes.

A size limit is interpreted using a context which consists of two elements. First, a vtree v which is used to define the live SDD nodes whose size is to be constrained by the limit. Second, an initial size s to be used as a reference point when measuring the amount of size increase. That is, a limit l will constrain the size of live SDD nodes in vtree v to <= l * s.

var(self)

Returns the variable associated with a vtree node.

If the vtree node is a leaf, and returns 0 otherwise.

Returns:variable

var_count(self)

Returns the number of variables contained in the vtree.