Module atms 

Assumption-based Truth Maintenance System (de Kleer’s ATMS).

Beliefs are tracked in terms of the assumptions that support them. An environment is a set of assumptions (one bit each, ≤64 assumptions → a u64 bitset). A node’s label is the set of minimal environments under which it holds (no environment in a label is a subset of another — minimality is what makes an ATMS efficient). A nogood is an inconsistent environment; every superset of a nogood is also inconsistent. A node is believed in a context iff the context is consistent and contains one of the node’s supporting environments.

Zero-heap: environments are u64 bitsets; labels live in caller-supplied slices.

Functions

env_subset

Is sub a subset of sup? (every assumption in sub is in sup)

holds_in

Is a node with this label believed in context? The context must be consistent (not a superset of any nogood) AND contain one of the node’s supporting environments.

is_nogood

Is env inconsistent given nogoods? True iff env is a superset of any nogood (a nogood’s assumptions are all present, so the contradiction fires).

label_add

Add env to a label held in label[..n], maintaining minimality: if an existing environment already subsumes env (existing ⊆ env), env is redundant and is dropped; any existing environments that env subsumes (env ⊆ existing) are removed in favour of the more general env. Returns the new label length. Zero-heap (in-place compaction of label).

label_holds

Does some environment in label hold under context? (ignoring consistency — see holds_in). True iff any label environment is a subset of context.

Type Aliases

Environment

A set of assumptions — one bit per assumption (≤64). The empty environment 0 is the “holds unconditionally” (premise) environment.