pyk.kore package

Submodules

• pyk.kore.kompiled module
  • KompiledKore
    • KompiledKore.add_injections()
    • KompiledKore.for_definition()
    • KompiledKore.from_dict()
    • KompiledKore.load()
    • KompiledKore.load_from_json()
    • KompiledKore.load_from_kore()
    • KompiledKore.sort_table
    • KompiledKore.symbol_table
    • KompiledKore.to_dict()
    • KompiledKore.write()
  • KoreSortTable
    • KoreSortTable.for_definition()
    • KoreSortTable.is_subsort()
    • KoreSortTable.meet()
  • KoreSymbolTable
    • KoreSymbolTable.for_definition()
    • KoreSymbolTable.infer_sort()
    • KoreSymbolTable.pattern_sorts()
    • KoreSymbolTable.resolve()
• pyk.kore.lexer module
  • KoreToken
    • KoreToken.text
    • KoreToken.type
  • TokenType
    • TokenType.COLON
    • TokenType.COMMA
    • TokenType.EOF
    • TokenType.ID
    • TokenType.KW_ALIAS
    • TokenType.KW_AXIOM
    • TokenType.KW_CLAIM
    • TokenType.KW_ENDMODULE
    • TokenType.KW_HOOKED_SORT
    • TokenType.KW_HOOKED_SYMBOL
    • TokenType.KW_IMPORT
    • TokenType.KW_MODULE
    • TokenType.KW_SORT
    • TokenType.KW_SYMBOL
    • TokenType.KW_WHERE
    • TokenType.LBRACE
    • TokenType.LBRACK
    • TokenType.LPAREN
    • TokenType.ML_AND
    • TokenType.ML_BOTTOM
    • TokenType.ML_CEIL
    • TokenType.ML_DV
    • TokenType.ML_EQUALS
    • TokenType.ML_EXISTS
    • TokenType.ML_FLOOR
    • TokenType.ML_FORALL
    • TokenType.ML_IFF
    • TokenType.ML_IMPLIES
    • TokenType.ML_IN
    • TokenType.ML_LEFT_ASSOC
    • TokenType.ML_MU
    • TokenType.ML_NEXT
    • TokenType.ML_NOT
    • TokenType.ML_NU
    • TokenType.ML_OR
    • TokenType.ML_REWRITES
    • TokenType.ML_RIGHT_ASSOC
    • TokenType.ML_TOP
    • TokenType.RBRACE
    • TokenType.RBRACK
    • TokenType.RPAREN
    • TokenType.SET_VAR_ID
    • TokenType.STRING
    • TokenType.SYMBOL_ID
    • TokenType.WALRUS
  • kore_lexer()
• pyk.kore.manip module
  • conjuncts()
  • free_occs()
• pyk.kore.match module
  • app()
  • arg()
  • args()
  • case_symbol()
  • inj()
  • kore_bool()
  • kore_bytes()
  • kore_id()
  • kore_int()
  • kore_list_of()
  • kore_map_of()
  • kore_rangemap_of()
  • kore_set_of()
  • kore_str()
  • match_app()
  • match_dv()
  • match_inj()
  • match_left_assoc()
  • match_list()
  • match_map()
  • match_rangemap()
  • match_set()
  • match_symbol()
• pyk.kore.parser module
  • KoreParser
    • KoreParser.alias_decl()
    • KoreParser.andd()
    • KoreParser.app()
    • KoreParser.axiom()
    • KoreParser.bottom()
    • KoreParser.ceil()
    • KoreParser.claim()
    • KoreParser.definition()
    • KoreParser.dv()
    • KoreParser.elem_var()
    • KoreParser.eof
    • KoreParser.equals()
    • KoreParser.exists()
    • KoreParser.floor()
    • KoreParser.forall()
    • KoreParser.hooked_sort_decl()
    • KoreParser.hooked_symbol_decl()
    • KoreParser.id()
    • KoreParser.iff()
    • KoreParser.implies()
    • KoreParser.importt()
    • KoreParser.inn()
    • KoreParser.left_assoc()
    • KoreParser.ml_pattern()
    • KoreParser.module()
    • KoreParser.mu()
    • KoreParser.multi_or()
    • KoreParser.next()
    • KoreParser.nott()
    • KoreParser.nu()
    • KoreParser.orr()
    • KoreParser.pattern()
    • KoreParser.rewrites()
    • KoreParser.right_assoc()
    • KoreParser.sentence()
    • KoreParser.set_var()
    • KoreParser.set_var_id()
    • KoreParser.sort()
    • KoreParser.sort_app()
    • KoreParser.sort_decl()
    • KoreParser.sort_var()
    • KoreParser.string()
    • KoreParser.symbol()
    • KoreParser.symbol_decl()
    • KoreParser.symbol_id()
    • KoreParser.top()
    • KoreParser.var_pattern()
• pyk.kore.pool module
  • KoreServerPool
    • KoreServerPool.close()
    • KoreServerPool.submit()
• pyk.kore.prelude module
  • and_bool()
  • bool_dv()
  • bytes_dv()
  • dv()
  • eq_bool()
  • eq_int()
  • ge_int()
  • generated_counter()
  • generated_top()
  • gt_int()
  • implies_bool()
  • init_generated_top_cell()
  • inj()
  • int_dv()
  • json2string()
  • json_entry()
  • json_key()
  • json_list()
  • json_object()
  • json_to_kore()
  • jsons()
  • k()
  • k_config_var()
  • kore_to_json()
  • kseq()
  • le_int()
  • list_pattern()
  • lt_int()
  • map_pattern()
  • ne_bool()
  • ne_int()
  • not_bool()
  • or_bool()
  • rangemap_pattern()
  • set_pattern()
  • str_dv()
  • string2json()
  • top_cell_initializer()
  • xor_bool()
• pyk.kore.rpc module
  • AbortedResult
    • AbortedResult.depth
    • AbortedResult.from_dict()
    • AbortedResult.logs
    • AbortedResult.next_states
    • AbortedResult.reason
    • AbortedResult.rule
    • AbortedResult.state
    • AbortedResult.unknown_predicate
  • BoosterServer
  • BoosterServerArgs
    • BoosterServerArgs.bug_report
    • BoosterServerArgs.command
    • BoosterServerArgs.fallback_on
    • BoosterServerArgs.haskell_log_entries
    • BoosterServerArgs.haskell_log_format
    • BoosterServerArgs.haskell_threads
    • BoosterServerArgs.interim_simplification
    • BoosterServerArgs.kompiled_dir
    • BoosterServerArgs.llvm_kompiled_dir
    • BoosterServerArgs.log_axioms_file
    • BoosterServerArgs.log_context
    • BoosterServerArgs.module_name
    • BoosterServerArgs.no_post_exec_simplify
    • BoosterServerArgs.not_log_context
    • BoosterServerArgs.port
    • BoosterServerArgs.smt_reset_interval
    • BoosterServerArgs.smt_retry_limit
    • BoosterServerArgs.smt_tactic
    • BoosterServerArgs.smt_timeout
  • BranchingResult
    • BranchingResult.depth
    • BranchingResult.from_dict()
    • BranchingResult.logs
    • BranchingResult.next_states
    • BranchingResult.reason
    • BranchingResult.rule
    • BranchingResult.state
  • CutPointResult
    • CutPointResult.depth
    • CutPointResult.from_dict()
    • CutPointResult.logs
    • CutPointResult.next_states
    • CutPointResult.reason
    • CutPointResult.rule
    • CutPointResult.state
  • DefaultError
    • DefaultError.code
    • DefaultError.data
    • DefaultError.message
  • DepthBoundResult
    • DepthBoundResult.depth
    • DepthBoundResult.from_dict()
    • DepthBoundResult.logs
    • DepthBoundResult.next_states
    • DepthBoundResult.reason
    • DepthBoundResult.rule
    • DepthBoundResult.state
  • DuplicateModuleError
    • DuplicateModuleError.module_name
  • ExecuteResult
    • ExecuteResult.depth
    • ExecuteResult.from_dict()
    • ExecuteResult.logs
    • ExecuteResult.next_states
    • ExecuteResult.reason
    • ExecuteResult.rule
    • ExecuteResult.state
  • FallbackReason
    • FallbackReason.ABORTED
    • FallbackReason.BRANCHING
    • FallbackReason.STUCK
  • GetModelResult
    • GetModelResult.from_dict()
  • HttpTransport
    • HttpTransport.close()
  • ImplicationError
    • ImplicationError.context
    • ImplicationError.error
  • ImpliesResult
    • ImpliesResult.from_dict()
    • ImpliesResult.implication
    • ImpliesResult.logs
    • ImpliesResult.predicate
    • ImpliesResult.substitution
    • ImpliesResult.valid
  • InvalidModuleError
    • InvalidModuleError.context
    • InvalidModuleError.error
  • JsonRpcClient
    • JsonRpcClient.close()
    • JsonRpcClient.request()
  • JsonRpcClientFacade
    • JsonRpcClientFacade.close()
    • JsonRpcClientFacade.request()
  • JsonRpcError
  • KoreClient
    • KoreClient.add_module()
    • KoreClient.close()
    • KoreClient.execute()
    • KoreClient.get_model()
    • KoreClient.implies()
    • KoreClient.port
    • KoreClient.simplify()
  • KoreClientError
  • KoreExecLogFormat
    • KoreExecLogFormat.ONELINE
    • KoreExecLogFormat.STANDARD
  • KoreServer
    • KoreServer.close()
    • KoreServer.host
    • KoreServer.pid
    • KoreServer.port
    • KoreServer.start()
  • KoreServerArgs
    • KoreServerArgs.bug_report
    • KoreServerArgs.command
    • KoreServerArgs.haskell_log_entries
    • KoreServerArgs.haskell_log_format
    • KoreServerArgs.haskell_threads
    • KoreServerArgs.kompiled_dir
    • KoreServerArgs.log_axioms_file
    • KoreServerArgs.module_name
    • KoreServerArgs.port
    • KoreServerArgs.smt_reset_interval
    • KoreServerArgs.smt_retry_limit
    • KoreServerArgs.smt_tactic
    • KoreServerArgs.smt_timeout
  • KoreServerInfo
    • KoreServerInfo.host
    • KoreServerInfo.pid
    • KoreServerInfo.port
  • LogEntry
    • LogEntry.from_dict()
    • LogEntry.to_dict()
  • LogOrigin
    • LogOrigin.BOOSTER
    • LogOrigin.KORE_RPC
    • LogOrigin.LLVM
    • LogOrigin.PROXY
    • LogOrigin.__format__()
  • LogRewrite
    • LogRewrite.from_dict()
    • LogRewrite.origin
    • LogRewrite.result
    • LogRewrite.to_dict()
  • ParseError
    • ParseError.error
  • PatternError
    • PatternError.context
    • PatternError.error
  • RewriteFailure
    • RewriteFailure.from_dict()
    • RewriteFailure.reason
    • RewriteFailure.rule_id
    • RewriteFailure.to_dict()
  • RewriteResult
    • RewriteResult.from_dict()
    • RewriteResult.rule_id
    • RewriteResult.to_dict()
  • RewriteSuccess
    • RewriteSuccess.from_dict()
    • RewriteSuccess.rewritten_term
    • RewriteSuccess.rule_id
    • RewriteSuccess.to_dict()
  • SatResult
    • SatResult.model
  • SingleSocketTransport
    • SingleSocketTransport.close()
  • SmtSolverError
    • SmtSolverError.error
    • SmtSolverError.pattern
  • State
    • State.from_dict()
    • State.kore
    • State.predicate
    • State.rule_id
    • State.rule_predicate
    • State.rule_substitution
    • State.substitution
    • State.term
  • StopReason
    • StopReason.ABORTED
    • StopReason.BRANCHING
    • StopReason.CUT_POINT_RULE
    • StopReason.DEPTH_BOUND
    • StopReason.STUCK
    • StopReason.TERMINAL_RULE
    • StopReason.TIMEOUT
    • StopReason.VACUOUS
    • StopReason.__format__()
  • StuckResult
    • StuckResult.depth
    • StuckResult.from_dict()
    • StuckResult.logs
    • StuckResult.next_states
    • StuckResult.reason
    • StuckResult.rule
    • StuckResult.state
  • TerminalResult
    • TerminalResult.depth
    • TerminalResult.from_dict()
    • TerminalResult.logs
    • TerminalResult.next_states
    • TerminalResult.reason
    • TerminalResult.rule
    • TerminalResult.state
  • TimeoutResult
    • TimeoutResult.depth
    • TimeoutResult.from_dict()
    • TimeoutResult.logs
    • TimeoutResult.next_states
    • TimeoutResult.reason
    • TimeoutResult.rule
    • TimeoutResult.state
  • Transport
    • Transport.close()
    • Transport.request()
  • TransportType
    • TransportType.HTTP
    • TransportType.SINGLE_SOCKET
  • UnknownModuleError
    • UnknownModuleError.module_name
  • UnknownResult
  • UnsatResult
  • VacuousResult
    • VacuousResult.depth
    • VacuousResult.from_dict()
    • VacuousResult.logs
    • VacuousResult.next_states
    • VacuousResult.reason
    • VacuousResult.rule
    • VacuousResult.state
  • kore_server()
• pyk.kore.rule module
  • AppRule
    • AppRule.ens
    • AppRule.from_axiom()
    • AppRule.lhs
    • AppRule.priority
    • AppRule.req
    • AppRule.rhs
    • AppRule.sort
  • CeilRule
    • CeilRule.ens
    • CeilRule.from_axiom()
    • CeilRule.lhs
    • CeilRule.priority
    • CeilRule.req
    • CeilRule.rhs
    • CeilRule.sort
  • EqualsRule
    • EqualsRule.ens
    • EqualsRule.from_axiom()
    • EqualsRule.lhs
    • EqualsRule.priority
    • EqualsRule.req
    • EqualsRule.rhs
    • EqualsRule.sort
  • FunctionRule
    • FunctionRule.anti_left
    • FunctionRule.arg_sorts
    • FunctionRule.ens
    • FunctionRule.from_axiom()
    • FunctionRule.lhs
    • FunctionRule.priority
    • FunctionRule.req
    • FunctionRule.rhs
    • FunctionRule.sort
    • FunctionRule.to_axiom()
  • RewriteRule
    • RewriteRule.ctx
    • RewriteRule.ens
    • RewriteRule.from_axiom()
    • RewriteRule.label
    • RewriteRule.lhs
    • RewriteRule.priority
    • RewriteRule.req
    • RewriteRule.rhs
    • RewriteRule.sort
    • RewriteRule.to_axiom()
    • RewriteRule.uid
  • Rule
    • Rule.ens
    • Rule.extract_all()
    • Rule.from_axiom()
    • Rule.is_rule()
    • Rule.lhs
    • Rule.priority
    • Rule.req
    • Rule.rhs
    • Rule.sort
    • Rule.to_axiom()
  • SimpliRule
    • SimpliRule.lhs
    • SimpliRule.sort
    • SimpliRule.to_axiom()
• pyk.kore.syntax module
  • AliasDecl
    • AliasDecl.alias
    • AliasDecl.attrs
    • AliasDecl.left
    • AliasDecl.let()
    • AliasDecl.let_attrs()
    • AliasDecl.param_sorts
    • AliasDecl.right
    • AliasDecl.sort
    • AliasDecl.write()
  • And
    • And.let()
    • And.let_patterns()
    • And.let_sort()
    • And.of()
    • And.ops
    • And.sort
    • And.symbol()
  • App
    • App.args
    • App.let()
    • App.let_patterns()
    • App.patterns
    • App.sorts
    • App.symbol
    • App.write()
  • Assoc
    • Assoc.app
    • Assoc.args
    • Assoc.kore_symbol()
    • Assoc.pattern
    • Assoc.patterns
    • Assoc.sorts
    • Assoc.symbol
    • Assoc.write()
  • Axiom
    • Axiom.attrs
    • Axiom.let()
    • Axiom.let_attrs()
    • Axiom.pattern
    • Axiom.vars
  • AxiomLike
    • AxiomLike.pattern
    • AxiomLike.vars
    • AxiomLike.write()
  • BinaryConn
    • BinaryConn.left
    • BinaryConn.patterns
    • BinaryConn.right
  • BinaryPred
    • BinaryPred.left
    • BinaryPred.patterns
    • BinaryPred.right
    • BinaryPred.sorts
  • Bottom
    • Bottom.let()
    • Bottom.let_patterns()
    • Bottom.let_sort()
    • Bottom.of()
    • Bottom.sort
    • Bottom.symbol()
  • Ceil
    • Ceil.let()
    • Ceil.let_patterns()
    • Ceil.let_sort()
    • Ceil.of()
    • Ceil.op_sort
    • Ceil.pattern
    • Ceil.sort
    • Ceil.symbol()
  • Claim
    • Claim.attrs
    • Claim.let()
    • Claim.let_attrs()
    • Claim.pattern
    • Claim.vars
  • DV
    • DV.ctor_patterns
    • DV.let()
    • DV.let_patterns()
    • DV.let_sort()
    • DV.of()
    • DV.patterns
    • DV.sort
    • DV.sorts
    • DV.symbol()
    • DV.value
  • Definition
    • Definition.attrs
    • Definition.axioms
    • Definition.compute_ordinals()
    • Definition.get_axiom_by_ordinal()
    • Definition.let()
    • Definition.let_attrs()
    • Definition.modules
    • Definition.write()
  • EVar
    • EVar.let()
    • EVar.let_patterns()
    • EVar.let_sort()
    • EVar.name
    • EVar.sort
  • Equals
    • Equals.left
    • Equals.let()
    • Equals.let_patterns()
    • Equals.let_sort()
    • Equals.of()
    • Equals.op_sort
    • Equals.right
    • Equals.sort
    • Equals.symbol()
  • Exists
    • Exists.let()
    • Exists.let_patterns()
    • Exists.let_sort()
    • Exists.of()
    • Exists.pattern
    • Exists.sort
    • Exists.symbol()
    • Exists.var
  • Floor
    • Floor.let()
    • Floor.let_patterns()
    • Floor.let_sort()
    • Floor.of()
    • Floor.op_sort
    • Floor.pattern
    • Floor.sort
    • Floor.symbol()
  • Forall
    • Forall.let()
    • Forall.let_patterns()
    • Forall.let_sort()
    • Forall.of()
    • Forall.pattern
    • Forall.sort
    • Forall.symbol()
    • Forall.var
  • Id
    • Id.value
  • Iff
    • Iff.left
    • Iff.let()
    • Iff.let_patterns()
    • Iff.let_sort()
    • Iff.of()
    • Iff.right
    • Iff.sort
    • Iff.symbol()
  • Implies
    • Implies.left
    • Implies.let()
    • Implies.let_patterns()
    • Implies.let_sort()
    • Implies.of()
    • Implies.right
    • Implies.sort
    • Implies.symbol()
  • Import
    • Import.attrs
    • Import.let()
    • Import.let_attrs()
    • Import.module_name
    • Import.write()
  • In
    • In.left
    • In.let()
    • In.let_patterns()
    • In.let_sort()
    • In.of()
    • In.op_sort
    • In.right
    • In.sort
    • In.symbol()
  • Kore
    • Kore.text
    • Kore.write()
  • LeftAssoc
    • LeftAssoc.args
    • LeftAssoc.kore_symbol()
    • LeftAssoc.let()
    • LeftAssoc.let_patterns()
    • LeftAssoc.pattern
    • LeftAssoc.sorts
    • LeftAssoc.symbol
  • MLConn
    • MLConn.sorts
  • MLFixpoint
    • MLFixpoint.ctor_patterns
    • MLFixpoint.pattern
    • MLFixpoint.patterns
    • MLFixpoint.sorts
    • MLFixpoint.var
  • MLPattern
    • MLPattern.ctor_patterns
    • MLPattern.of()
    • MLPattern.sorts
    • MLPattern.symbol()
    • MLPattern.write()
  • MLPred
    • MLPred.op_sort
  • MLQuant
    • MLQuant.ctor_patterns
    • MLQuant.pattern
    • MLQuant.patterns
    • MLQuant.sort
    • MLQuant.sorts
    • MLQuant.var
  • MLRewrite
    • MLRewrite.sorts
  • Module
    • Module.attrs
    • Module.axioms
    • Module.let()
    • Module.let_attrs()
    • Module.name
    • Module.sentences
    • Module.symbol_decls
    • Module.write()
  • Mu
    • Mu.let()
    • Mu.let_patterns()
    • Mu.of()
    • Mu.pattern
    • Mu.symbol()
    • Mu.var
  • MultiaryConn
    • MultiaryConn.ops
    • MultiaryConn.patterns
  • Next
    • Next.let()
    • Next.let_patterns()
    • Next.let_sort()
    • Next.of()
    • Next.pattern
    • Next.patterns
    • Next.sort
    • Next.symbol()
  • Not
    • Not.let()
    • Not.let_patterns()
    • Not.let_sort()
    • Not.of()
    • Not.pattern
    • Not.sort
    • Not.symbol()
  • Nu
    • Nu.let()
    • Nu.let_patterns()
    • Nu.of()
    • Nu.pattern
    • Nu.symbol()
    • Nu.var
  • NullaryConn
    • NullaryConn.patterns
  • Or
    • Or.let()
    • Or.let_patterns()
    • Or.let_sort()
    • Or.of()
    • Or.ops
    • Or.sort
    • Or.symbol()
  • Pattern
    • Pattern.bottom_up()
    • Pattern.dict
    • Pattern.from_dict()
    • Pattern.from_json()
    • Pattern.json
    • Pattern.let_patterns()
    • Pattern.map_patterns()
    • Pattern.patterns
    • Pattern.top_down()
  • Rewrites
    • Rewrites.left
    • Rewrites.let()
    • Rewrites.let_patterns()
    • Rewrites.let_sort()
    • Rewrites.of()
    • Rewrites.patterns
    • Rewrites.right
    • Rewrites.sort
    • Rewrites.symbol()
  • RightAssoc
    • RightAssoc.args
    • RightAssoc.kore_symbol()
    • RightAssoc.let()
    • RightAssoc.let_patterns()
    • RightAssoc.pattern
    • RightAssoc.sorts
    • RightAssoc.symbol
  • RoundPred
    • RoundPred.pattern
    • RoundPred.patterns
    • RoundPred.sorts
  • SVar
    • SVar.let()
    • SVar.let_patterns()
    • SVar.let_sort()
    • SVar.name
    • SVar.sort
  • Sentence
  • SetVarId
    • SetVarId.value
  • Sort
    • Sort.dict
    • Sort.from_dict()
    • Sort.from_json()
    • Sort.json
    • Sort.name
  • SortApp
    • SortApp.dict
    • SortApp.let()
    • SortApp.name
    • SortApp.sorts
    • SortApp.write()
  • SortDecl
    • SortDecl.attrs
    • SortDecl.hooked
    • SortDecl.let()
    • SortDecl.let_attrs()
    • SortDecl.name
    • SortDecl.vars
    • SortDecl.write()
  • SortVar
    • SortVar.dict
    • SortVar.let()
    • SortVar.name
    • SortVar.write()
  • String
    • String.let()
    • String.let_patterns()
    • String.patterns
    • String.value
    • String.write()
  • Symbol
    • Symbol.let()
    • Symbol.name
    • Symbol.vars
    • Symbol.write()
  • SymbolDecl
    • SymbolDecl.attrs
    • SymbolDecl.hooked
    • SymbolDecl.let()
    • SymbolDecl.let_attrs()
    • SymbolDecl.param_sorts
    • SymbolDecl.sort
    • SymbolDecl.symbol
    • SymbolDecl.write()
  • SymbolId
    • SymbolId.value
  • Top
    • Top.let()
    • Top.let_patterns()
    • Top.let_sort()
    • Top.of()
    • Top.sort
    • Top.symbol()
  • UnaryConn
    • UnaryConn.pattern
    • UnaryConn.patterns
  • VarPattern
    • VarPattern.name
    • VarPattern.patterns
    • VarPattern.sort
    • VarPattern.write()
  • WithAttrs
    • WithAttrs.attrs
    • WithAttrs.attrs_by_key
    • WithAttrs.let_attrs()
    • WithAttrs.map_attrs()
  • WithSort
    • WithSort.let_sort()
    • WithSort.map_sort()
    • WithSort.sort
  • kore_term()
• pyk.kore.tools module
  • PrintOutput
    • PrintOutput.BINARY
    • PrintOutput.JSON
    • PrintOutput.KAST
    • PrintOutput.KORE
    • PrintOutput.LATEX
    • PrintOutput.NONE
    • PrintOutput.PRETTY
    • PrintOutput.PROGRAM
  • kore_print()