Project

General

Profile

Revision d5e292c6

View differences:

src/coalg/coalg.ml
65 65

  
66 66
let printUsage name =
67 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 }";
68
  print_endline "       <task> in { sat print graph verify nnf prov (is »not.(sat ¬f)«) nom2fix solveNom}";
69 69
  print_endline "       <functor> in { MultiModalK (or equivalently K)";
70 70
  print_endline "                      MultiModalKD (or equivalently KD)";
71 71
  print_endline "                      Monotone";
......
189 189
        let str = CoAlgFormula.exportFormula g in
190 190
        incr counter;
191 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 choiceSolveNom 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 in
213
        let str = CoAlgFormula.exportFormula g in
214
        incr counter;
215
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192 216
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
193 217
        flush stdout;
194 218
      else ()
......
249 273
       | "verify" -> choiceVerify opts
250 274
       | "graph" -> choiceGraph opts
251 275
       | "nom2fix" -> choiceNom2fix opts
276
       | "solveNom" -> choiceSolveNom opts
252 277
       | _ -> printUsage (Sys.argv.(0))
253 278

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

Also available in: Unified diff