# HG changeset patch # User mengj # Date 1129696404 -7200 # Node ID 1574533861b1df4585cd3cb0ac44020c0e741afa # Parent 21c6894b5998356f43df3ee0d04911619aa628f8 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). diff -r 21c6894b5998 -r 1574533861b1 etc/settings --- 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" diff -r 21c6894b5998 -r 1574533861b1 src/HOL/IsaMakefile --- 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 diff -r 21c6894b5998 -r 1574533861b1 src/HOL/Main.thy --- 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 {* diff -r 21c6894b5998 -r 1574533861b1 src/HOL/ResAtpMethods.thy --- /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 diff -r 21c6894b5998 -r 1574533861b1 src/HOL/ResAtpOracle.thy --- /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 diff -r 21c6894b5998 -r 1574533861b1 src/HOL/Tools/res_atp_methods.ML --- /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 diff -r 21c6894b5998 -r 1574533861b1 src/HOL/Tools/res_atp_provers.ML --- /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; + diff -r 21c6894b5998 -r 1574533861b1 src/HOL/Tools/res_atp_setup.ML --- /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 diff -r 21c6894b5998 -r 1574533861b1 src/HOL/Tools/res_axioms.ML --- 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 =