pyk.cterm.symbolic module

class CTermExecute(state, next_states, depth, vacuous, logs)[source]

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

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')[source]: Bases: Exception

class CTermSymbolic(kore_client: KoreClient, definition: KDefinition, *, log_succ_rewrites: bool = True, log_fail_rewrites: bool = False)[source]

Bases: object

assume_defined(cterm: CTerm, module_name: str | None = None) → CTerm[source]

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

get_model(cterm: CTerm, module_name: str | None = None) → Subst | None[source]

implies(antecedent: CTerm, consequent: CTerm, bind_universally: bool = False, failure_reason: bool = False, module_name: str | None = None, assume_defined: bool = False) → CTermImplies[source]

kast_simplify(kast: KInner, module_name: str | None = None) → tuple[KInner, tuple[LogEntry, ...]][source]

kast_to_kore(kinner: KInner) → Pattern[source]

kore_to_kast(pattern: Pattern) → KInner[source]

simplify(cterm: CTerm, module_name: str | None = None) → tuple[CTerm, tuple[LogEntry, ...]][source]

class NextState(state, condition)[source]

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, start_server: bool = True, maude_port: int | None = None, fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool = False) → Iterator[CTermSymbolic][source]