wmpy.core.weights.WeightAtomsFinder

class WeightAtomsFinder(env=None, invalidate_memoization=False)

Bases: AtomsOracle

TODO

The flag invalidate_memoization can be used to clear the cache after the walk has been completed: the cache is one-time use.

Methods

get_atoms	Returns the set of atoms appearing in the formula.
iter_walk	Performs an iterative walk of the DAG
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
walk_algebraic_constant	Default function for a node that is not handled by the Walker.
walk_all	Returns True if all the children returned True.
walk_and	Default function for a node that is not handled by the Walker.
walk_any	Returns True if any of the children returned True.
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_bool_op
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_constant
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_false	Returns False, independently from the children's value.
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_identity	Returns formula, independently from the childrens's value.
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_none	Returns None, independently from the children's value.
walk_not	Default function for a node that is not handled by the Walker.
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_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_theory_op
walk_theory_relation
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.
walk_true	Returns True, independently from the children's value.

get_atoms(formula)

Returns the set of atoms appearing in the formula.

iter_walk(formula, **kwargs)

Performs an iterative walk of the DAG

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_algebraic_constant(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_all(formula, args, **kwargs)

Returns True if all the children returned True.

walk_and(formula, args, **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_any(formula, args, **kwargs)

Returns True if any of the children returned True.

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, **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_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, **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_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, args, **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.

Return type:

frozenset[FNode]

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, args, **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.

Return type:

frozenset[FNode]

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, args, **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_false(formula, args, **kwargs)

Returns False, independently from the children’s value.

walk_forall(formula, args, **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_identity(formula, **kwargs)

Returns formula, independently from the childrens’s value.

walk_iff(formula, args, **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, args, **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, **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_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, args, **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.

Return type:

frozenset[FNode]

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, args, **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.

Return type:

frozenset[FNode]

walk_none(formula, args, **kwargs)

Returns None, independently from the children’s value.

walk_not(formula, args, **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, args, **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, args, **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.

Return type:

frozenset[FNode]

walk_pow(formula, args, **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.

Return type:

frozenset[FNode]

walk_real_constant(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_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, **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_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, **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_times(formula, args, **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.

Return type:

frozenset[FNode]

walk_toreal(formula, args, **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.

Return type:

frozenset[FNode]

walk_true(formula, args, **kwargs)

Returns True, independently from the children’s value.