src/HOL/Tools/res_atp.ML
changeset 19194 7681c04d8bff
parent 18986 5060ca625e02
child 19205 4ec788c69f82
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Mar 07 03:49:26 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Mar 07 03:51:40 2006 +0100
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Author: Jia Meng, Cambridge University Computer Laboratory
     1.5 +(*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     1.6      ID: $Id$
     1.7      Copyright 2004 University of Cambridge
     1.8  
     1.9 @@ -13,19 +13,44 @@
    1.10    val helper_path: string -> string -> string
    1.11    val problem_name: string ref
    1.12    val time_limit: int ref
    1.13 +   
    1.14 +  datatype mode = Auto | Fol | Hol
    1.15 +  val write_subgoal_file: mode -> Proof.context -> Thm.thm list -> Thm.thm list -> int -> string
    1.16 +  val vampire_time: int ref
    1.17 +  val eprover_time: int ref
    1.18 +  val run_vampire: int -> unit
    1.19 +  val run_eprover: int -> unit
    1.20 +  val vampireLimit: unit -> int
    1.21 +  val eproverLimit: unit -> int
    1.22 +  val atp_method: (ProofContext.context -> Thm.thm list -> int -> Tactical.tactic) ->
    1.23 +		  Method.src -> ProofContext.context -> Method.method
    1.24 +  val cond_rm_tmp: string -> unit
    1.25 +  val keep_atp_input: bool ref
    1.26 +  val fol_keep_types: bool ref
    1.27 +  val hol_full_types: unit -> unit
    1.28 +  val hol_partial_types: unit -> unit
    1.29 +  val hol_const_types_only: unit -> unit
    1.30 +  val hol_no_types: unit -> unit
    1.31 +  val hol_typ_level: unit -> ResHolClause.type_level
    1.32 +  val run_relevance_filter: bool ref
    1.33 +
    1.34  end;
    1.35  
    1.36  structure ResAtp: RES_ATP =
    1.37  struct
    1.38  
    1.39 -val call_atp = ref false;
    1.40 +(********************************************************************)
    1.41 +(* some settings for both background automatic ATP calling procedure*)
    1.42 +(* and also explicit ATP invocation methods                         *)
    1.43 +(********************************************************************)
    1.44 +
    1.45 +(*** background linkup ***)
    1.46 +val call_atp = ref false; 
    1.47  val hook_count = ref 0;
    1.48  val time_limit = ref 30;
    1.49 -
    1.50  val prover = ref "E";   (* use E as the default prover *)
    1.51  val custom_spass =   (*specialized options for SPASS*)
    1.52        ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    1.53 -
    1.54  val destdir = ref "";   (*Empty means write files to /tmp*)
    1.55  val problem_name = ref "prob";
    1.56  
    1.57 @@ -48,6 +73,328 @@
    1.58  
    1.59  fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    1.60  
    1.61 +
    1.62 +(*** ATP methods ***)
    1.63 +val vampire_time = ref 60;
    1.64 +val eprover_time = ref 60;
    1.65 +fun run_vampire time =  
    1.66 +    if (time >0) then vampire_time:= time
    1.67 +    else vampire_time:=60;
    1.68 +
    1.69 +fun run_eprover time = 
    1.70 +    if (time > 0) then eprover_time:= time
    1.71 +    else eprover_time:=60;
    1.72 +
    1.73 +fun vampireLimit () = !vampire_time;
    1.74 +fun eproverLimit () = !eprover_time;
    1.75 +
    1.76 +val keep_atp_input = ref false;
    1.77 +val fol_keep_types = ResClause.keep_types;
    1.78 +val hol_full_types = ResHolClause.full_types;
    1.79 +val hol_partial_types = ResHolClause.partial_types;
    1.80 +val hol_const_types_only = ResHolClause.const_types_only;
    1.81 +val hol_no_types = ResHolClause.no_types;
    1.82 +fun hol_typ_level () = ResHolClause.find_typ_level ();
    1.83 +fun is_typed_hol () = 
    1.84 +    let val tp_level = hol_typ_level()
    1.85 +    in
    1.86 +	not (tp_level = ResHolClause.T_NONE)
    1.87 +    end;
    1.88 +val include_combS = ResHolClause.include_combS;
    1.89 +val include_min_comb = ResHolClause.include_min_comb;
    1.90 +
    1.91 +fun atp_input_file () =
    1.92 +    let val file = !problem_name 
    1.93 +    in
    1.94 +	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
    1.95 +	else if File.exists (File.unpack_platform_path (!destdir))
    1.96 +	then !destdir ^ "/" ^ file
    1.97 +	else error ("No such directory: " ^ !destdir)
    1.98 +    end;
    1.99 +
   1.100 +val include_simpset = ref false;
   1.101 +val include_claset = ref false; 
   1.102 +val include_atpset = ref true;
   1.103 +val add_simpset = (fn () => include_simpset:=true);
   1.104 +val add_claset = (fn () => include_claset:=true);
   1.105 +val add_clasimp = (fn () => include_simpset:=true;include_claset:=true);
   1.106 +val add_atpset = (fn () => include_atpset:=true);
   1.107 +val rm_simpset = (fn () => include_simpset:=false);
   1.108 +val rm_claset = (fn () => include_claset:=false);
   1.109 +val rm_clasimp = (fn () => include_simpset:=false;include_claset:=false);
   1.110 +val rm_atpset = (fn () => include_atpset:=false);
   1.111 +
   1.112 +(*** paths for HOL helper files ***)
   1.113 +fun full_typed_comb_inclS () =
   1.114 +    helper_path "E_HOME" "additionals/full_comb_inclS"
   1.115 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_inclS";
   1.116 +
   1.117 +fun full_typed_comb_noS () =
   1.118 +    helper_path "E_HOME" "additionals/full_comb_noS"
   1.119 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_comb_noS";
   1.120 +									      
   1.121 +fun partial_typed_comb_inclS () =
   1.122 +    helper_path "E_HOME" "additionals/par_comb_inclS"
   1.123 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_inclS";
   1.124 +
   1.125 +fun partial_typed_comb_noS () =
   1.126 +    helper_path "E_HOME" "additionals/par_comb_noS"
   1.127 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_comb_noS";
   1.128 +
   1.129 +fun const_typed_comb_inclS () =
   1.130 +    helper_path "E_HOME" "additionals/const_comb_inclS"
   1.131 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_inclS";
   1.132 +
   1.133 +fun const_typed_comb_noS () =
   1.134 +    helper_path "E_HOME" "additionals/const_comb_noS"
   1.135 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_comb_noS";
   1.136 +
   1.137 +fun untyped_comb_inclS () =
   1.138 +    helper_path "E_HOME" "additionals/u_comb_inclS"
   1.139 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_inclS";
   1.140 +
   1.141 +fun untyped_comb_noS () =
   1.142 +    helper_path "E_HOME" "additionals/u_comb_noS"
   1.143 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_comb_noS";
   1.144 +
   1.145 +fun full_typed_HOL_helper1 () =
   1.146 +    helper_path "E_HOME" "additionals/full_helper1"
   1.147 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/full_helper1";
   1.148 +
   1.149 +fun partial_typed_HOL_helper1 () = 
   1.150 +    helper_path "E_HOME" "additionals/par_helper1"
   1.151 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/par_helper1";
   1.152 +
   1.153 +fun const_typed_HOL_helper1 () = 
   1.154 +    helper_path "E_HOME" "additionals/const_helper1"
   1.155 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/const_helper1";
   1.156 +
   1.157 +fun untyped_HOL_helper1 () = 
   1.158 +    helper_path "E_HOME" "additionals/u_helper1"
   1.159 +    handle _ => helper_path "VAMPIRE_HOME" "additionals/u_helper1";
   1.160 +
   1.161 +fun get_full_typed_helpers () =
   1.162 +    (full_typed_HOL_helper1 (), full_typed_comb_noS (), full_typed_comb_inclS ());
   1.163 +
   1.164 +fun get_partial_typed_helpers () =
   1.165 +    (partial_typed_HOL_helper1 (), partial_typed_comb_noS (), partial_typed_comb_inclS ());
   1.166 +
   1.167 +fun get_const_typed_helpers () =
   1.168 +    (const_typed_HOL_helper1 (), const_typed_comb_noS (), const_typed_comb_inclS ());
   1.169 +
   1.170 +fun get_untyped_helpers () =
   1.171 +    (untyped_HOL_helper1 (), untyped_comb_noS (), untyped_comb_inclS ());
   1.172 +
   1.173 +fun get_all_helpers () =
   1.174 +    (get_full_typed_helpers (), get_partial_typed_helpers (), get_const_typed_helpers (), get_untyped_helpers ());
   1.175 +
   1.176 +
   1.177 +(**** relevance filter ****)
   1.178 +val run_relevance_filter = ref true;
   1.179 +
   1.180 +(******************************************************************)
   1.181 +(* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   1.182 +(******************************************************************)
   1.183 +
   1.184 +datatype logic = FOL | HOL | HOLC | HOLCS;
   1.185 +
   1.186 +fun string_of_logic FOL = "FOL"
   1.187 +  | string_of_logic HOL = "HOL"
   1.188 +  | string_of_logic HOLC = "HOLC"
   1.189 +  | string_of_logic HOLCS = "HOLCS";
   1.190 +
   1.191 +
   1.192 +fun is_fol_logic FOL = true
   1.193 +  | is_fol_logic  _ = false
   1.194 +
   1.195 +
   1.196 +(*HOLCS will not occur here*)
   1.197 +fun upgrade_lg HOLC _ = HOLC
   1.198 +  | upgrade_lg HOL HOLC = HOLC
   1.199 +  | upgrade_lg HOL _ = HOL
   1.200 +  | upgrade_lg FOL lg = lg; 
   1.201 +
   1.202 +(* check types *)
   1.203 +fun has_bool (Type("bool",_)) = true
   1.204 +  | has_bool (Type(_, Ts)) = exists has_bool Ts
   1.205 +  | has_bool _ = false;
   1.206 +
   1.207 +fun has_bool_arg tp = 
   1.208 +    let val (targs,tr) = strip_type tp
   1.209 +    in
   1.210 +	exists has_bool targs
   1.211 +    end;
   1.212 +
   1.213 +fun is_fn_tp (Type("fun",_)) = true
   1.214 +  | is_fn_tp _ = false;
   1.215 +
   1.216 +
   1.217 +exception FN_LG of term;
   1.218 +
   1.219 +fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   1.220 +    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   1.221 +  | fn_lg (t as Free(f,tp)) (lg,seen) = 
   1.222 +    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   1.223 +  | fn_lg (t as Var(f,tp)) (lg,seen) =
   1.224 +    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
   1.225 +    else (lg,t ins seen)
   1.226 +  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   1.227 +  | fn_lg f _ = raise FN_LG(f); 
   1.228 +
   1.229 +
   1.230 +fun term_lg [] (lg,seen) = (lg,seen)
   1.231 +  | term_lg (tm::tms) (FOL,seen) =
   1.232 +    let val (f,args) = strip_comb tm
   1.233 +	val (lg',seen') = if f mem seen then (FOL,seen) 
   1.234 +			  else fn_lg f (FOL,seen)
   1.235 +
   1.236 +	 in
   1.237 +	     term_lg (args@tms) (lg',seen')
   1.238 +    end
   1.239 +  | term_lg _ (lg,seen) = (lg,seen)
   1.240 +
   1.241 +exception PRED_LG of term;
   1.242 +
   1.243 +fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   1.244 +    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   1.245 +  | pred_lg (t as Free(P,tp)) (lg,seen) =
   1.246 +    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   1.247 +  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   1.248 +  | pred_lg P _ = raise PRED_LG(P);
   1.249 +
   1.250 +
   1.251 +fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   1.252 +  | lit_lg P (lg,seen) =
   1.253 +    let val (pred,args) = strip_comb P
   1.254 +	val (lg',seen') = if pred mem seen then (lg,seen) 
   1.255 +			  else pred_lg pred (lg,seen)
   1.256 +    in
   1.257 +	term_lg args (lg',seen')
   1.258 +    end;
   1.259 +
   1.260 +fun lits_lg [] (lg,seen) = (lg,seen)
   1.261 +  | lits_lg (lit::lits) (FOL,seen) =
   1.262 +    lits_lg lits (lit_lg lit (FOL,seen))
   1.263 +  | lits_lg lits (lg,seen) = (lg,seen);
   1.264 +
   1.265 +
   1.266 +fun logic_of_clause tm (lg,seen) =
   1.267 +    let val tm' = HOLogic.dest_Trueprop tm
   1.268 +	val disjs = HOLogic.dest_disj tm'
   1.269 +    in
   1.270 +	lits_lg disjs (lg,seen)
   1.271 +    end;
   1.272 +
   1.273 +fun lits_lg [] (lg,seen) = (lg,seen)
   1.274 +  | lits_lg (lit::lits) (FOL,seen) =
   1.275 +    lits_lg lits (lit_lg lit (FOL,seen))
   1.276 +  | lits_lg lits (lg,seen) = (lg,seen);
   1.277 +
   1.278 +
   1.279 +fun logic_of_clause tm (lg,seen) =
   1.280 +    let val tm' = HOLogic.dest_Trueprop tm
   1.281 +	val disjs = HOLogic.dest_disj tm'
   1.282 +    in
   1.283 +	lits_lg disjs (lg,seen)
   1.284 +    end;
   1.285 +
   1.286 +fun logic_of_clauses [] (lg,seen) = (lg,seen)
   1.287 +  | logic_of_clauses (cls::clss) (FOL,seen) =
   1.288 +    logic_of_clauses clss (logic_of_clause cls (FOL,seen))
   1.289 +  | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   1.290 +
   1.291 +fun logic_of_nclauses [] (lg,seen) = (lg,seen)
   1.292 +  | logic_of_nclauses (cls::clss) (FOL,seen) =
   1.293 +    logic_of_nclauses clss (logic_of_clauses (snd cls) (FOL,seen))
   1.294 +  | logic_of_nclauses clss (lg,seen) = (lg,seen);
   1.295 +
   1.296 +fun problem_logic (goal_cls,rules_cls) =
   1.297 +    let val (lg1,seen1) = logic_of_clauses goal_cls (FOL,[])
   1.298 +	val (lg2,seen2) = logic_of_nclauses rules_cls (lg1,seen1)
   1.299 +    in
   1.300 +	lg2
   1.301 +    end;
   1.302 +
   1.303 +fun problem_logic_goals_aux [] (lg,seen) = lg
   1.304 +  | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   1.305 +    problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   1.306 +    
   1.307 +fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   1.308 +
   1.309 +
   1.310 +(***************************************************************)
   1.311 +(* ATP invocation methods setup                                *)
   1.312 +(***************************************************************)
   1.313 +
   1.314 +
   1.315 +(**** prover-specific format: TPTP ****)
   1.316 +
   1.317 +
   1.318 +fun cnf_hyps_thms ctxt = 
   1.319 +    let val ths = ProofContext.prems_of ctxt
   1.320 +    in
   1.321 +	ResClause.union_all (map ResAxioms.skolem_thm ths)
   1.322 +    end;
   1.323 +
   1.324 +
   1.325 +(**** write to files ****)
   1.326 +
   1.327 +datatype mode = Auto | Fol | Hol;
   1.328 +
   1.329 +fun tptp_writer logic goals filename (axioms,classrels,arities) =
   1.330 +    if is_fol_logic logic then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   1.331 +    else
   1.332 +	ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) (get_all_helpers());
   1.333 +
   1.334 +
   1.335 +fun write_subgoal_file mode ctxt conjectures user_thms n =
   1.336 +    let val conj_cls = map prop_of (make_clauses conjectures) 
   1.337 +	val hyp_cls = map prop_of (cnf_hyps_thms ctxt)
   1.338 +	val goal_cls = conj_cls@hyp_cls
   1.339 +	val user_rules = map ResAxioms.pairname user_thms
   1.340 +	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)  
   1.341 +	val thy = ProofContext.theory_of ctxt
   1.342 +	val prob_logic = case mode of Auto => problem_logic_goals [goal_cls]
   1.343 +				    | Fol => FOL
   1.344 +				    | Hol => HOL
   1.345 +	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
   1.346 +	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   1.347 +	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   1.348 +	val writer = tptp_writer
   1.349 +	val file = atp_input_file()
   1.350 +    in
   1.351 +	(writer prob_logic goal_cls file (axclauses_as_tms,classrel_clauses,arity_clauses);
   1.352 +	 warning ("Writing to " ^ file);
   1.353 +	 file)
   1.354 +    end;
   1.355 +
   1.356 +
   1.357 +(**** remove tmp files ****)
   1.358 +fun cond_rm_tmp file = 
   1.359 +    if !keep_atp_input then warning "ATP input kept..." 
   1.360 +    else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir))
   1.361 +    else (warning "deleting ATP inputs..."; OS.FileSys.remove file);
   1.362 +
   1.363 +
   1.364 +(****** setup ATPs as Isabelle methods ******)
   1.365 +fun atp_meth' tac ths ctxt = 
   1.366 +    Method.SIMPLE_METHOD' HEADGOAL
   1.367 +    (tac ctxt ths);
   1.368 +
   1.369 +fun atp_meth tac ths ctxt = 
   1.370 +    let val thy = ProofContext.theory_of ctxt
   1.371 +	val _ = ResClause.init thy
   1.372 +	val _ = ResHolClause.init thy
   1.373 +    in
   1.374 +	atp_meth' tac ths ctxt
   1.375 +    end;
   1.376 +
   1.377 +fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   1.378 +
   1.379 +(***************************************************************)
   1.380 +(* automatic ATP invocation                                    *)
   1.381 +(***************************************************************)
   1.382 +
   1.383  (* call prover with settings and problem file for the current subgoal *)
   1.384  fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   1.385    let
   1.386 @@ -105,30 +452,35 @@
   1.387    subgoals, each involving &&.*)
   1.388  fun write_problem_files pf (ctxt,th)  =
   1.389    let val goals = Thm.prems_of th
   1.390 -      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals));
   1.391 -      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
   1.392 -      val _ = Output.debug ("claset and simprules total clauses = " ^ 
   1.393 -                     Int.toString (Array.length clause_arr))
   1.394 +      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   1.395 +      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 *)
   1.396 +      val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
   1.397 +                     Int.toString (Array.length names_arr))
   1.398        val thy = ProofContext.theory_of ctxt
   1.399 -      val classrel_clauses = 
   1.400 -          if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
   1.401 +      fun get_neg_subgoals n =
   1.402 +	  if n=0 then []
   1.403 +	  else
   1.404 +	      let val st = Seq.hd (EVERY'
   1.405 +				       [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac] n th)
   1.406 +		  val negs = Option.valOf (metahyps_thms n st)
   1.407 +		  val negs_clauses = map prop_of (make_clauses negs)
   1.408 +	      in
   1.409 +		  negs_clauses::(get_neg_subgoals (n - 1))
   1.410 +	      end
   1.411 +      val neg_subgoals = get_neg_subgoals (length goals) 
   1.412 +      val goals_logic = problem_logic_goals neg_subgoals
   1.413 +      val keep_types = if is_fol_logic goals_logic then !ResClause.keep_types else is_typed_hol ()
   1.414 +      val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   1.415        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
   1.416 -      val arity_clauses = 
   1.417 -          if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
   1.418 +      val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   1.419        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   1.420 -      val write = if !prover = "spass" then ResClause.dfg_write_file 
   1.421 -                                       else ResClause.tptp_write_file
   1.422 -      fun writenext n =
   1.423 -	if n=0 then []
   1.424 -	 else
   1.425 -	   (SELECT_GOAL
   1.426 -	    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
   1.427 -	      METAHYPS(fn negs => 
   1.428 -		(write (make_clauses negs) (pf n) 
   1.429 -		       (axclauses,classrel_clauses,arity_clauses);
   1.430 -		 all_tac))]) n th;
   1.431 -	    pf n :: writenext (n-1))
   1.432 -      in (writenext (length goals), clause_arr) end;
   1.433 +      val writer = (*if !prover ~= "spass" then *)tptp_writer 
   1.434 +      fun write_all [] _ = []
   1.435 +	| write_all (subgoal::subgoals) k =
   1.436 +	  (writer goals_logic subgoal (pf k) (axclauses_as_terms,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
   1.437 +  in
   1.438 +      (write_all neg_subgoals (length goals), names_arr)
   1.439 +  end;
   1.440  
   1.441  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   1.442                                      Posix.Process.pid * string list) option);
   1.443 @@ -150,8 +502,8 @@
   1.444    else
   1.445      let
   1.446        val _ = kill_last_watcher()
   1.447 -      val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
   1.448 -      val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
   1.449 +      val (files,names_arr) = write_problem_files prob_pathname (ctxt,th)
   1.450 +      val (childin, childout, pid) = Watcher.createWatcher (th, names_arr)
   1.451      in
   1.452        last_watcher_pid := SOME (childin, childout, pid, files);
   1.453        Output.debug ("problem files: " ^ space_implode ", " files); 
   1.454 @@ -183,6 +535,7 @@
   1.455      hook_count := !hook_count +1;
   1.456      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   1.457      ResClause.init thy;
   1.458 +    ResHolClause.init thy;
   1.459      if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   1.460      else isar_atp_writeonly (ctxt, goal)
   1.461    end);