Commit e298ec5d authored by Simon Cruanes's avatar Simon Cruanes
Browse files

tptp driver handles some timeout messages

tptp2why accepts stdin as a problem
parent f5cb7ea4
......@@ -8,8 +8,10 @@ filename "%f-%t-%g.p"
valid "Proof found"
valid "Completion found"
invalid "Failure"
invalid "No Proof Found"
fail "Failure" "Failure"
unknown "No Proof Found" "Unknown"
timeout "Resource limit exceeded"
timeout "Ran out of time"
(* to be improved *)
......@@ -18,7 +18,7 @@ end= struct
let rec getAllDecls ?first:(first=false) include_dir filename =
let filename = if first then filename else include_dir^"/"^filename in
let input = open_in filename in
let input = if filename = "-" then stdin else open_in filename in
let decls = TptpParser.tptp TptpLexer.token (Lexing.from_channel input) in
let isInclude = function | Include _ -> true | _ -> false in
close_in input;
......@@ -61,10 +61,11 @@ module Init = struct
let options = [
("-o", String output_updater, "outputs to a file");
("-I", String include_updater, "search for included files in this dir")
("-I", String include_updater, "search for included files in this dir");
("-", Unit (fun () -> input_files := "-" :: !input_files), "reads from stdin")
let usage = "tptp2why file1 [file2...] [-o file] [-I dir]
let usage = "tptp2why [file1|-] [file2...] [-o file] [-I dir]
It parses tptp files (fof or cnf format) and prints a why file
with one theory per input file."
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment