# HG changeset patch # User wenzelm # Date 1224007845 -7200 # Node ID fcd463a6b6de0cea75f050e40b0b4cbe4c1f7713 # Parent 67e3945b53f143c5cef7eb60c3377df8792091e1 tuned interfaces -- plain prover function, without thread; misc tuning and simplification; reduced NJ basis library stuff to bare minimum; diff -r 67e3945b53f1 -r fcd463a6b6de src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Tue Oct 14 20:10:44 2008 +0200 +++ b/src/HOL/Tools/atp_wrapper.ML Tue Oct 14 20:10:45 2008 +0200 @@ -7,144 +7,159 @@ signature ATP_WRAPPER = sig - (* hooks for writing problemfiles *) val destdir: string ref val problem_name: string ref - (* basic template *) val external_prover: ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) -> Path.T * string -> (string * int -> bool) -> (string * string vector * Proof.context * thm * int -> string) -> - int -> Proof.state -> Thread.thread - (* provers as functions returning threads *) - val tptp_prover_filter_opts_full: int -> bool -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val tptp_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val remote_prover_filter_opts: int -> bool -> string -> string -> int -> Proof.state -> Thread.thread - val full_prover_filter_opts: int -> bool -> Path.T * string -> int -> Proof.state -> Thread.thread - val tptp_prover: Path.T * string -> int -> Proof.state -> Thread.thread - val remote_prover: string -> string -> int -> Proof.state -> Thread.thread - val full_prover: Path.T * string -> int -> Proof.state -> Thread.thread - val spass_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val eprover_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val eprover_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread - val vampire_filter_opts: int -> bool -> int -> Proof.state -> Thread.thread - val vampire_filter_opts_full: int -> bool -> int -> Proof.state -> Thread.thread - val spass: int -> Proof.state -> Thread.thread - val eprover: int -> Proof.state -> Thread.thread - val eprover_full: int -> Proof.state -> Thread.thread - val vampire: int -> Proof.state -> Thread.thread - val vampire_full: int -> Proof.state -> Thread.thread + AtpManager.prover + val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover + val tptp_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover + val tptp_prover: Path.T * string -> AtpManager.prover + val full_prover_opts: int -> bool -> Path.T * string -> AtpManager.prover + val full_prover: Path.T * string -> AtpManager.prover + val vampire_opts: int -> bool -> AtpManager.prover + val vampire: AtpManager.prover + val vampire_opts_full: int -> bool -> AtpManager.prover + val vampire_full: AtpManager.prover + val eprover_opts: int -> bool -> AtpManager.prover + val eprover: AtpManager.prover + val eprover_opts_full: int -> bool -> AtpManager.prover + val eprover_full: AtpManager.prover + val spass_opts: int -> bool -> AtpManager.prover + val spass: AtpManager.prover + val remote_prover_opts: int -> bool -> string -> string -> AtpManager.prover + val remote_prover: string -> string -> AtpManager.prover end; structure AtpWrapper: ATP_WRAPPER = struct - - (* preferences for path and filename to problemfiles *) - val destdir = ref ""; (*Empty means write files to /tmp*) - val problem_name = ref "prob"; - - (*Setting up a Thread for an external prover*) - fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = - let + +(** generic ATP wrapper **) + +(* global hooks for writing problemfiles *) + +val destdir = ref ""; (*Empty means write files to /tmp*) +val problem_name = ref "prob"; + + +(* basic template *) + +fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = + let + (* path to unique problem file *) val destdir' = ! destdir val problem_name' = ! problem_name - val (ctxt, (chain_ths, goal)) = Proof.get_goal state - (* path to unique problem file *) fun prob_pathname nr = - let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ Int.toString nr) + let val probfile = Path.basic (problem_name' ^ serial_string () ^ "_" ^ string_of_int nr) in if destdir' = "" then File.tmp_path probfile else if File.exists (Path.explode (destdir')) then Path.append (Path.explode (destdir')) probfile else error ("No such directory: " ^ destdir') end + (* write out problem file and call prover *) - fun call_prover () = - let - val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths - val (filenames, thm_names_list) = - write_problem_files prob_pathname (ctxt, chain_ths, goal) - val thm_names = List.nth (thm_names_list, subgoalno - 1); (*(i-1)th element for i-th subgoal*) + val (ctxt, (chain_ths, goal)) = Proof.get_goal state + val chain_ths = map (Thm.put_name_hint ResReconstruct.chained_hint) chain_ths + val (filenames, thm_names_list) = write_problem_files prob_pathname (ctxt, chain_ths, goal) + val thm_names = nth thm_names_list (subgoalno - 1) + + val cmdline = + if File.exists cmd then File.shell_path cmd ^ " " ^ args + else error ("Bad executable: " ^ Path.implode cmd) + val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1)) + val _ = + if rc <> 0 then + warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline) + else () - val cmdline = - if File.exists cmd then File.shell_path cmd ^ " " ^ args - else error ("Bad executable: " ^ Path.implode cmd); - val (proof, rc) = system_out (cmdline ^ " " ^ List.nth (filenames, subgoalno - 1)) - val _ = - if rc <> 0 - then warning ("Sledgehammer with command " ^ quote cmdline ^ " exited with " ^ Int.toString rc) - else () - (* remove *temporary* files *) - val _ = if destdir' = "" then app (fn file => OS.FileSys.remove file) filenames else () - in - if check_success (proof, rc) then SOME (proof, thm_names, ctxt, goal, subgoalno) - else NONE - end - in - AtpManager.atp_thread call_prover produce_answer - end; + (* remove *temporary* files *) + val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else () - - (*=========== TEMPLATES FOR AUTOMATIC PROVERS =================*) + val success = check_success (proof, rc) + val message = + if success + then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) + else "Failed." + in (success, message) end; + - fun tptp_prover_filter_opts_full max_new theory_const full command sg = - external_prover + +(** common provers **) + +(* generic TPTP-based provers *) + +fun tptp_prover_opts_full max_new theory_const full command = + external_prover (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) command ResReconstruct.check_success_e_vamp_spass - (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp) - sg - - (* arbitrary atp with tptp input/output and problemfile as last argument*) - fun tptp_prover_filter_opts max_new theory_const = - tptp_prover_filter_opts_full max_new theory_const false; - (* default settings*) - val tptp_prover = tptp_prover_filter_opts 60 true; + (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp); + +(*arbitrary ATP with TPTP input/output and problemfile as last argument*) +fun tptp_prover_opts max_new theory_const = + tptp_prover_opts_full max_new theory_const false; + +val tptp_prover = tptp_prover_opts 60 true; + +(*for structured proofs: prover must support TSTP*) +fun full_prover_opts max_new theory_const = + tptp_prover_opts_full max_new theory_const true; + +val full_prover = full_prover_opts 60 true; + - (* for structured proofs: prover must support TSTP *) - fun full_prover_filter_opts max_new theory_const = - tptp_prover_filter_opts_full max_new theory_const true; - (* default settings*) - val full_prover = full_prover_filter_opts 60 true; +(* Vampire *) + +(*NB: Vampire does not work without explicit timelimit*) + +fun vampire_opts max_new theory_const = tptp_prover_opts + max_new theory_const + (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600"); + +val vampire = vampire_opts 60 false; + +fun vampire_opts_full max_new theory_const = full_prover_opts + max_new theory_const + (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600"); + +val vampire_full = vampire_opts 60 false; + - fun vampire_filter_opts max_new theory_const = tptp_prover_filter_opts - max_new theory_const - (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) - (* default settings*) - val vampire = vampire_filter_opts 60 false; - - (* a vampire for full proof output *) - fun vampire_filter_opts_full max_new theory_const = full_prover_filter_opts - max_new theory_const - (Path.explode "$VAMPIRE_HOME/vampire", "--output_syntax tptp --mode casc -t 3600") (* vampire does not work without timelimit*) - (* default settings*) - val vampire_full = vampire_filter_opts 60 false; +(* E prover *) + +fun eprover_opts max_new theory_const = tptp_prover_opts + max_new theory_const + (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent"); + +val eprover = eprover_opts 100 false; + +fun eprover_opts_full max_new theory_const = full_prover_opts + max_new theory_const + (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent"); + +val eprover_full = eprover_opts_full 100 false; + + +(* SPASS *) - fun eprover_filter_opts max_new theory_const = tptp_prover_filter_opts - max_new theory_const - (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") - (* default settings *) - val eprover = eprover_filter_opts 100 false; - - (* an E for full proof output*) - fun eprover_filter_opts_full max_new theory_const = full_prover_filter_opts - max_new theory_const - (Path.explode "$E_HOME/eproof", "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent") - (* default settings *) - val eprover_full = eprover_filter_opts_full 100 false; +fun spass_opts max_new theory_const = external_prover + (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) + (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") + ResReconstruct.check_success_e_vamp_spass + ResReconstruct.lemma_list_dfg; + +val spass = spass_opts 40 true; - fun spass_filter_opts max_new theory_const = external_prover - (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) - (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") - ResReconstruct.check_success_e_vamp_spass - ResReconstruct.lemma_list_dfg - (* default settings*) - val spass = spass_filter_opts 40 true; - - (* remote prover invocation via SystemOnTPTP *) - fun remote_prover_filter_opts max_new theory_const name command = - tptp_prover_filter_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command) - val remote_prover = remote_prover_filter_opts 60 false + +(* remote prover invocation via SystemOnTPTP *) + +fun remote_prover_opts max_new theory_const name command = + tptp_prover_opts max_new theory_const + (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ command); + +val remote_prover = remote_prover_opts 60 false; end;