Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ 7c4d2eb4

History | View | Annotate | Download (9.77 KB)

1
(** Common types, functions, and data structures for the CoAlgebraic reasoner.
2
    @author Florian Widmann
3
 *)
4

    
5

    
6
(*****************************************************************************)
7
(*     Types that can be modified rather easily                              *)
8
(*     (of course you then have to modify the implementations below too)     *)
9
(*****************************************************************************)
10

    
11
(* This type has to be extended for additional logics. *)
12
type functors =
13
  | MultiModalK
14
  | MultiModalKD
15
  | CoalitionLogic
16
  | GML
17
  | Choice
18
  | Fusion
19

    
20
(* This type may be extended for additional logics. *)
21
type formulaType =
22
  | Other
23
  | ConstF
24
  | AndF
25
  | OrF
26
  | AtF
27
  | NomF
28
  | ExF
29
  | AxF
30
  | EnforcesF
31
  | AllowsF
32
  | MoreThanF
33
  | MaxExceptF
34
  | ChcF
35
  | FusF
36

    
37
type localFormula
38
type bset
39

    
40
type atFormula
41
type cset
42
type csetSet
43

    
44
type lht
45
type fht
46
type nht
47

    
48
type state
49

    
50
type core
51

    
52
type setState
53

    
54
type setCore
55

    
56
type setCnstr
57

    
58

    
59
(*****************************************************************************)
60
(*                Types that are hard coded into the algorithm               *)
61
(*****************************************************************************)
62

    
63
and stateExpander = unit -> ruleEnumeration
64

    
65
and sort = CoAlgFormula.sort
66

    
67
and nodeStatus =
68
  | Expandable
69
  | Open
70
  | Sat
71
  | Unsat
72

    
73
and dependencies = bset list -> bset
74
and ruleEnumeration =
75
  | AllInOne of (dependencies * (sort * bset) list) list
76
  | NextRule of dependencies * (sort * bset) list
77
  | NoMoreRules
78

    
79
type nominal = sort * localFormula
80

    
81
type node =
82
  | State of state
83
  | Core of core
84

    
85
type constrnt =
86
  | UnsatC
87
  | SatC
88
  | OpenC of node list
89
  | UnexpandedC of node list
90

    
91
type propagateElement =
92
  | UState of state * int option
93
  | UCore of core * bool
94
  | UCnstr of cset
95

    
96
type queueElement =
97
  | QState of state
98
  | QCore of core
99
  | QCnstr of cset
100
  | QEmpty
101

    
102
type sortTable = (functors * int list) array
103

    
104
exception CoAlg_finished of bool
105

    
106

    
107
val sortTable : sortTable ref
108

    
109

    
110
(*****************************************************************************)
111
(*      "Module type" and a specific implementation of the main queue        *)
112
(*****************************************************************************)
113

    
114
val queueInit : unit -> unit
115
val queueIsEmpty : unit -> bool
116
val queueInsertState : state -> unit
117
val queueInsertCore : core -> unit
118
val queueInsertCnstr : cset -> unit
119
val queueGetElement : unit -> queueElement
120

    
121
val doNominalPropagation : unit -> bool
122
val doSatPropagation : unit -> bool
123

    
124

    
125
(*****************************************************************************)
126
(*        "Module type" and a specific implementation of the graph           *)
127
(*****************************************************************************)
128

    
129
val graphInit : unit -> unit
130
val graphIterStates : (state -> unit) -> unit
131
val graphIterCores : (core -> unit) -> unit
132
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
133
val graphClearCnstr : unit -> unit
134
val graphFindState : sort -> bset -> state option
135
val graphFindCore : sort -> bset -> core option
136
val graphFindCnstr : cset -> constrnt option
137
val graphInsertState : sort -> bset -> state -> unit
138
val graphInsertCore : sort -> bset -> core -> unit
139
val graphInsertCnstr : cset -> constrnt -> unit
140
val graphReplaceCnstr : cset -> constrnt -> unit
141
val graphSizeState : unit -> int
142
val graphSizeCore : unit -> int
143
val graphSizeCnstr : unit -> int
144
val graphAddRoot : core -> unit
145
val graphGetRoot : unit -> core
146

    
147

    
148
(*****************************************************************************)
149
(*     "Module type" and a specific implementation of sets of constraints    *)
150
(*****************************************************************************)
151

    
152
val cssEmpty : csetSet
153
val cssExists : (cset -> bool) -> csetSet -> bool
154
val cssForall : (cset -> bool) -> csetSet -> bool
155
val cssUnion : csetSet -> csetSet -> csetSet
156
val cssAdd : cset -> csetSet -> csetSet
157
val cssFold : (cset -> 'a -> 'a) -> csetSet -> 'a -> 'a
158
val cssSingleton : cset -> csetSet
159
val cssEqual : csetSet -> csetSet -> bool
160

    
161

    
162
(*****************************************************************************)
163
(*      "Module type" and a specific implementation of state nodes           *)
164
(*****************************************************************************)
165

    
166
val stateMake : sort -> bset -> stateExpander -> state
167
val stateGetSort : state -> sort
168
val stateGetBs : state -> bset
169
val stateSetBs : state -> bset -> unit
170
val stateGetStatus : state -> nodeStatus
171
val stateSetStatus : state -> nodeStatus -> unit
172
val stateGetParents : state -> core list
173
val stateAddParent : state -> core -> unit
174
val stateGetRule : state -> int -> dependencies * core list
175
val stateGetRules : state -> (dependencies * core list) list
176
val stateAddRule : state -> dependencies -> core list -> int
177
val stateGetConstraints : state -> csetSet
178
val stateSetConstraints : state -> csetSet -> unit
179
val stateNextRule : state -> ruleEnumeration
180

    
181

    
182
(*****************************************************************************)
183
(*      "Module type" and a specific implementation of core nodes            *)
184
(*****************************************************************************)
185

    
186
val coreMake : sort -> bset -> Minisat.solver -> fht -> core
187
val coreGetSort : core -> sort
188
val coreGetBs : core -> bset
189
val coreSetBs :core -> bset -> unit
190
val coreGetStatus : core -> nodeStatus
191
val coreSetStatus : core -> nodeStatus -> unit
192
val coreGetParents :core -> (state * int) list
193
val coreAddParent : core -> state -> int -> unit
194
val coreGetChildren : core -> state list
195
val coreAddChild : core -> state -> unit
196
val coreGetConstraints : core -> csetSet
197
val coreSetConstraints : core -> csetSet -> unit
198
val coreGetSolver : core -> Minisat.solver
199
val coreGetFht : core -> fht
200
val coreGetConstraintParents : core -> cset list
201
val coreAddConstraintParent : core -> cset -> unit
202

    
203

    
204
(*****************************************************************************)
205
(*      "Module type" and a specific implementation of sets of               *)
206
(*      states, cores, and constraints for the sat propagation               *)
207
(*****************************************************************************)
208

    
209
val setEmptyState : unit -> setState
210
val setEmptyCore : unit -> setCore
211
val setEmptyCnstr : unit -> setCnstr
212
val setAddState : setState -> state -> unit
213
val setAddCore : setCore -> core -> unit
214
val setAddCnstr : setCnstr -> cset -> unit
215
val setMemState : setState -> state -> bool
216
val setMemCore : setCore -> core -> bool
217
val setMemCnstr : setCnstr -> cset -> bool
218
val setRemoveState : setState -> state -> unit
219
val setRemoveCore : setCore -> core -> unit
220
val setRemoveCnstr : setCnstr -> cset -> unit
221
val setIterState : (state -> unit) -> setState -> unit
222
val setIterCore : (core -> unit) -> setCore -> unit
223
val setIterCnstr : (cset -> unit) -> setCnstr -> unit
224

    
225

    
226
(*****************************************************************************)
227
(*        "Module type" and a specific implementation of the mapping         *)
228
(*        between (local) formulae and literals of the sat solver,           *)
229
(*        and of a mapping of nominals to sets of formulae                   *)
230
(*****************************************************************************)
231

    
232
val lhtInit : unit -> lht
233
val lhtAdd : lht -> Minisat.lit -> localFormula -> unit
234
val lhtFind : lht -> Minisat.lit -> localFormula option
235

    
236
val fhtInit : unit -> fht
237
val fhtAdd : fht -> localFormula -> Minisat.lit -> unit
238
val fhtFind : fht -> localFormula -> Minisat.lit option
239

    
240
val nhtInit : unit -> nht
241
val nhtAdd : nht -> nominal -> bset -> unit
242
val nhtFind : nht -> nominal -> bset option
243
val nhtFold : (nominal -> bset -> 'a -> 'a) -> nht -> 'a -> 'a
244

    
245

    
246
(*****************************************************************************)
247
(*         "Module type" and a specific implementation of sets of            *)
248
(*         local formulae and @-formulae                                     *)
249
(*****************************************************************************)
250

    
251
val bsetMake : unit -> bset (* a new bset which only contains True *)
252
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
253
val bsetAdd : bset -> localFormula -> unit
254
val bsetMem : bset -> localFormula -> bool
255
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
256
val bsetIter : (localFormula -> unit) -> bset -> unit
257
val bsetFilter : bset -> (localFormula -> bool) -> bset
258
val bsetAddTBox : sort -> bset -> bset
259
val bsetCopy : bset -> bset
260

    
261
val csetMake : unit -> cset
262
val csetAdd : cset -> atFormula -> unit
263
val csetCopy : cset -> cset
264
val csetUnion : cset -> cset -> cset
265
val csetHasDot : cset -> bool
266
val csetAddDot : cset -> unit
267
val csetRemDot : cset -> unit
268
val csetAddTBox : sort -> cset -> bset
269
val csetIter : cset -> (atFormula -> unit) -> unit
270

    
271

    
272
(*****************************************************************************)
273
(*            "Module type" and a specific implementation of                 *)
274
(*            local formulae and @-formulae                                  *)
275
(*****************************************************************************)
276

    
277
val lfGetType : sort -> localFormula -> formulaType
278
val lfGetDest1 : sort -> localFormula -> localFormula
279
val lfGetDest2 : sort -> localFormula -> localFormula
280
val lfGetDest3 : sort -> localFormula -> int
281
val lfGetDestNum : sort -> localFormula -> int
282
val lfGetDestAg : sort -> localFormula -> int array
283
val lfGetNeg : sort -> localFormula -> localFormula option
284
val lfGetAt : nominal -> localFormula -> atFormula
285
val lfToInt : localFormula -> int
286
val lfFromInt : int -> localFormula
287

    
288
val atFormulaGetSubformula : atFormula -> localFormula
289
val atFormulaGetNominal : atFormula -> nominal
290

    
291
val lfToAt : sort -> localFormula -> atFormula
292

    
293
val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
294
    CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset