wmpy.core.utils.LiteralNormalizer

class LiteralNormalizer(env)

Bases: object

A helper class for normalizing literals. This class is useful whenever literals involving algebraic atoms are manipulated by an external procedure, such as an SMT-based enumerator.

Methods

known_aliases	Maps back a normalized atom into the original ones (multiple literals might map into the same normalized literal).
normalize	Normalizes 'literal', possibly storing original formula in the alias dictionary.

known_aliases(literal)

Maps back a normalized atom into the original ones (multiple literals might map into the same normalized literal).

Return type:

set[tuple[FNode, bool]]

Returns:

The set of known aliases for a normalized (positive) ‘literal’.

Each alias is a tuple containing: - the original literal - the Boolean flag ‘negative’

normalize(literal, remember_alias=False)

Normalizes ‘literal’, possibly storing original formula in the alias dictionary.

Parameters:

• literal (FNode) – the literal in pysmt format

• remember_alias (bool) – store ‘literal’ as an alias (def: False)

Return type:

tuple[FNode, bool]

Returns:

A normalized atom plus a Boolean that indicates if the normalized literal was negative.