pyk.kast.manip module

abstract_term_safely(kast: KInner, base_name: str = 'V', sort: KSort | None = None, existing_var_names: set[str] | None = None) → KVariable

apply_existential_substitutions(state: KInner, constraints: Iterable[KInner]) → tuple[KInner, Iterable[KInner]]

bool_to_ml_pred(kast: KInner) → KInner

build_claim(claim_id: str, init_config: KInner, final_config: KInner, init_constraints: Iterable[KInner] = (), final_constraints: Iterable[KInner] = (), keep_vars: Iterable[str] = ()) → tuple[KClaim, Subst]

Return a KClaim between the supplied initial and final states.

Parameters:

• claim_id – Label to give the claim.

• init_config – State to put on LHS of the rule.

• final_config – State to put on RHS of the rule.

• init_constraints – Constraints to use as requires clause.

• final_constraints – Constraints to use as ensures clause.

• keep_vars – Variables to leave in the side-conditions even if not bound in the configuration.

Returns:

tuple claim: KClaim, var_map: Subst: - claim: A KClaim with variable naming conventions applied so that it should be parseable by K frontend. - var_map: The variable renamings that happened to make the claim parseable by K frontend (which can be undone to recover original variables).

build_rule(rule_id: str, init_config: KInner, final_config: KInner, init_constraints: Iterable[KInner] = (), final_constraints: Iterable[KInner] = (), priority: int | None = None, keep_vars: Iterable[str] = ()) → tuple[KRule, Subst]

Return a KRule between the supplied initial and final states.

Parameters:

• rule_id – Label to give the rule.

• init_config – State to put on LHS of the rule.

• final_config – State to put on RHS of the rule.

• init_constraints – Constraints to use as requires clause.

• final_constraints – Constraints to use as ensures clause.

• priority – Rule priority to give to the generated KRule.

• keep_vars – Variables to leave in the side-conditions even if not bound in the configuration.

Returns:

tuple claim: KRule, var_map: Subst such that: - rule: A KRule with variable naming conventions applied so that it should be parseable by K frontend. - var_map: The variable renamings that happened to make the claim parseable by K frontend (which can be undone to recover original variables).

cell_label_to_var_name(label: str) → str

Return a variable name based on a cell label.

collapse_dots(kast: KInner) → KInner

Given a configuration with structural frames …, minimize the structural frames needed.

• Input: a configuration, potentially with structural frames.

• Output: the same configuration, with the amount of structural framing minimized.

count_vars(term: KInner) → Counter[str]

extract_cells(kast: KInner, keep_cells: Collection[str]) → KInner

extract_lhs(term: KInner) → KInner

extract_rhs(term: KInner) → KInner

extract_subst(term: KInner) → tuple[Subst, KInner]

flatten_label(label: str, kast: KInner) → list[KInner]

Given a cons list, return a flat Python list of the elements.

• Input: Cons operation to flatten.

• Output: Items of cons list.

free_vars(kast: KInner) → frozenset[str]

if_ktype(ktype: type[KI], then: Callable[[KI], KInner]) → Callable[[KInner], KInner]

indexed_rewrite(kast: KInner, rewrites: Iterable[KRewrite]) → KInner

inline_cell_maps(kast: KInner) → KInner

Ensure that cell map collections are printed nicely, not as Maps.”

• Input: kast term.

• Output: kast term with cell maps inlined.

is_anon_var(kast: KInner) → bool

is_term_like(kast: KInner) → bool

labels_to_dots(kast: KInner, labels: Collection[str]) → KInner

Abstract specific labels for printing.

• Input: kast term, and list of labels to abstract.

• Output: kast term with those labels abstracted.

minimize_rule(rule: RL, keep_vars: Iterable[str] = ()) → RL

Minimize a K rule or claim for pretty-printing.

• Input: kast representing a K rule or claim.

• Output: kast with the rule or claim minimized: - Variables only used once will be removed. - Unused cells will be abstracted. - Attempt to remove useless side-conditions.

minimize_term(term: KInner, keep_vars: Iterable[str] = (), abstract_labels: Collection[str] = (), keep_cells: Collection[str] = ()) → KInner

Minimize a K term for pretty-printing.

• Input: kast term, and optionally requires and ensures clauses with constraints.

• Output: kast term minimized. - Variables only used once will be removed. - Unused cells will be abstracted. - Attempt to remove useless conditions.

ml_pred_to_bool(kast: KInner, unsafe: bool = False) → KInner

no_cell_rewrite_to_dots(term: KInner) → KInner

Transforms a given term by replacing the contents of each cell with dots if the LHS and RHS are the same.

This function recursively traverses the cells in a term. When it finds a cell whose left-hand side (LHS) is identical to its right-hand side (RHS), it replaces the cell’s contents with a predefined DOTS.

Parameters: - term (KInner): The term to be transformed.

Returns: - KInner: The transformed term, where specific cell contents have been replaced with dots.

on_attributes(kast: W, f: Callable[[KAtt], KAtt]) → W

propagate_up_constraints(k: KInner) → KInner

push_down_rewrites(kast: KInner) → KInner

remove_attrs(term: KInner) → KInner

remove_generated_cells(term: KInner) → KInner

Remove <generatedTop> and <generatedCounter> from a configuration.

• Input: Constrained term.

• Output: Constrained term with those cells removed.

remove_semantic_casts(kast: KInner) → KInner

Remove injected #SemanticCast* nodes in AST.

• Input: kast (possibly) containing automatically injected #SemanticCast* KApply nodes.

• Output: kast without the #SemanticCast* nodes.

remove_source_map(definition: KDefinition) → KDefinition

remove_useless_constraints(constraints: Iterable[KInner], initial_vars: Iterable[str]) → list[KInner]

Given a list of constraints and a list of variables, return an updated list with only constraints that depend on these variables (directly or indirectly).

Parameters:

• constraints – Original list of constraints to remove from.

• initial_vars – Initial list of variables to keep constraints for.

Returns:

A list of constraints with only those constraints that contain the initial variables or variables that depend on those through other constraints in the list.

rename_generated_vars(term: KInner) → KInner

replace_rewrites_with_implies(kast: KInner) → KInner

set_cell(constrained_term: KInner, cell_variable: str, cell_value: KInner) → KInner

simplify_bool(k: KInner) → KInner

sort_ac_collections(kast: KInner) → KInner

sort_assoc_label(label: str, kast: KInner) → KInner

split_config_and_constraints(kast: KInner) → tuple[KInner, KInner]

split_config_from(configuration: KInner) → tuple[KInner, dict[str, KInner]]

Split the substitution from a given configuration.

Given an input configuration config, will return a tuple (symbolic_config, subst), where:

1. config == substitute(symbolic_config, subst)

2. symbolic_config is the same configuration structure, but where the contents of leaf cells is replaced with a fresh KVariable.

3. subst is the substitution for the generated KVariables back to the original configuration contents.

undo_aliases(definition: KDefinition, kast: KInner) → KInner

useless_vars_to_dots(kast: KInner, keep_vars: Iterable[str] = ()) → KInner

Structurally abstract away useless variables.

• Input: kast term, and a requires clause and ensures clause.

• Output: kast term with the useless vars structurally abstracted.