1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML Tue Aug 04 19:20:24 2009 +0200
1.3 @@ -0,0 +1,217 @@
1.4 +(* Title: HOL/Tools/ATP_Manager/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_ATP_MANAGER/SystemOnTPTP\" -w")
1.195 + in
1.196 + if rc <> 0 then error ("Failed to get available systems from SystemOnTPTP:\n" ^ answer)
1.197 + else split_lines answer
1.198 + end;
1.199 +
1.200 +fun refresh_systems () = Synchronized.change systems (fn _ =>
1.201 + get_systems ());
1.202 +
1.203 +fun get_system prefix = Synchronized.change_result systems (fn systems =>
1.204 + let val systems = if null systems then get_systems() else systems
1.205 + in (find_first (String.isPrefix prefix) systems, systems) end);
1.206 +
1.207 +fun remote_prover_opts max_new theory_const args prover_prefix timeout =
1.208 + let val sys =
1.209 + case get_system prover_prefix of
1.210 + NONE => error ("No system like " ^ quote prover_prefix ^ " at SystemOnTPTP")
1.211 + | SOME sys => sys
1.212 + in tptp_prover_opts max_new theory_const
1.213 + (Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
1.214 + args ^ " -t " ^ string_of_int timeout ^ " -s " ^ sys) timeout
1.215 + end;
1.216 +
1.217 +val remote_prover = remote_prover_opts 60 false;
1.218 +
1.219 +end;
1.220 +