## cool / src / coalg / coalg.ml @ 9631d5b7

History | View | Annotate | Download (8.57 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 |
module FE = FunctorParsing |

11 | |

12 |
open CoolUtils |

13 | |

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 |
(* A partial function mapping nominals to their sorts. *) |

34 |
let nomTable name = |

35 |
assert (CoAlgFormula.isNominal name); |

36 |
Some 0 |

37 | |

38 | |

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

40 | |

41 |
(* |

42 |
let _ = |

43 |
let str = "A . B C" in |

44 |
print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str)) |

45 |
*) |

46 | |

47 |
let printUsage () = |

48 |
print_endline "Usage: \"alc <task> <functor> [<flags>]\" where"; |

49 |
print_endline " <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) nom2fix }"; |

50 |
print_endline " <functor> in { MultiModalK (or equivalently K)"; |

51 |
print_endline " MultiModalKD (or equivalently KD)"; |

52 |
print_endline " Monotone"; |

53 |
print_endline " CoalitionLogic (or equivalently CL)"; |

54 |
print_endline " Const id1 ... idn (or equivalently Constant id1 ... idn)"; |

55 |
print_endline " Id (or equivalently Identity)"; |

56 |
print_endline " PML"; |

57 |
print_endline " GML"; |

58 |
print_endline " }"; |

59 |
print_endline " where you can compose functors by:"; |

60 |
print_endline " <functor> + <functor> (weakest precedence)"; |

61 |
print_endline " or <functor> * <functor>"; |

62 |
print_endline " or <functor> . <functor> (binds strongest)"; |

63 |
print_endline " (so K+KD.CL*PML stand for (K + ((KD.CL) * PML)))"; |

64 |
print_endline " <flags> = a list of the following items"; |

65 |
print_endline " --agents AGLIST"; |

66 |
print_endline " expects the next argument AGLIST to be a list of integers"; |

67 |
print_endline " which is treaten as the set of agents for CL formulas"; |

68 |
print_endline " it defaults to 1,2,3,4,5,6,7,8,9,10"; |

69 |
print_endline " --verbose"; |

70 |
print_endline " print verbose output for sat task"; |

71 |
print_endline ""; |

72 |
print_endline "Problems are read from standard input and have the form"; |

73 |
print_endline " [ ass_1; .. ; ass_n |- ] concept"; |

74 |
print_endline "where concept, ass_1, ..., ass_n are formulae (hypothesis"; |

75 |
print_endline "and TBox assumptions) built using"; |

76 |
print_endline " True, False, ident (atomic proposition), ident' (nominal)"; |

77 |
print_endline " <=> (equivalence), => (implication), | (or), & (and), ~ (not)"; |

78 |
print_endline " @ ident' (satisfaction operator)"; |

79 |
print_endline " [R], <R> (universal/existential restrictions along role R"; |

80 |
print_endline " [{ aglist }], <{ aglist }> (aglist can force / cannot avoid)"; |

81 |
print_endline " {<= n}, {>= n}, {< n}, {> n} (number / probability of successors)"; |

82 |
print_endline " =ident (constant value)"; |

83 |
print_endline " O (identity operator)"; |

84 |
print_endline " _ + _ (choice)"; |

85 |
print_endline " [pi1], [pi2] (fusion)"; |

86 |
print_endline ""; |

87 |
print_endline "Examples:"; |

88 |
print_endline " OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'"; |

89 |
print_endline " OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'"; |

90 |
print_endline " OCAMLRUNPARAM=b ./coalg sat 'K + KD' <<< '(([R] False) + ([R] False))'"; |

91 |
print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash"; |

92 |
exit 1 |

93 | |

94 |
let counter = ref 0 |

95 |
let verbose = ref false |

96 | |

97 |
let choiceSat () = |

98 |
let verb = !verbose in |

99 |
let sorts = (FE.sortTableFromString Sys.argv.(2)) in |

100 |
let printRes sat = |

101 |
if not verb then |

102 |
print_endline (if sat then "satisfiable\n" else "unsatisfiable\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 |
incr counter; |

111 |
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); |

112 |
flush stdout; |

113 |
printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f) |

114 |
else () |

115 |
done |

116 |
with End_of_file -> () |

117 | |

118 |
let choiceProvable () = |

119 |
let verb = !verbose in |

120 |
let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula = |

121 |
(s,CF.NOT f) |

122 |
in |

123 |
let sorts = (FE.sortTableFromString Sys.argv.(2)) in |

124 |
let printRes sat = |

125 |
if not verb then |

126 |
print_endline (if not sat then "provable\n" else "unprovable\n") |

127 |
else () |

128 |
in |

129 |
try |

130 |
while true do |

131 |
let input = read_line () in |

132 |
if not (GenAndComp.isEmptyString input) then |

133 |
let (tbox,f) = CoAlgFormula.importQuery input in |

134 |
let fneg = sorted_not f in |

135 |
incr counter; |

136 |
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": "); |

137 |
flush stdout; |

138 |
printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg) |

139 |
else () |

140 |
done |

141 |
with End_of_file -> () |

142 | |

143 |
let choicePrint () = |

144 |
try |

145 |
while true do |

146 |
let input = read_line () in |

147 |
if not (GenAndComp.isEmptyString input) then |

148 |
let f = CoAlgFormula.importFormula input in |

149 |
let str = CoAlgFormula.exportFormula f in |

150 |
incr counter; |

151 |
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); |

152 |
flush stdout; |

153 |
else () |

154 |
done |

155 |
with End_of_file -> () |

156 | |

157 |
let choiceNom2fix () = |

158 |
try |

159 |
while true do |

160 |
let input = read_line () in |

161 |
if not (GenAndComp.isEmptyString input) then |

162 |
let f = CoAlgFormula.importFormula input in |

163 |
let str = CoAlgFormula.exportFormula f in |

164 |
incr counter; |

165 |
print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); |

166 |
flush stdout; |

167 |
else () |

168 |
done |

169 |
with End_of_file -> () |

170 | |

171 |
let choiceNNF () = |

172 |
try |

173 |
while true do |

174 |
let input = read_line () in |

175 |
if not (GenAndComp.isEmptyString input) then |

176 |
let f = CoAlgFormula.nnf (CoAlgFormula.importFormula input) in |

177 |
let str = CoAlgFormula.exportFormula f in |

178 |
incr counter; |

179 |
print_string (str ^ "\n"); |

180 |
flush stdout; |

181 |
else () |

182 |
done |

183 |
with End_of_file -> () |

184 | |

185 |
let choiceGraph () = |

186 |
choiceSat (); |

187 |
print_endline "digraph reasonerstate {"; |

188 |
CM.graphIterCores (fun core -> print_endline (CM.coreToDot core)); |

189 |
CM.graphIterStates (fun state -> print_endline (CM.stateToDot state)); |

190 |
print_endline "}" |

191 | |

192 |
let choiceVerify () = |

193 |
try |

194 |
while true do |

195 |
let input = read_line () in |

196 |
if not (GenAndComp.isEmptyString input) then |

197 |
let f = CoAlgFormula.importFormula input in |

198 |
let str = CoAlgFormula.exportFormula f in |

199 |
incr counter; |

200 |
print_string ("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); |

201 |
flush stdout; |

202 |
CoAlgFormula.verifyFormula f; |

203 |
else () |

204 |
done |

205 |
with End_of_file -> () |

206 | |

207 |
let rec parseFlags arr offs : unit = |

208 |
let offs = ref (offs) in |

209 |
let getParam () = |

210 |
if ((!offs + 1) >= Array.length arr) then |

211 |
raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«")) |

212 |
else |

213 |
offs := !offs + 1; |

214 |
arr.(!offs) |

215 |
in |

216 |
if (!offs >= Array.length arr) then () |

217 |
else (ignore (match arr.(!offs) with |

218 |
| "--verbose" -> verbose := true |

219 |
| "--agents" -> |

220 |
let strAglist = getParam () in |

221 |
let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in |

222 |
CoolUtils.cl_set_agents (Array.of_list aglist) |

223 |
| _ -> |

224 |
raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«")) |

225 |
) ; parseFlags arr (!offs + 1) |

226 |
) |

227 | |

228 |
let _ = |

229 |
if Array.length Sys.argv < 3 then printUsage() |

230 |
else |

231 |
let choice = Sys.argv.(1) in |

232 |
parseFlags Sys.argv 3; |

233 |
match choice with |

234 |
| "sat" -> choiceSat () |

235 |
| "prov" -> choiceProvable () |

236 |
| "print" -> choicePrint () |

237 |
| "nnf" -> choiceNNF () |

238 |
| "verify" -> choiceVerify () |

239 |
| "graph" -> choiceGraph () |

240 |
| "nom2fix" -> choiceNom2fix() |

241 |
| _ -> printUsage () |