wmpy.enumeration.sae.AssignmentExtractor

class AssignmentExtractor(env)

Bases: TreeWalker

Extracts forced literals from a formula.

A forced literal is a literal that must be true for the formula to be satisfied. Such literals are found recursively in the formula structure: - If the formula is a conjunction, all literals in the conjunction are forced. - If the formula is a negated disjunction, all literals in the disjunction are forced with a negated value.

Methods

extract	Extracts the assignment of forced literals from a formula.
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_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_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_term
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.

extract(formula)

Extracts the assignment of forced literals from a formula.

Parameters:

formula (FNode) – The formula to extract the assignment from.

Returns:

• A dictionary with forced literals as keys and their truth values as values.

• A boolean indicating whether the formula is convex (i.e., can be expressed as a conjunction of literals).

Return type:

A tuple containing

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, **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_and(node)

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_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(node)

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, **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, **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_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, **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_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(node)

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_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, **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_le(node)

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_lt(node)

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_minus(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_not(node)

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_or(node)

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_plus(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_pow(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_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_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, **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(node)

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, **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_toreal(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.