537 |
537 |
538 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit) |
538 val vampire_tff0 = TFF (Monomorphic, TPTP_Implicit) |
539 |
539 |
540 val vampire_config : atp_config = |
540 val vampire_config : atp_config = |
541 {exec = (["VAMPIRE_HOME"], ["vampire"]), |
541 {exec = (["VAMPIRE_HOME"], ["vampire"]), |
542 arguments = fn _ => fn _ => fn sos => fn timeout => fn file_name => fn _ => |
542 arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name => |
|
543 fn _ => |
543 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ |
544 "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^ |
544 " --proof tptp --output_axiom_names on" ^ |
545 " --proof tptp --output_axiom_names on" ^ |
545 (if is_vampire_at_least_1_8 () then |
546 (if is_vampire_at_least_1_8 () then |
546 (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *) |
547 (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *) |
547 " --forced_options propositional_to_bdd=off:splitting=off:\ |
548 " --forced_options propositional_to_bdd=off" ^ |
548 \equality_proxy=off:general_splitting=off:inequality_splitting=0:\ |
549 (if full_proof then |
549 \naming=0" |
550 ":splitting=off:equality_proxy=off:general_splitting=off\ |
|
551 \:inequality_splitting=0:naming=0" |
|
552 else |
|
553 "") |
550 else |
554 else |
551 "") ^ |
555 "") ^ |
552 " --thanks \"Andrei and Krystof\" --input_file " ^ file_name |
556 " --thanks \"Andrei and Krystof\" --input_file " ^ file_name |
553 |> sos = sosN ? prefix "--sos on ", |
557 |> sos = sosN ? prefix "--sos on ", |
554 proof_delims = |
558 proof_delims = |