src/HOL/Tools/res_atp.ML
changeset 18863 a113b6839df1
parent 18798 ca02a2077955
child 18986 5060ca625e02
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jan 31 00:51:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jan 31 10:39:13 2006 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val helper_path: string -> string -> string
     1.5    val problem_name: string ref
     1.6    val time_limit: int ref
     1.7 -  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
     1.8  end;
     1.9  
    1.10  structure ResAtp: RES_ATP =
    1.11 @@ -49,39 +48,6 @@
    1.12  
    1.13  fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    1.14  
    1.15 -
    1.16 -(**** For running in Isar ****)
    1.17 -
    1.18 -fun writeln_strs _   []      = ()
    1.19 -  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    1.20 -
    1.21 -(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.22 -fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) =
    1.23 -  let
    1.24 -    val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.25 -    val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.26 -    val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.27 -    val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.28 -    val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    1.29 -    val out = TextIO.openOut(pf n)
    1.30 -  in
    1.31 -    writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.32 -    writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.33 -    TextIO.closeOut out
    1.34 -  end;
    1.35 -
    1.36 -(* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.37 -fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.38 -    let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.39 -        (*FIXME: classrel_clauses and arity_clauses*)
    1.40 -        val probN = ResClause.clauses2dfg (!problem_name ^ "_" ^ Int.toString n)
    1.41 -                        axclauses clss 
    1.42 -	val out = TextIO.openOut(pf n)
    1.43 -    in
    1.44 -	writeln_strs out [probN]; TextIO.closeOut out
    1.45 -    end;
    1.46 -
    1.47 -
    1.48  (* call prover with settings and problem file for the current subgoal *)
    1.49  fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    1.50    let
    1.51 @@ -145,14 +111,15 @@
    1.52        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.53        val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.54        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.55 -      val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.56 +      val write = if !prover = "spass" then ResClause.dfg_write_file 
    1.57 +                                       else ResClause.tptp_write_file
    1.58        fun writenext n =
    1.59  	if n=0 then []
    1.60  	 else
    1.61  	   (SELECT_GOAL
    1.62  	    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
    1.63  	      METAHYPS(fn negs => 
    1.64 -		(write (make_clauses negs) pf n 
    1.65 +		(write (make_clauses negs) (pf n) 
    1.66  		       (axclauses,classrel_clauses,arity_clauses);
    1.67  		 all_tac))]) n th;
    1.68  	    pf n :: writenext (n-1))