# 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](https://github.com/m62624/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 `RULE`s 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](https://github.com/jix/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
```rust
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}");
```
```text
RESULT: WARNING
WARNING w (PREMISE) [demo.vrf:2]
blocked by: A has wing
SUMMARY: 0 conflicts, 1 warnings, 0 derived
```
## License
MIT — see [LICENSE](LICENSE).