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

antecedent: KInner
bind_universally: bool
property can_progress: bool
commit(result: StepResult) → 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]
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: StepResult

csubst: CSubst | None
simplified_antecedent: KInner | None
simplified_consequent: KInner | None
class ImpliesProver(proof: ImpliesProof, kcfg_explore: KCFGExplore)[source]

Bases: Prover

failure_info() → FailureInfo[source]
proof: ImpliesProof
step_proof() → Iterable[StepResult][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]

Bases: ImpliesProof

property dict: dict[str, Any]
classmethod from_dict(dct: Mapping[str, Any], proof_dir: Path | None = None) → RefutationProof[source]
property last_constraint: KInner
property pre_constraints: list[KInner]
pretty(kprint: KPrint) → Iterable[str][source]
static read_proof_data(proof_dir: Path, id: str) → RefutationProof[source]
property simplified_constraints: KInner | None
property summary: RefutationSummary
to_claim(claim_id: str) → tuple[KClaim, Subst][source]
class RefutationSummary(id: 'str', status: 'ProofStatus')[source]

Bases: ProofSummary

id: str
property lines: list[str]
status: ProofStatus