elenchus_solver/
lib.rs

1//! elenchus-solver — the inference interpreter (forward pass).
2//!
3//! Consumes the [`Compiled`] IR from `elenchus-compiler` and evaluates it under
4//! three-valued Kleene logic (TRUE / FALSE / UNKNOWN, where UNKNOWN ≠ FALSE):
5//!
6//! 1. seed a model from confident `FACT`/`NOT` facts (and report `FACT X` + `NOT X`);
7//! 2. forward-chain `RULE`s to a fixpoint, deriving facts (a derived value that
8//!    contradicts an existing one is a CONFLICT);
9//! 3. evaluate every `Impossible` clause (the desugared `PREMISE`s):
10//!    - all literals forced TRUE → **CONFLICT** (the constraint is violated);
11//!    - some literal FALSE → satisfied → CONSISTENT;
12//!    - otherwise (no FALSE, an UNKNOWN remains): for implication premises this is a
13//!      **WARNING** (blocked by missing data), for list premises (EXCLUSIVE/FORBIDS/
14//!      ONEOF/ATLEAST) it is CONSISTENT (UNKNOWN means "no conflict yet").
15//!
16//! On `CHECK ... BIDIRECTIONAL` a **backward pass** also runs: the premises, rules
17//! and confident facts are encoded as CNF and handed to a small in-crate CDCL SAT
18//! core ([`sat`], replicating varisat's algorithm) to count models — 0 means the
19//! system is jointly unsatisfiable (a CONFLICT the forward pass may miss), ≥2
20//! means an alternative model exists (`UNDERDETERMINED`).
21#![no_std]
22// Every public item is documented; CI (`clippy -D warnings`) keeps it that way.
23#![warn(missing_docs)]
24
25extern crate alloc;
26
27#[cfg(feature = "std")]
28extern crate std;
29
30pub mod sat;
31
32use alloc::string::String;
33use alloc::vec;
34use alloc::vec::Vec;
35use core::fmt;
36
37use elenchus_compiler::{AtomId, Clause, Compiled, Lit, Origin, Value};
38pub use elenchus_compiler::{CompileError, MemoryResolver, Resolver, compile, compile_source};
39
40/// Three-valued truth (Kleene). UNKNOWN is a first-class value, not hidden FALSE.
41#[derive(Debug, Clone, Copy, PartialEq, Eq)]
42pub enum V3 {
43    /// Known true.
44    True,
45    /// Known false.
46    False,
47    /// Not asserted and not derivable — the absence of information, not falsity.
48    Unknown,
49}
50
51impl V3 {
52    /// Kleene negation: TRUE↔FALSE, and UNKNOWN stays UNKNOWN.
53    fn not(self) -> V3 {
54        match self {
55            V3::True => V3::False,
56            V3::False => V3::True,
57            V3::Unknown => V3::Unknown,
58        }
59    }
60}
61
62/// Overall verdict for the system.
63#[derive(Debug, Clone, Copy, PartialEq, Eq)]
64pub enum Status {
65    /// No contradictions, and (when checked) the model is pinned down.
66    Consistent,
67    /// The constraints are satisfiable but do not pin a unique assignment — an
68    /// alternative model exists (found by the backward pass on `BIDIRECTIONAL`).
69    Underdetermined,
70    /// A premise could not be checked because a needed atom is UNKNOWN.
71    Warning,
72    /// A premise is violated, or the premises + facts are jointly unsatisfiable.
73    Conflict,
74}
75
76/// A violated constraint (or a fact-level contradiction).
77#[derive(Debug, Clone, PartialEq, Eq)]
78pub struct Conflict {
79    /// Provenance of the violated constraint (source, line, premise name, kind).
80    pub origin: Origin,
81    /// Human labels of the atoms participating in the contradiction.
82    pub atoms: Vec<String>,
83    /// The derivation chain that forced the participating atoms to the values
84    /// which made the constraint fire — supporting facts first, then each rule
85    /// built on them, ending at the conflict. This is the answer to "CONFLICT,
86    /// but *why*?". Empty for a direct `FACT X` + `NOT X` contradiction and for
87    /// the `<system>` joint-unsatisfiability conflict (neither has a chain).
88    pub trace: Vec<TraceStep>,
89}
90
91/// One link in a [`Conflict`]'s derivation chain: an atom, the value it was
92/// forced to, and why it holds that value.
93#[derive(Debug, Clone, PartialEq, Eq)]
94pub struct TraceStep {
95    /// Human label of the atom (`subject predicate [object]`).
96    pub atom: String,
97    /// The confident value the atom was forced to (TRUE or FALSE).
98    pub value: Value,
99    /// Why the atom holds that value.
100    pub reason: TraceReason,
101}
102
103/// Why a [`TraceStep`] atom holds its value.
104#[derive(Debug, Clone, PartialEq, Eq)]
105pub enum TraceReason {
106    /// Asserted directly by a `FACT` / `NOT`.
107    Asserted(Origin),
108    /// Derived by a `RULE` whose antecedent atoms all held.
109    Derived {
110        /// Provenance of the firing rule.
111        origin: Origin,
112        /// Human labels of the antecedent atoms that supported the derivation.
113        from: Vec<String>,
114    },
115}
116
117/// A constraint that could not be checked because a needed atom is UNKNOWN.
118#[derive(Debug, Clone, PartialEq, Eq)]
119pub struct Warning {
120    /// Provenance of the constraint that could not be checked.
121    pub origin: Origin,
122    /// Human labels of the UNKNOWN atoms blocking the check.
123    pub blocked_by: Vec<String>,
124}
125
126/// A fact produced by a `RULE` during forward chaining.
127#[derive(Debug, Clone, PartialEq, Eq)]
128pub struct Derived {
129    /// Human label of the atom whose value was derived.
130    pub atom: String,
131    /// The value the rule assigned (TRUE, or FALSE for a `THEN NOT …`).
132    pub value: Value,
133    /// Provenance of the `RULE` that produced it.
134    pub origin: Origin,
135}
136
137/// The result of solving, self-contained (atom ids already resolved to labels).
138#[derive(Debug, Clone, PartialEq, Eq)]
139pub struct Report {
140    /// The overall verdict.
141    pub status: Status,
142    /// Every violated constraint / fact contradiction (sorted by source+line).
143    pub conflicts: Vec<Conflict>,
144    /// Every premise blocked by an UNKNOWN atom (sorted by source+line).
145    pub warnings: Vec<Warning>,
146    /// Facts produced by forward-chaining `RULE`s.
147    pub derived: Vec<Derived>,
148    /// When `UNDERDETERMINED`, the label of an atom left free by the constraints
149    /// (asserting it would pin the model down).
150    pub underdetermined: Option<String>,
151    /// When the system is jointly unsatisfiable but the forward pass found no
152    /// single violated constraint, the minimal set of constructs (facts /
153    /// premises / rules) whose removal restores satisfiability — i.e. the
154    /// smallest group jointly to blame. Empty in every other case.
155    pub unsat_core: Vec<CoreItem>,
156}
157
158/// One construct named in an [`Report::unsat_core`].
159#[derive(Debug, Clone, PartialEq, Eq)]
160pub struct CoreItem {
161    /// Provenance of the construct (source, line, kind, premise name if any).
162    pub origin: Origin,
163    /// A human label: the premise/rule name, or the atom for a bare `FACT`/`NOT`.
164    pub label: String,
165}
166
167impl Report {
168    /// CLI-style exit code: 0 = consistent, 1 = underdetermined/warnings, 2 = conflicts.
169    pub fn exit_code(&self) -> i32 {
170        match self.status {
171            Status::Conflict => 2,
172            Status::Underdetermined | Status::Warning => 1,
173            Status::Consistent => 0,
174        }
175    }
176
177    /// Render the report as a single-line JSON object (for tooling / MCP).
178    /// Hand-written so the crate stays dependency-free and `no_std`.
179    pub fn to_json(&self) -> String {
180        use core::fmt::Write as _;
181        let mut s = String::new();
182        let _ = write!(s, "{{\"status\":");
183        json_str(status_name(self.status), &mut s);
184        let _ = write!(s, ",\"exit_code\":{}", self.exit_code());
185
186        s.push_str(",\"conflicts\":[");
187        for (i, c) in self.conflicts.iter().enumerate() {
188            if i > 0 {
189                s.push(',');
190            }
191            json_origin(&c.origin, &mut s);
192            s.push_str(",\"atoms\":");
193            json_array(&c.atoms, &mut s);
194            s.push_str(",\"trace\":[");
195            for (j, step) in c.trace.iter().enumerate() {
196                if j > 0 {
197                    s.push(',');
198                }
199                json_trace_step(step, &mut s);
200            }
201            s.push_str("]}");
202        }
203        s.push_str("],\"warnings\":[");
204        for (i, w) in self.warnings.iter().enumerate() {
205            if i > 0 {
206                s.push(',');
207            }
208            json_origin(&w.origin, &mut s);
209            s.push_str(",\"blocked_by\":");
210            json_array(&w.blocked_by, &mut s);
211            s.push('}');
212        }
213        s.push_str("],\"derived\":[");
214        for (i, d) in self.derived.iter().enumerate() {
215            if i > 0 {
216                s.push(',');
217            }
218            s.push('{');
219            json_origin_fields(&d.origin, &mut s);
220            s.push_str(",\"atom\":");
221            json_str(&d.atom, &mut s);
222            let _ = write!(s, ",\"value\":{}", matches!(d.value, Value::True));
223            s.push('}');
224        }
225        s.push_str("],\"underdetermined\":");
226        match &self.underdetermined {
227            Some(atom) => json_str(atom, &mut s),
228            None => s.push_str("null"),
229        }
230        s.push_str(",\"unsat_core\":[");
231        for (i, it) in self.unsat_core.iter().enumerate() {
232            if i > 0 {
233                s.push(',');
234            }
235            json_origin(&it.origin, &mut s);
236            s.push_str(",\"label\":");
237            json_str(&it.label, &mut s);
238            s.push('}');
239        }
240        s.push_str("]}");
241        s
242    }
243}
244
245/// Push one derivation-trace step as a JSON object.
246fn json_trace_step(step: &TraceStep, out: &mut String) {
247    use core::fmt::Write as _;
248    out.push_str("{\"atom\":");
249    json_str(&step.atom, out);
250    let _ = write!(out, ",\"value\":{}", matches!(step.value, Value::True));
251    match &step.reason {
252        TraceReason::Asserted(o) => {
253            out.push_str(",\"how\":\"asserted\",");
254            json_origin_fields(o, out);
255            out.push_str(",\"from\":[]");
256        }
257        TraceReason::Derived { origin, from } => {
258            out.push_str(",\"how\":\"derived\",");
259            json_origin_fields(origin, out);
260            out.push_str(",\"from\":");
261            json_array(from, out);
262        }
263    }
264    out.push('}');
265}
266
267fn status_name(s: Status) -> &'static str {
268    match s {
269        Status::Consistent => "CONSISTENT",
270        Status::Underdetermined => "UNDERDETERMINED",
271        Status::Warning => "WARNING",
272        Status::Conflict => "CONFLICT",
273    }
274}
275
276/// Push a JSON-escaped string literal (including the surrounding quotes).
277fn json_str(value: &str, out: &mut String) {
278    use core::fmt::Write as _;
279    out.push('"');
280    for ch in value.chars() {
281        match ch {
282            '"' => out.push_str("\\\""),
283            '\\' => out.push_str("\\\\"),
284            '\n' => out.push_str("\\n"),
285            '\r' => out.push_str("\\r"),
286            '\t' => out.push_str("\\t"),
287            c if (c as u32) < 0x20 => {
288                let _ = write!(out, "\\u{:04x}", c as u32);
289            }
290            c => out.push(c),
291        }
292    }
293    out.push('"');
294}
295
296/// Push a JSON array of escaped strings.
297fn json_array(items: &[String], out: &mut String) {
298    out.push('[');
299    for (i, item) in items.iter().enumerate() {
300        if i > 0 {
301            out.push(',');
302        }
303        json_str(item, out);
304    }
305    out.push(']');
306}
307
308/// `"premise":..,"kind":..,"source":..,"line":..` (no braces).
309fn json_origin_fields(o: &Origin, out: &mut String) {
310    use core::fmt::Write as _;
311    out.push_str("\"premise\":");
312    match &o.premise {
313        Some(name) => json_str(name, out),
314        None => out.push_str("null"),
315    }
316    out.push_str(",\"kind\":");
317    json_str(o.kind, out);
318    out.push_str(",\"source\":");
319    json_str(&o.source, out);
320    let _ = write!(out, ",\"line\":{}", o.line);
321}
322
323/// Open an object `{` and write the origin fields.
324fn json_origin(o: &Origin, out: &mut String) {
325    out.push('{');
326    json_origin_fields(o, out);
327}
328
329/// Render atom `a` as the human string `subject predicate [object]`.
330fn label(c: &Compiled, a: AtomId) -> String {
331    let k = &c.atoms[a as usize];
332    match &k.object {
333        Some(o) => alloc::format!("{} {} {}", k.subject, k.predicate, o),
334        None => alloc::format!("{} {}", k.subject, k.predicate),
335    }
336}
337
338/// The three-valued value of a literal: the atom's value, flipped if negated.
339fn lit_value(model: &[V3], l: &Lit) -> V3 {
340    let v = model[l.atom as usize];
341    if l.negated { v.not() } else { v }
342}
343
344/// Kleene AND over a conjunction of literals (a rule antecedent / clause prefix).
345fn conjunction(model: &[V3], lits: &[Lit]) -> V3 {
346    let mut result = V3::True;
347    for l in lits {
348        match lit_value(model, l) {
349            V3::False => return V3::False,
350            V3::Unknown => result = V3::Unknown,
351            V3::True => {}
352        }
353    }
354    result
355}
356
357/// The status of one `Impossible` clause under the current model.
358enum ClauseEval {
359    /// Every literal is forced TRUE → the constraint is violated.
360    Violated,
361    /// Some literal is FALSE → the literals cannot all hold → satisfied.
362    Satisfied,
363    /// No FALSE literal, but an UNKNOWN remains: the check is blocked on these atoms.
364    Blocked(Vec<AtomId>),
365}
366
367/// Classify one `Impossible` clause under the model: all-true is a violation,
368/// any-false satisfies it, otherwise it is blocked on the remaining UNKNOWNs.
369fn eval_clause(model: &[V3], clause: &Clause) -> ClauseEval {
370    let mut any_false = false;
371    let mut all_true = true;
372    let mut blocked = Vec::new();
373    for l in &clause.lits {
374        match lit_value(model, l) {
375            V3::False => {
376                any_false = true;
377                all_true = false;
378            }
379            V3::Unknown => {
380                all_true = false;
381                blocked.push(l.atom);
382            }
383            V3::True => {}
384        }
385    }
386    if all_true {
387        ClauseEval::Violated
388    } else if any_false {
389        ClauseEval::Satisfied
390    } else {
391        ClauseEval::Blocked(blocked)
392    }
393}
394
395/// Why an atom holds its confident value — the forward pass records this so a
396/// conflict can be traced back to the facts and rules that forced it.
397#[derive(Clone)]
398enum AtomReason {
399    /// Set directly by a `FACT` / `NOT`.
400    Asserted(Origin),
401    /// Derived by a firing `RULE` from the listed antecedent atoms.
402    Derived { origin: Origin, from: Vec<AtomId> },
403}
404
405/// An internal conflict before labels and trace are materialized. `atoms` are the
406/// exact display strings; `cause` are the atoms whose forcing chains explain it
407/// (empty when there is no chain to show, e.g. a direct fact contradiction).
408struct RawConflict {
409    origin: Origin,
410    atoms: Vec<String>,
411    cause: Vec<AtomId>,
412}
413
414/// Working state of the forward + backward evaluation, evaluated as a pipeline.
415struct Eval<'a> {
416    c: &'a Compiled,
417    model: Vec<V3>,
418    /// Per-atom provenance, filled by `seed_facts` and `saturate_rules`; read by
419    /// `build_trace` once the model is final.
420    reason: Vec<Option<AtomReason>>,
421    conflicts: Vec<RawConflict>,
422    warnings: Vec<Warning>,
423    derived: Vec<Derived>,
424    /// Minimal set of constructs to blame when the backward pass finds UNSAT.
425    unsat_core: Vec<CoreItem>,
426}
427
428impl<'a> Eval<'a> {
429    fn new(c: &'a Compiled) -> Self {
430        Eval {
431            c,
432            model: vec![V3::Unknown; c.atoms.len()],
433            reason: vec![None; c.atoms.len()],
434            conflicts: Vec::new(),
435            warnings: Vec::new(),
436            derived: Vec::new(),
437            unsat_core: Vec::new(),
438        }
439    }
440
441    fn label(&self, a: AtomId) -> String {
442        label(self.c, a)
443    }
444
445    /// 1. Seed the model from confident facts; `FACT X` + `NOT X` is a CONFLICT.
446    fn seed_facts(&mut self) {
447        let c = self.c;
448        let n = c.atoms.len();
449        let mut t: Vec<Option<Origin>> = vec![None; n];
450        let mut f: Vec<Option<Origin>> = vec![None; n];
451        for fact in &c.facts {
452            let slot = match fact.value {
453                Value::True => &mut t,
454                Value::False => &mut f,
455            };
456            if slot[fact.atom as usize].is_none() {
457                slot[fact.atom as usize] = Some(fact.origin.clone());
458            }
459        }
460        for a in 0..n {
461            match (&t[a], &f[a]) {
462                (Some(o), Some(_)) => {
463                    self.model[a] = V3::True;
464                    self.reason[a] = Some(AtomReason::Asserted(o.clone()));
465                    self.conflicts.push(RawConflict {
466                        origin: o.clone(),
467                        atoms: vec![alloc::format!(
468                            "{} (asserted both TRUE and FALSE)",
469                            self.label(a as AtomId)
470                        )],
471                        cause: Vec::new(),
472                    });
473                }
474                (Some(o), None) => {
475                    self.model[a] = V3::True;
476                    self.reason[a] = Some(AtomReason::Asserted(o.clone()));
477                }
478                (None, Some(o)) => {
479                    self.model[a] = V3::False;
480                    self.reason[a] = Some(AtomReason::Asserted(o.clone()));
481                }
482                (None, None) => {}
483            }
484        }
485    }
486
487    /// 2. Forward-chain RULEs to a fixpoint, deriving facts (Kleene antecedent).
488    fn saturate_rules(&mut self) {
489        let c = self.c;
490        loop {
491            let mut changed = false;
492            for r in &c.rules {
493                if conjunction(&self.model, &r.antecedent) != V3::True {
494                    continue; // rule does not fire (FALSE, or blocked by UNKNOWN)
495                }
496                for cl in &r.consequent {
497                    let target = if cl.negated { V3::False } else { V3::True };
498                    match self.model[cl.atom as usize] {
499                        V3::Unknown => {
500                            self.model[cl.atom as usize] = target;
501                            self.reason[cl.atom as usize] = Some(AtomReason::Derived {
502                                origin: r.origin.clone(),
503                                from: r.antecedent.iter().map(|l| l.atom).collect(),
504                            });
505                            changed = true;
506                            self.derived.push(Derived {
507                                atom: self.label(cl.atom),
508                                value: if cl.negated {
509                                    Value::False
510                                } else {
511                                    Value::True
512                                },
513                                origin: r.origin.clone(),
514                            });
515                        }
516                        v if v == target => {}
517                        _ => {
518                            // The rule wants the opposite of a value the atom already
519                            // holds. Trace both sides: why the antecedent fired (its
520                            // atoms) and how the atom got its existing value.
521                            let mut cause: Vec<AtomId> =
522                                r.antecedent.iter().map(|l| l.atom).collect();
523                            cause.push(cl.atom);
524                            self.conflicts.push(RawConflict {
525                                origin: r.origin.clone(),
526                                atoms: vec![alloc::format!(
527                                    "{} (derived value contradicts a known fact)",
528                                    self.label(cl.atom)
529                                )],
530                                cause,
531                            });
532                        }
533                    }
534                }
535            }
536            if !changed {
537                break;
538            }
539        }
540    }
541
542    /// 3. Evaluate every `Impossible` clause against the model.
543    fn check_premises(&mut self) {
544        let c = self.c;
545        for clause in &c.clauses {
546            match eval_clause(&self.model, clause) {
547                ClauseEval::Violated => self.conflicts.push(RawConflict {
548                    origin: clause.origin.clone(),
549                    atoms: clause.lits.iter().map(|l| self.label(l.atom)).collect(),
550                    cause: clause.lits.iter().map(|l| l.atom).collect(),
551                }),
552                ClauseEval::Satisfied => {}
553                // Implication premises warn on missing data; list premises treat
554                // UNKNOWN as "no conflict yet" and stay consistent.
555                ClauseEval::Blocked(unknowns) if clause.origin.kind == "PREMISE" => {
556                    self.warnings.push(Warning {
557                        origin: clause.origin.clone(),
558                        blocked_by: unknowns.iter().map(|a| self.label(*a)).collect(),
559                    });
560                }
561                ClauseEval::Blocked(_) => {}
562            }
563        }
564    }
565
566    /// Build the derivation chain that explains why the `causes` atoms hold their
567    /// current values: a post-order walk of the reason graph so each atom's
568    /// supports appear before it (facts first, the conflict atoms last), with
569    /// every atom emitted once. Atoms with no recorded reason (UNKNOWN) are
570    /// skipped — a forced atom always has one.
571    fn build_trace(&self, causes: &[AtomId]) -> Vec<TraceStep> {
572        let mut visited = vec![false; self.c.atoms.len()];
573        let mut out = Vec::new();
574        for &a in causes {
575            self.trace_dfs(a, &mut visited, &mut out);
576        }
577        out
578    }
579
580    fn trace_dfs(&self, a: AtomId, visited: &mut [bool], out: &mut Vec<TraceStep>) {
581        if visited[a as usize] {
582            return;
583        }
584        visited[a as usize] = true;
585        let value = match v3_to_value(self.model[a as usize]) {
586            Some(v) => v,
587            None => return, // UNKNOWN: nothing forced it, nothing to explain
588        };
589        let reason = match &self.reason[a as usize] {
590            Some(AtomReason::Asserted(o)) => TraceReason::Asserted(o.clone()),
591            Some(AtomReason::Derived { origin, from }) => {
592                for &f in from {
593                    self.trace_dfs(f, visited, out); // supports first
594                }
595                TraceReason::Derived {
596                    origin: origin.clone(),
597                    from: from.iter().map(|&f| self.label(f)).collect(),
598                }
599            }
600            None => return,
601        };
602        out.push(TraceStep {
603            atom: self.label(a),
604            value,
605            reason,
606        });
607    }
608
609    /// Backward pass (model finding), run only when a CHECK requests BIDIRECTIONAL.
610    /// Encodes premises + rules + facts as CNF and asks the SAT core for models.
611    /// No model means the system is jointly unsatisfiable (a CONFLICT the forward
612    /// pass may have missed). Two or more models means an alternative exists; we
613    /// return the UNDERDETERMINED witness — the first constrained atom the two
614    /// models disagree on.
615    fn backward_pass(&mut self) -> Option<String> {
616        if !self.c.checks.iter().any(|ch| ch.bidirectional) {
617            return None;
618        }
619        let (cnf, project) = build_cnf(self.c);
620        let found = sat::models(&cnf, &project, 2);
621        match found.len() {
622            0 if self.conflicts.is_empty() => {
623                self.unsat_core = minimal_unsat_core(self.c);
624                self.conflicts.push(RawConflict {
625                    origin: Origin {
626                        source: String::from("<system>"),
627                        line: 0,
628                        premise: None,
629                        kind: "UNSAT",
630                    },
631                    atoms: vec![String::from(
632                        "the premises and facts are jointly unsatisfiable",
633                    )],
634                    cause: Vec::new(),
635                });
636                None
637            }
638            n if n >= 2 => {
639                let (m0, m1) = (&found[0], &found[1]);
640                project
641                    .iter()
642                    .find(|&&v| m0[v as usize] != m1[v as usize])
643                    .map(|&v| self.label(v))
644                    .or_else(|| Some(String::from("a free atom")))
645            }
646            _ => None,
647        }
648    }
649
650    /// Run the backward pass, sort deterministically, and assemble the report.
651    fn finish(mut self) -> Report {
652        let underdetermined = self.backward_pass();
653        self.conflicts.sort_by_key(|c| key(&c.origin));
654        self.warnings.sort_by_key(|w| key(&w.origin));
655        let status = if !self.conflicts.is_empty() {
656            Status::Conflict
657        } else if underdetermined.is_some() {
658            Status::Underdetermined
659        } else if !self.warnings.is_empty() {
660            Status::Warning
661        } else {
662            Status::Consistent
663        };
664        // Materialize each raw conflict into its public form, attaching the
665        // derivation chain (reasons are final once the forward pass is done).
666        let conflicts: Vec<Conflict> = self
667            .conflicts
668            .iter()
669            .map(|rc| Conflict {
670                origin: rc.origin.clone(),
671                atoms: rc.atoms.clone(),
672                trace: self.build_trace(&rc.cause),
673            })
674            .collect();
675        Report {
676            status,
677            conflicts,
678            warnings: self.warnings,
679            derived: self.derived,
680            underdetermined,
681            unsat_core: self.unsat_core,
682        }
683    }
684}
685
686/// Evaluate a compiled program: the three-valued forward pass, then the backward
687/// pass on `BIDIRECTIONAL`.
688pub fn solve(c: &Compiled) -> Report {
689    let mut e = Eval::new(c);
690    e.seed_facts();
691    e.saturate_rules();
692    e.check_premises();
693    e.finish()
694}
695
696/// Encode the premises (`Impossible` clauses), rules (as implications), and
697/// confident facts (as unit clauses) into CNF for the backward pass. Also
698/// returns the constrained atoms (those appearing in a clause or rule) to
699/// project model counting onto.
700fn build_cnf(c: &Compiled) -> (sat::Cnf, Vec<sat::Var>) {
701    use sat::SatLit;
702    let mut cnf = sat::Cnf::new(c.atoms.len());
703    let mut constrained = vec![false; c.atoms.len()];
704    let mark = |a: AtomId, constrained: &mut [bool]| constrained[a as usize] = true;
705
706    // Impossible([L1..Ln]) == (¬L1 ∨ … ∨ ¬Ln); ¬L of (atom, negated) is (atom, negated).
707    for clause in &c.clauses {
708        let lits = clause
709            .lits
710            .iter()
711            .map(|l| {
712                mark(l.atom, &mut constrained);
713                SatLit::new(l.atom, l.negated)
714            })
715            .collect();
716        cnf.add_clause(lits);
717    }
718    // RULE WHEN A.. THEN C.. == for each C: (¬A1 ∨ … ∨ C).
719    for r in &c.rules {
720        for cons in &r.consequent {
721            let mut lits: Vec<SatLit> = r
722                .antecedent
723                .iter()
724                .map(|a| {
725                    mark(a.atom, &mut constrained);
726                    SatLit::new(a.atom, a.negated)
727                })
728                .collect();
729            mark(cons.atom, &mut constrained);
730            lits.push(SatLit::new(cons.atom, !cons.negated));
731            cnf.add_clause(lits);
732        }
733    }
734    // Confident facts as unit clauses.
735    for f in &c.facts {
736        let lit = match f.value {
737            Value::True => SatLit::positive(f.atom),
738            Value::False => SatLit::negative(f.atom),
739        };
740        cnf.add_clause(vec![lit]);
741    }
742
743    let project = (0..c.atoms.len() as AtomId)
744        .filter(|&a| constrained[a as usize])
745        .collect();
746    (cnf, project)
747}
748
749/// Convert a three-valued model entry to a confident [`Value`] (UNKNOWN → `None`).
750fn v3_to_value(v: V3) -> Option<Value> {
751    match v {
752        V3::True => Some(Value::True),
753        V3::False => Some(Value::False),
754        V3::Unknown => None,
755    }
756}
757
758/// A removable source construct (one fact, one premise, or one rule) and the CNF
759/// clauses it contributes — the unit of an unsat-core explanation.
760struct Construct {
761    origin: Origin,
762    label: String,
763    clauses: Vec<Vec<sat::SatLit>>,
764}
765
766/// Two origins refer to the same source construct.
767fn same_origin(a: &Origin, b: &Origin) -> bool {
768    a.source == b.source && a.line == b.line && a.premise == b.premise && a.kind == b.kind
769}
770
771/// Split the program into removable constructs. A premise that desugared into
772/// several clauses (e.g. an `EXCLUSIVE` over n atoms) is grouped back into one
773/// construct by origin, so the core blames whole premises, not clause shards.
774fn constructs(c: &Compiled) -> Vec<Construct> {
775    use sat::SatLit;
776    let mut out: Vec<Construct> = Vec::new();
777
778    for f in &c.facts {
779        let lit = match f.value {
780            Value::True => SatLit::positive(f.atom),
781            Value::False => SatLit::negative(f.atom),
782        };
783        out.push(Construct {
784            origin: f.origin.clone(),
785            label: label(c, f.atom),
786            clauses: vec![vec![lit]],
787        });
788    }
789
790    let mut premises: Vec<Construct> = Vec::new();
791    for clause in &c.clauses {
792        let lits: Vec<SatLit> = clause
793            .lits
794            .iter()
795            .map(|l| SatLit::new(l.atom, l.negated))
796            .collect();
797        match premises
798            .iter_mut()
799            .find(|k| same_origin(&k.origin, &clause.origin))
800        {
801            Some(k) => k.clauses.push(lits),
802            None => premises.push(Construct {
803                label: clause.origin.premise.clone().unwrap_or_default(),
804                origin: clause.origin.clone(),
805                clauses: vec![lits],
806            }),
807        }
808    }
809    out.extend(premises);
810
811    for r in &c.rules {
812        let clauses = r
813            .consequent
814            .iter()
815            .map(|cons| {
816                let mut lits: Vec<SatLit> = r
817                    .antecedent
818                    .iter()
819                    .map(|a| SatLit::new(a.atom, a.negated))
820                    .collect();
821                lits.push(SatLit::new(cons.atom, !cons.negated));
822                lits
823            })
824            .collect();
825        out.push(Construct {
826            label: r.origin.premise.clone().unwrap_or_default(),
827            origin: r.origin.clone(),
828            clauses,
829        });
830    }
831    out
832}
833
834/// Is the program satisfiable using only the constructs marked active?
835fn subset_is_sat(num_vars: usize, all: &[Construct], active: &[bool]) -> bool {
836    let mut cnf = sat::Cnf::new(num_vars);
837    for (k, &keep) in all.iter().zip(active) {
838        if keep {
839            for cl in &k.clauses {
840                cnf.add_clause(cl.clone());
841            }
842        }
843    }
844    sat::solve(&cnf).is_some()
845}
846
847/// A minimal (1-minimal) unsat core via deletion-based minimization: starting
848/// from the whole (unsatisfiable) program, drop each construct in turn; if the
849/// rest is still unsatisfiable the construct was not needed. What survives is an
850/// irreducible set jointly to blame. Called only when the full system is UNSAT.
851fn minimal_unsat_core(c: &Compiled) -> Vec<CoreItem> {
852    let all = constructs(c);
853    let mut active = vec![true; all.len()];
854    for i in 0..all.len() {
855        active[i] = false;
856        if subset_is_sat(c.atoms.len(), &all, &active) {
857            active[i] = true; // removing it restored SAT → it is part of the core
858        }
859    }
860    let mut core: Vec<CoreItem> = all
861        .iter()
862        .zip(&active)
863        .filter(|&(_, &keep)| keep)
864        .map(|(k, _)| CoreItem {
865            origin: k.origin.clone(),
866            label: k.label.clone(),
867        })
868        .collect();
869    core.sort_by_key(|it| key(&it.origin));
870    core
871}
872
873/// Sort key giving conflicts/warnings a stable, source-then-line order.
874fn key(o: &Origin) -> (String, u32) {
875    (o.source.clone(), o.line)
876}
877
878/// Parse → compile → solve a single source.
879pub fn verify_source(name: &str, src: &str) -> Result<Report, CompileError> {
880    Ok(solve(&compile_source(name, src)?))
881}
882
883/// Parse → compile (resolving imports) → solve, given a [`Resolver`].
884pub fn verify<R: Resolver>(root: &str, resolver: &R) -> Result<Report, CompileError> {
885    Ok(solve(&compile(root, resolver)?))
886}
887
888// --- human-readable report -------------------------------------------------
889
890impl fmt::Display for Status {
891    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
892        f.write_str(match self {
893            Status::Consistent => "CONSISTENT",
894            Status::Underdetermined => "UNDERDETERMINED",
895            Status::Warning => "WARNING",
896            Status::Conflict => "CONFLICT",
897        })
898    }
899}
900
901/// Format provenance as `name (KIND)  [source:line]` for the human report.
902fn premise_tag(o: &Origin) -> String {
903    let name = o.premise.as_deref().unwrap_or("-");
904    alloc::format!("{} ({})  [{}:{}]", name, o.kind, o.source, o.line)
905}
906
907/// One derivation-trace line for the human report.
908fn trace_line(step: &TraceStep) -> String {
909    let v = match step.value {
910        Value::True => "TRUE",
911        Value::False => "FALSE",
912    };
913    match &step.reason {
914        TraceReason::Asserted(o) => {
915            alloc::format!(
916                "{} = {}   [{} {}:{}]",
917                step.atom,
918                v,
919                o.kind,
920                o.source,
921                o.line
922            )
923        }
924        TraceReason::Derived { origin, from } => alloc::format!(
925            "{} = {}   from {} ({})  [{}:{}]  <= {}",
926            step.atom,
927            v,
928            origin.premise.as_deref().unwrap_or("-"),
929            origin.kind,
930            origin.source,
931            origin.line,
932            from.join(", ")
933        ),
934    }
935}
936
937impl fmt::Display for Report {
938    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
939        writeln!(f, "RESULT: {}", self.status)?;
940        for c in &self.conflicts {
941            writeln!(f, "  CONFLICT  {}", premise_tag(&c.origin))?;
942            for a in &c.atoms {
943                writeln!(f, "      {}", a)?;
944            }
945            if !c.trace.is_empty() {
946                writeln!(f, "      why:")?;
947                for step in &c.trace {
948                    writeln!(f, "        {}", trace_line(step))?;
949                }
950            }
951        }
952        if !self.unsat_core.is_empty() {
953            writeln!(
954                f,
955                "  CORE  smallest jointly-unsatisfiable set ({}):",
956                self.unsat_core.len()
957            )?;
958            for it in &self.unsat_core {
959                let name = if it.label.is_empty() { "-" } else { &it.label };
960                writeln!(
961                    f,
962                    "        {} ({})  [{}:{}]",
963                    name, it.origin.kind, it.origin.source, it.origin.line
964                )?;
965            }
966        }
967        for w in &self.warnings {
968            writeln!(f, "  WARNING   {}", premise_tag(&w.origin))?;
969            writeln!(f, "      blocked by: {}", w.blocked_by.join(", "))?;
970        }
971        if let Some(atom) = &self.underdetermined {
972            writeln!(f, "  UNDERDETERMINED  an alternative model exists")?;
973            writeln!(f, "      pin it down: add  FACT {atom}  or  NOT {atom}")?;
974        }
975        for d in &self.derived {
976            let v = match d.value {
977                Value::True => "TRUE",
978                Value::False => "FALSE",
979            };
980            writeln!(
981                f,
982                "  DERIVED   {} = {}   from {}",
983                d.atom,
984                v,
985                premise_tag(&d.origin)
986            )?;
987        }
988        let underdetermined = usize::from(self.status == Status::Underdetermined);
989        writeln!(
990            f,
991            "SUMMARY: {} conflicts, {} underdetermined, {} warnings, {} derived",
992            self.conflicts.len(),
993            underdetermined,
994            self.warnings.len(),
995            self.derived.len()
996        )?;
997        write!(f, "EXIT_CODE: {}", self.exit_code())
998    }
999}
1000
1001#[cfg(test)]
1002mod tests {
1003    use super::*;
1004
1005    #[test]
1006    fn clean_consistent() {
1007        let r = verify_source("<t>", "FACT x a\nCHECK x\n").unwrap();
1008        assert_eq!(r.status, Status::Consistent);
1009        assert!(r.conflicts.is_empty() && r.warnings.is_empty());
1010    }
1011
1012    #[test]
1013    fn fact_contradiction_is_conflict() {
1014        let r = verify_source("<t>", "FACT x a\nNOT x a\n").unwrap();
1015        assert_eq!(r.status, Status::Conflict);
1016        assert_eq!(r.conflicts.len(), 1);
1017    }
1018
1019    #[test]
1020    fn exclusive_violation_is_conflict() {
1021        let src = include_str!("../../../docs/examples/conflict.vrf");
1022        let r = verify_source("conflict.vrf", src).unwrap();
1023        assert_eq!(r.status, Status::Conflict);
1024        assert_eq!(
1025            r.conflicts[0].origin.premise.as_deref(),
1026            Some("fly_xor_swim")
1027        );
1028        assert_eq!(r.conflicts[0].atoms.len(), 2);
1029    }
1030
1031    #[test]
1032    fn exclusive_with_unknown_is_consistent_not_warning() {
1033        // flying TRUE, swimming UNKNOWN — at most one can hold, no conflict, no warning.
1034        let r = verify_source("<t>", "FACT A has flying\nPREMISE e:\n    EXCLUSIVE\n        A has flying\n        A has swimming\n").unwrap();
1035        assert_eq!(r.status, Status::Consistent);
1036        assert!(r.warnings.is_empty());
1037    }
1038
1039    #[test]
1040    fn implication_missing_consequent_is_warning() {
1041        // WHEN flying THEN wing: flying TRUE, wing UNKNOWN → blocked → WARNING.
1042        let r = verify_source(
1043            "<t>",
1044            "FACT A has flying\nPREMISE w:\n    WHEN A has flying\n    THEN A has wing\n",
1045        )
1046        .unwrap();
1047        assert_eq!(r.status, Status::Warning);
1048        assert_eq!(r.warnings.len(), 1);
1049        assert_eq!(r.warnings[0].blocked_by, vec![String::from("A has wing")]);
1050    }
1051
1052    #[test]
1053    fn implication_satisfied_is_consistent() {
1054        let r = verify_source("<t>", "FACT A has flying\nFACT A has wing\nPREMISE w:\n    WHEN A has flying\n    THEN A has wing\n").unwrap();
1055        assert_eq!(r.status, Status::Consistent);
1056    }
1057
1058    #[test]
1059    fn implication_violated_is_conflict() {
1060        // antecedent TRUE, consequent FALSE → CONFLICT.
1061        let r = verify_source("<t>", "FACT A has flying\nNOT A has wing\nPREMISE w:\n    WHEN A has flying\n    THEN A has wing\n").unwrap();
1062        assert_eq!(r.status, Status::Conflict);
1063    }
1064
1065    #[test]
1066    fn rule_derives_fact() {
1067        let r = verify_source(
1068            "<t>",
1069            "FACT A has flying\nRULE o:\n    WHEN A has flying\n    THEN A needs oxygen\n",
1070        )
1071        .unwrap();
1072        assert_eq!(r.status, Status::Consistent);
1073        assert_eq!(r.derived.len(), 1);
1074        assert_eq!(r.derived[0].atom, "A needs oxygen");
1075    }
1076
1077    #[test]
1078    fn rule_derivation_contradiction_is_conflict() {
1079        // rule derives `A needs oxygen` TRUE, but it's asserted FALSE.
1080        let r = verify_source("<t>", "FACT A has flying\nNOT A needs oxygen\nRULE o:\n    WHEN A has flying\n    THEN A needs oxygen\n").unwrap();
1081        assert_eq!(r.status, Status::Conflict);
1082    }
1083
1084    #[test]
1085    fn bidirectional_finds_alternative_model_underdetermined() {
1086        // EXCLUSIVE(a,b) with no facts: {FF, TF, FT} all satisfy → not unique.
1087        let r = verify_source(
1088            "<t>",
1089            "PREMISE e:\n    EXCLUSIVE\n        x a\n        x b\nCHECK x BIDIRECTIONAL\n",
1090        )
1091        .unwrap();
1092        assert_eq!(r.status, Status::Underdetermined);
1093    }
1094
1095    #[test]
1096    fn fact_pins_unique_model_consistent() {
1097        // Same premise, but FACT x a forces b false → the only model → CONSISTENT.
1098        let r = verify_source(
1099            "<t>",
1100            "FACT x a\nPREMISE e:\n    EXCLUSIVE\n        x a\n        x b\nCHECK x BIDIRECTIONAL\n",
1101        )
1102        .unwrap();
1103        assert_eq!(r.status, Status::Consistent);
1104    }
1105
1106    #[test]
1107    fn no_bidirectional_skips_backward_pass() {
1108        // Plain CHECK: alternatives are not searched → stays CONSISTENT, not UNDERDETERMINED.
1109        let r = verify_source(
1110            "<t>",
1111            "PREMISE e:\n    EXCLUSIVE\n        x a\n        x b\nCHECK x\n",
1112        )
1113        .unwrap();
1114        assert_eq!(r.status, Status::Consistent);
1115    }
1116
1117    #[test]
1118    fn creature_example_forward_pass() {
1119        let src = include_str!("../../../docs/examples/creature.vrf");
1120        let r = verify_source("creature.vrf", src).unwrap();
1121        // fly_xor_swim & no_dual_temp consistent; wings_need_bone → 2 warnings
1122        // (wing, bone); needs_oxygen derived; no conflicts.
1123        assert_eq!(r.status, Status::Warning);
1124        assert!(r.conflicts.is_empty());
1125        assert_eq!(r.warnings.len(), 2);
1126        assert_eq!(r.derived.len(), 1);
1127        assert_eq!(r.derived[0].atom, "Creature.A needs oxygen");
1128    }
1129
1130    #[test]
1131    fn roles_puzzle_is_uniquely_solved() {
1132        // 3 people × 3 roles, ONEOF per person and per role, two clues. The
1133        // backward (SAT) pass must find the assignment satisfiable AND unique —
1134        // i.e. CONSISTENT, not UNDERDETERMINED.
1135        let src = include_str!("../../../docs/examples/roles-puzzle.vrf");
1136        let r = verify_source("roles-puzzle.vrf", src).unwrap();
1137        assert_eq!(r.status, Status::Consistent);
1138        assert!(r.conflicts.is_empty());
1139        assert!(r.underdetermined.is_none());
1140    }
1141
1142    #[test]
1143    fn roles_puzzle_underdetermined_without_a_clue() {
1144        // Drop the `NOT bob is qa` clue and the solution is no longer unique
1145        // (bob/carol can swap dev/qa) — the SAT pass reports UNDERDETERMINED.
1146        // Normalize CRLF first: on a Windows checkout include_str! embeds the file
1147        // with \r\n, so a literal "...\n" match would otherwise miss the line.
1148        let src = include_str!("../../../docs/examples/roles-puzzle.vrf")
1149            .replace("\r\n", "\n")
1150            .replace("NOT  bob is qa\n", "");
1151        let r = verify_source("roles-puzzle.vrf", &src).unwrap();
1152        assert_eq!(r.status, Status::Underdetermined);
1153    }
1154
1155    #[test]
1156    fn socrates_chain_is_a_conflict() {
1157        // human → animal → living → mortal (3 derivations), then mortal EXCLUSIVE
1158        // immortal with `immortal` asserted → CONFLICT on the exclusivity premise.
1159        let src = include_str!("../../../docs/examples/socrates.vrf");
1160        let r = verify_source("socrates.vrf", src).unwrap();
1161        assert_eq!(r.status, Status::Conflict);
1162        assert_eq!(r.conflicts.len(), 1);
1163        assert_eq!(
1164            r.conflicts[0].origin.premise.as_deref(),
1165            Some("mortal_xor_immortal")
1166        );
1167        assert_eq!(r.derived.len(), 3); // animal, living, mortal
1168    }
1169
1170    // --- conflict explainability: derivation trace + minimal unsat core ------
1171
1172    #[test]
1173    fn forward_conflict_carries_a_trace_of_its_facts() {
1174        let r = verify_source(
1175            "<t>",
1176            "FACT x a\nFACT x b\nPREMISE e:\n    EXCLUSIVE\n        x a\n        x b\nCHECK x\n",
1177        )
1178        .unwrap();
1179        assert_eq!(r.status, Status::Conflict);
1180        let t = &r.conflicts[0].trace;
1181        assert_eq!(t.len(), 2);
1182        assert_eq!(t[0].atom, "x a");
1183        assert_eq!(t[0].value, Value::True);
1184        assert!(matches!(t[0].reason, TraceReason::Asserted(_)));
1185        assert!(r.unsat_core.is_empty());
1186    }
1187
1188    #[test]
1189    fn derivation_chain_is_traced_back_to_the_root_fact() {
1190        // human → animal → living → mortal, then mortal XOR immortal (immortal asserted).
1191        let src = include_str!("../../../docs/examples/socrates.vrf");
1192        let r = verify_source("socrates.vrf", src).unwrap();
1193        let t = &r.conflicts[0].trace;
1194        // human (fact) + animal, living, mortal (derived) + immortal (fact) = 5 steps,
1195        // supports before dependents.
1196        assert_eq!(t.len(), 5);
1197        assert_eq!(t[0].atom, "socrates is human");
1198        assert!(matches!(t[0].reason, TraceReason::Asserted(_)));
1199        let mortal = t.iter().find(|s| s.atom == "socrates is mortal").unwrap();
1200        match &mortal.reason {
1201            TraceReason::Derived { from, .. } => {
1202                assert_eq!(from, &vec![String::from("socrates is living")]);
1203            }
1204            _ => panic!("mortal should be derived, not asserted"),
1205        }
1206    }
1207
1208    #[test]
1209    fn direct_fact_contradiction_has_no_trace() {
1210        let r = verify_source("<t>", "FACT x a\nNOT x a\nCHECK x\n").unwrap();
1211        assert_eq!(r.status, Status::Conflict);
1212        assert!(r.conflicts[0].trace.is_empty());
1213    }
1214
1215    #[test]
1216    fn jointly_unsatisfiable_reports_a_minimal_core() {
1217        // ONEOF(a,b); a→c; b→c; NOT c. Unsat only via case-split, so the forward
1218        // pass misses it and the backward pass produces the core.
1219        let src = "PREMISE one:\n    ONEOF\n        x a\n        x b\nPREMISE ac:\n    WHEN x a\n    THEN x c\nPREMISE bc:\n    WHEN x b\n    THEN x c\nNOT x c\nCHECK x BIDIRECTIONAL\n";
1220        let r = verify_source("<t>", src).unwrap();
1221        assert_eq!(r.status, Status::Conflict);
1222        assert_eq!(r.conflicts[0].origin.kind, "UNSAT");
1223        assert_eq!(r.unsat_core.len(), 4);
1224        let labels: Vec<&str> = r.unsat_core.iter().map(|c| c.label.as_str()).collect();
1225        assert!(labels.contains(&"one"));
1226        assert!(labels.contains(&"x c")); // the bare NOT fact is labelled by its atom
1227    }
1228
1229    #[test]
1230    fn unsat_core_excludes_irrelevant_constructs() {
1231        // The same unsat cluster, plus an unrelated fact + premise that must not
1232        // appear in the (irreducible) core.
1233        let src = "PREMISE one:\n    ONEOF\n        x a\n        x b\nPREMISE ac:\n    WHEN x a\n    THEN x c\nPREMISE bc:\n    WHEN x b\n    THEN x c\nNOT x c\nFACT z here\nPREMISE noise:\n    EXCLUSIVE\n        z here\n        z gone\nCHECK x BIDIRECTIONAL\n";
1234        let r = verify_source("<t>", src).unwrap();
1235        assert_eq!(r.status, Status::Conflict);
1236        assert_eq!(r.unsat_core.len(), 4);
1237        let labels: Vec<&str> = r.unsat_core.iter().map(|c| c.label.as_str()).collect();
1238        assert!(!labels.contains(&"noise"));
1239        assert!(!labels.iter().any(|l| l.contains("here")));
1240    }
1241
1242    #[test]
1243    fn consistent_report_has_empty_core_and_no_trace() {
1244        let r = verify_source("<t>", "FACT x a\nCHECK x BIDIRECTIONAL\n").unwrap();
1245        assert_eq!(r.status, Status::Consistent);
1246        assert!(r.unsat_core.is_empty());
1247        assert!(r.conflicts.is_empty());
1248    }
1249}
elenchus_solver/lib.rs

elenchus_solver/
lib.rs
