wmpy.core.weights.WeightConverterSkeleton

class WeightConverterSkeleton(env)

Bases: TreeWalker

This internal class implements the conversion of a weight function into a weight skeleton, as described in “Enhancing SMT-based Weighted Model Integration by structure awareness” (Spallitta et al., 2024).

Methods

convert
new_cond_label
set_function	Overrides the default walking function for each of the specified node_types with the given function
set_handler	Associate in cls the given function to the given node_types.
super	Call the correct walk_* function of cls for the given formula.
walk	Generic walk method, will apply the function defined by the map self.functions.
walk_algebraic_constant	Default function for a node that is not handled by the Walker.
walk_and	Default function for a node that is not handled by the Walker.
walk_array_select	Default function for a node that is not handled by the Walker.
walk_array_store	Default function for a node that is not handled by the Walker.
walk_array_value	Default function for a node that is not handled by the Walker.
walk_bool_constant	Default function for a node that is not handled by the Walker.
walk_bv_add	Default function for a node that is not handled by the Walker.
walk_bv_and	Default function for a node that is not handled by the Walker.
walk_bv_ashr	Default function for a node that is not handled by the Walker.
walk_bv_comp	Default function for a node that is not handled by the Walker.
walk_bv_concat	Default function for a node that is not handled by the Walker.
walk_bv_constant	Default function for a node that is not handled by the Walker.
walk_bv_extract	Default function for a node that is not handled by the Walker.
walk_bv_lshl	Default function for a node that is not handled by the Walker.
walk_bv_lshr	Default function for a node that is not handled by the Walker.
walk_bv_mul	Default function for a node that is not handled by the Walker.
walk_bv_neg	Default function for a node that is not handled by the Walker.
walk_bv_not	Default function for a node that is not handled by the Walker.
walk_bv_or	Default function for a node that is not handled by the Walker.
walk_bv_rol	Default function for a node that is not handled by the Walker.
walk_bv_ror	Default function for a node that is not handled by the Walker.
walk_bv_sdiv	Default function for a node that is not handled by the Walker.
walk_bv_sext	Default function for a node that is not handled by the Walker.
walk_bv_sle	Default function for a node that is not handled by the Walker.
walk_bv_slt	Default function for a node that is not handled by the Walker.
walk_bv_srem	Default function for a node that is not handled by the Walker.
walk_bv_sub	Default function for a node that is not handled by the Walker.
walk_bv_tonatural	Default function for a node that is not handled by the Walker.
walk_bv_udiv	Default function for a node that is not handled by the Walker.
walk_bv_ule	Default function for a node that is not handled by the Walker.
walk_bv_ult	Default function for a node that is not handled by the Walker.
walk_bv_urem	Default function for a node that is not handled by the Walker.
walk_bv_xor	Default function for a node that is not handled by the Walker.
walk_bv_zext	Default function for a node that is not handled by the Walker.
walk_div	Default function for a node that is not handled by the Walker.
walk_equals	Default function for a node that is not handled by the Walker.
walk_error	Default function for a node that is not handled by the Walker.
walk_exists	Default function for a node that is not handled by the Walker.
walk_forall	Default function for a node that is not handled by the Walker.
walk_function	Default function for a node that is not handled by the Walker.
walk_iff	Default function for a node that is not handled by the Walker.
walk_implies	Default function for a node that is not handled by the Walker.
walk_int_constant	Default function for a node that is not handled by the Walker.
walk_int_to_str	Default function for a node that is not handled by the Walker.
walk_ite	Default function for a node that is not handled by the Walker.
walk_le	Default function for a node that is not handled by the Walker.
walk_lt	Default function for a node that is not handled by the Walker.
walk_minus	Default function for a node that is not handled by the Walker.
walk_no_conditions
walk_not	Default function for a node that is not handled by the Walker.
walk_operator
walk_or	Default function for a node that is not handled by the Walker.
walk_plus	Default function for a node that is not handled by the Walker.
walk_pow	Default function for a node that is not handled by the Walker.
walk_real_constant	Default function for a node that is not handled by the Walker.
walk_skip	Default function to skip a node and process the children
walk_str_charat	Default function for a node that is not handled by the Walker.
walk_str_concat	Default function for a node that is not handled by the Walker.
walk_str_constant	Default function for a node that is not handled by the Walker.
walk_str_contains	Default function for a node that is not handled by the Walker.
walk_str_indexof	Default function for a node that is not handled by the Walker.
walk_str_length	Default function for a node that is not handled by the Walker.
walk_str_prefixof	Default function for a node that is not handled by the Walker.
walk_str_replace	Default function for a node that is not handled by the Walker.
walk_str_substr	Default function for a node that is not handled by the Walker.
walk_str_suffixof	Default function for a node that is not handled by the Walker.
walk_str_to_int	Default function for a node that is not handled by the Walker.
walk_symbol	Default function for a node that is not handled by the Walker.
walk_threshold
walk_times	Default function for a node that is not handled by the Walker.
walk_toreal	Default function for a node that is not handled by the Walker.

set_function(function, *node_types)

Overrides the default walking function for each of the specified node_types with the given function

classmethod set_handler(function, *node_types)

Associate in cls the given function to the given node_types.

classmethod super(self, formula, *args, **kwargs)

Call the correct walk_* function of cls for the given formula.

walk(formula, threshold=None)

Generic walk method, will apply the function defined by the map self.functions.

If threshold parameter is specified, the walk_threshold function will be called for all nodes with depth >= threshold.

walk_algebraic_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_and(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_select(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_store(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_array_value(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bool_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_bv_add(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_and(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ashr(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_comp(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_concat(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_bv_extract(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshl(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_lshr(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_mul(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_neg(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_not(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_or(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_rol(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ror(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sdiv(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sext(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sle(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_slt(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_srem(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_sub(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_tonatural(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_bv_udiv(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ule(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_ult(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_urem(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_xor(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_bv_zext(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_div(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_equals(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_error(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_exists(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_forall(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_function(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_iff(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_implies(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_int_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_int_to_str(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_ite(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_le(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_lt(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_minus(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_not(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_or(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_plus(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_pow(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_real_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_skip(formula)

Default function to skip a node and process the children

walk_str_charat(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_concat(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_constant(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_str_contains(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_indexof(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_length(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_prefixof(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_replace(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_substr(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_suffixof(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_str_to_int(formula, **kwargs)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

walk_symbol(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

None

walk_times(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]

walk_toreal(formula)

Default function for a node that is not handled by the Walker.

This tries to handle the node using the Dynamic Walker Function information from the environment. If this fails, then an UnsupportedOperatorError exception is given.

Return type:

Generator[FNode, None, None]