Crate elenchus_solver

Expand description

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

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

seed a model from confident FACT/NOT facts (and report FACT X + NOT X);
forward-chain RULEs to a fixpoint, deriving facts (a derived value that contradicts an existing one is a CONFLICT);
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).

§Example

use elenchus_solver::{Status, verify_source};

// `A has flying` fires the premise, but `A has wing` was never stated — so
// the engine cannot confirm the rule and reports WARNING (not CONFLICT).
let report = verify_source(
    "demo.vrf",
    "DOMAIN d\nFACT A has flying\nPREMISE w:\n    WHEN A has flying\n    THEN A has wing\n",
)
.unwrap();
assert_eq!(report.status, Status::Warning); // `A has wing` is UNKNOWN
println!("{report}"); // the full human report, ready to show a model

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).
CoreItem: One construct named in an Report::unsat_core.
Derived: A fact produced by a RULE during forward chaining.
Diagnostics: Re-exported so library users handling a CompileError::Parse can render the syntax diagnostics with their own error limit (e.g. CLI --max-errors). Every syntax error from one parse, plus the source label for the header.
FileResolver: The filesystem-backed resolver (reads IMPORTs from disk). Only with std. A filesystem-backed resolver. Mirrors vsm-grammar’s FileResolver: relative imports resolve against the importing file’s directory, with manual .. normalization (no canonicalization, to keep a virtual layout).
MemoryResolver: An in-memory resolver: serves sources from a name → content map. Pure no_std. Mirrors vsm-grammar’s MemoryResolver.
OrphanFact: An advisory lint: a FACT/NOT/ASSUME whose atom appears in no PREMISE or RULE. Such an assertion is logically inert — nothing checks it and nothing is derived from it, so it can never produce a CONFLICT, WARNING or DERIVED. It is almost always a typo’d atom name or a leftover line. Purely informational — it never changes the verdict, the warning pool, or the exit code (a program full of orphans is still perfectly CONSISTENT).
PlaceholderInfo: A reporting record for one declared VAR port: its key, how it resolved, the value it took (if any), and where that value came from.
PortBinding: One external value bound to a port key, supplied from outside the program (CLI / API / a data file). The origin is a short human tag used both in the placeholders report and in a [CompileError::PortConflict] message.
Report: The result of solving, self-contained (atom ids already resolved to labels).
SimilarAtoms: An advisory hint that two atom names look like the same atom typed two different ways (e.g. is_rolled_back vs is rolled_back). Purely a suggestion — it never changes the verdict, the warning pool, or the exit code. It exists to catch the silent-typo trap where a misspelling creates a new UNKNOWN atom that quietly never links to the rest of the program.
TraceStep: One link in a Conflict’s derivation chain: an atom, the value it was forced to, and why it holds that value.
UnusedImport: An advisory record: a file IMPORTs a domain it never references. Such an import is inert — no domain.atom in that file mentions it, so removing it would not change the result. It is almost always a leftover or a forgotten domain. prefix. Purely informational — it never changes the verdict.
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).
PlaceholderStatus: How a declared VAR port got (or did not get) its value — the per-port status shown in the report’s PLACEHOLDERS section. Advisory only; never affects the verdict.
Status: Overall verdict for the system.
TraceReason: Why a TraceStep atom holds its value.
V3: Three-valued truth (Kleene). UNKNOWN is a first-class value, not hidden FALSE.

Constants§

VERSION: The engine version (this crate’s package version). Exposed so a wrapper — e.g. the wasm/npm build, which carries its own, independent package version — can report the engine version (and compare it to a skill’s  marker) rather than its own.

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).
compile_source_with: Like compile_source, but resolving declared VAR ports against external inputs ((name, binding) pairs from CLI / API / data). The Compiled carries a placeholders record per declared port.
compile_with: Like compile, but resolving declared VAR ports against external inputs. Ports declared in any file of the import graph are aggregated, then resolved once after every file is added.
normalize_import_path: Normalize an IMPORT path identically on every OS and every surface: treat both / and \ as separators, resolve relative against base’s directory, collapse . / .., and re-join with /. Pure and no_std, so it does not depend on the host (or the compile target’s) path semantics — a Windows-style and a Unix-style import resolve to the same virtual path whether the resolver is filesystem-, JS-callback-, or in-memory-backed. The single source of truth all three Resolvers share.
read_data_bindings: Parse a data-only .vrf source into ready-to-merge port PortBindings, each tagged with origin data:<file>. The shared bridge every surface uses to turn a --data / data-map source into engine inputs, so a data file behaves identically whether it arrives from the CLI, wasm, or MCP.
read_data_source: Parse a data-only .vrf source and extract its PROVIDE bindings as (name, value) pairs. A data file carries only values: any statement other than PROVIDE (or a DOMAIN) is a CompileError::DataFileStatement. Used to load a --data <file> of port values without compiling it as a program.
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.
verify_source_with: Like verify_source, but resolving declared VAR ports against external inputs ((name, binding) pairs from CLI / API / data).
verify_with: Like verify, but resolving declared VAR ports against external inputs.