Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / coalg / coalg.ml @ 2d58f46f

History | View | Annotate | Download (12 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 choiceNom2fixNonOpt 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
  (*CoAlgMisc.sortTable = ref sorts;*)
182
  try
183
    while true do
184
      let input = read_line () in
185
      if not (GenAndComp.isEmptyString input) then
186
        let (s, f) = CoAlgFormula.importSortedFormula input in
187
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s false in
189
        let str = CoAlgFormula.exportFormula g in
190
        incr counter;
191
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192
        flush stdout;
193
      else ()
194
    done
195
  with End_of_file -> ()
196

    
197
let choiceNom2fix opts =
198
  let verb = opts.verbose in
199
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
200
    let printRes sat =
201
      if not verb then
202
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
203
      else ()
204
    in
205
  (*CoAlgMisc.sortTable = ref sorts;*)
206
  try
207
    while true do
208
      let input = read_line () in
209
      if not (GenAndComp.isEmptyString input) then
210
        let (s, f) = CoAlgFormula.importSortedFormula input in
211
        let (tbox, fu) = CoAlgFormula.importQuery input in
212
        let g = Nom2fix.translate f nomTable sorts s true in
213
        let str = CoAlgFormula.exportFormula g in
214
        incr counter;
215
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
216
        flush stdout;
217
      else ()
218
    done
219
  with End_of_file -> ()
220

    
221
let choiceSolveNomNonOpt opts =
222
  let verb = opts.verbose in
223
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
224
    let printRes sat =
225
      if not verb then
226
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
227
      else ()
228
    in
229
  (*CoAlgMisc.sortTable = ref sorts;*)
230
  try
231
    while true do
232
      let input = read_line () in
233
      if not (GenAndComp.isEmptyString input) then
234
        let (s, f) = CoAlgFormula.importSortedFormula input in
235
        let (tbox, fu) = CoAlgFormula.importQuery input in
236
        let g = Nom2fix.translate f nomTable sorts s false in
237
        let str = CoAlgFormula.exportFormula g in
238
        incr counter;
239
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
240
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
241
        flush stdout;
242
      else ()
243
    done
244
  with End_of_file -> ()
245

    
246
let choiceSolveNom 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 true 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 choiceNNF opts =
272
    try
273
      while true do
274
        let input = read_line () in
275
        if not (GenAndComp.isEmptyString input) then
276
          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
277
          let str = CoAlgFormula.exportFormula f in
278
          incr counter;
279
          print_string (str ^ "\n");
280
          flush stdout;
281
        else ()
282
      done
283
    with End_of_file -> ()
284

    
285
let choiceGraph opts =
286
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
287

    
288
  let input = read_line () in
289
  let (tbox, f) = CoAlgFormula.importQuery input in
290
  ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f);
291
  print_endline (CM.graphToDot ())
292

    
293
let choiceVerify opts =
294
    try
295
      while true do
296
        print_string "> ";
297
        let input = read_line () in
298
        if not (GenAndComp.isEmptyString input) then
299
          let f = CoAlgFormula.importFormula input in
300
          let str = CoAlgFormula.exportFormula f in
301
          incr counter;
302
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
303
          flush stdout;
304
          try CoAlgFormula.verifyFormula f;
305
          with CoAlgFormula.CoAlgException s -> print_string (s ^ "\n")
306
        else ()
307
      done
308
    with End_of_file -> ()
309

    
310
let _ =
311
  if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
312
  else
313
    let choice = Sys.argv.(1) in
314
    match Args.parse Sys.argv 3 options defaultOpts with
315
    | Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
316
    | Args.Ok opts ->
317
       match choice with
318
       | "sat" -> choiceSat opts
319
       | "prov" -> choiceProvable opts
320
       | "print" -> choicePrint opts
321
       | "nnf" -> choiceNNF opts
322
       | "verify" -> choiceVerify opts
323
       | "graph" -> choiceGraph opts
324
       | "nom2fix" -> choiceNom2fix opts
325
       | "nom2fixN" -> choiceNom2fixNonOpt opts
326
       | "solveNom" -> choiceSolveNom opts
327
       | "solveNomN" -> choiceSolveNomNonOpt opts
328
       | _ -> printUsage (Sys.argv.(0))
329

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