Struct FormatConverter 

pub struct FormatConverter { /* private fields */ }

Converter for proof formats.

This is a placeholder for future conversion implementations. Currently supports basic error types and scaffolding.

Implementations

impl FormatConverter

pub fn new() -> Self

Create a new format converter.

pub fn strict_mode(self, strict: bool) -> Self

Enable strict mode (fail on information loss).

pub fn add_comments(self, add: bool) -> Self

Enable/disable comment generation.

pub fn drat_to_alethe(&self, drat: &DratProof) -> ConversionResult<AletheProof>

Convert DRAT proof to Alethe proof.

This conversion maps:

• DRAT Add steps to Alethe Input steps (for clauses from the problem)
• Subsequent Add steps to Resolution steps
• Delete steps are skipped (Alethe is monotonic)

Note: This is a best-effort conversion. DRAT proofs are untyped and don’t contain all the information needed for a complete Alethe proof.

Examples

use oxiz_proof::conversion::{FormatConverter};
use oxiz_proof::drat::DratProof;

let converter = FormatConverter::new();
let mut drat = DratProof::new();

// Add some clauses
drat.add_clause(vec![1, 2, -3]);
drat.add_clause(vec![-1, 4]);

// Convert to Alethe
let alethe = converter.drat_to_alethe(&drat).unwrap();
assert_eq!(alethe.len(), 2);

pub fn alethe_to_lfsc( &self, alethe: &AletheProof, ) -> ConversionResult<LfscProof>

Convert Alethe proof to LFSC proof.

This conversion maps:

• Alethe Assume steps to LFSC variable declarations
• Alethe Step steps to LFSC proof term applications
• Alethe rules to corresponding LFSC proof rules

Examples

use oxiz_proof::conversion::FormatConverter;
use oxiz_proof::alethe::{AletheProof, AletheRule};

let converter = FormatConverter::new();
let mut alethe = AletheProof::new();

// Add assumptions and a resolution step
let a1 = alethe.assume("(or p q)");
let a2 = alethe.assume("(not p)");
alethe.resolution(vec!["q".to_string()], vec![a1, a2]);

// Convert to LFSC
let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
assert!(!lfsc.is_empty());

Trait Implementations

impl Default for FormatConverter

fn default() -> Self

Returns the “default value” for a type.