Index

_

__call__() (CSubst method) (Subst method) __format__() (LogOrigin method) (StopReason method) __getitem__() (Subst method) __init__() (CSubst method) (CTerm method) (KApply method) (KAs method) (KLabel method) (KoreHeader method) (KRewrite method) (KSequence method) (KSort method) (KToken method) (KVariable method) (LLVMArgument method) (LLVMEventAnnotated method) (LLVMEventType method) (LLVMFunctionEvent method) (LLVMHookEvent method) (LLVMPatternMatchingFailureEvent method) (LLVMRewriteTrace method) (LLVMRewriteTraceIterator method) (LLVMRuleEvent method) (LLVMSideConditionEventEnter method) (LLVMSideConditionEventExit method) (Subst method) __iter__() (CSubst method) (CTerm method) (KLabel method) (KRewrite method) (LLVMRewriteTraceIterator method) (Subst method)

__len__() (Subst method) __lt__() (KVariable method) __mul__() (Subst method) __next__() (LLVMRewriteTraceIterator method) __repr__() (LLVMArgument method) (LLVMFunctionEvent method) (LLVMHookEvent method) (LLVMPatternMatchingFailureEvent method) (LLVMRewriteTrace method) (LLVMRewriteTraceIterator method) (LLVMRuleEvent method) (LLVMSideConditionEventEnter method) (LLVMSideConditionEventExit method) _annotated_llvm_event (LLVMEventAnnotated attribute) _argument (LLVMArgument attribute) _event_type (LLVMEventType attribute) _function_event (LLVMFunctionEvent attribute) _hook_event (LLVMHookEvent attribute) _kore_header (KoreHeader attribute) _pattern_matching_failure_event (LLVMPatternMatchingFailureEvent attribute) _rewrite_trace (LLVMRewriteTrace attribute) _rewrite_trace_iterator (LLVMRewriteTraceIterator attribute) _rule_event (LLVMRuleEvent attribute) _side_condition_end_event (LLVMSideConditionEventExit attribute) _side_condition_event (LLVMSideConditionEventEnter attribute)

A

ABORTED (FallbackReason attribute) (StopReason attribute) AbortedResult (class in pyk.kore.rpc) abs_or_rel_to() (in module pyk.utils) absInt() (in module pyk.prelude.kint) 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_brackets() (in module pyk.kast.formatter) 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_request() (BugReport 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) addInt() (in module pyk.prelude.kint) 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) ALICE_BLUE (Color attribute) all_files (Project property) all_module_names (KDefinition property) all_modules (KDefinition attribute) all_modules_dict (KDefinition property) 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) andInt() (in module pyk.prelude.kint) ansi_code (Color property) antecedent (ImpliesProof attribute) anti_left (FunctionRule attribute) anti_unify() (CTerm method) (in module pyk.cterm.cterm) ANTIQUE_WHITE (Color attribute) AnyType (class in pyk.kast.att) ANYWHERE (Atts attribute) app (Assoc property) App (class in pyk.kore.syntax) 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) AppRule (class in pyk.kore.rule) APRFailureInfo (class in pyk.proof.reachability) APRICOT (Color attribute) APRProof (class in pyk.proof.reachability) APRProofBehaviorView (class in pyk.proof.tui) APRProofBoundedResult (class in pyk.proof.reachability) APRProofExtendAndCacheResult (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) APRProofStep (class in pyk.proof.reachability)

APRProofSubsumeResult (class in pyk.proof.reachability) APRProofTerminalResult (class in pyk.proof.reachability) APRProofUseCacheResult (class in pyk.proof.reachability) APRProofViewer (class in pyk.proof.tui) APRProver (class in pyk.proof.reachability) APRSummary (class in pyk.proof.reachability) AQUA (Color attribute) AQUAMARINE (Color attribute) arg() (in module pyk.kore.match) arg_sorts (FunctionRule attribute) args (App attribute) (Assoc attribute) (KApply attribute) (LeftAssoc attribute) (LLVMFunctionEvent property) (LLVMHookEvent property) (RightAssoc attribute) (Sort attribute) (SortDecl attribute) (Target attribute) args() (in module pyk.kore.match) argument_sorts (KProduction property) arity (KApply property) (KSequence property) as_rule() (APRProof method) as_rules() (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 (APRProver attribute) (ImpliesProver attribute) 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) attrs_by_key (WithAttrs property) Atts (class in pyk.kast.att) atts (KAtt attribute) AttType (class in pyk.kast.att) AVOID (Atts attribute) Axiom (class in pyk.kore.syntax) axiom() (KoreParser method) AxiomLike (class in pyk.kore.syntax) axioms (Definition property) (Module property) AZURE (Color attribute)

B

backend (KPrint attribute) BaseRepl (class in pyk.krepl.repl) BehaviorView (class in pyk.kcfg.tui) BehaviorView.Selected (class in pyk.kcfg.tui) BEIGE (Color attribute) 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) BISQUE (Color attribute) BITTERSWEET (Color attribute) BLACK (Color attribute) BLANCHED_ALMOND (Color attribute) blocks (SyntaxDefn attribute) BLUE (Color attribute) BLUE_GREEN (Color attribute) BLUE_VIOLET (Color attribute) bmc_depth (APRProof attribute) (APRProofStep 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) (PykBackend 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) BRACKET_LABEL (Atts attribute) brackets (KDefinition property) Branch (class in pyk.kcfg.kcfg) BRANCHING (FallbackReason attribute) (StopReason attribute) BranchingResult (class in pyk.kore.rpc) BRICK_RED (Color attribute) BROWN (Color attribute) 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) builtin_dir (KDistribution property) BURLY_WOOD (Color attribute) BURNT_ORANGE (Color attribute) 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

cached_node_id (APRProofUseCacheResult attribute) CADET_BLUE (Color attribute) 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_make_custom_step() (DefaultSemantics method) (KCFGSemantics method) can_progress (APRProof property) (ImpliesProof property) (Proof property) CARNATION_PINK (Color attribute) 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) CeilRule (class in pyk.kore.rule) 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) CERULEAN (Color attribute) Chainable (class in pyk.utils) CHARTREUSE (Color attribute) 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_result (LLVMSideConditionEventExit property) check_type() (in module pyk.utils) CHOCOLATE (Color attribute) chunk_id (GraphChunk.Selected attribute) circularities_module_name (APRProof property) circularity (APRProof attribute) (APRProofStep attribute) CIRCULARITY (Atts attribute) circularity_rule_id (APRProofStep attribute) Claim (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) claim() (KoreParser method) ClaimIndex (class in pyk.ktool.claim_index) ClaimLoader (class in pyk.ktool.claim_loader) claims (ClaimIndex attribute) (KFlatModule property) close() (APRProver method) (HttpTransport method) (ImpliesProver method) (JsonRpcClient method) (JsonRpcClientFacade method) (KoreClient method) (KoreServer method) (KoreServerPool method) (Prover method) (SingleSocketTransport method) (Transport method) code (CodeBlock attribute) (DefaultError attribute) code_blocks() (in module pyk.kast.markdown) CodeBlock (class in pyk.kast.markdown) col (Loc attribute) collapse_dots() (in module pyk.kast.manip) collect() (in module pyk.kast.inner) (Pattern method) collect_symbols() (in module pyk.kore.manip) COLON (TokenType attribute), [1], [2] COLOR (Atts attribute) Color (class in pyk.kast.color) COLORS (Atts attribute) ColorsType (class in pyk.kast.att) ColorType (class in pyk.kast.att) COMM (Atts attribute) COMMA (TokenType attribute), [1], [2] command (BoosterServerArgs attribute) (KoreServerArgs attribute) (KRun attribute) commit() (APRProof method) (ImpliesProof method) (Proof 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) compute_ordinals() (Definition method) CONCAT (Atts attribute) CONCRETE (Atts attribute) condition (NextState 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_merged_edge() (KCFG method) contains_ndbranch() (KCFG method) contains_node() (KCFG method) contains_split() (KCFG method) contents (KBubble attribute) Context (class in pyk.kast.outer_syntax) context (ImplicationError attribute) (InvalidModuleError attribute) (PatternError attribute) CONTEXT (State attribute) context() (Target method) CORAL (Color attribute) CORNFLOWER_BLUE (Color attribute) CORNSILK (Color attribute) 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() (KDistribution static method) (KoreHeader static method) create_cover() (KCFG method) create_cover_map() (in module pyk.kcovr) create_edge() (KCFG method) create_merged_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_split_by_nodes() (KCFG method) create_temp() (KBuildEnv static method) CRIMSON (Color attribute) 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) cterms_anti_unify() (in module pyk.cterm.cterm) CTermSMTError CTermSymbolic (class in pyk.cterm.symbolic) ctor_patterns (DV property) (MLFixpoint property) (MLPattern property) (MLQuant property) ctor_symbols (KoreDefn property) ctx (RewriteRule attribute) Custom (class in pyk.kcfg.tui) custom_step() (DefaultSemantics method) (KCFGSemantics method) 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) CYAN (Color attribute)

D

DANDELION (Color attribute) DARK_BLUE (Color attribute) DARK_CYAN (Color attribute) DARK_GOLDENROD (Color attribute) DARK_GRAY (Color attribute) DARK_GREEN (Color attribute) DARK_GREY (Color attribute) DARK_KHAKI (Color attribute) DARK_MAGENTA (Color attribute) DARK_OLIVE_GREEN (Color attribute) DARK_ORANGE (Color attribute) DARK_ORCHID (Color attribute) DARK_RED (Color attribute) DARK_SALMON (Color attribute) DARK_SEA_GREEN (Color attribute) DARK_SLATE_BLUE (Color attribute) DARK_SLATE_GRAY (Color attribute) DARK_SLATE_GREY (Color attribute) DARK_TURQUOISE (Color attribute) DARK_VIOLET (Color attribute) DARKGRAY (Color attribute) 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) DEEP_PINK (Color attribute) DEEP_SKY_BLUE (Color attribute) DEFAULT (State attribute), [1] default_format (KProduction property) DefaultError DefaultSemantics (class in pyk.kcfg.semantics) Definition (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) definition (Formatter attribute) (KPrint property) (PrettyPrinter attribute) definition() (KoreParser method) (OuterParser method) definition_dir (KFuzz attribute) (KInterpreter attribute) (KPrint attribute) (KState attribute) definition_dir() (KBuild method) definition_hash (KPrint property) definition_to_llvm() (in module pyk.kllvm.convert) defunctionalize() (in module pyk.kast.manip) dependencies (KClaim property) (Project attribute) dependencies_module_name (APRProof property) 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) 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) DIM_GRAY (Color attribute) DIM_GREY (Color attribute) direct_subproof_rules (APRProver attribute) dirty (KVersion.Git attribute) discard() (KAtt method) discard_attr() (KCFG method) (KCFG.Node method) discard_stuck() (KCFG method) discard_vacuous() (KCFG method) divInt() (in module pyk.prelude.kint) do_load() (BaseRepl method) (KRepl method) do_show() (BaseRepl method) do_step() (BaseRepl method) DODGER_BLUE (Color attribute) dot() (APRProofShow method) (KCFGShow method) DOTK (TokenType attribute) DOTKLIST (TokenType attribute) 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.MergedEdge attribute) (KCFG.NDBranch property) edges() (KCFG method) elem_var() (KoreParser method) ELEMENT (Atts attribute) EMERALD (Color attribute) empty_config() (KDefinition method) enquote_bytes() (in module pyk.dequote) enquote_string() (in module pyk.dequote) enquoted() (in module pyk.dequote) ens (AppRule attribute) (CeilRule attribute) (EqualsRule attribute) (FunctionRule attribute) (RewriteRule attribute) (Rule attribute) ensure_dir_path() (in module pyk.utils) ensures (KClaim attribute) (KRule attribute) (KRuleLike attribute) entries() (KAtt method) eof (KoreParser property) EOF (TokenType attribute), [1], [2] eof() (KAstParser method) 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) EqualsRule (class in pyk.kore.rule) error (ImplicationError attribute) (InvalidModuleError attribute) (ParseError attribute) (PatternError attribute) (SmtSolverError attribute)

error_info (APRProof attribute) euclidDivInt() (in module pyk.prelude.kint) euclidModInt() (in module pyk.prelude.kint) eval() (And method) (Atom method) (Not method) (Or method) (Selector method) evaluate() (Runtime method) EVar (class in pyk.kore.syntax) event (LLVMEventAnnotated property) 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 (Atts attribute) exit_with_process_error() (in module pyk.utils) expInt() (in module pyk.prelude.kint) explorable (KCFGExploration property) expModInt() (in module pyk.prelude.kint) extend() (KCFG method) extend_cterm() (KCFGExplore method) extension_to_apply (APRProofExtendResult attribute) extension_to_cache (APRProofExtendAndCacheResult attribute) extra_module (APRProver attribute) extract_all() (Rule static 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) FIRE_BRICK (Color attribute) flatten_label() (in module pyk.kast.inner) Floor (class in pyk.kore.syntax) floor() (KoreParser method) FLORAL_WHITE (Color attribute) for_definition() (KompiledKore static method) (KoreSortTable static method) (KoreSymbolTable static method) Forall (class in pyk.kore.syntax) forall() (KoreParser method) FOREST_GREEN (Color attribute) FORMAT (Atts attribute) Format (class in pyk.kast.att) format() (Formatter method) formatted_exec_time (APRSummary attribute) formatted_exec_time() (APRProof method) Formatter (class in pyk.kast.formatter) 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_axiom() (AppRule static method) (CeilRule static method) (EqualsRule static method) (FunctionRule static method) (RewriteRule static method) (Rule static method) from_claim() (APRProof static method) (EqualityProof static method) (KCFG static method) from_definition() (KoreDefn static method) from_dict() (AbortedResult class method) (AnyType method) (APRProof class method) (AttType method) (BranchingResult class method) (ColorsType method) (ColorType 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.MergedEdge 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) (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_file() (LLVMRewriteTraceIterator static method) from_json() (KCFG static method) (KInner static method) (Pattern static method) (Sort static method) from_kast() (CTerm static method) from_module_list() (ClaimIndex static method) from_pred() (CSubst static method) (Subst static method) from_proof() (APRFailureInfo static method) from_spec_modules() (APRProof static method) FrozenDict (class in pyk.utils) FUCHSIA (Color attribute) full_name (TargetId property) full_printer (NodePrinter attribute) FUNCTION (Atts attribute) function_labels (KDefinition property) function_name (LLVMPatternMatchingFailureEvent property) FUNCTIONAL (Atts attribute) FunctionRule (class in pyk.kore.rule) functions (KDefinition property) (KFlatModule property) (KoreDefn attribute) fuzz() (in module pyk.ktool.kfuzz) fuzz_with_check() (KFuzz method) fuzz_with_exit_code() (KFuzz method)

G

GAINSBORO (Color attribute) 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) general_edges() (KCFG method) generate_hints() (in module pyk.kllvm.compiler) generated_counter() (in module pyk.kore.prelude) generated_top() (in module pyk.kore.prelude) get() (KAtt method) get_axiom_by_ordinal() (Definition method) get_claim_index() (KProve method) get_claims() (KProve method) get_kllvm() (in module pyk.kllvm.load_static) get_model() (CTermSymbolic method) (KoreClient method) get_node() (KCFG method) get_refutation_id() (APRProof method) get_requires() (in module pyk.kllvm.utils) get_rule_by_id() (in module pyk.coverage)

get_steps() (APRProof method) (ImpliesProof method) (Proof method) get_target() (Project method) GetModelResult (class in pyk.kore.rpc) GHOST_WHITE (Color attribute) git (KVersion attribute) GOLD (Color attribute) GOLDENROD (Color attribute) GraphChunk (class in pyk.kcfg.tui) GraphChunk.Selected (class in pyk.kcfg.tui) GRAY (Color attribute) greatest_common_subsort() (KDefinition method) GREEN (Color attribute) GREEN_YELLOW (Color attribute) GREY (Color attribute) GROUP (Atts attribute) groups (SyntaxPriority attribute) GT (TokenType attribute) gt_int() (in module pyk.kore.prelude) gtInt() (in module pyk.prelude.kint)

H

handle_failure() (KFuzzHandler method) handle_test() (KFuzzHandler method) handler (KFuzz attribute) 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 (PykBackend attribute) haskell_log_entries (BoosterServerArgs attribute) (KoreServerArgs attribute) haskell_log_format (BoosterServerArgs attribute) (KoreServerArgs attribute)

haskell_threads (BoosterServerArgs attribute) (KoreServerArgs attribute) HaskellLogEntry (class in pyk.kore_exec_covr.kore_exec_covr) heuristic (Branch attribute) hide_cells() (KCFGShow static method) HONEYDEW (Color attribute) HOOK (Atts attribute) hooked (SortDecl attribute) (SymbolDecl attribute) hooked_sort_decl() (KoreParser method) hooked_symbol_decl() (KoreParser method) host (KoreServer property) (KoreServerInfo attribute) HOT_PINK (Color 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), [1] 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) ImpliesProofStep (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.rewrite) INDIAN_RED (Color attribute) INDIGO (Color attribute) infer_sort() (KoreSymbolTable method) info (Branch attribute) Info (class in pyk.kcfg.tui) info (CodeBlock attribute) (Step attribute) init (APRProof attribute) init_config() (KDefinition method) init_generated_top_cell() (in module pyk.kore.prelude) init_proof() (APRProver method) (ImpliesProver method) (Prover method) init_state() (Interpreter method) (KInterpreter method) initial_config (LLVMRewriteTrace property) INITIALIZER (Atts attribute)

inj() (in module pyk.kore.match) (in module pyk.kore.prelude) (in module pyk.prelude.k) 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_initial_config (LLVMEventType property) is_kore_pattern() (LLVMArgument method) is_leaf() (KCFG method) is_loop() (DefaultSemantics method) (KCFGSemantics method) is_mergeable() (DefaultSemantics method) (KCFGSemantics method) is_ndbranch() (KCFG method) is_pending() (APRProof method) is_pre_trace (LLVMEventType property) is_prefix (KProduction property) is_record (KProduction property) is_refuted() (APRProof method) is_root() (KCFG method) is_rule() (Rule static method) is_split() (KCFG method) is_spurious_constraint() (in module pyk.kast.manip) is_step_event() (LLVMArgument 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_trace (LLVMEventType property) is_trusted (KClaim property) is_vacuous() (KCFG method) items (Att attribute) (KProduction attribute) (KSequence attribute) (Production attribute) IVORY (Color 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) JUNGLE_GREEN (Color attribute)

K

k() (in module pyk.kore.prelude) (KAstParser method) 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) KAstParser (class in pyk.kast.parser) 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) (KCFGMinimizer attribute) KCFG.Cover (class in pyk.kcfg.kcfg) KCFG.Edge (class in pyk.kcfg.kcfg) KCFG.EdgeLike (class in pyk.kcfg.kcfg) KCFG.MergedEdge (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 (APRProver attribute) (ImpliesProver 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) KCFGMinimizer (class in pyk.kcfg.minimize) 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) kdef (KCFGMinimizer attribute) KDefinition (class in pyk.kast.outer) kdist_dir (KBuild attribute) KDistribution (class in pyk.ktool.utils) key (AttEntry attribute) keys() (Atts class method) KFlatModule (class in pyk.kast.outer) KFlatModuleList (class in pyk.kast.outer) KFuzz (class in pyk.ktool.kfuzz) KFuzzHandler (class in pyk.ktool.kfuzz) KHAKI (Color attribute) KImport (class in pyk.kast.outer) KInner (class in pyk.kast.inner) kintegers() (in module pyk.ktool.kfuzz) KInterpreter (class in pyk.krepl.repl) kitem() (KAstParser method) KLabel (class in pyk.kast.inner) klabel (KProduction attribute) KLABEL (State attribute) (TokenType attribute), [1] klabel() (KAstParser method) klabels (SyntaxAssoc attribute) klist() (KAstParser method) KNonTerminal (class in pyk.kast.outer) kompile() (in module pyk.ktool.kompile) (in module pyk.testing.plugin) (KBuild method) (KBuildEnv method) kompiled_dir (BoosterServerArgs attribute) (KoreServerArgs attribute) KompiledKore (class in pyk.kore.kompiled) Kore (class in pyk.kore.syntax) KORE (KAstInput attribute) (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) (PykBackend 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_pattern (LLVMArgument property) kore_print() (in module pyk.kore.tools) kore_rangemap_of() (in module pyk.kore.match) 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_symbol() (Assoc class method) (LeftAssoc class method) (RightAssoc class method) 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 KoreDefn (class in pyk.kore.internal) KoreExecLogFormat (class in pyk.kore.rpc) KoreHeader (class in pyk.kllvm.hints.prooftrace) 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 (TokenType attribute) 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) (RewriteRule attribute) (Rule attribute) (StringSentence attribute) labels() (ClaimIndex method) labels_to_dots() (in module pyk.kast.manip) last_constraint (RefutationProof property) LATEX (KAstOutput attribute) (KProveOutput attribute) (KRunOutput attribute) (PrintOutput attribute) LAVENDER (Color attribute) LAVENDER_BLUSH (Color attribute) LAWN_GREEN (Color 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) left_assocs (KDefinition property) LeftAssoc (class in pyk.kore.syntax) leInt() (in module pyk.prelude.kint) LEMON_CHIFFON (Color attribute) 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) (KoreDefn 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) (Token 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) lexer() (in module pyk.kast.lexer) Lexical (class in pyk.kast.outer_syntax) lhs (AppRule attribute) (CeilRule attribute) (EqualsRule attribute) (FunctionRule attribute) (KRewrite attribute) (RewriteRule attribute) (Rule attribute) (SimpliRule attribute) lhs_body (EqualityProof property) lift_edge() (KCFGMinimizer method) lift_edges() (KCFGMinimizer method) lift_split_edge() (KCFGMinimizer method) lift_split_split() (KCFGMinimizer method) lift_splits() (KCFGMinimizer method) LIGHT_BLUE (Color attribute) LIGHT_CORAL (Color attribute) LIGHT_CYAN (Color attribute) LIGHT_GOLDENROD (Color attribute) LIGHT_GOLDENROD_YELLOW (Color attribute) LIGHT_GRAY (Color attribute) LIGHT_GREEN (Color attribute) LIGHT_GREY (Color attribute) LIGHT_PINK (Color attribute) LIGHT_SALMON (Color attribute) LIGHT_SEA_GREEN (Color attribute) LIGHT_SKY_BLUE (Color attribute) LIGHT_SLATE_BLUE (Color attribute) LIGHT_SLATE_GRAY (Color attribute) LIGHT_SLATE_GREY (Color attribute) LIGHT_STEEL_BLUE (Color attribute) LIGHT_YELLOW (Color attribute) LIGHTGRAY (Color attribute) LIME (Color attribute) LIME_GREEN (Color attribute) line (Loc attribute) LINEN (Color attribute) 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 (LogOrigin attribute) (PykBackend attribute) llvm_interpret() (in module pyk.ktool.krun) llvm_interpret_raw() (in module pyk.ktool.krun) llvm_kompiled_dir (BoosterServerArgs attribute) llvm_to_definition() (in module pyk.kllvm.convert) llvm_to_module() (in module pyk.kllvm.convert) llvm_to_pattern() (in module pyk.kllvm.convert) llvm_to_sentence() (in module pyk.kllvm.convert) llvm_to_sort() (in module pyk.kllvm.convert) llvm_to_sort_var() (in module pyk.kllvm.convert) LLVMArgument (class in pyk.kllvm.hints.prooftrace) LLVMEventAnnotated (class in pyk.kllvm.hints.prooftrace) LLVMEventType (class in pyk.kllvm.hints.prooftrace) LLVMFunctionEvent (class in pyk.kllvm.hints.prooftrace) LLVMHookEvent (class in pyk.kllvm.hints.prooftrace) LLVMPatternMatchingFailureEvent (class in pyk.kllvm.hints.prooftrace) LLVMRewriteEvent (class in pyk.kllvm.hints.prooftrace) LLVMRewriteTrace (class in pyk.kllvm.hints.prooftrace) LLVMRewriteTraceIterator (class in pyk.kllvm.hints.prooftrace) LLVMRuleEvent (class in pyk.kllvm.hints.prooftrace) LLVMSideConditionEventEnter (class in pyk.kllvm.hints.prooftrace) LLVMSideConditionEventExit (class in pyk.kllvm.hints.prooftrace) LLVMStepEvent (class in pyk.kllvm.hints.prooftrace) load() (KompiledKore static method) (Project static method) load_claims() (ClaimLoader method) load_from_dir() (Project static method) load_from_json() (KompiledKore static method) load_from_kore() (KompiledKore static method) Loc (class in pyk.kast.outer_lexer) loc (LocationIterator property) (Token attribute) location (AST attribute) LOCATION (Atts attribute) LocationIterator (class in pyk.kast.outer_lexer) LocationType (class in pyk.kast.att) log_axioms_file (BoosterServerArgs attribute) (KoreServerArgs attribute) log_context (BoosterServerArgs 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) LPAREN (TokenType attribute), [1], [2] lshiftInt() (in module pyk.prelude.kint) 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) MAGENTA (Color attribute) MAHOGANY (Color attribute) main() (in module pyk.kcovr) main_file (KProve attribute) main_module (KDefinition attribute) (KFlatModuleList attribute) (KPrint attribute) main_module_name (APRProver attribute) (ClaimIndex 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) MAROON (Color attribute) 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_rangemap() (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 (PykBackend attribute) maxInt() (in module pyk.prelude.kint) maybe() (in module pyk.utils) MEDIUM_AQUAMARINE (Color attribute) MEDIUM_BLUE (Color attribute) MEDIUM_ORCHID (Color attribute) MEDIUM_PURPLE (Color attribute) MEDIUM_SEA_GREEN (Color attribute) MEDIUM_SLATE_BLUE (Color attribute) MEDIUM_SPRING_GREEN (Color attribute) MEDIUM_TURQUOISE (Color attribute) MEDIUM_VIOLET_RED (Color attribute) meet() (KoreSortTable method) MELON (Color attribute) merge_nodes() (KCFGMinimizer method) merge_with() (in module pyk.utils) merged_edge() (KCFG method) merged_edges() (KCFG method) message (DefaultError attribute) MIDNIGHT_BLUE (Color attribute) minimize (NodePrinter attribute) minimize() (KCFGMinimizer method) (Subst method) minimize_kcfg() (KCFGExploration method) minimize_rule_like() (in module pyk.kast.manip) minimize_term() (in module pyk.kast.manip) minInt() (in module pyk.prelude.kint) minor (KVersion attribute) MINT_CREAM (Color attribute) MISTY_ROSE (Color 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_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) mlTop() (in module pyk.prelude.ml) MOCCASIN (Color attribute) model (SatResult attribute) models (APRFailureInfo attribute) modInt() (in module pyk.prelude.kint) 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.color pyk.kast.formatter pyk.kast.inner pyk.kast.kast pyk.kast.lexer pyk.kast.manip pyk.kast.markdown pyk.kast.outer pyk.kast.outer_lexer pyk.kast.outer_parser pyk.kast.outer_syntax pyk.kast.parser pyk.kast.pretty pyk.kast.rewrite pyk.kast.utils 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.minimize 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.ast pyk.kllvm.compiler pyk.kllvm.convert pyk.kllvm.hints pyk.kllvm.hints.prooftrace pyk.kllvm.importer pyk.kllvm.load pyk.kllvm.load_static pyk.kllvm.parser pyk.kllvm.runtime pyk.kllvm.utils pyk.konvert pyk.kore pyk.kore.internal 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.rule 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.claim_index pyk.ktool.claim_loader pyk.ktool.kfuzz pyk.ktool.kompile pyk.ktool.kprint pyk.ktool.kprove pyk.ktool.krun pyk.ktool.prove_rpc pyk.ktool.utils 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.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) (APRProofStep attribute) (BoosterServerArgs attribute) (DuplicateModuleError attribute) (Import attribute), [1] (KoreServerArgs attribute) (UnknownModuleError attribute) module_names (KDefinition property) module_to_llvm() (in module pyk.kllvm.convert) modules (Definition attribute), [1] (KDefinition property) (KFlatModuleList attribute) Mu (class in pyk.kore.syntax) mu() (KoreParser method) MULBERRY (Color attribute) mulInt() (in module pyk.prelude.kint) multi_or() (KoreParser method) MultiaryConn (class in pyk.kore.syntax) MULTIPLICITY (Atts attribute)

N

name (Atom attribute) (AttKey attribute) (EVar attribute) (KFlatModule attribute) (KImport attribute) (KLabel attribute) (KNonTerminal attribute) (KSort attribute) (KSyntaxLexical attribute) (KVariable attribute) (LLVMFunctionEvent property) (LLVMHookEvent property) (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) NAVAJO_WHITE (Color attribute) NavWidget (class in pyk.kcfg.tui) NavWidget.Selected (class in pyk.kcfg.tui) NAVY (Color attribute) NAVY_BLUE (Color attribute) NDBranch (class in pyk.kcfg.kcfg) ndbranches() (KCFG method) ne_bool() (in module pyk.kore.prelude) ne_int() (in module pyk.kore.prelude) neqInt() (in module pyk.prelude.kint) 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)

NextState (class in pyk.cterm.symbolic) no_cell_rewrite_to_dots() (in module pyk.kast.manip) no_dispatch (BehaviorView.Selected attribute) (GraphChunk.Selected attribute) (NavWidget.Selected attribute) NO_EVALUATORS (Atts attribute) no_post_exec_simplify (BoosterServerArgs attribute) node (APRProofStep 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 (APRProofStep attribute) nonzero_depth() (APRProof method) normalize_constraints() (in module pyk.kast.manip) normalize_ml_pred() (in module pyk.kast.manip) Not (class in pyk.kast.markdown) (class in pyk.kore.syntax) not_bool() (in module pyk.kore.prelude) not_log_context (BoosterServerArgs attribute) not_none() (in module pyk.utils) notBool() (in module pyk.prelude.kbool) notInt() (in module pyk.prelude.kint) 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) (MLPattern class method) (Mu class method) (Next class method) (Not class method) (Nu class method) (Or class method) (Rewrites class method) (Top class method) old (SyntaxSynonym attribute) OLD_LACE (Color attribute) old_sort (KSortSynonym attribute) OLIVE (Color attribute) OLIVE_DRAB (Color attribute) OLIVE_GREEN (Color 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) one_line_summary (APRProof property) (Proof property) 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] optimize_kcfg (APRProofResult attribute) (APRProver attribute) 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) ORANGE (Color attribute) ORANGE_RED (Color attribute) orBool() (in module pyk.prelude.kbool) ORCHID (Color attribute) origin (LogRewrite attribute) orInt() (in module pyk.prelude.kint) 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) PALE_GOLDENROD (Color attribute) PALE_GREEN (Color attribute) PALE_TURQUOISE (Color attribute) PALE_VIOLET_RED (Color attribute) PAPAYA_WHIP (Color attribute) parallel_advance_proof() (in module pyk.proof.proof) param_sorts (AliasDecl attribute) (SymbolDecl attribute) params (KLabel attribute) (KProduction attribute) (KSyntaxSort attribute) (SortDecl attribute) paren() (in module pyk.kast.pretty) parse() (AnyType method) (AttType method) (ColorsType method) (ColorType method) (Format class method) (FormatType method) (IntType method) (KAtt class method) (KVersion static method) (LLVMRewriteTrace static method) (LocationType method) (NoneType method) (OptionalType method) (PathType method) (SelectorParser method) (StrType method) (TargetId static method) parse_args() (in module pyk.kcovr) parse_definition() (in module pyk.kllvm.parser) parse_definition_file() (in module pyk.kllvm.parser) parse_modules() (KProve method) parse_outer() (in module pyk.kast.utils) parse_pattern() (in module pyk.kllvm.parser) parse_pattern_file() (in module pyk.kllvm.parser) parse_rule_applications() (in module pyk.kore_exec_covr.kore_exec_covr) parse_sort() (in module pyk.kllvm.parser) parse_sort_file() (in module pyk.kllvm.parser) parse_tags() (in module pyk.kast.markdown) parse_token() (KPrint method) ParseError partition() (in module pyk.utils) passed (Proof property) PASSED (ProofStatus attribute) patch (KVersion attribute) path (KBuildEnv attribute) (KDistribution attribute), [1] (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) pattern_to_llvm() (in module pyk.kllvm.convert) 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) PEACH (Color attribute) PEACH_PUFF (Color attribute) pending (APRProof property) (APRSummary attribute) PENDING (ProofStatus attribute) pending_nodes (APRFailureInfo attribute) PERIWINKLE (Color attribute) PERU (Color attribute) pid (KoreServer property) (KoreServerInfo attribute) PINE_GREEN (Color attribute) PINK (Color attribute) plugin_name (TargetId attribute) PLUM (Color attribute) PLUS (TokenType attribute) port (BoosterServerArgs attribute) (KoreClient attribute) (KoreServer property) (KoreServerArgs attribute) (KoreServerInfo attribute) POSet (class in pyk.utils) POWDER_BLUE (Color attribute) pre_constraints (RefutationProof property) pre_trace (LLVMRewriteTrace property) pred (Subst property) pred() (CSubst method) 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() (APRProofShow method) (EqualityProof method) (KCFGShow method) (RefutationProof 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) (APRProofStep attribute) prior_loops_cache_update (APRProofResult attribute) PRIORITIES (Atts attribute) priorities (KDefinition property) (KSyntaxPriority attribute) priority (AppRule attribute) PRIORITY (Atts attribute) priority (CeilRule attribute) (EqualsRule attribute) (FunctionRule attribute) (KRule property) (RewriteRule attribute) (Rule attribute) PriorityBlock (class in pyk.kast.outer_syntax) PRIVATE (Atts attribute) PROCESS_BLUE (Color 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) project_to_rewrites() (KoreDefn method) project_to_symbols() (KoreDefn method) PROJECTION (Atts attribute) prompt (BaseRepl attribute) proof (APRProofNodePrinter attribute) Proof (class in pyk.proof.proof) proof (ImpliesProofStep attribute) (ImpliesProver attribute) proof_data_exists() (Proof static method) proof_dir (Proof attribute) proof_exists() (Proof static method) proof_id (APRProofStep attribute) proof_subdir (Proof property) ProofStatus (class in pyk.proof.proof) ProofSummary (class in pyk.proof.proof) propagate_up_constraints() (in module pyk.kast.manip) prove() (KProve method) prove_claim() (KProve method) prove_rpc() (ProveRpc method)

Prover (class in pyk.proof.proof) prover (KProve attribute) prover_args (KProve attribute) ProveRpc (class in pyk.ktool.prove_rpc) PROXY (LogOrigin attribute) prune() (APRProof method) (KCFG method) (KCFGExploration method) public (Import attribute) (KImport attribute) PURPLE (Color 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.color module pyk.kast.formatter module pyk.kast.inner module pyk.kast.kast module pyk.kast.lexer 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.parser module pyk.kast.pretty module pyk.kast.rewrite module pyk.kast.utils 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.minimize 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.ast module pyk.kllvm.compiler module pyk.kllvm.convert module pyk.kllvm.hints module pyk.kllvm.hints.prooftrace module pyk.kllvm.importer module pyk.kllvm.load module pyk.kllvm.load_static module pyk.kllvm.parser module pyk.kllvm.runtime module pyk.kllvm.utils module pyk.konvert module pyk.kore module pyk.kore.internal 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.rule 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.claim_index module pyk.ktool.claim_loader module pyk.ktool.kfuzz module pyk.ktool.kompile module pyk.ktool.kprint module pyk.ktool.kprove module pyk.ktool.krun module pyk.ktool.prove_rpc module pyk.ktool.utils 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.proof module pyk.proof.reachability module pyk.proof.show module pyk.proof.tui module pyk.testing module pyk.testing.plugin module pyk.utils module PykBackend (class in pyk.ktool.kompile) pytest_addoption() (in module pyk.testing.plugin)

Q

QUESTION (TokenType attribute)

R

raised() (in module pyk.utils) rangemap_empty() (in module pyk.prelude.collections) rangemap_item() (in module pyk.prelude.collections) rangemap_of() (in module pyk.prelude.collections) rangemap_pattern() (in module pyk.kore.prelude) RAW_SIENNA (Color attribute) 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) RED (Color attribute) RED_ORANGE (Color attribute) RED_VIOLET (Color 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) relative_position (LLVMFunctionEvent property) (LLVMHookEvent property) 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_edges_around() (KCFG method) remove_generated_cells() (in module pyk.kast.manip) remove_merged_edge() (KCFG method) 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.MergedEdge method) (KCFG.NDBranch method) (KCFG.Split method) (KCFG.Successor method) replace_target() (KCFG.Cover method) (KCFG.Edge method) (KCFG.MergedEdge method) (KCFG.NDBranch method) (KCFG.Split method) (KCFG.Successor method) replace_top() (KRewrite method) ReplError req (AppRule attribute) (CeilRule attribute) (EqualsRule attribute) (FunctionRule attribute) (RewriteRule attribute) (Rule attribute) request() (JsonRpcClient method) (JsonRpcClientFacade 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) reset() (Color static method) reset_code() (Color static method) resolve() (ClaimIndex method) (KoreSymbolTable method) (PackageSource method) (PathSource method) (Source method) resolve_all() (ClaimIndex method) resolve_sorts() (KDefinition method) resource_file_names (Project property) resource_files (Project property) resources (Project attribute) result (LLVMHookEvent property) (LogRewrite attribute) RETURNS_UNIT (Atts attribute) rev (KVersion.Git attribute) RewriteFailure (class in pyk.kore.rpc) RewriteResult (class in pyk.kore.rpc) RewriteRule (class in pyk.kore.rule) Rewrites (class in pyk.kore.syntax) rewrites (KoreDefn attribute) rewrites() (KoreParser method) RewriteSuccess (class in pyk.kore.rpc) rewritten_term (RewriteSuccess attribute) RHODAMINE (Color attribute) rhs (AppRule attribute) (CeilRule attribute) (EqualsRule attribute) (FunctionRule attribute) (KRewrite attribute) (RewriteRule attribute) (Rule 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) right_assocs (KDefinition property) RightAssoc (class in pyk.kore.syntax) root (KCFG property) ROSY_BROWN (Color attribute) RoundPred (class in pyk.kore.syntax) ROYAL_BLUE (Color attribute) ROYAL_PURPLE (Color attribute) RPAREN (TokenType attribute), [1], [2] rshiftInt() (in module pyk.prelude.kint) rtld_local() (in module pyk.kllvm.importer) RUBINE_RED (Color attribute) rule (AbortedResult attribute) (BranchingResult attribute) Rule (class in pyk.kast.outer_syntax) (class in pyk.kore.rule) rule (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) RULE (KAstInput attribute) rule (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) rule_id (APRProof property) (RewriteFailure attribute) (RewriteResult attribute) (RewriteSuccess attribute) (State attribute) RULE_LABEL (TokenType attribute) rule_labels (NDBranch attribute) (Step attribute) rule_ordinal (LLVMRewriteEvent property) (LLVMRuleEvent property) (LLVMSideConditionEventEnter property) (LLVMSideConditionEventExit property) 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) run_process_2() (in module pyk.utils) run_proof_hint() (KRun method) Runtime (class in pyk.kllvm.runtime)

S

SADDLE_BROWN (Color attribute) SALMON (Color attribute) same_loop() (DefaultSemantics method) (KCFGSemantics method) SANDY_BROWN (Color attribute) SatResult (class in pyk.kore.rpc) SEA_GREEN (Color attribute) SEASHELL (Color attribute) 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) semantics (KCFGMinimizer attribute) 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_to_llvm() (in module pyk.kllvm.convert) sentence_type (KBubble attribute) sentences (Definition property) (KFlatModule attribute) (Module attribute), [1] sep (UserList attribute) SEPIA (Color attribute) SEQSTRICT (Atts attribute) serialize() (Term method) set() (Color 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) shortest_path_to_node (APRProofStep attribute) show() (APRProofShow method) (KCFGShow method) SIENNA (Color attribute) SILVER (Color attribute) 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) SimpliRule (class in pyk.kore.rule) single() (in module pyk.utils) SINGLE_SOCKET (TransportType attribute) SingleSocketTransport (class in pyk.kore.rpc) SKY_BLUE (Color attribute) SLATE_BLUE (Color attribute) SLATE_GRAY (Color attribute) SLATE_GREY (Color attribute) slurp_definitions() (in module pyk.kast.utils) 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) SMTLEMMA (Atts attribute) SmtSolverError SNOW (Color attribute) some() (in module pyk.utils) sort (AliasDecl attribute) (And attribute) (AppRule attribute) SORT (Atts attribute) sort (Bottom attribute) (Ceil attribute) (CeilRule attribute) Sort (class in pyk.kast.outer_syntax) (class in pyk.kore.syntax) sort (DV attribute) (EqualityProof property) (Equals attribute) (EqualsRule attribute) (EVar attribute) (Exists attribute) (Floor attribute) (Forall attribute) (FunctionRule 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) (RewriteRule attribute) (Rewrites attribute) (Rule attribute) (SimpliRule attribute) SORT (State attribute) sort (SVar attribute) (SymbolDecl attribute) SORT (TokenType attribute) sort (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_to_llvm() (in module pyk.kllvm.convert) 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 attribute) (BinaryPred property) (DV property) (KoreDefn attribute) (LeftAssoc attribute) (MLConn property) (MLFixpoint property) (MLPattern property) (MLQuant property) (MLRewrite property) (RightAssoc attribute) (RoundPred property) (SortApp attribute)

SortVar (class in pyk.kore.syntax) source (AST attribute) SOURCE (Atts attribute) Source (class in pyk.kbuild.project) source (KCFG.Cover attribute) (KCFG.Edge attribute) (KCFG.EdgeLike attribute) (KCFG.MergedEdge 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) SPRING_GREEN (Color attribute) STANDARD (KoreExecLogFormat attribute) start() (KoreServer method) state (AbortedResult attribute) (BaseRepl attribute) (BranchingResult attribute) State (class in pyk.kast.lexer) (class in pyk.kast.outer_lexer) (class in pyk.kore.rpc) state (CTermExecute attribute) (CutPointResult attribute) (DepthBoundResult attribute) (ExecuteResult attribute) (NextState attribute) (StuckResult attribute) (TerminalResult attribute) (TimeoutResult attribute) (VacuousResult attribute) status (APRSummary attribute) Status (class in pyk.kcfg.tui) status (EqualitySummary attribute) (Proof property) (ProofSummary attribute) (RefutationSummary attribute) STEEL_BLUE (Color attribute) Step (class in pyk.kcfg.kcfg) step() (KCFGExplore method) (Runtime method) (Term method) step_event (LLVMArgument property) step_proof() (APRProver method) (ImpliesProver method) (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], [2] 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) subInt() (in module pyk.prelude.kint) submit() (KoreServerPool method) subproof_ids (Proof property) subproofs (APRSummary attribute) (Proof property) subproofs_status (Proof property) subsort_table (KDefinition property) subsorts (KoreDefn attribute) subsorts() (KDefinition method) Subst (class in pyk.kast.inner) subst (CSubst attribute) substitution (ImpliesResult attribute) (LLVMRewriteEvent property) (LLVMRuleEvent property) (LLVMSideConditionEventEnter property) (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) (Assoc attribute) SYMBOL (Atts attribute) Symbol (class in pyk.kore.syntax) symbol (LeftAssoc attribute) (RightAssoc attribute) (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) (MLPattern class method) (Mu class method) (Next class method) (Not class method) (Nu class method) (Or class method) (Rewrites 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) SYMBOLIC (Atts attribute) SymbolId (class in pyk.kore.syntax) symbols (KDefinition property) (KoreDefn attribute) sync() (KBuildEnv method) sync_files() (in module pyk.kbuild.utils) SYNTAX (State attribute) SYNTAX_MODULE (Atts attribute) syntax_productions (KDefinition property) (KFlatModule property) syntax_sentence() (OuterParser method) syntax_sorts (KFlatModule property) syntax_symbols (KDefinition 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) TAN (Color attribute) target (APRProof attribute) (APRProofStep attribute) Target (class in pyk.kbuild.project) (class in pyk.kdist.api) target (KCFG.Cover attribute) (KCFG.Edge attribute) (KCFG.EdgeLike attribute) (KCFG.MergedEdge 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) TEAL (Color attribute) TEAL_BLUE (Color 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) TERMINATOR_SYMBOL (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), [1] THISTLE (Color 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_axiom() (FunctionRule method) (RewriteRule method) (Rule method) (SimpliRule method) to_claim() (RefutationProof method) to_dict() (AnyType method) (AttType method) (ColorsType method) (ColorType method) (CSubst method) (CTerm method) (FormatType method) (IntType method) (KAst method) (KAtt method) (KBubble method) (KCFG method) (KCFG.Cover method) (KCFG.Edge method) (KCFG.MergedEdge 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) (NoneType method) (OptionalType method) (PathType method) (RewriteFailure method) (RewriteResult method) (RewriteSuccess method) (StrType method) (Subst method)

to_dict_no_nodes() (KCFG method) to_json() (KAst method) (KCFG method) to_module() (KCFG method) (KCFGShow method) to_rule() (KCFG.Edge method) (KCFG.MergedEdge method) to_rules() (KCFG method) toggle_option() (NodeView method) toggle_view() (NodeView method) TOKEN (Atts attribute) Token (class in pyk.kast.lexer) (class in pyk.kast.outer_lexer) token (KToken attribute) TOKEN (TokenType attribute) token() (in module pyk.prelude.utils) tokens (Format attribute) TokenType (class in pyk.kast.lexer) (class in pyk.kast.outer_lexer) (class in pyk.kore.lexer) TOMATO (Color attribute) 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) trace (LLVMRewriteTrace property) 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) TURQUOISE (Color attribute) type (AttKey attribute) TYPE (Atts attribute) type (KoreToken attribute) (LLVMEventAnnotated property) (Token attribute), [1]

U

uid (RewriteRule attribute) 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() (AnyType method) (AttType method) (ColorsType method) (ColorType method) (Format method) (FormatType method) (IntType method) (LocationType method) (NoneType method) (OptionalType method) (PathType method) (StrType 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 (Atts attribute) update() (Info method) (KAtt method) (NavWidget method) (NodeView method) update_atts() (WithKAtt method) use_cache (APRProofStep attribute) 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 (ImpliesResult attribute) 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) VARIABLE (TokenType attribute) 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 (LLVMRewriteTrace property) (LLVMRewriteTraceIterator property) (Project attribute) version() (KAst static method) VIOLET (Color attribute) VIOLET_RED (Color attribute)

W

WALRUS (TokenType attribute) watch_text() (Info method) (NavWidget method) WHEAT (Color attribute) WHITE (Color attribute) WHITE_SMOKE (Color attribute) WILD_STRAWBERRY (Color attribute) 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) (Assoc 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)

xorInt() (in module pyk.prelude.kint)

Y

YELLOW (Color attribute)

YELLOW_GREEN (Color attribute) YELLOW_ORANGE (Color attribute)

Z

zero_depth_between() (KCFG method)