Crate elenchus_solver 

elenchus-solver — the reasoning interpreter (forward pass).

Consumes the Compiled IR from elenchus-compiler and evaluates it under three-valued Kleene logic (TRUE / FALSE / UNKNOWN, where UNKNOWN ≠ FALSE):

1. seed a model from confident FACT/NOT facts (and report FACT X + NOT X);
2. forward-chain RULEs to a fixpoint, deriving facts (a derived value that contradicts an existing one is a CONFLICT);
3. evaluate every Impossible clause (the desugared PREMISEs):
   • all literals forced TRUE → CONFLICT (the constraint is violated);
   • some literal FALSE → satisfied → CONSISTENT;
   • otherwise (no FALSE, an UNKNOWN remains): for implication premises this is a WARNING (blocked by missing data), for list premises (EXCLUSIVE/FORBIDS/ ONEOF/ATLEAST) it is CONSISTENT (UNKNOWN means “no conflict yet”).

On CHECK ... BIDIRECTIONAL a backward pass also runs: the premises, rules and confident facts are encoded as CNF and handed to a small in-crate CDCL SAT core (sat, replicating varisat’s algorithm) to count models — 0 means the system is jointly unsatisfiable (a CONFLICT the forward pass may miss), ≥2 means an alternative model exists (UNDERDETERMINED).

Modules

sat

A compact, single-threaded CDCL SAT solver in no_std, replicating the core algorithm of varisat (jix/varisat) in a readable, lazy style.

Structs

Conflict

A violated constraint (or a fact-level contradiction).

Derived

A fact produced by a RULE during forward chaining.

MemoryResolver

An in-memory resolver: serves sources from a name → content map. Pure no_std. Mirrors vsm-grammar’s MemoryResolver.

Report

The result of solving, self-contained (atom ids already resolved to labels).

Warning

A constraint that could not be checked because a needed atom is UNKNOWN.

Enums

CompileError

Anything that can go wrong while compiling (and resolving imports).

Status

Overall verdict for the system.

V3

Three-valued truth (Kleene). UNKNOWN is a first-class value, not hidden FALSE.

Traits

Resolver

Resolves IMPORT "path" to source text. The engine is source-agnostic: it consumes strings, so a file is merely one backing store. Mirrors vsm-grammar’s SourceResolver.

Functions

compile

Compile a root source and all its transitive IMPORTs into one IR.

compile_source

Convenience: compile a single source into the IR. IMPORTs are recorded as pending, not resolved (use compile with a Resolver to resolve them).

solve

Evaluate a compiled program: the three-valued forward pass, then the backward pass on BIDIRECTIONAL.

verify

Parse → compile (resolving imports) → solve, given a Resolver.

verify_source

Parse → compile → solve a single source.