Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / coalg / coalg.ml @ def3763d

History | View | Annotate | Download (9.15 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 }";
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 choiceNom2fix opts =
174
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
175
  (*CoAlgMisc.sortTable = ref sorts;*)
176
  try
177
    while true do
178
      let input = read_line () in
179
      if not (GenAndComp.isEmptyString input) then
180
        let f = CoAlgFormula.importFormula input in
181
        (*let g = EAFormula.nom2EA f nomTable sorts in*)
182
        (*let str = EAFormula.exportFormula g in*)
183
        let g = Nom2fix.translate f nomTable sorts in
184
        let str = CoAlgFormula.exportFormula g in
185
        incr counter;
186
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
187
        flush stdout;
188
      else ()
189
    done
190
  with End_of_file -> ()
191

    
192
let choiceNNF opts =
193
    try
194
      while true do
195
        let input = read_line () in
196
        if not (GenAndComp.isEmptyString input) then
197
          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
198
          let str = CoAlgFormula.exportFormula f in
199
          incr counter;
200
          print_string (str ^ "\n");
201
          flush stdout;
202
        else ()
203
      done
204
    with End_of_file -> ()
205

    
206
let choiceGraph opts =
207
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
208

    
209
  let input = read_line () in
210
  let (tbox, f) = CoAlgFormula.importQuery input in
211
  ignore(CoAlgReasoner.isSat opts.fragment sorts nomTable tbox f);
212
  print_endline (CM.graphToDot ())
213

    
214
let choiceVerify opts =
215
    try
216
      while true do
217
        print_string "> ";
218
        let input = read_line () in
219
        if not (GenAndComp.isEmptyString input) then
220
          let f = CoAlgFormula.importFormula input in
221
          let str = CoAlgFormula.exportFormula f in
222
          incr counter;
223
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
224
          flush stdout;
225
          try CoAlgFormula.verifyFormula f;
226
          with CoAlgFormula.CoAlgException s -> print_string (s ^ "\n")
227
        else ()
228
      done
229
    with End_of_file -> ()
230

    
231
let _ =
232
  if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
233
  else
234
    let choice = Sys.argv.(1) in
235
    match Args.parse Sys.argv 3 options defaultOpts with
236
    | Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
237
    | Args.Ok opts ->
238
       match choice with
239
       | "sat" -> choiceSat opts
240
       | "prov" -> choiceProvable opts
241
       | "print" -> choicePrint opts
242
       | "nnf" -> choiceNNF opts
243
       | "verify" -> choiceVerify opts
244
       | "graph" -> choiceGraph opts
245
       | "nom2fix" -> choiceNom2fix opts
246
       | _ -> printUsage (Sys.argv.(0))
247

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