Project

General

Profile

Revision 946e8213 src/coalg/coalg.ml

View differences:

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

  
173 173
let choiceNom2fix opts =
174
  let verb = opts.verbose in
174 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
175 181
  (*CoAlgMisc.sortTable = ref sorts;*)
176 182
  try
177 183
    while true do
178 184
      let input = read_line () in
179 185
      if not (GenAndComp.isEmptyString input) then
180
        let f = CoAlgFormula.importFormula input in
181
        (*let g = EAFormula.nom2EA f nomTable sorts in*)
182
        (*let str = EAFormula.exportFormula g in*)
183
        let g = Nom2fix.translate f nomTable sorts in
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 in
184 189
        let str = CoAlgFormula.exportFormula g in
185 190
        incr counter;
186 191
        print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
192
        printRes (CoAlgReasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox (s,g));
187 193
        flush stdout;
188 194
      else ()
189 195
    done

Also available in: Unified diff