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

haskell_threads: int | None

interim_simplification: int | None

kompiled_dir: Required[str | Path]

llvm_kompiled_dir: Required[str | Path]

log_axioms_file: Path | None

log_context: Iterable[str] | None

module_name: Required[str]

no_post_exec_simplify: bool | None

not_log_context: Iterable[str] | 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]

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

Bases: KoreClientError

context: tuple[str, ...]

error: str

final class ImpliesResult(valid: '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

substitution: Pattern | None

valid: bool

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) → ExecuteResult[source]

get_model(pattern: Pattern, module_name: str | None = None) → GetModelResult[source]

implies(antecedent: Pattern, consequent: Pattern, *, module_name: str | None = None, assume_defined: bool = False) → ImpliesResult[source]

port: int

simplify(pattern: Pattern, *, module_name: str | 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

haskell_threads: int | 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]

abstract to_dict() → dict[str, Any][source]

class LogOrigin(value)[source]

Bases: str, Enum

An enumeration.

BOOSTER = 'booster'

KORE_RPC = 'kore-rpc'

LLVM = 'llvm'

PROXY = 'proxy'

__format__(format_spec): Returns format using actual value type unless __str__ has been overridden.

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 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 | None', reason: 'str')[source]

Bases: RewriteResult

classmethod from_dict(dct: Mapping[str, Any]) → RewriteFailure[source]

reason: str

rule_id: str | None

to_dict() → dict[str, Any][source]

class RewriteResult[source]

Bases: ABC

classmethod from_dict(dct: Mapping[str, Any]) → RR[source]

rule_id: str | None

abstract to_dict() → dict[str, Any][source]

final class RewriteSuccess(rule_id: 'str', rewritten_term: 'Pattern | None' = None)[source]

Bases: RewriteResult

classmethod from_dict(dct: Mapping[str, Any]) → RewriteSuccess[source]

rewritten_term: Pattern | None = 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]

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'

__format__(format_spec): Returns format using actual value type unless __str__ has been overridden.

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]

request(req: str, request_id: str, method_name: 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, haskell_threads: int | 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]