Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
--- a/etc/settings Tue Oct 18 17:59:37 2005 +0200
+++ b/etc/settings Wed Oct 19 06:33:24 2005 +0200
@@ -87,6 +87,11 @@
# 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"
--- a/src/HOL/IsaMakefile Tue Oct 18 17:59:37 2005 +0200
+++ b/src/HOL/IsaMakefile Wed Oct 19 06:33:24 2005 +0200
@@ -113,8 +113,11 @@
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 \
- thy_syntax.ML
+ document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML \
+ thy_syntax.ML \
+ ResAtpOracle.thy \
+ 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
--- a/src/HOL/Main.thy Tue Oct 18 17:59:37 2005 +0200
+++ b/src/HOL/Main.thy Wed Oct 19 06:33:24 2005 +0200
@@ -5,7 +5,7 @@
header {* Main HOL *}
theory Main
-imports SAT Reconstruction
+imports SAT Reconstruction ResAtpMethods
begin
text {*
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ResAtpMethods.thy Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,16 @@
+(* ID: $Id$
+ Author: Jia Meng
+ a method to setup "vampire" method
+ a method to setup "eprover" method
+*)
+
+theory ResAtpMethods
+ imports Reconstruction ResAtpOracle
+
+ uses "Tools/res_atp_setup.ML"
+ "Tools/res_atp_methods.ML"
+
+begin
+setup ResAtpMethods.ResAtps_setup
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ResAtpOracle.thy Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,28 @@
+(* ID: $Id$
+ Author: Jia Meng
+
+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
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_atp_methods.ML Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,50 @@
+(* ID: $Id$
+ Author: Jia Meng
+*)
+
+
+structure ResAtpMethods =
+
+struct
+
+
+val vampire_time = ref 60;
+val eprover_time = ref 60;
+
+fun run_vampire time =
+ if (time >0) then vampire_time:= time
+ else vampire_time:=60;
+
+fun run_eprover time =
+ if (time > 0) then eprover_time:= time
+ else eprover_time:=60;
+
+fun vampireLimit () = !vampire_time;
+fun eproverLimit () = !eprover_time;
+
+
+
+(* convert the negated 1st subgoal into CNF, write to files and call an ATP oracle *)
+fun res_atp_tac res_atp_oracle timeLimit ctxt files tfrees n thm =
+ SELECT_GOAL
+ ((EVERY1 [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac,
+ METAHYPS(fn negs =>
+ HEADGOAL(Tactic.rtac
+ (res_atp_oracle (ProofContext.theory_of ctxt)
+ ((ResAtpSetup.tptp_form (make_clauses (map make_nnf negs)) n tfrees)::files, timeLimit))))]) handle Fail _ => no_tac) n thm;
+
+
+(* vampire_tac and eprover_tac *)
+val vampire_tac = res_atp_tac vampire_oracle (!vampire_time);
+
+val eprover_tac = res_atp_tac eprover_oracle (!eprover_time);
+
+
+val ResAtps_setup = [Method.add_methods
+ [("vampire", ResAtpSetup.atp_method vampire_tac, "A Vampire method"),
+ ("eprover", ResAtpSetup.atp_method eprover_tac, "A E prover method")]];
+
+
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_atp_provers.ML Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,50 @@
+(* ID: $Id$
+ Author: Jia Meng
+
+Functions used for ATP Oracle.
+*)
+
+
+structure ResAtpProvers =
+
+struct
+
+fun if_proof_vampire instr = (TextIO.inputLine instr = "Refutation found. Thanks to Tanya!\n");
+
+fun if_proof_E instr =
+ let val thisLine = TextIO.inputLine instr
+ in
+ if thisLine = "# Proof found!\n"
+ then true
+ else if (thisLine = "") then false
+ else if_proof_E instr end;
+
+fun call_vampire (files:string list, time: int) =
+ let val output = (space_implode " " files) ^ " "
+ val runtime = "-t " ^ (string_of_int time)
+ val vampire = ResAtp.helper_path "VAMPIRE_HOME" "vampire"
+ val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(vampire, [runtime,output])
+ val (instr,outstr) = Unix.streamsOf ch
+ in if_proof_vampire instr
+ end;
+
+fun call_eprover (files:string list, time:int) =
+ let val output = (space_implode " " files) ^ " "
+ val eprover = ResAtp.helper_path "E_HOME" "/PROVER/eprover"
+ val runtime = "--cpu-limit=" ^ (string_of_int time)
+ val ch:(TextIO.instream,TextIO.outstream) Unix.proc = Unix.execute(eprover, [runtime,"--tptp-format","-tAuto","-xAuto",output])
+ val (instr,outstr) = Unix.streamsOf ch
+ in if_proof_E instr
+ end;
+
+
+
+fun vampire_o thy (files,time) = (if (call_vampire (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
+ else (ResAtpSetup.cond_rm_tmp files;raise Fail ("vampire oracle failed")));
+
+
+fun eprover_o thy (files,time) = (if (call_eprover (files,time)) then (ResAtpSetup.cond_rm_tmp files;HOLogic.mk_Trueprop HOLogic.false_const)
+ else (raise Fail ("eprover oracle failed")));
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/res_atp_setup.ML Wed Oct 19 06:33:24 2005 +0200
@@ -0,0 +1,234 @@
+(* Author: Jia Meng
+ Date: 12/09/2005
+
+*)
+structure ResAtpSetup =
+
+struct
+
+val keep_atp_input = ref false;
+val debug = ref true;
+val filter_ax = ref false;
+
+
+fun writeln_strs _ [] = ()
+ | 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 =
+ let val _ = warning ("total " ^ (string_of_int n) ^ " " ^ nm)
+ fun warning_thms_aux [] = warning ("no more " ^ nm)
+ | warning_thms_aux (th::ths) = (warning_thm th nm; warning_thms_aux ths)
+ in
+ warning_thms_aux thms
+ end;
+
+
+(*******************************************************)
+(* set up the output paths *)
+(*******************************************************)
+
+val claset_file = File.tmp_path (Path.basic "claset");
+val simpset_file = File.tmp_path (Path.basic "simp");
+
+val prob_file = File.tmp_path (Path.basic "prob");
+val hyps_file = File.tmp_path (Path.basic "hyps");
+
+
+
+(*******************************************************)
+(* operations on Isabelle theorems: *)
+(* retrieving from ProofContext, *)
+(* modifying local theorems, *)
+(* CNF *)
+(*******************************************************)
+
+fun repeat_RS thm1 thm2 =
+ let val thm1' = thm1 RS thm2 handle THM _ => thm1
+ in
+ if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
+ end;
+
+(* a special version of repeat_RS *)
+fun repeat_someI_ex thm = repeat_RS thm someI_ex;
+
+val include_simpset = ref false;
+val include_claset = ref false;
+
+val add_simpset = (fn () => include_simpset:=true);
+val add_claset = (fn () => include_claset:=true);
+val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
+val rm_simpset = (fn () => include_simpset:=false);
+val rm_claset = (fn () => include_claset:=false);
+val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
+
+
+
+val rules_modifiers =
+ Simplifier.simp_modifiers @ Splitter.split_modifiers @
+ Classical.cla_modifiers @ iff_modifiers;
+
+
+
+fun get_local_claR ctxt =
+ let val cla_rules = rep_cs (Classical.get_local_claset ctxt)
+ val safeEs = #safeEs cla_rules
+ val safeIs = #safeIs cla_rules
+ val hazEs = #hazEs cla_rules
+ val hazIs = #hazIs cla_rules
+ in
+ map ResAxioms.pairname (safeEs @ safeIs @ hazEs @ hazIs)
+ end;
+
+
+fun get_local_simpR ctxt =
+ let val simpset_rules = #rules(fst (rep_ss (Simplifier.get_local_simpset ctxt)))
+ in
+ map (fn r => (#name r, #thm r)) (Net.entries simpset_rules) end;
+
+
+
+(***************************************************************)
+(* prover-specific output format: *)
+(* TPTP *)
+(***************************************************************)
+
+
+
+
+(***************** TPTP format *********************************)
+
+(* convert each (sub)goal clause (Thm.thm) into one or more TPTP clauses. The additional TPTP clauses are tfree_lits. Write the output TPTP clauses to a problem file *)
+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 probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
+ val out = TextIO.openOut(probfile)
+ in
+ writeln_strs out (tfree_clss @ tptp_clss);
+ TextIO.closeOut out;
+ warning probfile; (* show the location for debugging *)
+ probfile (* return the location *)
+
+ end;
+
+
+fun tptp_hyps [] = ([], [])
+ | tptp_hyps thms =
+ let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
+ val prems' = map repeat_someI_ex prems
+ val prems'' = make_clauses prems'
+ 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_clss = map ResClause.tfree_clause tfree_lits
+ val hypsfile = File.platform_path hyps_file
+ val out = TextIO.openOut(hypsfile)
+ in
+ writeln_strs out (tfree_clss @ tptp_clss);
+ TextIO.closeOut out; warning hypsfile;
+ ([hypsfile],tfree_lits)
+ end;
+
+
+fun subtract_simpset thy ctxt =
+ let
+ val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
+ val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
+ in map ResAxioms.pairname (map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2)) end;
+
+fun subtract_claset thy ctxt =
+ let
+ val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
+ val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
+ val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
+ in map ResAxioms.pairname (subtract netI1 netI2 @ subtract netE1 netE2) end;
+
+local
+
+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',names) = ListPair.unzip clss
+ val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
+ in
+ writeln_strs out tptpclss;
+ TextIO.closeOut out; warning file;
+ [file]
+ end;
+
+in
+
+(* TPTP Isabelle theorems *)
+fun tptp_cnf_rules (clasetR,simpsetR) =
+ let val simpfile = File.platform_path simpset_file
+ val clafile = File.platform_path claset_file
+ in
+ (write_rules clasetR clafile) @ (write_rules simpsetR simpfile)
+ end;
+
+end
+
+fun tptp_cnf_clasimp ctxt (include_claset,include_simpset) =
+ let val local_claR = if include_claset then get_local_claR ctxt else (subtract_claset (ProofContext.theory_of ctxt) ctxt)
+ val local_simpR = if include_simpset then get_local_simpR ctxt else (subtract_simpset (ProofContext.theory_of ctxt) ctxt)
+
+ in
+ tptp_cnf_rules (local_claR,local_simpR)
+ end;
+
+
+(*FIXME: a function that does not perform any filtering now *)
+fun find_relevant_ax ctxt = tptp_cnf_clasimp ctxt (true,true);
+
+
+
+(***************************************************************)
+(* 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))
+ 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)))
+ end;
+
+
+fun atp_meth tac prems ctxt =
+ let val _ = ResClause.init (ProofContext.theory_of ctxt)
+ in
+ if not(List.null prems) then (warning_thms_n (length prems) prems "prems!!!"; atp_meth' tac prems ctxt)
+ else (atp_meth' tac prems ctxt)
+ end;
+
+val atp_method = Method.bang_sectioned_args rules_modifiers o atp_meth;
+
+
+
+
+(*************Remove tmp files********************************)
+fun rm_tmp_files1 [] = ()
+ | 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));
+
+
+end
\ No newline at end of file
--- a/src/HOL/Tools/res_axioms.ML Tue Oct 18 17:59:37 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Oct 19 06:33:24 2005 +0200
@@ -23,6 +23,7 @@
val clausify_rules_pairs : (string*thm) list -> (ResClause.clause*thm) list list
val clause_setup : (theory -> theory) list
val meson_method_setup : (theory -> theory) list
+ val pairname : thm -> (string * thm)
end;
structure ResAxioms : RES_AXIOMS =