1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
use crate::dirty::OntologyRevision;
use crate::error::{Error, Result};
use crate::ontology::Ontology;
use crate::taxonomy::Taxonomy;
const MAX_PARALLELISM: usize = 64;
/// OWL profile selected for reasoning.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub enum Profile {
/// Detect the most specific supported profile automatically.
#[default]
Auto,
/// RDFS reasoning only.
Rdfs,
/// OWL RL rule-based reasoning.
Rl,
/// OWL EL completion-based classification.
El,
/// OWL ALC tableau-lite (pre-DL bridge).
Alc,
/// OWL 2 DL coupled saturation + tableau.
Dl,
/// OWL 2 DL preview mode (gated subset checks; same engine as [`Dl`](Self::Dl)).
DlPreview,
/// DLSafe SWRL rules with DL.
Swrl,
}
/// Configuration options for the reasoner builder.
#[derive(Debug, Clone)]
pub struct ReasonerConfig {
/// Enable incremental re-classification when axioms change.
pub incremental: bool,
/// Record explanations for inferences.
pub explanations: bool,
/// Thread count for DL tableau workers (`1..=64`). RL saturation ignores this (reasonable manages parallelism internally).
pub parallelism: usize,
/// Optional wall-clock budget (seconds) for DL consistency/classify paths.
/// Falls back to `ONTOLOGOS_DL_BUDGET_SECS` when unset.
pub budget_secs: Option<u64>,
}
impl Default for ReasonerConfig {
fn default() -> Self {
Self {
incremental: false,
explanations: false,
parallelism: 1,
budget_secs: None,
}
}
}
/// Builder for constructing a configured reasoner instance.
#[derive(Debug, Default)]
pub struct ReasonerBuilder {
profile: Profile,
config: ReasonerConfig,
}
impl ReasonerBuilder {
/// Create a builder with default configuration.
#[must_use]
pub fn new() -> Self {
Self::default()
}
/// Set the OWL profile for reasoning.
#[must_use]
pub fn profile(mut self, profile: Profile) -> Self {
self.profile = profile;
self
}
/// Set reasoner configuration options.
#[must_use]
pub fn config(mut self, config: ReasonerConfig) -> Self {
self.config = config;
self
}
/// Build a reasoner over the given ontology.
pub fn build(self, ontology: Ontology) -> Result<Reasoner> {
if self.config.parallelism == 0 || self.config.parallelism > MAX_PARALLELISM {
return Err(Error::Message(format!(
"parallelism must be in 1..={MAX_PARALLELISM}, got {}",
self.config.parallelism
)));
}
Ok(Reasoner {
ontology,
profile: self.profile,
config: self.config,
session: None,
classify_cache: None,
})
}
}
#[derive(Debug, Clone)]
struct ReasonerCache {
revision: OntologyRevision,
taxonomy: Taxonomy,
}
/// Main reasoner facade over profile-specific engines.
#[derive(Debug)]
pub struct Reasoner {
ontology: Ontology,
profile: Profile,
config: ReasonerConfig,
session: Option<Box<dyn crate::session::ReasonerSession>>,
classify_cache: Option<ReasonerCache>,
}
impl Reasoner {
/// Create a new reasoner builder.
#[must_use]
pub fn builder() -> ReasonerBuilder {
ReasonerBuilder::new()
}
/// The configured OWL profile.
#[must_use]
pub fn profile(&self) -> Profile {
self.profile
}
/// The reasoner configuration.
#[must_use]
pub fn config(&self) -> &ReasonerConfig {
&self.config
}
/// Borrow the loaded ontology.
#[must_use]
pub fn ontology(&self) -> &Ontology {
&self.ontology
}
/// Mutably borrow the loaded ontology (e.g. for RDFS materialization).
pub fn ontology_mut(&mut self) -> &mut Ontology {
self.invalidate_classify_cache();
&mut self.ontology
}
/// Borrow incremental session state, if any.
#[must_use]
pub fn session(&self) -> Option<&dyn crate::session::ReasonerSession> {
self.session.as_deref()
}
/// Mutably borrow incremental session state.
pub fn session_mut(&mut self) -> Option<&mut dyn crate::session::ReasonerSession> {
self.session.as_deref_mut()
}
/// Take session state out of the reasoner (for facade downcasting).
pub fn take_session(&mut self) -> Option<Box<dyn crate::session::ReasonerSession>> {
self.session.take()
}
/// Install or replace incremental session state.
pub fn set_session(&mut self, session: Box<dyn crate::session::ReasonerSession>) {
self.session = Some(session);
}
/// Clear incremental session state.
pub fn clear_session(&mut self) {
if let Some(session) = self.session.as_mut() {
session.clear();
}
self.session = None;
}
/// Borrow cached taxonomy when revision matches the loaded ontology.
#[must_use]
pub fn cached_taxonomy(&self) -> Option<&Taxonomy> {
let cache = self.classify_cache.as_ref()?;
if cache.revision == self.ontology.revision() {
Some(&cache.taxonomy)
} else {
None
}
}
/// Store a taxonomy from the latest classification for entailment reuse.
pub fn set_cached_taxonomy(&mut self, taxonomy: Taxonomy) {
self.classify_cache = Some(ReasonerCache {
revision: self.ontology.revision(),
taxonomy,
});
}
/// Drop cached classification results.
pub fn invalidate_classify_cache(&mut self) {
self.classify_cache = None;
}
}