Struct CoreSession 

pub struct CoreSession { /* private fields */ }

The shared session: a nibli_reason::KnowledgeBase + the compute-predicate registry, with the compile/assert/query verbs every surface previously hand-mirrored. No env reads, no linting, no persistence — those are per-surface boundary policy (see the module doc).

Implementations

impl CoreSession

pub fn new() -> Self

A fresh in-memory session seeded with the built-in arithmetic compute predicates (nibli_reason::default_compute_predicates).

pub fn with_kb(kb: KnowledgeBase) -> Self

Wrap an already-constructed KB (e.g. one built with a persistent write-through fact store via KnowledgeBase::with_store).

pub fn kb(&self) -> &KnowledgeBase

The underlying KB, for surface-specific extras (cancel flags, predicate tracing, contradiction scans, store replay via assert_fact_with_id).

pub fn compute_predicates(&self) -> &HashSet<String>

The current compute-predicate set (the marking input).

pub fn register_compute_predicate(&mut self, name: String)

Register a predicate name for external compute dispatch.

pub fn set_compute_dispatch( &self, eval: fn(&str, &[LogicalTerm]) -> Result<bool, String>, batch_eval: fn(&[ComputeRequest]) -> Vec<Result<bool, String>>, )

Register this session’s external compute dispatch (per-instance; see nibli_reason::KnowledgeBase::set_compute_dispatch for the trust boundary). Without it, external predicates error; built-in arithmetic still resolves in-engine.

pub fn set_verbose(&self, verbose: bool)

Engine stdout diagnostics ([Rule]/[Skolem]/[Constraint]). Default OFF — a silent library; surfaces opt in.

pub fn set_strict(&self, strict: bool)

STRICT MODE (default off — permissive warn-and-insert).

pub fn set_existential_import(&self, on: bool)

EXISTENTIAL-IMPORT MODE (default ON — the v0.1 xorlo behavior). OFF gives the clean-core some = plain ∃ profile (no presupposition witnesses).

pub fn set_materialization(&self, on: bool)

STRATUM-ORDERED MATERIALISATION (default ON). OFF sends every negation-as-failure check back through backward chaining.

pub fn materialization_report(&self) -> (Vec<String>, Vec<(String, String)>)

What the last query’s saturation covered: (complete, [(relation, why not)]). Empty until a query has run and after any KB mutation.

pub fn compile_text(&self, text: &str) -> Result<LogicBuffer, NibliError>

THE compile chain against this session’s compute-predicate set.

pub fn assert_text( &self, text: &str, ) -> Result<Vec<(u64, LogicBuffer)>, NibliError>

Compile KR text and assert it, splitting a multi-statement input into one INDEPENDENT fact per root (split_roots — connectives compile to a single root and stay one compound fact). The full input text is each root’s label. Returns one (id, compiled-sub-buffer) pair per root so a persisting caller can store the FACT itself and replay it recompile-free; callers that only need ids map the pairs down.

pub fn assert_fact_direct( &self, relation: &str, args: &[LogicalTerm], id: Option<u64>, ) -> Result<u64, NibliError>

Assert a fact directly by relation name and arguments, bypassing text parsing, under an optional caller-chosen id (store replay). The label is ":assert {relation}". Event-decomposes to the SAME shape a surface assertion produces, so the injected fact is matched by surface text queries (not just raw-FOL / same-shape direct queries). Identity stays flat; arity follows the injected-arity policy (fail-closed) — see nibli_semantics::compile_injected_fact.

pub fn query_text(&self, text: &str) -> Result<QueryResult, NibliError>

Compile a KR query and run the entailment check.

pub fn query_text_with_proof( &self, text: &str, ) -> Result<(QueryResult, ProofTrace), NibliError>

Compile a KR query, run the entailment check, and return the typed result with the canonical wire ProofTrace.

pub fn query_find_text( &self, text: &str, ) -> Result<Vec<Vec<WitnessBinding>>, NibliError>

Compile a KR query and extract all satisfying witness binding sets.

pub fn count_witnesses_text(&self, text: &str) -> Result<usize, NibliError>

Count the distinct witness binding sets satisfying a KR query.

pub fn aggregate_text( &self, text: &str, variable: &str, op: AggregateOp, ) -> Result<Option<f64>, NibliError>

Aggregate the numeric values bound to variable across all witness binding sets of a KR query. Ok(None) when no numeric witnesses exist.

pub fn retract_fact(&self, id: u64) -> Result<(), NibliError>

Retract a fact by id and rebuild derived state (KB only — durable tombstones are the persisting surface’s concern).

pub fn reset(&self) -> Result<(), NibliError>

Reset the KB, clearing all facts and rules.

pub fn list_facts(&self) -> Result<Vec<FactSummary>, NibliError>

List all active (non-retracted) facts with their ids and labels.

Trait Implementations

impl Default for CoreSession

fn default() -> Self

Returns the “default value” for a type.