nibli-reason 0.1.0

//! nibli-reason (logic/reasoning) engine: FOL assertion and query via demand-driven backward-chaining.
//!
//! This is the core inference component of Nibli. It maintains a stateful knowledge
//! base with a fact index and backward-chaining rule engine:
//!
//! - **Fact assertion** — Ground predicates stored as typed `StoredFact` via pluggable `FactStore` backend.
//!   Universal quantifiers compile to `UniversalRuleRecord` templates for backward-chaining.
//! - **Entailment queries** — Recursive formula checking via [`check_formula_holds`] with
//!   demand-driven backward-chaining through universal rules.
//! - **Proof traces** — [`check_formula_holds_recording`] builds a proof tree recording which
//!   rule/axiom was applied at each step (19 proof rule variants). Multi-hop derivation
//!   provenance traces derived facts through universal rule chains via backward-chaining.
//! - **Witness extraction** — [`find_witnesses`] returns all satisfying entity bindings for
//!   existential variables.
//! - **Compute dispatch** — `ComputeNode` predicates are forwarded to the host-provided
//!   `compute-backend` WIT interface for external evaluation.
//!
//! The knowledge base uses `RefCell` (not `Mutex`) — single-threaded WASI. All
//! mutable state — facts, rules, the predicate-result cache, the compute
//! dispatch, and the cancel flag — lives PER-INSTANCE on `KnowledgeBaseInner`;
//! there are no global or thread-local statics, so distinct KBs (e.g. one per
//! request on the multithreaded server) never interfere.

#![allow(dead_code)]

use nibli_types::error::NibliError;
use nibli_types::logic::{
    FactSummary, LogicBuffer, LogicNode, LogicalTerm, ProofRule, ProofStep, ProofTrace,
    QueryResult, ResourceKind, UnknownReason, WitnessBinding,
};
use std::borrow::Cow;
use std::cell::RefCell;
use std::collections::{HashMap, HashSet};
use std::sync::Arc;
mod compute;
/// Fact store abstraction (trait + in-memory implementation).
pub mod fact_store;
mod materialize;
mod reasoning;
mod rules;

pub use materialize::Ineligible;

pub use compute::ComputeRequest;

use compute::*;
use reasoning::*;
use rules::*;

/// The built-in arithmetic predicates marked as `ComputeNode` by default —
/// `product` (×), `sum` (+), `quotient` (÷). The shared default for every
/// embedder (nibli-engine, nibli-pipeline, nibli-wasm), paired with
/// `transform_compute_nodes`.
pub fn default_compute_predicates() -> HashSet<String> {
    nibli_types::relations::BUILTIN_ARITHMETIC
        .iter()
        .map(|s| s.to_string())
        .collect()
}

/// Transform registered compute predicates from Predicate → ComputeNode in a logic buffer.
/// Call this after nibli-semantics compilation and before asserting/querying.
pub fn transform_compute_nodes(buf: &mut LogicBuffer, compute_preds: &HashSet<String>) {
    let nodes = std::mem::take(&mut buf.nodes);
    buf.nodes = nodes
        .into_iter()
        .map(|node| match &node {
            LogicNode::Predicate((rel, _)) if compute_preds.contains(rel.as_str()) => {
                let LogicNode::Predicate(inner) = node else {
                    unreachable!("already matched as Predicate in guard")
                };
                LogicNode::ComputeNode(inner)
            }
            _ => node,
        })
        .collect();
}

pub mod kb;
pub use kb::KnowledgeBase;
pub(crate) use kb::*;

/// One predicate's row in [`KnowledgeBase::stratification_report`].
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub struct StratumRow {
    /// Surface relation name — role predicates (`p_x1`) collapsed onto their anchor (`p`).
    pub predicate: String,
    /// Stratum level. 0 means nothing negative sits beneath it; each negative edge
    /// crossed raises the level by one, so a rule may only read `~q` from a STRICTLY
    /// lower stratum. This is the assignment `proofs/Stratification.lean` proves exists
    /// whenever `check_stratification` accepted the KB.
    pub stratum: usize,
    /// `true` when NO rule concludes this predicate: base / extensional (EDB).
    /// `false` when at least one rule does: derived / intensional (IDB).
    pub base: bool,
    /// Outgoing dependency edges — "this predicate READS that one" — sorted and
    /// deduplicated.
    pub edges: Vec<StratumEdge>,
}

/// One outgoing dependency edge in a [`StratumRow`].
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
pub struct StratumEdge {
    /// The predicate depended upon (surface name).
    pub to: String,
    /// `true` when read under negation-as-failure — the edge that forces a stratum
    /// boundary. `false` for an ordinary positive dependency.
    pub negative: bool,
}

/// Internal methods that return `Result<_, String>` for use by both the WIT boundary and tests.
impl KnowledgeBase {
    fn combine_root_results(left: QueryResult, right: QueryResult) -> QueryResult {
        if left.is_false() || right.is_false() {
            QueryResult::False
        } else if left.is_true() && right.is_true() {
            QueryResult::True
        } else {
            // Shared with And/Or so the four-valued non-definitive precedence cannot drift.
            reasoning::combine_indeterminate(left, right)
        }
    }

    /// Assert FOL facts from a logic buffer into the knowledge base.
    /// Stores the buffer in the fact registry and returns a unique fact ID.
    fn assert_fact_inner(&self, logic: LogicBuffer, label: String) -> Result<u64, String> {
        let mut inner = self.inner.borrow_mut();
        let id = inner.fresh_fact_id();
        inner.current_assertion_id = Some(id);
        let result = process_assertion(&mut inner, &logic);
        // ALWAYS clear: a stale id would mis-attribute the NEXT assertion's rules
        // in rule_source_map (register_rule reads current_assertion_id).
        inner.current_assertion_id = None;
        if let Err(e) = result {
            // Atomic rollback. A multi-root assertion that fails on a later root
            // leaves earlier roots' facts/rules in the live store, but the
            // FactRecord is only inserted on success — so those facts would be
            // orphaned (un-listable, un-retractable). The failed assertion has no
            // FactRecord, so rebuilding from the durable registry reproduces the
            // exact pre-assertion state, discarding the partial mutation.
            let rb = Self::rebuild_inner(&mut inner);
            invalidate_pred_cache(&inner);
            return match rb {
                Ok(()) => Err(e),
                Err(re) => Err(format!("{e} (additionally, rollback failed: {re})")),
            };
        }
        inner.fact_registry.insert(
            id,
            FactRecord {
                id,
                buffer: logic,
                label,
                retracted: false,
            },
        );
        invalidate_pred_cache(&inner); // Tabling: KB mutated, clear cached derivations.
        Ok(id)
    }

    /// Assert a fact with a pre-assigned ID. Used for replay from persistent store.
    /// Advances the internal counter past the given ID.
    pub fn assert_fact_with_id(
        &self,
        logic: LogicBuffer,
        label: String,
        id: u64,
    ) -> Result<(), String> {
        let mut inner = self.inner.borrow_mut();
        if id >= inner.fact_counter {
            inner.fact_counter = id + 1;
        }
        // Attribute any rule compiled during this replay to THIS fact in
        // rule_source_map (otherwise a later retract of a replayed rule-producing
        // fact leaves a stale rule behind).
        inner.current_assertion_id = Some(id);
        let result = process_assertion(&mut inner, &logic);
        inner.current_assertion_id = None;
        if let Err(e) = result {
            let rb = Self::rebuild_inner(&mut inner);
            invalidate_pred_cache(&inner);
            return match rb {
                Ok(()) => Err(e),
                Err(re) => Err(format!("{e} (additionally, rollback failed: {re})")),
            };
        }
        inner.fact_registry.insert(
            id,
            FactRecord {
                id,
                buffer: logic,
                label,
                retracted: false,
            },
        );
        invalidate_pred_cache(&inner);
        Ok(())
    }

    /// Retract a previously asserted fact by its ID: mark the registry record
    /// retracted, then rebuild from the surviving records.
    ///
    /// There USED to be an "incremental O(1)" branch here for flat skolem-free
    /// ground facts. It was retired (2026-08-01, the numbers-join-the-domain
    /// adversarial review): it was never O(1) — preserving fact multiplicity
    /// already walked every surviving record — and it could not maintain
    /// `retract ≡ never-asserted` for the QUANTIFIER DOMAIN. The noted sets
    /// (`known_entities`/`known_descriptions`/`known_numbers`) are insert-only;
    /// precise un-noting needs cross-record reference counting PLUS the witness
    /// entities minted outside record buffers (existential-import
    /// presuppositions, count extra witnesses), so a retracted flat
    /// `Adam = Bel.` left both names as quantifier-domain members and a bare
    /// `all $x: p($x).` reported a counterexample the store no longer contained
    /// (22/200 sequences diverged the moment the retraction differential gained
    /// quantified battery rows) — and a lingering NUMBER is worse, satisfying
    /// arithmetic/comparison bodies with no store backing at all. Replay
    /// re-derives every noted set exactly; `retract_diff.rs` pins the
    /// equivalence, and the rebuild is the same primitive `:accept-scoped`
    /// already trusts.
    fn retract_fact_inner(&self, id: u64) -> Result<(), String> {
        let mut inner = self.inner.borrow_mut();
        match inner.fact_registry.get_mut(&id) {
            None => return Err(format!("Fact #{} not found", id)),
            Some(r) if r.retracted => return Ok(()), // idempotent
            Some(r) => r.retracted = true,
        }
        let result = Self::rebuild_inner(&mut inner);
        invalidate_pred_cache(&inner);
        result
    }

    /// Full rebuild from non-retracted facts. Kept as fallback / consistency check.
    pub fn rebuild(&self) -> Result<(), String> {
        let mut inner = self.inner.borrow_mut();
        Self::rebuild_inner(&mut inner)
    }

    /// Rebuild the KB from all non-retracted facts.
    /// Preserves fact_registry and fact_counter; resets all derived state.
    fn rebuild_inner(inner: &mut KnowledgeBaseInner) -> Result<(), String> {
        // Preserve user-declared arg sorts (set via `set_predicate_sorts`): replay
        // only re-infers arity+source per predicate, never the sorts, so clearing
        // `predicate_registry` below would silently drop them.
        let saved_arg_sorts: Vec<(String, Vec<String>)> = inner
            .predicate_registry
            .iter()
            .filter(|(_, sig)| !sig.arg_sorts.is_empty())
            .map(|(pred, sig)| (pred.clone(), sig.arg_sorts.clone()))
            .collect();

        // Reset derived state (interner too — all interned keys become invalid)
        inner.skolem_counter = 0;
        inner.known_entities.clear();
        inner.known_event_entities.clear();
        inner.known_descriptions.clear();
        inner.known_numbers.clear();
        // The member CACHES must go with the sets they were built from, and the
        // dirty flag must be raised HERE rather than left to replay re-noting:
        // `note_entity`/`note_number` set it only on fresh insertion, so a
        // replay of ZERO surviving records (retract the last fact, then query)
        // notes nothing and a warmed cache would keep serving the
        // pre-retraction members — a quantified query then reports a
        // counterexample the store no longer contains.
        inner.typed_domain_members_cache.clear();
        inner.typed_non_event_members_cache.clear();
        inner.domain_members_dirty = true;
        inner.known_rules.clear();
        inner.skolem_fn_registry.clear();
        inner.fact_store.clear();
        inner.universal_rules.clear();
        inner.pred_dep_graph.clear();
        inner.equivalence_parent.clear();
        inner.equivalence_classes.clear();
        inner.predicate_registry.clear();
        inner.arg_position_index.clear();
        inner.rule_source_map.clear();
        inner.negative_facts.clear();
        inner.disjunctive_constraints.clear();
        // The saturated extensions are derived from the rules and facts being cleared
        // right above. Cleared HERE rather than left to the callers' pairing with
        // `invalidate_pred_cache`, because `KnowledgeBase::rebuild` is the one rebuild
        // entry point that does NOT invalidate — a stale extension surviving it would
        // answer `~p(x)` from the pre-rebuild knowledge base.
        *inner.materialized.borrow_mut() = None;

        // Collect non-retracted buffers + their ids ordered by ID (owned, to avoid
        // a borrow conflict with the mutable replay below).
        let mut entries: Vec<(&u64, &FactRecord)> = inner
            .fact_registry
            .iter()
            .filter(|(_, r)| !r.retracted)
            .collect();
        entries.sort_by_key(|(id, _)| **id);
        let ids: Vec<u64> = entries.iter().map(|(id, _)| **id).collect();
        let buffers: Vec<LogicBuffer> = entries.iter().map(|(_, r)| r.buffer.clone()).collect();

        // Replay with diagnostic output + stratification checks suppressed
        // (inner.rebuilding == true). Collect-and-continue: replay EVERY surviving
        // fact so the store stays maximally consistent, accumulating errors rather
        // than silently dropping a fact that fails to replay.
        inner.rebuilding = true;
        let mut replay_errors: Vec<(u64, String)> = Vec::new();
        for (buf, &fid) in buffers.iter().zip(ids.iter()) {
            if let Err(e) = process_assertion(inner, buf) {
                replay_errors.push((fid, e));
            }
        }
        inner.rebuilding = false;

        // Restore the preserved sorts into the re-populated registry.
        for (pred, sorts) in saved_arg_sorts {
            let arity = sorts.len();
            inner
                .predicate_registry
                .entry(pred)
                .or_insert_with(|| PredicateSignature {
                    arity,
                    source: SignatureSource::Inferred,
                    arg_sorts: Vec::new(),
                })
                .arg_sorts = sorts;
        }

        if replay_errors.is_empty() {
            Ok(())
        } else {
            let detail = replay_errors
                .iter()
                .map(|(id, e)| format!("#{id}: {e}"))
                .collect::<Vec<_>>()
                .join("; ");
            Err(format!("rebuild replay errors: {detail}"))
        }
    }

    /// List all active (non-retracted) facts in the KB.
    fn list_facts_inner(&self) -> Result<Vec<FactSummary>, String> {
        let inner = self.inner.borrow();
        let mut facts: Vec<FactSummary> = inner
            .fact_registry
            .values()
            .filter(|r| !r.retracted)
            .map(|r| FactSummary {
                id: r.id,
                label: r.label.clone(),
                root_count: r.buffer.roots.len() as u32,
            })
            .collect();
        facts.sort_by_key(|f| f.id);
        Ok(facts)
    }

    /// Set the backward-chaining depth bound (`max_chain_depth`, default 10) —
    /// the "Configurable" knob `GUARANTEES.md §Resource Limits` documents.
    /// Iterative deepening tries 1..=depth; a query whose shallowest proof needs a
    /// longer chain returns `ResourceExceeded(Depth)`, never FALSE. Practical note:
    /// deepening cost grows steeply with depth (each level re-explores the shallower
    /// search — measured ~15×+ per level on linear rule chains), so the bound is a
    /// soundness/termination contract, not a performance envelope. Values below 1
    /// are clamped to 1.
    pub fn set_max_chain_depth(&self, depth: usize) {
        self.inner.borrow_mut().max_chain_depth = depth.max(1);
    }

    /// Saturate the relations this query will read under `~`, so the NAF checks below
    /// are set-membership tests instead of exhaustive proof attempts.
    ///
    /// Called ONCE per query, before the iterative-deepening loop — the extension does
    /// not depend on the depth budget, so re-deriving it per pass would be pure waste.
    /// Everything here is best-effort: a relation that cannot be saturated is simply
    /// absent from the completed set, and its NAF takes the ordinary path.
    ///
    /// TARGETS. The relations read under `~`: those under a `NotNode` in the query
    /// buffer, plus the negated conditions and `~` restrictor groups of every
    /// registered rule. Rule-body NAF is included unconditionally rather than by
    /// reachability from the query's head, because backward chaining reaches rules
    /// through the fact store and the equality fallback as well as through the
    /// dependency graph — an under-approximated target set would silently lose the
    /// optimisation, and the saturation is scoped by the dependency closure anyway.
    fn ensure_materialized(&self, logic: &LogicBuffer) {
        let inner = self.inner.borrow();
        if !inner.materialization || inner.materialized.borrow().is_some() {
            return;
        }
        let elig = materialize::eligible_relations(&inner);
        // TARGETS. Every relation the saturator is ALLOWED to complete, not just the ones
        // read under `~`: since the positive probe in `check_formula_holds_core`'s
        // `ExistsNode` arm, a completed extension answers ordinary queries too, so
        // restricting the target set to the NAF cone would leave the positive fast path
        // permanently cold. `saturate` still scopes the actual work to the dependency
        // closure of these, and `eligible_relations` has already refused everything it
        // cannot project — so widening here cannot admit an unsound relation, only more
        // sound ones.
        //
        // The `~`-read relations are unioned in explicitly because a NAF target may be
        // pure EDB (no rule concludes it, so it is not an `eligible` key) and still needs
        // to be marked complete from its seed — that is the common `~rotten(x)` case.
        let mut targets: HashSet<String> = elig.eligible.iter().cloned().collect();
        materialize::collect_negated_relations(logic, &mut targets);
        for rule in materialize::distinct_rules(&inner) {
            for (i, c) in rule.typed_conditions.iter().enumerate() {
                if rule.negated_condition_indices.contains(&i) {
                    targets.insert(materialize::surface_relation(c.relation()).to_string());
                }
            }
            for g in &rule.negated_exists_groups {
                for c in &g.conditions {
                    targets.insert(materialize::surface_relation(c.relation()).to_string());
                }
            }
        }
        // The query's own relations: a positive query over a saturable relation should hit
        // the fast path even when nothing in the KB negates anything.
        materialize::collect_query_relations(logic, &mut targets);
        if targets.is_empty() {
            *inner.materialized.borrow_mut() = Some(materialize::Materialized::empty());
            return;
        }
        let strata = materialize::compute_strata(&inner.pred_dep_graph);
        let m = materialize::saturate(&inner, &elig, &strata, &targets);
        *inner.materialized.borrow_mut() = Some(m);
    }

    /// Single-pass entailment check at the current max_chain_depth.
    fn run_entailment_check(&self, logic: &LogicBuffer) -> Result<QueryResult, String> {
        // Enable WITHOUT clearing: the cache is cleared once before the
        // iterative-deepening loop in query_entailment_inner, then definitive
        // results persist across depth passes (cross-depth tabling).
        let mut inner = self.inner.borrow_mut();
        enable_pred_cache(&inner);
        inner.ensure_domain_members_cached();
        let mut overall = QueryResult::True;
        for &root_id in &logic.roots {
            let mut subs = HashMap::new();
            let result = check_formula_holds(logic, root_id, &mut subs, &mut inner, None)?;
            overall = Self::combine_root_results(overall, result);
        }
        Ok(overall)
    }

    /// Check whether all root formulas in the logic buffer are entailed by the KB.
    /// Uses iterative deepening: tries depth 1, 2, ..., max_chain_depth.
    /// Guarantees finding the shallowest proof.
    fn query_entailment_inner(&self, logic: LogicBuffer) -> Result<QueryResult, String> {
        // Tabling: clear once, persist across depth iterations.
        self.ensure_materialized(&logic);
        let configured_max = {
            let inner = self.inner.borrow();
            clear_and_enable_pred_cache(&inner);
            inner.max_chain_depth
        };
        for depth_limit in 1..=configured_max {
            self.inner.borrow_mut().max_chain_depth = depth_limit;
            // Restore the configured depth on EVERY exit, including the error
            // path (e.g. cooperative cancellation), so an aborted query never
            // leaves a reusable KB pinned at a partial deepening depth.
            let result = match self.run_entailment_check(&logic) {
                Ok(result) => result,
                Err(e) => {
                    self.inner.borrow_mut().max_chain_depth = configured_max;
                    return Err(e);
                }
            };
            if !matches!(result, QueryResult::ResourceExceeded(ResourceKind::Depth)) {
                self.inner.borrow_mut().max_chain_depth = configured_max;
                return Ok(result);
            }
        }
        self.inner.borrow_mut().max_chain_depth = configured_max;
        Ok(QueryResult::ResourceExceeded(ResourceKind::Depth))
    }

    /// Find all satisfying binding sets for existential variables in the query formula.
    /// Returns one `Vec<WitnessBinding>` per satisfying assignment.
    fn query_find_inner(&self, logic: LogicBuffer) -> Result<Vec<Vec<WitnessBinding>>, String> {
        // Surfaced (as an Err) when witness enumeration is CUT at the depth/cycle
        // horizon: find/count/aggregate must refuse a definitive (under)count rather
        // than silently report a wrong quantity. See `find_witnesses` /
        // `find_horizon_hit` — this is the find-path analog of the entailment path's
        // `ResourceExceeded(Depth)` verdict.
        //
        // WHAT THIS MEANS SINCE STRATUM-ORDERED MATERIALISATION. A saturated relation
        // returns only definitive verdicts, so `witness_search_cut` never fires for a
        // leaf inside the materialised fragment and this refusal never triggers there —
        // no code change was needed for that, it falls out. What remains is the genuine
        // residue: compute predicates (an infinite numeric domain, not a finite set to
        // saturate) and any relation the eligibility analysis refused. So the refusal
        // stopped meaning "your search was too deep" and now means "this query reached
        // the fragment the engine cannot complete" — and the advice changed with it,
        // because raising the depth limit does nothing for an unsaturable relation.
        // `KnowledgeBase::materialization_report` names which relations those are.
        const INCOMPLETE_MSG: &str = "witness enumeration incomplete: a witness leaf could not be decided \
             (a compute predicate, or a relation outside the materialised fragment), so \
             find/count/aggregate would undercount — run `:materialize` (or call \
             `materialization_report`) to see which relations were not saturated and why; \
             raising the depth limit helps only for a relation the engine falls back to \
             backward chaining on";
        self.ensure_materialized(&logic);
        let mut inner = self.inner.borrow_mut();
        clear_and_enable_pred_cache(&inner);
        inner.ensure_domain_members_cached();
        inner.find_horizon_hit = false;
        let mut result_sets: Option<Vec<Vec<(String, GroundTerm)>>> = None;
        for &root_id in &logic.roots {
            let mut subs = HashMap::new();
            let witnesses = find_witnesses(&logic, root_id, &mut subs, &mut inner, None)?;
            match result_sets {
                None => result_sets = Some(witnesses),
                Some(prev) => {
                    if witnesses.is_empty() {
                        if inner.find_horizon_hit {
                            return Err(INCOMPLETE_MSG.to_string());
                        }
                        return Ok(vec![]);
                    }
                    // Join binding sets across roots: shared variables must agree,
                    // and fresh variables from later roots are preserved.
                    let mut joined = Vec::new();
                    for prev_bindings in prev {
                        for witness_bindings in &witnesses {
                            if let Some(combined) =
                                merge_witness_bindings(&prev_bindings, witness_bindings)
                            {
                                joined.push(combined);
                            }
                        }
                    }
                    if joined.is_empty() {
                        if inner.find_horizon_hit {
                            return Err(INCOMPLETE_MSG.to_string());
                        }
                        return Ok(vec![]);
                    }
                    result_sets = Some(joined);
                }
            }
        }
        // Enumeration finished — but if any witness leaf was cut at the depth/cycle
        // horizon, the result is an under-count, not a definitive one. Refuse it.
        if inner.find_horizon_hit {
            return Err(INCOMPLETE_MSG.to_string());
        }
        let mut binding_sets = result_sets.unwrap_or_default();
        // Determinism + dedup: witness enumeration touches HashSet-backed
        // candidate collections, so the order binding sets arrive in is
        // hasher-seed dependent, and the SAME solution can arrive via distinct
        // candidates (an Or-overlap where one entity satisfies both disjuncts,
        // equivalence-class expansion, or the shared entailment/find candidate
        // superset). Sort the outer list by each set's canonical key (its
        // sorted (var, term) pairs) so `[Find]` output is byte-reproducible
        // across runs and processes, THEN drop adjacent canonical duplicates so
        // `count_witnesses`/`aggregate` count each distinct binding exactly once
        // (an inflated count would be a hallucinated quantity). Comparison is at
        // GroundTerm level — distinct terms never collapse; intra-set binding
        // order (structural, inner-to-outer) is preserved for display.
        // ENTITY-LEVEL identity (GUARANTEES §Aggregation): tuples binding an
        // ENTITY variable to a existential-import presupposition witness are dropped
        // entirely — a phantom entity a rule presupposed satisfies ∃/∀ but is
        // not an enumerable "thing". Entity variables = everything except the
        // `_ev*` EVENT vars (description vars `_v{n}` carry answer entities).
        binding_sets.retain(|bindings| {
            !bindings.iter().any(|(var, gt)| {
                !var.starts_with("_ev")
                    && matches!(gt, GroundTerm::Constant(name)
                        if inner.presupposition_witnesses.contains(name.as_str()))
            })
        });
        // The DEDUP key is the binding set projected onto ENTITY variables —
        // `_ev*` event vars are derivation bookkeeping and must not multiply
        // results (pre-change, one dog answered `?? da gerku` once per
        // derivation event) — with each term du-CANONICALIZED so two names for
        // one entity count once. The sort key appends the full raw key so the
        // total order — and therefore WHICH tuple survives dedup — stays
        // byte-reproducible regardless of hasher-seed-dependent arrival order;
        // the survivor's display terms are real asserted names, not
        // canonicalized rewrites.
        let entity_key = |bindings: &Vec<(String, GroundTerm)>| {
            let mut key: Vec<(String, GroundTerm)> = bindings
                .iter()
                .filter(|(var, _)| !var.starts_with("_ev"))
                .map(|(var, gt)| {
                    (
                        var.clone(),
                        find_canonical_readonly(&inner.equivalence_parent, gt),
                    )
                })
                .collect();
            key.sort();
            key
        };
        let full_key = |bindings: &Vec<(String, GroundTerm)>| {
            let mut key = bindings.clone();
            key.sort();
            key
        };
        binding_sets.sort_by_cached_key(|b| (entity_key(b), full_key(b)));
        binding_sets.dedup_by_key(|bindings| entity_key(bindings));
        Ok(binding_sets
            .into_iter()
            .map(|bindings| {
                bindings
                    .into_iter()
                    .map(|(var, gt)| WitnessBinding {
                        variable: var,
                        term: witness_term_to_logical_term(&gt),
                    })
                    .collect()
            })
            .collect())
    }

    /// Single-pass entailment check with proof trace at the current max_chain_depth.
    fn run_entailment_check_with_proof(
        &self,
        logic: &LogicBuffer,
    ) -> Result<(QueryResult, ProofTrace), String> {
        // Enable WITHOUT clearing: cleared once before the iterative-deepening
        // loop in query_entailment_with_proof_inner; definitive results persist
        // across depth passes (cross-depth tabling).
        let mut inner = self.inner.borrow_mut();
        enable_pred_cache(&inner);
        inner.ensure_domain_members_cached();
        let mut steps: Vec<ProofStep> = Vec::new();
        let mut memo: HashMap<String, u32> = HashMap::new();
        let mut root_children: Vec<u32> = Vec::new();
        let mut overall = QueryResult::True;
        for &root_id in &logic.roots {
            let mut subs = HashMap::new();
            // ONE walk per root: the recording evaluator returns the authoritative
            // four-valued verdict AND builds the proof trace, so the trace's
            // per-node `holds` is natively `verdict.is_true()` — no separate
            // untraced pass and no root `holds` reconciliation needed.
            let (result, step_idx) = check_formula_holds_recording(
                logic, root_id, &mut subs, &mut inner, &mut steps, None, &mut memo,
            )?;
            overall = Self::combine_root_results(overall, result);
            root_children.push(step_idx);
        }
        let root = if root_children.len() == 1 {
            root_children[0]
        } else {
            let idx = steps.len() as u32;
            steps.push(ProofStep {
                rule: ProofRule::Conjunction,
                holds: overall.is_true(),
                children: root_children,
            });
            idx
        };
        let naf_dependent = steps
            .iter()
            .any(|s| matches!(s.rule, ProofRule::Negation) && s.holds);
        // A FALSE verdict is closed-world ("not derivable from the KB") UNLESS a
        // numeric/arithmetic compute DECIDED it (e.g. `5 dunli 3` is genuinely false).
        // The dual of `naf_dependent`: under open-world semantics it would be Unknown.
        let cwa_false = overall.is_false()
            && !steps.iter().any(|s| {
                !s.holds
                    && matches!(
                        &s.rule,
                        ProofRule::ComputeCheck { method, .. }
                            if method == "numeric" || method == "arithmetic"
                    )
            });
        Ok((
            overall,
            ProofTrace {
                steps,
                root,
                naf_dependent,
                cwa_false,
            },
        ))
    }

    /// Check entailment with proof trace using iterative deepening.
    fn query_entailment_with_proof_inner(
        &self,
        logic: LogicBuffer,
    ) -> Result<(QueryResult, ProofTrace), String> {
        // Same saturation the untraced path uses — the NAF probe stays on, and its trace
        // shape is unaffected (`emit_derived` records a `Negation` leaf per group without
        // re-evaluating it, so `naf_dependent` still computes correctly).
        self.ensure_materialized(&logic);
        // The POSITIVE lookup, however, is lowered for the whole traced query — BOTH
        // phases. A lookup has no derivation to record, and gating it per-sink would let
        // the untraced phase-1 probe resolve at depth 1 while phase 2 rebuilt the trace by
        // backward chaining at that same depth and failed to reach it, turning a TRUE into
        // `ResourceExceeded(Depth)`. Restored on every exit below, error paths included.
        self.inner.borrow().positive_lookup.set(false);
        // Tabling: clear once, persist across phases.
        let configured_max = {
            let inner = self.inner.borrow();
            clear_and_enable_pred_cache(&inner);
            inner.max_chain_depth
        };
        // Phase 1: find the resolving depth with the CHEAP untraced walk — no proof
        // trace is built (then discarded) on the probe passes. The costly part of a
        // proof query is the ProofStep-tree construction, which (unlike the verdict,
        // which the predicate cache amortizes across depths) is NOT cross-depth-
        // cached, so the old per-depth loop rebuilt D-1 partial traces only to throw
        // them away. If no depth resolves, `resolving_depth` stays `configured_max`
        // so Phase 2 builds the deepest trace (matching the old `last_trace`).
        let mut resolving_depth = configured_max;
        for depth_limit in 1..=configured_max {
            self.inner.borrow_mut().max_chain_depth = depth_limit;
            // Restore the configured depth on the error path too (see
            // query_entailment_inner) — explicit `match`, NOT `?`, so a cancelled
            // query never leaves the KB pinned at a partial deepening depth.
            let result = match self.run_entailment_check(&logic) {
                Ok(r) => r,
                Err(e) => {
                    let inner = self.inner.borrow();
                    inner.positive_lookup.set(true);
                    drop(inner);
                    self.inner.borrow_mut().max_chain_depth = configured_max;
                    return Err(e);
                }
            };
            if !matches!(result, QueryResult::ResourceExceeded(ResourceKind::Depth)) {
                resolving_depth = depth_limit;
                break;
            }
        }
        // Phase 2: build the proof trace ONCE at the resolving depth. The predicate
        // cache (warmed by Phase 1) makes this build's verdict sub-checks cheap; the
        // trace is byte-identical to the former per-depth build because the trace
        // descent never shortcuts on the verdict cache and the fact store is
        // set-idempotent for the only state it reads (`typed_fact_is_asserted`).
        self.inner.borrow_mut().max_chain_depth = resolving_depth;
        let out = self.run_entailment_check_with_proof(&logic);
        {
            let inner = self.inner.borrow();
            inner.positive_lookup.set(true);
        }
        self.inner.borrow_mut().max_chain_depth = configured_max;
        out
    }
}

fn merge_witness_bindings(
    left: &[(String, GroundTerm)],
    right: &[(String, GroundTerm)],
) -> Option<Vec<(String, GroundTerm)>> {
    let mut combined = left.to_vec();
    for (var, val) in right {
        match combined
            .iter()
            .find(|(existing_var, _)| existing_var == var)
        {
            Some((_, existing_val)) if existing_val != val => return None,
            Some(_) => {}
            None => combined.push((var.clone(), val.clone())),
        }
    }
    Some(combined)
}

/// Public API for native callers (nibli-pipeline, nibli-engine).
/// Uses nibli-semantics's logic types directly — no bridge conversion needed.
impl KnowledgeBase {
    /// Create a new knowledge base with the default in-memory fact store.
    pub fn new() -> Self {
        KnowledgeBase {
            inner: RefCell::new(KnowledgeBaseInner::new()),
        }
    }

    /// Create a KB with a custom fact store backend (e.g., persistent redb).
    pub fn with_store(store: Box<dyn fact_store::FactStore>) -> Self {
        let mut inner = KnowledgeBaseInner::new();
        inner.fact_store = store;
        KnowledgeBase {
            inner: RefCell::new(inner),
        }
    }

    /// Install a cooperative cancellation flag. When the flag is set to `true`,
    /// the next central reasoning checkpoint aborts the in-flight query via the
    /// `Err` channel (the verdict variants are untouched). The native nibli-server
    /// watchdog sets the flag when a request's wall-clock budget elapses, freeing
    /// the blocking thread instead of letting a pathological query run to
    /// completion. No clock is read inside the engine, so the WASI sandbox
    /// guarantee is preserved; nibli-host/nibli-pipeline never install a flag.
    pub fn set_cancel_flag(&self, flag: std::sync::Arc<std::sync::atomic::AtomicBool>) {
        self.inner.borrow_mut().cancel = Some(flag);
    }

    /// Remove any installed cancellation flag (queries run unbounded again).
    pub fn clear_cancel_flag(&self) {
        self.inner.borrow_mut().cancel = None;
    }

    /// Enable/disable informational stdout diagnostics (`[Rule]`/`[Skolem]`/
    /// `[Constraint] Registered`). Default OFF — a silent library; the
    /// server/validate/tavla stay quiet. nibli-pipeline (the nibli-host REPL) and the native
    /// `nibli` REPL opt in. Configuration, not derived state — survives `reset()`.
    pub fn set_verbose(&self, verbose: bool) {
        self.inner.borrow_mut().verbose = verbose;
    }

    /// Whether diagnostic verbosity is enabled.
    pub fn is_verbose(&self) -> bool {
        self.inner.borrow().verbose
    }

    /// Enable/disable STRICT MODE (default OFF — permissive warn-and-insert,
    /// the documented v1 behavior). When on, an arity mismatch or an
    /// integrity-constraint violation REJECTS the offending fact and fails the
    /// assertion (`Err`) ATOMICALLY — the failed assertion's partial mutations
    /// are rolled back via the registry rebuild, exactly like any other
    /// assertion error. Facts inserted internally (forward chaining, compute
    /// auto-assert) are also rejected loudly but cannot fail a user call.
    /// Configuration, not derived state — survives `reset()`; inert during
    /// retraction-replay rebuilds.
    pub fn set_strict(&self, strict: bool) {
        self.inner.borrow_mut().strict = strict;
    }

    /// Whether strict mode is enabled.
    pub fn is_strict(&self) -> bool {
        self.inner.borrow().strict
    }

    /// Enable/disable EXISTENTIAL-IMPORT MODE (default ON — the v0.1 xorlo
    /// behavior, kept byte-identical). When on, a description universal
    /// (`animal(every dog).`) mints a presupposition witness so `∃x. dog(x)`
    /// holds. Set OFF for the clean-core profile (`some` = plain classical ∃,
    /// no phantom entity injected — NIBLI_KR §14.4 item 3). Configuration, not
    /// derived state — survives `reset()`.
    pub fn set_existential_import(&self, on: bool) {
        self.inner.borrow_mut().existential_import = on;
    }

    /// Whether existential-import (xorlo witness minting) is enabled.
    pub fn is_existential_import(&self) -> bool {
        self.inner.borrow().existential_import
    }

    /// Enable/disable STRATUM-ORDERED MATERIALISATION (default ON — see
    /// [`crate::materialize`]). When on, the relations a query reads under `~` are
    /// saturated bottom-up in stratum order before the query runs, and each NAF check
    /// becomes a set-membership test instead of an exhaustive proof attempt. When off,
    /// every NAF takes the backward-chaining path — byte-identical to the pre-2026-07-31
    /// engine, which is what the ON/OFF differential in `nibli-verify` compares against.
    ///
    /// Configuration, not derived state — survives `reset()`. Turning it OFF drops any
    /// existing saturation immediately, so the switch takes effect on the next query
    /// rather than at the next mutation.
    pub fn set_materialization(&self, on: bool) {
        let mut inner = self.inner.borrow_mut();
        inner.materialization = on;
        *inner.materialized.borrow_mut() = None;
    }

    /// Whether stratum-ordered materialisation is enabled.
    pub fn is_materialization(&self) -> bool {
        self.inner.borrow().materialization
    }

    /// What the last query's saturation actually covered: `(completed relations, why
    /// each refused relation was not)`, both sorted for reproducible output.
    ///
    /// This exists because the optimisation is INVISIBLE when it fails. A knowledge base
    /// whose `~p(x)` still takes seconds has no other way to learn that `p` fell out of
    /// the materialisable fragment, or which of its dependencies did. Empty until a
    /// query has run (the saturation is built lazily) and after any mutation.
    pub fn materialization_report(&self) -> (Vec<String>, Vec<(String, String)>) {
        let inner = self.inner.borrow();
        let m = inner.materialized.borrow();
        let Some(m) = m.as_ref() else {
            return (Vec::new(), Vec::new());
        };
        let mut complete: Vec<String> = m.complete.iter().cloned().collect();
        complete.sort();
        let mut refused: Vec<(String, String)> = m
            .refused
            .iter()
            .filter(|(rel, _)| !m.complete.contains(*rel))
            .map(|(rel, why)| (rel.clone(), why.reason()))
            .collect();
        refused.sort();
        (complete, refused)
    }

    /// The KB's STRATIFICATION as machine-readable data: every predicate with its
    /// stratum, whether it is base (EDB) or derived (IDB), and its outgoing dependency
    /// edges marked positive or negative.
    ///
    /// Exists so a consuming project does not have to re-implement the stratifier to
    /// read it. A second implementation — a regex over `.nibli` text, say — is a second
    /// thing to keep in sync with this one, and it will drift; anything presented as
    /// *"this order was derived by the engine"* has to come from the engine that
    /// enforces it. Read-only and verdict-inert: it reports `pred_dep_graph`, which
    /// `register_rule` already maintains and `check_stratification` already gates.
    ///
    /// **Surface projection.** The graph the engine stratifies is keyed on
    /// event-decomposed relation names — the anchor `false` alongside its role
    /// predicates `false_x1`, `false_x2`. Those are one atom, so they always carry
    /// identical dependency sets and therefore always land in the same stratum
    /// (pinned by `strata_surface_projection_is_lossless`). The report collapses each
    /// role onto its anchor, because that is the name a KB author wrote and the only
    /// name a reader can check. A self-edge that survives the collapse is GENUINE
    /// recursion, not a decomposition artifact: a rule never reads the roles of its own
    /// conclusion, so `p -> p_x1` edges do not exist to begin with.
    ///
    /// Deterministic by construction: rows sorted by predicate, edges sorted, duplicates
    /// (four raw edges collapsing onto one surface edge) removed — safe to diff across
    /// runs.
    pub fn stratification_report(&self) -> Vec<StratumRow> {
        use std::collections::{BTreeMap, BTreeSet};

        let inner = self.inner.borrow();
        let strata = materialize::compute_strata(&inner.pred_dep_graph);

        // Anything a rule concludes is DERIVED, whatever else is true of it. Keyed on the
        // raw conclusion relation, so project it the same way as the nodes.
        let derived: BTreeSet<&str> = inner
            .universal_rules
            .keys()
            .map(|k| materialize::surface_relation(k))
            .collect();

        let mut level: BTreeMap<&str, usize> = BTreeMap::new();
        for (raw, lvl) in &strata {
            let surface = materialize::surface_relation(raw);
            // `max` is defensive only — see the lossless-projection pin above.
            let slot = level.entry(surface).or_insert(*lvl);
            *slot = (*slot).max(*lvl);
        }
        // `pred_dep_graph`'s keys are a STRICT SUBSET of the rule heads: a conditionless
        // rule pushes no edges, so its head never becomes a node. Such a head is still a
        // derived predicate and must appear, at stratum 0 — it depends on nothing, so
        // nothing can raise it. Omitting it would drop a whole predicate from a dump whose
        // purpose is to be complete.
        for head in derived.iter() {
            level.entry(head).or_insert(0);
        }

        let mut edges: BTreeMap<&str, BTreeSet<(&str, bool)>> = BTreeMap::new();
        for (head, deps) in &inner.pred_dep_graph {
            let h = materialize::surface_relation(head);
            let bucket = edges.entry(h).or_default();
            for (dep, is_neg) in deps {
                bucket.insert((materialize::surface_relation(dep), *is_neg));
            }
        }

        level
            .into_iter()
            .map(|(predicate, stratum)| StratumRow {
                stratum,
                base: !derived.contains(predicate),
                edges: edges
                    .get(predicate)
                    .map(|s| {
                        s.iter()
                            .map(|(to, negative)| StratumEdge {
                                to: (*to).to_string(),
                                negative: *negative,
                            })
                            .collect()
                    })
                    .unwrap_or_default(),
                predicate: predicate.to_string(),
            })
            .collect()
    }

    /// Declare `relation` DERIVED-ONLY (intensional / IDB): thereafter it may be
    /// concluded by a rule but never asserted directly — a direct ground
    /// assertion is rejected and the whole assertion unwinds atomically.
    ///
    /// The KB-level spelling is `derived_only("<relation>").`, which routes here;
    /// this is the programmatic twin. Declaring is IDEMPOTENT and one-way within
    /// a session: there is deliberately no `undeclare`, since a relation that
    /// could be re-opened at runtime would give back exactly the capability the
    /// declaration exists to remove. Reopen it by editing the KB.
    ///
    /// Declaring does NOT retroactively remove facts already asserted, and it is
    /// a DECLARATION, not derived state — it survives `reset()` and retraction
    /// replay.
    pub fn declare_derived(&self, relation: &str) {
        self.inner
            .borrow_mut()
            .derived_only
            .insert(relation.to_string());
    }

    /// Declare `relation` ADMITTED base vocabulary. The FIRST such declaration
    /// CLOSES this knowledge base's vocabulary: thereafter a ground assertion of
    /// any relation not admitted is rejected, atomically, the way `derived_only`
    /// rejects. While nothing has been declared the KB is OPEN, which is the
    /// default and what every v0.1 knowledge base gets.
    ///
    /// The KB-level spelling is `admits("<relation>").`; this is the programmatic
    /// twin. It is the DUAL of [`Self::declare_derived`] — that one says a relation
    /// may not be asserted, this one says which relations may — and the pair
    /// together is what lets a document claim its record has exactly these entries
    /// and have the engine hold it to that.
    ///
    /// ORDER IS LOAD-BEARING and enforced: the whole admits block must precede
    /// every ordinary assertion, because a declaration that arrives later would
    /// silently grandfather everything above it. Declaring is idempotent and
    /// one-way within a session, for the same reason `declare_derived` is: a
    /// vocabulary that could be re-opened at runtime gives back exactly the
    /// capability the declaration exists to remove.
    pub fn declare_admitted(&self, relation: &str) {
        self.inner
            .borrow_mut()
            .admitted
            .insert(relation.to_string());
    }

    /// Whether `relation` is admitted base vocabulary. Note an OPEN knowledge base
    /// (nothing declared) returns `false` for everything while still admitting
    /// everything — ask [`Self::vocabulary_is_closed`] first.
    pub fn is_admitted(&self, relation: &str) -> bool {
        self.inner.borrow().admitted.contains(relation)
    }

    /// Whether this KB has closed its vocabulary at all.
    pub fn vocabulary_is_closed(&self) -> bool {
        !self.inner.borrow().admitted.is_empty()
    }

    /// The admitted base vocabulary, sorted. Empty when the KB is open.
    pub fn admitted_relations(&self) -> Vec<String> {
        let mut v: Vec<String> = self.inner.borrow().admitted.iter().cloned().collect();
        v.sort();
        v
    }

    /// Whether `relation` is declared derived-only.
    pub fn is_derived_only(&self, relation: &str) -> bool {
        self.inner.borrow().derived_only.contains(relation)
    }

    /// Every relation declared derived-only, sorted — the KB's closure list, for
    /// tests and for surfaces that want to show it.
    pub fn derived_only_relations(&self) -> Vec<String> {
        let mut v: Vec<String> = self.inner.borrow().derived_only.iter().cloned().collect();
        v.sort();
        v
    }

    /// Register this KB's external compute dispatch (per-instance — replaces the
    /// old thread-local `register_compute_dispatch`, which the multithreaded
    /// server could never register because each tokio blocking-pool worker had
    /// its own `None` thread-local). Built-in arithmetic (pilji/sumji/dilcu) is
    /// always evaluated locally; everything else is forwarded to `eval`/
    /// `batch_eval`.
    ///
    /// TRUST BOUNDARY: a `true` reply is auto-asserted as a ground fact mid-query
    /// that downstream universal rules can chain on, so a malicious or MITM
    /// backend can seed arbitrary predicates. The backend is part of the trusted
    /// computing base — run it on localhost or a network segment you control.
    /// (Auto-asserted compute facts are non-durable: no FactRecord, never
    /// replayed by rebuild.)
    pub fn set_compute_dispatch(
        &self,
        eval: crate::compute::EvalFn,
        batch_eval: crate::compute::BatchEvalFn,
    ) {
        let mut inner = self.inner.borrow_mut();
        inner.compute_eval = Some(eval);
        inner.compute_batch_eval = Some(batch_eval);
    }

    /// Assert a compiled FOL formula into the knowledge base. Returns the fact ID.
    pub fn assert_fact(&self, logic: LogicBuffer, label: String) -> Result<u64, NibliError> {
        // The assert IS the reasoning stage: by the time this runs the buffer has
        // already passed nibli-semantics, so every failure here (stratification, fail-closed
        // rule compilation, the zero-ingest guard, rebuild replay) is reasoning-layer.
        // The layer contract is Syntax=nibli-kr / Semantic=nibli-semantics / Reasoning=nibli-reason.
        self.assert_fact_inner(logic, label)
            .map_err(NibliError::Reasoning)
    }

    /// Run a query under temporary assumptions without mutating the real KB.
    /// Clones the KB, asserts all assumptions into the clone, runs the callback,
    /// and discards the clone. The original KB is untouched.
    ///
    /// Supports multiple independent hypotheticals (each gets its own snapshot)
    /// and nesting (the callback receives a `&KnowledgeBase` with `with_assumptions`).
    pub fn with_assumptions<F, R>(&self, assumptions: &[LogicBuffer], f: F) -> Result<R, NibliError>
    where
        F: FnOnce(&KnowledgeBase) -> R,
    {
        let snapshot = self.inner.borrow().clone();
        let temp_kb = KnowledgeBase {
            inner: RefCell::new(snapshot),
        };
        for buf in assumptions {
            temp_kb.assert_fact(buf.clone(), "assumption".into())?;
        }
        Ok(f(&temp_kb))
    }

    /// Register an integrity constraint: a set of facts that must NOT all hold simultaneously.
    /// Checked after every fact insertion (permissive mode: warns on violation).
    pub fn register_constraint(&self, label: String, conjuncts: Vec<kb::StoredFact>) {
        let predicates: Vec<String> = conjuncts.iter().map(|c| c.relation().to_string()).collect();
        let mut inner = self.inner.borrow_mut();
        inner.integrity_constraints.push(kb::IntegrityConstraint {
            label,
            conjuncts,
            predicates,
        });
    }

    /// Check whether a formula is entailed by the knowledge base (four-valued result).
    pub fn query_entailment(&self, logic: LogicBuffer) -> Result<QueryResult, NibliError> {
        self.query_entailment_inner(logic)
            .map_err(NibliError::Reasoning)
    }

    /// Find all satisfying witness binding sets for existential variables in the formula.
    pub fn query_find(&self, logic: LogicBuffer) -> Result<Vec<Vec<WitnessBinding>>, NibliError> {
        self.query_find_inner(logic).map_err(NibliError::Reasoning)
    }

    /// Count the number of distinct witness binding sets satisfying the formula.
    pub fn count_witnesses(&self, logic: LogicBuffer) -> Result<usize, NibliError> {
        self.query_find(logic).map(|bindings| bindings.len())
    }

    /// Aggregate numeric values of a named variable across all witness binding sets.
    /// Returns `None` if no numeric witnesses found for the variable.
    pub fn aggregate(
        &self,
        logic: LogicBuffer,
        variable: &str,
        op: nibli_types::logic::AggregateOp,
    ) -> Result<Option<f64>, NibliError> {
        let bindings = self.query_find(logic)?;
        let values: Vec<f64> = bindings
            .iter()
            .filter_map(|binding_set| {
                binding_set
                    .iter()
                    .find(|b| b.variable == variable)
                    .and_then(|b| match &b.term {
                        LogicalTerm::Number(n) => Some(*n),
                        _ => None,
                    })
            })
            .collect();
        if values.is_empty() {
            return Ok(None);
        }
        use nibli_types::logic::AggregateOp;
        let result = match op {
            AggregateOp::Sum => values.iter().sum(),
            AggregateOp::Min => values.iter().cloned().reduce(f64::min).unwrap_or(0.0),
            AggregateOp::Max => values.iter().cloned().reduce(f64::max).unwrap_or(0.0),
            AggregateOp::Avg => values.iter().sum::<f64>() / values.len() as f64,
        };
        Ok(Some(result))
    }

    /// Check entailment and return a proof trace showing the full derivation chain.
    pub fn query_entailment_with_proof(
        &self,
        logic: LogicBuffer,
    ) -> Result<(QueryResult, ProofTrace), NibliError> {
        self.query_entailment_with_proof_inner(logic)
            .map_err(NibliError::Reasoning)
    }

    /// Clear all facts, rules, indexes, and derived state.
    pub fn reset(&self) -> Result<(), NibliError> {
        let mut inner = self.inner.borrow_mut();
        inner.reset();
        invalidate_pred_cache(&inner); // Tabling: KB cleared.
        Ok(())
    }

    /// Retract a fact by ID. Uses incremental removal for ground facts,
    /// full rebuild for facts that compiled into rules.
    pub fn retract_fact(&self, id: u64) -> Result<(), NibliError> {
        self.retract_fact_inner(id).map_err(NibliError::Reasoning)
    }

    /// List all active (non-retracted) facts with their IDs and labels.
    pub fn list_facts(&self) -> Result<Vec<FactSummary>, NibliError> {
        self.list_facts_inner().map_err(NibliError::Reasoning)
    }

    /// Mark all rules concluding the given predicate as forward-chaining enabled.
    /// Forward-enabled rules fire eagerly on fact assertion when all conditions
    /// are directly asserted in the fact store.
    ///
    /// FAIL CLOSED: a rule with a negation-as-failure condition (a flat negated
    /// condition or a `poi na <predicate>` group) is NOT forward-enabled — it stays
    /// backward-only, where it is sound (backward chaining re-evaluates `¬Q` at
    /// query time). Forward chaining + NAF has no truth maintenance: a
    /// forward-derived conclusion would never be retracted when a later assertion
    /// makes the negated dependency true. Positive (negation-free) rules enable
    /// normally; `forward = false` (disabling) always applies.
    pub fn set_rule_forward(&self, conclusion_predicate: &str, forward: bool) {
        let mut inner = self.inner.borrow_mut();
        let rebuilding = inner.rebuilding;
        if let Some(rules) = inner.universal_rules.get_mut(conclusion_predicate) {
            for rule in rules.iter_mut() {
                if forward
                    && (!rule.negated_condition_indices.is_empty()
                        || !rule.negated_exists_groups.is_empty())
                {
                    if !rebuilding {
                        eprintln!(
                            "[Forward] rule '{}' has a negation-as-failure condition; \
                             keeping it backward-only (forward chaining + NAF has no \
                             truth maintenance).",
                            rule.label
                        );
                    }
                    continue;
                }
                // Arc::get_mut only succeeds if there's one strong reference.
                // If shared, clone-on-write.
                if let Some(r) = Arc::get_mut(rule) {
                    r.forward = forward;
                } else {
                    let mut cloned = (**rule).clone();
                    cloned.forward = forward;
                    *rule = Arc::new(cloned);
                }
            }
        }
    }

    /// Set priority for all rules concluding the given predicate.
    /// Higher priority = tried first during backward/forward chaining.
    /// Default is 0. Rules with higher priority override lower-priority ones
    /// (defeasible reasoning / exception hierarchies).
    pub fn set_rule_priority(&self, conclusion_predicate: &str, priority: u32) {
        let mut inner = self.inner.borrow_mut();
        if let Some(rules) = inner.universal_rules.get_mut(conclusion_predicate) {
            for rule in rules.iter_mut() {
                if let Some(r) = Arc::get_mut(rule) {
                    r.priority = priority;
                } else {
                    let mut cloned = (**rule).clone();
                    cloned.priority = priority;
                    *rule = Arc::new(cloned);
                }
            }
            // Re-establish the descending-priority order the backward-chain read
            // path relies on (`matching_rules_typed` borrows the bucket as-is).
            sort_rule_bucket(rules);
        }
    }

    /// Declare that an entity belongs to a sort.
    /// e.g., `declare_entity_sort("adam", "person")` means adam is a person.
    pub fn declare_entity_sort(&self, entity: &str, sort: &str) {
        let mut inner = self.inner.borrow_mut();
        inner
            .entity_sorts
            .insert(entity.to_string(), sort.to_string());
    }

    /// Declare a subsort relationship: child ⊂ parent.
    /// e.g., `declare_subsort("person", "animal")` means every person is an animal.
    /// Transitive: if person ⊂ animal and animal ⊂ entity, then person is compatible with entity.
    pub fn declare_subsort(&self, child: &str, parent: &str) {
        let mut inner = self.inner.borrow_mut();
        inner
            .sort_hierarchy
            .entry(child.to_string())
            .or_default()
            .insert(parent.to_string());
    }

    /// Set expected sorts for a predicate's arguments.
    /// e.g., `set_predicate_sorts("gerku", vec!["animal", ""])` means gerku's x1 must be
    /// an "animal" sort, x2 has no sort constraint.
    /// Empty string = no constraint for that position.
    pub fn set_predicate_sorts(&self, predicate: &str, arg_sorts: Vec<String>) {
        let mut inner = self.inner.borrow_mut();
        if let Some(sig) = inner.predicate_registry.get_mut(predicate) {
            sig.arg_sorts = arg_sorts;
        } else {
            inner.predicate_registry.insert(
                predicate.to_string(),
                PredicateSignature {
                    arity: arg_sorts.len(),
                    source: SignatureSource::Inferred,
                    arg_sorts,
                },
            );
        }
    }

    /// Enable tracing for a predicate. When the predicate is encountered
    /// during backward chaining, diagnostic output is printed showing
    /// depth, rule matches, and results.
    pub fn trace_predicate(&self, predicate: &str) {
        self.inner
            .borrow_mut()
            .traced_predicates
            .insert(predicate.to_string());
    }

    /// Disable tracing for a predicate.
    pub fn untrace_predicate(&self, predicate: &str) {
        self.inner.borrow_mut().traced_predicates.remove(predicate);
    }

    /// List all currently traced predicates.
    pub fn traced_predicates(&self) -> Vec<String> {
        self.inner
            .borrow()
            .traced_predicates
            .iter()
            .cloned()
            .collect()
    }

    /// Scan the KB for contradictions. Returns human-readable descriptions.
    ///
    /// **Category 4 (negation)** uses a two-tier check: (a) store membership of
    /// the positive counterpart (asserted facts), then (b) a *cheap middle* —
    /// after dropping the inner borrow, each unmatched asserted `~P` is re-run
    /// as a positive entailment query, so a **rule-derived** positive also
    /// flags (e.g. `travel(every person where ~prisoner)` + `person(Kilo)` +
    /// `~travel(Kilo)`). This is not full closure consistency (integrity §1/§6
    /// and disjunctive antecedents stay store-bound by design — re-entrancy /
    /// false-flag conservatism; see
    /// `test_mixed_conclusion_conservative_p_check_misses_derived_antecedent`).
    /// Vampire/clingo remain the fragment-level closure oracles.
    ///
    /// Checks:
    /// 1. Integrity constraint violations (conjuncts that all hold in the store)
    /// 2. Predicate arity inconsistencies across asserted facts
    /// 3. Equality-expanded integrity violations (`equals` / du union-find)
    /// 4. Negation contradictions — asserted `~P` whose positive holds in the
    ///    store **or** is derivable via backward chaining
    /// 5. Inequality contradictions (`~equals(X,Y)` vs union-find equivalence)
    /// 6. Disjunctive-conclusion constraints — antecedent P by store membership
    ///    only (conservative miss on derived P)
    pub fn check_contradictions(&self) -> Vec<String> {
        let mut violations = Vec::new();
        // Negative groups that fail the store-membership leg of §4 — re-checked
        // via query after the borrow ends (cheap middle for derived positives).
        let mut derived_negation_candidates: Vec<Vec<StoredFact>> = Vec::new();

        let inner = self.inner.borrow();

        // 1. Check integrity constraints.
        for constraint in &inner.integrity_constraints {
            let all_hold = constraint
                .conjuncts
                .iter()
                .all(|c| inner.fact_store.contains(c));
            if all_hold {
                let facts: Vec<String> = constraint
                    .conjuncts
                    .iter()
                    .map(|c| c.to_display_string())
                    .collect();
                violations.push(format!(
                    "Integrity violation '{}': {} all hold",
                    constraint.label,
                    facts.join(" ∧ ")
                ));
            }
        }

        // 2. Check predicate arity consistency across the fact store.
        // The predicate registry tracks first-seen arity. Scan all facts for mismatches.
        let mut arity_map: HashMap<String, usize> = HashMap::new();
        for fact in inner.fact_store.all_facts() {
            let rel = fact.relation().to_string();
            let arity = fact.inner().args.len();
            match arity_map.get(&rel) {
                Some(&expected) if expected != arity => {
                    violations.push(format!(
                        "Arity inconsistency: '{}' has facts with {} and {} arguments",
                        rel, expected, arity
                    ));
                }
                None => {
                    arity_map.insert(rel, arity);
                }
                _ => {}
            }
        }

        // 3. Check equality-induced constraint violations.
        // If du(a,b) and a constraint says "deny P(a) ∧ Q(a)", but P(a) and Q(b) are
        // asserted (which means Q(a) holds via equivalence), flag it.
        if !inner.equivalence_parent.is_empty() && !inner.integrity_constraints.is_empty() {
            for constraint in &inner.integrity_constraints {
                // For each conjunct, expand by equivalence class and check all combos.
                let expanded: Vec<Vec<StoredFact>> = constraint
                    .conjuncts
                    .iter()
                    .map(|c| {
                        let gf = c.inner();
                        let equiv_args: Vec<Vec<GroundTerm>> = gf
                            .args
                            .iter()
                            .map(|arg| {
                                get_equivalence_class_readonly(
                                    &inner.equivalence_parent,
                                    &inner.equivalence_classes,
                                    arg,
                                )
                            })
                            .collect();
                        // Generate all argument combinations.
                        let mut variants = Vec::new();
                        fn cartesian(
                            sets: &[Vec<GroundTerm>],
                            idx: usize,
                            current: &mut Vec<GroundTerm>,
                            out: &mut Vec<Vec<GroundTerm>>,
                        ) {
                            if idx == sets.len() {
                                out.push(current.clone());
                                return;
                            }
                            for val in &sets[idx] {
                                current.push(val.clone());
                                cartesian(sets, idx + 1, current, out);
                                current.pop();
                            }
                        }
                        let mut buf = Vec::new();
                        cartesian(&equiv_args, 0, &mut buf, &mut variants);
                        variants
                            .into_iter()
                            .map(|args| {
                                StoredFact::with_tense_from(
                                    GroundFact::new(gf.relation.clone(), args),
                                    c,
                                )
                            })
                            .collect()
                    })
                    .collect();

                // Check if any combination of expanded conjuncts all hold.
                fn check_combos(
                    expanded: &[Vec<StoredFact>],
                    idx: usize,
                    store: &dyn crate::fact_store::FactStore,
                ) -> bool {
                    if idx == expanded.len() {
                        return true; // All conjuncts satisfied.
                    }
                    expanded[idx].iter().any(|variant| {
                        store.contains(variant) && check_combos(expanded, idx + 1, store)
                    })
                }

                if check_combos(&expanded, 0, &*inner.fact_store) {
                    let facts: Vec<String> = constraint
                        .conjuncts
                        .iter()
                        .map(|c| c.to_display_string())
                        .collect();
                    let msg = format!(
                        "Equality-expanded integrity violation '{}': {} (via du equivalence)",
                        constraint.label,
                        facts.join(" ∧ ")
                    );
                    if !violations.contains(&msg) {
                        violations.push(msg);
                    }
                }
            }
        }

        // 4. Explicitly asserted negative facts (`na <predicate>`) whose positive
        //    counterpart holds. Each negation is a template group with event
        //    arguments generalized to pattern variables (see
        //    `record_negative_ground_fact`). Leg (a): one consistent binding
        //    satisfies EVERY template against the **asserted** fact store
        //    (whole-group requirement prevents false positives from unrelated
        //    events sharing a predicate). Leg (b): after this borrow ends, groups
        //    that miss the store are re-checked via `query_entailment` so a
        //    **derived** positive also flags. Flat `du` inequalities go to §5.
        //    Query semantics (NAF/CWA) are unaffected — negatives never enter
        //    the positive store.
        fn flat_equals_pair(group: &[StoredFact]) -> Option<(&GroundTerm, &GroundTerm)> {
            if group.len() == 1 {
                if let StoredFact::Bare(gf) = &group[0] {
                    if gf.relation == "equals" && gf.args.len() == 2 {
                        return Some((&gf.args[0], &gf.args[1]));
                    }
                }
            }
            None
        }

        for group in &inner.negative_facts {
            if flat_equals_pair(group).is_some() {
                continue;
            }
            if negative_group_holds(group, &*inner.fact_store) {
                let facts: Vec<String> = group.iter().map(|f| f.to_display_string()).collect();
                let msg = format!(
                    "Negation contradiction: ¬({}) was asserted, but the positive \
                     counterpart is also asserted",
                    facts.join(" ∧ ")
                );
                if !violations.contains(&msg) {
                    violations.push(msg);
                }
            } else {
                // Cheap middle: try derivation after the borrow drops.
                derived_negation_candidates.push(group.clone());
            }
        }

        // 5. Asserted inequalities (`na du`). A flat `na du(X, Y)` is contradicted
        //    when X and Y are equivalent under the du union-find — catching both
        //    a directly-asserted `du(X, Y)` and transitive equality
        //    (`du(X, Z) ∧ du(Z, Y)`) that a store-membership check would miss.
        //    (Reflexive `na du(a, a)` is correctly always a contradiction.)
        for group in &inner.negative_facts {
            if let Some((x, y)) = flat_equals_pair(group) {
                let rx = find_canonical_readonly(&inner.equivalence_parent, x);
                let ry = find_canonical_readonly(&inner.equivalence_parent, y);
                if rx == ry {
                    let msg = format!(
                        "Inequality contradiction: ¬({}) was asserted, but the terms are \
                         equivalent under du",
                        group[0].to_display_string()
                    );
                    if !violations.contains(&msg) {
                        violations.push(msg);
                    }
                }
            }
        }

        // 6. Disjunctive-conclusion constraints `¬(P ∧ ¬Q ∧ ¬R)` (from a rule with a
        //    disjunctive head, `ro lo X cu Q ja R`). Flag a contradiction when, for some
        //    binding, ALL P-conditions hold in the positive store AND EVERY disjunct is
        //    explicitly denied (a stored `na <predicate>` covers it). A disjunct is never
        //    DERIVED (unsound in a Horn engine — `R` might hold instead); the positive
        //    use is served by a disjunctive QUERY. P uses store-membership only (via
        //    `solve_group_bindings` over `fact_store`): a rule-DERIVED P does NOT trigger
        //    this — sound + conservative (it can only MISS a contradiction, never falsely
        //    flag one). The check holds `self.inner.borrow()` and stays store-bound by
        //    design (re-entering the query engine here would be a borrow / re-entrancy
        //    hazard). Pinned by
        //    `test_mixed_conclusion_conservative_p_check_misses_derived_antecedent`.
        for dc in &inner.disjunctive_constraints {
            let bindings = solve_group_bindings(&dc.conditions, &*inner.fact_store);
            let violated = bindings.iter().any(|b| {
                dc.disjuncts.iter().all(|disj| {
                    let substituted: Vec<StoredFact> =
                        disj.iter().map(|f| substitute_fact(f, b)).collect();
                    disjunct_explicitly_denied(&substituted, &inner.negative_facts)
                })
            });
            if violated {
                let msg = format!(
                    "Disjunctive constraint violated '{}': the antecedent holds but every \
                     disjunct is explicitly denied (na)",
                    dc.label
                );
                if !violations.contains(&msg) {
                    violations.push(msg);
                }
            }
        }

        // Drop `inner` before re-entering the query engine (borrow / re-entrancy).
        drop(inner);

        // 4b. Cheap middle: asserted `~P` vs *derivable* positive.
        for group in derived_negation_candidates {
            let Some(buf) = negative_group_to_query_buffer(&group) else {
                continue;
            };
            match self.query_entailment_inner(buf) {
                Ok(r) if r.is_true() => {
                    let facts: Vec<String> = group.iter().map(|f| f.to_display_string()).collect();
                    let msg = format!(
                        "Negation contradiction: ¬({}) was asserted, but the positive \
                         counterpart is derivable",
                        facts.join(" ∧ ")
                    );
                    if !violations.contains(&msg) {
                        violations.push(msg);
                    }
                }
                _ => {}
            }
        }

        // Determinism: §2 (arity) iterates `all_facts()` and §4/§5 iterate the
        // `negative_facts` HashSet, so the violation order is otherwise
        // hasher-seed dependent. A single global sort fixes the order of every
        // section at once (ordering only — the SET of violations is unchanged).
        violations.sort();
        violations
    }
}

/// Convert a negative-fact template group into a positive entailment query.
/// Pattern variables (generalized event Skolems) become existentially quantified
/// logic variables so a later contrary (or derived) positive with a different
/// event Skolem still matches — same intent as `negative_group_holds` over the store.
fn negative_group_to_query_buffer(group: &[StoredFact]) -> Option<LogicBuffer> {
    if group.is_empty() {
        return None;
    }
    fn ground_term_to_logical(t: &GroundTerm) -> LogicalTerm {
        match t {
            GroundTerm::Constant(s) => LogicalTerm::Constant(s.clone()),
            GroundTerm::Number(bits) => LogicalTerm::Number(f64::from_bits(*bits)),
            GroundTerm::Description(s) => LogicalTerm::Description(s.clone()),
            GroundTerm::Unspecified => LogicalTerm::Unspecified,
            GroundTerm::PatternVar(s) => LogicalTerm::Variable(s.clone()),
            // Dependent Skolems rarely appear in negative templates; treat as opaque constants.
            GroundTerm::SkolemFn(name, _) => LogicalTerm::Constant(name.clone()),
            GroundTerm::DepPair(_, _) => LogicalTerm::Unspecified,
        }
    }

    let mut nodes: Vec<LogicNode> = Vec::new();
    let mut pattern_vars: Vec<String> = Vec::new();
    let mut leaf_ids: Vec<u32> = Vec::new();

    for fact in group {
        let gf = fact.inner();
        for arg in &gf.args {
            if let GroundTerm::PatternVar(s) = arg {
                if !pattern_vars.iter().any(|v| v == s) {
                    pattern_vars.push(s.clone());
                }
            }
        }
        let args: Vec<LogicalTerm> = gf.args.iter().map(ground_term_to_logical).collect();
        let pred_id = nodes.len() as u32;
        nodes.push(LogicNode::Predicate((gf.relation.clone(), args)));
        let wrapped = match fact {
            StoredFact::Bare(_) => pred_id,
            StoredFact::Past(_) => {
                let id = nodes.len() as u32;
                nodes.push(LogicNode::PastNode(pred_id));
                id
            }
            StoredFact::Present(_) => {
                let id = nodes.len() as u32;
                nodes.push(LogicNode::PresentNode(pred_id));
                id
            }
            StoredFact::Future(_) => {
                let id = nodes.len() as u32;
                nodes.push(LogicNode::FutureNode(pred_id));
                id
            }
            StoredFact::Obligatory(_) => {
                let id = nodes.len() as u32;
                nodes.push(LogicNode::ObligatoryNode(pred_id));
                id
            }
            StoredFact::Permitted(_) => {
                let id = nodes.len() as u32;
                nodes.push(LogicNode::PermittedNode(pred_id));
                id
            }
        };
        leaf_ids.push(wrapped);
    }

    let mut root = leaf_ids[0];
    for &id in &leaf_ids[1..] {
        let and_id = nodes.len() as u32;
        nodes.push(LogicNode::AndNode((root, id)));
        root = and_id;
    }
    // Outermost ∃ for each pattern var (event slots) so free variables are bound.
    for pvar in pattern_vars.into_iter().rev() {
        let ex_id = nodes.len() as u32;
        nodes.push(LogicNode::ExistsNode((pvar, root)));
        root = ex_id;
    }

    Some(LogicBuffer {
        nodes,
        roots: vec![root],
    })
}

#[cfg(test)]
mod tests;