pub struct NibliEngine { /* private fields */ }Implementations§
Source§impl NibliEngine
impl NibliEngine
Sourcepub fn kb(&self) -> &KnowledgeBase
pub fn kb(&self) -> &KnowledgeBase
Access the underlying KnowledgeBase for sort/constraint declarations.
Sourcepub fn set_cancel_flag(&self, flag: Arc<AtomicBool>)
pub fn set_cancel_flag(&self, flag: Arc<AtomicBool>)
Install a cooperative cancellation flag on the underlying reasoning core.
When the flag is raised, an in-flight query aborts via the error channel
(returned as a String error from the query methods). The native
nibli-server watchdog uses this to free a blocking thread when a request’s
wall-clock budget elapses, instead of letting a pathological query run to
completion. No clock is read inside the engine.
Sourcepub fn clear_cancel_flag(&self)
pub fn clear_cancel_flag(&self)
Remove any installed cancellation flag.
Sourcepub fn set_verbose(&self, verbose: bool)
pub fn set_verbose(&self, verbose: bool)
Enable/disable the engine’s informational stdout diagnostics
([Rule]/[Skolem]/[Constraint] Registered). Default OFF — nibli-engine
is a silent library, so the server/validate/tavla do not spam stdout on a
per-query corpus re-assertion. Interactive callers (the native nibli
REPL) opt in. Configuration — survives reset().
Sourcepub fn set_strict(&self, strict: bool)
pub fn set_strict(&self, strict: bool)
Enable/disable STRICT MODE (default off — permissive warn-and-insert):
when on, an arity mismatch or integrity-constraint violation REJECTS the
offending fact and fails the assertion. Like set_verbose, the library
stays permissive by default; embedders opt in programmatically (the
runtime surfaces read NIBLI_STRICT=1 — nibli-host forwards it into the
guest, where nibli-pipeline::Session::new applies it).
Sourcepub fn set_existential_import(&self, on: bool)
pub fn set_existential_import(&self, on: bool)
Enable/disable EXISTENTIAL-IMPORT MODE (default ON — the v0.1 xorlo
behavior). OFF gives the clean-core some = plain classical ∃ profile:
a description universal no longer mints a presupposition witness. The
runtime surfaces read NIBLI_EXISTENTIAL_IMPORT=0 (nibli-host forwards it
into the guest, where nibli-pipeline::Session::new applies it).
Sourcepub fn set_materialization(&self, on: bool)
pub fn set_materialization(&self, on: bool)
Enable/disable STRATUM-ORDERED MATERIALISATION (default ON). When on, the
relations a query reads under ~ are saturated bottom-up in stratum order and
each NAF check becomes a set-membership test. OFF restores the pure
backward-chaining path. The runtime surfaces read NIBLI_MATERIALIZE=0
(nibli-host forwards it into the guest, where nibli-pipeline::Session::new
applies it).
Sourcepub fn materialization_report(&self) -> (Vec<String>, Vec<(String, String)>)
pub fn materialization_report(&self) -> (Vec<String>, Vec<(String, String)>)
What the last query’s saturation covered: (completed, [(relation, why not)]).
The only way to see whether a slow ~p(x) actually got the lookup.
Sourcepub fn set_compute_dispatch(
&self,
eval: fn(&str, &[EngineLogicalTerm]) -> Result<bool, String>,
batch_eval: fn(&[ComputeRequest]) -> Vec<Result<bool, String>>,
)
pub fn set_compute_dispatch( &self, eval: fn(&str, &[EngineLogicalTerm]) -> Result<bool, String>, batch_eval: fn(&[ComputeRequest]) -> Vec<Result<bool, String>>, )
Register this engine’s external compute dispatch (per-instance). Without
it, external predicates (e.g. tenfa/dugri) return an error; built-in
arithmetic (pilji/sumji/dilcu) works regardless. Replaces the old
thread-local registration that the multithreaded server could not use.
See nibli_reason::KnowledgeBase::set_compute_dispatch for the trust boundary.
Sourcepub fn enable_compute_backend(&self, addr: &str)
pub fn enable_compute_backend(&self, addr: &str)
Enable external compute dispatch to a Python-style JSON-Lines backend at
addr (e.g. "127.0.0.1:5555"). Wires the native TCP client as this
engine’s compute dispatch, so registered external predicates (e.g.
tenfa/dugri) are evaluated by the backend; built-in arithmetic
(pilji/sumji/dilcu) is still resolved in-engine. Opt-in — engines that do
not call this leave external compute unregistered (set_compute_dispatch
isolation preserved). The address is stored per-thread; in the
multithreaded server each spawn_blocking worker connects lazily and
reuses its connection. Register the external predicate names separately
via register_compute_predicate. Trust boundary: the backend is a
plaintext, unauthenticated peer in the trusted computing base.
Sourcepub fn open(db_path: &Path) -> Result<Self, String>
pub fn open(db_path: &Path) -> Result<Self, String>
Create an engine with disk persistence at the given path.
Opens a RedbFactStore for typed fact persistence and replays
the legacy NibliStore (LogicBuffer-level) for backward compatibility.
Sourcepub fn validate(&self, text: &str) -> Result<(), String>
pub fn validate(&self, text: &str) -> Result<(), String>
Validate KR text without asserting — returns Ok if it parses and compiles.
Sourcepub fn register_compute_predicate(&mut self, name: String)
pub fn register_compute_predicate(&mut self, name: String)
Register a predicate name for external compute dispatch.
Sourcepub fn assert_text(&self, text: &str) -> Result<Vec<u64>, EngineError>
pub fn assert_text(&self, text: &str) -> Result<Vec<u64>, EngineError>
Parse KR text, compile to FOL, and assert into the knowledge base.
A bare-.i multi-sentence text becomes N INDEPENDENT facts — one per root —
each with its own id, store record, and retraction (connectives compile to a
single root and stay one fact). Returns the minted ids in root order. A
single-sentence text yields exactly one id.
Sourcepub fn assert_fact_direct(
&self,
relation: String,
args: Vec<EngineLogicalTerm>,
) -> Result<u64, EngineError>
pub fn assert_fact_direct( &self, relation: String, args: Vec<EngineLogicalTerm>, ) -> Result<u64, EngineError>
Assert a fact directly by relation name and arguments, bypassing text
parsing. Delegates to the shared core (label ":assert {relation}";
event-decomposed to the surface shape — see
CoreSession::assert_fact_direct).
Sourcepub fn query_text_with_proof(
&self,
text: &str,
) -> Result<(EngineQueryResult, String, String), EngineError>
pub fn query_text_with_proof( &self, text: &str, ) -> Result<(EngineQueryResult, String, String), EngineError>
Parse KR query, run entailment check, return result + formatted proof + JSON proof.
Sourcepub fn query_text_raw_proof(
&self,
text: &str,
) -> Result<(EngineQueryResult, ProofTrace), EngineError>
pub fn query_text_raw_proof( &self, text: &str, ) -> Result<(EngineQueryResult, ProofTrace), EngineError>
Parse a KR query, run the entailment check, and return the typed
result together with the raw wire nibli_protocol::ProofTrace — for
callers/tests that need structured proof access (the plain-English “why”
summary, the collapsed macro-DAG view) rather than the pre-formatted text.
Sourcepub fn query_holds(&self, text: &str) -> Result<EngineQueryResult, EngineError>
pub fn query_holds(&self, text: &str) -> Result<EngineQueryResult, EngineError>
Evaluate a KR query against the KB and return the typed query result.
Sourcepub fn query_find_text(
&self,
text: &str,
) -> Result<Vec<Vec<EngineWitnessBinding>>, EngineError>
pub fn query_find_text( &self, text: &str, ) -> Result<Vec<Vec<EngineWitnessBinding>>, EngineError>
Parse a KR query and extract all satisfying witness bindings.
Sourcepub fn count_witnesses_text(&self, text: &str) -> Result<usize, EngineError>
pub fn count_witnesses_text(&self, text: &str) -> Result<usize, EngineError>
Count the number of distinct witness binding sets satisfying a KR query.
Exposes nibli_reason::KnowledgeBase::count_witnesses at the embedding level.
Sourcepub fn aggregate_text(
&self,
text: &str,
variable: &str,
op: AggregateOp,
) -> Result<Option<f64>, EngineError>
pub fn aggregate_text( &self, text: &str, variable: &str, op: AggregateOp, ) -> Result<Option<f64>, EngineError>
Aggregate the numeric values bound to variable across all witness binding
sets of a KR query, applying op (Sum/Min/Max/Avg). Returns Ok(None)
when no numeric witnesses are found. Exposes nibli_reason::KnowledgeBase::aggregate.
Sourcepub fn compile_debug(
&self,
text: &str,
) -> Result<EngineLogicBuffer, EngineError>
pub fn compile_debug( &self, text: &str, ) -> Result<EngineLogicBuffer, EngineError>
Compile KR text to the typed FOL LogicBuffer without asserting.
Returns the IR directly — the caller renders it (e.g. via
nibli_render::render_logic_tree / render_logic_buffer). No
S-expression string is produced.
Sourcepub fn list_facts(&self) -> Result<Vec<EngineFactSummary>, EngineError>
pub fn list_facts(&self) -> Result<Vec<EngineFactSummary>, EngineError>
List all active (non-retracted) facts with their IDs and labels.
Sourcepub fn retract_fact(&self, id: u64) -> Result<(), EngineError>
pub fn retract_fact(&self, id: u64) -> Result<(), EngineError>
Retract a fact by ID and rebuild derived state.
When persistence is configured, the retraction is also written through to
the on-disk store as a tombstone, so a subsequent open() does NOT replay
(resurrect) the retracted fact. The in-memory KB is retracted first (this
validates the ID and rebuilds derived state); the durable tombstone is only
written if that succeeds, keeping both layers consistent.
Sourcepub fn check_contradictions(&self) -> Vec<String>
pub fn check_contradictions(&self) -> Vec<String>
Scan for contradictions (asserted store + derived positives for ~P;
not a full closure proof — see
nibli_reason::KnowledgeBase::check_contradictions).
Sourcepub fn trace_predicate(&self, predicate: &str)
pub fn trace_predicate(&self, predicate: &str)
Enable tracing for a predicate (interactive debugging).
Sourcepub fn untrace_predicate(&self, predicate: &str)
pub fn untrace_predicate(&self, predicate: &str)
Disable tracing for a predicate.
Sourcepub fn traced_predicates(&self) -> Vec<String>
pub fn traced_predicates(&self) -> Vec<String>
List all currently traced predicates.