diff --git a/solver.ml b/solver.ml index da23db87ee6d4d4a3192270c6e31cf68d5fe0fae..b93fa9c049d0b9a12d74c40804e49b79f37c43c3 100644 --- a/solver.ml +++ b/solver.ml @@ -57,7 +57,7 @@ let default_exe_name_of_solver = function | Marabou -> "Marabou" let default_option_of_solver = function - | Pyrat -> "--version" + | Pyrat -> "-v" | Marabou -> "--version" let exe_path_of_solver solver = @@ -122,6 +122,8 @@ let version_of_solver solver s = in let regexp_version = Str.regexp regexp_string in try + (* We suppose that the first occurrence that matches [regexp_string] is + indeed the version of the concercend [solver]. *) ignore (Str.search_forward regexp_version s 0); Version (Str.matched_string s) with Stdlib.Not_found -> @@ -204,9 +206,18 @@ let detect_default_solvers () = (fun m -> m "Executing command `%s' to detect `%a'." cmd pp_solver solver); let retcode = Sys.command cmd in - let in_channel = Stdlib.open_in tmp in - let firstline = Stdlib.input_line in_channel in - Stdlib.close_in in_channel; + let cmd_output = + let in_channel = Stdlib.open_in tmp in + let buf = Buffer.create 512 in + try + while true do + Stdlib.Buffer.add_channel buf in_channel 512; + done; + assert false + with End_of_file -> + Stdlib.close_in in_channel; + Buffer.contents buf + in Sys.remove tmp; if retcode <> 0 then begin @@ -215,7 +226,7 @@ let detect_default_solvers () = end else begin (* If available, we save a [config] for solver. *) - let version = version_of_solver solver firstline in + let version = version_of_solver solver cmd_output in let config = { solver; exe; version; } in Logs.app (fun m -> m "Found solver `%a' `%a' (%s)."