# HG changeset patch # User wenzelm # Date 1121263643 -7200 # Node ID 6eeee59dac4cceb34e2ec1b2d4cee1ec7fe412f2 # Parent 4bb13fa6ae72705b3ade73208950073d5e000613 use Toplevel.print_state_hook instead of adhoc Proof.atp_hook; added call_atp: bool ref; do 'setmp print_mode []', which is more robust than manual ref manipulation; added subtract_simpset, subtract_claset (supercede delta approximation); diff -r 4bb13fa6ae72 -r 6eeee59dac4c src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Jul 13 16:07:22 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Jul 13 16:07:23 2005 +0200 @@ -1,46 +1,36 @@ (* Author: Jia Meng, Cambridge University Computer Laboratory - ID: $Id$ - Copyright 2004 University of Cambridge ATPs with TPTP format input. *) -(*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*) -(*Claire: changed: added actual watcher calls *) - - -signature RES_ATP = -sig -val trace_res : bool ref -val subgoals: Thm.thm list -val traceflag : bool ref -val axiom_file : Path.T -val hyps_file : Path.T -val isar_atp : ProofContext.context * Thm.thm -> unit -val prob_file : Path.T; -(*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*) +signature RES_ATP = +sig + val call_atp: bool ref + val trace_res : bool ref + val traceflag : bool ref + val axiom_file : Path.T + val hyps_file : Path.T + val prob_file : Path.T; +(*val atp_ax_tac : thm list -> int -> Tactical.tactic*) (*val atp_tac : int -> Tactical.tactic*) -val debug: bool ref -val full_spass: bool ref + val debug: bool ref + val full_spass: bool ref (*val spass: bool ref*) -val vampire: bool ref -val custom_spass :string list ref + val vampire: bool ref + val custom_spass: string list ref end; -structure ResAtp : RES_ATP = - +structure ResAtp: RES_ATP = struct -val subgoals = []; +val call_atp = ref false; val traceflag = ref true; -(* used for debug *) val debug = ref false; -fun debug_tac tac = (warning "testing";tac); -(* default value is false *) +fun debug_tac tac = (warning "testing"; tac); val full_spass = ref false; @@ -55,41 +45,37 @@ val skolem_tac = skolemize_tac; val num_of_clauses = ref 0; -val clause_arr = Array.array(3500, ("empty", 0)); +val clause_arr = Array.array (3500, ("empty", 0)); val atomize_tac = SUBGOAL (fn (prop,_) => - let val ts = Logic.strip_assums_hyp prop - in EVERY1 - [METAHYPS - (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), - REPEAT_DETERM_N (length ts) o (etac thin_rl)] + let val ts = Logic.strip_assums_hyp prop + in EVERY1 + [METAHYPS + (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), + REPEAT_DETERM_N (length ts) o (etac thin_rl)] end); (* temporarily use these files, which will be loaded by Vampire *) -val file_id_num =ref 0; - -fun new_prob_file () = (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num))); - +val file_id_num = ref 0; +fun new_prob_file () = "prob" ^ string_of_int (inc file_id_num); val axiom_file = File.tmp_path (Path.basic "axioms"); val clasimp_file = File.tmp_path (Path.basic "clasimp"); val hyps_file = File.tmp_path (Path.basic "hyps"); val prob_file = File.tmp_path (Path.basic "prob"); -val dummy_tac = PRIMITIVE(fn thm => thm ); +val dummy_tac = all_tac; - + (**** for Isabelle/ML interface ****) -fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") +fun is_proof_char ch = + (33 <= ord ch andalso ord ch <= 126 andalso ord ch <> 63) + orelse ch = " "; -fun proofstring x = let val exp = explode x - in - List.filter (is_proof_char ) exp - end - +val proofstring = List.filter is_proof_char o explode; (* @@ -103,7 +89,7 @@ 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) + if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2) end; (* a special version of repeat_RS *) @@ -115,7 +101,6 @@ (*********************************************************************) (*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *) fun isar_atp_h 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' @@ -126,9 +111,11 @@ (* tfree clause is different in tptp and dfg versions *) val tfree_clss = map ResClause.tfree_clause tfree_lits val hypsfile = File.platform_path hyps_file - val out = TextIO.openOut(hypsfile) + val out = TextIO.openOut(hypsfile) in - ((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) + (ResLib.writeln_strs out (tfree_clss @ tptp_clss); + TextIO.closeOut out; if !trace_res then (warning hypsfile) else ()); + tfree_lits end; @@ -137,18 +124,21 @@ (* where N is the number of this subgoal *) (*********************************************************************) -fun tptp_inputs_tfrees thms n tfrees = - let val _ = (warning ("in tptp_inputs_tfrees 0")) - val clss = map (ResClause.make_conjecture_clause_thm) thms - val _ = (warning ("in tptp_inputs_tfrees 1")) - val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) - val _ = (warning ("in tptp_inputs_tfrees 2")) - val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) - val _ = (warning ("in tptp_inputs_tfrees 3")) - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - val out = TextIO.openOut(probfile) +fun tptp_inputs_tfrees thms n tfrees = + let + val _ = warning ("in tptp_inputs_tfrees 0") + val clss = map (ResClause.make_conjecture_clause_thm) thms + val _ = warning ("in tptp_inputs_tfrees 1") + val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) + val _ = warning ("in tptp_inputs_tfrees 2") + val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) + val _ = warning ("in tptp_inputs_tfrees 3") + val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n + val out = TextIO.openOut(probfile) in - (ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) + ResLib.writeln_strs out (tfree_clss @ tptp_clss); + TextIO.closeOut out; + if !trace_res then (warning probfile) else () end; @@ -176,87 +166,84 @@ (* should be modified to allow other provers to be called *) (*********************************************************************) (* now passing in list of skolemized thms and list of sgterms to go with them *) -fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = - let - val axfile = (File.platform_path axiom_file) +fun call_resolve_tac (thms: thm list list) sign (sg_terms: term list) (childin, childout,pid) n = + let + val axfile = (File.platform_path axiom_file) val hypsfile = (File.platform_path hyps_file) - val clasimpfile = (File.platform_path clasimp_file) - val spass_home = getenv "SPASS_HOME" - - - fun make_atp_list [] sign n = [] - | make_atp_list ((sko_thm, sg_term)::xs) sign n = - let + val clasimpfile = (File.platform_path clasimp_file) - val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) - val thmproofstr = proofstring ( skothmstr) - val no_returns =List.filter not_newline ( thmproofstr) - val thmstr = implode no_returns - val _ = warning ("thmstring in make_atp_lists is: "^thmstr) + fun make_atp_list [] sign n = [] + | make_atp_list ((sko_thm, sg_term)::xs) sign n = + let + val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) + val thmproofstr = proofstring ( skothmstr) + val no_returns = filter_out (equal "\n") thmproofstr + val thmstr = implode no_returns + val _ = warning ("thmstring in make_atp_lists is: "^thmstr) - val sgstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring sgstr - val no_returns =List.filter not_newline ( goalproofstring) - val goalstring = implode no_returns - val _ = warning ("goalstring in make_atp_lists is: "^goalstring) + val sgstr = Sign.string_of_term sign sg_term + val goalproofstring = proofstring sgstr + val no_returns = filter_out (equal "\n") goalproofstring + val goalstring = implode no_returns + val _ = warning ("goalstring in make_atp_lists is: "^goalstring) - val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) + val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) - val _ = (warning ("prob file in cal_res_tac is: "^probfile)) - in - if !SpassComm.spass - then - let val _ = ResLib.helper_path "SPASS_HOME" "SPASS" - in (*We've checked that SPASS is there for ATP/spassshell to run.*) - if !full_spass - then (*Allow SPASS to run in Auto mode, using all its inference rules*) - - ([("spass", thmstr, goalstring (*,spass_home*), - - getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), - "-DocProof%-TimeLimit=60%-SOS", + val _ = (warning ("prob file in cal_res_tac is: "^probfile)) + in + if !SpassComm.spass + then + let val _ = ResLib.helper_path "SPASS_HOME" "SPASS" + in (*We've checked that SPASS is there for ATP/spassshell to run.*) + if !full_spass + then (*Allow SPASS to run in Auto mode, using all its inference rules*) + ([("spass", thmstr, goalstring (*,spass_home*), - clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) - else (*Restrict SPASS to a small set of rules that we can parse*) - ([("spass", thmstr, goalstring (*,spass_home*), - getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), - ("-" ^ space_implode "%-" (!custom_spass)), - clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) - end - else - let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" - in - ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", - clasimpfile, axfile, hypsfile, probfile)] @ - (make_atp_list xs sign (n+1))) - end - end + getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), + "-DocProof%-TimeLimit=60%-SOS", + + clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) + else (*Restrict SPASS to a small set of rules that we can parse*) + ([("spass", thmstr, goalstring (*,spass_home*), + getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), + ("-" ^ space_implode "%-" (!custom_spass)), + clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) + end + else + let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" + in + ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", + clasimpfile, axfile, hypsfile, probfile)] @ + (make_atp_list xs sign (n+1))) + end + end -val thms_goals = ListPair.zip( thms, sg_terms) -val atp_list = make_atp_list thms_goals sign 1 -in - Watcher.callResProvers(childout,atp_list); - warning("Sent commands to watcher!"); - dummy_tac - end + val thms_goals = ListPair.zip( thms, sg_terms) + val atp_list = make_atp_list thms_goals sign 1 + in + Watcher.callResProvers(childout,atp_list); + warning "Sent commands to watcher!"; + dummy_tac + end (**********************************************************) (* write out the current subgoal as a tptp file, probN, *) (* then call dummy_tac - should be call_res_tac *) (**********************************************************) - -fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms = - if n=0 then - (call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm) - else - - ( SELECT_GOAL - (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, - METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees; - get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n -1) (negs::sko_thms);dummy_tac))]) n thm ) - +fun get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm n sko_thms = + if n = 0 then + (call_resolve_tac (rev sko_thms) + sign sg_terms (childin, childout, pid) (List.length sg_terms); + dummy_tac thm) + else + SELECT_GOAL + (EVERY1 [rtac ccontr, atomize_tac, skolemize_tac, + METAHYPS (fn negs => + (tptp_inputs_tfrees (make_clauses negs) n tfrees; + get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n - 1) + (negs::sko_thms); dummy_tac))]) n thm; (**********************************************) @@ -265,21 +252,21 @@ (* in proof reconstruction *) (**********************************************) -fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = - let val prems = prems_of thm - (*val sg_term = get_nth k prems*) - val sign = sign_of_thm thm - val thmstring = string_of_thm thm - in - warning("in isar_atp_goal'"); - warning("thmstring in isar_atp_goal': "^thmstring); - (* go and call callResProvers with this subgoal *) - (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) - (* recursive call to pick up the remaining subgoals *) - (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) - get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] - end ; - +fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = + let + val prems = Thm.prems_of thm + (*val sg_term = get_nth k prems*) + val sign = sign_of_thm thm + val thmstring = string_of_thm thm + in + warning("in isar_atp_goal'"); + warning("thmstring in isar_atp_goal': " ^ thmstring); + (* go and call callResProvers with this subgoal *) + (* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) + (* recursive call to pick up the remaining subgoals *) + (* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) + get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] + end; (**************************************************) @@ -290,13 +277,12 @@ (* write to file "hyps" *) (**************************************************) - -fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = - let val tfree_lits = isar_atp_h thms - in - (warning("in isar_atp_aux")); - isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) - end; +fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = + let val tfree_lits = isar_atp_h thms + in + warning ("in isar_atp_aux"); + isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) + end; (******************************************************************) (* called in Isar automatically *) @@ -305,78 +291,55 @@ (* turns off xsymbol at start of function, restoring it at end *) (******************************************************************) (*FIX changed to clasimp_file *) -fun isar_atp' (ctxt,thms, thm) = - if null (prems_of thm) then () - else - let - val _= (print_mode := (Library.gen_rems (op =) - (! print_mode, ["xsymbols", "symbols"]))) - val _= (warning ("in isar_atp'")) - val prems = prems_of thm - val sign = sign_of_thm thm - val thms_string = Meson.concat_with_and (map string_of_thm thms) - val thmstring = string_of_thm thm - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) - - (* set up variables for writing out the clasimps to a tptp file *) - val (clause_arr, num_of_clauses) = - ResClasimp.write_out_clasimp (File.platform_path clasimp_file) - (ProofContext.theory_of ctxt) - (hd prems) (*FIXME: hack!! need to do all prems*) - val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) - val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) - val pidstring = string_of_int(Word.toInt - (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) +val isar_atp' = setmp print_mode [] (fn (ctxt, thms, thm) => + if Thm.no_prems thm then () + else + let + val _= warning ("in isar_atp'") + val thy = ProofContext.theory_of ctxt + val prems = Thm.prems_of thm + val thms_string = Meson.concat_with_and (map string_of_thm thms) + val thm_string = string_of_thm thm + val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems) + + (*set up variables for writing out the clasimps to a tptp file*) + val (clause_arr, num_of_clauses) = + ResClasimp.write_out_clasimp (File.platform_path clasimp_file) thy + (hd prems) (*FIXME: hack!! need to do all prems*) + val _ = warning ("clasimp_file is " ^ File.platform_path clasimp_file) + val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr, num_of_clauses) + val pid_string = + string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid))) in - warning ("initial thms: "^thms_string); - warning ("initial thm: "^thmstring); - warning ("subgoals: "^prems_string); - warning ("pid: "^ pidstring); - isar_atp_aux thms thm (length prems) (childin, childout, pid); - warning("turning xsymbol back on!"); - print_mode := (["xsymbols", "symbols"] @ ! print_mode) - end; + warning ("initial thms: " ^ thms_string); + warning ("initial thm: " ^ thm_string); + warning ("subgoals: " ^ prems_string); + warning ("pid: "^ pid_string); + isar_atp_aux thms thm (length prems) (childin, childout, pid); + () + end); - - -local - fun get_thms_cs claset = - let val clsset = rep_cs claset - val safeEs = #safeEs clsset - val safeIs = #safeIs clsset - val hazEs = #hazEs clsset - val hazIs = #hazIs clsset - in - safeEs @ safeIs @ hazEs @ hazIs - end; - - + let val {safeEs, safeIs, hazEs, hazIs, ...} = rep_cs claset + in safeEs @ safeIs @ hazEs @ hazIs end; fun append_name name [] _ = [] - | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1)); + | append_name name (thm :: thms) k = + Thm.name_thm ((name ^ "_" ^ string_of_int k), thm) :: append_name name thms (k + 1); -fun append_names (name::names) (thms::thmss) = - let val thms' = append_name name thms 0 - in - thms'::(append_names names thmss) - end; - +fun append_names (name :: names) (thms :: thmss) = + append_name name thms 0 :: append_names names thmss; fun get_thms_ss [] = [] | get_thms_ss thms = - let val names = map Thm.name_of_thm thms + let + val names = map Thm.name_of_thm thms val thms' = map (mksimps mksimps_pairs) thms val thms'' = append_names names thms' - in - ResLib.flat_noDup thms'' - end; - - - - -in + in + ResLib.flat_noDup thms'' + end; (* convert locally declared rules to axiom clauses *) @@ -387,43 +350,55 @@ (* FIX*) (*fun isar_local_thms (delta_cs, delta_ss_thms) = let val thms_cs = get_thms_cs delta_cs - val thms_ss = get_thms_ss delta_ss_thms - val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss)) - val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*) - val ax_file = File.platform_path axiom_file - val out = TextIO.openOut ax_file + val thms_ss = get_thms_ss delta_ss_thms + val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss)) + val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*) + val ax_file = File.platform_path axiom_file + val out = TextIO.openOut ax_file in - (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) + (ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) end; *) - - -(* called in Isar automatically *) +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 #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end; -fun isar_atp (ctxt,thm) = - let val prems = ProofContext.prems_of ctxt - val d_cs = Classical.get_delta_claset ctxt - val d_ss_thms = Simplifier.get_delta_simpset ctxt - val thmstring = string_of_thm thm - val sg_prems = prems_of thm - val sign = sign_of_thm thm - val prem_no = length sg_prems - val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) - in - (warning ("initial thm in isar_atp: "^thmstring)); - (warning ("subgoals in isar_atp: "^prems_string)); - (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); - (*isar_local_thms (d_cs,d_ss_thms);*) - isar_atp' (ctxt,prems, thm) - end; - -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 subtract netI1 netI2 @ subtract netE1 netE2 end; +(** the Isar toplevel hook **) + +val _ = Toplevel.print_state_hook (fn _ => fn state => + let + val _ = if ! call_atp then () else raise Toplevel.UNDEF; + val prf = + (case Toplevel.node_of state of Toplevel.Proof prf => prf | _ => raise Toplevel.UNDEF); + val _ = Proof.assert_backward (the (ProofHistory.previous prf)); + val proof = Proof.assert_forward (ProofHistory.current prf); + val (ctxt, (_, goal)) = Proof.get_goal proof; + + val thy = ProofContext.theory_of ctxt; + val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) (Thm.prems_of goal)); + + (* FIXME presently unused *) + val ss_thms = subtract_simpset thy ctxt; + val cs_thms = subtract_claset thy ctxt; + in + warning ("initial thm in isar_atp: " ^ string_of_thm goal); + warning ("subgoals in isar_atp: " ^ prems_string); + warning ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal)); + (*isar_local_thms (d_cs,d_ss_thms);*) + isar_atp' (ctxt, ProofContext.prems_of ctxt, goal) + end); end; - -Proof.atp_hook := ResAtp.isar_atp;