Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ de84f40d

History | View | Annotate | Download (12.3 KB)

1 4fd28192 Thorsten Wißmann
(** 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 a87192e8 Thorsten Wißmann
  | MultiModalKD
15 f1fa9ad5 Thorsten Wißmann
  | CoalitionLogic
16 29b2e3f3 Thorsten Wißmann
  | GML
17 86b07be8 Thorsten Wißmann
  | PML
18 5e0983fe Thorsten Wißmann
  | Constant of string list
19 19f5dad0 Dirk Pattinson
  | Identity
20
  | DefaultImplication
21 4fd28192 Thorsten Wißmann
  | Choice
22
  | Fusion
23
24 5e0983fe Thorsten Wißmann
(* functors whose constructor takes additional parameters *)
25
type parametricFunctorName =
26
  | NameConstant
27
28
val functor_of_string : string -> string list -> functors option
29
val unaryfunctor_of_string : string -> string list -> functors option
30 db23edf7 Thorsten Wißmann
val string_of_functor : functors -> string
31
32 4fd28192 Thorsten Wißmann
(* This type may be extended for additional logics. *)
33
type formulaType =
34
  | Other
35 3b055ae8 dirk
  | TrueFalseF
36 4fd28192 Thorsten Wißmann
  | AndF
37
  | OrF
38
  | AtF
39
  | NomF
40
  | ExF
41
  | AxF
42 f1fa9ad5 Thorsten Wißmann
  | EnforcesF
43
  | AllowsF
44 af276a36 Thorsten Wißmann
  | MoreThanF
45
  | MaxExceptF
46 9bae2c4f Thorsten Wißmann
  | AtLeastProbF (* diamond for PML *)
47
  | LessProbFailF (* box for PML *)
48 c49eea11 Thorsten Wißmann
  | ConstF (* constant functor *)
49
  | ConstnF (* constant functor *)
50 19f5dad0 Dirk Pattinson
  | IdF (* Identity functor *)
51
  | NormF (* Default Implication *)
52
  | NormnF (* negation normal form of default implication *)
53 4fd28192 Thorsten Wißmann
  | ChcF
54
  | FusF
55 3b407438 Christoph Egger
  | MuF
56
  | NuF
57 4fd28192 Thorsten Wißmann
58
type localFormula
59
type bset
60
61
type atFormula
62
type cset
63
type csetSet
64
65
type lht
66
type fht
67
type nht
68
69
type state
70
71
type core
72
73
type setState
74
75
type setCore
76
77
type setCnstr
78
79
(*****************************************************************************)
80
(*                Types that are hard coded into the algorithm               *)
81
(*****************************************************************************)
82
83 269d93e5 Thorsten Wißmann
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
84
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
85
86 b36e57bc Thorsten Wißmann
and stateExpander = unit -> ruleEnumeration
87 4fd28192 Thorsten Wißmann
88
and sort = CoAlgFormula.sort
89
90
and nodeStatus =
91
  | Expandable
92
  | Open
93
  | Sat
94
  | Unsat
95
96
and dependencies = bset list -> bset
97 269d93e5 Thorsten Wißmann
98 16af388e Christoph Egger
and rule = (dependencies * (sort * bset * bset) lazylist)
99 269d93e5 Thorsten Wißmann
100 a9949a25 Thorsten Wißmann
and 'a lazyliststep =
101 69243f7f Thorsten Wißmann
  | MultipleElements of 'a list
102
  | SingleElement    of 'a
103
  | NoMoreElements
104
105 a9949a25 Thorsten Wißmann
(* a lazylist returns on successive calls the entire list until it eventually
106
   returns NoMoreElements
107
*)
108
and 'a lazylist = unit -> 'a lazyliststep
109
110
and ruleEnumeration = rule lazyliststep
111
112
val lazylistFromList : 'a list -> 'a lazylist
113 4fd28192 Thorsten Wißmann
114 672429b4 Thorsten Wißmann
val listFromLazylist : 'a lazylist -> 'a list
115
116 4fd28192 Thorsten Wißmann
type nominal = sort * localFormula
117
118
type node =
119
  | State of state
120
  | Core of core
121
122
type constrnt =
123
  | UnsatC
124
  | SatC
125
  | OpenC of node list
126
  | UnexpandedC of node list
127
128 269d93e5 Thorsten Wißmann
type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
129 4fd28192 Thorsten Wißmann
  | UState of state * int option
130
  | UCore of core * bool
131
  | UCnstr of cset
132
133
type queueElement =
134
  | QState of state
135
  | QCore of core
136
  | QCnstr of cset
137
  | QEmpty
138
139
type sortTable = (functors * int list) array
140
141
exception CoAlg_finished of bool
142
143
144
val sortTable : sortTable ref
145
146 269d93e5 Thorsten Wißmann
(* evaluate a junction in the obvious way *)
147
val junctionEvalBool : bool list junction -> bool
148
val junctionEval: ('a -> bool) -> 'a list junction -> bool
149
val optionalizeOperator: ('a -> 'b -> 'c) -> ('a option -> 'b option -> 'c option)
150
val junctionEvalBoolOption : bool option list junction -> bool option
151
152
(* decompose a junction in it's content and its constructor,
153
   such that: eval∘junctionExtract = id
154
   (with eval: X × (X -> Y) -> Y)
155
 *)
156
val junctionExtract: 'a junction -> ('a * ('b -> 'b junction))
157 4fd28192 Thorsten Wißmann
158
(*****************************************************************************)
159
(*      "Module type" and a specific implementation of the main queue        *)
160
(*****************************************************************************)
161
162
val queueInit : unit -> unit
163
val queueIsEmpty : unit -> bool
164
val queueInsertState : state -> unit
165
val queueInsertCore : core -> unit
166
val queueInsertCnstr : cset -> unit
167
val queueGetElement : unit -> queueElement
168 c2cc0c2e Thorsten Wißmann
val queuePrettyStatus : unit -> string
169 4fd28192 Thorsten Wißmann
170
val doNominalPropagation : unit -> bool
171
val doSatPropagation : unit -> bool
172
173
174
(*****************************************************************************)
175
(*        "Module type" and a specific implementation of the graph           *)
176
(*****************************************************************************)
177
178
val graphInit : unit -> unit
179
val graphIterStates : (state -> unit) -> unit
180
val graphIterCores : (core -> unit) -> unit
181
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
182
val graphClearCnstr : unit -> unit
183 16af388e Christoph Egger
val graphFindState : sort -> (bset * bset) -> state option
184
val graphFindCore : sort -> (bset * bset) -> core option
185 4fd28192 Thorsten Wißmann
val graphFindCnstr : cset -> constrnt option
186 16af388e Christoph Egger
val graphInsertState : sort -> (bset * bset) -> state -> unit
187
val graphInsertCore : sort -> (bset * bset) -> core -> unit
188 4fd28192 Thorsten Wißmann
val graphInsertCnstr : cset -> constrnt -> unit
189
val graphReplaceCnstr : cset -> constrnt -> unit
190
val graphSizeState : unit -> int
191
val graphSizeCore : unit -> int
192
val graphSizeCnstr : unit -> int
193
val graphAddRoot : core -> unit
194
val graphGetRoot : unit -> core
195
196
197
(*****************************************************************************)
198
(*     "Module type" and a specific implementation of sets of constraints    *)
199
(*****************************************************************************)
200
201
val cssEmpty : csetSet
202
val cssExists : (cset -> bool) -> csetSet -> bool
203
val cssForall : (cset -> bool) -> csetSet -> bool
204
val cssUnion : csetSet -> csetSet -> csetSet
205
val cssAdd : cset -> csetSet -> csetSet
206
val cssFold : (cset -> 'a -> 'a) -> csetSet -> 'a -> 'a
207
val cssSingleton : cset -> csetSet
208
val cssEqual : csetSet -> csetSet -> bool
209 f335015f Thorsten Wißmann
val cssIter : (cset -> unit) -> csetSet -> unit
210 4fd28192 Thorsten Wißmann
211
(*****************************************************************************)
212
(*      "Module type" and a specific implementation of state nodes           *)
213
(*****************************************************************************)
214
215 3285ac30 Christoph Egger
val stateMake : sort -> bset -> bset -> stateExpander -> state
216 4fd28192 Thorsten Wißmann
val stateGetSort : state -> sort
217
val stateGetBs : state -> bset
218
val stateSetBs : state -> bset -> unit
219 3285ac30 Christoph Egger
val stateGetDeferral : state -> bset
220
val stateSetDeferral : state -> bset -> unit
221 4fd28192 Thorsten Wißmann
val stateGetStatus : state -> nodeStatus
222
val stateSetStatus : state -> nodeStatus -> unit
223
val stateGetParents : state -> core list
224
val stateAddParent : state -> core -> unit
225
val stateGetRule : state -> int -> dependencies * core list
226
val stateGetRules : state -> (dependencies * core list) list
227
val stateAddRule : state -> dependencies -> core list -> int
228
val stateGetConstraints : state -> csetSet
229
val stateSetConstraints : state -> csetSet -> unit
230 b36e57bc Thorsten Wißmann
val stateNextRule : state -> ruleEnumeration
231 73762b19 Thorsten Wißmann
val stateToString : state -> string
232 8d6bf016 Christoph Egger
val stateToDot : state -> string
233 73762b19 Thorsten Wißmann
val stateGetIdx : state -> int
234 4fd28192 Thorsten Wißmann
235
236
(*****************************************************************************)
237
(*      "Module type" and a specific implementation of core nodes            *)
238
(*****************************************************************************)
239
240 3285ac30 Christoph Egger
val coreMake : sort -> bset -> bset -> Minisat.solver -> fht -> core
241 4fd28192 Thorsten Wißmann
val coreGetSort : core -> sort
242
val coreGetBs : core -> bset
243 b9a8d969 Christoph Egger
val coreSetBs : core -> bset -> unit
244 3285ac30 Christoph Egger
val coreGetDeferral : core -> bset
245 b9a8d969 Christoph Egger
val coreSetDeferral : core -> bset -> unit
246 4fd28192 Thorsten Wißmann
val coreGetStatus : core -> nodeStatus
247
val coreSetStatus : core -> nodeStatus -> unit
248 b9a8d969 Christoph Egger
val coreGetParents : core -> (state * int) list
249 4fd28192 Thorsten Wißmann
val coreAddParent : core -> state -> int -> unit
250
val coreGetChildren : core -> state list
251
val coreAddChild : core -> state -> unit
252
val coreGetConstraints : core -> csetSet
253
val coreSetConstraints : core -> csetSet -> unit
254
val coreGetSolver : core -> Minisat.solver
255
val coreGetFht : core -> fht
256 73762b19 Thorsten Wißmann
val coreGetIdx : core -> int
257 4fd28192 Thorsten Wißmann
val coreGetConstraintParents : core -> cset list
258
val coreAddConstraintParent : core -> cset -> unit
259 f335015f Thorsten Wißmann
val coreToString : core -> string
260 8d6bf016 Christoph Egger
val coreToDot : core -> string
261 4fd28192 Thorsten Wißmann
262
263
(*****************************************************************************)
264
(*      "Module type" and a specific implementation of sets of               *)
265
(*      states, cores, and constraints for the sat propagation               *)
266
(*****************************************************************************)
267
268
val setEmptyState : unit -> setState
269
val setEmptyCore : unit -> setCore
270
val setEmptyCnstr : unit -> setCnstr
271
val setAddState : setState -> state -> unit
272
val setAddCore : setCore -> core -> unit
273
val setAddCnstr : setCnstr -> cset -> unit
274
val setMemState : setState -> state -> bool
275
val setMemCore : setCore -> core -> bool
276
val setMemCnstr : setCnstr -> cset -> bool
277
val setRemoveState : setState -> state -> unit
278
val setRemoveCore : setCore -> core -> unit
279
val setRemoveCnstr : setCnstr -> cset -> unit
280
val setIterState : (state -> unit) -> setState -> unit
281
val setIterCore : (core -> unit) -> setCore -> unit
282
val setIterCnstr : (cset -> unit) -> setCnstr -> unit
283 50df1dc2 Christoph Egger
val setLengthState : setState -> int
284
val setLengthCore : setCore -> int
285 4fd28192 Thorsten Wißmann
286
287
(*****************************************************************************)
288
(*        "Module type" and a specific implementation of the mapping         *)
289
(*        between (local) formulae and literals of the sat solver,           *)
290
(*        and of a mapping of nominals to sets of formulae                   *)
291
(*****************************************************************************)
292
293
val lhtInit : unit -> lht
294
val lhtAdd : lht -> Minisat.lit -> localFormula -> unit
295
val lhtFind : lht -> Minisat.lit -> localFormula option
296
297
val fhtInit : unit -> fht
298
val fhtAdd : fht -> localFormula -> Minisat.lit -> unit
299
val fhtFind : fht -> localFormula -> Minisat.lit option
300
301
val nhtInit : unit -> nht
302
val nhtAdd : nht -> nominal -> bset -> unit
303
val nhtFind : nht -> nominal -> bset option
304
val nhtFold : (nominal -> bset -> 'a -> 'a) -> nht -> 'a -> 'a
305
306
307
(*****************************************************************************)
308
(*         "Module type" and a specific implementation of sets of            *)
309
(*         local formulae and @-formulae                                     *)
310
(*****************************************************************************)
311
312 45d554b0 Thorsten Wißmann
val bsetMake : unit -> bset (* a new bset which only contains True *)
313
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
314 4fd28192 Thorsten Wißmann
val bsetAdd : bset -> localFormula -> unit
315
val bsetMem : bset -> localFormula -> bool
316 16af388e Christoph Egger
val bsetCompare : bset -> bset -> int
317 4fd28192 Thorsten Wißmann
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
318
val bsetIter : (localFormula -> unit) -> bset -> unit
319 e4cd869a Thorsten Wißmann
val bsetFilter : bset -> (localFormula -> bool) -> bset
320 4fd28192 Thorsten Wißmann
val bsetAddTBox : sort -> bset -> bset
321 b7c3a47e Thorsten Wißmann
val bsetCopy : bset -> bset
322 f335015f Thorsten Wißmann
val bsetToString : sort -> bset -> string
323 4fd28192 Thorsten Wißmann
324
val csetMake : unit -> cset
325
val csetAdd : cset -> atFormula -> unit
326
val csetCopy : cset -> cset
327
val csetUnion : cset -> cset -> cset
328
val csetHasDot : cset -> bool
329
val csetAddDot : cset -> unit
330
val csetRemDot : cset -> unit
331
val csetAddTBox : sort -> cset -> bset
332
val csetIter : cset -> (atFormula -> unit) -> unit
333 f335015f Thorsten Wißmann
val csetToString : sort -> cset -> string
334 4fd28192 Thorsten Wißmann
335
336
(*****************************************************************************)
337
(*            "Module type" and a specific implementation of                 *)
338
(*            local formulae and @-formulae                                  *)
339
(*****************************************************************************)
340
341
val lfGetType : sort -> localFormula -> formulaType
342
val lfGetDest1 : sort -> localFormula -> localFormula
343
val lfGetDest2 : sort -> localFormula -> localFormula
344
val lfGetDest3 : sort -> localFormula -> int
345 c67aca42 Christoph Egger
val lfGetDeferral : sort -> localFormula -> int
346 29b2e3f3 Thorsten Wißmann
val lfGetDestNum : sort -> localFormula -> int
347 eda515b6 Thorsten Wißmann
val lfGetDestNum2 : sort -> localFormula -> int
348 f1fa9ad5 Thorsten Wißmann
val lfGetDestAg : sort -> localFormula -> int array
349 4fd28192 Thorsten Wißmann
val lfGetNeg : sort -> localFormula -> localFormula option
350
val lfGetAt : nominal -> localFormula -> atFormula
351 a0cffef0 Thorsten Wißmann
val lfToInt : localFormula -> int
352
val lfFromInt : int -> localFormula
353 f335015f Thorsten Wißmann
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
354 4fd28192 Thorsten Wißmann
355
val atFormulaGetSubformula : atFormula -> localFormula
356
val atFormulaGetNominal : atFormula -> nominal
357
358
val lfToAt : sort -> localFormula -> atFormula
359
360
val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
361
    CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset