strixonomy_reasoner/
result.rs

1use serde::{Deserialize, Serialize};
2use std::collections::{BTreeMap, BTreeSet};
3use strixonomy_catalog::{ClassHierarchy, SubclassEdge};
4
5#[derive(Debug, Clone, Serialize, Deserialize)]
6pub struct ReasonerWarning {
7    pub code: String,
8    pub message: String,
9    #[serde(skip_serializing_if = "Option::is_none")]
10    pub suggested_profile: Option<String>,
11}
12
13#[derive(Debug, Clone, Serialize, Deserialize)]
14pub struct InferredHierarchy {
15    pub edges: Vec<SubclassEdge>,
16    pub unsatisfiable: Vec<String>,
17    pub combined: ClassHierarchy,
18}
19
20#[derive(Debug, Clone, Serialize, Deserialize)]
21pub struct ClassificationResult {
22    pub profile_used: String,
23    /// `true` when no **named class** is unsatisfiable (⊑ `owl:Nothing`).
24    /// Does not detect all ontology inconsistencies (e.g. some ABox clashes).
25    pub consistent: bool,
26    pub unsatisfiable: Vec<String>,
27    pub inferred: InferredHierarchy,
28    pub new_inferences: Vec<SubclassEdge>,
29    pub warnings: Vec<ReasonerWarning>,
30    pub duration_ms: u64,
31    pub subsumption_count: usize,
32    pub inferred_axiom_count: usize,
33    /// Equivalence clusters from taxonomy classifiers (EL/DL/SWRL).
34    /// Empty for RL/RDFS paths that do not produce taxonomy clusters.
35    #[serde(default, skip_serializing_if = "Vec::is_empty")]
36    pub equivalences: Vec<Vec<String>>,
37}
38
39#[derive(Debug, Clone, Serialize, Deserialize)]
40pub struct ConsistencyResult {
41    /// Ontology + class-level consistency when available (see [`ConsistencyDetail`]).
42    pub consistent: bool,
43    pub unsatisfiable: Vec<String>,
44    #[serde(default, skip_serializing_if = "Option::is_none")]
45    pub detail: Option<ConsistencyDetail>,
46}
47
48/// Full consistency semantics (TBox unsat + ABox / ontology consistency).
49#[derive(Debug, Clone, Serialize, Deserialize)]
50pub struct ConsistencyDetail {
51    pub consistent: bool,
52    /// Whether the facade consistency check finished (budget / cancel complete).
53    pub complete: bool,
54    /// `true` when the ontology itself is consistent (ABox + TBox engines).
55    pub ontology_consistent: bool,
56    pub abox_clashes: Vec<String>,
57    pub unsatisfiable: Vec<String>,
58}
59
60#[derive(Debug, Clone, Serialize, Deserialize)]
61pub struct RealizationEntry {
62    pub individual_iri: String,
63    pub types: Vec<String>,
64    pub most_specific: Vec<String>,
65    pub asserted: Vec<String>,
66    pub inferred: Vec<String>,
67}
68
69#[derive(Debug, Clone, Serialize, Deserialize)]
70pub struct RealizationResult {
71    pub profile_used: String,
72    pub individuals: Vec<RealizationEntry>,
73    pub duration_ms: u64,
74    /// `true` when the individual list or entailment budget was hit, or some
75    /// entailment checks failed (#359 / #361). Incomplete — not a full realization.
76    #[serde(default)]
77    pub truncated: bool,
78    /// Count of non-cancel entailment check failures treated as incomplete (#361).
79    #[serde(default)]
80    pub entailment_errors: usize,
81}
82
83#[derive(Debug, Clone, Serialize, Deserialize)]
84pub struct InstanceCheckResult {
85    pub individual_iri: String,
86    pub class_iri: String,
87    pub entailed: bool,
88    pub profile_used: String,
89    pub duration_ms: u64,
90}
91
92#[derive(Debug, Clone, Serialize, Deserialize)]
93pub struct InferredClassAssertion {
94    pub individual_iri: String,
95    pub class_iri: String,
96}
97
98#[derive(Debug, Clone, Serialize, Deserialize)]
99pub struct InferredObjectPropertyAssertion {
100    pub subject_iri: String,
101    pub property_iri: String,
102    pub object_iri: String,
103}
104
105#[derive(Debug, Clone, Serialize, Deserialize)]
106pub struct SameAsCluster {
107    pub individuals: Vec<String>,
108}
109
110#[derive(Debug, Clone, Serialize, Deserialize)]
111pub struct InferredAssertions {
112    pub class_assertions: Vec<InferredClassAssertion>,
113    pub object_property_assertions: Vec<InferredObjectPropertyAssertion>,
114    pub same_as_clusters: Vec<SameAsCluster>,
115}
116
117#[derive(Debug, Clone, Serialize, Deserialize)]
118pub struct ReasonerSnapshot {
119    pub profile_used: String,
120    pub consistent: bool,
121    pub unsatisfiable: Vec<String>,
122    pub inferred: InferredHierarchy,
123    pub new_inferences: Vec<SubclassEdge>,
124    pub warnings: Vec<ReasonerWarning>,
125    pub duration_ms: u64,
126    pub classified_at: u64,
127    #[serde(default, skip_serializing_if = "Option::is_none")]
128    pub consistency: Option<ConsistencyDetail>,
129    #[serde(default, skip_serializing_if = "Option::is_none")]
130    pub realization: Option<RealizationResult>,
131    #[serde(default, skip_serializing_if = "Option::is_none")]
132    pub inferred_assertions: Option<InferredAssertions>,
133}
134
135impl From<ClassificationResult> for ReasonerSnapshot {
136    fn from(result: ClassificationResult) -> Self {
137        Self {
138            profile_used: result.profile_used,
139            consistent: result.consistent,
140            unsatisfiable: result.unsatisfiable,
141            inferred: result.inferred,
142            new_inferences: result.new_inferences,
143            warnings: result.warnings,
144            duration_ms: result.duration_ms,
145            classified_at: std::time::SystemTime::now()
146                .duration_since(std::time::UNIX_EPOCH)
147                .map(|d| d.as_secs())
148                .unwrap_or(0),
149            consistency: None,
150            realization: None,
151            inferred_assertions: None,
152        }
153    }
154}
155
156#[derive(Debug, Clone, Serialize, Deserialize)]
157pub struct ExplanationRequest {
158    pub class_iri: String,
159}
160
161#[derive(Debug, Clone, Serialize, Deserialize)]
162pub struct ExplanationStep {
163    pub index: usize,
164    pub rule: String,
165    pub display: String,
166    #[serde(skip_serializing_if = "Option::is_none")]
167    pub subject_iri: Option<String>,
168    #[serde(skip_serializing_if = "Option::is_none")]
169    pub object_iri: Option<String>,
170}
171
172#[derive(Debug, Clone, Serialize, Deserialize)]
173pub struct ExplanationResult {
174    pub class_iri: String,
175    pub steps: Vec<ExplanationStep>,
176    pub text: String,
177}
178
179const OWL_NOTHING: &str = "http://www.w3.org/2002/07/owl#Nothing";
180
181/// Expand taxonomy unsatisfiable IRIs to **named** classes that are ⊑ ⊥.
182///
183/// Ontologos sometimes reports only `owl:Nothing` itself. User-facing consistency
184/// (see [`ClassificationResult::consistent`]) must reflect named classes that are
185/// unsatisfiable via asserted/inferred ⊑ `owl:Nothing` (and descendants of any
186/// unsatisfiable class).
187pub fn expand_named_unsatisfiable(reported: &[String], hierarchy: &ClassHierarchy) -> Vec<String> {
188    let mut unsat: BTreeSet<String> = reported.iter().cloned().collect();
189    for edge in &hierarchy.edges {
190        if edge.parent == OWL_NOTHING {
191            unsat.insert(edge.child.clone());
192        }
193    }
194    let mut changed = true;
195    while changed {
196        changed = false;
197        for edge in &hierarchy.edges {
198            if unsat.contains(&edge.parent) && unsat.insert(edge.child.clone()) {
199                changed = true;
200            }
201        }
202    }
203    unsat.remove(OWL_NOTHING);
204    unsat.into_iter().collect()
205}
206
207pub fn build_inferred_hierarchy(
208    taxonomy_edges: &[(String, String)],
209    unsatisfiable: &[String],
210    asserted: &ClassHierarchy,
211) -> InferredHierarchy {
212    let asserted_set: BTreeSet<(String, String)> =
213        asserted.edges.iter().map(|e| (e.child.clone(), e.parent.clone())).collect();
214
215    let mut inferred_edges = Vec::new();
216    for (child, parent) in taxonomy_edges {
217        let pair = (child.clone(), parent.clone());
218        if !asserted_set.contains(&pair) {
219            inferred_edges.push(SubclassEdge { child: child.clone(), parent: parent.clone() });
220        }
221    }
222
223    let mut combined_edges = asserted.edges.clone();
224    let mut combined_set = asserted_set;
225    for edge in &inferred_edges {
226        let pair = (edge.child.clone(), edge.parent.clone());
227        if combined_set.insert(pair) {
228            combined_edges.push(edge.clone());
229        }
230    }
231
232    let combined = hierarchy_from_edges(combined_edges);
233    let expanded = expand_named_unsatisfiable(unsatisfiable, &combined);
234    InferredHierarchy { edges: inferred_edges, unsatisfiable: expanded, combined }
235}
236
237pub fn new_inferences(asserted: &ClassHierarchy, inferred: &[SubclassEdge]) -> Vec<SubclassEdge> {
238    let asserted_set: BTreeSet<(String, String)> =
239        asserted.edges.iter().map(|e| (e.child.clone(), e.parent.clone())).collect();
240    inferred
241        .iter()
242        .filter(|e| !asserted_set.contains(&(e.child.clone(), e.parent.clone())))
243        .cloned()
244        .collect()
245}
246
247pub fn hierarchy_from_edges(edges: Vec<SubclassEdge>) -> ClassHierarchy {
248    let mut parents: BTreeMap<String, Vec<String>> = BTreeMap::new();
249    let mut children: BTreeMap<String, Vec<String>> = BTreeMap::new();
250
251    for edge in &edges {
252        parents.entry(edge.child.clone()).or_default().push(edge.parent.clone());
253        children.entry(edge.parent.clone()).or_default().push(edge.child.clone());
254    }
255
256    for list in parents.values_mut() {
257        list.sort();
258        list.dedup();
259    }
260    for list in children.values_mut() {
261        list.sort();
262        list.dedup();
263    }
264
265    ClassHierarchy { edges, parents, children }
266}
267
268pub fn taxonomy_to_iri_edges(
269    ontology: &ontologos_core::Ontology,
270    taxonomy: &ontologos_core::Taxonomy,
271) -> Result<Vec<(String, String)>, String> {
272    taxonomy
273        .subsumptions
274        .iter()
275        .map(|(sub, sup)| {
276            let child = entity_iri(ontology, *sub)?;
277            let parent = entity_iri(ontology, *sup)?;
278            Ok((child, parent))
279        })
280        .collect()
281}
282
283/// Convert taxonomy equivalence clusters to IRI vectors (skip singleton / empty).
284pub fn taxonomy_equivalence_clusters(
285    ontology: &ontologos_core::Ontology,
286    taxonomy: &ontologos_core::Taxonomy,
287) -> Result<Vec<Vec<String>>, String> {
288    let mut out = Vec::new();
289    for cluster in &taxonomy.equivalences {
290        if cluster.len() < 2 {
291            continue;
292        }
293        let mut iris = Vec::with_capacity(cluster.len());
294        for id in cluster {
295            iris.push(entity_iri(ontology, *id)?);
296        }
297        iris.sort();
298        iris.dedup();
299        if iris.len() >= 2 {
300            out.push(iris);
301        }
302    }
303    Ok(out)
304}
305
306pub fn entity_iri(
307    ontology: &ontologos_core::Ontology,
308    id: ontologos_core::EntityId,
309) -> Result<String, String> {
310    let entity = ontology.entity(id).map_err(|e| e.to_string())?;
311    ontology.resolve_iri(entity.iri).map(|s| s.to_string()).map_err(|e| e.to_string())
312}
313
314pub fn unsatisfiable_iris(
315    ontology: &ontologos_core::Ontology,
316    taxonomy: &ontologos_core::Taxonomy,
317) -> Result<Vec<String>, String> {
318    taxonomy.unsatisfiable.iter().map(|id| entity_iri(ontology, *id)).collect()
319}
320
321/// Run EL classification to detect unsatisfiable classes (used after RL/RDFS saturation).
322pub fn detect_unsatisfiable_classes(
323    ontology: &ontologos_core::Ontology,
324) -> Result<Vec<String>, String> {
325    use ontologos_el::ElClassifier;
326    let taxonomy =
327        ElClassifier::new().classify(ontology).map_err(|e| format!("unsat detection: {e}"))?;
328    unsatisfiable_iris(ontology, &taxonomy)
329}
330
331#[cfg(test)]
332mod tests {
333    use super::*;
334    use strixonomy_catalog::SubclassEdge;
335
336    #[test]
337    fn expand_named_unsatisfiable_includes_descendants_of_nothing() {
338        let hierarchy = hierarchy_from_edges(vec![
339            SubclassEdge { child: "http://ex/B".into(), parent: OWL_NOTHING.into() },
340            SubclassEdge { child: "http://ex/Invalid".into(), parent: "http://ex/B".into() },
341        ]);
342        let expanded = expand_named_unsatisfiable(&[OWL_NOTHING.to_string()], &hierarchy);
343        assert!(expanded.iter().any(|i| i == "http://ex/B"));
344        assert!(expanded.iter().any(|i| i == "http://ex/Invalid"));
345        assert!(!expanded.iter().any(|i| i == OWL_NOTHING));
346    }
347}
strixonomy_reasoner/result.rs

strixonomy_reasoner/
result.rs
