pyk.proof package

Submodules

• pyk.proof.implies module
  • EqualityProof
    • EqualityProof.constraint
    • EqualityProof.constraints
    • EqualityProof.dict
    • EqualityProof.equality
    • EqualityProof.from_claim()
    • EqualityProof.from_dict()
    • EqualityProof.lhs_body
    • EqualityProof.pretty()
    • EqualityProof.read_proof_data()
    • EqualityProof.rhs_body
    • EqualityProof.simplified_constraints
    • EqualityProof.simplified_equality
    • EqualityProof.sort
    • EqualityProof.summary
  • EqualitySummary
    • EqualitySummary.admitted
    • EqualitySummary.id
    • EqualitySummary.lines
    • EqualitySummary.status
  • ImpliesProof
    • ImpliesProof.antecedent
    • ImpliesProof.bind_universally
    • ImpliesProof.can_progress
    • ImpliesProof.commit()
    • ImpliesProof.consequent
    • ImpliesProof.csubst
    • ImpliesProof.dict
    • ImpliesProof.from_dict()
    • ImpliesProof.get_steps()
    • ImpliesProof.own_status
    • ImpliesProof.simplified_antecedent
    • ImpliesProof.simplified_consequent
    • ImpliesProof.write_proof_data()
  • ImpliesProofResult
    • ImpliesProofResult.csubst
    • ImpliesProofResult.simplified_antecedent
    • ImpliesProofResult.simplified_consequent
  • ImpliesProofStep
    • ImpliesProofStep.proof
  • ImpliesProver
    • ImpliesProver.assume_defined
    • ImpliesProver.close()
    • ImpliesProver.failure_info()
    • ImpliesProver.init_proof()
    • ImpliesProver.kcfg_explore
    • ImpliesProver.proof
    • ImpliesProver.step_proof()
  • RefutationProof
    • RefutationProof.dict
    • RefutationProof.from_dict()
    • RefutationProof.last_constraint
    • RefutationProof.pre_constraints
    • RefutationProof.pretty()
    • RefutationProof.read_proof_data()
    • RefutationProof.simplified_constraints
    • RefutationProof.summary
    • RefutationProof.to_claim()
  • RefutationSummary
    • RefutationSummary.id
    • RefutationSummary.lines
    • RefutationSummary.status
• pyk.proof.proof module
  • CompositeSummary
    • CompositeSummary.lines
    • CompositeSummary.summaries
  • FailureInfo
  • Proof
    • Proof.add_subproof()
    • Proof.admit()
    • Proof.admitted
    • Proof.can_progress
    • Proof.commit()
    • Proof.dict
    • Proof.digest
    • Proof.failed
    • Proof.failure_info
    • Proof.fetch_subproof()
    • Proof.fetch_subproof_data()
    • Proof.from_dict()
    • Proof.get_steps()
    • Proof.id
    • Proof.json
    • Proof.one_line_summary
    • Proof.own_status
    • Proof.passed
    • Proof.proof_data_exists()
    • Proof.proof_dir
    • Proof.proof_exists()
    • Proof.proof_subdir
    • Proof.read_proof()
    • Proof.read_proof_data()
    • Proof.read_subproof()
    • Proof.read_subproof_data()
    • Proof.remove_subproof()
    • Proof.status
    • Proof.subproof_ids
    • Proof.subproofs
    • Proof.subproofs_status
    • Proof.summary
    • Proof.up_to_date
    • Proof.write_proof()
    • Proof.write_proof_data()
  • ProofStatus
    • ProofStatus.FAILED
    • ProofStatus.PASSED
    • ProofStatus.PENDING
  • ProofSummary
    • ProofSummary.id
    • ProofSummary.lines
    • ProofSummary.status
  • Prover
    • Prover.advance_proof()
    • Prover.close()
    • Prover.failure_info()
    • Prover.init_proof()
    • Prover.step_proof()
  • parallel_advance_proof()
• pyk.proof.prove_rpc module
  • ProveRpc
    • ProveRpc.prove_rpc()
• pyk.proof.reachability module
  • APRFailureInfo
    • APRFailureInfo.failing_nodes
    • APRFailureInfo.failure_reasons
    • APRFailureInfo.from_proof()
    • APRFailureInfo.models
    • APRFailureInfo.path_conditions
    • APRFailureInfo.pending_nodes
    • APRFailureInfo.print()
  • APRProof
    • APRProof.add_bounded()
    • APRProof.add_exec_time()
    • APRProof.as_claim()
    • APRProof.as_rule()
    • APRProof.as_rules()
    • APRProof.bmc_depth
    • APRProof.bounded
    • APRProof.can_progress
    • APRProof.circularities_module_name
    • APRProof.circularity
    • APRProof.commit()
    • APRProof.construct_node_refutation()
    • APRProof.dependencies_module_name
    • APRProof.dict
    • APRProof.error_info
    • APRProof.exec_time
    • APRProof.failing
    • APRProof.formatted_exec_time()
    • APRProof.from_claim()
    • APRProof.from_dict()
    • APRProof.from_spec_modules()
    • APRProof.get_refutation_id()
    • APRProof.get_steps()
    • APRProof.init
    • APRProof.is_bounded()
    • APRProof.is_failing()
    • APRProof.is_init()
    • APRProof.is_pending()
    • APRProof.is_refuted()
    • APRProof.is_target()
    • APRProof.logs
    • APRProof.module_name
    • APRProof.node_refutations
    • APRProof.nonzero_depth()
    • APRProof.one_line_summary
    • APRProof.own_status
    • APRProof.path_constraints()
    • APRProof.pending
    • APRProof.prior_loops_cache
    • APRProof.prune()
    • APRProof.read_proof()
    • APRProof.read_proof_data()
    • APRProof.refute_node()
    • APRProof.rule_id
    • APRProof.set_exec_time()
    • APRProof.shortest_path_to()
    • APRProof.summary
    • APRProof.target
    • APRProof.unrefute_node()
    • APRProof.write_proof_data()
  • APRProofBoundedResult
  • APRProofExtendAndCacheResult
    • APRProofExtendAndCacheResult.extension_to_cache
  • APRProofExtendResult
    • APRProofExtendResult.extension_to_apply
  • APRProofResult
    • APRProofResult.node_id
    • APRProofResult.optimize_kcfg
    • APRProofResult.prior_loops_cache_update
  • APRProofStep
    • APRProofStep.bmc_depth
    • APRProofStep.circularity
    • APRProofStep.circularity_rule_id
    • APRProofStep.module_name
    • APRProofStep.node
    • APRProofStep.nonzero_depth
    • APRProofStep.prior_loops_cache
    • APRProofStep.proof_id
    • APRProofStep.shortest_path_to_node
    • APRProofStep.target
    • APRProofStep.use_cache
  • APRProofSubsumeResult
    • APRProofSubsumeResult.csubst
  • APRProofTerminalResult
  • APRProofUseCacheResult
    • APRProofUseCacheResult.cached_node_id
  • APRProver
    • APRProver.assume_defined
    • APRProver.close()
    • APRProver.counterexample_info
    • APRProver.cut_point_rules
    • APRProver.direct_subproof_rules
    • APRProver.execute_depth
    • APRProver.extra_module
    • APRProver.failure_info()
    • APRProver.fast_check_subsumption
    • APRProver.init_proof()
    • APRProver.kcfg_explore
    • APRProver.main_module_name
    • APRProver.optimize_kcfg
    • APRProver.step_proof()
    • APRProver.terminal_rules
  • APRSummary
    • APRSummary.admitted
    • APRSummary.bmc_depth
    • APRSummary.bounded
    • APRSummary.failing
    • APRSummary.formatted_exec_time
    • APRSummary.id
    • APRSummary.lines
    • APRSummary.nodes
    • APRSummary.pending
    • APRSummary.refuted
    • APRSummary.status
    • APRSummary.stuck
    • APRSummary.subproofs
    • APRSummary.terminal
    • APRSummary.vacuous
• pyk.proof.show module
  • APRProofNodePrinter
    • APRProofNodePrinter.node_attrs()
    • APRProofNodePrinter.proof
  • APRProofShow
    • APRProofShow.dot()
    • APRProofShow.dump()
    • APRProofShow.kcfg_show
    • APRProofShow.pretty()
    • APRProofShow.pretty_segments()
    • APRProofShow.show()
• pyk.proof.tui module
  • APRProofBehaviorView
    • APRProofBehaviorView.can_focus
    • APRProofBehaviorView.can_focus_children
    • APRProofBehaviorView.compose()
  • APRProofViewer
    • APRProofViewer.compose()
    • APRProofViewer.on_mount()