pyk.proof.implies module

class EqualityProof(id: str, lhs_body: KInner, rhs_body: KInner, sort: KSort, constraints: Iterable[KInner] = (), simplified_constraints: KInner | None = None, simplified_equality: KInner | None = None, csubst: CSubst | None = None, proof_dir: Path | None = None, subproof_ids: Iterable[str] = (), admitted: bool = False)[source]

Bases: ImpliesProof

property constraint: KInner

property constraints: list[KInner]

property dict: dict[str, Any]

property equality: KApply

static from_claim(claim: KClaim, defn: KDefinition, proof_dir: Path | None = None) → EqualityProof[source]

classmethod from_dict(dct: Mapping[str, Any], proof_dir: Path | None = None) → EqualityProof[source]

property lhs_body: KInner

pretty(kprint: KPrint) → Iterable[str][source]

static read_proof_data(proof_dir: Path, id: str) → EqualityProof[source]

property rhs_body: KInner

property simplified_constraints: KInner | None

property simplified_equality: KInner | None

property sort: KSort

property summary: EqualitySummary

class EqualitySummary(id: 'str', status: 'ProofStatus', admitted: 'bool')[source]

Bases: ProofSummary

admitted: bool

id: str

property lines: list[str]

status: ProofStatus

class ImpliesProof(id: str, antecedent: KInner, consequent: KInner, bind_universally: bool = False, simplified_antecedent: KInner | None = None, simplified_consequent: KInner | None = None, csubst: CSubst | None = None, proof_dir: Path | None = None, subproof_ids: Iterable[str] = (), admitted: bool = False)[source]

Bases: Proof[ImpliesProofStep, ImpliesProofResult]

antecedent: KInner

bind_universally: bool

property can_progress: bool

commit(result: ImpliesProofResult) → None[source]

consequent: KInner

csubst: CSubst | None

property dict: dict[str, Any]

classmethod from_dict(dct: Mapping[str, Any], proof_dir: Path | None = None) → ImpliesProof[source]

get_steps() → list[ImpliesProofStep][source]

property own_status: ProofStatus

simplified_antecedent: KInner | None

simplified_consequent: KInner | None

write_proof_data(subproofs: bool = False) → None[source]

class ImpliesProofResult(csubst: 'CSubst | None', simplified_antecedent: 'KInner | None', simplified_consequent: 'KInner | None')[source]

Bases: object

csubst: CSubst | None

simplified_antecedent: KInner | None

simplified_consequent: KInner | None

class ImpliesProofStep(proof: 'ImpliesProof')[source]

Bases: object

proof: ImpliesProof

class ImpliesProver(proof: ImpliesProof, kcfg_explore: KCFGExplore, assume_defined: bool = False)[source]

Bases: Prover[ImpliesProof, ImpliesProofStep, ImpliesProofResult]

assume_defined: bool

close() → None[source]

failure_info(proof: ImpliesProof) → FailureInfo[source]

init_proof(proof: ImpliesProof) → None[source]

kcfg_explore: KCFGExplore

proof: ImpliesProof

step_proof(step: ImpliesProofStep) → list[ImpliesProofResult][source]

class RefutationProof(id: str, pre_constraints: Iterable[KInner], last_constraint: KInner, simplified_antecedent: KInner | None = None, simplified_consequent: KInner | None = None, csubst: CSubst | None = None, proof_dir: Path | None = None, subproof_ids: Iterable[str] = (), admitted: bool = False)[source]