Expand description
§Pigeons
A proof logging library for VeriPB.
This library is a simple abstraction layer for writing proofs checkable with VeriPB.
§Features
short-keywords: use short rule keywords, e.g.,pinstead ofpolserde: add implementations forserde::Serializeandserde::Deserializefor library types
§Coverage of VeriPB Syntax
-
f:Proof::new -
pol:Proof::operations -
rup:Proof::reverse_unit_prop -
del:Proof::delete_ids,Proof::delete_id_range,Proof::delete_constr -
delc:Proof::delete_core_ids -
deld:Proof::delete_derived_ids -
obju:Proof::update_objective -
red:Proof::redundant -
dom:Proof::dominated -
core:Proof::move_ids_to_core,Proof::move_range_to_core -
sol:Proof::solution -
solx:Proof::exclude_solution -
soli:Proof::improve_solution -
output:Proof::output,Proof::conclude -
conclusion:Proof::conclude,Proof::new_with_conclusion,Proof::update_default_conclusion - Sub-proofs
-
e:Proof::equals -
ea:Proof::equals_add -
eobj:Proof::obj_equals -
i:Proof::implied -
ia:Proof::implied_add -
#:Proof::set_level -
w:Proof::wipe_level -
strengthening_to_core:Proof::strengthening_to_core -
def_order -
load_order
Structs§
- AbsConstraint
Id - A type representing a VeriPB constraint ID
- Axiom
- An axiom or literal
- Constraint
Id - A constraint ID referring to a constraint
- Operation
Sequence - A sequence of operations to be added to the proof in reverse polish notation
- Order
- An order in the proof
- Proof
- A type representing a VeriPB proof.
- Proof
Goal - A proof target of a sub-proof
- Proof
Only Var - A variable that is only present in the proof
- Substitution
- A substitution of a variable to a value or a literal
Enums§
- Conclusion
- Possible conclusions
- Derivation
- A derivation step
- Objective
Update - An objective update step (
obju) - Order
Var - A variable to be used in an order definition
- Output
Guarantee - Possible output guarantees for the output section
- Output
Type - Possible output types for the output section
- Problem
Type - The proof problem type
- Proof
Goal Id - A
ProofGoalID - Subproof
Element - An element of a sub-proof
Traits§
- Constraint
Like - Trait that needs to be implemented for types used as constraints
- Objective
Like - Trait that needs to be implemented for types used as objectives
- Operation
Like - A trait implemented by all types intended to be used in building an
OperationSequence - VarLike
- Trait that needs to be implemented for types used as variables