simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-11 05:28:34 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Safer code for input format auto-detection

Browse source
This commit is contained in:
Guillaume Bury 2014-11-11 10:45:01 +01:00
parent 172ff8bca3
commit ccfbe72bdf
1 changed files with 12 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

21
util/sat_solve.ml
View file

@ -48,23 +48,26 @@ let rec rev_flat_map f acc = function
let format_of_filename s = let format_of_filename s =
let last n = let last n =
try try String.sub s (String.length s - n) n
String.sub s (String.length s - n) n with Invalid_argument _ -> ""
with Invalid_argument _ ->
""
in in
if last 4 = ".cnf" then if last 4 = ".cnf" then
"dimacs" Dimacs
else if last 5 = ".smt2" then else if last 5 = ".smt2" then
"smtlib" Smtlib
else (* Default choice *) else (* Default choice *)
"dimacs" Dimacs
let rec parse_input file = match !input with let parse_with_input file = function
| Auto -> set_input (format_of_filename file); parse_input file | Auto -> assert false
| Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file) | Dimacs -> List.rev_map (List.rev_map S.make) (Parsedimacs.parse file)
| Smtlib -> Sat.Tseitin.simplify_cnf (rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file)) | Smtlib -> Sat.Tseitin.simplify_cnf (rev_flat_map Sat.Tseitin.make_cnf [] (Smtlib.parse file))
let parse_input file =
parse_with_input file (match !input with
| Auto -> format_of_filename file
| f -> f)
(* Printing wrappers *) (* Printing wrappers *)
let std = Format.std_formatter let std = Format.std_formatter