Project

General

Profile

Revision 1d36cd07 src/coalg/coalg.ml

View differences:

src/coalg/coalg.ml
170 170
      done
171 171
    with End_of_file -> ()
172 172

  
173
let choiceApprox opts =
174
  let verb = opts.verbose in
175
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
176
    let printRes sat =
177
      if not verb then
178
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
179
      else ()
180
    in
181
    try
182
      while true do
183
        let input = read_line () in
184
        if not (GenAndComp.isEmptyString input) then
185
          let (s, fo) = CoAlgFormula.importSortedFormula input in
186
          let (tbox, fu) = CoAlgFormula.importQuery input in
187
          let g = Nom2fix.translate fo nomTable sorts s true in
188
          let f = Nom2fix.delFix g in
189
          let str = CoAlgFormula.exportFormula f in
190
          incr counter;
191
          print_string("\nFormula " ^ (string_of_int !counter) ^ ": ");
192
          printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
193
          flush stdout;
194
        else ()
195
      done
196
    with End_of_file -> ()
197

  
173 198
let choiceNom2fixNonOpt opts =
174 199
  let verb = opts.verbose in
175 200
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
......
325 350
       | "nom2fixN" -> choiceNom2fixNonOpt opts
326 351
       | "solveNom" -> choiceSolveNom opts
327 352
       | "solveNomN" -> choiceSolveNomNonOpt opts
353
       | "approx" -> choiceApprox opts
328 354
       | _ -> printUsage (Sys.argv.(0))
329 355

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

Also available in: Unified diff