706 |
706 |
707 |
707 |
708 (* generic TPTP-based provers *) |
708 (* generic TPTP-based provers *) |
709 |
709 |
710 fun prover_fun name |
710 fun prover_fun name |
711 {home_var, executable, arguments, proof_delims, known_failures, |
711 {executable, required_executables, arguments, proof_delims, |
712 max_new_relevant_facts_per_iter, prefers_theory_relevant, |
712 known_failures, max_new_relevant_facts_per_iter, |
713 explicit_forall} |
713 prefers_theory_relevant, explicit_forall} |
714 ({debug, overlord, full_types, explicit_apply, relevance_threshold, |
714 ({debug, overlord, full_types, explicit_apply, relevance_threshold, |
715 relevance_convergence, theory_relevant, defs_relevant, isar_proof, |
715 relevance_convergence, theory_relevant, defs_relevant, isar_proof, |
716 isar_shrink_factor, ...} : params) |
716 isar_shrink_factor, ...} : params) |
717 minimize_command timeout |
717 minimize_command timeout |
718 ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} |
718 ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses} |
751 else if File.exists (Path.explode the_dest_dir) |
751 else if File.exists (Path.explode the_dest_dir) |
752 then Path.append (Path.explode the_dest_dir) probfile |
752 then Path.append (Path.explode the_dest_dir) probfile |
753 else error ("No such directory: " ^ the_dest_dir ^ ".") |
753 else error ("No such directory: " ^ the_dest_dir ^ ".") |
754 end; |
754 end; |
755 |
755 |
756 val home = getenv home_var |
756 val command = Path.explode (getenv (fst executable) ^ "/" ^ snd executable) |
757 val command = Path.explode (home ^ "/" ^ executable) |
|
758 (* write out problem file and call prover *) |
757 (* write out problem file and call prover *) |
759 fun command_line complete probfile = |
758 fun command_line complete probfile = |
760 let |
759 let |
761 val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
760 val core = File.shell_path command ^ " " ^ arguments complete timeout ^ |
762 " " ^ File.shell_path probfile |
761 " " ^ File.shell_path probfile |
776 val num3 = as_num (digit ::: digit ::: (digit >> single)); |
775 val num3 = as_num (digit ::: digit ::: (digit >> single)); |
777 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
776 val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b); |
778 val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; |
777 val as_time = the_default 0 o Scan.read Symbol.stopper time o explode; |
779 in (output, as_time t) end; |
778 in (output, as_time t) end; |
780 fun run_on probfile = |
779 fun run_on probfile = |
781 if home = "" then |
780 case filter (curry (op =) "" o getenv o fst) |
|
781 (executable :: required_executables) of |
|
782 (home_var, _) :: _ => |
782 error ("The environment variable " ^ quote home_var ^ " is not set.") |
783 error ("The environment variable " ^ quote home_var ^ " is not set.") |
783 else if File.exists command then |
784 | [] => |
784 let |
785 if File.exists command then |
785 fun do_run complete = |
786 let |
786 let |
787 fun do_run complete = |
787 val command = command_line complete probfile |
788 let |
788 val ((output, msecs), res_code) = |
789 val command = command_line complete probfile |
789 bash_output command |
790 val ((output, msecs), res_code) = |
790 |>> (if overlord then |
791 bash_output command |
791 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
792 |>> (if overlord then |
792 else |
793 prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") |
793 I) |
794 else |
794 |>> (if Config.get ctxt measure_runtime then split_time |
795 I) |
795 else rpair 0) |
796 |>> (if Config.get ctxt measure_runtime then split_time |
796 val (proof, outcome) = |
797 else rpair 0) |
797 extract_proof_and_outcome complete res_code proof_delims |
798 val (proof, outcome) = |
798 known_failures output |
799 extract_proof_and_outcome complete res_code proof_delims |
799 in (output, msecs, proof, outcome) end |
800 known_failures output |
800 val readable_names = debug andalso overlord |
801 in (output, msecs, proof, outcome) end |
801 val (pool, conjecture_offset) = |
802 val readable_names = debug andalso overlord |
802 write_tptp_file thy readable_names explicit_forall full_types |
803 val (pool, conjecture_offset) = |
803 explicit_apply probfile clauses |
804 write_tptp_file thy readable_names explicit_forall full_types |
804 val conjecture_shape = |
805 explicit_apply probfile clauses |
805 conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |
806 val conjecture_shape = |
806 val result = |
807 conjecture_offset + 1 upto conjecture_offset + length hyp_ts + 1 |
807 do_run false |
808 val result = |
808 |> (fn (_, msecs0, _, SOME _) => |
809 do_run false |
809 do_run true |
810 |> (fn (_, msecs0, _, SOME _) => |
810 |> (fn (output, msecs, proof, outcome) => |
811 do_run true |
811 (output, msecs0 + msecs, proof, outcome)) |
812 |> (fn (output, msecs, proof, outcome) => |
812 | result => result) |
813 (output, msecs0 + msecs, proof, outcome)) |
813 in ((pool, conjecture_shape), result) end |
814 | result => result) |
814 else |
815 in ((pool, conjecture_shape), result) end |
815 error ("Bad executable: " ^ Path.implode command ^ "."); |
816 else |
|
817 error ("Bad executable: " ^ Path.implode command ^ ".") |
816 |
818 |
817 (* If the problem file has not been exported, remove it; otherwise, export |
819 (* If the problem file has not been exported, remove it; otherwise, export |
818 the proof file too. *) |
820 the proof file too. *) |
819 fun cleanup probfile = |
821 fun cleanup probfile = |
820 if the_dest_dir = "" then try File.rm probfile else NONE |
822 if the_dest_dir = "" then try File.rm probfile else NONE |