1use super::working_memory::FactHandle;
24use std::collections::{HashMap, HashSet};
25use std::time::Instant;
26
27#[derive(Debug, Clone, PartialEq, Eq)]
29pub enum JustificationType {
30 Explicit,
32 Logical,
34}
35
36#[derive(Debug, Clone)]
41pub struct Justification {
42 pub fact_handle: FactHandle,
44
45 pub justification_type: JustificationType,
47
48 pub source_rule: Option<String>,
50
51 pub premise_facts: Vec<FactHandle>,
54
55 pub created_at: Instant,
57
58 pub id: u64,
60}
61
62impl Justification {
63 pub fn explicit(fact_handle: FactHandle, id: u64) -> Self {
65 Self {
66 fact_handle,
67 justification_type: JustificationType::Explicit,
68 source_rule: None,
69 premise_facts: Vec::new(),
70 created_at: Instant::now(),
71 id,
72 }
73 }
74
75 pub fn logical(
77 fact_handle: FactHandle,
78 source_rule: String,
79 premise_facts: Vec<FactHandle>,
80 id: u64,
81 ) -> Self {
82 Self {
83 fact_handle,
84 justification_type: JustificationType::Logical,
85 source_rule: Some(source_rule),
86 premise_facts,
87 created_at: Instant::now(),
88 id,
89 }
90 }
91
92 pub fn is_valid(&self, retracted_facts: &HashSet<FactHandle>) -> bool {
95 if self.justification_type == JustificationType::Explicit {
97 return true;
98 }
99
100 !self
102 .premise_facts
103 .iter()
104 .any(|h| retracted_facts.contains(h))
105 }
106}
107
108pub struct TruthMaintenanceSystem {
113 justifications: HashMap<u64, Justification>,
115
116 fact_justifications: HashMap<FactHandle, Vec<u64>>,
118
119 fact_dependents: HashMap<FactHandle, Vec<u64>>,
121
122 logical_facts: HashSet<FactHandle>,
124
125 explicit_facts: HashSet<FactHandle>,
127
128 retracted_facts: HashSet<FactHandle>,
130
131 next_justification_id: u64,
133}
134
135impl TruthMaintenanceSystem {
136 pub fn new() -> Self {
138 Self {
139 justifications: HashMap::new(),
140 fact_justifications: HashMap::new(),
141 fact_dependents: HashMap::new(),
142 logical_facts: HashSet::new(),
143 explicit_facts: HashSet::new(),
144 retracted_facts: HashSet::new(),
145 next_justification_id: 1,
146 }
147 }
148
149 pub fn add_explicit_justification(&mut self, fact_handle: FactHandle) {
151 let id = self.next_justification_id;
152 self.next_justification_id += 1;
153
154 let justification = Justification::explicit(fact_handle, id);
155
156 self.justifications.insert(id, justification);
157 self.fact_justifications
158 .entry(fact_handle)
159 .or_default()
160 .push(id);
161
162 self.explicit_facts.insert(fact_handle);
163 }
164
165 pub fn add_logical_justification(
172 &mut self,
173 fact_handle: FactHandle,
174 source_rule: String,
175 premise_facts: Vec<FactHandle>,
176 ) {
177 let id = self.next_justification_id;
178 self.next_justification_id += 1;
179
180 let justification =
181 Justification::logical(fact_handle, source_rule, premise_facts.clone(), id);
182
183 self.justifications.insert(id, justification);
185
186 self.fact_justifications
188 .entry(fact_handle)
189 .or_default()
190 .push(id);
191
192 for premise in premise_facts {
194 self.fact_dependents.entry(premise).or_default().push(id);
195 }
196
197 self.logical_facts.insert(fact_handle);
198 }
199
200 pub fn is_logical(&self, fact_handle: FactHandle) -> bool {
202 self.logical_facts.contains(&fact_handle)
203 }
204
205 pub fn is_explicit(&self, fact_handle: FactHandle) -> bool {
207 self.explicit_facts.contains(&fact_handle)
208 }
209
210 pub fn get_justifications(&self, fact_handle: FactHandle) -> Vec<&Justification> {
212 if let Some(just_ids) = self.fact_justifications.get(&fact_handle) {
213 just_ids
214 .iter()
215 .filter_map(|id| self.justifications.get(id))
216 .collect()
217 } else {
218 Vec::new()
219 }
220 }
221
222 pub fn has_valid_justification(&self, fact_handle: FactHandle) -> bool {
224 if let Some(just_ids) = self.fact_justifications.get(&fact_handle) {
225 just_ids
226 .iter()
227 .filter_map(|id| self.justifications.get(id))
228 .any(|j| j.is_valid(&self.retracted_facts))
229 } else {
230 false
231 }
232 }
233
234 pub fn retract_with_cascade(&mut self, fact_handle: FactHandle) -> Vec<FactHandle> {
238 let mut to_retract = Vec::new();
239
240 self.retracted_facts.insert(fact_handle);
242 self.logical_facts.remove(&fact_handle);
243 self.explicit_facts.remove(&fact_handle);
244
245 if let Some(dependent_just_ids) = self.fact_dependents.get(&fact_handle) {
247 for just_id in dependent_just_ids.clone() {
248 if let Some(justification) = self.justifications.get(&just_id) {
249 let dependent_fact = justification.fact_handle;
250
251 if !self.has_valid_justification(dependent_fact) {
253 if !self.retracted_facts.contains(&dependent_fact) {
255 to_retract.push(dependent_fact);
256
257 let cascaded = self.retract_with_cascade(dependent_fact);
259 to_retract.extend(cascaded);
260 }
261 }
262 }
263 }
264 }
265
266 to_retract
267 }
268
269 pub fn remove_justifications(&mut self, fact_handle: FactHandle) {
271 if let Some(just_ids) = self.fact_justifications.remove(&fact_handle) {
272 for id in just_ids {
273 self.justifications.remove(&id);
274 }
275 }
276 }
277
278 pub fn stats(&self) -> TmsStats {
280 TmsStats {
281 total_justifications: self.justifications.len(),
282 logical_facts: self.logical_facts.len(),
283 explicit_facts: self.explicit_facts.len(),
284 retracted_facts: self.retracted_facts.len(),
285 }
286 }
287
288 pub fn clear(&mut self) {
290 self.justifications.clear();
291 self.fact_justifications.clear();
292 self.fact_dependents.clear();
293 self.logical_facts.clear();
294 self.explicit_facts.clear();
295 self.retracted_facts.clear();
296 self.next_justification_id = 1;
297 }
298
299 pub fn get_logical_facts(&self) -> &HashSet<FactHandle> {
301 &self.logical_facts
302 }
303
304 pub fn get_explicit_facts(&self) -> &HashSet<FactHandle> {
306 &self.explicit_facts
307 }
308}
309
310impl Default for TruthMaintenanceSystem {
311 fn default() -> Self {
312 Self::new()
313 }
314}
315
316#[derive(Debug, Clone)]
318pub struct TmsStats {
319 pub total_justifications: usize,
320 pub logical_facts: usize,
321 pub explicit_facts: usize,
322 pub retracted_facts: usize,
323}
324
325impl std::fmt::Display for TmsStats {
326 fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
327 write!(
328 f,
329 "TMS Stats: {} justifications, {} logical facts, {} explicit facts, {} retracted",
330 self.total_justifications,
331 self.logical_facts,
332 self.explicit_facts,
333 self.retracted_facts
334 )
335 }
336}
337
338#[cfg(test)]
339mod tests {
340 use super::*;
341
342 #[test]
343 fn test_explicit_justification() {
344 let mut tms = TruthMaintenanceSystem::new();
345 let fact = FactHandle::new(1);
346
347 tms.add_explicit_justification(fact);
348
349 assert!(tms.is_explicit(fact));
350 assert!(!tms.is_logical(fact));
351 assert!(tms.has_valid_justification(fact));
352 }
353
354 #[test]
355 fn test_logical_justification() {
356 let mut tms = TruthMaintenanceSystem::new();
357 let premise = FactHandle::new(1);
358 let derived = FactHandle::new(2);
359
360 tms.add_explicit_justification(premise);
361 tms.add_logical_justification(derived, "TestRule".to_string(), vec![premise]);
362
363 assert!(tms.is_logical(derived));
364 assert!(!tms.is_explicit(derived));
365 assert!(tms.has_valid_justification(derived));
366 }
367
368 #[test]
369 fn test_cascade_retraction() {
370 let mut tms = TruthMaintenanceSystem::new();
371
372 let fact_a = FactHandle::new(1);
374 let fact_b = FactHandle::new(2);
375 let fact_c = FactHandle::new(3);
376
377 tms.add_explicit_justification(fact_a);
378 tms.add_logical_justification(fact_b, "Rule1".to_string(), vec![fact_a]);
379 tms.add_logical_justification(fact_c, "Rule2".to_string(), vec![fact_b]);
380
381 let cascaded = tms.retract_with_cascade(fact_a);
383
384 assert!(cascaded.contains(&fact_b));
385 assert!(cascaded.contains(&fact_c));
386 assert!(!tms.has_valid_justification(fact_b));
387 assert!(!tms.has_valid_justification(fact_c));
388 }
389
390 #[test]
391 fn test_multiple_justifications() {
392 let mut tms = TruthMaintenanceSystem::new();
393
394 let premise1 = FactHandle::new(1);
395 let premise2 = FactHandle::new(2);
396 let derived = FactHandle::new(3);
397
398 tms.add_explicit_justification(premise1);
399 tms.add_explicit_justification(premise2);
400
401 tms.add_logical_justification(derived, "Rule1".to_string(), vec![premise1]);
403 tms.add_logical_justification(derived, "Rule2".to_string(), vec![premise2]);
404
405 let cascaded = tms.retract_with_cascade(premise1);
407
408 assert!(tms.has_valid_justification(derived));
410 assert!(cascaded.is_empty());
411
412 let cascaded = tms.retract_with_cascade(premise2);
414
415 assert!(!tms.has_valid_justification(derived));
417 assert!(cascaded.contains(&derived));
418 }
419}