Project

General

Profile

Revision 2d58f46f src/coalg/coalg.ml

View differences:

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

  
173
let choiceNom2fixNonOpt 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
  (*CoAlgMisc.sortTable = ref sorts;*)
182
  try
183
    while true do
184
      let input = read_line () in
185
      if not (GenAndComp.isEmptyString input) then
186
        let (s, f) = CoAlgFormula.importSortedFormula input in
187
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s false in
189
        let str = CoAlgFormula.exportFormula g in
190
        incr counter;
191
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192
        flush stdout;
193
      else ()
194
    done
195
  with End_of_file -> ()
196

  
173 197
let choiceNom2fix opts =
174 198
  let verb = opts.verbose in
175 199
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
......
185 209
      if not (GenAndComp.isEmptyString input) then
186 210
        let (s, f) = CoAlgFormula.importSortedFormula input in
187 211
        let (tbox, fu) = CoAlgFormula.importQuery input in
188
        let g = Nom2fix.translate f nomTable sorts s in
212
        let g = Nom2fix.translate f nomTable sorts s true in
213
        let str = CoAlgFormula.exportFormula g in
214
        incr counter;
215
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
216
        flush stdout;
217
      else ()
218
    done
219
  with End_of_file -> ()
220

  
221
let choiceSolveNomNonOpt opts =
222
  let verb = opts.verbose in
223
  let sorts = (FE.sortTableFromString Sys.argv.(2)) in
224
    let printRes sat =
225
      if not verb then
226
        print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
227
      else ()
228
    in
229
  (*CoAlgMisc.sortTable = ref sorts;*)
230
  try
231
    while true do
232
      let input = read_line () in
233
      if not (GenAndComp.isEmptyString input) then
234
        let (s, f) = CoAlgFormula.importSortedFormula input in
235
        let (tbox, fu) = CoAlgFormula.importQuery input in
236
        let g = Nom2fix.translate f nomTable sorts s false in
189 237
        let str = CoAlgFormula.exportFormula g in
190 238
        incr counter;
191 239
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
240
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
192 241
        flush stdout;
193 242
      else ()
194 243
    done
......
209 258
      if not (GenAndComp.isEmptyString input) then
210 259
        let (s, f) = CoAlgFormula.importSortedFormula input in
211 260
        let (tbox, fu) = CoAlgFormula.importQuery input in
212
        let g = Nom2fix.translate f nomTable sorts s in
261
        let g = Nom2fix.translate f nomTable sorts s true in
213 262
        let str = CoAlgFormula.exportFormula g in
214 263
        incr counter;
215
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
264
        (*print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");*)
216 265
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
217 266
        flush stdout;
218 267
      else ()
......
273 322
       | "verify" -> choiceVerify opts
274 323
       | "graph" -> choiceGraph opts
275 324
       | "nom2fix" -> choiceNom2fix opts
325
       | "nom2fixN" -> choiceNom2fixNonOpt opts
276 326
       | "solveNom" -> choiceSolveNom opts
327
       | "solveNomN" -> choiceSolveNomNonOpt opts
277 328
       | _ -> printUsage (Sys.argv.(0))
278 329

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

Also available in: Unified diff