# HG changeset patch # User mengj # Date 1141699900 -3600 # Node ID 7681c04d8bffaf41b2148932d9879f68c7f2fae2 # Parent 45c8db82893d7b9f1ac35daaee20c1e9ae115f82 Merged res_atp_setup.ML into res_atp.ML. HOL translation is integrated with background Isabelle-ATP linkup. Both ATP methods and background linkup retrieve lemmas stored in claset, simpset and atpset. diff -r 45c8db82893d -r 7681c04d8bff src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Tue Mar 07 03:49:26 2006 +0100 +++ b/src/HOL/Tools/res_atp.ML Tue Mar 07 03:51:40 2006 +0100 @@ -1,4 +1,4 @@ -(* Author: Jia Meng, Cambridge University Computer Laboratory +(* Author: Jia Meng, Cambridge University Computer Laboratory, NICTA ID: $Id$ Copyright 2004 University of Cambridge @@ -13,19 +13,44 @@ val helper_path: string -> string -> string val problem_name: string ref val time_limit: int ref + + datatype mode = Auto | Fol | Hol + val write_subgoal_file: mode -> Proof.context -> Thm.thm list -> Thm.thm list -> int -> string + val vampire_time: int ref + val eprover_time: int ref + val run_vampire: int -> unit + val run_eprover: int -> unit + val vampireLimit: unit -> int + val eproverLimit: unit -> int + val atp_method: (ProofContext.context -> Thm.thm list -> int -> Tactical.tactic) -> + Method.src -> ProofContext.context -> Method.method + val cond_rm_tmp: string -> unit + val keep_atp_input: bool ref + val fol_keep_types: bool ref + val hol_full_types: unit -> unit + val hol_partial_types: unit -> unit + val hol_const_types_only: unit -> unit + val hol_no_types: unit -> unit + val hol_typ_level: unit -> ResHolClause.type_level + val run_relevance_filter: bool ref + end; structure ResAtp: RES_ATP = struct -val call_atp = ref false; +(********************************************************************) +(* some settings for both background automatic ATP calling procedure*) +(* and also explicit ATP invocation methods *) +(********************************************************************) + +(*** background linkup ***) +val call_atp = ref false; val hook_count = ref 0; val time_limit = ref 30; - val prover = ref "E"; (* use E as the default prover *) val custom_spass = (*specialized options for SPASS*) ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"]; - val destdir = ref ""; (*Empty means write files to /tmp*) val problem_name = ref "prob"; @@ -48,6 +73,328 @@ fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n; + +(*** ATP methods ***) +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; + +val keep_atp_input = ref false; +val fol_keep_types = ResClause.keep_types; +val hol_full_types = ResHolClause.full_types; +val hol_partial_types = ResHolClause.partial_types; +val hol_const_types_only = ResHolClause.const_types_only; +val hol_no_types = ResHolClause.no_types; +fun hol_typ_level () = ResHolClause.find_typ_level (); +fun is_typed_hol () = + let val tp_level = hol_typ_level() + in + not (tp_level = ResHolClause.T_NONE) + end; +val include_combS = ResHolClause.include_combS; +val include_min_comb = ResHolClause.include_min_comb; + +fun atp_input_file () = + let val file = !problem_name + in + if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file)) + else if File.exists (File.unpack_platform_path (!destdir)) + then !destdir ^ "/" ^ file + else error ("No such directory: " ^ !destdir) + end; + +val include_simpset = ref false; +val include_claset = ref false; +val include_atpset = ref true; +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 add_atpset = (fn () => include_atpset:=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 rm_atpset = (fn () => include_atpset:=false); + +(*** paths for HOL helper files ***) +fun full_typed_comb_inclS () = + helper_path "E_HOME" "additionals/full_comb_inclS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS"; + +fun full_typed_comb_noS () = + helper_path "E_HOME" "additionals/full_comb_noS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS"; + +fun partial_typed_comb_inclS () = + helper_path "E_HOME" "additionals/par_comb_inclS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS"; + +fun partial_typed_comb_noS () = + helper_path "E_HOME" "additionals/par_comb_noS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS"; + +fun const_typed_comb_inclS () = + helper_path "E_HOME" "additionals/const_comb_inclS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS"; + +fun const_typed_comb_noS () = + helper_path "E_HOME" "additionals/const_comb_noS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS"; + +fun untyped_comb_inclS () = + helper_path "E_HOME" "additionals/u_comb_inclS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS"; + +fun untyped_comb_noS () = + helper_path "E_HOME" "additionals/u_comb_noS" + handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS"; + +fun full_typed_HOL_helper1 () = + helper_path "E_HOME" "additionals/full_helper1" + handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1"; + +fun partial_typed_HOL_helper1 () = + helper_path "E_HOME" "additionals/par_helper1" + handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1"; + +fun const_typed_HOL_helper1 () = + helper_path "E_HOME" "additionals/const_helper1" + handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1"; + +fun untyped_HOL_helper1 () = + helper_path "E_HOME" "additionals/u_helper1" + handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1"; + +fun get_full_typed_helpers () = + (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ()); + +fun get_partial_typed_helpers () = + (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ()); + +fun get_const_typed_helpers () = + (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ()); + +fun get_untyped_helpers () = + (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ()); + +fun get_all_helpers () = + (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ()); + + +(**** relevance filter ****) +val run_relevance_filter = ref true; + +(******************************************************************) +(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *) +(******************************************************************) + +datatype logic = FOL | HOL | HOLC | HOLCS; + +fun string_of_logic FOL = "FOL" + | string_of_logic HOL = "HOL" + | string_of_logic HOLC = "HOLC" + | string_of_logic HOLCS = "HOLCS"; + + +fun is_fol_logic FOL = true + | is_fol_logic _ = false + + +(*HOLCS will not occur here*) +fun upgrade_lg HOLC _ = HOLC + | upgrade_lg HOL HOLC = HOLC + | upgrade_lg HOL _ = HOL + | upgrade_lg FOL lg = lg; + +(* check types *) +fun has_bool (Type("bool",_)) = true + | has_bool (Type(_, Ts)) = exists has_bool Ts + | has_bool _ = false; + +fun has_bool_arg tp = + let val (targs,tr) = strip_type tp + in + exists has_bool targs + end; + +fun is_fn_tp (Type("fun",_)) = true + | is_fn_tp _ = false; + + +exception FN_LG of term; + +fun fn_lg (t as Const(f,tp)) (lg,seen) = + if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + | fn_lg (t as Free(f,tp)) (lg,seen) = + if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + | fn_lg (t as Var(f,tp)) (lg,seen) = + if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen) + else (lg,t ins seen) + | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen) + | fn_lg f _ = raise FN_LG(f); + + +fun term_lg [] (lg,seen) = (lg,seen) + | term_lg (tm::tms) (FOL,seen) = + let val (f,args) = strip_comb tm + val (lg',seen') = if f mem seen then (FOL,seen) + else fn_lg f (FOL,seen) + + in + term_lg (args@tms) (lg',seen') + end + | term_lg _ (lg,seen) = (lg,seen) + +exception PRED_LG of term; + +fun pred_lg (t as Const(P,tp)) (lg,seen)= + if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + | pred_lg (t as Free(P,tp)) (lg,seen) = + if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) + | pred_lg P _ = raise PRED_LG(P); + + +fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen) + | lit_lg P (lg,seen) = + let val (pred,args) = strip_comb P + val (lg',seen') = if pred mem seen then (lg,seen) + else pred_lg pred (lg,seen) + in + term_lg args (lg',seen') + end; + +fun lits_lg [] (lg,seen) = (lg,seen) + | lits_lg (lit::lits) (FOL,seen) = + lits_lg lits (lit_lg lit (FOL,seen)) + | lits_lg lits (lg,seen) = (lg,seen); + + +fun logic_of_clause tm (lg,seen) = + let val tm' = HOLogic.dest_Trueprop tm + val disjs = HOLogic.dest_disj tm' + in + lits_lg disjs (lg,seen) + end; + +fun lits_lg [] (lg,seen) = (lg,seen) + | lits_lg (lit::lits) (FOL,seen) = + lits_lg lits (lit_lg lit (FOL,seen)) + | lits_lg lits (lg,seen) = (lg,seen); + + +fun logic_of_clause tm (lg,seen) = + let val tm' = HOLogic.dest_Trueprop tm + val disjs = HOLogic.dest_disj tm' + in + lits_lg disjs (lg,seen) + end; + +fun logic_of_clauses [] (lg,seen) = (lg,seen) + | logic_of_clauses (cls::clss) (FOL,seen) = + logic_of_clauses clss (logic_of_clause cls (FOL,seen)) + | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen); + +fun logic_of_nclauses [] (lg,seen) = (lg,seen) + | logic_of_nclauses (cls::clss) (FOL,seen) = + logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen)) + | logic_of_nclauses clss (lg,seen) = (lg,seen); + +fun problem_logic (goal_cls,rules_cls) = + let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[]) + val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1) + in + lg2 + end; + +fun problem_logic_goals_aux [] (lg,seen) = lg + | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = + problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen)); + +fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]); + + +(***************************************************************) +(* ATP invocation methods setup *) +(***************************************************************) + + +(**** prover-specific format: TPTP ****) + + +fun cnf_hyps_thms ctxt = + let val ths = ProofContext.prems_of ctxt + in + ResClause.union_all (map ResAxioms.skolem_thm ths) + end; + + +(**** write to files ****) + +datatype mode = Auto | Fol | Hol; + +fun tptp_writer logic goals filename (axioms,classrels,arities) = + if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities) + else + ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) (get_all_helpers()); + + +fun write_subgoal_file mode ctxt conjectures user_thms n = + let val conj_cls = map prop_of (make_clauses conjectures) + val hyp_cls = map prop_of (cnf_hyps_thms ctxt) + val goal_cls = conj_cls@hyp_cls + val user_rules = map ResAxioms.pairname user_thms + val (names_arr,axclauses_as_tms) = ResClasimp.get_clasimp_atp_lemmas ctxt (goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter) + val thy = ProofContext.theory_of ctxt + val prob_logic = case mode of Auto => problem_logic_goals [goal_cls] + | Fol => FOL + | Hol => HOL + val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol () + val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] + val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] + val writer = tptp_writer + val file = atp_input_file() + in + (writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses); + warning ("Writing to " ^ file); + file) + end; + + +(**** remove tmp files ****) +fun cond_rm_tmp file = + if !keep_atp_input then warning "ATP input kept..." + else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir)) + else (warning "deleting ATP inputs..."; OS.FileSys.remove file); + + +(****** setup ATPs as Isabelle methods ******) +fun atp_meth' tac ths ctxt = + Method.SIMPLE_METHOD' HEADGOAL + (tac ctxt ths); + +fun atp_meth tac ths ctxt = + let val thy = ProofContext.theory_of ctxt + val _ = ResClause.init thy + val _ = ResHolClause.init thy + in + atp_meth' tac ths ctxt + end; + +fun atp_method tac = Method.thms_ctxt_args (atp_meth tac); + +(***************************************************************) +(* automatic ATP invocation *) +(***************************************************************) + (* call prover with settings and problem file for the current subgoal *) fun watcher_call_provers sign sg_terms (childin, childout, pid) = let @@ -105,30 +452,35 @@ subgoals, each involving &&.*) fun write_problem_files pf (ctxt,th) = let val goals = Thm.prems_of th - val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)); - val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals - val _ = Output.debug ("claset and simprules total clauses = " ^ - Int.toString (Array.length clause_arr)) + val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals)) + val (names_arr, axclauses_as_terms) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *) + val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ + Int.toString (Array.length names_arr)) val thy = ProofContext.theory_of ctxt - val classrel_clauses = - if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else [] + fun get_neg_subgoals n = + if n=0 then [] + else + let val st = Seq.hd (EVERY' + [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th) + val negs = Option.valOf (metahyps_thms n st) + val negs_clauses = map prop_of (make_clauses negs) + in + negs_clauses::(get_neg_subgoals (n - 1)) + end + val neg_subgoals = get_neg_subgoals (length goals) + val goals_logic = problem_logic_goals neg_subgoals + val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol () + val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else [] val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses)) - val arity_clauses = - if !ResClause.keep_types then ResClause.arity_clause_thy thy else [] + val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else [] val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses)) - val write = if !prover = "spass" then ResClause.dfg_write_file - else ResClause.tptp_write_file - fun writenext n = - if n=0 then [] - else - (SELECT_GOAL - (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, - METAHYPS(fn negs => - (write (make_clauses negs) (pf n) - (axclauses,classrel_clauses,arity_clauses); - all_tac))]) n th; - pf n :: writenext (n-1)) - in (writenext (length goals), clause_arr) end; + val writer = (*if !prover ~= "spass" then *)tptp_writer + fun write_all [] _ = [] + | write_all (subgoal::subgoals) k = + (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1)) + in + (write_all neg_subgoals (length goals), names_arr) + end; val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid * string list) option); @@ -150,8 +502,8 @@ else let val _ = kill_last_watcher() - val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th) - val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr) + val (files,names_arr) = write_problem_files prob_pathname (ctxt,th) + val (childin, childout, pid) = Watcher.createWatcher (th, names_arr) in last_watcher_pid := SOME (childin, childout, pid, files); Output.debug ("problem files: " ^ space_implode ", " files); @@ -183,6 +535,7 @@ hook_count := !hook_count +1; Output.debug ("in hook for time: " ^ Int.toString (!hook_count)); ResClause.init thy; + ResHolClause.init thy; if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal) else isar_atp_writeonly (ctxt, goal) end);