Struct ProofLogger 

pub struct ProofLogger { /* private fields */ }

Streams proof steps to a binary log file during solving.

Examples

use std::path::Path;
use oxiz_proof::logging::ProofLogger;
use oxiz_proof::proof::{ProofStep, ProofNodeId};

let mut logger = ProofLogger::create(Path::new("/tmp/proof.oxizlog"))
    .expect("failed to create log");

logger.log_step(ProofNodeId(0), &ProofStep::Axiom {
    conclusion: "true".to_string(),
}).expect("failed to log step");

logger.close().expect("failed to close log");

Implementations

impl ProofLogger

pub fn create(path: &Path) -> LoggingResult<Self>

Create a new proof log at path, overwriting any existing file.

Writes the file header immediately.

pub fn append(path: &Path) -> LoggingResult<Self>

Open an existing proof log for appending.

Does not write a new header; the file must already have a valid header written by a previous ProofLogger::create call.

pub fn log_step( &mut self, node_id: ProofNodeId, step: &ProofStep, ) -> LoggingResult<()>

Append a single ProofStep to the log.

node_id is the ProofNodeId assigned to this step in the live proof DAG; it is recorded so that cross-references in Inference premises can be resolved during replay.

Errors

Returns LoggingError::AlreadyClosed if called after close().

pub fn flush(&mut self) -> LoggingResult<()>

Flush the internal write buffer to the OS.

Under normal operation you do not need to call this explicitly; close() flushes before closing. Call flush() for crash-safety checkpointing during long-running solves.

pub fn close(&mut self) -> LoggingResult<()>

Flush and close the log file.

After this call, further log_step calls will return LoggingError::AlreadyClosed.

pub fn step_count(&self) -> u64

Return the number of proof steps written since this logger was created.

pub fn path(&self) -> &Path

Return the path of the log file.

pub fn is_closed(&self) -> bool

Return true if the logger has been closed.

Trait Implementations

impl Drop for ProofLogger

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.