Index

A

ABORTED (FallbackReason attribute) (StopReason attribute) AbortedResult (class in pyk.kore.rpc) abs_or_rel_to() (in module pyk.utils) Abstract (class in pyk.kcfg.kcfg) abstract_node() (DefaultSemantics method) (KCFGSemantics method) abstract_term_safely() (in module pyk.kast.manip) action_keystroke() (KCFGViewer method) add_alias() (KCFG method) add_attr() (KCFG method) (KCFG.Node method) add_bounded() (APRProof method) add_cell_map_items() (KDefinition method) add_command() (BugReport method) add_constraint() (CSubst method) (CTerm method) add_exec_time() (APRProof method) add_file() (BugReport method) add_file_contents() (BugReport method) add_indent() (in module pyk.utils) add_injections() (KompiledKore method) add_ksequence_under_k_productions() (KDefinition method) add_module() (KoreClient method) add_node() (KCFG method) add_sort_params() (KDefinition method) add_stuck() (KCFG method) add_subproof() (Proof method) add_successor() (KCFG method) add_terminal() (KCFGExploration method) add_vacuous() (KCFG method) admit() (Proof method) admitted (APRSummary attribute) (EqualitySummary attribute) (Proof attribute) advance_proof() (Prover method) ahead (KVersion.Git attribute) alias (AliasDecl attribute) ALIAS (Atts attribute) Alias (class in pyk.kast.outer_syntax) alias (KAs attribute) alias_decl() (KoreParser method) ALIAS_REC (Atts attribute) alias_rules (KDefinition property) AliasDecl (class in pyk.kore.syntax) aliases() (KCFG method) all_files (Project property) all_module_names (KDefinition property) all_modules (KDefinition attribute) all_modules_dict (KDefinition property) always_check_subsumption (APRProver attribute) And (class in pyk.kast.markdown) (class in pyk.kore.syntax) and_bool() (in module pyk.kore.prelude) andBool() (in module pyk.prelude.kbool) andd() (KoreParser method) antecedent (ImpliesProof attribute) anti_unify() (CTerm method) (in module pyk.cterm.cterm) AnyType (class in pyk.kast.att) ANYWHERE (Atts attribute) app (Assoc attribute) App (class in pyk.kore.syntax) app (LeftAssoc attribute) (RightAssoc attribute) app() (in module pyk.kore.match) (KoreParser method) apply() (CSubst method) (KLabel method) (KRewrite method) (Subst method) apply_existential_substitutions() (in module pyk.kast.manip) apply_top() (KRewrite method) APRFailureInfo (class in pyk.proof.reachability) APRProof (class in pyk.proof.reachability) APRProofBehaviorView (class in pyk.proof.tui) APRProofBoundedResult (class in pyk.proof.reachability) APRProofExtendResult (class in pyk.proof.reachability) APRProofNodePrinter (class in pyk.proof.show)

APRProofResult (class in pyk.proof.reachability) APRProofShow (class in pyk.proof.show) APRProofSubsumeResult (class in pyk.proof.reachability) APRProofTerminalResult (class in pyk.proof.reachability) APRProofViewer (class in pyk.proof.tui) APRProver (class in pyk.proof.reachability) APRSummary (class in pyk.proof.reachability) arg() (in module pyk.kore.match) args (App attribute) (KApply attribute) (KompileBackend property) (Sort attribute) (SortDecl attribute) (Target attribute) args() (in module pyk.kore.match) argument_sorts (KProduction property) argument_sorts() (KDefinition method) arity (KApply property) (KSequence property) as_rule() (APRProof method) as_subsort (KProduction property) ASSOC (Atts attribute) Assoc (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) assoc (KSyntaxAssociativity attribute) (PriorityBlock attribute) (SyntaxAssoc attribute) assoc_with_unit() (in module pyk.kast.pretty) assume_defined() (CTermSymbolic method) AST (class in pyk.kast.outer_syntax) Atom (class in pyk.kast.markdown) att (Alias attribute) (Claim attribute) Att (class in pyk.kast.outer_syntax) att (Config attribute) (Context attribute) (KBubble attribute) (KClaim attribute) (KContext attribute) (KDefinition attribute) (KFlatModule attribute) (KProduction attribute) (KRule attribute) (KSortSynonym attribute) (KSyntaxAssociativity attribute) (KSyntaxLexical attribute) (KSyntaxPriority attribute) (KSyntaxSort attribute) (Module attribute) (Production attribute) (ProductionLike attribute) (Rule attribute) (StringSentence attribute) (SyntaxDecl attribute) (SyntaxSynonym attribute) (UserList attribute) (WithKAtt attribute) AttEntry (class in pyk.kast.att) AttKey (class in pyk.kast.att) ATTR (State attribute) ATTR_CONTENT (TokenType attribute) ATTR_KEY (TokenType attribute) attrs (AliasDecl attribute) (Axiom attribute) (Claim attribute) (Definition attribute) (Import attribute) (KCFG.Node attribute) (Module attribute) (SortDecl attribute) (SymbolDecl attribute) (WithAttrs attribute) Atts (class in pyk.kast.att) atts (KAtt attribute) AttType (class in pyk.kast.att) Axiom (class in pyk.kore.syntax) axiom() (KoreParser method) AxiomLike (class in pyk.kore.syntax) axioms (Module property)

B

backend (KPrint attribute) BaseRepl (class in pyk.krepl.repl) BehaviorView (class in pyk.kcfg.tui) BehaviorView.Selected (class in pyk.kcfg.tui) BINARY (KAstInput attribute) (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) BinaryConn (class in pyk.kore.syntax) BinaryPred (class in pyk.kore.syntax) bind_universally (ImpliesProof attribute) BINDINGS (KCFGViewer attribute) (NavWidget attribute) blocks (SyntaxDefn attribute) bmc_depth (APRProof attribute) (APRSummary attribute) body (KClaim attribute) (KContext attribute) (KRule attribute) (KRuleLike attribute) bool_dv() (in module pyk.kore.prelude) bool_to_ml_pred() (in module pyk.kast.manip) boolToken() (in module pyk.prelude.kbool) BOOSTER (LogOrigin attribute) BoosterServer (class in pyk.kore.rpc) BoosterServerArgs (class in pyk.kore.rpc) Bottom (class in pyk.kore.syntax) bottom() (CTerm static method) (KoreParser method) bottom_up() (in module pyk.kast.inner) (Pattern method) bottom_up_with_summary() (in module pyk.kast.inner)

bounded (APRProof property) (APRSummary attribute) BRACKET (Atts attribute) Branch (class in pyk.kcfg.kcfg) BRANCHING (FallbackReason attribute) (StopReason attribute) BranchingResult (class in pyk.kore.rpc) bubble (Alias attribute) (BehaviorView.Selected attribute) (Claim attribute) (Config attribute) (Context attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) (Rule attribute) BUBBLE (State attribute) bubble (StringSentence attribute) BUBBLE (TokenType attribute) bug_report (BoosterServerArgs attribute) (KoreServerArgs attribute) bug_report() (in module pyk.testing.plugin) BugReport (class in pyk.utils) build() (Target method) build_assoc() (in module pyk.kast.inner) build_claim() (in module pyk.kast.manip) build_cons() (in module pyk.kast.inner) build_rule() (in module pyk.kast.manip) build_rule_dict() (in module pyk.kore_exec_covr.kore_exec_covr) build_symbol_table() (in module pyk.kast.pretty) bytes_decode() (in module pyk.dequote) bytes_dv() (in module pyk.kore.prelude) bytes_encode() (in module pyk.dequote) bytesToken() (in module pyk.prelude.bytes) bytesToken_from_str() (in module pyk.prelude.bytes)

C

can_focus (APRProofBehaviorView attribute) (BehaviorView attribute) (Constraint attribute) (Custom attribute) (GraphChunk attribute) (Info attribute) (NavWidget attribute) (NodeView attribute) (Status attribute) (Term attribute) can_focus_children (APRProofBehaviorView attribute) (BehaviorView attribute) (Constraint attribute) (Custom attribute) (GraphChunk attribute) (Info attribute) (NavWidget attribute) (NodeView attribute) (Status attribute) (Term attribute) can_progress (APRProof property) (ImpliesProof property) (Proof property) case() (in module pyk.utils) case_symbol() (in module pyk.kore.match) CAT_BUILTIN (BaseRepl attribute) CAT_DEBUG (BaseRepl attribute) Ceil (class in pyk.kore.syntax) ceil() (KoreParser method) CELL (Atts attribute) cell() (CTerm method) CELL_COLLECTION (Atts attribute) cell_collection_productions (KDefinition property) (KFlatModule property) CELL_FRAGMENT (Atts attribute) cell_label_to_var_name() (in module pyk.kast.manip) CELL_NAME (Atts attribute) CELL_OPT_ABSENT (Atts attribute) cells (CTerm property) Chainable (class in pyk.utils) check_absolute_path() (in module pyk.utils) check_dir_path() (in module pyk.utils) check_extendable() (KCFGExplore method) check_file_path() (in module pyk.utils) check_relative_path() (in module pyk.utils) check_type() (in module pyk.utils) chunk_id (GraphChunk.Selected attribute) circularities_module_name (APRProver attribute) circularity (APRProof attribute) CIRCULARITY (Atts attribute) Claim (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) claim() (KoreParser method) claims (KFlatModule property) close() (HttpTransport method) (JsonRpcClient method) (JsonRpcClientFacade method) (KoreClient method) (KoreServer method) (KoreServerPool method) (SingleSocketTransport method) (Transport method) code (CodeBlock attribute) (DefaultError attribute) code_blocks() (in module pyk.kast.markdown) CodeBlock (class in pyk.kast.markdown) collapse_dots() (in module pyk.kast.manip) collect() (in module pyk.kast.inner) COLON (TokenType attribute), [1] COLOR (Atts attribute) COLORS (Atts attribute) COMM (Atts attribute) COMMA (TokenType attribute), [1] command (BoosterServerArgs attribute) (KoreServerArgs attribute) (KRun attribute) command() (HttpTransport method) (SingleSocketTransport method) (Transport method) commit() (APRProof method) (ImpliesProof method) (Proof method) (Prover method) compare_short_hashes() (in module pyk.utils) compile_kllvm() (in module pyk.kllvm.compiler) compile_runtime() (in module pyk.kllvm.compiler) compose() (APRProofBehaviorView method) (APRProofViewer method) (BehaviorView method) (Info method) (KCFGViewer method) (NavWidget method) (NodeView method) (Subst method)

CompositeSummary (class in pyk.proof.proof) CONCAT (Atts attribute) Config (class in pyk.kast.outer_syntax) config (CTerm attribute) conjuncts() (in module pyk.kore.manip) consequent (ImpliesProof attribute) Constraint (class in pyk.kcfg.tui) constraint (CSubst property) (EqualityProof property) constraints (Branch attribute) (CSubst attribute) (CTerm attribute) (EqualityProof property) construct_node_refutation() (APRProof method) CONSTRUCTOR (Atts attribute) constructors (KDefinition property) (KFlatModule property) contains_cover() (KCFG method) contains_edge() (KCFG method) contains_ndbranch() (KCFG method) contains_node() (KCFG method) contains_split() (KCFG method) content (KBubble attribute) Context (class in pyk.kast.outer_syntax) context (ImplicationError attribute) (InvalidModuleError attribute) (PatternError attribute) CONTEXT (State attribute) context() (Target method) count_lines_covered() (in module pyk.kcovr) count_lines_file() (in module pyk.kcovr) count_lines_global() (in module pyk.kcovr) count_rules_covered() (in module pyk.kcovr) count_vars() (in module pyk.kast.manip) counterexample_info (APRProver attribute) cover() (KCFG method) covered (KCFG property) covers (KCFG.Split property) covers() (KCFG method) create_cover() (KCFG method) create_cover_map() (in module pyk.kcovr) create_edge() (KCFG method) create_ndbranch() (KCFG method) create_node() (KCFG method) create_rule_map() (in module pyk.kcovr) create_rule_map_by_file() (in module pyk.kcovr) create_rule_map_by_line() (in module pyk.kcovr) create_split() (KCFG method) create_temp() (KBuildEnv static method) CSS_PATH (KCFGViewer attribute) csubst (APRProofSubsumeResult attribute) CSubst (class in pyk.cterm.cterm) csubst (CTermImplies attribute) (ImpliesProof attribute) (ImpliesProofResult attribute) (KCFG.Cover attribute) cterm (Abstract attribute) CTerm (class in pyk.cterm.cterm) cterm (KCFG.Node attribute) (Step attribute) cterm_build_claim() (in module pyk.cterm.cterm) cterm_build_rule() (in module pyk.cterm.cterm) cterm_symbolic (KCFGExplore attribute) cterm_symbolic() (in module pyk.cterm.symbolic) CTermExecute (class in pyk.cterm.symbolic) CTermImplies (class in pyk.cterm.symbolic) cterms (NDBranch attribute) CTermSMTError CTermSymbolic (class in pyk.cterm.symbolic) ctor_patterns (Assoc property) (DV property) (MLFixpoint property) (MLPattern property) (MLQuant property) Custom (class in pyk.kcfg.tui) cut (Step attribute) CUT_POINT_RULE (StopReason attribute) cut_point_rules (APRProver attribute) CutPointResult (class in pyk.kore.rpc) cwd() (in module pyk.kdist.utils)

D

data (DefaultError attribute) DCOLONEQ (TokenType attribute) DEBUG_APPLIED_REWRITE_RULES (HaskellLogEntry attribute) DEBUG_APPLY_EQUATION (HaskellLogEntry attribute) decl (SyntaxDecl attribute) (SyntaxDefn attribute) deconstruct_short_hash() (in module pyk.utils) DEFAULT (State attribute) default_format (KProduction property) DefaultError DefaultSemantics (class in pyk.kcfg.semantics) Definition (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) definition (KPrint property) (PrettyPrinter attribute) definition() (KoreParser method) (OuterParser method) definition_dir (KInterpreter attribute) (KPrint attribute) (KState attribute) definition_dir() (KBuild method) definition_hash (KPrint property) dependencies (KClaim property) (Project attribute) dependencies_module_name (APRProver attribute) DEPENDS (Atts attribute) deps() (Target method) depth (AbortedResult attribute) (BranchingResult attribute) (CTermExecute attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (KCFG.Edge attribute) (Step attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute)

DEPTH_BOUND (StopReason attribute) DepthBoundResult (class in pyk.kore.rpc) dequote_bytes() (in module pyk.dequote) dequote_string() (in module pyk.dequote) dequoted() (in module pyk.dequote) description() (HttpTransport method) (SingleSocketTransport method) (Transport method) deserialize() (Runtime method) dict (APRProof property) (EqualityProof property) (ImpliesProof property) (Pattern property) (Proof property) (RefutationProof property) (Sort property) (SortApp property) (SortVar property) DIGEST (Atts attribute) digest (Proof property) dirty (KVersion.Git attribute) discard() (KAtt method) discard_attr() (KCFG method) (KCFG.Node method) discard_stuck() (KCFG method) discard_vacuous() (KCFG method) do_load() (BaseRepl method) (KRepl method) do_show() (BaseRepl method) do_step() (BaseRepl method) dot() (APRProofShow method) (KCFGShow method) drop_source() (KAtt method) dump() (APRProofShow method) (KCFGShow method) DuplicateModuleError DV (class in pyk.kore.syntax) dv() (in module pyk.kore.prelude) (KoreParser method)

E

edge() (KCFG method) edge_likes() (KCFG method) edges (KCFG.NDBranch property) edges() (KCFG method) elem_var() (KoreParser method) ELEMENT (Atts attribute) empty_config() (KDefinition method) enquote_bytes() (in module pyk.dequote) enquote_string() (in module pyk.dequote) enquoted() (in module pyk.dequote) ensure_dir_path() (in module pyk.utils) ensures (KClaim attribute) (KRule attribute) (KRuleLike attribute) entries() (KAtt method) eof (KoreParser property) EOF (TokenType attribute), [1] EQ (TokenType attribute) eq_bool() (in module pyk.kore.prelude) eq_int() (in module pyk.kore.prelude) eqInt() (in module pyk.prelude.kint) equality (EqualityProof property) EqualityProof (class in pyk.proof.implies) EqualitySummary (class in pyk.proof.implies) Equals (class in pyk.kore.syntax) equals() (KoreParser method) error (ImplicationError attribute) (InvalidModuleError attribute) (ParseError attribute) (PatternError attribute) (SmtSolverError attribute)

error_info (APRProof attribute) eval() (And method) (Atom method) (Not method) (Or method) (Selector method) EVar (class in pyk.kore.syntax) exec() (ProofStep method) exec_time (APRProof property) execute() (CTermSymbolic method) (KoreClient method) execute_depth (APRProver attribute) ExecuteResult (class in pyk.kore.rpc) Exists (class in pyk.kore.syntax) exists() (KoreParser method) exit_with_process_error() (in module pyk.utils) explorable (KCFGExploration property) extend() (KCFG method) extend_cterm() (KCFGExplore method) extend_result (APRProofExtendResult attribute) extract_branches() (DefaultSemantics method) (KCFGSemantics method) extract_cells() (in module pyk.kast.manip) extract_lhs() (in module pyk.kast.manip) extract_rhs() (in module pyk.kast.manip) extract_subst() (in module pyk.kast.manip)

F

failed (Proof property) FAILED (ProofStatus attribute) failing (APRProof property) (APRSummary attribute) failing_cells (CTermImplies attribute) failing_nodes (APRFailureInfo attribute) failure_info (Proof attribute) failure_info() (APRProver method) (ImpliesProver method) (Prover method) failure_reasons (APRFailureInfo attribute) FailureInfo (class in pyk.proof.proof) fallback_on (BoosterServerArgs attribute) FallbackReason (class in pyk.kore.rpc) fast_check_subsumption (APRProver attribute) fetch_subproof() (Proof method) fetch_subproof_data() (Proof method) files_for_path() (in module pyk.kdist.utils) filter_none() (in module pyk.utils) find_common_items() (in module pyk.utils) find_file_upwards() (in module pyk.kbuild.utils) flatten_label() (in module pyk.kast.manip) Floor (class in pyk.kore.syntax) floor() (KoreParser method) follow_regex (KRegexTerminal attribute) for_definition() (KompiledKore static method) (KoreSortTable static method) (KoreSymbolTable static method) Forall (class in pyk.kore.syntax) forall() (KoreParser method) FORMAT (Atts attribute) Format (class in pyk.kast.att) formatted_exec_time (APRSummary attribute) formatted_exec_time() (APRProof method) FormatType (class in pyk.kast.att) free_occs() (in module pyk.kore.manip) free_vars (CTerm property) (KCFG.Node property) free_vars() (in module pyk.kast.manip) FRESH_GENERATOR (Atts attribute) from_claim() (APRProof static method) (EqualityProof static method) (KCFG static method) from_dict() (AbortedResult class method) (AnyType method) (APRProof class method) (AttType method) (BranchingResult class method) (CSubst static method) (CTerm static method) (CutPointResult class method) (DepthBoundResult class method) (EqualityProof class method) (ExecuteResult class method) (FormatType method) (GetModelResult static method) (ImpliesProof class method) (ImpliesResult static method) (IntType method) (KAtt class method) (KCFG static method) (KCFG.Cover static method) (KCFG.Edge static method) (KCFG.NDBranch static method) (KCFG.Node static method) (KCFG.Split static method) (KCFG.Successor static method) (KCFGExploration static method) (KDefinition static method) (KFlatModule static method) (KFlatModuleList static method) (KImport static method) (KInner static method) (KLabel static method) (KompiledKore static method) (KProductionItem static method) (KRequire static method) (KSentence static method) (KSort static method) (LocationType method) (LogEntry class method) (LogRewrite class method) (LogSimplification class method) (NoneType method) (OptionalType method) (PathType method) (Pattern static method) (Proof class method) (RefutationProof class method) (RewriteFailure class method) (RewriteResult class method) (RewriteSuccess class method) (Sort static method) (Source static method) (State static method) (StrType method) (StuckResult class method) (Subst static method) (TerminalResult class method) (TimeoutResult class method) (VacuousResult class method)

from_json() (KCFG static method) (KInner static method) (Pattern static method) (Sort static method) from_kast() (CTerm static method) from_pred() (Subst static method) from_proof() (APRFailureInfo static method) from_spec_modules() (APRProof static method) FrozenDict (class in pyk.utils) full_name (TargetId property) full_printer (NodePrinter attribute) FUNCTION (Atts attribute) FUNCTIONAL (Atts attribute) functions (KDefinition property) (KFlatModule property)

G

ge_int() (in module pyk.kore.prelude) geInt() (in module pyk.prelude.kint) gen_file_timestamp() (in module pyk.utils) gen_glr_parser() (in module pyk.ktool.kprint) generated_counter() (in module pyk.kore.prelude) generated_top() (in module pyk.kore.prelude) get() (KAtt method) get_claim_modules() (KProve method) get_claims() (KProve method) get_model() (CTermSymbolic method) (KoreClient method) get_node() (KCFG method)

get_refutation_id() (APRProof method) get_rule_by_id() (in module pyk.coverage) get_target() (Project method) GetModelResult (class in pyk.kore.rpc) git (KVersion attribute) GraphChunk (class in pyk.kcfg.tui) GraphChunk.Selected (class in pyk.kcfg.tui) greatest_common_subsort() (KDefinition method) GROUP (Atts attribute) groups (SyntaxPriority attribute) GT (TokenType attribute) gt_int() (in module pyk.kore.prelude) gtInt() (in module pyk.prelude.kint)

H

handler_name (BehaviorView.Selected attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) HAS_DOMAIN_VALUES (Atts attribute) hash (CTerm property) (KAst property) hash_file() (in module pyk.utils) hash_str() (in module pyk.utils) HASKELL (KompileBackend attribute) haskell_log_entries (BoosterServerArgs attribute) (KoreServerArgs attribute) haskell_log_format (BoosterServerArgs attribute) (KoreServerArgs attribute)

HaskellLogEntry (class in pyk.kore_exec_covr.kore_exec_covr) heuristic (Branch attribute) hide_cells() (KCFGShow static method) HOOK (Atts attribute) hooked (SortDecl attribute) (SymbolDecl attribute) hooked_sort_decl() (KoreParser method) hooked_symbol_decl() (KoreParser method) host (KoreServer property) (KoreServerInfo attribute) HTTP (TransportType attribute) HttpTransport (class in pyk.kore.rpc)

I

id (APRSummary attribute) Id (class in pyk.kore.syntax) id (EqualitySummary attribute) (KCFG.Node attribute) (KCFGExplore attribute) (Proof attribute) (ProofSummary attribute) (RefutationSummary attribute) ID (TokenType attribute) id() (KoreParser method) ID_LOWER (TokenType attribute) ID_UPPER (TokenType attribute) IDEM (Atts attribute) if_ktype() (in module pyk.kast.manip) Iff (class in pyk.kore.syntax) iff() (KoreParser method) image (POSet attribute) implication (ImpliesResult attribute) implication_failure_reason() (KCFGExplore method) ImplicationError Implies (class in pyk.kore.syntax) implies() (CTermSymbolic method) (KoreClient method) (KoreParser method) implies_bool() (in module pyk.kore.prelude) impliesBool() (in module pyk.prelude.kbool) ImpliesProof (class in pyk.proof.implies) ImpliesProofResult (class in pyk.proof.implies) ImpliesProver (class in pyk.proof.implies) ImpliesResult (class in pyk.kore.rpc) Import (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) import_from_file() (in module pyk.kllvm.importer) import_kllvm() (in module pyk.kllvm.importer) import_runtime() (in module pyk.kllvm.importer) imports (KFlatModule attribute) (Module attribute) importt() (KoreParser method) (OuterParser method) IMPURE (Atts attribute) In (class in pyk.kore.syntax) indent() (in module pyk.kast.pretty) INDEX (Atts attribute) indexed_rewrite() (in module pyk.kast.manip) infer_sort() (KoreSymbolTable method) Info (class in pyk.kcfg.tui) info (CodeBlock attribute) init (APRProof attribute) init_config() (KDefinition method) init_generated_top_cell() (in module pyk.kore.prelude) init_state() (Interpreter method) (KInterpreter method)

INITIALIZER (Atts attribute) inj() (in module pyk.kore.match) (in module pyk.kore.prelude) INJECTIVE (Atts attribute) inline_cell_maps() (in module pyk.kast.manip) inn() (KoreParser method) instantiate_cell_vars() (KDefinition method) int_dv() (in module pyk.kore.prelude) interim_simplification (BoosterServerArgs attribute) interpreter (BaseRepl attribute) Interpreter (class in pyk.krepl.repl) intersperse() (in module pyk.utils) intro (KRepl attribute) intToken() (in module pyk.prelude.kint) IntType (class in pyk.kast.att) InvalidModuleError is_anon_var() (in module pyk.kast.manip) is_bottom (CTerm property) is_bottom() (in module pyk.prelude.ml) is_bounded() (APRProof method) is_cell (KApply property) is_circularity (KClaim property) is_covered() (KCFG method) is_explorable() (KCFGExploration method) is_failing() (APRProof method) is_hash() (in module pyk.utils) is_hexstring() (in module pyk.utils) is_identity (Subst property) is_init() (APRProof method) is_leaf() (KCFG method) is_ndbranch() (KCFG method) is_pending() (APRProof method) is_prefix (KProduction property) is_record (KProduction property) is_refuted() (APRProof method) is_relative_to() (in module pyk.utils) is_root() (KCFG method) is_split() (KCFG method) is_stuck() (KCFG method) is_subsort() (KoreSortTable method) is_target() (APRProof method) is_term_like() (in module pyk.kast.manip) is_terminal() (DefaultSemantics method) (KCFGExploration method) (KCFGSemantics method) is_top() (in module pyk.prelude.ml) is_trusted (KClaim property) is_vacuous() (KCFG method) items (Att attribute) (KProduction attribute) (KSequence attribute) (Production attribute)

J

JSON (KAstInput attribute) (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) json (Pattern property) JSON (PrintOutput attribute) json (Proof property) (Sort property) json2string() (in module pyk.kore.prelude)

json_entry() (in module pyk.kore.prelude) json_key() (in module pyk.kore.prelude) json_list() (in module pyk.kore.prelude) json_object() (in module pyk.kore.prelude) json_to_kore() (in module pyk.kore.prelude) JsonRpcClient (class in pyk.kore.rpc) JsonRpcClientFacade (class in pyk.kore.rpc) JsonRpcError jsons() (in module pyk.kore.prelude)

K

k() (in module pyk.kore.prelude) k_config_var() (in module pyk.kore.prelude) k_version (KBuild property) k_version() (in module pyk.kbuild.utils) KApply (class in pyk.kast.inner) KAs (class in pyk.kast.inner) KAssoc (class in pyk.kast.outer) KAst (class in pyk.kast.kast) kast (CTerm property) KAST (KAstInput attribute) (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) kast_simplify() (CTermSymbolic method) kast_term() (in module pyk.kast.kast) kast_to_kore() (CTermSymbolic method) (KPrint method) KAstInput (class in pyk.ktool.kprint) KAstOutput (class in pyk.ktool.kprint) KAtt (class in pyk.kast.att) KBubble (class in pyk.kast.outer) KBuild (class in pyk.kbuild.kbuild) KBuildEnv (class in pyk.kbuild.kbuild) KCFG (class in pyk.kcfg.kcfg) kcfg (KCFGExploration attribute) KCFG.Cover (class in pyk.kcfg.kcfg) KCFG.Edge (class in pyk.kcfg.kcfg) KCFG.EdgeLike (class in pyk.kcfg.kcfg) KCFG.MultiEdge (class in pyk.kcfg.kcfg) KCFG.NDBranch (class in pyk.kcfg.kcfg) KCFG.Node (class in pyk.kcfg.kcfg) KCFG.Split (class in pyk.kcfg.kcfg) KCFG.Successor (class in pyk.kcfg.kcfg) kcfg_explore (Prover attribute) kcfg_json_path (KCFGStore property) kcfg_node_dir (KCFGStore property) kcfg_node_path() (KCFGStore method) kcfg_semantics (KCFGExplore attribute) kcfg_show (APRProofShow attribute) KCFGExploration (class in pyk.kcfg.exploration) KCFGExplorationNodeAttr (class in pyk.kcfg.exploration) KCFGExplore (class in pyk.kcfg.explore) KCFGExtendResult (class in pyk.kcfg.kcfg) KCFGNodeAttr (class in pyk.kcfg.kcfg) KCFGSemantics (class in pyk.kcfg.semantics) KCFGShow (class in pyk.kcfg.show) KCFGStore (class in pyk.kcfg.kcfg) KCFGViewer (class in pyk.kcfg.tui) KClaim (class in pyk.kast.outer) KContext (class in pyk.kast.outer) KDefinition (class in pyk.kast.outer) kdist_dir (KBuild attribute) key (AttEntry attribute) keys() (Atts class method) KFlatModule (class in pyk.kast.outer) KFlatModuleList (class in pyk.kast.outer) KImport (class in pyk.kast.outer) KInner (class in pyk.kast.inner) KInterpreter (class in pyk.krepl.repl) KLABEL (Atts attribute) KLabel (class in pyk.kast.inner) klabel (KProduction attribute) KLABEL (State attribute) (TokenType attribute) klabels (SyntaxAssoc attribute) KNonTerminal (class in pyk.kast.outer) kompile() (in module pyk.ktool.kompile) (in module pyk.testing.plugin) (KBuild method) (KBuildEnv method) KompileBackend (class in pyk.ktool.kompile) kompiled_dir (BoosterServerArgs attribute) (KoreServerArgs attribute) kompiled_kore (KPrint property) KompiledKore (class in pyk.kore.kompiled) Kore (class in pyk.kore.syntax) KORE (KAstInput attribute) (KAstOutput attribute) (KompileBackend attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) kore (State property)

kore_bool() (in module pyk.kore.match) kore_bytes() (in module pyk.kore.match) kore_id() (in module pyk.kore.match) kore_int() (in module pyk.kore.match) kore_lexer() (in module pyk.kore.lexer) kore_list_of() (in module pyk.kore.match) kore_map_of() (in module pyk.kore.match) kore_print() (in module pyk.kore.tools) KORE_RPC (LogOrigin attribute) kore_server() (in module pyk.kore.rpc) kore_set_of() (in module pyk.kore.match) kore_str() (in module pyk.kore.match) kore_term() (in module pyk.kore.syntax) kore_to_json() (in module pyk.kore.prelude) kore_to_kast() (CTermSymbolic method) (KPrint method) kore_to_pretty() (KPrint method) KoreClient (class in pyk.kore.rpc) KoreClientError KoreExecLogFormat (class in pyk.kore.rpc) KoreParser (class in pyk.kore.parser) KoreServer (class in pyk.kore.rpc) KoreServerArgs (class in pyk.kore.rpc) KoreServerInfo (class in pyk.kore.rpc) KoreServerPool (class in pyk.kore.pool) KoreSortTable (class in pyk.kore.kompiled) KoreSymbolTable (class in pyk.kore.kompiled) KoreToken (class in pyk.kore.lexer) KOuter (class in pyk.kast.outer) KPrint (class in pyk.ktool.kprint) kprint (KCFGShow attribute) (NodePrinter attribute) KProduction (class in pyk.kast.outer) KProductionItem (class in pyk.kast.outer) KProve (class in pyk.ktool.kprove) KProveOutput (class in pyk.ktool.kprove) KRegexTerminal (class in pyk.kast.outer) KRepl (class in pyk.krepl.repl) KRequire (class in pyk.kast.outer) KRewrite (class in pyk.kast.inner) KRule (class in pyk.kast.outer) KRuleLike (class in pyk.kast.outer) KRun (class in pyk.ktool.krun) krun() (KRun method) KRunOutput (class in pyk.ktool.krun) KSentence (class in pyk.kast.outer) kseq() (in module pyk.kore.prelude) KSequence (class in pyk.kast.inner) KSort (class in pyk.kast.inner) KSortSynonym (class in pyk.kast.outer) KState (class in pyk.krepl.repl) KSyntaxAssociativity (class in pyk.kast.outer) KSyntaxLexical (class in pyk.kast.outer) KSyntaxPriority (class in pyk.kast.outer) KSyntaxSort (class in pyk.kast.outer) KTerminal (class in pyk.kast.outer) KToken (class in pyk.kast.inner) KVariable (class in pyk.kast.inner) KVersion (class in pyk.kbuild.utils) KVersion.Git (class in pyk.kbuild.utils) KW_ALIAS (TokenType attribute), [1] KW_AXIOM (TokenType attribute) KW_CLAIM (TokenType attribute), [1] KW_CONFIG (TokenType attribute) KW_CONTEXT (TokenType attribute) KW_ENDMODULE (TokenType attribute), [1] KW_HOOKED_SORT (TokenType attribute) KW_HOOKED_SYMBOL (TokenType attribute) KW_IMPORT (TokenType attribute) KW_IMPORTS (TokenType attribute) KW_LEFT (TokenType attribute) KW_LEXICAL (TokenType attribute) KW_MODULE (TokenType attribute), [1] KW_NONASSOC (TokenType attribute) KW_PRIORITY (TokenType attribute) KW_PRIVATE (TokenType attribute) KW_PUBLIC (TokenType attribute) KW_REQUIRES (TokenType attribute) KW_RIGHT (TokenType attribute) KW_RULE (TokenType attribute) KW_SORT (TokenType attribute) KW_SYMBOL (TokenType attribute) KW_SYNTAX (TokenType attribute) KW_WHERE (TokenType attribute)

L

label (Alias attribute) LABEL (Atts attribute) label (Claim attribute) (Config attribute) (Context attribute) (KApply attribute) (KSentence property) (Rule attribute) (StringSentence attribute) labels_to_dots() (in module pyk.kast.manip) last_constraint (RefutationProof property) LATEX (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) LBRACE (TokenType attribute), [1] LBRACK (TokenType attribute), [1] le_int() (in module pyk.kore.prelude) least_common_supersort() (KDefinition method) leaves (KCFG property) left (AliasDecl attribute) LEFT (Assoc attribute) (Atts attribute) left (BinaryConn attribute) (BinaryPred attribute) (Equals attribute) (Iff attribute) (Implies attribute) (In attribute) LEFT (KAssoc attribute) left (Rewrites attribute) left_assoc() (KoreParser method) LeftAssoc (class in pyk.kore.syntax) leInt() (in module pyk.prelude.kint) let() (AliasDecl method) (And method) (App method) (Axiom method) (Bottom method) (Ceil method) (Claim method) (Definition method) (DV method) (Equals method) (EVar method) (Exists method) (Floor method) (Forall method) (Iff method) (Implies method) (Import method) (In method) (KApply method) (KAs method) (KBubble method) (KCFG.Node method) (KClaim method) (KContext method) (KDefinition method) (KFlatModule method) (KFlatModuleList method) (KImport method) (KLabel method) (KNonTerminal method) (KProduction method) (KRegexTerminal method) (KRequire method) (KRewrite method) (KRule method) (KRuleLike method) (KSequence method) (KSort method) (KSortSynonym method) (KSyntaxAssociativity method) (KSyntaxLexical method) (KSyntaxPriority method) (KSyntaxSort method) (KTerminal method) (KToken method) (KVariable method) (LeftAssoc method) (Module method) (Mu method) (Next method) (Not method) (Nu method) (Or method) (Rewrites method) (RightAssoc method) (SortApp method) (SortDecl method) (SortVar method) (String method) (SVar method) (Symbol method) (SymbolDecl method) (Top method) let_att() (KBubble method) (KClaim method) (KContext method) (KDefinition method) (KFlatModule method) (KProduction method) (KRule method) (KSortSynonym method) (KSyntaxAssociativity method) (KSyntaxLexical method) (KSyntaxPriority method) (KSyntaxSort method) (WithKAtt method) let_attrs() (AliasDecl method) (Axiom method) (Claim method) (Definition method) (Import method) (Module method) (SortDecl method) (SymbolDecl method) (WithAttrs method)

let_node() (KCFG method) let_patterns() (And method) (App method) (Bottom method) (Ceil method) (DV method) (Equals method) (EVar method) (Exists method) (Floor method) (Forall method) (Iff method) (Implies method) (In method) (LeftAssoc method) (Mu method) (Next method) (Not method) (Nu method) (Or method) (Pattern method) (Rewrites method) (RightAssoc method) (String method) (SVar method) (Top method) let_sort() (And method) (Bottom method) (Ceil method) (DV method) (Equals method) (EVar method) (Exists method) (Floor method) (Forall method) (Iff method) (Implies method) (In method) (KVariable method) (Next method) (Not method) (Or method) (Rewrites method) (SVar method) (Top method) (WithSort method) let_terms() (KApply method) (KAs method) (KInner method) (KRewrite method) (KSequence method) (KToken method) (KVariable method) Lexical (class in pyk.kast.outer_syntax) lhs (KRewrite attribute) lhs_body (EqualityProof property) lift_edge() (KCFG method) lift_edges() (KCFG method) lift_split_edge() (KCFG method) lift_split_split() (KCFG method) lift_splits() (KCFG method) lines (APRSummary property) (CompositeSummary property) (EqualitySummary property) (ProofSummary property) (RefutationSummary property) list_empty() (in module pyk.prelude.collections) list_item() (in module pyk.prelude.collections) list_of() (in module pyk.prelude.collections) list_pattern() (in module pyk.kore.prelude) LLVM (KompileBackend attribute) (LogOrigin attribute) llvm_interpret() (in module pyk.ktool.krun) llvm_kompiled_dir (BoosterServerArgs attribute) load() (KompiledKore static method) (Project static method) load_from_dir() (Project static method) load_from_json() (KompiledKore static method) load_from_kore() (KompiledKore static method) LOCATION (Atts attribute) LocationType (class in pyk.kast.att) log_axioms_file (BoosterServerArgs attribute) (KoreServerArgs attribute) LogEntry (class in pyk.kore.rpc) LogOrigin (class in pyk.kore.rpc) LogRewrite (class in pyk.kore.rpc) logs (AbortedResult attribute) (APRProof attribute) (BranchingResult attribute) (CTermExecute attribute) (CTermImplies attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (ImpliesResult attribute) (NDBranch attribute) (Step attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) LogSimplification (class in pyk.kore.rpc) LPAREN (TokenType attribute), [1] lt_int() (in module pyk.kore.prelude) ltInt() (in module pyk.prelude.kint)

M

MACRO (Atts attribute) MACRO_REC (Atts attribute) macro_rules (KDefinition property) main() (in module pyk.kcovr) main_file (KProve attribute) main_module (KDefinition attribute) (KFlatModuleList attribute) (KPrint attribute) main_module_name (APRProver attribute) (KDefinition attribute) MAINCELL (Atts attribute) major (KVersion attribute) make_unique_segments() (KCFGShow static method) manifest() (Target method) map_att() (WithKAtt method) map_attrs() (WithAttrs method) map_empty() (in module pyk.prelude.collections) map_inner() (KInner method) map_item() (in module pyk.prelude.collections) map_of() (in module pyk.prelude.collections) map_pattern() (in module pyk.kore.prelude) map_patterns() (Pattern method) map_sentences() (KFlatModule method) map_sort() (WithSort method) match() (CTerm method) (KApply method) (KAs method) (KInner method) (KRewrite method) (KSequence method) (KToken method) (KVariable method) match_app() (in module pyk.kore.match) match_dv() (in module pyk.kore.match) match_inj() (in module pyk.kore.match) match_left_assoc() (in module pyk.kore.match) match_list() (in module pyk.kore.match) match_map() (in module pyk.kore.match) match_set() (in module pyk.kore.match) match_symbol() (in module pyk.kore.match) match_with_constraint() (CTerm method) MAUDE (KompileBackend attribute) maybe() (in module pyk.utils) meet() (KoreSortTable method) merge_with() (in module pyk.utils) message (DefaultError attribute) minimize (NodePrinter attribute) minimize() (KCFG method) (Subst method) minimize_kcfg() (KCFGExploration method) minimize_rule() (in module pyk.kast.manip) minimize_term() (in module pyk.kast.manip) minor (KVersion attribute) ML_AND (TokenType attribute) ML_BOTTOM (TokenType attribute) ML_CEIL (TokenType attribute) ML_DV (TokenType attribute) ML_EQUALS (TokenType attribute) ML_EXISTS (TokenType attribute) ML_FLOOR (TokenType attribute) ML_FORALL (TokenType attribute) ML_IFF (TokenType attribute) ML_IMPLIES (TokenType attribute) ML_IN (TokenType attribute) ML_LEFT_ASSOC (TokenType attribute) ML_MU (TokenType attribute) ML_NEXT (TokenType attribute) ML_NOT (TokenType attribute) ML_NU (TokenType attribute) ML_OR (TokenType attribute) ml_pattern() (KoreParser method) ml_pred (Subst property) ml_pred_to_bool() (in module pyk.kast.manip) ML_REWRITES (TokenType attribute) ML_RIGHT_ASSOC (TokenType attribute) ML_TOP (TokenType attribute) mlAnd() (in module pyk.prelude.ml) mlBottom() (in module pyk.prelude.ml) mlCeil() (in module pyk.prelude.ml) MLConn (class in pyk.kore.syntax) mlEquals() (in module pyk.prelude.ml) mlEqualsFalse() (in module pyk.prelude.ml) mlEqualsTrue() (in module pyk.prelude.ml) mlExists() (in module pyk.prelude.ml) MLFixpoint (class in pyk.kore.syntax) mlImplies() (in module pyk.prelude.ml) mlNot() (in module pyk.prelude.ml) mlOr() (in module pyk.prelude.ml) MLPattern (class in pyk.kore.syntax) MLPred (class in pyk.kore.syntax) MLQuant (class in pyk.kore.syntax) MLRewrite (class in pyk.kore.syntax) MLSyntaxSugar (class in pyk.kore.syntax) mlTop() (in module pyk.prelude.ml) model (SatResult attribute) models (APRFailureInfo attribute) MODNAME (State attribute) (TokenType attribute)

module pyk pyk.coverage pyk.cterm pyk.cterm.cterm pyk.cterm.symbolic pyk.dequote pyk.kast pyk.kast.att pyk.kast.inner pyk.kast.kast pyk.kast.manip pyk.kast.markdown pyk.kast.outer pyk.kast.outer_lexer pyk.kast.outer_parser pyk.kast.outer_syntax pyk.kast.pretty pyk.kbuild pyk.kbuild.config pyk.kbuild.kbuild pyk.kbuild.project pyk.kbuild.utils pyk.kcfg pyk.kcfg.exploration pyk.kcfg.explore pyk.kcfg.kcfg pyk.kcfg.semantics pyk.kcfg.show pyk.kcfg.store pyk.kcfg.tui pyk.kcovr pyk.kdist pyk.kdist.api pyk.kdist.utils pyk.kllvm pyk.kllvm.compiler pyk.kllvm.importer pyk.kllvm.runtime pyk.konvert pyk.kore pyk.kore.kompiled pyk.kore.lexer pyk.kore.manip pyk.kore.match pyk.kore.parser pyk.kore.pool pyk.kore.prelude pyk.kore.rpc pyk.kore.syntax pyk.kore.tools pyk.kore_exec_covr pyk.kore_exec_covr.kore_exec_covr pyk.krepl pyk.krepl.repl pyk.ktool pyk.ktool.kompile pyk.ktool.kprint pyk.ktool.kprove pyk.ktool.krun pyk.prelude pyk.prelude.bytes pyk.prelude.collections pyk.prelude.k pyk.prelude.kbool pyk.prelude.kint pyk.prelude.ml pyk.prelude.string pyk.prelude.utils pyk.proof pyk.proof.implies pyk.proof.parallel pyk.proof.proof pyk.proof.reachability pyk.proof.show pyk.proof.tui pyk.testing pyk.testing.plugin pyk.utils Module (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) module() (KDefinition method) (KoreParser method) (OuterParser method) module_name (APRProof property) (BoosterServerArgs attribute) (DuplicateModuleError attribute) (Import attribute), [1] (KoreServerArgs attribute) (UnknownModuleError attribute) module_names (KDefinition property) modules (Definition attribute), [1] (KDefinition property) (KFlatModuleList attribute) Mu (class in pyk.kore.syntax) mu() (KoreParser method) multi_or() (KoreParser method) MultiaryConn (class in pyk.kore.syntax)

N

name (Atom attribute) (AttKey attribute) (EVar attribute) (KFlatModule attribute) (KImport attribute) (KLabel attribute) (KNonTerminal attribute) (KSort attribute) (KSyntaxLexical attribute) (KVariable attribute) (Module attribute), [1] (NonTerminal attribute) (Project attribute) (Sort attribute), [1] (SortApp attribute) (SortDecl attribute), [1] (SortVar attribute) (SVar attribute) (Symbol attribute) (SyntaxLexical attribute) (Target attribute) (VarPattern attribute) NAT (TokenType attribute) NavWidget (class in pyk.kcfg.tui) NavWidget.Selected (class in pyk.kcfg.tui) NDBranch (class in pyk.kcfg.kcfg) ndbranches() (KCFG method) ne_bool() (in module pyk.kore.prelude) ne_int() (in module pyk.kore.prelude) new (SyntaxSynonym attribute) new_sort (KSortSynonym attribute) Next (class in pyk.kore.syntax) next() (KoreParser method) next_state() (Interpreter method) (KInterpreter method) next_states (AbortedResult attribute) (BranchingResult attribute) (CTermExecute attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute)

no_cell_rewrite_to_dots() (in module pyk.kast.manip) no_dispatch (BehaviorView.Selected attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) no_post_exec_simplify (BoosterServerArgs attribute) node() (KCFG method) node_attrs() (APRProofNodePrinter method) (NodePrinter method) node_id (APRProofResult attribute) node_printer (KCFGShow attribute) node_refutations (APRProof attribute) node_short_info() (KCFGShow method) NodeAttr (class in pyk.kcfg.kcfg) NodePrinter (class in pyk.kcfg.show) nodes (APRSummary attribute) (KCFG property) NodeView (class in pyk.kcfg.tui) NON_ASSOC (Assoc attribute) (KAssoc attribute) non_empty (UserList attribute) non_terminals (KProduction property) NONE (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) none() (in module pyk.utils) nonempty_str() (in module pyk.utils) NoneType (class in pyk.kast.att) NonTerminal (class in pyk.kast.outer_syntax) nonzero_depth() (APRProver method) Not (class in pyk.kast.markdown) (class in pyk.kore.syntax) not_bool() (in module pyk.kore.prelude) not_none() (in module pyk.utils) notBool() (in module pyk.prelude.kbool) nott() (KoreParser method) Nu (class in pyk.kore.syntax) nu() (KoreParser method) NullaryConn (class in pyk.kore.syntax)

O

of() (And class method) (Bottom class method) (Ceil class method) (DV class method) (Equals class method) (Exists class method) (Floor class method) (Forall class method) (Iff class method) (Implies class method) (In class method) (LeftAssoc class method) (MLPattern class method) (Mu class method) (Next class method) (Not class method) (Nu class method) (Or class method) (Rewrites class method) (RightAssoc class method) (Top class method) old (SyntaxSynonym attribute) old_sort (KSortSynonym attribute) on_attributes() (in module pyk.kast.manip) on_behavior_view_selected() (NodeView method) on_click() (BehaviorView method) (Constraint method) (Custom method) (GraphChunk method) (Status method) (Term method) on_constraint_selected() (NodeView method) on_custom_selected() (NodeView method) on_enter() (GraphChunk method) on_graph_chunk_selected() (KCFGViewer method)

on_leave() (GraphChunk method) on_mount() (APRProofViewer method) (NodeView method) on_status_selected() (NodeView method) on_term_selected() (NodeView method) ONELINE (KoreExecLogFormat attribute) op (Not attribute) op_sort (Ceil attribute) (Equals attribute) (Floor attribute) (In attribute) (MLPred attribute) ops (And attribute), [1] (MultiaryConn attribute) (Or attribute), [1] OptimizedNodeStore (class in pyk.kcfg.store) OptionalType (class in pyk.kast.att) Or (class in pyk.kast.markdown) (class in pyk.kore.syntax) or_bool() (in module pyk.kore.prelude) orBool() (in module pyk.prelude.kbool) origin (LogEntry attribute) (LogRewrite attribute) (LogSimplification attribute) original_term (LogSimplification attribute) original_term_index (LogSimplification attribute) orr() (KoreParser method) outer_lexer() (in module pyk.kast.outer_lexer) OuterParser (class in pyk.kast.outer_parser) OVERLOAD (Atts attribute) overloads (KDefinition property) OWISE (Atts attribute) own_status (APRProof property) (ImpliesProof property) (Proof property)

P

package (PackageSource attribute) package_path() (in module pyk.kdist.utils) PackageSource (class in pyk.kbuild.project) param_sorts (AliasDecl attribute) (SymbolDecl attribute) params (KLabel attribute) (KProduction attribute) (KSyntaxSort attribute) (SortDecl attribute) paren() (in module pyk.kast.pretty) parse() (Format class method) (KVersion static method) (SelectorParser method) (TargetId static method) parse_args() (in module pyk.kcovr) parse_rule_applications() (in module pyk.kore_exec_covr.kore_exec_covr) parse_tags() (in module pyk.kast.markdown) parse_token() (KPrint method) ParseError passed (Proof property) PASSED (ProofStatus attribute) patch (KVersion attribute) path (KBuildEnv attribute) (PathSource attribute) (Project attribute) (Require attribute) path_conditions (APRFailureInfo attribute) path_constraints() (APRProof method) path_length() (KCFG static method) paths_between() (KCFG method) PathSource (class in pyk.kbuild.project) PathType (class in pyk.kast.att) pattern (Assoc property) (Axiom attribute) (AxiomLike attribute) (Ceil attribute) (Claim attribute) Pattern (class in pyk.kore.syntax) pattern (Exists attribute) (Floor attribute) (Forall attribute) (KAs attribute) (KState attribute) PATTERN (KVersion attribute) pattern (LeftAssoc property) (MLFixpoint attribute) (MLQuant attribute) (Mu attribute) (Next attribute) (Not attribute) (Nu attribute) (RightAssoc property) (RoundPred attribute) (SmtSolverError attribute) (Term property) (UnaryConn attribute) pattern() (KoreParser method) pattern_sorts() (KoreSymbolTable method) PatternError patterns (App property) (Assoc property) (BinaryConn property) (BinaryPred property) (DV property) (MLFixpoint property) (MLQuant property) (MultiaryConn property) (Next property) (NullaryConn property) (Pattern property) (Rewrites property) (RoundPred property) (String property) (UnaryConn property) (VarPattern property) pending (APRProof property) (APRSummary attribute) PENDING (ProofStatus attribute) pending_nodes (APRFailureInfo attribute) pid (KoreServer property) (KoreServerInfo attribute) plugin_name (TargetId attribute) PLUS (TokenType attribute) port (BoosterServerArgs attribute) (KoreServer property) (KoreServerArgs attribute) (KoreServerInfo attribute) POSet (class in pyk.utils) pre_constraints (RefutationProof property) precede_regex (KRegexTerminal attribute) pred (Subst property) predecessors() (KCFG method) PREDICATE (Atts attribute) predicate (ImpliesResult attribute) (State attribute) PREFER (Atts attribute) PRETTY (KAstOutput attribute) pretty (KAtt property) PRETTY (KProveOutput attribute) (KRunOutput attribute) pretty (KState property) PRETTY (PrintOutput attribute) pretty() (AnyType method) (APRProofShow method) (AttType method) (EqualityProof method) (FormatType method) (IntType method) (KCFGShow method) (LocationType method) (NoneType method) (OptionalType method) (PathType method) (RefutationProof method) (StrType method) pretty_bytes() (in module pyk.prelude.bytes) pretty_bytes_str() (in module pyk.prelude.bytes) pretty_print() (KCFGExplore method) (KPrint method) pretty_segments() (APRProofShow method) (KCFGShow method) pretty_string() (in module pyk.prelude.string) PrettyPrinter (class in pyk.kast.pretty) print() (APRFailureInfo method) (PrettyPrinter method) print_node() (NodePrinter method) PrintOutput (class in pyk.kore.tools) prior_loops_cache (APRProof attribute) PRIORITIES (Atts attribute) priorities (KDefinition property) (KSyntaxPriority attribute) PRIORITY (Atts attribute) priority (KRule property) PriorityBlock (class in pyk.kast.outer_syntax) PRIVATE (Atts attribute) PRODUCTION (Atts attribute) Production (class in pyk.kast.outer_syntax) production_for_cell_sort() (KDefinition method) ProductionItem (class in pyk.kast.outer_syntax) ProductionLike (class in pyk.kast.outer_syntax) productions (KDefinition property) (KFlatModule property) (PriorityBlock attribute) profile() (in module pyk.testing.plugin) PROGAM (KProveOutput attribute) PROGRAM (KAstInput attribute) (KAstOutput attribute) (KRunOutput attribute) (PrintOutput attribute) program_file (KInterpreter attribute) Project (class in pyk.kbuild.project) project (KBuildEnv attribute) project_file (Project property) PROJECTION (Atts attribute) prompt (BaseRepl attribute) proof (APRProofNodePrinter attribute) (APRProver attribute) Proof (class in pyk.proof.parallel) (class in pyk.proof.proof) proof (ImpliesProver attribute) (Prover attribute) proof_data_exists() (Proof static method) proof_dir (Proof attribute) proof_exists() (Proof static method) proof_subdir (Proof property) ProofStatus (class in pyk.proof.proof) ProofStep (class in pyk.proof.parallel) ProofSummary (class in pyk.proof.proof) propagate_up_constraints() (in module pyk.kast.manip) prove() (KProve method)

prove_claim() (KProve method) prove_claim_rpc() (KProve method) prove_parallel() (in module pyk.proof.parallel) prove_rpc() (KProve method) Prover (class in pyk.proof.parallel) (class in pyk.proof.proof) prover (KProve attribute) prover_args (KProve attribute) prune() (APRProof method) (KCFG method) (KCFGExploration method) public (Import attribute) (KImport attribute) push_down_rewrites() (in module pyk.kast.manip) pyk module pyk.coverage module pyk.cterm module pyk.cterm.cterm module pyk.cterm.symbolic module pyk.dequote module pyk.kast module pyk.kast.att module pyk.kast.inner module pyk.kast.kast module pyk.kast.manip module pyk.kast.markdown module pyk.kast.outer module pyk.kast.outer_lexer module pyk.kast.outer_parser module pyk.kast.outer_syntax module pyk.kast.pretty module pyk.kbuild module pyk.kbuild.config module pyk.kbuild.kbuild module pyk.kbuild.project module pyk.kbuild.utils module pyk.kcfg module pyk.kcfg.exploration module pyk.kcfg.explore module pyk.kcfg.kcfg module pyk.kcfg.semantics module pyk.kcfg.show module pyk.kcfg.store module pyk.kcfg.tui module pyk.kcovr module pyk.kdist module pyk.kdist.api module pyk.kdist.utils module pyk.kllvm module pyk.kllvm.compiler module pyk.kllvm.importer module pyk.kllvm.runtime module pyk.konvert module pyk.kore module pyk.kore.kompiled module pyk.kore.lexer module pyk.kore.manip module pyk.kore.match module pyk.kore.parser module pyk.kore.pool module pyk.kore.prelude module pyk.kore.rpc module pyk.kore.syntax module pyk.kore.tools module pyk.kore_exec_covr module pyk.kore_exec_covr.kore_exec_covr module pyk.krepl module pyk.krepl.repl module pyk.ktool module pyk.ktool.kompile module pyk.ktool.kprint module pyk.ktool.kprove module pyk.ktool.krun module pyk.prelude module pyk.prelude.bytes module pyk.prelude.collections module pyk.prelude.k module pyk.prelude.kbool module pyk.prelude.kint module pyk.prelude.ml module pyk.prelude.string module pyk.prelude.utils module pyk.proof module pyk.proof.implies module pyk.proof.parallel module pyk.proof.proof module pyk.proof.reachability module pyk.proof.show module pyk.proof.tui module pyk.testing module pyk.testing.plugin module pyk.utils module pytest_addoption() (in module pyk.testing.plugin)

Q

QUESTION (TokenType attribute)

R

raised() (in module pyk.utils) RBRACE (TokenType attribute), [1] RBRACK (TokenType attribute), [1] reachable_nodes() (KCFG method) read_cfg_data() (KCFG static method) (KCFGStore method) read_kast_definition() (in module pyk.kast.outer) read_node_data() (KCFG static method) (KCFGStore method) read_proof() (APRProof static method) (Proof class method) read_proof_data() (APRProof static method) (EqualityProof static method) (Proof static method) (RefutationProof static method) read_subproof() (Proof method) read_subproof_data() (Proof method) reason (AbortedResult attribute) (BranchingResult attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (RewriteFailure attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) RefutationProof (class in pyk.proof.implies) RefutationSummary (class in pyk.proof.implies) refute_node() (APRProof method) refuted (APRSummary attribute) regex (KRegexTerminal attribute) (KSyntaxLexical attribute) (Lexical attribute) (SyntaxLexical attribute) REGEX (TokenType attribute) remaining_implication (CTermImplies attribute) remove_alias() (KCFG method) remove_attr() (KCFG method) (KCFG.Node method) remove_attrs() (in module pyk.kast.manip) remove_cell_map_items() (KDefinition method) remove_cover() (KCFG method) remove_edge() (KCFG method) remove_generated_cells() (in module pyk.kast.manip) remove_node() (KCFG method) (KCFGExploration method) remove_semantic_casts() (in module pyk.kast.manip) remove_source_map() (in module pyk.kast.manip) remove_stuck() (KCFG method) remove_subproof() (Proof method) remove_terminal() (KCFGExploration method) remove_useless_constraints() (CTerm method) (in module pyk.kast.manip) remove_vacuous() (KCFG method) rename_generated_vars() (in module pyk.kast.manip) render_classes() (in module pyk.kcovr) render_coverage_xml() (in module pyk.kcovr) render_lines() (in module pyk.kcovr) repeat_last() (in module pyk.utils) replace() (KRewrite method) replace_node() (KCFG method) replace_rewrites_with_implies() (in module pyk.kast.manip) replace_source() (KCFG.Cover method) (KCFG.Edge method) (KCFG.NDBranch method) (KCFG.Split method) (KCFG.Successor method) replace_target() (KCFG.Cover method) (KCFG.Edge method) (KCFG.NDBranch method) (KCFG.Split method) (KCFG.Successor method) replace_top() (KRewrite method) ReplError request() (HttpTransport method) (JsonRpcClient method) (JsonRpcClientFacade method) (SingleSocketTransport method) (Transport method)

Require (class in pyk.kast.outer_syntax) require (KRequire attribute) require() (OuterParser method) requires (Definition attribute) (KClaim attribute) (KContext attribute) (KDefinition attribute) (KRule attribute) (KRuleLike attribute) resolve() (KoreSymbolTable method) (PackageSource method) (PathSource method) (Source method) resource_file_names (Project property) resource_files (Project property) resources (Project attribute) result (LogEntry attribute) (LogRewrite attribute) (LogSimplification attribute) return_sort() (KDefinition method) rev (KVersion.Git attribute) RewriteFailure (class in pyk.kore.rpc) RewriteResult (class in pyk.kore.rpc) Rewrites (class in pyk.kore.syntax) rewrites() (KoreParser method) RewriteSuccess (class in pyk.kore.rpc) rewritten_term (RewriteSuccess attribute) rhs (KRewrite attribute) rhs_body (EqualityProof property) right (AliasDecl attribute) RIGHT (Assoc attribute) (Atts attribute) right (BinaryConn attribute) (BinaryPred attribute) (Equals attribute) (Iff attribute) (Implies attribute) (In attribute) RIGHT (KAssoc attribute) right (Rewrites attribute) right_assoc() (KoreParser method) RightAssoc (class in pyk.kore.syntax) root (KCFG property) RoundPred (class in pyk.kore.syntax) RPAREN (TokenType attribute), [1] rule (AbortedResult attribute) (BranchingResult attribute) Rule (class in pyk.kast.outer_syntax) rule (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) RULE (KAstInput attribute) rule (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) rule_id (RewriteFailure attribute) (RewriteResult attribute) (RewriteSuccess attribute) (State attribute) RULE_LABEL (TokenType attribute) rule_labels (NDBranch attribute) (Step attribute) rule_predicate (State attribute) rule_substitution (State attribute) rules (KCFG.Edge attribute) (KCFG.NDBranch attribute) (KDefinition property) (KFlatModule property) run() (KRun method) (Runtime method) (Term method) run_pattern() (KRun method) run_process() (in module pyk.utils) (KRun method) Runtime (class in pyk.kllvm.runtime)

S

same_loop() (DefaultSemantics method) (KCFGSemantics method) satisfiable (ImpliesResult attribute) SatResult (class in pyk.kore.rpc) section_edge() (KCFGExplore method) select_code_blocks() (in module pyk.kast.markdown) Selector (class in pyk.kast.markdown) selector_lexer() (in module pyk.kast.markdown) SelectorParser (class in pyk.kast.markdown) semantic_rules (KDefinition property) Sentence (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) sentence() (KoreParser method) (OuterParser method) sentence_by_unique_id (KDefinition property) (KFlatModule property) sentence_type (KBubble attribute) sentences (KFlatModule attribute) (Module attribute), [1] sep (UserList attribute) SEQSTRICT (Atts attribute) serialize() (Term method) set_cell() (in module pyk.kast.manip) set_empty() (in module pyk.prelude.collections) set_exec_time() (APRProof method) set_item() (in module pyk.prelude.collections) set_of() (in module pyk.prelude.collections) set_pattern() (in module pyk.kore.prelude) set_var() (KoreParser method) SET_VAR_ID (TokenType attribute) set_var_id() (KoreParser method) SetVarId (class in pyk.kore.syntax) shorten_hash() (in module pyk.utils) shorten_hashes() (in module pyk.utils) shortest_distance_between() (KCFG method) shortest_path_between() (KCFG method) shortest_path_to() (APRProof method) show() (APRProofShow method) (KCFGShow method) SIMPLIFICATION (Atts attribute) simplified_antecedent (ImpliesProof attribute) (ImpliesProofResult attribute) simplified_consequent (ImpliesProof attribute) (ImpliesProofResult attribute) simplified_constraints (EqualityProof property) (RefutationProof property) simplified_equality (EqualityProof property) simplify() (CTermSymbolic method) (KCFGExplore method) (KoreClient method) (Runtime method) simplify_bool() (in module pyk.kast.manip) (Runtime method) simplify_config() (KCFGShow static method) single() (in module pyk.utils) SINGLE_SOCKET (TransportType attribute) SingleSocketTransport (class in pyk.kore.rpc) smt_reset_interval (BoosterServerArgs attribute) (KoreServerArgs attribute) smt_retry_limit (BoosterServerArgs attribute) (KoreServerArgs attribute) smt_tactic (BoosterServerArgs attribute) (KoreServerArgs attribute) smt_timeout (BoosterServerArgs attribute) (KoreServerArgs attribute) SmtSolverError some() (in module pyk.utils) sort (AliasDecl attribute) (And attribute) SORT (Atts attribute) sort (Bottom attribute) (Ceil attribute) Sort (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) sort (DV attribute) (EqualityProof property) (Equals attribute) (EVar attribute) (Exists attribute) (Floor attribute) (Forall attribute) (Iff attribute) (Implies attribute) (In attribute) (KNonTerminal attribute) (KProduction attribute) (KSyntaxSort attribute) (KToken attribute) (KVariable attribute) (MLQuant attribute) (Next attribute) (NonTerminal attribute) (Not attribute) (Or attribute) (Rewrites attribute) (SVar attribute) (SymbolDecl attribute) (Top attribute) (UserList attribute) (VarPattern attribute) (WithSort attribute) sort() (KDefinition method) (KoreParser method) sort_ac_collections() (in module pyk.kast.manip) sort_app() (KoreParser method) sort_assoc_label() (in module pyk.kast.manip) sort_decl() (KoreParser method) sort_strict() (KDefinition method) sort_table (KompiledKore attribute) sort_var() (KoreParser method) sort_vars() (KDefinition method) SortApp (class in pyk.kore.syntax) SortDecl (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) sorts (App attribute) (Assoc property) (BinaryPred property) (DV property) (MLConn property) (MLFixpoint property) (MLPattern property) (MLQuant property) (MLRewrite property) (RoundPred property) (SortApp attribute) SortVar (class in pyk.kore.syntax) SOURCE (Atts attribute) Source (class in pyk.kbuild.project) source (KCFG.Cover attribute) (KCFG.Edge attribute) (KCFG.EdgeLike attribute) (KCFG.MultiEdge attribute) (KCFG.NDBranch attribute) (KCFG.Split attribute) (KCFG.Successor attribute) (KSentence property)

source() (Target method) source_dir (Project attribute) source_file_names (Project property) source_files (Project property) source_vars (KCFG.Successor property) split_config_and_constraints() (in module pyk.kast.manip) split_config_from() (in module pyk.kast.manip) split_on_constraints() (KCFG method) splits (KCFG.Split property) splits() (KCFG method) STANDARD (KoreExecLogFormat attribute) start() (KoreServer method) state (AbortedResult attribute) (BaseRepl attribute) (BranchingResult attribute) State (class in pyk.kast.outer_lexer) (class in pyk.kore.rpc) state (CTermExecute attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) status (APRSummary attribute) Status (class in pyk.kcfg.tui) status (EqualitySummary attribute) (Proof property), [1] (ProofSummary attribute) (RefutationSummary attribute) Step (class in pyk.kcfg.kcfg) step() (KCFGExplore method) (Runtime method) (Term method) step_proof() (APRProver method) (ImpliesProver method) (Prover method) StepResult (class in pyk.proof.proof) steps() (Prover method) StopReason (class in pyk.kore.rpc) store_path (KCFGStore attribute) str_dv() (in module pyk.kore.prelude) STRICT (Atts attribute) String (class in pyk.kore.syntax) STRING (TokenType attribute), [1] string() (KoreParser method) string2json() (in module pyk.kore.prelude) string_sentence() (OuterParser method) StringSentence (class in pyk.kast.outer_syntax) stringToken() (in module pyk.prelude.string) strip_coverage_logger() (in module pyk.coverage) StrType (class in pyk.kast.att) stuck (APRSummary attribute) Stuck (class in pyk.kcfg.kcfg) STUCK (FallbackReason attribute) stuck (KCFG property) STUCK (KCFGNodeAttr attribute) (StopReason attribute) StuckResult (class in pyk.kore.rpc) sub_projects (Project property) submit() (KoreServerPool method) subproof_ids (Proof property) subproofs (APRSummary attribute) (Proof property) subproofs_status (Proof property) subsort_table (KDefinition property) subsorts() (KDefinition method) Subst (class in pyk.kast.inner) subst (CSubst attribute) substitution (ImpliesResult attribute) (State attribute) successors() (KCFG method) summaries (CompositeSummary attribute) summary (APRProof property) (EqualityProof property) (Proof property) (RefutationProof property) SVar (class in pyk.kore.syntax) symbol (App attribute) SYMBOL (Atts attribute) Symbol (class in pyk.kore.syntax) symbol (SymbolDecl attribute) symbol() (And class method) (Bottom class method) (Ceil class method) (DV class method) (Equals class method) (Exists class method) (Floor class method) (Forall class method) (Iff class method) (Implies class method) (In class method) (KoreParser method) (LeftAssoc class method) (MLPattern class method) (Mu class method) (Next class method) (Not class method) (Nu class method) (Or class method) (Rewrites class method) (RightAssoc class method) (Top class method) symbol_decl() (KoreParser method) symbol_decls (Module property) SYMBOL_ID (TokenType attribute) symbol_id() (KoreParser method) symbol_table (KompiledKore attribute) (PrettyPrinter property) SymbolDecl (class in pyk.kore.syntax) SymbolId (class in pyk.kore.syntax) symbols (KDefinition property) sync() (KBuildEnv method) sync_files() (in module pyk.kbuild.utils) SYNTAX (State attribute) syntax_productions (KDefinition property) (KFlatModule property) syntax_sentence() (OuterParser method) syntax_sorts (KFlatModule property) SyntaxAssoc (class in pyk.kast.outer_syntax) SyntaxDecl (class in pyk.kast.outer_syntax) SyntaxDefn (class in pyk.kast.outer_syntax) SyntaxLexical (class in pyk.kast.outer_syntax) SyntaxPriority (class in pyk.kast.outer_syntax) SyntaxSentence (class in pyk.kast.outer_syntax) SyntaxSynonym (class in pyk.kast.outer_syntax)

T

tags (KSyntaxAssociativity attribute) target (APRProof attribute) Target (class in pyk.kbuild.project) (class in pyk.kdist.api) target (KCFG.Cover attribute) (KCFG.Edge attribute) (KCFG.EdgeLike attribute) target_ids (KCFG.Successor property) target_name (TargetId attribute) target_vars (KCFG.Successor property) TargetId (class in pyk.kdist.api) targets (KCFG.EdgeLike property) (KCFG.NDBranch property) (KCFG.Split property) (KCFG.Successor property) (Project attribute) Term (class in pyk.kcfg.tui) (class in pyk.kllvm.runtime) term (State attribute) term() (Runtime method) terminal (APRSummary attribute) Terminal (class in pyk.kast.outer_syntax) terminal (KCFGExploration property) TERMINAL (KCFGExplorationNodeAttr attribute) terminal_ids (KCFGExploration property) TERMINAL_RULE (StopReason attribute) terminal_rules (APRProver attribute) TerminalResult (class in pyk.kore.rpc) TERMINALS (Atts attribute) terms (KApply property) (KAs property) (KInner property) (KRewrite property) (KSequence property) (KToken property) (KVariable property) text (Info attribute) (Kore property) (KoreToken attribute) (KVersion property) (NavWidget attribute) (Token attribute) TILDE (TokenType attribute) time (BehaviorView.Selected attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) TIMEOUT (StopReason attribute) TimeoutResult (class in pyk.kore.rpc) TIMES (TokenType attribute) timestamp() (in module pyk.kdist.utils) to_claim() (RefutationProof method) to_dict() (AnyType method) (AttType method) (CSubst method) (CTerm method) (FormatType method) (IntType method) (KAst method) (KAtt method) (KBubble method) (KCFG method) (KCFG.Cover method) (KCFG.Edge method) (KCFG.NDBranch method) (KCFG.Node method) (KCFG.Split method) (KCFG.Successor method) (KCFGExploration method) (KClaim method) (KContext method) (KDefinition method) (KFlatModule method) (KFlatModuleList method) (KImport method) (KInner method) (KLabel method) (KNonTerminal method) (KompiledKore method) (KProduction method) (KRegexTerminal method) (KRequire method) (KRule method) (KSort method) (KSortSynonym method) (KSyntaxAssociativity method) (KSyntaxLexical method) (KSyntaxPriority method) (KSyntaxSort method) (KTerminal method) (LocationType method) (LogEntry method) (LogRewrite method) (LogSimplification method) (NoneType method) (OptionalType method) (PathType method) (RewriteFailure method) (RewriteResult method) (RewriteSuccess method) (StrType method) (Subst method)

to_json() (KAst method) (KCFG method) to_module() (KCFG method) (KCFGShow method) to_rule() (KCFG.Edge method) to_rules() (KCFG method) toggle_option() (NodeView method) toggle_view() (NodeView method) TOKEN (Atts attribute) Token (class in pyk.kast.outer_lexer) token (KToken attribute) token() (in module pyk.prelude.utils) tokens (Format attribute) TokenType (class in pyk.kast.outer_lexer) (class in pyk.kore.lexer) Top (class in pyk.kore.syntax) top() (CTerm static method) (KoreParser method) top_cell_initializer() (in module pyk.kore.prelude) top_down() (in module pyk.kast.inner) (Pattern method) TOTAL (Atts attribute) translate_coverage() (in module pyk.coverage) translate_coverage_from_paths() (in module pyk.coverage) Transport (class in pyk.kore.rpc) TransportType (class in pyk.kore.rpc) TRUSTED (Atts attribute) try_cell() (CTerm method) tuple_of() (in module pyk.utils) type (AttKey attribute) (KoreToken attribute) (Token attribute)

U

unapply() (Subst method) UnaryConn (class in pyk.kore.syntax) uncovered (KCFG property) undo_aliases() (in module pyk.kast.manip) union() (Subst method) unique() (in module pyk.utils) UNIQUE_ID (Atts attribute) unique_id (KSentence property) UNIT (Atts attribute) unknown_predicate (AbortedResult attribute) UnknownModuleError UnknownResult (class in pyk.kore.rpc) unparse() (Format method) UNPARSE_AVOID (Atts attribute)

unparser_for_production() (in module pyk.kast.pretty) unrefute_node() (APRProof method) UnsatResult (class in pyk.kore.rpc) up_to_date (Proof property) up_to_date() (KBuild method) update() (Info method) (KAtt method) (NavWidget method) (NodeView method) update_atts() (WithKAtt method) use_directory (KPrint attribute) use_server() (in module pyk.testing.plugin) useless_vars_to_dots() (in module pyk.kast.manip) USER_LIST (Atts attribute) UserList (class in pyk.kast.outer_syntax)

V

vacuous (APRSummary attribute) Vacuous (class in pyk.kcfg.kcfg) vacuous (CTermExecute attribute) (KCFG property) VACUOUS (KCFGNodeAttr attribute) (StopReason attribute) VacuousResult (class in pyk.kore.rpc) valid_id() (in module pyk.kdist.api) value (AttEntry attribute) (DV attribute) (Id attribute) (KTerminal attribute) (NodeAttr attribute) (SetVarId attribute) (String attribute) (SymbolId attribute) (Terminal attribute) var (Exists attribute) (Forall attribute) (MLFixpoint attribute) (MLQuant attribute) (Mu attribute) (Nu attribute)

var_occurrences() (in module pyk.kast.inner) var_pattern() (KoreParser method) VarPattern (class in pyk.kore.syntax) vars (Axiom attribute) (AxiomLike attribute) (Claim attribute) (SortDecl attribute) (Symbol attribute) VBAR (TokenType attribute) verbose (BehaviorView.Selected attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) version (Project attribute) version() (KAst static method)

W

WALRUS (TokenType attribute) watch_text() (Info method) (NavWidget method) with_single_target() (KCFG.MultiEdge method) (KCFG.NDBranch method) (KCFG.Split method) WithAttrs (class in pyk.kore.syntax) WithKAtt (class in pyk.kast.att) WithSort (class in pyk.kore.syntax) WRAP_ELEMENT (Atts attribute) write() (AliasDecl method) (App method) (AxiomLike method) (Definition method) (Import method) (KompiledKore method) (Kore method) (MLPattern method) (Module method) (SortApp method) (SortDecl method) (SortVar method) (String method) (Symbol method) (SymbolDecl method) (VarPattern method)

write_cfg_data() (KCFG method) (KCFGStore method) write_proof() (Proof method) write_proof_data() (APRProof method) (ImpliesProof method) (Proof method)

X

xor_bool() (in module pyk.kore.prelude)

Z

zero_depth_between() (KCFG method)