elenchus_solver/report/mod.rs
1//! The report data model: status, conflicts, warnings, derived facts, and the
2//! advisory pools, plus the shared atom-label helper.
3use alloc::string::String;
4use alloc::vec::Vec;
5use elenchus_compiler::{AtomId, Compiled, Origin, PlaceholderInfo, UnusedImport, Value};
6
7/// Overall verdict for the system.
8#[derive(Debug, Clone, Copy, PartialEq, Eq)]
9pub enum Status {
10 /// No contradictions, and (when checked) the model is pinned down.
11 Consistent,
12 /// The constraints are satisfiable but do not pin a unique assignment — an
13 /// alternative model exists (found by the backward pass on `BIDIRECTIONAL`).
14 Underdetermined,
15 /// A premise could not be checked because a needed atom is UNKNOWN.
16 Warning,
17 /// A premise is violated, or the premises + facts are jointly unsatisfiable.
18 Conflict,
19}
20
21/// A violated constraint (or a fact-level contradiction).
22#[derive(Debug, Clone, PartialEq, Eq)]
23pub struct Conflict {
24 /// Provenance of the violated constraint (source, line, premise name, kind).
25 pub origin: Origin,
26 /// Human labels of the atoms participating in the contradiction.
27 pub atoms: Vec<String>,
28 /// The derivation chain that forced the participating atoms to the values
29 /// which made the constraint fire — supporting facts first, then each rule
30 /// built on them, ending at the conflict. This is the answer to "CONFLICT,
31 /// but *why*?". Empty for a direct `FACT X` + `NOT X` contradiction and for
32 /// the `<system>` joint-unsatisfiability conflict (neither has a chain).
33 pub trace: Vec<TraceStep>,
34}
35
36/// One link in a [`Conflict`]'s derivation chain: an atom, the value it was
37/// forced to, and why it holds that value.
38#[derive(Debug, Clone, PartialEq, Eq)]
39pub struct TraceStep {
40 /// Human label of the atom (`subject predicate [object]`).
41 pub atom: String,
42 /// The confident value the atom was forced to (TRUE or FALSE).
43 pub value: Value,
44 /// Why the atom holds that value.
45 pub reason: TraceReason,
46}
47
48/// Why a [`TraceStep`] atom holds its value.
49#[derive(Debug, Clone, PartialEq, Eq)]
50pub enum TraceReason {
51 /// Asserted directly by a `FACT` / `NOT`.
52 Asserted(Origin),
53 /// Derived by a `RULE` whose antecedent atoms all held.
54 Derived {
55 /// Provenance of the firing rule.
56 origin: Origin,
57 /// Human labels of the antecedent atoms that supported the derivation.
58 from: Vec<String>,
59 },
60}
61
62/// A constraint that could not be checked because a needed atom is UNKNOWN.
63#[derive(Debug, Clone, PartialEq, Eq)]
64pub struct Warning {
65 /// Provenance of the constraint that could not be checked.
66 pub origin: Origin,
67 /// Human labels of the UNKNOWN atoms blocking the check.
68 pub blocked_by: Vec<String>,
69 /// A directed fix for the most informative blocking atom, distinguishing the
70 /// two reasons a check stays blocked: the atom is a *free input* nothing can
71 /// determine (→ add a `FACT`/`NOT`, or make a `PREMISE` a `RULE` so it derives
72 /// the value), versus the atom *is* derivable by a `RULE` that has not fired
73 /// (→ assert that rule's antecedent). Advisory text; never changes the verdict.
74 pub hint: Option<String>,
75}
76
77/// A fact produced by a `RULE` during forward chaining.
78#[derive(Debug, Clone, PartialEq, Eq)]
79pub struct Derived {
80 /// Human label of the atom whose value was derived.
81 pub atom: String,
82 /// The value the rule assigned (TRUE, or FALSE for a `THEN NOT …`).
83 pub value: Value,
84 /// Provenance of the `RULE` that produced it.
85 pub origin: Origin,
86}
87
88/// The result of solving, self-contained (atom ids already resolved to labels).
89#[derive(Debug, Clone, PartialEq, Eq)]
90pub struct Report {
91 /// The overall verdict.
92 pub status: Status,
93 /// Every violated constraint / fact contradiction (sorted by source+line).
94 pub conflicts: Vec<Conflict>,
95 /// Every premise blocked by an UNKNOWN atom (sorted by source+line).
96 pub warnings: Vec<Warning>,
97 /// Facts produced by forward-chaining `RULE`s.
98 pub derived: Vec<Derived>,
99 /// When `UNDERDETERMINED`, the label of an atom left free by the constraints
100 /// (asserting it would pin the model down).
101 pub underdetermined: Option<String>,
102 /// When the system is jointly unsatisfiable but the forward pass found no
103 /// single violated constraint, the minimal set of constructs (facts /
104 /// premises / rules) whose removal restores satisfiability — i.e. the
105 /// smallest group jointly to blame. Empty in every other case.
106 pub unsat_core: Vec<CoreItem>,
107 /// When `ASSUME` hypotheses are what break an otherwise-consistent program,
108 /// the minimal set of assumptions that cannot all hold *together with the
109 /// (consistent) facts, premises and rules* — dropping any one restores
110 /// consistency. Only ever lists `ASSUME` constructs: facts and premises are
111 /// never blamed. Empty whenever the facts/premises are themselves to blame
112 /// (a hard contradiction) or there is no conflict at all. The verdict stays
113 /// `CONFLICT` (exit code 2); this field only says *which dial to turn*.
114 pub retract: Vec<CoreItem>,
115 /// Advisory near-duplicate atom-name hints (possible typos). Never affects
116 /// [`Report::status`] or [`Report::exit_code`] — purely informational.
117 pub hints: Vec<SimilarAtoms>,
118 /// Advisory "orphan fact" lints: a `FACT`/`NOT`/`ASSUME` whose atom is never
119 /// referenced by any `PREMISE` or `RULE`, so it can neither be checked nor
120 /// derive anything — it has no effect on the verdict. Never affects
121 /// [`Report::status`] or [`Report::exit_code`] — purely informational.
122 pub orphans: Vec<OrphanFact>,
123 /// Advisory "unused import" lints: a file `IMPORT`s a domain it never
124 /// references (no `domain.atom` from that file uses it), so the import is
125 /// inert. Never affects [`Report::status`] or [`Report::exit_code`] — purely
126 /// informational. (Carried through from compilation; see [`UnusedImport`].)
127 pub unused_imports: Vec<UnusedImport>,
128 /// One record per declared `VAR` port: whether its value was supplied, fell
129 /// back to `DEFAULT`, or stayed UNKNOWN. The report's PLACEHOLDERS section.
130 /// Never affects [`Report::status`] or [`Report::exit_code`] — purely
131 /// informational. (Carried through from compilation; see [`PlaceholderInfo`].)
132 pub placeholders: Vec<PlaceholderInfo>,
133}
134
135/// An advisory hint that two atom names look like the same atom typed two
136/// different ways (e.g. `is_rolled_back` vs `is rolled_back`). **Purely a
137/// suggestion** — it never changes the verdict, the warning pool, or the exit
138/// code. It exists to catch the silent-typo trap where a misspelling creates a
139/// new UNKNOWN atom that quietly never links to the rest of the program.
140#[derive(Debug, Clone, PartialEq, Eq)]
141pub struct SimilarAtoms {
142 /// One atom's human label (`subject predicate [object]`).
143 pub a: String,
144 /// The other atom's human label.
145 pub b: String,
146 /// Why the pair was flagged (a short, fixed explanation).
147 pub reason: &'static str,
148}
149
150/// An advisory lint: a `FACT`/`NOT`/`ASSUME` whose atom appears in **no**
151/// `PREMISE` or `RULE`. Such an assertion is logically inert — nothing checks it
152/// and nothing is derived from it, so it can never produce a CONFLICT, WARNING or
153/// DERIVED. It is almost always a typo'd atom name or a leftover line. **Purely
154/// informational** — it never changes the verdict, the warning pool, or the exit
155/// code (a program full of orphans is still perfectly CONSISTENT).
156#[derive(Debug, Clone, PartialEq, Eq)]
157pub struct OrphanFact {
158 /// The atom's human label (`subject predicate [object]`), without polarity.
159 pub atom: String,
160 /// The asserted value — `False` means the surface line was `NOT`/`ASSUME NOT`.
161 pub value: Value,
162 /// Provenance of the inert assertion (source, line, kind = `FACT`/`NOT`/`ASSUME`).
163 pub origin: Origin,
164}
165
166/// One construct named in an [`Report::unsat_core`].
167#[derive(Debug, Clone, PartialEq, Eq)]
168pub struct CoreItem {
169 /// Provenance of the construct (source, line, kind, premise name if any).
170 pub origin: Origin,
171 /// A human label: the premise/rule name, or the atom for a bare `FACT`/`NOT`.
172 pub label: String,
173}
174
175/// Render atom `a` as the human string `domain.subject predicate [object]`. The
176/// domain prefix is always shown — atom identity now includes it, so the label
177/// is unambiguous (`physics.engine runs` vs `plan.engine runs`).
178pub(crate) fn label(c: &Compiled, a: AtomId) -> String {
179 let k = &c.atoms[a as usize];
180 match (&k.predicate, &k.object) {
181 // Full triple `domain.subject predicate object`.
182 (Some(p), Some(o)) => alloc::format!("{}.{} {} {}", k.domain, k.subject, p, o),
183 // Two-word atom `domain.subject predicate`.
184 (Some(p), None) => alloc::format!("{}.{} {}", k.domain, k.subject, p),
185 // Bare proposition (a VAR port): just `domain.subject`.
186 (None, _) => alloc::format!("{}.{}", k.domain, k.subject),
187 }
188}
189
190mod human;
191mod json;