Struct ProofWriter 

pub struct ProofWriter<W, Int> { /* private fields */ }

Write a DRCP proof to some sink.

See the module documentation of crate::writer for examples on how to use the ProofWriter.

Implementations

impl<W: Write, Int> ProofWriter<W, Int>

pub fn new(writer: W) -> Self

Create a new proof writer which writes the proof to an underlying sink implementing Write.

impl<W: Write, Int: IntValue> ProofWriter<W, Int>

pub fn log_deduction<Identifier: Into<Box<str>>>( &mut self, deduction: Deduction<Identifier, Int>, ) -> Result<()>

Write a deduction step.

The propagation_hints can be optionally given to indicate which previously derived facts should be applied to derive the conflict.

This function wraps an IO operation, which is why it can fail with an IO error.

pub fn log_inference<Identifier: Into<Box<str>>, Label: Display>( &mut self, inference: Inference<Identifier, Int, Label>, ) -> Result<()>

Log an inference step.

Besides premises and a consequent, an inference step can optionally include hints regarding the constraint that generated the inference, and the label of the filtering algorithm which identified the inference.

If there is no consequent, then the format prescribes that the consequent is false, so that the premises form a nogood.

This function wraps an IO operation, which is why it can fail with an IO error.

pub fn log_conclusion<Identifier: Into<Box<str>>>( &mut self, conclusion: Conclusion<Identifier, Int>, ) -> Result<()>

Conclude the proof with a conclusion.

Trait Implementations

impl<W: Debug, Int: Debug> Debug for ProofWriter<W, Int>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.