Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / FuzzyALCABox.mli @ fa1727d2

History | View | Annotate | Download (1.25 KB)

1
(*
2
 * vim: ts=2 sw=2
3
 *)
4

    
5
exception CoAlgException of string
6

    
7
type concept =
8
  | TRUE
9
  | FALSE
10
  | AP of string
11
  | NOT of concept
12
  | OR of concept * concept
13
  | AND of concept * concept
14
  | EXISTS of int * concept
15
  | FORALL of int * concept
16

    
17
type asst =
18
  | ROLE of int * int * int
19
  | CONCEPT of int * concept
20
type assertion = (asst list) * int * (asst list)
21

    
22
exception ConversionException of concept
23

    
24
(** Hash-consed formulae, which are in negation normal form,
25
    such that structural and physical equality coincide.
26
 *)
27
type hcConcept = (hcConcept_node, concept) HashConsing.hash_consed
28
and hcConcept_node =
29
  | HCTRUE
30
  | HCFALSE
31
  | HCAP of string
32
  | HCNOT of hcConcept
33
  | HCOR of hcConcept * hcConcept
34
  | HCAND of hcConcept * hcConcept
35
  | HCEXISTS of int * hcConcept
36
  | HCFORALL of int * hcConcept
37

    
38
module HcFormula : (HashConsing.S with type nde = hcConcept_node and type fml = concept)
39

    
40
type hcAsst =
41
  | HCROLE of int * int * int
42
  | HCCONCEPT of int * hcConcept
43

    
44
val toAsst : hcAsst -> asst
45
val printAssertion : assertion -> string
46
val toHcAsst : HcFormula.t -> asst -> hcAsst
47
val hc_formula : HcFormula.t -> concept -> hcConcept
48
val importQuery : string -> assertion list
49
val replaceOrForall : assertion -> assertion
50
val collapseNeg : assertion -> assertion