Struct ProofRecorder 

pub struct ProofRecorder { /* private fields */ }

A proof recorder that can be used during SAT/SMT solving

This provides a simple interface for recording proof steps during search

Implementations

impl ProofRecorder

pub fn new() -> Self

Create a new proof recorder

pub fn enable_batch_mode(&mut self)

Enable batch mode (queue steps instead of adding immediately)

pub fn disable_batch_mode(&mut self)

Disable batch mode

pub fn alloc_clause_id(&mut self) -> u32

Allocate a new clause ID

pub fn record_input(&mut self, conclusion: impl Into<String>) -> u32

Record an input clause

pub fn record_derived( &mut self, rule: impl Into<String>, premises: &[u32], conclusion: impl Into<String>, ) -> u32

Record a derived clause

pub fn flush(&mut self)

Flush the batched steps

pub const fn builder(&self) -> &IncrementalProofBuilder

Get the builder

pub fn builder_mut(&mut self) -> &mut IncrementalProofBuilder

Get the mutable builder

pub fn take_proof(&mut self) -> Proof

Take the proof

Trait Implementations

impl Debug for ProofRecorder

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

Formats the value using the given formatter.

impl Default for ProofRecorder

fn default() -> Self

Returns the “default value” for a type.