tiny.smt.ProofStep

1/// One step of a proof trace: a clause that has to follow from the starting clauses, the2/// assumptions and the earlier steps by unit propagation. A caller walks the steps of the last3/// solve through `Solver.lastProofTrace`, and code that writes or checks a proof walks the steps of4/// a `ProofArtifact`. The last step of a complete refutation is the empty clause.5pub const ProofStep = struct {6    /// The literals of the step's clause, and an empty slice for the empty clause. In the solver's7    /// trace the solver owns them, and they stay valid until the next change to the solver. In a8    /// `ProofArtifact` the artifact owns its own copy.9    literals: []Literal,10};

1pub const ProofStep = sat.ProofStep;