Struct IncrementalProofBuilder 

pub struct IncrementalProofBuilder { /* private fields */ }

A scoped proof builder for incremental construction

Supports:

• Push/pop scoping (for backtracking)
• Efficient deduplication
• Premise tracking

Implementations

impl IncrementalProofBuilder

pub fn new() -> Self

Create a new incremental proof builder

pub fn enable(&mut self)

Enable proof recording

pub fn disable(&mut self)

Disable proof recording

pub const fn is_enabled(&self) -> bool

Check if proof recording is enabled

pub fn push_scope(&mut self)

Push a new scope (for backtracking)

pub fn pop_scope(&mut self)

Pop a scope (backtrack)

pub fn scope_level(&self) -> usize

Get the current scope level

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

Record an axiom (input clause)

pub fn record_inference( &mut self, clause_id: u32, rule: impl Into<String>, premise_ids: &[u32], conclusion: impl Into<String>, ) -> ProofNodeId

Record an inference step

pub fn record_inference_with_args( &mut self, clause_id: u32, rule: impl Into<String>, premise_ids: &[u32], args: Vec<String>, conclusion: impl Into<String>, ) -> ProofNodeId

Record an inference step with arguments

pub fn get_clause_proof(&self, clause_id: u32) -> Option<ProofNodeId>

Get the proof node for a solver clause ID

pub const fn proof(&self) -> &Proof

Get the proof (immutable)

pub fn take_proof(&mut self) -> Proof

Take the proof, leaving an empty one

pub fn reset(&mut self)

Reset the builder

pub fn stats(&self) -> IncrementalStats

Get statistics about the incremental construction

Trait Implementations

impl Debug for IncrementalProofBuilder

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

Formats the value using the given formatter.

impl Default for IncrementalProofBuilder

fn default() -> Self

Returns the “default value” for a type.