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.drat_to_alethe(&drat).unwrap();
573
574        assert!(alethe.is_empty());
575    }
576
577    #[test]
578    fn test_drat_to_alethe_single_clause() {
579        let converter = FormatConverter::new();
580        let mut drat = DratProof::new();
581        drat.add_clause(vec![1, 2, -3]);
582
583        let alethe = converter.drat_to_alethe(&drat).unwrap();
584
585        assert_eq!(alethe.len(), 1);
586        let output = alethe.to_string();
587        assert!(output.contains("p1"));
588        assert!(output.contains("p2"));
589        assert!(output.contains("(not p3)"));
590    }
591
592    #[test]
593    fn test_drat_to_alethe_multiple_clauses() {
594        let converter = FormatConverter::new();
595        let mut drat = DratProof::new();
596        drat.add_clause(vec![1, 2]);
597        drat.add_clause(vec![-1, 3]);
598        drat.add_clause(vec![-2, 4]);
599        drat.add_clause(vec![2, -3]);
600
601        let alethe = converter.drat_to_alethe(&drat).unwrap();
602
603        assert_eq!(alethe.len(), 4);
604        // First clauses should be Input
605        let output = alethe.to_string();
606        assert!(output.contains(":rule input"));
607    }
608
609    #[test]
610    fn test_drat_to_alethe_with_resolution() {
611        let converter = FormatConverter::new();
612        let mut drat = DratProof::new();
613
614        // Add enough clauses to trigger resolution heuristic
615        for i in 1..=6 {
616            drat.add_clause(vec![i, -i]);
617        }
618
619        let alethe = converter.drat_to_alethe(&drat).unwrap();
620
621        assert_eq!(alethe.len(), 6);
622        let output = alethe.to_string();
623        // Later clauses should use resolution
624        assert!(output.contains(":rule resolution"));
625    }
626
627    #[test]
628    fn test_drat_to_alethe_with_deletion_non_strict() {
629        let converter = FormatConverter::new();
630        let mut drat = DratProof::new();
631        drat.add_clause(vec![1, 2]);
632        drat.delete_clause(vec![1, 2]);
633        drat.add_clause(vec![3, 4]);
634
635        // Should succeed in non-strict mode, skipping deletion
636        let alethe = converter.drat_to_alethe(&drat).unwrap();
637
638        // Only the additions should be present
639        assert_eq!(alethe.len(), 2);
640    }
641
642    #[test]
643    fn test_drat_to_alethe_with_deletion_strict() {
644        let converter = FormatConverter::new().strict_mode(true);
645        let mut drat = DratProof::new();
646        drat.add_clause(vec![1, 2]);
647        drat.delete_clause(vec![1, 2]);
648
649        // Should fail in strict mode
650        let result = converter.drat_to_alethe(&drat);
651        assert!(result.is_err());
652
653        if let Err(ConversionError::InformationLoss { reason }) = result {
654            assert!(reason.contains("monotonic"));
655        } else {
656            panic!("Expected InformationLoss error");
657        }
658    }
659
660    #[test]
661    fn test_drat_to_alethe_empty_clause() {
662        let converter = FormatConverter::new();
663        let mut drat = DratProof::new();
664        drat.add_clause(vec![1]);
665        drat.add_clause(vec![-1]);
666        drat.add_clause(vec![]); // Empty clause (contradiction)
667
668        let alethe = converter.drat_to_alethe(&drat).unwrap();
669
670        assert_eq!(alethe.len(), 3);
671        let output = alethe.to_string();
672        // Empty clause represented as (cl)
673        assert!(output.contains("(cl)"));
674    }
675
676    // Alethe to LFSC conversion tests
677
678    #[test]
679    fn test_alethe_to_lfsc_empty() {
680        let converter = FormatConverter::new();
681        let alethe = AletheProof::new();
682        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
683
684        // Should have the boolean signature
685        assert!(!lfsc.is_empty());
686        let output = lfsc.to_string();
687        assert!(output.contains("formula"));
688        assert!(output.contains("proof"));
689    }
690
691    #[test]
692    fn test_alethe_to_lfsc_assumption() {
693        let converter = FormatConverter::new();
694        let mut alethe = AletheProof::new();
695        alethe.assume("(= x 5)");
696
697        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
698
699        let output = lfsc.to_string();
700        assert!(output.contains("t1"));
701        assert!(output.contains("proof"));
702    }
703
704    #[test]
705    fn test_alethe_to_lfsc_resolution() {
706        let converter = FormatConverter::new();
707        let mut alethe = AletheProof::new();
708        let a1 = alethe.assume("(or p q)");
709        let a2 = alethe.assume("(not p)");
710        alethe.resolution(vec!["q".to_string()], vec![a1, a2]);
711
712        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
713
714        let output = lfsc.to_string();
715        assert!(output.contains("resolution"));
716        assert!(output.contains("t1"));
717        assert!(output.contains("t2"));
718        assert!(output.contains("t3"));
719    }
720
721    #[test]
722    fn test_alethe_to_lfsc_equality_rules() {
723        let converter = FormatConverter::new();
724        let mut alethe = AletheProof::new();
725
726        alethe.step_simple(vec!["(= x x)".to_string()], AletheRule::EqRefl);
727        alethe.step_simple(vec!["(= y x)".to_string()], AletheRule::EqSymm);
728
729        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
730
731        let output = lfsc.to_string();
732        assert!(output.contains("eq_refl"));
733        assert!(output.contains("eq_symm"));
734    }
735
736    #[test]
737    fn test_alethe_to_lfsc_anchor() {
738        let converter = FormatConverter::new();
739        let mut alethe = AletheProof::new();
740
741        alethe.anchor(vec![("x".to_string(), "Int".to_string())]);
742
743        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
744
745        let output = lfsc.to_string();
746        assert!(output.contains("anchor1"));
747    }
748
749    #[test]
750    fn test_alethe_to_lfsc_define_fun() {
751        let converter = FormatConverter::new();
752        let mut alethe = AletheProof::new();
753
754        alethe.define_fun(
755            "f",
756            vec![("x".to_string(), "Int".to_string())],
757            "Int",
758            "(+ x 1)",
759        );
760
761        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
762
763        let output = lfsc.to_string();
764        assert!(output.contains("(define f"));
765    }
766
767    #[test]
768    fn test_alethe_to_lfsc_with_comments() {
769        let converter = FormatConverter::new().add_comments(true);
770        let mut alethe = AletheProof::new();
771        alethe.assume("(= x 5)");
772
773        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
774
775        let output = lfsc.to_string();
776        assert!(output.contains("t1_formula"));
777    }
778
779    #[test]
780    fn test_alethe_to_lfsc_without_comments() {
781        let converter = FormatConverter::new().add_comments(false);
782        let mut alethe = AletheProof::new();
783        alethe.assume("(= x 5)");
784
785        let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
786
787        let output = lfsc.to_string();
788        assert!(!output.contains("t1_formula"));
789    }
790
791    #[test]
792    fn test_alethe_to_lfsc_unsupported_rule() {
793        let converter = FormatConverter::new();
794        let mut alethe = AletheProof::new();
795
796        // Use a rule that doesn't have LFSC mapping
797        alethe.step_simple(vec!["p".to_string()], AletheRule::Skolem);
798
799        let result = converter.alethe_to_lfsc(&alethe);
800        assert!(result.is_err());
801
802        if let Err(ConversionError::UnsupportedConversion { from, to }) = result {
803            assert!(from.contains("Skolem"));
804            assert_eq!(to, "LFSC");
805        } else {
806            panic!("Expected UnsupportedConversion error");
807        }
808    }
809
810    // Helper function tests
811
812    #[test]
813    fn test_term_to_lfsc_term_literals() {
814        assert!(matches!(
815            FormatConverter::term_to_lfsc_term("true"),
816            Ok(LfscTerm::True)
817        ));
818        assert!(matches!(
819            FormatConverter::term_to_lfsc_term("false"),
820            Ok(LfscTerm::False)
821        ));
822        assert!(matches!(
823            FormatConverter::term_to_lfsc_term("42"),
824            Ok(LfscTerm::IntLit(42))
825        ));
826    }
827
828    #[test]
829    fn test_term_to_lfsc_term_variable() {
830        if let Ok(LfscTerm::Var(name)) = FormatConverter::term_to_lfsc_term("x") {
831            assert_eq!(name, "x");
832        } else {
833            panic!("Expected Var term");
834        }
835    }
836
837    #[test]
838    fn test_term_to_lfsc_term_application() {
839        if let Ok(LfscTerm::App(func, args)) = FormatConverter::term_to_lfsc_term("(+ x y)") {
840            assert_eq!(func, "+");
841            assert_eq!(args.len(), 2);
842        } else {
843            panic!("Expected App term");
844        }
845    }
846
847    #[test]
848    fn test_term_to_lfsc_term_nested() {
849        // Test nested s-expressions
850        if let Ok(LfscTerm::App(func, args)) = FormatConverter::term_to_lfsc_term("(+ (* 2 x) y)") {
851            assert_eq!(func, "+");
852            assert_eq!(args.len(), 2);
853
854            // First arg should be (* 2 x)
855            if let LfscTerm::App(inner_func, inner_args) = &args[0] {
856                assert_eq!(inner_func, "*");
857                assert_eq!(inner_args.len(), 2);
858            } else {
859                panic!("Expected nested App term");
860            }
861        } else {
862            panic!("Expected App term");
863        }
864    }
865
866    #[test]
867    fn test_term_to_lfsc_term_negative_number() {
868        if let Ok(LfscTerm::IntLit(n)) = FormatConverter::term_to_lfsc_term("-42") {
869            assert_eq!(n, -42);
870        } else {
871            panic!("Expected IntLit term");
872        }
873    }
874
875    #[test]
876    fn test_term_to_lfsc_term_rational() {
877        if let Ok(LfscTerm::RatLit(num, den)) = FormatConverter::term_to_lfsc_term("3/4") {
878            assert_eq!(num, 3);
879            assert_eq!(den, 4);
880        } else {
881            panic!("Expected RatLit term");
882        }
883    }
884
885    #[test]
886    fn test_term_to_lfsc_term_negative_rational() {
887        if let Ok(LfscTerm::RatLit(num, den)) = FormatConverter::term_to_lfsc_term("-5/7") {
888            assert_eq!(num, -5);
889            assert_eq!(den, 7);
890        } else {
891            panic!("Expected RatLit term");
892        }
893    }
894
895    #[test]
896    fn test_term_to_lfsc_term_complex_nested() {
897        // (= (+ x (* 3 y)) z)
898        let term = "(= (+ x (* 3 y)) z)";
899        let result = FormatConverter::term_to_lfsc_term(term);
900
901        assert!(result.is_ok());
902        if let Ok(LfscTerm::App(func, args)) = result {
903            assert_eq!(func, "=");
904            assert_eq!(args.len(), 2);
905        } else {
906            panic!("Expected App term");
907        }
908    }
909
910    #[test]
911    fn test_tokenize_sexpr_simple() {
912        let tokens = FormatConverter::tokenize_sexpr("+ x y").unwrap();
913        assert_eq!(tokens, vec!["+", "x", "y"]);
914    }
915
916    #[test]
917    fn test_tokenize_sexpr_nested() {
918        let tokens = FormatConverter::tokenize_sexpr("+ (- x y) z").unwrap();
919        assert_eq!(tokens, vec!["+", "(- x y)", "z"]);
920    }
921
922    #[test]
923    fn test_tokenize_sexpr_deeply_nested() {
924        let tokens = FormatConverter::tokenize_sexpr("f (g (h x)) y").unwrap();
925        assert_eq!(tokens, vec!["f", "(g (h x))", "y"]);
926    }
927
928    #[test]
929    fn test_tokenize_sexpr_unbalanced() {
930        let result = FormatConverter::tokenize_sexpr("+ (x y z");
931        assert!(result.is_err());
932
933        if let Err(ConversionError::InvalidSource { reason }) = result {
934            assert!(reason.contains("Unbalanced parentheses"));
935        } else {
936            panic!("Expected InvalidSource error");
937        }
938    }
939
940    #[test]
941    fn test_parse_sort_basic() {
942        assert!(matches!(
943            FormatConverter::parse_sort("Bool"),
944            Ok(LfscSort::Bool)
945        ));
946        assert!(matches!(
947            FormatConverter::parse_sort("Int"),
948            Ok(LfscSort::Int)
949        ));
950        assert!(matches!(
951            FormatConverter::parse_sort("Real"),
952            Ok(LfscSort::Real)
953        ));
954    }
955
956    #[test]
957    fn test_parse_sort_bitvector() {
958        if let Ok(LfscSort::BitVec(width)) = FormatConverter::parse_sort("(_ BitVec 32)") {
959            assert_eq!(width, 32);
960        } else {
961            panic!("Expected BitVec sort");
962        }
963    }
964
965    #[test]
966    fn test_parse_sort_named() {
967        if let Ok(LfscSort::Named(name)) = FormatConverter::parse_sort("MySort") {
968            assert_eq!(name, "MySort");
969        } else {
970            panic!("Expected Named sort");
971        }
972    }
973
974    #[test]
975    fn test_information_loss_error_display() {
976        let err = ConversionError::InformationLoss {
977            reason: "test reason".to_string(),
978        };
979        assert!(err.to_string().contains("Information loss"));
980        assert!(err.to_string().contains("test reason"));
981    }
982
983    #[test]
984    fn test_invalid_source_error_display() {
985        let err = ConversionError::InvalidSource {
986            reason: "bad input".to_string(),
987        };
988        assert!(err.to_string().contains("Invalid source"));
989        assert!(err.to_string().contains("bad input"));
990    }
991
992    #[test]
993    fn test_conversion_failed_error_display() {
994        let err = ConversionError::ConversionFailed {
995            reason: "conversion issue".to_string(),
996        };
997        assert!(err.to_string().contains("Conversion failed"));
998        assert!(err.to_string().contains("conversion issue"));
999    }
1000
1001    // Property-based tests
1002
1003    proptest! {
1004        /// DRAT to Alethe conversion should never lose steps (except deletions in non-strict mode)
1005        #[test]
1006        fn prop_drat_to_alethe_preserves_additions(
1007            clauses in prop::collection::vec(
1008                prop::collection::vec(-100i32..100i32, 0..5),
1009                0..20
1010            )
1011        ) {
1012            let converter = FormatConverter::new();
1013            let mut drat = DratProof::new();
1014
1015            let mut add_count = 0;
1016            for clause in clauses {
1017                drat.add_clause(clause);
1018                add_count += 1;
1019            }
1020
1021            let alethe = converter.drat_to_alethe(&drat).unwrap();
1022
1023            // Alethe should have the same number of steps as DRAT additions
1024            prop_assert_eq!(alethe.len(), add_count);
1025        }
1026
1027        /// DRAT to Alethe conversion should fail in strict mode with deletions
1028        #[test]
1029        fn prop_drat_deletion_strict_mode_fails(
1030            clauses in prop::collection::vec(-100i32..100i32, 1..5)
1031        ) {
1032            let converter = FormatConverter::new().strict_mode(true);
1033            let mut drat = DratProof::new();
1034
1035            drat.add_clause(clauses.clone());
1036            drat.delete_clause(clauses);
1037
1038            let result = converter.drat_to_alethe(&drat);
1039            prop_assert!(result.is_err());
1040        }
1041
1042        /// Alethe to LFSC conversion should always produce non-empty LFSC (due to signature)
1043        #[test]
1044        fn prop_alethe_to_lfsc_nonempty(
1045            num_assumptions in 0usize..10
1046        ) {
1047            let converter = FormatConverter::new();
1048            let mut alethe = AletheProof::new();
1049
1050            for i in 0..num_assumptions {
1051                alethe.assume(format!("p{}", i));
1052            }
1053
1054            let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
1055
1056            // LFSC should never be empty because of the boolean signature
1057            prop_assert!(!lfsc.is_empty());
1058        }
1059
1060        /// Term parsing should be deterministic
1061        #[test]
1062        fn prop_term_parsing_deterministic(
1063            term in "[a-z][a-z0-9]{0,5}"
1064        ) {
1065            let result1 = FormatConverter::term_to_lfsc_term(&term);
1066            let result2 = FormatConverter::term_to_lfsc_term(&term);
1067
1068            prop_assert_eq!(
1069                result1.is_ok(),
1070                result2.is_ok(),
1071                "Parsing determinism violated"
1072            );
1073        }
1074
1075        /// Sort parsing should accept basic sorts
1076        #[test]
1077        fn prop_sort_parsing_basic(
1078            sort in prop::sample::select(vec!["Bool", "Int", "Real"])
1079        ) {
1080            let result = FormatConverter::parse_sort(sort);
1081            prop_assert!(result.is_ok());
1082        }
1083
1084        /// BitVec parsing should handle various widths
1085        #[test]
1086        fn prop_bitvec_parsing(
1087            width in 1u32..256
1088        ) {
1089            let sort_str = format!("(_ BitVec {})", width);
1090            let result = FormatConverter::parse_sort(&sort_str);
1091
1092            prop_assert!(result.is_ok());
1093            if let Ok(LfscSort::BitVec(w)) = result {
1094                prop_assert_eq!(w, width);
1095            }
1096        }
1097
1098        /// Conversion errors should always have non-empty messages
1099        #[test]
1100        fn prop_conversion_errors_nonempty(
1101            reason in "[a-zA-Z ]{1,50}"
1102        ) {
1103            let errors = vec![
1104                ConversionError::InformationLoss { reason: reason.clone() },
1105                ConversionError::InvalidSource { reason: reason.clone() },
1106                ConversionError::ConversionFailed { reason },
1107            ];
1108
1109            for err in errors {
1110                let msg = err.to_string();
1111                prop_assert!(!msg.is_empty());
1112            }
1113        }
1114
1115        /// DRAT clauses with zero literals should be handled correctly
1116        #[test]
1117        fn prop_drat_empty_clause_handling(
1118            prefix_clauses in prop::collection::vec(
1119                prop::collection::vec(-10i32..10i32, 1..3),
1120                0..5
1121            )
1122        ) {
1123            let converter = FormatConverter::new();
1124            let mut drat = DratProof::new();
1125
1126            // Add prefix clauses
1127            for clause in prefix_clauses {
1128                drat.add_clause(clause);
1129            }
1130
1131            // Add empty clause (contradiction)
1132            drat.add_clause(vec![]);
1133
1134            let alethe = converter.drat_to_alethe(&drat).unwrap();
1135
1136            // Should successfully convert
1137            prop_assert!(!alethe.is_empty());
1138        }
1139
1140        /// Alethe to LFSC with multiple resolution steps
1141        #[test]
1142        fn prop_alethe_resolution_chain(
1143            chain_length in 1usize..10
1144        ) {
1145            let converter = FormatConverter::new();
1146            let mut alethe = AletheProof::new();
1147
1148            // Build a chain of resolution steps
1149            let mut indices = Vec::new();
1150            for i in 0..chain_length {
1151                let idx = alethe.assume(format!("p{}", i));
1152                indices.push(idx);
1153            }
1154
1155            // Add resolution step using first two assumptions
1156            if indices.len() >= 2 {
1157                alethe.resolution(
1158                    vec!["q".to_string()],
1159                    vec![indices[0], indices[1]]
1160                );
1161            }
1162
1163            let lfsc = converter.alethe_to_lfsc(&alethe).unwrap();
1164
1165            // Should succeed
1166            prop_assert!(!lfsc.is_empty());
1167        }
1168
1169        /// FormatConverter settings should be preserved
1170        #[test]
1171        fn prop_converter_settings_preserved(
1172            strict in prop::bool::ANY,
1173            comments in prop::bool::ANY
1174        ) {
1175            let converter = FormatConverter::new()
1176                .strict_mode(strict)
1177                .add_comments(comments);
1178
1179            prop_assert_eq!(converter.strict_mode, strict);
1180            prop_assert_eq!(converter.add_comments, comments);
1181        }
1182    }
1183}
oxiz_proof/conversion.rs

oxiz_proof/
conversion.rs
