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[CTerm, ...]

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, kompiled_kore: KompiledKore, *, trace_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) → 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]
cterm_symbolic(definition: KDefinition, kompiled_kore: KompiledKore, 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, trace_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]