-
Notifications
You must be signed in to change notification settings - Fork 0
/
fact.h
404 lines (354 loc) · 18.4 KB
/
fact.h
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
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
/* This file is part of the FaCT++ DL reasoner
Copyright (C) 2011-2012 by Dmitry Tsarkov
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 version 2.1 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU GNU
Lesser General Public License for more details.
You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
*/
#ifndef __FACT_H__
#define __FACT_H__
#ifdef __cplusplus
extern "C" {
#endif
/* type declarations */
#define DECLARE_STRUCT(name) typedef struct name ## _st name
/* FaCT++ kernel */
DECLARE_STRUCT(fact_reasoning_kernel);
/* progress monitor */
DECLARE_STRUCT(fact_progress_monitor);
/* axiom */
DECLARE_STRUCT(fact_axiom);
/* expression */
DECLARE_STRUCT(fact_expression);
/* concept expression */
DECLARE_STRUCT(fact_concept_expression);
/* data- or object-role expression */
DECLARE_STRUCT(fact_role_expression);
/* object role expression */
DECLARE_STRUCT(fact_o_role_expression);
/* complex object role expression */
DECLARE_STRUCT(fact_o_role_complex_expression);
/* data role expression */
DECLARE_STRUCT(fact_d_role_expression);
/* individual expression */
DECLARE_STRUCT(fact_individual_expression);
/* general data expression */
DECLARE_STRUCT(fact_data_expression);
/* data type expression */
DECLARE_STRUCT(fact_data_type_expression);
/* data value expression */
DECLARE_STRUCT(fact_data_value_expression);
/* facet expression */
DECLARE_STRUCT(fact_facet_expression);
/* actor to traverse taxonomy */
DECLARE_STRUCT(fact_actor);
#undef DECLARE_STRUCT
const char *fact_get_version ();
fact_reasoning_kernel *fact_reasoning_kernel_new (void);
void fact_reasoning_kernel_free (fact_reasoning_kernel *);
/*
ifOptionSet* getOptions ( );
const ifOptionSet* getOptions ( );
*/
int fact_is_kb_preprocessed (fact_reasoning_kernel *);
int fact_is_kb_classified (fact_reasoning_kernel *);
int fact_is_kb_realised (fact_reasoning_kernel *);
void fact_set_progress_monitor (fact_reasoning_kernel *, fact_progress_monitor *);
void fact_set_verbose_output (fact_reasoning_kernel *, int value);
void fact_set_top_bottom_role_names (fact_reasoning_kernel *,
const char *top_b_role_name,
const char *bot_b_role_name,
const char *top_d_role_name,
const char *bot_d_role_name);
void fact_set_operation_timeout (fact_reasoning_kernel *,
unsigned long timeout);
int fact_new_kb (fact_reasoning_kernel *);
int fact_release_kb (fact_reasoning_kernel *);
int fact_clear_kb (fact_reasoning_kernel *);
fact_axiom *fact_declare (fact_reasoning_kernel *, fact_expression *c);
fact_axiom *fact_implies_concepts (fact_reasoning_kernel *,
fact_concept_expression *c,
fact_concept_expression *d);
fact_axiom *fact_equal_concepts (fact_reasoning_kernel *);
fact_axiom *fact_disjoint_concepts (fact_reasoning_kernel *);
fact_axiom *fact_disjoint_union (fact_reasoning_kernel *,
fact_concept_expression *c);
fact_axiom *fact_set_inverse_roles (fact_reasoning_kernel *,
fact_o_role_expression *r,
fact_o_role_expression *s);
fact_axiom *fact_implies_o_roles (fact_reasoning_kernel *,
fact_o_role_complex_expression *r,
fact_o_role_expression *s);
fact_axiom *fact_implies_d_roles (fact_reasoning_kernel *,
fact_d_role_expression *r,
fact_d_role_expression *s);
fact_axiom *fact_equal_o_roles (fact_reasoning_kernel *);
fact_axiom *fact_equal_d_roles (fact_reasoning_kernel *);
fact_axiom *fact_disjoint_o_roles (fact_reasoning_kernel *);
fact_axiom *fact_disjoint_d_roles (fact_reasoning_kernel *);
fact_axiom* fact_set_o_domain (fact_reasoning_kernel *,
fact_o_role_expression *r,
fact_concept_expression *c);
fact_axiom *fact_set_d_domain (fact_reasoning_kernel *,
fact_d_role_expression *r,
fact_concept_expression *c);
fact_axiom *fact_set_o_range (fact_reasoning_kernel *,
fact_o_role_expression *r,
fact_concept_expression *c);
fact_axiom *fact_set_d_range (fact_reasoning_kernel *,
fact_d_role_expression *r,
fact_data_expression *e);
fact_axiom *fact_set_transitive (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_reflexive (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_irreflexive (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_symmetric (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_asymmetric (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_o_functional (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_set_d_functional (fact_reasoning_kernel *,
fact_d_role_expression *r);
fact_axiom *fact_set_inverse_functional (fact_reasoning_kernel *,
fact_o_role_expression *r);
fact_axiom *fact_instance_of (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_concept_expression *c);
fact_axiom *fact_related_to (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_o_role_expression *r,
fact_individual_expression *j);
fact_axiom *fact_related_to_not (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_o_role_expression *r,
fact_individual_expression *j);
fact_axiom *fact_value_of (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_d_role_expression *a,
fact_data_value_expression *v);
fact_axiom *fact_value_of_not (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_d_role_expression *a,
fact_data_value_expression *v);
fact_axiom *fact_process_same (fact_reasoning_kernel *);
fact_axiom *fact_process_different (fact_reasoning_kernel *);
fact_axiom *fact_set_fairness_constraint (fact_reasoning_kernel *);
void fact_retract (fact_reasoning_kernel *, fact_axiom *axiom);
int fact_is_kb_consistent (fact_reasoning_kernel *);
void fact_preprocess_kb (fact_reasoning_kernel *);
void fact_classify_kb (fact_reasoning_kernel *);
void fact_realise_kb (fact_reasoning_kernel *);
int fact_is_o_functional (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_d_functional (fact_reasoning_kernel *,
fact_d_role_expression *r);
int fact_is_inverse_functional (fact_reasoning_kernel *,
fact_o_role_expression *r);
int fact_is_transitive (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_symmetric (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_asymmetric (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_reflexive (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_irreflexive (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_sub_o_roles (fact_reasoning_kernel *, fact_o_role_expression *r,
fact_o_role_expression *s);
int fact_is_sub_d_roles (fact_reasoning_kernel *, fact_d_role_expression *r,
fact_d_role_expression *s);
int fact_is_disjoint_o_roles (fact_reasoning_kernel *,
fact_o_role_expression *r,
fact_o_role_expression *s);
int fact_is_disjoint_d_roles (fact_reasoning_kernel *,
fact_d_role_expression *r,
fact_d_role_expression *s);
int fact_is_disjoint_roles (fact_reasoning_kernel *);
int fact_is_sub_chain (fact_reasoning_kernel *, fact_o_role_expression *r);
int fact_is_satisfiable (fact_reasoning_kernel *, fact_concept_expression *c);
int fact_is_subsumed_by (fact_reasoning_kernel *, fact_concept_expression *c,
fact_concept_expression *d);
int fact_is_disjoint (fact_reasoning_kernel *, fact_concept_expression *c,
fact_concept_expression *d);
int fact_is_equivalent (fact_reasoning_kernel *, fact_concept_expression *c,
fact_concept_expression *d);
void fact_get_sup_concepts (fact_reasoning_kernel *, fact_concept_expression *c,
int direct, fact_actor **actor);
void fact_get_sub_concepts (fact_reasoning_kernel *, fact_concept_expression *c,
int direct, fact_actor **actor);
void fact_get_equivalent_concepts (fact_reasoning_kernel *,
fact_concept_expression *c,
fact_actor **actor);
void fact_get_disjoint_concepts (fact_reasoning_kernel *,
fact_concept_expression *c,
fact_actor **actor);
void fact_get_sup_roles (fact_reasoning_kernel *, fact_role_expression *r,
int direct, fact_actor **actor);
void fact_get_sub_roles (fact_reasoning_kernel *, fact_role_expression *r,
int direct, fact_actor **actor);
void fact_get_equivalent_roles (fact_reasoning_kernel *, fact_role_expression *r,
fact_actor **actor);
void fact_get_o_role_domain (fact_reasoning_kernel *, fact_o_role_expression *r,
int direct, fact_actor **actor);
void fact_get_d_role_domain (fact_reasoning_kernel *, fact_d_role_expression *r,
int direct, fact_actor **actor);
void fact_get_role_range (fact_reasoning_kernel *, fact_o_role_expression *r,
int direct, fact_actor **actor);
void fact_get_direct_instances (fact_reasoning_kernel *,
fact_concept_expression *c, fact_actor **actor);
void fact_get_instances (fact_reasoning_kernel *, fact_concept_expression *c,
fact_actor **actor);
void fact_get_types (fact_reasoning_kernel *, fact_individual_expression *i,
int direct, fact_actor **actor);
void fact_get_same_as (fact_reasoning_kernel *,
fact_individual_expression *i, fact_actor **actor);
int fact_is_same_individuals (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_individual_expression *j);
int fact_is_instance (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_concept_expression *c);
/*
void fact_get_related_roles (fact_reasoning_kernel *,
fact_individual_expression *i,
int data, int needI,
fact_names_vector **result);
void fact_get_role_fillers (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_o_role_expression *r,
fact_individual_set **result);
*/
int fact_is_related (fact_reasoning_kernel *,
fact_individual_expression *i,
fact_o_role_expression *r,
fact_individual_expression *j);
fact_actor* fact_concept_actor_new();
fact_actor* fact_individual_actor_new();
fact_actor* fact_o_role_actor_new();
fact_actor* fact_d_role_actor_new();
void fact_actor_free(fact_actor*);
/* get 1-d NULL-terminated array of synonyms of the 1st entry(necessary for Equivalents, for example) */
const char** fact_get_synonyms ( fact_actor* );
/* get NULL-terminated 2D array of all required elements of the taxonomy */
const char*** fact_get_elements_2d ( fact_actor* );
/* get NULL-terminated 1D array of all required elements of the taxonomy */
const char** fact_get_elements_1d ( fact_actor* );
/* opens new argument list */
void fact_new_arg_list ( fact_reasoning_kernel *k );
/* add argument _a_rG to the current argument list */
void fact_add_arg ( fact_reasoning_kernel *k,fact_expression* e );
/* create expressions methods */
/* concepts */
/* get _t_o_p concept */
fact_concept_expression* fact_top ( fact_reasoning_kernel *k );
/* get _b_o_t_t_o_m concept */
fact_concept_expression* fact_bottom ( fact_reasoning_kernel *k );
/* get named concept */
fact_concept_expression* fact_concept ( fact_reasoning_kernel *k,const char* name );
/* get negation of a concept c */
fact_concept_expression* fact_not ( fact_reasoning_kernel *k,fact_concept_expression* c );
/* get an n-ary conjunction expression; take the arguments from the last argument list */
fact_concept_expression* fact_and ( fact_reasoning_kernel *k );
/* get an n-ary disjunction expression; take the arguments from the last argument list */
fact_concept_expression* fact_or ( fact_reasoning_kernel *k );
/* get an n-ary one-of expression; take the arguments from the last argument list */
fact_concept_expression* fact_one_of ( fact_reasoning_kernel *k );
/* get self-reference restriction of an object role r */
fact_concept_expression* fact_self_reference ( fact_reasoning_kernel *k,fact_o_role_expression* r );
/* get value restriction wrt an object role r and an individual i */
fact_concept_expression* fact_o_value ( fact_reasoning_kernel *k,fact_o_role_expression* r, fact_individual_expression* i );
/* get existential restriction wrt an object role r and a concept c */
fact_concept_expression* fact_o_exists ( fact_reasoning_kernel *k,fact_o_role_expression* r, fact_concept_expression* c );
/* get universal restriction wrt an object role r and a concept c */
fact_concept_expression* fact_o_forall ( fact_reasoning_kernel *k,fact_o_role_expression* r, fact_concept_expression* c );
/* get min cardinality restriction wrt number _n, an object role r and a concept c */
fact_concept_expression* fact_o_min_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_o_role_expression* r, fact_concept_expression* c );
/* get max cardinality restriction wrt number _n, an object role r and a concept c */
fact_concept_expression* fact_o_max_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_o_role_expression* r, fact_concept_expression* c );
/* get exact cardinality restriction wrt number _n, an object role r and a concept c */
fact_concept_expression* fact_o_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_o_role_expression* r, fact_concept_expression* c );
/* get value restriction wrt a data role r and a data value v */
fact_concept_expression* fact_d_value ( fact_reasoning_kernel *k,fact_d_role_expression* r, fact_data_value_expression* v );
/* get existential restriction wrt a data role r and a data expression e */
fact_concept_expression* fact_d_exists ( fact_reasoning_kernel *k,fact_d_role_expression* r, fact_data_expression* e );
/* get universal restriction wrt a data role r and a data expression e */
fact_concept_expression* fact_d_forall ( fact_reasoning_kernel *k,fact_d_role_expression* r, fact_data_expression* e );
/* get min cardinality restriction wrt number _n, a data role r and a data expression e */
fact_concept_expression* fact_d_min_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_d_role_expression* r, fact_data_expression* e );
/* get max cardinality restriction wrt number _n, a data role r and a data expression e */
fact_concept_expression* fact_d_max_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_d_role_expression* r, fact_data_expression* e );
/* get exact cardinality restriction wrt number _n, a data role r and a data expression e */
fact_concept_expression* fact_d_cardinality ( fact_reasoning_kernel *k,unsigned int n, fact_d_role_expression* r, fact_data_expression* e );
/* individuals */
/* get named individual */
fact_individual_expression* fact_individual ( fact_reasoning_kernel *k,const char* name );
/* object roles */
/* get _t_o_p object role */
fact_o_role_expression* fact_object_role_top ( fact_reasoning_kernel *k );
/* get _b_o_t_t_o_m object role */
fact_o_role_expression* fact_object_role_bottom ( fact_reasoning_kernel *k );
/* get named object role */
fact_o_role_expression* fact_object_role ( fact_reasoning_kernel *k,const char* name );
/* get an inverse of a given object role expression r */
fact_o_role_expression* fact_inverse ( fact_reasoning_kernel *k,fact_o_role_expression* r );
/* get a role chain corresponding to _r1 o ... o _rn; take the arguments from the last argument list */
fact_o_role_complex_expression* fact_compose ( fact_reasoning_kernel *k );
/* get a expression corresponding to r projected from c */
fact_o_role_complex_expression* fact_project_from ( fact_reasoning_kernel *k,fact_o_role_expression* r, fact_concept_expression* c );
/* get a expression corresponding to r projected into c */
fact_o_role_complex_expression* fact_project_into ( fact_reasoning_kernel *k,fact_o_role_expression* r, fact_concept_expression* c );
/* data roles */
/* get _t_o_p data role */
fact_d_role_expression* fact_data_role_top ( fact_reasoning_kernel *k );
/* get _b_o_t_t_o_m data role */
fact_d_role_expression* fact_data_role_bottom ( fact_reasoning_kernel *k );
/* get named data role */
fact_d_role_expression* fact_data_role ( fact_reasoning_kernel *k,const char* name );
/* data expressions */
/* get _t_o_p data element */
fact_data_expression* fact_data_top ( fact_reasoning_kernel *k );
/* get _b_o_t_t_o_m data element */
fact_data_expression* fact_data_bottom ( fact_reasoning_kernel *k );
/* get named data type */
fact_data_type_expression* fact_data_type ( fact_reasoning_kernel *k,const char* name );
/* get basic string data type */
fact_data_type_expression* fact_get_str_data_type ( fact_reasoning_kernel *k );
/* get basic integer data type */
fact_data_type_expression* fact_get_int_data_type ( fact_reasoning_kernel *k );
/* get basic floating point data type */
fact_data_type_expression* fact_get_real_data_type ( fact_reasoning_kernel *k );
/* get basic boolean data type */
fact_data_type_expression* fact_get_bool_data_type ( fact_reasoning_kernel *k );
/* get basic date-time data type */
fact_data_type_expression* fact_get_time_data_type ( fact_reasoning_kernel *k );
/* get basic boolean data type */
fact_data_type_expression* fact_restricted_type ( fact_reasoning_kernel *k,fact_data_type_expression* type, fact_facet_expression* facet );
/* get data value with given _v_a_lU_e and _tY_p_e; */
/* _f_iX_m_e!! now change the type to the basic type of the given one */
/* _that is, value of a type positive_integer will be of a type _integer */
fact_data_value_expression* fact_data_value ( fact_reasoning_kernel *k,const char* value, fact_data_type_expression* type );
/* get negation of a data expression e */
fact_data_expression* fact_data_not ( fact_reasoning_kernel *k,fact_data_expression* e );
/* get an n-ary data conjunction expression; take the arguments from the last argument list */
fact_data_expression* fact_data_and ( fact_reasoning_kernel *k );
/* get an n-ary data disjunction expression; take the arguments from the last argument list */
fact_data_expression* fact_data_or ( fact_reasoning_kernel *k );
/* get an n-ary data one-of expression; take the arguments from the last argument list */
fact_data_expression* fact_data_one_of ( fact_reasoning_kernel *k );
/* get min_inclusive facet with a given _v */
fact_facet_expression* fact_facet_min_inclusive ( fact_reasoning_kernel *k,fact_data_value_expression* v );
/* get min_exclusive facet with a given _v */
fact_facet_expression* fact_facet_min_exclusive ( fact_reasoning_kernel *k,fact_data_value_expression* v );
/* get max_inclusive facet with a given _v */
fact_facet_expression* fact_facet_max_inclusive ( fact_reasoning_kernel *k,fact_data_value_expression* v );
/* get max_exclusive facet with a given _v */
fact_facet_expression* fact_facet_max_exclusive ( fact_reasoning_kernel *k,fact_data_value_expression* v );
#ifdef __cplusplus
}
#endif
#endif