pyk.kore.rpc module

final class AbortedResult(state: 'State', depth: 'int', unknown_predicate: 'Pattern | None', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → AbortedResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'aborted'
rule: str | None = None
state: State
unknown_predicate: Pattern | None
class BoosterServer(args: BoosterServerArgs)[source]

Bases: KoreServer

class BoosterServerArgs[source]

Bases: dict

bug_report: BugReport | None
command: str | Iterable[str] | None
fallback_on: Iterable[str | FallbackReason] | None
haskell_log_entries: Iterable[str] | None
haskell_log_format: KoreExecLogFormat | None
interim_simplification: int | None
kompiled_dir: Required[str | Path]
llvm_kompiled_dir: Required[str | Path]
log_axioms_file: Path | None
module_name: Required[str]
no_post_exec_simplify: bool | None
port: int | None
smt_reset_interval: int | None
smt_retry_limit: int | None
smt_tactic: str | None
smt_timeout: int | None
final class BranchingResult(state: 'State', depth: 'int', next_states: 'tuple[State, ...]', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → BranchingResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...]
reason: ClassVar[StopReason] = 'branching'
rule: str | None = None
state: State
final class CutPointResult(state: 'State', depth: 'int', next_states: 'tuple[State, ...]', rule: 'str', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → CutPointResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...]
reason: ClassVar[StopReason] = 'cut-point-rule'
rule: str
state: State
final exception DefaultError(message: 'str', code: 'int', data: 'Any' = None)[source]

Bases: KoreClientError

code: int
data: Any
message: str
final class DepthBoundResult(state: 'State', depth: 'int', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → DepthBoundResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'depth-bound'
rule: str | None = None
state: State
final exception DuplicateModuleError(module_name: 'str')[source]

Bases: KoreClientError

module_name: str
class ExecuteResult[source]

Bases: ABC

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → ER[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None
reason: ClassVar[StopReason]
rule: str | None
state: State
class FallbackReason(value)[source]

Bases: Enum

An enumeration.

ABORTED = 'Aborted'
BRANCHING = 'Branching'
STUCK = 'Stuck'
class GetModelResult[source]

Bases: ABC

static from_dict(dct: Mapping[str, Any]) → GetModelResult[source]
final class HttpTransport(host: str, port: int, *, timeout: int | None = None)[source]

Bases: Transport

close() → None[source]
command(bug_report_id: str, old_id: int, bug_report_request: str) → list[str][source]
description() → str[source]
request(req: str) → str[source]
final exception ImplicationError(error: 'str', context: 'Iterable[str]')[source]

Bases: KoreClientError

context: tuple[str, ...]
error: str
final class ImpliesResult(satisfiable: 'bool', implication: 'Pattern', substitution: 'Pattern | None', predicate: 'Pattern | None', logs: 'tuple[LogEntry, ...]')[source]

Bases: object

static from_dict(dct: Mapping[str, Any]) → ImpliesResult[source]
implication: Pattern
logs: tuple[LogEntry, ...]
predicate: Pattern | None
satisfiable: bool
substitution: Pattern | None
final exception InvalidModuleError(error: 'str', context: 'Iterable[str] | None')[source]

Bases: KoreClientError

context: tuple[str, ...] | None
error: str
class JsonRpcClient(host: str, port: int, *, timeout: int | None = None, bug_report: BugReport | None = None, bug_report_id: str | None = None, transport: TransportType = TransportType.SINGLE_SOCKET)[source]

Bases: ContextManager[JsonRpcClient]

close() → None[source]
request(method: str, **params: Any) → dict[str, Any][source]
class JsonRpcClientFacade(default_host: str, default_port: int, default_transport: TransportType, dispatch: dict[str, list[tuple[str, int, TransportType]]], *, timeout: int | None = None, bug_report: BugReport | None = None, bug_report_id: str | None = None)[source]

Bases: ContextManager[JsonRpcClientFacade]

close() → None[source]
request(method: str, **params: Any) → dict[str, Any][source]
final exception JsonRpcError(message: 'str', code: 'int', data: 'Any' = None)[source]

Bases: Exception

class KoreClient(host: str, port: int, *, timeout: int | None = None, bug_report: BugReport | None = None, bug_report_id: str | None = None, transport: TransportType = TransportType.SINGLE_SOCKET, dispatch: dict[str, list[tuple[str, int, TransportType]]] | None = None)[source]

Bases: ContextManager[KoreClient]

add_module(module: Module, *, name_as_id: bool | None = None) → str[source]
close() → None[source]
execute(pattern: Pattern, *, max_depth: int | None = None, assume_state_defined: bool | None = None, cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, moving_average_step_timeout: bool | None = None, step_timeout: int | None = None, module_name: str | None = None, log_successful_rewrites: bool | None = None, log_failed_rewrites: bool | None = None, log_successful_simplifications: bool | None = None, log_failed_simplifications: bool | None = None, log_timing: bool | None = None) → ExecuteResult[source]
get_model(pattern: Pattern, module_name: str | None = None) → GetModelResult[source]
implies(antecedent: Pattern, consequent: Pattern, *, module_name: str | None = None, log_successful_simplifications: bool | None = None, log_failed_simplifications: bool | None = None) → ImpliesResult[source]
simplify(pattern: Pattern, *, module_name: str | None = None, log_successful_simplifications: bool | None = None, log_failed_simplifications: bool | None = None) → tuple[Pattern, tuple[LogEntry, ...]][source]
exception KoreClientError(message: str)[source]

Bases: Exception, ABC

class KoreExecLogFormat(value)[source]

Bases: Enum

An enumeration.

ONELINE = 'oneline'
STANDARD = 'standard'
class KoreServer(args: KoreServerArgs)[source]

Bases: ContextManager[KoreServer]

close() → None[source]
property host: str
property pid: int
property port: int
start() → None[source]
class KoreServerArgs[source]

Bases: TypedDict

bug_report: BugReport | None
command: str | Iterable[str] | None
haskell_log_entries: Iterable[str] | None
haskell_log_format: KoreExecLogFormat | None
kompiled_dir: Required[str | Path]
log_axioms_file: Path | None
module_name: Required[str]
port: int | None
smt_reset_interval: int | None
smt_retry_limit: int | None
smt_tactic: str | None
smt_timeout: int | None
class KoreServerInfo(pid, host, port)[source]

Bases: NamedTuple

host: str

Alias for field number 1

pid: int

Alias for field number 0

port: int

Alias for field number 2

class LogEntry[source]

Bases: ABC

classmethod from_dict(dct: Mapping[str, Any]) → LE[source]
origin: LogOrigin
result: RewriteResult
abstract to_dict() → dict[str, Any][source]
class LogOrigin(value)[source]

Bases: str, Enum

An enumeration.

BOOSTER = 'booster'
KORE_RPC = 'kore-rpc'
LLVM = 'llvm'
final class LogRewrite(origin: 'LogOrigin', result: 'RewriteResult')[source]

Bases: LogEntry

classmethod from_dict(dct: Mapping[str, Any]) → LogRewrite[source]
origin: LogOrigin
result: RewriteResult
to_dict() → dict[str, Any][source]
final class LogSimplification(origin: 'LogOrigin', result: 'RewriteResult', original_term: 'Pattern | None', original_term_index: 'tuple[int, ...] | None')[source]

Bases: LogEntry

classmethod from_dict(dct: Mapping[str, Any]) → LogSimplification[source]
origin: LogOrigin
original_term: Pattern | None
original_term_index: tuple[int, ...] | None
result: RewriteResult
to_dict() → dict[str, Any][source]
final exception ParseError(error: 'str')[source]

Bases: KoreClientError

error: str
final exception PatternError(error: 'str', context: 'Iterable[str]')[source]

Bases: KoreClientError

context: tuple[str, ...]
error: str
final class RewriteFailure(rule_id: 'str', reason: 'str')[source]

Bases: RewriteResult

classmethod from_dict(dct: Mapping[str, Any]) → RewriteFailure[source]
reason: str
rule_id: str
to_dict() → dict[str, Any][source]
class RewriteResult[source]

Bases: ABC

classmethod from_dict(dct: Mapping[str, Any]) → RR[source]
rule_id: str
abstract to_dict() → dict[str, Any][source]
final class RewriteSuccess(rule_id: 'str', rewritten_term: 'Pattern | None')[source]

Bases: RewriteResult

classmethod from_dict(dct: Mapping[str, Any]) → RewriteSuccess[source]
rewritten_term: Pattern | None
rule_id: str
to_dict() → dict[str, Any][source]
final class SatResult(model: 'Pattern | None')[source]

Bases: GetModelResult

model: Pattern | None
final class SingleSocketTransport(host: str, port: int, *, timeout: int | None = None)[source]

Bases: Transport

close() → None[source]
command(bug_report_id: str, old_id: int, bug_report_request: str) → list[str][source]
description() → str[source]
request(req: str) → str[source]
final exception SmtSolverError(error: 'str', pattern: 'Pattern')[source]

Bases: KoreClientError

error: str
pattern: Pattern
final class State(term: 'Pattern', *, substitution: 'Mapping[EVar, Pattern] | None' = None, predicate: 'Pattern | None' = None, rule_id: 'str | None' = None, rule_substitution: 'Mapping[EVar, Pattern] | None' = None, rule_predicate: 'Pattern | None' = None)[source]

Bases: object

static from_dict(dct: Mapping[str, Any]) → State[source]
property kore: Pattern
predicate: Pattern | None
rule_id: str | None
rule_predicate: Pattern | None
rule_substitution: FrozenDict[EVar, Pattern] | None
substitution: FrozenDict[EVar, Pattern] | None
term: Pattern
class StopReason(value)[source]

Bases: str, Enum

An enumeration.

ABORTED = 'aborted'
BRANCHING = 'branching'
CUT_POINT_RULE = 'cut-point-rule'
DEPTH_BOUND = 'depth-bound'
STUCK = 'stuck'
TERMINAL_RULE = 'terminal-rule'
TIMEOUT = 'timeout'
VACUOUS = 'vacuous'
final class StuckResult(state: 'State', depth: 'int', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → StuckResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'stuck'
rule: str | None = None
state: State
final class TerminalResult(state: 'State', depth: 'int', rule: 'str', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → TerminalResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'terminal-rule'
rule: str
state: State
final class TimeoutResult(state: 'State', depth: 'int', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → TimeoutResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'timeout'
rule: str | None = None
state: State
class Transport[source]

Bases: ContextManager[Transport], ABC

abstract close() → None[source]
abstract command(bug_report_id: str, old_id: int, bug_report_request: str) → list[str][source]
abstract description() → str[source]
abstract request(req: str) → str[source]
class TransportType(value)[source]

Bases: Enum

An enumeration.

HTTP = 2
SINGLE_SOCKET = 1
final exception UnknownModuleError(module_name: 'str')[source]

Bases: KoreClientError

module_name: str
final class UnknownResult[source]

Bases: GetModelResult

final class UnsatResult[source]

Bases: GetModelResult

final class VacuousResult(state: 'State', depth: 'int', logs: 'tuple[LogEntry, ...]')[source]

Bases: ExecuteResult

depth: int
classmethod from_dict(dct: Mapping[str, Any]) → VacuousResult[source]
logs: tuple[LogEntry, ...]
next_states: tuple[State, ...] | None = None
reason: ClassVar[StopReason] = 'vacuous'
rule: str | None = None
state: State
kore_server(definition_dir: str | Path, module_name: str, *, port: int | None = None, command: str | Iterable[str] | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, smt_tactic: str | None = None, log_axioms_file: Path | None = None, haskell_log_format: KoreExecLogFormat | None = None, haskell_log_entries: Iterable[str] | None = None, llvm_definition_dir: Path | None = None, fallback_on: Iterable[str | FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool | None = None, bug_report: BugReport | None = None) → KoreServer[source]