oxiz_theories/checking/
array.rs

1//! Array Theory Checker
2//!
3//! Validates array theory inferences (select/store axioms).
4
5use super::{CheckResult, CheckerStats, Literal, TheoryChecker};
6use oxiz_core::ast::TermId;
7use std::time::Instant;
8
9/// Array theory checker
10#[derive(Debug)]
11pub struct ArrayChecker {
12    stats: CheckerStats,
13    /// Whether to check extensionality axiom
14    check_extensionality: bool,
15}
16
17impl ArrayChecker {
18    /// Create a new array checker
19    pub fn new() -> Self {
20        Self {
21            stats: CheckerStats::default(),
22            check_extensionality: true,
23        }
24    }
25
26    /// Create with extensionality checking disabled
27    pub fn without_extensionality() -> Self {
28        Self {
29            stats: CheckerStats::default(),
30            check_extensionality: false,
31        }
32    }
33
34    /// Check array conflict validity
35    /// Array conflicts typically involve:
36    /// - Read-over-write: select(store(a, i, v), i) = v
37    /// - Read-over-write-miss: i != j => select(store(a, i, v), j) = select(a, j)
38    /// - Extensionality: (forall i. select(a, i) = select(b, i)) => a = b
39    fn check_array_conflict(&self, clause: &[Literal]) -> CheckResult {
40        if clause.is_empty() {
41            return CheckResult::Invalid("Empty conflict clause".to_string());
42        }
43
44        // For array theory, conflicts arise from:
45        // 1. Contradictory read/write combinations
46        // 2. Equality propagation conflicts
47
48        // Simplified: assume valid for now
49        // Real implementation would check select/store axioms
50        CheckResult::Valid
51    }
52
53    /// Check array propagation
54    fn check_array_propagation(&self, _literal: Literal, _explanation: &[Literal]) -> CheckResult {
55        // Array propagations include:
56        // - i = j => select(a, i) = select(a, j)
57        // - store(a, i, v) = store(b, j, w) => i = j AND v = w (for equal arrays)
58        CheckResult::Valid
59    }
60
61    /// Check model for array consistency
62    fn check_array_model(&self, _assignments: &[(TermId, bool)]) -> CheckResult {
63        // Verify array assignments satisfy select/store semantics
64        CheckResult::Valid
65    }
66
67    /// Enable/disable extensionality checking
68    pub fn set_extensionality(&mut self, enabled: bool) {
69        self.check_extensionality = enabled;
70    }
71}
72
73impl Default for ArrayChecker {
74    fn default() -> Self {
75        Self::new()
76    }
77}
78
79impl TheoryChecker for ArrayChecker {
80    fn name(&self) -> &'static str {
81        "array"
82    }
83
84    fn check_conflict(&self, clause: &[Literal]) -> CheckResult {
85        let start = Instant::now();
86        let result = self.check_array_conflict(clause);
87        let _elapsed = start.elapsed();
88        result
89    }
90
91    fn check_propagation(&self, literal: Literal, explanation: &[Literal]) -> CheckResult {
92        let start = Instant::now();
93        let result = self.check_array_propagation(literal, explanation);
94        let _elapsed = start.elapsed();
95        result
96    }
97
98    fn check_model(&self, assignments: &[(TermId, bool)]) -> CheckResult {
99        self.check_array_model(assignments)
100    }
101
102    fn stats(&self) -> CheckerStats {
103        self.stats.clone()
104    }
105
106    fn reset_stats(&mut self) {
107        self.stats = CheckerStats::default();
108    }
109}
110
111#[cfg(test)]
112mod tests {
113    use super::*;
114
115    #[test]
116    fn test_array_checker_creation() {
117        let checker = ArrayChecker::new();
118        assert_eq!(checker.name(), "array");
119        assert!(checker.check_extensionality);
120    }
121
122    #[test]
123    fn test_array_without_extensionality() {
124        let checker = ArrayChecker::without_extensionality();
125        assert!(!checker.check_extensionality);
126    }
127
128    #[test]
129    fn test_array_conflict_empty() {
130        let checker = ArrayChecker::new();
131        let result = checker.check_conflict(&[]);
132        assert!(result.is_invalid());
133    }
134
135    #[test]
136    fn test_array_conflict_valid() {
137        let checker = ArrayChecker::new();
138        let t1 = TermId::from(1u32);
139        let clause = vec![Literal::pos(t1)];
140        let result = checker.check_conflict(&clause);
141        assert!(result.is_valid());
142    }
143
144    #[test]
145    fn test_array_propagation() {
146        let checker = ArrayChecker::new();
147        let t1 = TermId::from(1u32);
148        let t2 = TermId::from(2u32);
149
150        let literal = Literal::pos(t1);
151        let explanation = vec![Literal::pos(t2)];
152        let result = checker.check_propagation(literal, &explanation);
153        assert!(result.is_valid());
154    }
155
156    #[test]
157    fn test_array_model_check() {
158        let checker = ArrayChecker::new();
159        let t1 = TermId::from(1u32);
160        let assignments = vec![(t1, true)];
161        let result = checker.check_model(&assignments);
162        assert!(result.is_valid());
163    }
164
165    #[test]
166    fn test_set_extensionality() {
167        let mut checker = ArrayChecker::new();
168        assert!(checker.check_extensionality);
169
170        checker.set_extensionality(false);
171        assert!(!checker.check_extensionality);
172
173        checker.set_extensionality(true);
174        assert!(checker.check_extensionality);
175    }
176
177    #[test]
178    fn test_array_stats() {
179        let mut checker = ArrayChecker::new();
180        let stats = checker.stats();
181        assert_eq!(stats.conflict_checks, 0);
182
183        checker.reset_stats();
184        let stats = checker.stats();
185        assert_eq!(stats.propagation_checks, 0);
186    }
187}
oxiz_theories/checking/array.rs

oxiz_theories/checking/
array.rs
