elenchus-solver

⚠️ Experimental. elenchus is mostly an AI-built experiment — written with the help of a small local model (Qwen3.6-35B-A3B-UD-Q4_K_XL.gguf) and various Claude models, in roughly equal measure. Expect non-professional design choices, rough edges, broken behavior, or mistakes. Use it at your own risk.

The inference interpreter for elenchus — the forward pass.

no_std (needs alloc). Consumes the [elenchus-compiler] Compiled IR and evaluates it under three-valued Kleene logic (TRUE / FALSE / UNKNOWN, where UNKNOWN ≠ FALSE).

What it does

1. Seeds a model from confident FACT/NOT facts; FACT X + NOT X is a CONFLICT.
2. Forward-chains RULEs to a fixpoint, deriving facts (a derived value that contradicts a known one is a CONFLICT).
3. Evaluates every Impossible clause (the desugared premises):
   • all literals forced TRUE → CONFLICT (constraint violated);
   • some literal FALSE → satisfied → CONSISTENT;
   • otherwise an UNKNOWN blocks the check → WARNING for implication premises (missing data), CONSISTENT for list premises (EXCLUSIVE/FORBIDS/ONEOF/ ATLEAST — UNKNOWN means "no conflict yet").

On CHECK ... BIDIRECTIONAL a backward pass runs too: the premises, rules and confident facts are encoded as CNF and solved by a small in-crate CDCL SAT core (sat, a no_std replication of varisat's algorithm — trail + decision levels, two-watched-literal propagation, 1-UIP clause learning, non-chronological backjumping, VSIDS). It counts models: 0 → jointly unsatisfiable (a CONFLICT the forward pass may miss), ≥2 → an alternative model exists (UNDERDETERMINED). varisat's infra (proof logging, GC, restarts, multithreading) is intentionally omitted.

Usage

use elenchus_solver::{verify_source, Status};

let report = verify_source(
    "demo.vrf",
    "FACT 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}");

RESULT: WARNING
  WARNING   w (PREMISE)  [demo.vrf:2]
      blocked by: A has wing
SUMMARY: 0 conflicts, 1 warnings, 0 derived

License

MIT — see LICENSE.