Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / coalg / coalg.ml @ 7c4d2eb4

History | View | Annotate | Download (5.85 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

    
10
open CoolUtils
11

    
12
(* The type of formulae that are accepted. *)
13
(*
14
let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0])
15
*)
16
(*
17
let sorts = Array.make 3 (CoAlgMisc.MultiModalK, [0])
18
let _ = sorts.(0) <- (CoAlgMisc.Choice, [1; 2])
19
*)
20
(*
21
let sorts = [| (CoAlgMisc.MultiModalKD, [0])
22
            (*;  (CoAlgMisc.MultiModalKD, [1])
23
            ;  (CoAlgMisc.Fusion, [1; 1]) *)
24
            |]
25
let sorts = [| (CM.MultiModalK, [0])
26
            (*;  (CoAlgMisc.MultiModalKD, [1])
27
            ;  (CoAlgMisc.Fusion, [1; 1]) *)
28
            |]
29
*)
30

    
31
(* A partial function mapping nominals to their sorts. *)
32
let nomTable name =
33
  assert (CoAlgFormula.isNominal name);
34
  Some 0
35

    
36

    
37
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
38

    
39

    
40
let printUsage () =
41
  print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
42
  print_endline "       <task> in { sat print nnf prov (is »not.(sat ¬f)«) }";
43
  print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
44
  print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
45
  print_endline "       <flags> = a list of the following items";
46
  print_endline "           --agents AGLIST";
47
  print_endline "             expects the next argument AGLIST to be a list of integers";
48
  print_endline "             which is treaten as the set of agents for CL formulas";
49
  print_endline "             it defaults to 1,2,3,4,5,6,7,8,9,10";
50
  print_endline "           --verbose";
51
  print_endline "             print verbose output for sat task";
52
  print_endline "";
53
  print_endline "Examples:";
54
  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
55
  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
56
  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash";
57
  exit 1
58

    
59
let counter = ref 0
60
let verbose = ref false
61

    
62
let parseFunctor str =
63
    match str with
64
    | "K" -> CM.MultiModalK
65
    | "KD" -> CM.MultiModalKD
66
    | "CL" -> CM.CoalitionLogic
67
    | "GML" -> CM.GML
68
    | "MultiModalK" -> CM.MultiModalK
69
    | "MultiModalKD" -> CM.MultiModalKD
70
    | "CoalitionLogic" -> CM.CoalitionLogic
71
    | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Functor name »" ^ str ^ "«"))
72

    
73
let choiceSat () =
74
    let verb = !verbose in
75
    let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] in
76
    let printRes sat =
77
      if not verb then
78
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
79
      else ()
80
    in
81
    try
82
      while true do
83
        let input = read_line () in
84
        if not (GenAndComp.isEmptyString input) then
85
          let (tbox, f) = CoAlgFormula.importQuery input in
86
          incr counter;
87
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
88
          flush stdout;
89
          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f)
90
        else ()
91
      done
92
    with End_of_file -> ()
93

    
94
let choiceProvable () =
95
    let verb = !verbose in
96
    let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
97
        (s,CF.NOT f)
98
    in
99
    let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] in
100
    let printRes sat =
101
      if not verb then
102
        print_endline (if not sat then "provable\n" else "unprovable\n")
103
      else ()
104
    in
105
    try
106
      while true do
107
        let input = read_line () in
108
        if not (GenAndComp.isEmptyString input) then
109
          let (tbox,f) = CoAlgFormula.importQuery input in
110
          let fneg = sorted_not f in
111
          incr counter;
112
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
113
          flush stdout;
114
          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg)
115
        else ()
116
      done
117
    with End_of_file -> ()
118

    
119
let choicePrint () =
120
    try
121
      while true do
122
        let input = read_line () in
123
        if not (GenAndComp.isEmptyString input) then
124
          let f = CoAlgFormula.importFormula input in
125
          let str = CoAlgFormula.exportFormula f in
126
          incr counter;
127
          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
128
          flush stdout;
129
        else ()
130
      done
131
    with End_of_file -> ()
132

    
133
let choiceNNF () =
134
    try
135
      while true do
136
        let input = read_line () in
137
        if not (GenAndComp.isEmptyString input) then
138
          let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in
139
          let str = CoAlgFormula.exportFormula f in
140
          incr counter;
141
          print_string (str ^ "\n");
142
          flush stdout;
143
        else ()
144
      done
145
    with End_of_file -> ()
146

    
147
let rec parseFlags arr offs : unit =
148
    let offs = ref (offs) in
149
    let getParam () =
150
        if ((!offs + 1) >= Array.length arr) then
151
            raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«"))
152
        else
153
            offs := !offs + 1;
154
            arr.(!offs)
155
    in
156
    if (!offs >= Array.length arr) then ()
157
    else (ignore (match arr.(!offs) with
158
         | "--verbose" -> verbose := true
159
         | "--agents" ->
160
            let strAglist = getParam () in
161
            let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
162
            CoolUtils.cl_set_agents (Array.of_list aglist)
163
         | _ ->
164
            raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
165
         ) ; parseFlags arr (!offs + 1)
166
     )
167

    
168
let _ =
169
  if Array.length Sys.argv < 3 then printUsage()
170
  else
171
    let choice = Sys.argv.(1) in
172
    parseFlags Sys.argv 3;
173
    match choice with
174
    | "sat" -> choiceSat ()
175
    | "prov" -> choiceProvable ()
176
    | "print" -> choicePrint ()
177
    | "nnf" -> choiceNNF ()
178
    | _ -> printUsage ()
179

    
180