Project

General

Profile

Statistics
| Branch: | Revision:

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

History | View | Annotate | Download (12.9 KB)

1
(** 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
module CM = CoAlgMisc
8
module CF = CoAlgFormula
9
module EA = EAFormula
10
module NF = Nom2fix
11

    
12
module FE = FunctorParsing
13

    
14
open CoolUtils
15

    
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
type options =
25
  { verbose : bool
26
  ; fragment : CM.fragment_spec
27
  }
28

    
29
let defaultOpts = { verbose = false; fragment = CM.Auto }
30

    
31
let options =
32
  [ { Args.long = "verbose"
33
    ; Args.short = Some 'v'
34
    ; Args.description = "print verbose output with statistics"
35
    ; Args.argument = Args.No_arg (fun a -> { a with verbose = true })
36
    }
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
  ; { 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
  ]
65

    
66
let printUsage name =
67
  print_endline ("Usage: \"" ^ name ^ " <task> <functor> [<flags>]\" where");
68
  print_endline "       <task> in { sat print graph verify nnf prov (is »not.(sat ¬f)«) nom2fix solveNom}";
69
  print_endline "       <functor> in { MultiModalK (or equivalently K)";
70
  print_endline "                      MultiModalKD (or equivalently KD)";
71
  print_endline "                      Monotone";
72
  print_endline "                      CoalitionLogic (or equivalently CL)";
73
  print_endline "                      Const id1 ... idn (or equivalently Constant id1 ... idn)";
74
  print_endline "                      Id (or equivalently Identity)";
75
  print_endline "                    }";
76
  print_endline "                 where you can compose functors by:";
77
  print_endline "                    <functor> + <functor> (weakest precedence)";
78
  print_endline "                 or <functor> * <functor>";
79
  print_endline "                 or <functor> . <functor> (binds strongest)";
80
  print_endline "                 (so K+KD.CL*Id stand for (K + ((KD.CL) * Id)))";
81
  print_endline "       <flags> = a list of the following items";
82
  Args.help stdout 11 options;
83
  print_endline "";
84
  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
  print_endline "Examples:";
99
  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
100
  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
101
  print_endline "  OCAMLRUNPARAM=b ./coalg sat 'K + KD' <<< '(([R] False) + ([R] False))'";
102
  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash";
103
  exit 1
104

    
105
let counter = ref 0
106

    
107
let choiceSat opts =
108
    let verb = opts.verbose in
109
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
110
    
111
    (* 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
      raise (CF.CoAlgException "GML and PML are currently not supported")
114
    else ();
115

    
116
    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
          let (tbox, f) = CoAlgFormula.importQuery input in
126
          incr counter;
127
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
128
          flush stdout;
129
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f)
130
        else ()
131
      done
132
    with End_of_file -> ()
133

    
134
let choiceProvable opts =
135
    let verb = opts.verbose in
136
    let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
137
        (s,CF.NOT f)
138
    in
139
    let sorts = (FE.sortTableFromString Sys.argv.(2)) in
140
    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
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg)
155
        else ()
156
      done
157
    with End_of_file -> ()
158

    
159
let choicePrint opts =
160
    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
        else ()
170
      done
171
    with End_of_file -> ()
172

    
173
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
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
let choiceNom2fix opts =
223
  let verb = opts.verbose in
224
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
225
    let printRes sat =
226
      if not verb then
227
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
228
      else ()
229
    in
230
  (*CoAlgMisc.sortTable = ref sorts;*)
231
  try
232
    while true do
233
      let input = read_line () in
234
      if not (GenAndComp.isEmptyString input) then
235
        let (s, f) = CoAlgFormula.importSortedFormula input in
236
        let (tbox, fu) = CoAlgFormula.importQuery input in
237
        let g = Nom2fix.translate f nomTable sorts s true in
238
        let str = CoAlgFormula.exportFormula g in
239
        incr counter;
240
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
241
        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
        let str = CoAlgFormula.exportFormula g in
263
        incr counter;
264
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
265
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
266
        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
        let g = Nom2fix.translate f nomTable sorts s true in
287
        let str = CoAlgFormula.exportFormula g in
288
        incr counter;
289
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
290
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
291
        flush stdout;
292
      else ()
293
    done
294
  with End_of_file -> ()
295

    
296
let choiceNNF opts =
297
    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
let choiceGraph opts =
311
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
312

    
313
  let input = read_line () in
314
  let (tbox, f) = CoAlgFormula.importQuery input in
315
  ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f);
316
  print_endline (CM.graphToDot ())
317

    
318
let choiceVerify opts =
319
    try
320
      while true do
321
        print_string "> ";
322
        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
          try CoAlgFormula.verifyFormula f;
330
          with CoAlgFormula.CoAlgException s -> print_string (s ^ "\n")
331
        else ()
332
      done
333
    with End_of_file -> ()
334

    
335
let _ =
336
  if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
337
  else
338
    let choice = Sys.argv.(1) in
339
    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
       | "nom2fixN" -> choiceNom2fixNonOpt opts
351
       | "solveNom" -> choiceSolveNom opts
352
       | "solveNomN" -> choiceSolveNomNonOpt opts
353
       | "approx" -> choiceApprox opts
354
       | _ -> printUsage (Sys.argv.(0))
355

    
356
(* vim: set et sw=2 sts=2 ts=8 : *)