Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / coalg / coalg.ml @ 1d36cd07

History | View | Annotate | Download (12.9 KB)

1 4fd28192 Thorsten Wißmann
(** Accepts formulae from the standard input and tests them for satisfiability.
2
    Each formula has to be on a separate line and empty lines are ignored.
3
    The input is terminated by EOF.
4
    @author Florian Widmann
5
 *)
6
7 4fd82fa1 Thorsten Wißmann
module CM = CoAlgMisc
8 46d4b2bf Thorsten Wißmann
module CF = CoAlgFormula
9 200774f4 Kristin Braun
module EA = EAFormula
10 def3763d Kristin Braun
module NF = Nom2fix
11 58c30aee Thorsten Wißmann
12 3879f710 Thorsten Wißmann
module FE = FunctorParsing
13
14 58c30aee Thorsten Wißmann
open CoolUtils
15 4fd28192 Thorsten Wißmann
16
(* A partial function mapping nominals to their sorts. *)
17
let nomTable name =
18
  assert (CoAlgFormula.isNominal name);
19
  Some 0
20
21
22
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
23
24 4c23563e Hans-Peter Deifel
type options =
25
  { verbose : bool
26 f24367c4 Hans-Peter Deifel
  ; fragment : CM.fragment_spec
27 4c23563e Hans-Peter Deifel
  }
28
29 f24367c4 Hans-Peter Deifel
let defaultOpts = { verbose = false; fragment = CM.Auto }
30 4c23563e Hans-Peter Deifel
31
let options =
32
  [ { Args.long = "verbose"
33
    ; Args.short = Some 'v'
34
    ; Args.description = "print verbose output with statistics"
35 f24367c4 Hans-Peter Deifel
    ; Args.argument = Args.No_arg (fun a -> { a with verbose = true })
36 4c23563e Hans-Peter Deifel
    }
37
  ; { Args.long = "agents"
38
    ; Args.short = None
39
    ; Args.description = "expects the next argument AGLIST to be a list of integers\n"
40
                    ^ "which is treaten as the set of agents for CL formulas\n"
41
                    ^ "it defaults to 1,2,3,4,5,6,7,8,9,10"
42
    ; Args.argument =
43
        let parse_agents strAglist =
44
          let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
45
          CoolUtils.cl_set_agents (Array.of_list aglist)
46
        in
47
        Args.Required_arg ("AGLIST", fun s a -> parse_agents s; a)
48
    }
49 f24367c4 Hans-Peter Deifel
  ; { Args.long = "fragment"
50
    ; Args.short = None
51
    ; Args.description = "Use reasoner algorithm specialized to FRAGMENT.\n"
52
                         ^ "Possible values are: auto, altfree, altfreeaconj\n"
53
                         ^ "where \"auto\" detects the fragment from the given formulas"
54
    ; Args.argument =
55
        let parse_fragment s = match s with
56
          | "auto" -> CM.Auto
57
          | "altfree" -> CM.Fragment CM.AlternationFree
58
          | "altfreeaconj" -> CM.Fragment CM.AconjunctiveAltFree
59
          | _ -> raise (Args.ParseError ("Unknown fragment " ^ s))
60
        in
61
        Args.Required_arg
62
          ("FRAGMENT", fun s a -> { a with fragment = parse_fragment s })
63
    }
64 4c23563e Hans-Peter Deifel
  ]
65 4fd28192 Thorsten Wißmann
66 cf70b199 Hans-Peter Deifel
let printUsage name =
67
  print_endline ("Usage: \"" ^ name ^ " <task> <functor> [<flags>]\" where");
68 d5e292c6 Kristin Braun
  print_endline "       <task> in { sat print graph verify nnf prov (is »not.(sat ¬f)«) nom2fix solveNom}";
69 3e5fbf7e Thorsten Wißmann
  print_endline "       <functor> in { MultiModalK (or equivalently K)";
70
  print_endline "                      MultiModalKD (or equivalently KD)";
71 f4e43751 Christoph Egger
  print_endline "                      Monotone";
72 3e5fbf7e Thorsten Wißmann
  print_endline "                      CoalitionLogic (or equivalently CL)";
73 19f5dad0 Dirk Pattinson
  print_endline "                      Const id1 ... idn (or equivalently Constant id1 ... idn)";
74
  print_endline "                      Id (or equivalently Identity)";
75 b03cc745 Thorsten Wißmann
  print_endline "                    }";
76 3e5fbf7e Thorsten Wißmann
  print_endline "                 where you can compose functors by:";
77
  print_endline "                    <functor> + <functor> (weakest precedence)";
78 b03cc745 Thorsten Wißmann
  print_endline "                 or <functor> * <functor>";
79 3e5fbf7e Thorsten Wißmann
  print_endline "                 or <functor> . <functor> (binds strongest)";
80 c4aee922 Hans-Peter Deifel
  print_endline "                 (so K+KD.CL*Id stand for (K + ((KD.CL) * Id)))";
81 845adfba Thorsten Wißmann
  print_endline "       <flags> = a list of the following items";
82 4c23563e Hans-Peter Deifel
  Args.help stdout 11 options;
83 4fd82fa1 Thorsten Wißmann
  print_endline "";
84 19f5dad0 Dirk Pattinson
  print_endline "Problems are read from standard input and have the form";
85
  print_endline "       [ ass_1; .. ; ass_n |- ] concept";
86
  print_endline "where concept, ass_1, ..., ass_n are formulae (hypothesis";
87
  print_endline "and TBox assumptions) built using";
88
  print_endline "    True, False, ident (atomic proposition), ident' (nominal)";
89
  print_endline "    <=> (equivalence), => (implication), | (or), & (and), ~ (not)";
90
  print_endline "    @ ident' (satisfaction operator)";
91
  print_endline "    [R], <R> (universal/existential restrictions along role R";
92
  print_endline "    [{ aglist }], <{ aglist }> (aglist can force / cannot avoid)";
93
  print_endline "    =ident (constant value)";
94
  print_endline "    O (identity operator)";
95
  print_endline "    _ + _ (choice)";
96
  print_endline "    [pi1], [pi2] (fusion)";
97
  print_endline "";
98 4fd82fa1 Thorsten Wißmann
  print_endline "Examples:";
99
  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
100
  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
101 a9243a88 Thorsten Wißmann
  print_endline "  OCAMLRUNPARAM=b ./coalg sat 'K + KD' <<< '(([R] False) + ([R] False))'";
102 4fd82fa1 Thorsten Wißmann
  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash";
103 4fd28192 Thorsten Wißmann
  exit 1
104
105
let counter = ref 0
106
107 4c23563e Hans-Peter Deifel
let choiceSat opts =
108
    let verb = opts.verbose in
109 b03cc745 Thorsten Wißmann
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
110 267e3fcf Kristin Braun
    
111 5736aabb Hans-Peter Deifel
    (* test if GML or PML occurs in sort table *)
112
    if Array.fold_left (fun x (func,_) -> x || func == CM.GML || func == CM.PML) false sorts then
113 c4aee922 Hans-Peter Deifel
      raise (CF.CoAlgException "GML and PML are currently not supported")
114
    else ();
115 5736aabb Hans-Peter Deifel
116 4fd28192 Thorsten Wißmann
    let printRes sat =
117
      if not verb then
118
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
119
      else ()
120
    in
121
    try
122
      while true do
123
        let input = read_line () in
124
        if not (GenAndComp.isEmptyString input) then
125 46d4b2bf Thorsten Wißmann
          let (tbox, f) = CoAlgFormula.importQuery input in
126 4fd28192 Thorsten Wißmann
          incr counter;
127
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
128
          flush stdout;
129 f24367c4 Hans-Peter Deifel
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f)
130 7aa620ce Thorsten Wißmann
        else ()
131
      done
132
    with End_of_file -> ()
133
134 4c23563e Hans-Peter Deifel
let choiceProvable opts =
135
    let verb = opts.verbose in
136 46d4b2bf Thorsten Wißmann
    let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
137
        (s,CF.NOT f)
138
    in
139 b03cc745 Thorsten Wißmann
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
140 46d4b2bf Thorsten Wißmann
    let printRes sat =
141
      if not verb then
142
        print_endline (if not sat then "provable\n" else "unprovable\n")
143
      else ()
144
    in
145
    try
146
      while true do
147
        let input = read_line () in
148
        if not (GenAndComp.isEmptyString input) then
149
          let (tbox,f) = CoAlgFormula.importQuery input in
150
          let fneg = sorted_not f in
151
          incr counter;
152
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
153
          flush stdout;
154 f24367c4 Hans-Peter Deifel
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg)
155 46d4b2bf Thorsten Wißmann
        else ()
156
      done
157
    with End_of_file -> ()
158 1ec1a764 Thorsten Wißmann
159 4c23563e Hans-Peter Deifel
let choicePrint opts =
160 7aa620ce Thorsten Wißmann
    try
161
      while true do
162
        let input = read_line () in
163
        if not (GenAndComp.isEmptyString input) then
164
          let f = CoAlgFormula.importFormula input in
165
          let str = CoAlgFormula.exportFormula f in
166
          incr counter;
167
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
168
          flush stdout;
169 4fd28192 Thorsten Wißmann
        else ()
170
      done
171
    with End_of_file -> ()
172 7aa620ce Thorsten Wißmann
173 1d36cd07 Kristin Braun
let choiceApprox opts =
174
  let verb = opts.verbose in
175
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
176
    let printRes sat =
177
      if not verb then
178
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
179
      else ()
180
    in
181
    try
182
      while true do
183
        let input = read_line () in
184
        if not (GenAndComp.isEmptyString input) then
185
          let (s, fo) = CoAlgFormula.importSortedFormula input in
186
          let (tbox, fu) = CoAlgFormula.importQuery input in
187
          let g = Nom2fix.translate fo nomTable sorts s true in
188
          let f = Nom2fix.delFix g in
189
          let str = CoAlgFormula.exportFormula f in
190
          incr counter;
191
          print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
192
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
193
          flush stdout;
194
        else ()
195
      done
196
    with End_of_file -> ()
197
198 2d58f46f Kristin Braun
let choiceNom2fixNonOpt opts =
199
  let verb = opts.verbose in
200
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
201
    let printRes sat =
202
      if not verb then
203
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
204
      else ()
205
    in
206
  (*CoAlgMisc.sortTable = ref sorts;*)
207
  try
208
    while true do
209
      let input = read_line () in
210
      if not (GenAndComp.isEmptyString input) then
211
        let (s, f) = CoAlgFormula.importSortedFormula input in
212
        let (tbox, fu) = CoAlgFormula.importQuery input in
213
        let g = Nom2fix.translate f nomTable sorts s false in
214
        let str = CoAlgFormula.exportFormula g in
215
        incr counter;
216
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
217
        flush stdout;
218
      else ()
219
    done
220
  with End_of_file -> ()
221
222 4c23563e Hans-Peter Deifel
let choiceNom2fix opts =
223 946e8213 Kristin Braun
  let verb = opts.verbose in
224 89613c41 Kristin Braun
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
225 946e8213 Kristin Braun
    let printRes sat =
226
      if not verb then
227
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
228
      else ()
229
    in
230 89613c41 Kristin Braun
  (*CoAlgMisc.sortTable = ref sorts;*)
231 b81e4887 Hans-Peter Deifel
  try
232
    while true do
233
      let input = read_line () in
234
      if not (GenAndComp.isEmptyString input) then
235 946e8213 Kristin Braun
        let (s, f) = CoAlgFormula.importSortedFormula input in
236
        let (tbox, fu) = CoAlgFormula.importQuery input in
237 2d58f46f Kristin Braun
        let g = Nom2fix.translate f nomTable sorts s true in
238
        let str = CoAlgFormula.exportFormula g in
239
        incr counter;
240 bc0691dc Kristin Braun
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
241 2d58f46f Kristin Braun
        flush stdout;
242
      else ()
243
    done
244
  with End_of_file -> ()
245
246
let choiceSolveNomNonOpt opts =
247
  let verb = opts.verbose in
248
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
249
    let printRes sat =
250
      if not verb then
251
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
252
      else ()
253
    in
254
  (*CoAlgMisc.sortTable = ref sorts;*)
255
  try
256
    while true do
257
      let input = read_line () in
258
      if not (GenAndComp.isEmptyString input) then
259
        let (s, f) = CoAlgFormula.importSortedFormula input in
260
        let (tbox, fu) = CoAlgFormula.importQuery input in
261
        let g = Nom2fix.translate f nomTable sorts s false in
262 def3763d Kristin Braun
        let str = CoAlgFormula.exportFormula g in
263 b81e4887 Hans-Peter Deifel
        incr counter;
264
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
265 2d58f46f Kristin Braun
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
266 d5e292c6 Kristin Braun
        flush stdout;
267
      else ()
268
    done
269
  with End_of_file -> ()
270
271
let choiceSolveNom opts =
272
  let verb = opts.verbose in
273
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
274
    let printRes sat =
275
      if not verb then
276
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
277
      else ()
278
    in
279
  (*CoAlgMisc.sortTable = ref sorts;*)
280
  try
281
    while true do
282
      let input = read_line () in
283
      if not (GenAndComp.isEmptyString input) then
284
        let (s, f) = CoAlgFormula.importSortedFormula input in
285
        let (tbox, fu) = CoAlgFormula.importQuery input in
286 2d58f46f Kristin Braun
        let g = Nom2fix.translate f nomTable sorts s true in
287 d5e292c6 Kristin Braun
        let str = CoAlgFormula.exportFormula g in
288
        incr counter;
289 bc0691dc Kristin Braun
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
290 946e8213 Kristin Braun
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
291 b81e4887 Hans-Peter Deifel
        flush stdout;
292
      else ()
293
    done
294
  with End_of_file -> ()
295 9631d5b7 Kristin Braun
296 4c23563e Hans-Peter Deifel
let choiceNNF opts =
297 1ec1a764 Thorsten Wißmann
    try
298
      while true do
299
        let input = read_line () in
300
        if not (GenAndComp.isEmptyString input) then
301
          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
302
          let str = CoAlgFormula.exportFormula f in
303
          incr counter;
304
          print_string (str ^ "\n");
305
          flush stdout;
306
        else ()
307
      done
308
    with End_of_file -> ()
309
310 4c23563e Hans-Peter Deifel
let choiceGraph opts =
311 62cbb102 Hans-Peter Deifel
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
312
313
  let input = read_line () in
314
  let (tbox, f) = CoAlgFormula.importQuery input in
315 f24367c4 Hans-Peter Deifel
  ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f);
316 86c2c2ee Hans-Peter Deifel
  print_endline (CM.graphToDot ())
317 4942adb7 Christoph Egger
318 4c23563e Hans-Peter Deifel
let choiceVerify opts =
319 1484d8cb Christoph Egger
    try
320
      while true do
321 e928d370 Hans-Peter Deifel
        print_string "> ";
322 1484d8cb Christoph Egger
        let input = read_line () in
323
        if not (GenAndComp.isEmptyString input) then
324
          let f = CoAlgFormula.importFormula input in
325
          let str = CoAlgFormula.exportFormula f in
326
          incr counter;
327
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
328
          flush stdout;
329 e928d370 Hans-Peter Deifel
          try CoAlgFormula.verifyFormula f;
330
          with CoAlgFormula.CoAlgException s -> print_string (s ^ "\n")
331 1484d8cb Christoph Egger
        else ()
332
      done
333
    with End_of_file -> ()
334
335 4fd82fa1 Thorsten Wißmann
let _ =
336 cf70b199 Hans-Peter Deifel
  if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
337 7aa620ce Thorsten Wißmann
  else
338
    let choice = Sys.argv.(1) in
339 4c23563e Hans-Peter Deifel
    match Args.parse Sys.argv 3 options defaultOpts with
340
    | Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
341
    | Args.Ok opts ->
342
       match choice with
343
       | "sat" -> choiceSat opts
344
       | "prov" -> choiceProvable opts
345
       | "print" -> choicePrint opts
346
       | "nnf" -> choiceNNF opts
347
       | "verify" -> choiceVerify opts
348
       | "graph" -> choiceGraph opts
349
       | "nom2fix" -> choiceNom2fix opts
350 2d58f46f Kristin Braun
       | "nom2fixN" -> choiceNom2fixNonOpt opts
351 d5e292c6 Kristin Braun
       | "solveNom" -> choiceSolveNom opts
352 2d58f46f Kristin Braun
       | "solveNomN" -> choiceSolveNomNonOpt opts
353 1d36cd07 Kristin Braun
       | "approx" -> choiceApprox opts
354 4c23563e Hans-Peter Deifel
       | _ -> printUsage (Sys.argv.(0))
355 a57eb439 Hans-Peter Deifel
356
(* vim: set et sw=2 sts=2 ts=8 : *)