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]