src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
changeset 74046 462d652ad910
parent 74005 14de47e29fe4
child 74047 a2b470e315ee
equal deleted inserted replaced
74045:302994f5a3c2 74046:462d652ad910
   317 (* iProver *)
   317 (* iProver *)
   318 
   318 
   319 val iprover_config : atp_config =
   319 val iprover_config : atp_config =
   320   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
   320   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
   321    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
   321    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
   322      ["--clausifier \"$E_HOME\"/eprover " ^
   322      ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
   323       "--clausifier_options \"--tstp-format --silent --cnf\" " ^
   323       "--clausifier_options \"--mode clausify\" " ^
   324       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
   324       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
   325    proof_delims = tstp_proof_delims,
   325    proof_delims = tstp_proof_delims,
   326    known_failures =
   326    known_failures =
   327      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
   327      [(ProofIncomplete, "% SZS output start CNFRefutation")] @
   328      known_szs_status_failures,
   328      known_szs_status_failures,