1.1 --- a/src/HOL/Tools/atp_wrapper.ML Tue Aug 04 16:13:16 2009 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,218 +0,0 @@
1.4 -(* Title: HOL/Tools/atp_wrapper.ML
1.5 - Author: Fabian Immler, TU Muenchen
1.6 -
1.7 -Wrapper functions for external ATPs.
1.8 -*)
1.9 -
1.10 -signature ATP_WRAPPER =
1.11 -sig
1.12 - val destdir: string ref
1.13 - val problem_name: string ref
1.14 - val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover
1.15 - val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
1.16 - val tptp_prover: Path.T * string -> AtpManager.prover
1.17 - val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover
1.18 - val full_prover: Path.T * string -> AtpManager.prover
1.19 - val vampire_opts: int -> bool -> AtpManager.prover
1.20 - val vampire: AtpManager.prover
1.21 - val vampire_opts_full: int -> bool -> AtpManager.prover
1.22 - val vampire_full: AtpManager.prover
1.23 - val eprover_opts: int -> bool -> AtpManager.prover
1.24 - val eprover: AtpManager.prover
1.25 - val eprover_opts_full: int -> bool -> AtpManager.prover
1.26 - val eprover_full: AtpManager.prover
1.27 - val spass_opts: int -> bool -> AtpManager.prover
1.28 - val spass: AtpManager.prover
1.29 - val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover
1.30 - val remote_prover: string -> string -> AtpManager.prover
1.31 - val refresh_systems: unit -> unit
1.32 -end;
1.33 -
1.34 -structure AtpWrapper: ATP_WRAPPER =
1.35 -struct
1.36 -
1.37 -(** generic ATP wrapper **)
1.38 -
1.39 -(* global hooks for writing problemfiles *)
1.40 -
1.41 -val destdir = ref ""; (*Empty means write files to /tmp*)
1.42 -val problem_name = ref "prob";
1.43 -
1.44 -
1.45 -(* basic template *)
1.46 -
1.47 -fun external_prover relevance_filter preparer writer (cmd, args) find_failure produce_answer
1.48 - timeout axiom_clauses filtered_clauses name subgoalno goal =
1.49 - let
1.50 - (* path to unique problem file *)
1.51 - val destdir' = ! destdir
1.52 - val problem_name' = ! problem_name
1.53 - fun prob_pathname nr =
1.54 - let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr)
1.55 - in if destdir' = "" then File.tmp_path probfile
1.56 - else if File.exists (Path.explode (destdir'))
1.57 - then Path.append (Path.explode (destdir')) probfile
1.58 - else error ("No such directory: " ^ destdir')
1.59 - end
1.60 -
1.61 - (* get clauses and prepare them for writing *)
1.62 - val (ctxt, (chain_ths, th)) = goal
1.63 - val thy = ProofContext.theory_of ctxt
1.64 - val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths
1.65 - val goal_cls = #1 (ResAxioms.neg_conjecture_clauses ctxt th subgoalno)
1.66 - val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm ctxt th)) goal_cls
1.67 - val the_filtered_clauses =
1.68 - case filtered_clauses of
1.69 - NONE => relevance_filter goal goal_cls
1.70 - | SOME fcls => fcls
1.71 - val the_axiom_clauses =
1.72 - case axiom_clauses of
1.73 - NONE => the_filtered_clauses
1.74 - | SOME axcls => axcls
1.75 - val (thm_names, clauses) =
1.76 - preparer goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy
1.77 -
1.78 - (* write out problem file and call prover *)
1.79 - val probfile = prob_pathname subgoalno
1.80 - val conj_pos = writer probfile clauses
1.81 - val (proof, rc) = system_out (
1.82 - if File.exists cmd then
1.83 - space_implode " " ["exec", File.shell_path cmd, args, File.platform_path probfile]
1.84 - else error ("Bad executable: " ^ Path.implode cmd))
1.85 -
1.86 - (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
1.87 - val _ =
1.88 - if destdir' = "" then File.rm probfile
1.89 - else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof
1.90 -
1.91 - (* check for success and print out some information on failure *)
1.92 - val failure = find_failure proof
1.93 - val success = rc = 0 andalso is_none failure
1.94 - val message =
1.95 - if is_some failure then "External prover failed."
1.96 - else if rc <> 0 then "External prover failed: " ^ proof
1.97 - else "Try this command: " ^
1.98 - produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoalno)
1.99 - val _ = Output.debug (fn () => "Sledgehammer response (rc = " ^ string_of_int rc ^ "):\n" ^ proof)
1.100 - in (success, message, proof, thm_names, the_filtered_clauses) end;
1.101 -
1.102 -
1.103 -
1.104 -(** common provers **)
1.105 -
1.106 -(* generic TPTP-based provers *)
1.107 -
1.108 -fun tptp_prover_opts_full max_new theory_const full command timeout ax_clauses fcls name n goal =
1.109 - external_prover
1.110 - (ResAtp.get_relevant max_new theory_const)
1.111 - (ResAtp.prepare_clauses false)
1.112 - (ResHolClause.tptp_write_file (AtpManager.get_full_types()))
1.113 - command
1.114 - ResReconstruct.find_failure
1.115 - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list false)
1.116 - timeout ax_clauses fcls name n goal;
1.117 -
1.118 -(*arbitrary ATP with TPTP input/output and problemfile as last argument*)
1.119 -fun tptp_prover_opts max_new theory_const =
1.120 - tptp_prover_opts_full max_new theory_const false;
1.121 -
1.122 -fun tptp_prover x = tptp_prover_opts 60 true x;
1.123 -
1.124 -(*for structured proofs: prover must support TSTP*)
1.125 -fun full_prover_opts max_new theory_const =
1.126 - tptp_prover_opts_full max_new theory_const true;
1.127 -
1.128 -fun full_prover x = full_prover_opts 60 true x;
1.129 -
1.130 -
1.131 -(* Vampire *)
1.132 -
1.133 -(*NB: Vampire does not work without explicit timelimit*)
1.134 -
1.135 -fun vampire_opts max_new theory_const timeout = tptp_prover_opts
1.136 - max_new theory_const
1.137 - (Path.explode "$VAMPIRE_HOME/vampire",
1.138 - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
1.139 - timeout;
1.140 -
1.141 -val vampire = vampire_opts 60 false;
1.142 -
1.143 -fun vampire_opts_full max_new theory_const timeout = full_prover_opts
1.144 - max_new theory_const
1.145 - (Path.explode "$VAMPIRE_HOME/vampire",
1.146 - ("--output_syntax tptp --mode casc -t " ^ string_of_int timeout))
1.147 - timeout;
1.148 -
1.149 -val vampire_full = vampire_opts_full 60 false;
1.150 -
1.151 -
1.152 -(* E prover *)
1.153 -
1.154 -fun eprover_opts max_new theory_const timeout = tptp_prover_opts
1.155 - max_new theory_const
1.156 - (Path.explode "$E_HOME/eproof",
1.157 - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
1.158 - timeout;
1.159 -
1.160 -val eprover = eprover_opts 100 false;
1.161 -
1.162 -fun eprover_opts_full max_new theory_const timeout = full_prover_opts
1.163 - max_new theory_const
1.164 - (Path.explode "$E_HOME/eproof",
1.165 - "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent --cpu-limit=" ^ string_of_int timeout)
1.166 - timeout;
1.167 -
1.168 -val eprover_full = eprover_opts_full 100 false;
1.169 -
1.170 -
1.171 -(* SPASS *)
1.172 -
1.173 -fun spass_opts max_new theory_const timeout ax_clauses fcls name n goal = external_prover
1.174 - (ResAtp.get_relevant max_new theory_const)
1.175 - (ResAtp.prepare_clauses true)
1.176 - (ResHolClause.dfg_write_file (AtpManager.get_full_types()))
1.177 - (Path.explode "$SPASS_HOME/SPASS",
1.178 - "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof -TimeLimit=" ^
1.179 - string_of_int timeout)
1.180 - ResReconstruct.find_failure
1.181 - (ResReconstruct.lemma_list true)
1.182 - timeout ax_clauses fcls name n goal;
1.183 -
1.184 -val spass = spass_opts 40 true;
1.185 -
1.186 -
1.187 -(* remote prover invocation via SystemOnTPTP *)
1.188 -
1.189 -val systems =
1.190 - Synchronized.var "atp_wrapper_systems" ([]: string list);
1.191 -
1.192 -fun get_systems () =
1.193 - let
1.194 - val (answer, rc) = system_out (("$ISABELLE_HOME/lib/scripts/SystemOnTPTP" |>
1.195 - Path.explode |> File.shell_path) ^ " -w")
1.196 - in
1.197 - if rc <> 0 then error ("Get available systems from SystemOnTPTP:\n" ^ answer)
1.198 - else split_lines answer
1.199 - end;
1.200 -
1.201 -fun refresh_systems () = Synchronized.change systems (fn _ =>
1.202 - get_systems ());
1.203 -
1.204 -fun get_system prefix = Synchronized.change_result systems (fn systems =>
1.205 - let val systems = if null systems then get_systems() else systems
1.206 - in (find_first (String.isPrefix prefix) systems, systems) end);
1.207 -
1.208 -fun remote_prover_opts max_new theory_const args prover_prefix timeout =
1.209 - let val sys =
1.210 - case get_system prover_prefix of
1.211 - NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
1.212 - | SOME sys => sys
1.213 - in tptp_prover_opts max_new theory_const
1.214 - (Path.explode "$ISABELLE_HOME/lib/scripts/SystemOnTPTP",
1.215 - args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
1.216 - end;
1.217 -
1.218 -val remote_prover = remote_prover_opts 60 false;
1.219 -
1.220 -end;
1.221 -