Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ de84f40d

History | View | Annotate | Download (12.3 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
  | PML
18
  | Constant of string list
19
  | Identity
20
  | DefaultImplication
21
  | Choice
22
  | Fusion
23

    
24
(* 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
val string_of_functor : functors -> string
31

    
32
(* This type may be extended for additional logics. *)
33
type formulaType =
34
  | Other
35
  | TrueFalseF
36
  | AndF
37
  | OrF
38
  | AtF
39
  | NomF
40
  | ExF
41
  | AxF
42
  | EnforcesF
43
  | AllowsF
44
  | MoreThanF
45
  | MaxExceptF
46
  | AtLeastProbF (* diamond for PML *)
47
  | LessProbFailF (* box for PML *)
48
  | ConstF (* constant functor *)
49
  | ConstnF (* constant functor *)
50
  | IdF (* Identity functor *)
51
  | NormF (* Default Implication *)
52
  | NormnF (* negation normal form of default implication *)
53
  | ChcF
54
  | FusF
55
  | MuF
56
  | NuF
57

    
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
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
and stateExpander = unit -> ruleEnumeration
87

    
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

    
98
and rule = (dependencies * (sort * bset * bset) lazylist)
99

    
100
and 'a lazyliststep =
101
  | MultipleElements of 'a list
102
  | SingleElement    of 'a
103
  | NoMoreElements
104

    
105
(* 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

    
114
val listFromLazylist : 'a lazylist -> 'a list
115

    
116
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
type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
129
  | 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
(* 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

    
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
val queuePrettyStatus : unit -> string
169

    
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
val graphFindState : sort -> (bset * bset) -> state option
184
val graphFindCore : sort -> (bset * bset) -> core option
185
val graphFindCnstr : cset -> constrnt option
186
val graphInsertState : sort -> (bset * bset) -> state -> unit
187
val graphInsertCore : sort -> (bset * bset) -> core -> unit
188
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
val cssIter : (cset -> unit) -> csetSet -> unit
210

    
211
(*****************************************************************************)
212
(*      "Module type" and a specific implementation of state nodes           *)
213
(*****************************************************************************)
214

    
215
val stateMake : sort -> bset -> bset -> stateExpander -> state
216
val stateGetSort : state -> sort
217
val stateGetBs : state -> bset
218
val stateSetBs : state -> bset -> unit
219
val stateGetDeferral : state -> bset
220
val stateSetDeferral : state -> bset -> unit
221
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
val stateNextRule : state -> ruleEnumeration
231
val stateToString : state -> string
232
val stateToDot : state -> string
233
val stateGetIdx : state -> int
234

    
235

    
236
(*****************************************************************************)
237
(*      "Module type" and a specific implementation of core nodes            *)
238
(*****************************************************************************)
239

    
240
val coreMake : sort -> bset -> bset -> Minisat.solver -> fht -> core
241
val coreGetSort : core -> sort
242
val coreGetBs : core -> bset
243
val coreSetBs : core -> bset -> unit
244
val coreGetDeferral : core -> bset
245
val coreSetDeferral : core -> bset -> unit
246
val coreGetStatus : core -> nodeStatus
247
val coreSetStatus : core -> nodeStatus -> unit
248
val coreGetParents : core -> (state * int) list
249
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
val coreGetIdx : core -> int
257
val coreGetConstraintParents : core -> cset list
258
val coreAddConstraintParent : core -> cset -> unit
259
val coreToString : core -> string
260
val coreToDot : core -> string
261

    
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
val setLengthState : setState -> int
284
val setLengthCore : setCore -> int
285

    
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
val bsetMake : unit -> bset (* a new bset which only contains True *)
313
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
314
val bsetAdd : bset -> localFormula -> unit
315
val bsetMem : bset -> localFormula -> bool
316
val bsetCompare : bset -> bset -> int
317
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
318
val bsetIter : (localFormula -> unit) -> bset -> unit
319
val bsetFilter : bset -> (localFormula -> bool) -> bset
320
val bsetAddTBox : sort -> bset -> bset
321
val bsetCopy : bset -> bset
322
val bsetToString : sort -> bset -> string
323

    
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
val csetToString : sort -> cset -> string
334

    
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
val lfGetDeferral : sort -> localFormula -> int
346
val lfGetDestNum : sort -> localFormula -> int
347
val lfGetDestNum2 : sort -> localFormula -> int
348
val lfGetDestAg : sort -> localFormula -> int array
349
val lfGetNeg : sort -> localFormula -> localFormula option
350
val lfGetAt : nominal -> localFormula -> atFormula
351
val lfToInt : localFormula -> int
352
val lfFromInt : int -> localFormula
353
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
354

    
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
362