oxiz_proof/
theory_combination.rs

1//! Proof certificates for theory combination.
2
3use crate::proof::ProofNodeId;
4use oxiz_core::TermId;
5
6/// Theory identifier used in theory-combination certificates.
7#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
8pub struct TheoryId(pub u32);
9
10/// One Nelson-Oppen combination step.
11#[derive(Debug, Clone, PartialEq, Eq)]
12pub struct CombinationStep {
13    /// Theory that propagated these equalities.
14    pub theory: TheoryId,
15    /// Interface equalities propagated at this step.
16    pub propagated_equalities: Vec<(TermId, TermId)>,
17    /// Proof nodes justifying the propagation.
18    pub justification: Vec<ProofNodeId>,
19}
20
21/// Structured certificate for a Nelson-Oppen theory-combination trace.
22#[derive(Debug, Clone, PartialEq, Eq)]
23pub struct NelsonOppenCertificate {
24    /// Ordered combination steps.
25    pub steps: Vec<CombinationStep>,
26    /// Theory that concludes the combined derivation.
27    pub concluding_theory: TheoryId,
28    /// Final contradiction node, when available.
29    pub contradiction: ProofNodeId,
30}
31
32impl NelsonOppenCertificate {
33    /// Create an empty certificate.
34    #[must_use]
35    pub fn new(concluding_theory: TheoryId, contradiction: ProofNodeId) -> Self {
36        Self {
37            steps: Vec::new(),
38            concluding_theory,
39            contradiction,
40        }
41    }
42
43    /// Append a combination step.
44    pub fn add_step(&mut self, step: CombinationStep) {
45        self.steps.push(step);
46    }
47
48    /// Verify basic certificate shape.
49    #[must_use]
50    pub fn verify(&self) -> bool {
51        let Some(last) = self.steps.last() else {
52            return false;
53        };
54
55        last.theory == self.concluding_theory
56            && (!last.propagated_equalities.is_empty() || !last.justification.is_empty())
57    }
58}
oxiz_proof/theory_combination.rs

oxiz_proof/
theory_combination.rs
