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