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¶ Returns the node count (live+dead) of all SDD nodes in the vtree.
Returns: count
-
count_at¶ Returns the node count of all SDD nodes normalized for a vtree node (the root where this Vtree points at).
For example, Vtree.size(vtree) returns the sum of Vtree.size_at(v) where v ranges over all nodes of vtree.
Returns: size
-
dead_count¶ Returns the node count (dead only) of all SDD nodes in the vtree.
Returns: count
-
dead_count_at¶
-
dead_size¶ Returns the size (dead only) of all SDD nodes in the vtree.
Returns: size
-
dead_size_at¶
-
dot¶ Vtree to Graphiv dot string.
-
from_file¶ Create Vtree from file.
-
get_sdd_nodes¶ 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¶ 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¶ 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¶ Returns 1 if vtree is a leaf node, and 0 otherwise.
-
is_ref¶ is_ref: ‘bool’
-
is_sub¶ Returns 1 if vtree1 is a sub-vtree of vtree2 and 0 otherwise.
-
lca¶ Returns the lowest common ancestor (lca) of vtree nodes vtree1 and vtree2, assuming that root is a common ancestor of these two nodes.
-
left¶ Returns the left child of a vtree node (returns NULL if the vtree is a leaf node).
-
live_count¶ Returns the node count (live only) of all SDD nodes in the vtree.
Returns: count
-
live_count_at¶
-
live_size¶ Returns the size (live only) of all SDD nodes in the vtree.
Returns: size
-
live_size_at¶
-
location¶ 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¶ 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.
-
new_with_X_constrained¶ 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
-
new_with_var_order¶ 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¶ Returns the parent of a vtree node (return NULL if the vtree is a root node).
-
position¶ Returns the position of a given vtree node in the vtree inorder.
Position indices start at 0.
-
read¶ Reads a vtree from file.
-
right¶ Returns the right child of a vtree node (returns NULL if the vtree is a leaf node).
-
root¶
-
rotate_left¶ 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¶ 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¶ Saves a vtree to file.
-
save_as_dot¶
-
size¶ Returns the size (live+dead) of all SDD nodes in the vtree.
Returns: size
-
size_at¶ Returns the size of all SDD nodes normalized for a vtree node (the root where this Vtree points at).
For example, Vtree.size(vtree) returns the sum of Vtree.size_at(v) where v ranges over all nodes of vtree.
Returns: size
-
swap¶ 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¶ Returns the variable associated with a vtree node.
If the vtree node is a leaf, and returns 0 otherwise.
Returns: variable
-
var_count¶ Returns the number of variables contained in the vtree.