pyk.kore.manip module

collect_symbols(pattern: Pattern) → set[str][source]

Return the set of all symbols referred to in a pattern.

Parameters:

pattern – Pattern to collect symbols from.

conjuncts(pattern: Pattern) → tuple[Pattern, ...][source]
elim_aliases(pattern: Pattern) → Pattern[source]

Eliminate subpatterns of the form \and{S}(p, X : S).

Both the \and and instances of X : S are replaced by the definition p.

free_occs(pattern: Pattern, *, bound_vars: Collection[str] = ()) → dict[str, list[EVar]][source]
substitute_vars(pattern: Pattern, subst_map: Mapping[EVar, Pattern]) → Pattern[source]

Substitute variables in a pattern using a bottom-up traversal.

Parameters:

  • pattern – The pattern containing variables to be substituted.

  • subst_map – A mapping from variables to their replacement patterns.