# HG changeset patch # User mengj # Date 1129856242 -7200 # Node ID 3925ab7b8a18c0eb171eeb8c3a2612bbf4a3a5ed # Parent 6c20fae2416c1dae20a7a360cbe898620a0094ba Merged theory ResAtpOracle.thy into ResAtpMethods.thy diff -r 6c20fae2416c -r 3925ab7b8a18 etc/settings --- a/etc/settings Wed Oct 19 21:53:34 2005 +0200 +++ b/etc/settings Fri Oct 21 02:57:22 2005 +0200 @@ -87,6 +87,10 @@ # The place for user configuration, heap files, etc. ISABELLE_HOME_USER=~/isabelle +# The places for external proversetc. +#VAMPIRE_HOME=~/Vampire +#E_HOME=~/E + # Where to look for isabelle tools (multiple dirs separated by ':'). ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools" diff -r 6c20fae2416c -r 3925ab7b8a18 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Oct 19 21:53:34 2005 +0200 +++ b/src/HOL/IsaMakefile Fri Oct 21 02:57:22 2005 +0200 @@ -113,8 +113,7 @@ Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \ Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy \ antisym_setup.ML arith_data.ML blastdata.ML cladata.ML \ - document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \ - ResAtpOracle.thy \ + document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \ ResAtpMethods.thy \ Tools/res_atp_setup.ML Tools/res_atp_provers.ML Tools/res_atp_methods.ML @$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL diff -r 6c20fae2416c -r 3925ab7b8a18 src/HOL/ResAtpMethods.thy --- a/src/HOL/ResAtpMethods.thy Wed Oct 19 21:53:34 2005 +0200 +++ b/src/HOL/ResAtpMethods.thy Fri Oct 21 02:57:22 2005 +0200 @@ -5,12 +5,22 @@ *) theory ResAtpMethods - imports Reconstruction ResAtpOracle + imports Reconstruction - uses "Tools/res_atp_setup.ML" - "Tools/res_atp_methods.ML" +uses ("Tools/res_atp_setup.ML") + ("Tools/res_atp_provers.ML") + ("Tools/res_atp_methods.ML") begin -setup ResAtpMethods.ResAtps_setup + +ML{*use "Tools/res_atp_setup.ML"*} +ML{*use "Tools/res_atp_provers.ML"*} +oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o*} +oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o*} + + +ML{*use "Tools/res_atp_methods.ML"*} + +setup ResAtpMethods.ResAtps_setup end diff -r 6c20fae2416c -r 3925ab7b8a18 src/HOL/ResAtpOracle.thy --- a/src/HOL/ResAtpOracle.thy Wed Oct 19 21:53:34 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,28 +0,0 @@ -(* ID: $Id$ - Author: Jia Meng, NICTA - -setup vampire prover as an oracle -setup E prover as an oracle -*) - -theory ResAtpOracle - imports HOL -uses "Tools/res_atp_setup.ML" - "Tools/res_atp_provers.ML" - -begin - - - - -oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o -*} - - - - -oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o - *} - - -end diff -r 6c20fae2416c -r 3925ab7b8a18 src/HOL/Tools/res_atp_setup.ML --- a/src/HOL/Tools/res_atp_setup.ML Wed Oct 19 21:53:34 2005 +0200 +++ b/src/HOL/Tools/res_atp_setup.ML Fri Oct 21 02:57:22 2005 +0200 @@ -15,16 +15,6 @@ | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss); -fun no_rep_add x [] = [x] - | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z); - -fun no_rep_app l1 [] = l1 - | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y; - - -fun flat_noDup [] = [] - | flat_noDup (x::y) = no_rep_app x (flat_noDup y); - fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm)); fun warning_thms_n n thms nm = @@ -114,7 +104,7 @@ fun tptp_form thms n tfrees = let val clss = ResClause.make_conjecture_clauses (map prop_of thms) val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) - val tfree_clss = map ResClause.tfree_clause ((flat_noDup tfree_litss) \\ tfrees) + val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees) val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n val out = TextIO.openOut(probfile) in @@ -134,7 +124,7 @@ val prems''' = ResAxioms.rm_Eps [] prems'' val clss = ResClause.make_conjecture_clauses prems''' val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) - val tfree_lits = flat_noDup tfree_litss + val tfree_lits = ResClause.union_all tfree_litss val tfree_clss = map ResClause.tfree_clause tfree_lits val hypsfile = File.platform_path hyps_file val out = TextIO.openOut(hypsfile) @@ -163,7 +153,7 @@ fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *) | write_rules rules file = let val out = TextIO.openOut(file) - val clss = flat_noDup(ResAxioms.clausify_rules_pairs rules) + val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules) val (clss',names) = ListPair.unzip clss val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss') in @@ -202,12 +192,14 @@ (* setup ATPs as Isabelle methods *) (***************************************************************) fun atp_meth' tac prems ctxt = - let val rules = if !filter_ax then (find_relevant_ax ctxt) else (tptp_cnf_clasimp ctxt (!include_claset, !include_simpset)) + let val rules = if !filter_ax then find_relevant_ax ctxt + else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset) val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt) val files = hyps @ rules in Method.METHOD (fn facts => - if !debug then ((warning_thms_n (length facts) facts "facts");HEADGOAL (tac ctxt files tfrees)) else (HEADGOAL (tac ctxt files tfrees))) + if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees)) + else HEADGOAL (tac ctxt files tfrees)) end; @@ -228,7 +220,9 @@ | rm_tmp_files1 (f::fs) = (OS.FileSys.remove f; rm_tmp_files1 fs); -fun cond_rm_tmp files = (if (!keep_atp_input) then (warning "ATP input kept...") else (warning "deleting ATP inputs..."; rm_tmp_files1 files)); +fun cond_rm_tmp files = + if !keep_atp_input then warning "ATP input kept..." + else (warning "deleting ATP inputs..."; rm_tmp_files1 files); end