pyk.cterm.symbolic module

class CTermExecute(state, next_states, depth, vacuous, logs)

Bases: NamedTuple

depth: int

Alias for field number 2

logs: tuple[LogEntry, ...]

Alias for field number 4

next_states: tuple[NextState, ...]

Alias for field number 1

state: CTerm

Alias for field number 0

vacuous: bool

Alias for field number 3

class CTermImplies(csubst, failing_cells, remaining_implication, logs)

Bases: NamedTuple

csubst: CSubst | None

Alias for field number 0

failing_cells: tuple[tuple[str, KInner], ...]

Alias for field number 1

logs: tuple[LogEntry, ...]

Alias for field number 3

remaining_implication: KInner | None

Alias for field number 2

final exception CTermSMTError(message: 'str')

Bases: Exception

class CTermSymbolic(kore_client: KoreClient, definition: KDefinition, *, log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, booster_only_simplify: bool = False, haskell_log_entries: Iterable[str] = ('DebugAttemptEquation', 'DebugApplyEquation', 'DebugTerm', 'Proxy', 'Detail', 'Abort', 'Simplify', 'Rewrite'), haskell_log_dir: Path | None = None)

Bases: object

add_module(module: KFlatModule, name_as_id: bool = False) → str

assume_defined(cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool = False) → CTerm

execute(cterm: CTerm, depth: int | None = None, cut_point_rules: Iterable[str] | None = None, terminal_rules: Iterable[str] | None = None, module_name: str | None = None, booster_only_simplify: bool | None = None, haskell_logging: bool | None = None) → CTermExecute

get_model(cterm: CTerm, module_name: str | None = None) → Subst | None

implies(antecedent: CTerm, consequent: CTerm, bind_universally: bool = False, failure_reason: bool = False, module_name: str | None = None, assume_defined: bool = False, booster_only_simplify: bool | None = None, haskell_logging: bool | None = None) → CTermImplies

interrupt() → None

Abort a backend request currently in flight on another thread; see KoreClient.interrupt.

kast_simplify(kast: KInner, module_name: str | None = None, booster_only_simplify: bool | None = None, haskell_logging: bool | None = None) → tuple[KInner, tuple[LogEntry, ...]]

kast_to_kore(kinner: KInner) → Pattern

kore_to_kast(pattern: Pattern) → KInner

simplify(cterm: CTerm, module_name: str | None = None, booster_only_simplify: bool | None = None, haskell_logging: bool | None = None) → tuple[CTerm, tuple[LogEntry, ...]]

HASKELL_LOGGING_ENTRIES: Final = ('DebugAttemptEquation', 'DebugApplyEquation', 'DebugTerm', 'Proxy', 'Detail', 'Abort', 'Simplify', 'Rewrite')

Canonical default set of haskell-backend log entries to capture per request for fallback diagnosis. Spans both engines: kore entry types (resolved by the backend against its log registry) and booster context tags. Sent verbatim on the haskell-logging request field; the backend skips any name it does not recognise, so this can evolve without a lockstep backend release. Override per CTermSymbolic (e.g. downstream semantics needing a different set).

class NextState(state, condition)

Bases: NamedTuple

condition: KInner | None

Alias for field number 1

state: CTerm

Alias for field number 0

cterm_symbolic(definition: KDefinition, definition_dir: Path, *, id: str | None = None, port: int | None = None, kore_rpc_command: str | Iterable[str] | None = None, llvm_definition_dir: Path | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, smt_tactic: str | None = None, bug_report: BugReport | None = None, haskell_log_format: KoreExecLogFormat = KoreExecLogFormat.ONELINE, haskell_log_entries: Iterable[str] = (), log_axioms_file: Path | None = None, log_succ_rewrites: bool = True, log_fail_rewrites: bool = False, booster_only_simplify: bool = False, haskell_log_dir: Path | None = None, start_server: bool = True, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, simplify_each: int | None = None, no_post_exec_simplify: bool = False) → Iterator[CTermSymbolic]