Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / coalgcompare.ml @ 7c4d2eb4

History | View | Annotate | Download (17.8 KB)

1 4fd28192 Thorsten Wißmann
(** This module generates coalgebraic formulae and queries, and runs solvers on them.
2
    The generated formulae contain randomly generated formulae
3
    as well as instances of certain classes of formulae.
4
    @author Florian Widmann
5
 *)
6
7
8
module G = GenAndComp
9
module C = CoAlgFormula
10
module A = ALCFormula
11
12 de854a5a Thorsten Wißmann
open CoolUtils
13
14
type solvanswer = ASAT | AUNSAT | ATIMEOUT | AFAILED
15
16 f725ccae Thorsten Wißmann
exception UserInterupt
17
18 de854a5a Thorsten Wißmann
let string_of_solvanswer a =
19
    match a with
20
    | ASAT -> "sat"
21
    | AUNSAT -> "unsat"
22
    | ATIMEOUT -> "timeout"
23
    | AFAILED -> "failed"
24 17ed0ef0 Thorsten Wißmann
25
type testresults =
26
   ((string list) (* solver names *)
27
    * ((string * ((solvanswer * int) list)) (*some test case with times for each reasoner*)
28
        list))
29
30 de854a5a Thorsten Wißmann
let debugMsg str =
31 c16fd631 Thorsten Wißmann
    prerr_endline (":: " ^ str)
32 de854a5a Thorsten Wißmann
33 f725ccae Thorsten Wißmann
let ptimeout = ref (300) (* default timeout in seconds *)
34
35
36 17ed0ef0 Thorsten Wißmann
(* generates the int range from i to j (including) *)
37
let (--) i j = 
38
    let rec aux n acc =
39
      if n < i then acc else aux (n-1) (n :: acc)
40
    in aux j []
41 4fd28192 Thorsten Wißmann
42
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
43
44
45 9b58f1e4 Thorsten Wißmann
(*
46 4fd28192 Thorsten Wißmann
let seed =
47
  Random.self_init (); 
48
  Random.int ((1 lsl 30) - 1)
49 9b58f1e4 Thorsten Wißmann
*)
50 4fd28192 Thorsten Wißmann
51 fbdaf510 Thorsten Wißmann
let pseed = ref (209314489)
52 4fd28192 Thorsten Wißmann
53 17ed0ef0 Thorsten Wißmann
let sortK = Array.make 1 (CoAlgMisc.MultiModalK, [0])
54 4fd28192 Thorsten Wißmann
55
let nomTable name =
56
  assert (CoAlgFormula.isNominal name);
57
  Some 0
58
59
60
(*
61
let maxCard = ref 100
62
63
let const_min r f =
64
  let card = (Random.int !maxCard) + 1 in
65
  C.const_min card r f
66
67
let const_max r f =
68
  let card = (Random.int (!maxCard+1)) in
69
  C.const_max card r f
70
 *)
71
72
let lFF = [(C.const_not, 1)]
73
let lFFF = [(C.const_or, 1); (C.const_and, 1)]
74
let lPFF = [(C.const_ex, 1); (C.const_ax, 1)]
75
76
let genFormula litFkt pFkt size =
77
  let nrLitsF = litFkt size in
78
  let lF =
79
    G.genLiterals ~litlst:[C.const_true; C.const_false] ~prio:10 C.const_ap "p" nrLitsF
80
  in
81
  let nrLitsP = pFkt size in
82
  let lP =
83
    if nrLitsP > 1 then G.genLiterals (fun x -> x) "a" nrLitsP
84
    else [("", 1)]
85
  in
86
  let genRF = fst (G.mk_generator lF lFF lFFF lPFF lP [] [] []) in
87
  genRF size
88
89
let genQuery litFkt pFkt tbcardFkt tbfsizeFkt size =
90
  let tbcard = tbcardFkt size in
91
  let tbfsize = tbfsizeFkt size in
92
  let tblitFkt n = litFkt size in
93
  let tbpFkt n = pFkt size in
94
  let tbox = ref [] in
95
  for i = 1 to tbcard do
96
    let tbf = genFormula tblitFkt tbpFkt tbfsize in
97
    tbox := (0, tbf)::!tbox
98
  done;
99
  let f = genFormula litFkt pFkt size in
100
  (!tbox, (0, f))
101
102
103
let rec exportALCFormula f =
104
  match f with
105
  | C.TRUE -> A.TRUE
106
  | C.FALSE -> A.FALSE
107
  | C.AP s when not (C.isNominal s) -> A.AP s
108
  | C.NOT f1 -> A.NOT (exportALCFormula f1)
109
  | C.OR (f1, f2) -> A.OR (exportALCFormula f1, exportALCFormula f2)
110
  | C.AND (f1, f2) -> A.AND (exportALCFormula f1, exportALCFormula f2)
111
  | C.EQU (f1, f2) -> A.EQU (exportALCFormula f1, exportALCFormula f2)
112
  | C.IMP (f1, f2) -> A.IMP (exportALCFormula f1, exportALCFormula f2)
113
  | C.EX (s, f1) -> A.EX (s, false, exportALCFormula f1)
114
  | C.AX (s, f1) -> A.AX (s, false, exportALCFormula f1)
115 06bd2098 Thorsten Wißmann
  | C.MIN (n, s, f1) -> A.MIN (n, s, false, exportALCFormula f1)
116
  | C.MAX (n, s, f1) -> A.MAX (n, s, false, exportALCFormula f1)
117
  | C.MORETHAN (n, s, f1) -> A.MIN (n+1, s, false, exportALCFormula f1)
118
  | C.MAXEXCEPT (n, s, f1) -> A.MAX (n, s, false, exportALCFormula (C.NOT f1))
119 4fd28192 Thorsten Wißmann
  | _ -> raise (C.CoAlgException "Formula is not expressible in ALC.")
120
121
let exportALCQuery tbox (_, f) =
122
  let tboxND = List.map (fun (_, f) -> exportALCFormula f) tbox in
123
  ([exportALCFormula f], tboxND, [])
124
125
126 17ed0ef0 Thorsten Wißmann
let solvCoalg sortTable args =
127
  G.evaluateFkt (fun (tbox, sf) -> CoAlgReasoner.isSat sortTable nomTable tbox sf) args
128 4fd28192 Thorsten Wißmann
129
let solvALC (tbox, sf) =
130
  let args = exportALCQuery tbox sf in
131
  G.evaluateFkt (fun (fl, tboxND, tboxD) -> ALCGraph.isSat fl tboxND tboxD) args
132
133 de854a5a Thorsten Wißmann
let solvFact (tbox, sf) timeout =
134 4fd28192 Thorsten Wißmann
  let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
135
  A.createFactTBox "fact.tbox" fl tboxND tboxD;
136 7993e0bf Thorsten Wißmann
  let fact = "./FaCT++" in
137 de854a5a Thorsten Wißmann
  let reg = "is satisfiable" in
138
  let call () = G.callExt None fact ["fact.conf"] (Str.regexp_string reg) timeout in
139
  let ignore_exception = false in
140
  if ignore_exception then try call () with _ -> (G.FAILED, -1.0, 0)
141
                      else call ()
142 4fd28192 Thorsten Wißmann
143 01b1ab69 Thorsten Wißmann
let solvTatl agents (tbox,(_,sf)) timeout = (* ignore the TBox... *)
144
  let tatl = "./tatl" in
145 53e9b267 Thorsten Wißmann
  let tboxlist = List.map (fun (_,f) -> CoAlgFormula.exportTatlFormula f) tbox in
146
  let agstr = String.concat "," (List.map string_of_int agents) in
147
  let tboxstr = "~<<"^agstr^">>F~ ("^(String.concat " /\\ " tboxlist) ^ ") /\\ " in
148
  let inp = CoAlgFormula.exportTatlFormula sf in
149
  let inp = if TList.empty tbox then inp else (tboxstr ^ "(" ^ inp ^ ")") in
150 064f3099 Thorsten Wißmann
  G.callExt (Some ("1\n"^inp^"\n4")) tatl [] (Str.regexp_string "The formula is satisfiable") timeout
151 f725ccae Thorsten Wißmann
152 b59059c4 Thorsten Wißmann
let solvCool functorname (tbox,sf) timeout =
153
  let inp = CoAlgFormula.exportQueryParsable tbox sf in
154
  G.callExt (Some inp) "./coalg" ["sat"; functorname] (Str.regexp_string "1: satisfiable") timeout
155
156
let solvCoolCL = solvCool "CL"
157 f725ccae Thorsten Wißmann
158 4fd28192 Thorsten Wißmann
let solvers =
159 17ed0ef0 Thorsten Wißmann
  let _ = [(solvCoalg sortK, "CoAlg"); (solvALC, "alc"); (solvFact, "fact")] in
160
  [(solvFact, "fact"); (solvCoalg sortK, "CoAlg")]
161
162
let printUsage () =
163 fbdaf510 Thorsten Wißmann
  print_endline "Usage: \"coalgcompare [<flags>] <logic> <logicargs>\" does tests where";
164
  print_endline "       <flags> in { --seed INITIALSEED }";
165
  print_endline "       <logic> in {";
166 b59059c4 Thorsten Wißmann
  print_endline "                     K <formula counts in tbox> <list of sizes>";
167
  print_endline "                     (e.g. »K 0,5,10 10000,15000,20000«)";
168 fbdaf510 Thorsten Wißmann
  print_endline "                     genCL <agents> <list of sizes>";
169
  print_endline "                     (e.g. »genCL 1,2,3 4000,42«)";
170
  print_endline "                  }";
171 17ed0ef0 Thorsten Wißmann
  exit 1
172
173 f725ccae Thorsten Wißmann
let runTests solvs formulas timeout : testresults =
174
  let reasonerNames = List.map (fun (_,s) -> s) solvs in
175
  let fillCell (fn,formula) (solver,sn) =
176
    debugMsg ("running " ^ sn ^ " on " ^ fn);
177 b59059c4 Thorsten Wißmann
    let (res, time, _) = solver formula timeout in
178 f725ccae Thorsten Wißmann
    let answer = match res with
179
                 | G.FINISHED (v) -> if (v) then ASAT else AUNSAT
180
                 | G.TIMED_OUT -> ATIMEOUT
181
                 | G.FAILED -> AFAILED
182
    in
183
    (answer, int_of_float time)
184
  in
185
  let interrupted = ref (false) in
186
  let do_line (str,f) = if not !interrupted then
187
                            try (str,List.map (fun s -> fillCell (str,f) s) solvs)
188
                            with UserInterupt -> (interrupted := true; ("",[]))
189
                        else ("",[])
190
  in
191
  let results = List.filter (fun (_,cols) -> match cols with
192
                                             | (_::_) -> true
193
                                             | [] -> false)
194
                            (List.map do_line formulas)
195
  in
196
  (reasonerNames,results)
197
198
199 b59059c4 Thorsten Wißmann
let doTestK (tboxsizes:int list) (szlist:int list) : testresults =
200
  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
201 17ed0ef0 Thorsten Wißmann
  (*
202
    lF A list of pairs (f, n), e.g. (p, 1).
203
    The list must not be empty.
204
    lFF A list of pairs (f->f, n), e.g. (~., 1).
205
    The list must not be empty.
206
    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
207
    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
208
    lP A list of pairs (p, n), e.g. (a, 1).
209
    The list must not be empty unless lPFF is also empty.
210
    lPP A list of pairs (p->p, n), e.g. ( *., 1).
211
    lFP A list of pairs (f->p, n), e.g. (?., 1).
212
    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
213
  *)
214 f725ccae Thorsten Wißmann
  let timeout = !ptimeout in (* 5 minutes *)
215 ad63163e Thorsten Wißmann
  let lF = List.map (fun p -> C.AP ("p"^(string_of_int p))) (1--3) in
216
  let lF = List.append lF (List.map (C.const_not) lF) in
217
  let lF = C.TRUE :: C.FALSE :: lF in
218
  let lF = List.map (fun v -> (v,1)) lF in
219
  let roles : string list = List.map (fun p -> "R"^(string_of_int p)) (1--3) in
220
  let exs : (C.formula -> C.formula) list = List.map C.const_ex roles in
221
  let axs : (C.formula -> C.formula) list = List.map C.const_ax roles in
222
  let lFF = List.map (fun v -> (v,1)) (List.append exs axs) in
223
  let lFFF : (C.formula -> C.formula -> C.formula) list = List.append
224
                (List.map (fun x y z -> x (C.const_and y z)) exs)
225
                (List.map (fun x y z -> x (C.const_or y z))  axs)
226
  in
227
  let lFFF = List.map (fun v -> (v,1)) lFFF in
228
  let (genF,_) = G.mk_generator lF lFF lFFF [] [] [] [] [] in
229 2cef7a7c Thorsten Wißmann
  let reasonerNames = List.map (fun (_,s) -> s) solvs in
230 b59059c4 Thorsten Wißmann
  let s1 = 0 in (* probably the correct formula... *)
231
  let formulas = List.map (fun (sz,cnt) ->
232
                            let tbox = List.map (fun _ -> (s1,genF sz)) (1 -- cnt) in
233
                            ("sz"^(string_of_int sz)^"tb"^(string_of_int cnt),(tbox,(s1,genF sz)))
234
                          ) (TList.prod szlist tboxsizes) in
235
  runTests solvs formulas timeout
236 4fd28192 Thorsten Wißmann
237 b09ef622 Thorsten Wißmann
let doTestGenericGML () : testresults =
238 06bd2098 Thorsten Wißmann
  let solvs = [(solvFact, "fact"); (solvCool "GML", "cool")] in
239 b09ef622 Thorsten Wißmann
  let timeout = !ptimeout in (* 5 minutes *)
240
  let formulas = ref [] in
241
  let counter = ref 0 in
242
  let s1 = 0 in
243
  (try
244
    while true do
245
      let input = read_line () in
246
      if not (GenAndComp.isEmptyString input) then
247
        let (tbox, f) = CoAlgFormula.importQuery input in
248
        incr counter;
249
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
250
        formulas := test::(!formulas)
251
      else ()
252
    done
253
  with End_of_file -> ());
254
  let formulas = List.rev !formulas in
255
  runTests solvs formulas timeout
256
257
258 9c2018ff Thorsten Wißmann
let doTestGenericK () : testresults =
259
  let solvs = [(solvFact, "fact"); (solvCool "K", "cool")] in
260
  let timeout = !ptimeout in (* 5 minutes *)
261
  let formulas = ref [] in
262
  let counter = ref 0 in
263
  let s1 = 0 in
264
  (try
265
    while true do
266
      let input = read_line () in
267
      if not (GenAndComp.isEmptyString input) then
268
        let (tbox, f) = CoAlgFormula.importQuery input in
269
        incr counter;
270
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
271
        formulas := test::(!formulas)
272
      else ()
273
    done
274
  with End_of_file -> ());
275
  let formulas = List.rev !formulas in
276
  runTests solvs formulas timeout
277
278
279
280 8e79646a Thorsten Wißmann
let doTestGenericCL () : testresults =
281 01b1ab69 Thorsten Wißmann
  let agents = [1;2;3;4;5] in
282 14f2b341 Thorsten Wißmann
  let solvs = [(solvTatl agents, "tatl"); (solvCoolCL, "cool")] in
283 8e79646a Thorsten Wißmann
  let timeout = !ptimeout in (* 5 minutes *)
284
  let formulas = ref [] in
285
  let counter = ref 0 in
286
  let s1 = 0 in
287
  (try
288
    while true do
289
      let input = read_line () in
290
      if not (GenAndComp.isEmptyString input) then
291
        let (tbox, f) = CoAlgFormula.importQuery input in
292
        incr counter;
293
        let test = ("line" ^ (string_of_int !counter), (tbox,f)) in
294
        formulas := test::(!formulas)
295
      else ()
296
    done
297
  with End_of_file -> ());
298
  let formulas = List.rev !formulas in
299
  runTests solvs formulas timeout
300
301
302
303 de854a5a Thorsten Wißmann
let printRawData ((rn,results):testresults) : unit =
304
    let doubler l = List.fold_right (fun a b -> (a ^ "_state")::(a^"_time")::b) l [] in
305
    print_endline (String.concat ";" ("formula"::doubler rn)) ;
306
    let format_cell (stat,time) = (string_of_solvanswer stat) ^ ";" ^ (string_of_int time) in
307
    let format_line (fn,res) = fn ^ ";" ^ (String.concat ";" (List.map format_cell res)) in
308
    let lines = List.map format_line results in
309
    print_endline (String.concat "\n" lines)
310
311 01b1ab69 Thorsten Wißmann
let doTestCL agents formulas : testresults =
312 14f2b341 Thorsten Wißmann
  let solvs = [(solvTatl agents, "tatl"); (solvCoolCL, "cool")] in
313 f725ccae Thorsten Wißmann
  runTests solvs formulas !ptimeout
314
315
let doGenCL aglist sizelist : CoAlgFormula.formula list =
316 7993e0bf Thorsten Wißmann
  (*
317
    lF A list of pairs (f, n), e.g. (p, 1).
318
    The list must not be empty.
319
    lFF A list of pairs (f->f, n), e.g. (~., 1).
320
    The list must not be empty.
321
    lFFF A list of pairs (f->f->f, n), e.g. (.&., 1).
322
    lPFF A list of pairs (p->f->f, n), e.g. (<.>., 1).
323
    lP A list of pairs (p, n), e.g. (a, 1).
324
    The list must not be empty unless lPFF is also empty.
325
    lPP A list of pairs (p->p, n), e.g. ( *., 1).
326
    lFP A list of pairs (f->p, n), e.g. (?., 1).
327
    lPPP A list of pairs (p->p->p, n), e.g. (.+., 1).
328
  *)
329 c16fd631 Thorsten Wißmann
  let lF = List.map (fun p -> (C.AP ("p"^(string_of_int p)), 1)) (1--3) in
330 7993e0bf Thorsten Wißmann
  let lFF = [(C.const_not,1)] in
331 c16fd631 Thorsten Wißmann
  let lFFF = [(C.const_and,1)] in (* Warning: This forbids disjunctions! *)
332 7993e0bf Thorsten Wißmann
  let lPFF = [(C.const_enforces,1); (C.const_allows, 1)] in
333
  (* role names *)
334
  let lP = List.map (fun p -> (p, 1)) (TList.powerset aglist) in
335
  let lPP : ((int list -> int list) * int) list= [] in
336
  let lFP = [] in
337
  let lPPP = [] in
338
  let (genF,_) = G.mk_generator lF lFF lFFF lPFF lP lPP lFP lPPP in
339 f725ccae Thorsten Wißmann
  List.map (fun sz -> (genF sz)) sizelist
340 de854a5a Thorsten Wißmann
341 17ed0ef0 Thorsten Wißmann
let _ =
342 3068712a Thorsten Wißmann
    let argidx = ref (1) in
343 fbdaf510 Thorsten Wißmann
    let fail str = (prerr_endline str ; printUsage ()) in
344 3068712a Thorsten Wißmann
    let getarg () =
345 c16fd631 Thorsten Wißmann
        if !argidx >= Array.length Sys.argv then (fail "Error: Missing argument ") else ();
346 3068712a Thorsten Wißmann
        let str = Sys.argv.(!argidx) in
347
        argidx := 1 + !argidx;
348
        str
349
    in
350 fbdaf510 Thorsten Wißmann
    let pcmd = ref (getarg ()) in
351
    let rec parseflags () =
352
        match !pcmd with
353
        | "--seed" -> (pseed := (int_of_string (getarg ()));
354
                       pcmd := getarg ();
355
                       parseflags ())
356 f725ccae Thorsten Wißmann
        | "--timeout" -> (ptimeout := (int_of_string (getarg ()));
357
                       pcmd := getarg ();
358
                       parseflags ())
359 fbdaf510 Thorsten Wißmann
        | _ -> ()
360
    in
361
    parseflags ();
362
    Random.init !pseed;
363 f725ccae Thorsten Wißmann
    let alarmHandler (n : int) = raise G.Timeout in
364 b59059c4 Thorsten Wißmann
    let sigintHandler (n : int) = prerr_endline "" ; raise UserInterupt in
365 f725ccae Thorsten Wißmann
    let oldHandler = Sys.signal Sys.sigalrm (Sys.Signal_handle alarmHandler) in
366
    let oldSigint = Sys.signal Sys.sigint (Sys.Signal_handle sigintHandler) in
367 fbdaf510 Thorsten Wißmann
    debugMsg ("seed is " ^ (string_of_int (!pseed)));
368
    let cmd = !pcmd in
369 f725ccae Thorsten Wißmann
    (
370 fbdaf510 Thorsten Wißmann
    match cmd with
371 b59059c4 Thorsten Wißmann
    | "K" ->
372
             let tboxsizes = intlist_of_string (getarg ()) in
373
             let szlist = intlist_of_string (getarg()) in
374
             printRawData (doTestK tboxsizes szlist)
375 9c2018ff Thorsten Wißmann
    | "genericK" ->
376
            printRawData (doTestGenericK ())
377 b09ef622 Thorsten Wißmann
    | "genericGML" ->
378
            printRawData (doTestGenericGML ())
379 8e79646a Thorsten Wißmann
    | "genericCL" ->
380
            printRawData (doTestGenericCL ())
381 b59059c4 Thorsten Wißmann
    | "CL1" -> let sz = (5000 -- 5080) in
382 01b1ab69 Thorsten Wißmann
               let agents = [1;2;3;4;5] in
383 b59059c4 Thorsten Wißmann
               let ats (str,f) = (str, ([], (0, f))) in (* add tbox and sort *)
384 01b1ab69 Thorsten Wißmann
               printRawData (doTestCL agents (List.map ats (TList.zip (List.map string_of_int sz) (doGenCL agents sz))))
385 3068712a Thorsten Wißmann
    | "genCL" -> let p1 = getarg () in
386
                 let p2 = getarg () in
387 f725ccae Thorsten Wißmann
                 let forms = doGenCL (intlist_of_string p1) (intlist_of_string p2) in
388
                 List.iter (fun f -> print_endline (CoAlgFormula.exportFormula f)) forms
389 2cef7a7c Thorsten Wißmann
    | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Logic name »" ^ (Sys.argv.(1)) ^ "«"))
390 f725ccae Thorsten Wißmann
    );
391
    Sys.set_signal Sys.sigalrm oldHandler;
392
    Sys.set_signal Sys.sigint oldSigint
393 4fd28192 Thorsten Wißmann
394
395 9e70511b Thorsten Wißmann
(*
396 17ed0ef0 Thorsten Wißmann
let expQ (tbox, sf) = C.exportQuery tbox sf
397
398 4fd28192 Thorsten Wißmann
let rateF = int_of_string Sys.argv.(1)
399
let rateP = int_of_string Sys.argv.(2)
400
let nr = int_of_string Sys.argv.(3)
401
let start = int_of_string Sys.argv.(4)
402
let stop = int_of_string Sys.argv.(5)
403
let step = int_of_string Sys.argv.(6)
404
405
let litFkt n = n / rateF
406
let pFkt n = n / rateP
407
let tbcardFkt n = 0
408
let tbfsizeFkt n = max 1 (n / 10)
409
410
let genQ = genQuery litFkt pFkt tbcardFkt tbfsizeFkt
411
412
let _ = G.toGnuPlot ~dots:10 ~timeout:10 ~fail:true expQ genQ solvers nr start stop ((+) step)
413
414 9e70511b Thorsten Wißmann
*)
415 4fd28192 Thorsten Wißmann
416
(*
417
let files = [ ("benchmarks/DL98/DL98_alc_branch_sat.txt", "branch\\_n");
418
              ("benchmarks/DL98/DL98_alc_branch_unsat.txt", "branch\\_p");
419
              ("benchmarks/DL98/DL98_alc_d4_sat.txt", "d4\\_n");
420
              ("benchmarks/DL98/DL98_alc_d4_unsat.txt", "d4\\_p");
421
              ("benchmarks/DL98/DL98_alc_dum_sat.txt", "dum\\_n");
422
              ("benchmarks/DL98/DL98_alc_dum_unsat.txt", "dum\\_p");
423
              ("benchmarks/DL98/DL98_alc_grz_sat.txt", "grz\\_n");
424
              ("benchmarks/DL98/DL98_alc_grz_unsat.txt", "grz\\_p");
425
              ("benchmarks/DL98/DL98_alc_lin_sat.txt", "lin\\_n");
426
              ("benchmarks/DL98/DL98_alc_lin_unsat.txt", "lin\\_p");
427
              ("benchmarks/DL98/DL98_alc_path_sat.txt", "path\\_n");
428
              ("benchmarks/DL98/DL98_alc_path_unsat.txt", "path\\_p");
429
              ("benchmarks/DL98/DL98_alc_ph_sat.txt", "ph\\_n");
430
              ("benchmarks/DL98/DL98_alc_ph_unsat.txt", "ph\\_p");
431
              ("benchmarks/DL98/DL98_alc_poly_sat.txt", "poly\\_n");
432
              ("benchmarks/DL98/DL98_alc_poly_unsat.txt", "poly\\_p");
433
              ("benchmarks/DL98/DL98_alc_t4p_sat.txt", "t4p\\_n");
434
              ("benchmarks/DL98/DL98_alc_t4p_unsat.txt", "t4p\\_p") ]
435
436
let prebenchmarks =
437
  let mapB (filename, lab) =
438
    let file = open_in filename in
439
    let res = ref [] in
440
    let _ =
441
      try
442
        while true do
443
          let input = input_line file in
444
          if not (G.isEmptyString input) then
445
            let q = C.importQuery input in
446
            res := q::!res
447
          else ()
448
        done
449
      with End_of_file -> ()
450
    in
451
    (List.rev !res, lab)
452
  in
453
  List.map mapB files
454
455
let benchmarks =
456
  List.map (fun f -> fun () -> f) (List.flatten (List.map (fun (fl, _) -> fl) prebenchmarks))
457
458
let labels = List.map (fun (fl, lab) -> (List.length fl, lab)) prebenchmarks
459
460
let timeouts = [ 1; 2; 4; 8; 15; 30; 60 ]
461
462
let _ = G.outputBenchmarks ~fail:true expQ solvers timeouts benchmarks labels
463
 *)
464
465
let logicFkts = {
466
  G.l_tt = C.TRUE;
467
  G.l_ff = C.FALSE;
468
  G.l_ap = (fun s i -> C.AP (s ^ (string_of_int i)));
469
  G.l_not = C.const_not;
470
  G.l_and = C.const_and;
471
  G.l_or = C.const_or;
472
  G.l_imp = C.const_imp;
473
  G.l_aa = (fun s i -> s ^ (string_of_int i));
474
  G.l_box = C.const_ax;
475
  G.l_dia = C.const_ex;
476
  G.l_aw = (fun _ _ -> raise (C.CoAlgException "not implemented"));
477
  G.l_ev = (fun _ _ -> raise (C.CoAlgException "not implemented"));
478
  G.l_until = (fun _ _ -> raise (C.CoAlgException "not implemented"))
479
}
480
481
(*
482
let m = int_of_string Sys.argv.(1)
483
let k = int_of_string Sys.argv.(2)
484
485
let wrapSorts (f, tbox) =
486
  let tbox1 = List.map (fun f -> (0, f)) tbox in
487
  (tbox1, (0, f))
488
489
let (tbox, sf) =
490
  let (concl, tbox) = G.mk_wisemen_tbox logicFkts m k in
491
  wrapSorts (C.NOT concl, tbox)
492
493
let (tbox, sf) =
494
  let (concl, tbox) = G.mk_muddychildren_tbox logicFkts m k in
495
  wrapSorts (C.NOT concl, tbox)
496
497
let (tbox, sf) = wrapSorts (G.mk_exptime_tbox logicFkts m false)
498
499
let _ = CoAlgReasoner.isSat ~verbose:true sorts nomTable tbox sf
500
let _ =
501
  let (fl, tboxND, tboxD) = exportALCQuery tbox sf in
502
  ALCGraph.isSat ~verbose:true fl tboxND tboxD
503
 *)