Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / fuzzy / fuzzy.ml @ b75e5a66

History | View | Annotate | Download (7.67 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 AF = ALCFormula
8

    
9
open CoolUtils
10
open Glpk
11
open FuzzyALCReasoner
12

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

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

    
39

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

    
42

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

    
62
let verbose = ref false
63

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

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

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

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

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

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

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

    
182

    
183
*)
184

    
185
(*
186
let printUsage () =
187
  print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
188
  print_endline "       <task> in { sat print nnf prov (is »not.(sat ¬f)«) }";
189
  print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
190
  print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
191
  print_endline "       <flags> = a list of the following items";
192
  print_endline "           --agents AGLIST";
193
  print_endline "             expects the next argument AGLIST to be a list of integers";
194
  print_endline "             which is treaten as the set of agents for CL formulas";
195
  print_endline "             it defaults to 1,2,3,4,5,6,7,8,9,10";
196
  print_endline "           --verbose";
197
  print_endline "             print verbose output for sat task";
198
  print_endline "";
199
  print_endline "Examples:";
200
  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
201
  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
202
  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash"
203
*)
204

    
205
let funConcat f1 f2 x = f1 (f2 x) (* XXX can't this be done better? *)
206

    
207
let _ =
208
    try
209
      while true do
210
        let input = read_line () in
211
        if not (GenAndComp.isEmptyString input) then
212
          try (
213
            let in1 = FuzzyALCABox.importQuery input in
214
            incr counter;
215
            print_string ("ABox " ^ (string_of_int !counter) ^ ": ");
216
            let in2 = List.map (funConcat FuzzyALCABox.replaceOrForall FuzzyALCABox.collapseNeg) in1 in
217
            (if fuzzyALCsat in2 then
218
                print_endline "Satisfiable"
219
            else
220
                print_endline "Not satisfiable")
221
          ) with FuzzyALCABox.CoAlgException("Parsing error") -> print_endline "Parsing error"
222
        else ()
223
      done
224
    with End_of_file -> ()