Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ f20718d2

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 bsetRem : bset -> int -> unit
317
val bsetCompare : bset -> bset -> int
318
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
319
val bsetIter : (localFormula -> unit) -> bset -> unit
320
val bsetFilter : bset -> (localFormula -> bool) -> bset
321
val bsetAddTBox : sort -> bset -> bset
322
val bsetCopy : bset -> bset
323
val bsetToString : sort -> bset -> string
324

    
325
val csetMake : unit -> cset
326
val csetAdd : cset -> atFormula -> unit
327
val csetCopy : cset -> cset
328
val csetUnion : cset -> cset -> cset
329
val csetHasDot : cset -> bool
330
val csetAddDot : cset -> unit
331
val csetRemDot : cset -> unit
332
val csetAddTBox : sort -> cset -> bset
333
val csetIter : cset -> (atFormula -> unit) -> unit
334
val csetToString : sort -> cset -> string
335

    
336

    
337
(*****************************************************************************)
338
(*            "Module type" and a specific implementation of                 *)
339
(*            local formulae and @-formulae                                  *)
340
(*****************************************************************************)
341

    
342
val lfGetType : sort -> localFormula -> formulaType
343
val lfGetDest1 : sort -> localFormula -> localFormula
344
val lfGetDest2 : sort -> localFormula -> localFormula
345
val lfGetDest3 : sort -> localFormula -> int
346
val lfGetDeferral : sort -> localFormula -> int
347
val lfGetDestNum : sort -> localFormula -> int
348
val lfGetDestNum2 : sort -> localFormula -> int
349
val lfGetDestAg : sort -> localFormula -> int array
350
val lfGetNeg : sort -> localFormula -> localFormula option
351
val lfGetAt : nominal -> localFormula -> atFormula
352
val lfToInt : localFormula -> int
353
val lfFromInt : int -> localFormula
354
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
355

    
356
val atFormulaGetSubformula : atFormula -> localFormula
357
val atFormulaGetNominal : atFormula -> nominal
358

    
359
val lfToAt : sort -> localFormula -> atFormula
360

    
361
val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
362
    CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
363