qualia_core_db/modalities/abductive/
atms.rs

1//! Assumption-based Truth Maintenance System (de Kleer's ATMS).
2//!
3//! Beliefs are tracked in terms of the **assumptions** that support them. An *environment* is a
4//! set of assumptions (one bit each, ≤64 assumptions → a `u64` bitset). A node's *label* is the
5//! set of **minimal** environments under which it holds (no environment in a label is a subset of
6//! another — minimality is what makes an ATMS efficient). A *nogood* is an inconsistent
7//! environment; every superset of a nogood is also inconsistent. A node is believed in a context
8//! iff the context is consistent and contains one of the node's supporting environments.
9//!
10//! Zero-heap: environments are `u64` bitsets; labels live in caller-supplied slices.
11
12/// A set of assumptions — one bit per assumption (≤64). The empty environment `0` is the
13/// "holds unconditionally" (premise) environment.
14pub type Environment = u64;
15
16/// Is `sub` a subset of `sup`? (every assumption in `sub` is in `sup`)
17#[inline]
18pub fn env_subset(sub: Environment, sup: Environment) -> bool {
19    sub & sup == sub
20}
21
22/// Is `env` inconsistent given `nogoods`? True iff `env` is a superset of any nogood (a nogood's
23/// assumptions are all present, so the contradiction fires).
24#[inline]
25pub fn is_nogood(env: Environment, nogoods: &[Environment]) -> bool {
26    nogoods.iter().any(|&ng| env_subset(ng, env))
27}
28
29/// Add `env` to a label held in `label[..n]`, **maintaining minimality**: if an existing
30/// environment already subsumes `env` (existing ⊆ env), `env` is redundant and is dropped; any
31/// existing environments that `env` subsumes (env ⊆ existing) are removed in favour of the more
32/// general `env`. Returns the new label length. Zero-heap (in-place compaction of `label`).
33pub fn label_add(label: &mut [Environment], n: usize, env: Environment) -> usize {
34    // Redundant if a more-general (smaller) environment is already present.
35    for &e in label.iter().take(n) {
36        if env_subset(e, env) {
37            return n;
38        }
39    }
40    // Drop existing environments that `env` is more general than, compacting in place.
41    let mut w = 0usize;
42    for i in 0..n {
43        if !env_subset(env, label[i]) {
44            label[w] = label[i];
45            w += 1;
46        }
47    }
48    if w < label.len() {
49        label[w] = env;
50        w += 1;
51    }
52    w
53}
54
55/// Does some environment in `label` hold under `context`? (ignoring consistency — see
56/// [`holds_in`]). True iff any label environment is a subset of `context`.
57#[inline]
58pub fn label_holds(label: &[Environment], context: Environment) -> bool {
59    label.iter().any(|&e| env_subset(e, context))
60}
61
62/// Is a node with this `label` **believed** in `context`? The context must be consistent (not a
63/// superset of any nogood) AND contain one of the node's supporting environments.
64pub fn holds_in(label: &[Environment], context: Environment, nogoods: &[Environment]) -> bool {
65    !is_nogood(context, nogoods) && label_holds(label, context)
66}
67
68#[cfg(test)]
69mod tests {
70    use super::*;
71
72    // Assumption bits.
73    const A: Environment = 1 << 0;
74    const B: Environment = 1 << 1;
75    const C: Environment = 1 << 2;
76
77    #[test]
78    fn label_maintains_minimal_environments() {
79        let mut label = [0u64; 8];
80        let mut n = 0;
81        n = label_add(&mut label, n, A | B); // {A,B}
82        assert_eq!(n, 1);
83        // Adding the more-general {A} removes {A,B}.
84        n = label_add(&mut label, n, A);
85        assert_eq!(n, 1);
86        assert_eq!(label[0], A, "{{A}} subsumes {{A,B}}");
87        // Adding the more-specific {A,C} is redundant (A already supports) → dropped.
88        n = label_add(&mut label, n, A | C);
89        assert_eq!(n, 1);
90        assert_eq!(label[0], A);
91        // An independent environment {B} coexists.
92        n = label_add(&mut label, n, B);
93        assert_eq!(n, 2);
94        assert!(label[..n].contains(&A) && label[..n].contains(&B));
95    }
96
97    #[test]
98    fn nogoods_are_superset_closed() {
99        let nogoods = [A | B]; // {A,B} is contradictory
100        assert!(is_nogood(A | B, &nogoods));
101        assert!(
102            is_nogood(A | B | C, &nogoods),
103            "any superset of a nogood is a nogood"
104        );
105        assert!(!is_nogood(A | C, &nogoods));
106        assert!(!is_nogood(A, &nogoods));
107    }
108
109    #[test]
110    fn belief_requires_a_consistent_supporting_context() {
111        // Node supported by {A} or {B}.
112        let mut label = [0u64; 4];
113        let mut n = 0;
114        n = label_add(&mut label, n, A);
115        n = label_add(&mut label, n, B);
116        let nogoods = [A | C]; // assuming A and C together is contradictory
117
118        // Context {A}: consistent, contains supporting env {A} → believed.
119        assert!(holds_in(&label[..n], A, &nogoods));
120        // Context {A,C}: contains support {A} but is a nogood → NOT believed (contradiction).
121        assert!(!holds_in(&label[..n], A | C, &nogoods));
122        // Context {B,C}: consistent, contains support {B} → believed.
123        assert!(holds_in(&label[..n], B | C, &nogoods));
124        // Context {C}: consistent but contains no supporting environment → not believed.
125        assert!(!holds_in(&label[..n], C, &nogoods));
126    }
127}
qualia_core_db/modalities/abductive/atms.rs

qualia_core_db/modalities/abductive/
atms.rs
