oxiz_proof/
conversion.rs

1//! Format conversion utilities.
2//!
3//! This module provides conversion utilities between different proof formats:
4//! - DRAT to Alethe: Convert SAT proofs to SMT format
5//! - Alethe to LFSC: Convert SMT proofs to typed proof format
6
7use crate::alethe::{AletheProof, AletheRule, AletheStep};
8use crate::drat::{DratProof, DratStep};
9use crate::lfsc::{LfscProof, LfscSort, LfscTerm};
10use std::fmt;
11
12/// Result of format conversion.
13pub type ConversionResult<T> = Result<T, ConversionError>;
14
15/// Errors that can occur during format conversion.
16#[derive(Debug, Clone, PartialEq, Eq)]
17pub enum ConversionError {
18    /// Unsupported conversion
19    UnsupportedConversion { from: String, to: String },
20    /// Information loss during conversion
21    InformationLoss { reason: String },
22    /// Invalid source format
23    InvalidSource { reason: String },
24    /// Conversion failed
25    ConversionFailed { reason: String },
26}
27
28impl fmt::Display for ConversionError {
29    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
30        match self {
31            ConversionError::UnsupportedConversion { from, to } => {
32                write!(f, "Unsupported conversion from {} to {}", from, to)
33            }
34            ConversionError::InformationLoss { reason } => {
35                write!(f, "Information loss during conversion: {}", reason)
36            }
37            ConversionError::InvalidSource { reason } => {
38                write!(f, "Invalid source format: {}", reason)
39            }
40            ConversionError::ConversionFailed { reason } => {
41                write!(f, "Conversion failed: {}", reason)
42            }
43        }
44    }
45}
46
47impl std::error::Error for ConversionError {}
48
49/// Converter for proof formats.
50///
51/// This is a placeholder for future conversion implementations.
52/// Currently supports basic error types and scaffolding.
53pub struct FormatConverter {
54    /// Preserve all information (may fail if not possible)
55    strict_mode: bool,
56    /// Generate comments in target format
57    add_comments: bool,
58}
59
60impl Default for FormatConverter {
61    fn default() -> Self {
62        Self::new()
63    }
64}
65
66impl FormatConverter {
67    /// Create a new format converter.
68    pub fn new() -> Self {
69        Self {
70            strict_mode: false,
71            add_comments: true,
72        }
73    }
74
75    /// Enable strict mode (fail on information loss).
76    pub fn strict_mode(mut self, strict: bool) -> Self {
77        self.strict_mode = strict;
78        self
79    }
80
81    /// Enable/disable comment generation.
82    pub fn add_comments(mut self, add: bool) -> Self {
83        self.add_comments = add;
84        self
85    }
86
87    /// Convert DRAT proof to Alethe proof.
88    ///
89    /// This conversion maps:
90    /// - DRAT Add steps to Alethe Input steps (for clauses from the problem)
91    /// - Subsequent Add steps to Resolution steps
92    /// - Delete steps are skipped (Alethe is monotonic)
93    ///
94    /// Note: This is a best-effort conversion. DRAT proofs are untyped and
95    /// don't contain all the information needed for a complete Alethe proof.
96    ///
97    /// # Examples
98    ///
99    /// ```
100    /// use oxiz_proof::conversion::{FormatConverter};
101    /// use oxiz_proof::drat::DratProof;
102    ///
103    /// let converter = FormatConverter::new();
104    /// let mut drat = DratProof::new();
105    ///
106    /// // Add some clauses
107    /// drat.add_clause(vec![1, 2, -3]);
108    /// drat.add_clause(vec![-1, 4]);
109    ///
110    /// // Convert to Alethe
111    /// let alethe = converter.drat_to_alethe(&drat).unwrap();
112    /// assert_eq!(alethe.len(), 2);
113    /// ```
114    pub fn drat_to_alethe(&self, drat: &DratProof) -> ConversionResult<AletheProof> {
115        let mut alethe = AletheProof::new();
116
117        // Track step indices for premises
118        let mut step_indices = Vec::new();
119
120        for (i, step) in drat.steps().iter().enumerate() {
121            match step {
122                DratStep::Add(clause) => {
123                    // Convert DRAT literals to Alethe terms
124                    let alethe_clause: Vec<String> = clause
125                        .iter()
126                        .map(|&lit| {
127                            if lit == 0 {
128                                // Terminator - skip
129                                return String::new();
130                            }
131                            if lit > 0 {
132                                format!("p{}", lit)
133                            } else {
134                                format!("(not p{})", -lit)
135                            }
136                        })
137                        .filter(|s| !s.is_empty())
138                        .collect();
139
140                    // First few clauses are inputs, later ones are derived
141                    let rule = if i < 5 {
142                        // Heuristic: first clauses are likely from the problem
143                        AletheRule::Input
144                    } else {
145                        // Derived clauses use resolution
146                        AletheRule::Resolution
147                    };
148
149                    // Add the step
150                    let premises = if rule == AletheRule::Resolution && !step_indices.is_empty() {
151                        // Use last two steps as premises (simplified heuristic)
152                        let len = step_indices.len();
153                        if len >= 2 {
154                            vec![step_indices[len - 2], step_indices[len - 1]]
155                        } else {
156                            vec![step_indices[len - 1]]
157                        }
158                    } else {
159                        Vec::new()
160                    };
161
162                    let idx = alethe.step(alethe_clause, rule, premises, Vec::new());
163                    step_indices.push(idx);
164                }
165                DratStep::Delete(_clause) => {
166                    // Alethe is monotonic, so deletions are not represented
167                    // In strict mode, this is an error
168                    if self.strict_mode {
169                        return Err(ConversionError::InformationLoss {
170                            reason:
171                                "DRAT deletions cannot be represented in Alethe (monotonic format)"
172                                    .to_string(),
173                        });
174                    }
175                    // Otherwise, skip the deletion
176                }
177            }
178        }
179
180        Ok(alethe)
181    }
182
183    /// Convert Alethe proof to LFSC proof.
184    ///
185    /// This conversion maps:
186    /// - Alethe Assume steps to LFSC variable declarations
187    /// - Alethe Step steps to LFSC proof term applications
188    /// - Alethe rules to corresponding LFSC proof rules
189    ///
190    /// # Examples
191    ///
192    /// ```
193    /// use oxiz_proof::conversion::FormatConverter;
194    /// use oxiz_proof::alethe::{AletheProof, AletheRule};
195    ///
196    /// let converter = FormatConverter::new();
197    /// let mut alethe = AletheProof::new();
198    ///
199    /// // Add assumptions and a resolution step
200    /// let a1 = alethe.assume("(or p q)");
201    /// let a2 = alethe.assume("(not p)");
202    /// alethe.resolution(vec!["q".to_string()], vec![a1, a2]);
203    ///
204    /// // Convert to LFSC
205    /// let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
206    /// assert!(!lfsc.is_empty());
207    /// ```
208    pub fn alethe_to_lfsc(&self, alethe: &AletheProof) -> ConversionResult<LfscProof> {
209        let mut lfsc = LfscProof::new();
210
211        // Add standard LFSC signatures for boolean reasoning
212        self.add_boolean_signature(&mut lfsc);
213
214        // Convert each Alethe step
215        for step in alethe.steps() {
216            match step {
217                AletheStep::Assume { index, term } => {
218                    // Declare assumption as a proof variable
219                    let var_name = format!("t{}", index);
220                    let formula = Self::term_to_lfsc_term(term)?;
221
222                    // Declare as a proof that the formula holds
223                    lfsc.declare_const(&var_name, LfscSort::Named("proof".to_string()));
224
225                    if self.add_comments {
226                        // Add a comment about the assumption (as a definition)
227                        lfsc.define(
228                            format!("{}_formula", var_name),
229                            LfscSort::Named("formula".to_string()),
230                            formula,
231                        );
232                    }
233                }
234                AletheStep::Step {
235                    index,
236                    clause,
237                    rule,
238                    premises,
239                    args: _args,
240                } => {
241                    let var_name = format!("t{}", index);
242
243                    // Build LFSC proof term
244                    let proof_term = self.alethe_rule_to_lfsc(*rule, clause, premises)?;
245
246                    // Define the proof step
247                    lfsc.define(var_name, LfscSort::Named("proof".to_string()), proof_term);
248                }
249                AletheStep::Anchor { step, args } => {
250                    // Anchors represent local scopes in Alethe
251                    // In LFSC, we can represent this as a lambda abstraction
252                    let var_name = format!("anchor{}", step);
253
254                    // Create lambda for each argument
255                    let mut body = LfscTerm::Var(var_name.clone());
256                    for (arg_name, arg_sort) in args.iter().rev() {
257                        let sort = Self::parse_sort(arg_sort)?;
258                        body = LfscTerm::Lambda(arg_name.clone(), Box::new(sort), Box::new(body));
259                    }
260
261                    lfsc.define(var_name, LfscSort::Named("proof".to_string()), body);
262                }
263                AletheStep::DefineFun {
264                    name,
265                    args,
266                    return_sort,
267                    body,
268                } => {
269                    // Convert to LFSC definition
270                    let lfsc_sort = Self::parse_sort(return_sort)?;
271                    let lfsc_body = Self::term_to_lfsc_term(body)?;
272
273                    // Wrap in lambdas for each argument
274                    let mut def_body = lfsc_body;
275                    for (arg_name, arg_sort) in args.iter().rev() {
276                        let sort = Self::parse_sort(arg_sort)?;
277                        def_body =
278                            LfscTerm::Lambda(arg_name.clone(), Box::new(sort), Box::new(def_body));
279                    }
280
281                    lfsc.define(name.clone(), lfsc_sort, def_body);
282                }
283            }
284        }
285
286        Ok(lfsc)
287    }
288
289    /// Add standard boolean signature to LFSC proof
290    fn add_boolean_signature(&self, lfsc: &mut LfscProof) {
291        // Declare formula sort
292        lfsc.declare_sort("formula", 0);
293
294        // Declare proof sort
295        lfsc.declare_sort("proof", 0);
296
297        // Declare holds predicate
298        lfsc.declare_const(
299            "holds",
300            LfscSort::Arrow(
301                Box::new(LfscSort::Named("formula".to_string())),
302                Box::new(LfscSort::Type),
303            ),
304        );
305
306        // Declare boolean connectives
307        lfsc.declare_const("true", LfscSort::Named("formula".to_string()));
308        lfsc.declare_const("false", LfscSort::Named("formula".to_string()));
309
310        lfsc.declare_const(
311            "not",
312            LfscSort::Arrow(
313                Box::new(LfscSort::Named("formula".to_string())),
314                Box::new(LfscSort::Named("formula".to_string())),
315            ),
316        );
317
318        lfsc.declare_const(
319            "and",
320            LfscSort::Arrow(
321                Box::new(LfscSort::Named("formula".to_string())),
322                Box::new(LfscSort::Arrow(
323                    Box::new(LfscSort::Named("formula".to_string())),
324                    Box::new(LfscSort::Named("formula".to_string())),
325                )),
326            ),
327        );
328
329        lfsc.declare_const(
330            "or",
331            LfscSort::Arrow(
332                Box::new(LfscSort::Named("formula".to_string())),
333                Box::new(LfscSort::Arrow(
334                    Box::new(LfscSort::Named("formula".to_string())),
335                    Box::new(LfscSort::Named("formula".to_string())),
336                )),
337            ),
338        );
339    }
340
341    /// Convert Alethe rule to LFSC proof term
342    fn alethe_rule_to_lfsc(
343        &self,
344        rule: AletheRule,
345        _clause: &[String],
346        premises: &[u32],
347    ) -> ConversionResult<LfscTerm> {
348        // Map Alethe rules to LFSC proof rule applications
349        let rule_name = match rule {
350            AletheRule::Resolution => "resolution",
351            AletheRule::Trans => "trans",
352            AletheRule::Cong => "cong",
353            AletheRule::Refl => "refl",
354            AletheRule::Symm => "symm",
355            AletheRule::EqRefl => "eq_refl",
356            AletheRule::EqSymm => "eq_symm",
357            AletheRule::EqTrans => "eq_trans",
358            AletheRule::EqCong => "eq_cong",
359            AletheRule::Input => "input",
360            _ => {
361                return Err(ConversionError::UnsupportedConversion {
362                    from: format!("Alethe rule {:?}", rule),
363                    to: "LFSC".to_string(),
364                });
365            }
366        };
367
368        // Build application of rule to premises
369        let premise_terms: Vec<LfscTerm> = premises
370            .iter()
371            .map(|&idx| LfscTerm::Var(format!("t{}", idx)))
372            .collect();
373
374        Ok(LfscTerm::App(rule_name.to_string(), premise_terms))
375    }
376
377    /// Convert SMT-LIB term string to LFSC term
378    ///
379    /// This is an improved parser that handles:
380    /// - Nested s-expressions
381    /// - Negative numbers
382    /// - Rational literals
383    /// - Proper tokenization
384    fn term_to_lfsc_term(term: &str) -> ConversionResult<LfscTerm> {
385        let trimmed = term.trim();
386
387        // Handle boolean literals
388        if trimmed == "true" {
389            return Ok(LfscTerm::True);
390        } else if trimmed == "false" {
391            return Ok(LfscTerm::False);
392        }
393
394        // Handle s-expressions
395        if trimmed.starts_with('(') && trimmed.ends_with(')') {
396            return Self::parse_sexpr(trimmed);
397        }
398
399        // Handle numeric literals
400        if let Some(term) = Self::try_parse_number(trimmed) {
401            return Ok(term);
402        }
403
404        // Everything else is a variable/symbol
405        Ok(LfscTerm::Var(trimmed.to_string()))
406    }
407
408    /// Try to parse a number (integer or rational)
409    fn try_parse_number(s: &str) -> Option<LfscTerm> {
410        // Try parsing as rational (e.g., "3/4")
411        if let Some(slash_pos) = s.find('/') {
412            let num_str = &s[..slash_pos];
413            let den_str = &s[slash_pos + 1..];
414
415            if let (Ok(num), Ok(den)) = (num_str.parse::<i64>(), den_str.parse::<i64>()) {
416                return Some(LfscTerm::RatLit(num, den));
417            }
418        }
419
420        // Try parsing as integer
421        if let Ok(n) = s.parse::<i64>() {
422            return Some(LfscTerm::IntLit(n));
423        }
424
425        None
426    }
427
428    /// Parse an s-expression into an LFSC term
429    fn parse_sexpr(s: &str) -> ConversionResult<LfscTerm> {
430        let inner = &s[1..s.len() - 1].trim();
431
432        if inner.is_empty() {
433            return Err(ConversionError::InvalidSource {
434                reason: "Empty s-expression".to_string(),
435            });
436        }
437
438        // Tokenize the s-expression (handling nested parens)
439        let tokens = Self::tokenize_sexpr(inner)?;
440
441        if tokens.is_empty() {
442            return Err(ConversionError::InvalidSource {
443                reason: "Empty s-expression".to_string(),
444            });
445        }
446
447        let func = &tokens[0];
448        let args: ConversionResult<Vec<LfscTerm>> = tokens[1..]
449            .iter()
450            .map(|arg| Self::term_to_lfsc_term(arg))
451            .collect();
452
453        Ok(LfscTerm::App(func.to_string(), args?))
454    }
455
456    /// Tokenize an s-expression, respecting nested parentheses
457    fn tokenize_sexpr(s: &str) -> ConversionResult<Vec<String>> {
458        let mut tokens = Vec::new();
459        let mut current = String::new();
460        let mut depth = 0;
461        let mut in_string = false;
462
463        for ch in s.chars() {
464            match ch {
465                '"' => {
466                    in_string = !in_string;
467                    current.push(ch);
468                }
469                '(' if !in_string => {
470                    if depth == 0 && !current.trim().is_empty() {
471                        tokens.push(current.trim().to_string());
472                        current.clear();
473                    }
474                    depth += 1;
475                    current.push(ch);
476                }
477                ')' if !in_string => {
478                    depth -= 1;
479                    current.push(ch);
480                    if depth == 0 {
481                        tokens.push(current.trim().to_string());
482                        current.clear();
483                    }
484                }
485                ' ' | '\t' | '\n' if !in_string && depth == 0 => {
486                    if !current.trim().is_empty() {
487                        tokens.push(current.trim().to_string());
488                        current.clear();
489                    }
490                }
491                _ => {
492                    current.push(ch);
493                }
494            }
495        }
496
497        if in_string {
498            return Err(ConversionError::InvalidSource {
499                reason: "Unterminated string literal".to_string(),
500            });
501        }
502
503        if depth != 0 {
504            return Err(ConversionError::InvalidSource {
505                reason: "Unbalanced parentheses in s-expression".to_string(),
506            });
507        }
508
509        if !current.trim().is_empty() {
510            tokens.push(current.trim().to_string());
511        }
512
513        Ok(tokens)
514    }
515
516    /// Parse SMT-LIB sort string to LFSC sort
517    fn parse_sort(sort: &str) -> ConversionResult<LfscSort> {
518        match sort.trim() {
519            "Bool" => Ok(LfscSort::Bool),
520            "Int" => Ok(LfscSort::Int),
521            "Real" => Ok(LfscSort::Real),
522            s if s.starts_with("(_ BitVec ") => {
523                // Parse bitvector width
524                let width_str = s.trim_start_matches("(_ BitVec ").trim_end_matches(')');
525                let width =
526                    width_str
527                        .parse::<u32>()
528                        .map_err(|_| ConversionError::InvalidSource {
529                            reason: format!("Invalid bitvector width: {}", width_str),
530                        })?;
531                Ok(LfscSort::BitVec(width))
532            }
533            other => Ok(LfscSort::Named(other.to_string())),
534        }
535    }
536}
537
538#[cfg(test)]
539mod tests {
540    use super::*;
541    use proptest::prelude::*;
542
543    #[test]
544    fn test_converter_new() {
545        let converter = FormatConverter::new();
546        assert!(!converter.strict_mode);
547        assert!(converter.add_comments);
548    }
549
550    #[test]
551    fn test_converter_with_settings() {
552        let converter = FormatConverter::new().strict_mode(true).add_comments(false);
553        assert!(converter.strict_mode);
554        assert!(!converter.add_comments);
555    }
556
557    #[test]
558    fn test_conversion_error_display() {
559        let err = ConversionError::UnsupportedConversion {
560            from: "DRAT".to_string(),
561            to: "Coq".to_string(),
562        };
563        assert!(err.to_string().contains("Unsupported conversion"));
564    }
565
566    // DRAT to Alethe conversion tests
567
568    #[test]
569    fn test_drat_to_alethe_empty() {
570        let converter = FormatConverter::new();
571        let drat = DratProof::new();
572        let alethe = converter
573            .drat_to_alethe(&drat)
574            .expect("test operation should succeed");
575
576        assert!(alethe.is_empty());
577    }
578
579    #[test]
580    fn test_drat_to_alethe_single_clause() {
581        let converter = FormatConverter::new();
582        let mut drat = DratProof::new();
583        drat.add_clause(vec![1, 2, -3]);
584
585        let alethe = converter
586            .drat_to_alethe(&drat)
587            .expect("test operation should succeed");
588
589        assert_eq!(alethe.len(), 1);
590        let output = alethe.to_string();
591        assert!(output.contains("p1"));
592        assert!(output.contains("p2"));
593        assert!(output.contains("(not p3)"));
594    }
595
596    #[test]
597    fn test_drat_to_alethe_multiple_clauses() {
598        let converter = FormatConverter::new();
599        let mut drat = DratProof::new();
600        drat.add_clause(vec![1, 2]);
601        drat.add_clause(vec![-1, 3]);
602        drat.add_clause(vec![-2, 4]);
603        drat.add_clause(vec![2, -3]);
604
605        let alethe = converter
606            .drat_to_alethe(&drat)
607            .expect("test operation should succeed");
608
609        assert_eq!(alethe.len(), 4);
610        // First clauses should be Input
611        let output = alethe.to_string();
612        assert!(output.contains(":rule input"));
613    }
614
615    #[test]
616    fn test_drat_to_alethe_with_resolution() {
617        let converter = FormatConverter::new();
618        let mut drat = DratProof::new();
619
620        // Add enough clauses to trigger resolution heuristic
621        for i in 1..=6 {
622            drat.add_clause(vec![i, -i]);
623        }
624
625        let alethe = converter
626            .drat_to_alethe(&drat)
627            .expect("test operation should succeed");
628
629        assert_eq!(alethe.len(), 6);
630        let output = alethe.to_string();
631        // Later clauses should use resolution
632        assert!(output.contains(":rule resolution"));
633    }
634
635    #[test]
636    fn test_drat_to_alethe_with_deletion_non_strict() {
637        let converter = FormatConverter::new();
638        let mut drat = DratProof::new();
639        drat.add_clause(vec![1, 2]);
640        drat.delete_clause(vec![1, 2]);
641        drat.add_clause(vec![3, 4]);
642
643        // Should succeed in non-strict mode, skipping deletion
644        let alethe = converter
645            .drat_to_alethe(&drat)
646            .expect("test operation should succeed");
647
648        // Only the additions should be present
649        assert_eq!(alethe.len(), 2);
650    }
651
652    #[test]
653    fn test_drat_to_alethe_with_deletion_strict() {
654        let converter = FormatConverter::new().strict_mode(true);
655        let mut drat = DratProof::new();
656        drat.add_clause(vec![1, 2]);
657        drat.delete_clause(vec![1, 2]);
658
659        // Should fail in strict mode
660        let result = converter.drat_to_alethe(&drat);
661        assert!(result.is_err());
662
663        if let Err(ConversionError::InformationLoss { reason }) = result {
664            assert!(reason.contains("monotonic"));
665        } else {
666            panic!("Expected InformationLoss error");
667        }
668    }
669
670    #[test]
671    fn test_drat_to_alethe_empty_clause() {
672        let converter = FormatConverter::new();
673        let mut drat = DratProof::new();
674        drat.add_clause(vec![1]);
675        drat.add_clause(vec![-1]);
676        drat.add_clause(vec![]); // Empty clause (contradiction)
677
678        let alethe = converter
679            .drat_to_alethe(&drat)
680            .expect("test operation should succeed");
681
682        assert_eq!(alethe.len(), 3);
683        let output = alethe.to_string();
684        // Empty clause represented as (cl)
685        assert!(output.contains("(cl)"));
686    }
687
688    // Alethe to LFSC conversion tests
689
690    #[test]
691    fn test_alethe_to_lfsc_empty() {
692        let converter = FormatConverter::new();
693        let alethe = AletheProof::new();
694        let lfsc = converter
695            .alethe_to_lfsc(&alethe)
696            .expect("test operation should succeed");
697
698        // Should have the boolean signature
699        assert!(!lfsc.is_empty());
700        let output = lfsc.to_string();
701        assert!(output.contains("formula"));
702        assert!(output.contains("proof"));
703    }
704
705    #[test]
706    fn test_alethe_to_lfsc_assumption() {
707        let converter = FormatConverter::new();
708        let mut alethe = AletheProof::new();
709        alethe.assume("(= x 5)");
710
711        let lfsc = converter
712            .alethe_to_lfsc(&alethe)
713            .expect("test operation should succeed");
714
715        let output = lfsc.to_string();
716        assert!(output.contains("t1"));
717        assert!(output.contains("proof"));
718    }
719
720    #[test]
721    fn test_alethe_to_lfsc_resolution() {
722        let converter = FormatConverter::new();
723        let mut alethe = AletheProof::new();
724        let a1 = alethe.assume("(or p q)");
725        let a2 = alethe.assume("(not p)");
726        alethe.resolution(vec!["q".to_string()], vec![a1, a2]);
727
728        let lfsc = converter
729            .alethe_to_lfsc(&alethe)
730            .expect("test operation should succeed");
731
732        let output = lfsc.to_string();
733        assert!(output.contains("resolution"));
734        assert!(output.contains("t1"));
735        assert!(output.contains("t2"));
736        assert!(output.contains("t3"));
737    }
738
739    #[test]
740    fn test_alethe_to_lfsc_equality_rules() {
741        let converter = FormatConverter::new();
742        let mut alethe = AletheProof::new();
743
744        alethe.step_simple(vec!["(= x x)".to_string()], AletheRule::EqRefl);
745        alethe.step_simple(vec!["(= y x)".to_string()], AletheRule::EqSymm);
746
747        let lfsc = converter
748            .alethe_to_lfsc(&alethe)
749            .expect("test operation should succeed");
750
751        let output = lfsc.to_string();
752        assert!(output.contains("eq_refl"));
753        assert!(output.contains("eq_symm"));
754    }
755
756    #[test]
757    fn test_alethe_to_lfsc_anchor() {
758        let converter = FormatConverter::new();
759        let mut alethe = AletheProof::new();
760
761        alethe.anchor(vec![("x".to_string(), "Int".to_string())]);
762
763        let lfsc = converter
764            .alethe_to_lfsc(&alethe)
765            .expect("test operation should succeed");
766
767        let output = lfsc.to_string();
768        assert!(output.contains("anchor1"));
769    }
770
771    #[test]
772    fn test_alethe_to_lfsc_define_fun() {
773        let converter = FormatConverter::new();
774        let mut alethe = AletheProof::new();
775
776        alethe.define_fun(
777            "f",
778            vec![("x".to_string(), "Int".to_string())],
779            "Int",
780            "(+ x 1)",
781        );
782
783        let lfsc = converter
784            .alethe_to_lfsc(&alethe)
785            .expect("test operation should succeed");
786
787        let output = lfsc.to_string();
788        assert!(output.contains("(define f"));
789    }
790
791    #[test]
792    fn test_alethe_to_lfsc_with_comments() {
793        let converter = FormatConverter::new().add_comments(true);
794        let mut alethe = AletheProof::new();
795        alethe.assume("(= x 5)");
796
797        let lfsc = converter
798            .alethe_to_lfsc(&alethe)
799            .expect("test operation should succeed");
800
801        let output = lfsc.to_string();
802        assert!(output.contains("t1_formula"));
803    }
804
805    #[test]
806    fn test_alethe_to_lfsc_without_comments() {
807        let converter = FormatConverter::new().add_comments(false);
808        let mut alethe = AletheProof::new();
809        alethe.assume("(= x 5)");
810
811        let lfsc = converter
812            .alethe_to_lfsc(&alethe)
813            .expect("test operation should succeed");
814
815        let output = lfsc.to_string();
816        assert!(!output.contains("t1_formula"));
817    }
818
819    #[test]
820    fn test_alethe_to_lfsc_unsupported_rule() {
821        let converter = FormatConverter::new();
822        let mut alethe = AletheProof::new();
823
824        // Use a rule that doesn't have LFSC mapping
825        alethe.step_simple(vec!["p".to_string()], AletheRule::Skolem);
826
827        let result = converter.alethe_to_lfsc(&alethe);
828        assert!(result.is_err());
829
830        if let Err(ConversionError::UnsupportedConversion { from, to }) = result {
831            assert!(from.contains("Skolem"));
832            assert_eq!(to, "LFSC");
833        } else {
834            panic!("Expected UnsupportedConversion error");
835        }
836    }
837
838    // Helper function tests
839
840    #[test]
841    fn test_term_to_lfsc_term_literals() {
842        assert!(matches!(
843            FormatConverter::term_to_lfsc_term("true"),
844            Ok(LfscTerm::True)
845        ));
846        assert!(matches!(
847            FormatConverter::term_to_lfsc_term("false"),
848            Ok(LfscTerm::False)
849        ));
850        assert!(matches!(
851            FormatConverter::term_to_lfsc_term("42"),
852            Ok(LfscTerm::IntLit(42))
853        ));
854    }
855
856    #[test]
857    fn test_term_to_lfsc_term_variable() {
858        if let Ok(LfscTerm::Var(name)) = FormatConverter::term_to_lfsc_term("x") {
859            assert_eq!(name, "x");
860        } else {
861            panic!("Expected Var term");
862        }
863    }
864
865    #[test]
866    fn test_term_to_lfsc_term_application() {
867        if let Ok(LfscTerm::App(func, args)) = FormatConverter::term_to_lfsc_term("(+ x y)") {
868            assert_eq!(func, "+");
869            assert_eq!(args.len(), 2);
870        } else {
871            panic!("Expected App term");
872        }
873    }
874
875    #[test]
876    fn test_term_to_lfsc_term_nested() {
877        // Test nested s-expressions
878        if let Ok(LfscTerm::App(func, args)) = FormatConverter::term_to_lfsc_term("(+ (* 2 x) y)") {
879            assert_eq!(func, "+");
880            assert_eq!(args.len(), 2);
881
882            // First arg should be (* 2 x)
883            if let LfscTerm::App(inner_func, inner_args) = &args[0] {
884                assert_eq!(inner_func, "*");
885                assert_eq!(inner_args.len(), 2);
886            } else {
887                panic!("Expected nested App term");
888            }
889        } else {
890            panic!("Expected App term");
891        }
892    }
893
894    #[test]
895    fn test_term_to_lfsc_term_negative_number() {
896        if let Ok(LfscTerm::IntLit(n)) = FormatConverter::term_to_lfsc_term("-42") {
897            assert_eq!(n, -42);
898        } else {
899            panic!("Expected IntLit term");
900        }
901    }
902
903    #[test]
904    fn test_term_to_lfsc_term_rational() {
905        if let Ok(LfscTerm::RatLit(num, den)) = FormatConverter::term_to_lfsc_term("3/4") {
906            assert_eq!(num, 3);
907            assert_eq!(den, 4);
908        } else {
909            panic!("Expected RatLit term");
910        }
911    }
912
913    #[test]
914    fn test_term_to_lfsc_term_negative_rational() {
915        if let Ok(LfscTerm::RatLit(num, den)) = FormatConverter::term_to_lfsc_term("-5/7") {
916            assert_eq!(num, -5);
917            assert_eq!(den, 7);
918        } else {
919            panic!("Expected RatLit term");
920        }
921    }
922
923    #[test]
924    fn test_term_to_lfsc_term_complex_nested() {
925        // (= (+ x (* 3 y)) z)
926        let term = "(= (+ x (* 3 y)) z)";
927        let result = FormatConverter::term_to_lfsc_term(term);
928
929        assert!(result.is_ok());
930        if let Ok(LfscTerm::App(func, args)) = result {
931            assert_eq!(func, "=");
932            assert_eq!(args.len(), 2);
933        } else {
934            panic!("Expected App term");
935        }
936    }
937
938    #[test]
939    fn test_tokenize_sexpr_simple() {
940        let tokens =
941            FormatConverter::tokenize_sexpr("+ x y").expect("test operation should succeed");
942        assert_eq!(tokens, vec!["+", "x", "y"]);
943    }
944
945    #[test]
946    fn test_tokenize_sexpr_nested() {
947        let tokens =
948            FormatConverter::tokenize_sexpr("+ (- x y) z").expect("test operation should succeed");
949        assert_eq!(tokens, vec!["+", "(- x y)", "z"]);
950    }
951
952    #[test]
953    fn test_tokenize_sexpr_deeply_nested() {
954        let tokens = FormatConverter::tokenize_sexpr("f (g (h x)) y")
955            .expect("test operation should succeed");
956        assert_eq!(tokens, vec!["f", "(g (h x))", "y"]);
957    }
958
959    #[test]
960    fn test_tokenize_sexpr_unbalanced() {
961        let result = FormatConverter::tokenize_sexpr("+ (x y z");
962        assert!(result.is_err());
963
964        if let Err(ConversionError::InvalidSource { reason }) = result {
965            assert!(reason.contains("Unbalanced parentheses"));
966        } else {
967            panic!("Expected InvalidSource error");
968        }
969    }
970
971    #[test]
972    fn test_parse_sort_basic() {
973        assert!(matches!(
974            FormatConverter::parse_sort("Bool"),
975            Ok(LfscSort::Bool)
976        ));
977        assert!(matches!(
978            FormatConverter::parse_sort("Int"),
979            Ok(LfscSort::Int)
980        ));
981        assert!(matches!(
982            FormatConverter::parse_sort("Real"),
983            Ok(LfscSort::Real)
984        ));
985    }
986
987    #[test]
988    fn test_parse_sort_bitvector() {
989        if let Ok(LfscSort::BitVec(width)) = FormatConverter::parse_sort("(_ BitVec 32)") {
990            assert_eq!(width, 32);
991        } else {
992            panic!("Expected BitVec sort");
993        }
994    }
995
996    #[test]
997    fn test_parse_sort_named() {
998        if let Ok(LfscSort::Named(name)) = FormatConverter::parse_sort("MySort") {
999            assert_eq!(name, "MySort");
1000        } else {
1001            panic!("Expected Named sort");
1002        }
1003    }
1004
1005    #[test]
1006    fn test_information_loss_error_display() {
1007        let err = ConversionError::InformationLoss {
1008            reason: "test reason".to_string(),
1009        };
1010        assert!(err.to_string().contains("Information loss"));
1011        assert!(err.to_string().contains("test reason"));
1012    }
1013
1014    #[test]
1015    fn test_invalid_source_error_display() {
1016        let err = ConversionError::InvalidSource {
1017            reason: "bad input".to_string(),
1018        };
1019        assert!(err.to_string().contains("Invalid source"));
1020        assert!(err.to_string().contains("bad input"));
1021    }
1022
1023    #[test]
1024    fn test_conversion_failed_error_display() {
1025        let err = ConversionError::ConversionFailed {
1026            reason: "conversion issue".to_string(),
1027        };
1028        assert!(err.to_string().contains("Conversion failed"));
1029        assert!(err.to_string().contains("conversion issue"));
1030    }
1031
1032    // Property-based tests
1033
1034    proptest! {
1035        /// DRAT to Alethe conversion should never lose steps (except deletions in non-strict mode)
1036        #[test]
1037        fn prop_drat_to_alethe_preserves_additions(
1038            clauses in prop::collection::vec(
1039                prop::collection::vec(-100i32..100i32, 0..5),
1040                0..20
1041            )
1042        ) {
1043            let converter = FormatConverter::new();
1044            let mut drat = DratProof::new();
1045
1046            let mut add_count = 0;
1047            for clause in clauses {
1048                drat.add_clause(clause);
1049                add_count += 1;
1050            }
1051
1052            let alethe = converter.drat_to_alethe(&drat).expect("test operation should succeed");
1053
1054            // Alethe should have the same number of steps as DRAT additions
1055            prop_assert_eq!(alethe.len(), add_count);
1056        }
1057
1058        /// DRAT to Alethe conversion should fail in strict mode with deletions
1059        #[test]
1060        fn prop_drat_deletion_strict_mode_fails(
1061            clauses in prop::collection::vec(-100i32..100i32, 1..5)
1062        ) {
1063            let converter = FormatConverter::new().strict_mode(true);
1064            let mut drat = DratProof::new();
1065
1066            drat.add_clause(clauses.clone());
1067            drat.delete_clause(clauses);
1068
1069            let result = converter.drat_to_alethe(&drat);
1070            prop_assert!(result.is_err());
1071        }
1072
1073        /// Alethe to LFSC conversion should always produce non-empty LFSC (due to signature)
1074        #[test]
1075        fn prop_alethe_to_lfsc_nonempty(
1076            num_assumptions in 0usize..10
1077        ) {
1078            let converter = FormatConverter::new();
1079            let mut alethe = AletheProof::new();
1080
1081            for i in 0..num_assumptions {
1082                alethe.assume(format!("p{}", i));
1083            }
1084
1085            let lfsc = converter.alethe_to_lfsc(&alethe).expect("test operation should succeed");
1086
1087            // LFSC should never be empty because of the boolean signature
1088            prop_assert!(!lfsc.is_empty());
1089        }
1090
1091        /// Term parsing should be deterministic
1092        #[test]
1093        fn prop_term_parsing_deterministic(
1094            term in "[a-z][a-z0-9]{0,5}"
1095        ) {
1096            let result1 = FormatConverter::term_to_lfsc_term(&term);
1097            let result2 = FormatConverter::term_to_lfsc_term(&term);
1098
1099            prop_assert_eq!(
1100                result1.is_ok(),
1101                result2.is_ok(),
1102                "Parsing determinism violated"
1103            );
1104        }
1105
1106        /// Sort parsing should accept basic sorts
1107        #[test]
1108        fn prop_sort_parsing_basic(
1109            sort in prop::sample::select(vec!["Bool", "Int", "Real"])
1110        ) {
1111            let result = FormatConverter::parse_sort(sort);
1112            prop_assert!(result.is_ok());
1113        }
1114
1115        /// BitVec parsing should handle various widths
1116        #[test]
1117        fn prop_bitvec_parsing(
1118            width in 1u32..256
1119        ) {
1120            let sort_str = format!("(_ BitVec {})", width);
1121            let result = FormatConverter::parse_sort(&sort_str);
1122
1123            prop_assert!(result.is_ok());
1124            if let Ok(LfscSort::BitVec(w)) = result {
1125                prop_assert_eq!(w, width);
1126            }
1127        }
1128
1129        /// Conversion errors should always have non-empty messages
1130        #[test]
1131        fn prop_conversion_errors_nonempty(
1132            reason in "[a-zA-Z ]{1,50}"
1133        ) {
1134            let errors = vec![
1135                ConversionError::InformationLoss { reason: reason.clone() },
1136                ConversionError::InvalidSource { reason: reason.clone() },
1137                ConversionError::ConversionFailed { reason },
1138            ];
1139
1140            for err in errors {
1141                let msg = err.to_string();
1142                prop_assert!(!msg.is_empty());
1143            }
1144        }
1145
1146        /// DRAT clauses with zero literals should be handled correctly
1147        #[test]
1148        fn prop_drat_empty_clause_handling(
1149            prefix_clauses in prop::collection::vec(
1150                prop::collection::vec(-10i32..10i32, 1..3),
1151                0..5
1152            )
1153        ) {
1154            let converter = FormatConverter::new();
1155            let mut drat = DratProof::new();
1156
1157            // Add prefix clauses
1158            for clause in prefix_clauses {
1159                drat.add_clause(clause);
1160            }
1161
1162            // Add empty clause (contradiction)
1163            drat.add_clause(vec![]);
1164
1165            let alethe = converter.drat_to_alethe(&drat).expect("test operation should succeed");
1166
1167            // Should successfully convert
1168            prop_assert!(!alethe.is_empty());
1169        }
1170
1171        /// Alethe to LFSC with multiple resolution steps
1172        #[test]
1173        fn prop_alethe_resolution_chain(
1174            chain_length in 1usize..10
1175        ) {
1176            let converter = FormatConverter::new();
1177            let mut alethe = AletheProof::new();
1178
1179            // Build a chain of resolution steps
1180            let mut indices = Vec::new();
1181            for i in 0..chain_length {
1182                let idx = alethe.assume(format!("p{}", i));
1183                indices.push(idx);
1184            }
1185
1186            // Add resolution step using first two assumptions
1187            if indices.len() >= 2 {
1188                alethe.resolution(
1189                    vec!["q".to_string()],
1190                    vec![indices[0], indices[1]]
1191                );
1192            }
1193
1194            let lfsc = converter.alethe_to_lfsc(&alethe).expect("test operation should succeed");
1195
1196            // Should succeed
1197            prop_assert!(!lfsc.is_empty());
1198        }
1199
1200        /// FormatConverter settings should be preserved
1201        #[test]
1202        fn prop_converter_settings_preserved(
1203            strict in prop::bool::ANY,
1204            comments in prop::bool::ANY
1205        ) {
1206            let converter = FormatConverter::new()
1207                .strict_mode(strict)
1208                .add_comments(comments);
1209
1210            prop_assert_eq!(converter.strict_mode, strict);
1211            prop_assert_eq!(converter.add_comments, comments);
1212        }
1213    }
1214}
oxiz_proof/conversion.rs

oxiz_proof/
conversion.rs
