Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgMisc.mli @ 15537461

History | View | Annotate | Download (12.9 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
  | Monotone
16
  | CoalitionLogic
17
  | GML
18
  | PML
19
  | Constant of string list
20
  | Identity
21
  | DefaultImplication
22
  | Choice
23
  | Fusion
24

    
25
(* functors whose constructor takes additional parameters *)
26
type parametricFunctorName =
27
  | NameConstant
28

    
29
val functor_of_string : string -> string list -> functors option
30
val unaryfunctor_of_string : string -> string list -> functors option
31
val string_of_functor : functors -> string
32

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

    
59
type localFormula
60
type bset
61

    
62
type atFormula
63
type cset
64
type csetSet
65

    
66
type lht
67
type fht
68
type nht
69

    
70
type state
71

    
72
type core
73

    
74
type setState
75

    
76
type setCore
77

    
78
type setCnstr
79

    
80
(*****************************************************************************)
81
(*                Types that are hard coded into the algorithm               *)
82
(*****************************************************************************)
83

    
84
and 'a junction = | Disjunctive of 'a (*specifies that any of the 'a needs to be satifsfied *)
85
                  | Conjunctive of 'a (*specifies that all of the 'a need  to be satifsfied *)
86

    
87
and stateExpander = unit -> ruleEnumeration
88

    
89
and sort = CoAlgFormula.sort
90

    
91
and nodeStatus =
92
  | Expandable
93
  | Open
94
  | Sat
95
  | Unsat
96

    
97
and dependencies = bset list -> bset
98

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

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

    
106
(* a lazylist returns on successive calls the entire list until it eventually
107
   returns NoMoreElements
108
*)
109
and 'a lazylist = unit -> 'a lazyliststep
110

    
111
and ruleEnumeration = rule lazyliststep
112

    
113
val lazylistFromList : 'a list -> 'a lazylist
114

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

    
117
type nominal = sort * localFormula
118

    
119
type node =
120
  | State of state
121
  | Core of core
122

    
123
type constrnt =
124
  | UnsatC
125
  | SatC
126
  | OpenC of node list
127
  | UnexpandedC of node list
128

    
129
type propagateElement = (* TODO: What does the prefix "U" mean? unsat? *)
130
  | UState of state * int option
131
  | UCore of core * bool
132
  | UCnstr of cset
133

    
134
type queueElement =
135
  | QState of state
136
  | QCore of core
137
  | QCnstr of cset
138
  | QEmpty
139

    
140
type sortTable = (functors * int list) array
141

    
142
exception CoAlg_finished of bool
143

    
144

    
145
val sortTable : sortTable ref
146

    
147
(* evaluate a junction in the obvious way *)
148
val junctionEvalBool : bool list junction -> bool
149
val junctionEval: ('a -> bool) -> 'a list junction -> bool
150
val optionalizeOperator: ('a -> 'b -> 'c) -> ('a option -> 'b option -> 'c option)
151
val junctionEvalBoolOption : bool option list junction -> bool option
152

    
153
(* decompose a junction in it's content and its constructor,
154
   such that: eval∘junctionExtract = id
155
   (with eval: X × (X -> Y) -> Y)
156
 *)
157
val junctionExtract: 'a junction -> ('a * ('b -> 'b junction))
158

    
159
(*****************************************************************************)
160
(*      "Module type" and a specific implementation of the main queue        *)
161
(*****************************************************************************)
162

    
163
val queueInit : unit -> unit
164
val queueIsEmpty : unit -> bool
165
val queueInsertState : state -> unit
166
val queueInsertCore : core -> unit
167
val queueInsertCnstr : cset -> unit
168
val queueGetElement : unit -> queueElement
169
val queuePrettyStatus : unit -> string
170

    
171
val setPropagationCounter : int -> unit
172
val doNominalPropagation : unit -> bool
173
val doSatPropagation : unit -> bool
174

    
175

    
176
(*****************************************************************************)
177
(*        "Module type" and a specific implementation of the graph           *)
178
(*****************************************************************************)
179

    
180
val graphInit : unit -> unit
181
val graphIterStates : (state -> unit) -> unit
182
val graphIterCores : (core -> unit) -> unit
183
val graphIterCnstrs : (cset -> constrnt -> unit) -> unit
184
val graphClearCnstr : unit -> unit
185
val graphFindState : sort -> (bset * bset) -> state option
186
val graphFindCore : sort -> (bset * bset) -> core option
187
val graphFindCnstr : cset -> constrnt option
188
val graphInsertState : sort -> (bset * bset) -> state -> unit
189
val graphInsertCore : sort -> (bset * bset) -> core -> unit
190
val graphInsertCnstr : cset -> constrnt -> unit
191
val graphReplaceCnstr : cset -> constrnt -> unit
192
val graphSizeState : unit -> int
193
val graphSizeCore : unit -> int
194
val graphSizeCnstr : unit -> int
195
val graphAddRoot : core -> unit
196
val graphGetRoot : unit -> core
197

    
198

    
199
(*****************************************************************************)
200
(*     "Module type" and a specific implementation of sets of constraints    *)
201
(*****************************************************************************)
202

    
203
val cssEmpty : csetSet
204
val cssExists : (cset -> bool) -> csetSet -> bool
205
val cssForall : (cset -> bool) -> csetSet -> bool
206
val cssUnion : csetSet -> csetSet -> csetSet
207
val cssAdd : cset -> csetSet -> csetSet
208
val cssFold : (cset -> 'a -> 'a) -> csetSet -> 'a -> 'a
209
val cssSingleton : cset -> csetSet
210
val cssEqual : csetSet -> csetSet -> bool
211
val cssIter : (cset -> unit) -> csetSet -> unit
212

    
213
(*****************************************************************************)
214
(*      "Module type" and a specific implementation of state nodes           *)
215
(*****************************************************************************)
216

    
217
val stateMake : sort -> bset -> bset -> stateExpander -> state
218
val stateGetSort : state -> sort
219
val stateGetBs : state -> bset
220
val stateSetBs : state -> bset -> unit
221
val stateGetDeferral : state -> bset
222
val stateSetDeferral : state -> bset -> unit
223
val stateGetStatus : state -> nodeStatus
224
val stateSetStatus : state -> nodeStatus -> unit
225
val stateGetParents : state -> core list
226
val stateAddParent : state -> core -> unit
227
val stateGetRule : state -> int -> dependencies * core list
228
val stateGetRules : state -> (dependencies * core list) list
229
val stateAddRule : state -> dependencies -> core list -> int
230
val stateGetConstraints : state -> csetSet
231
val stateSetConstraints : state -> csetSet -> unit
232
val stateNextRule : state -> ruleEnumeration
233
val stateToString : state -> string
234
val stateToDot : state -> string
235
val stateGetIdx : state -> int
236

    
237

    
238
(*****************************************************************************)
239
(*      "Module type" and a specific implementation of core nodes            *)
240
(*****************************************************************************)
241

    
242
val coreMake : sort -> bset -> bset -> Minisat.solver option -> fht -> core
243
val coreGetSort : core -> sort
244
val coreGetBs : core -> bset
245
val coreSetBs : core -> bset -> unit
246
val coreGetDeferral : core -> bset
247
val coreSetDeferral : core -> bset -> unit
248
val coreGetStatus : core -> nodeStatus
249
val coreSetStatus : core -> nodeStatus -> unit
250
val coreGetParents : core -> (state * int) list
251
val coreAddParent : core -> state -> int -> unit
252
val coreGetChildren : core -> state list
253
val coreAddChild : core -> state -> unit
254
val coreGetConstraints : core -> csetSet
255
val coreSetConstraints : core -> csetSet -> unit
256
val coreGetSolver : core -> Minisat.solver option
257
val coreDeallocateSolver : core -> unit
258
val coreGetFht : core -> fht
259
val coreGetIdx : core -> int
260
val coreGetConstraintParents : core -> cset list
261
val coreAddConstraintParent : core -> cset -> unit
262
val coreToString : core -> string
263
val coreToDot : core -> string
264

    
265

    
266
(*****************************************************************************)
267
(*      "Module type" and a specific implementation of sets of               *)
268
(*      states, cores, and constraints for the sat propagation               *)
269
(*****************************************************************************)
270

    
271
val setEmptyState : unit -> setState
272
val setEmptyCore : unit -> setCore
273
val setCopyState : setState -> setState
274
val setCopyCore : setCore -> setCore
275
val setEmptyCnstr : unit -> setCnstr
276
val setAddState : setState -> state -> unit
277
val setAddCore : setCore -> core -> unit
278
val setAddCnstr : setCnstr -> cset -> unit
279
val setMemState : setState -> state -> bool
280
val setMemCore : setCore -> core -> bool
281
val setMemCnstr : setCnstr -> cset -> bool
282
val setRemoveState : setState -> state -> unit
283
val setRemoveCore : setCore -> core -> unit
284
val setRemoveCnstr : setCnstr -> cset -> unit
285
val setIterState : (state -> unit) -> setState -> unit
286
val setIterCore : (core -> unit) -> setCore -> unit
287
val setIterCnstr : (cset -> unit) -> setCnstr -> unit
288
val setLengthState : setState -> int
289
val setLengthCore : setCore -> int
290

    
291

    
292
(*****************************************************************************)
293
(*        "Module type" and a specific implementation of the mapping         *)
294
(*        between (local) formulae and literals of the sat solver,           *)
295
(*        and of a mapping of nominals to sets of formulae                   *)
296
(*****************************************************************************)
297

    
298
val lhtInit : unit -> lht
299
val lhtAdd : lht -> Minisat.lit -> localFormula -> unit
300
val lhtFind : lht -> Minisat.lit -> localFormula option
301

    
302
val fhtInit : unit -> fht
303
val fhtAdd : fht -> localFormula -> Minisat.lit -> unit
304
val fhtFind : fht -> localFormula -> Minisat.lit option
305

    
306
val nhtInit : unit -> nht
307
val nhtAdd : nht -> nominal -> bset -> unit
308
val nhtFind : nht -> nominal -> bset option
309
val nhtFold : (nominal -> bset -> 'a -> 'a) -> nht -> 'a -> 'a
310

    
311

    
312
(*****************************************************************************)
313
(*         "Module type" and a specific implementation of sets of            *)
314
(*         local formulae and @-formulae                                     *)
315
(*****************************************************************************)
316

    
317
val bsetMake : unit -> bset (* a new bset which only contains True *)
318
val bsetMakeRealEmpty : unit -> bset (* a new bset without containing True *)
319
val bsetAdd : bset -> localFormula -> unit
320
val bsetMem : bset -> localFormula -> bool
321
val bsetRem : bset -> int -> unit
322
val bsetCompare : bset -> bset -> int
323
val bsetRem : bset -> localFormula -> unit
324
val bsetFold : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
325
val bsetReplace : (localFormula -> 'a -> 'a) -> bset -> 'a -> 'a
326
val bsetIter : (localFormula -> unit) -> bset -> unit
327
val bsetFilter : bset -> (localFormula -> bool) -> bset
328
val bsetPartition : (localFormula -> bool) -> bset -> bset * bset
329
val bsetAddTBox : sort -> bset -> bset
330
val bsetCopy : bset -> bset
331
val bsetToString : sort -> bset -> string
332

    
333
val csetMake : unit -> cset
334
val csetAdd : cset -> atFormula -> unit
335
val csetCopy : cset -> cset
336
val csetUnion : cset -> cset -> cset
337
val csetHasDot : cset -> bool
338
val csetAddDot : cset -> unit
339
val csetRemDot : cset -> unit
340
val csetAddTBox : sort -> cset -> bset
341
val csetIter : cset -> (atFormula -> unit) -> unit
342
val csetToString : sort -> cset -> string
343

    
344

    
345
(*****************************************************************************)
346
(*            "Module type" and a specific implementation of                 *)
347
(*            local formulae and @-formulae                                  *)
348
(*****************************************************************************)
349

    
350
val lfGetType : sort -> localFormula -> formulaType
351
val lfGetDest1 : sort -> localFormula -> localFormula
352
val lfGetDest2 : sort -> localFormula -> localFormula
353
val lfGetDest3 : sort -> localFormula -> int
354
val lfGetDeferral : sort -> localFormula -> int
355
val lfGetDestNum : sort -> localFormula -> int
356
val lfGetDestNum2 : sort -> localFormula -> int
357
val lfGetDestAg : sort -> localFormula -> int array
358
val lfGetNeg : sort -> localFormula -> localFormula option
359
val lfGetAt : nominal -> localFormula -> atFormula
360
val lfToInt : localFormula -> int
361
val lfFromInt : int -> localFormula
362
val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
363

    
364
val atFormulaGetSubformula : atFormula -> localFormula
365
val atFormulaGetNominal : atFormula -> nominal
366

    
367
val lfToAt : sort -> localFormula -> atFormula
368

    
369
val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
370
    CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
371

    
372

    
373
val ppELFormulae : CoAlgFormula.sortedAxiom list -> CoAlgFormula.sort-> CoAlgFormula.formula -> CoAlgFormula.formula -> (bset * localFormula)
374

    
375
val lookup : sort -> localFormula -> bset option
376
val isNeg : sort -> localFormula -> bool
377
val unfold : sort -> bset -> bset