src/HOL/Tools/res_atp.ML
author paulson
Mon Sep 19 15:12:13 2005 +0200 (2005-09-19)
changeset 17484 f6a225f97f0a
parent 17435 0eed5a1c00c1
child 17488 67376a311a2b
permissions -rw-r--r--
simplification of the Isabelle-ATP code; hooks for batch generation of problems
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 signature RES_ATP =
     9 sig
    10   val prover: string ref
    11   val custom_spass: string list ref
    12   val destdir: string ref
    13   val hook_count: int ref
    14   val problem_name: string ref
    15 end;
    16 
    17 structure ResAtp: RES_ATP =
    18 struct
    19 
    20 val call_atp = ref false;
    21 val hook_count = ref 0;
    22 
    23 val prover = ref "E";   (* use E as the default prover *)
    24 val custom_spass =   (*specialized options for SPASS*)
    25       ref ["Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub",
    26            "-DocProof","-TimeLimit=60"];
    27 
    28 val destdir = ref "";   (*Empty means write files to /tmp*)
    29 val problem_name = ref "prob";
    30 
    31 fun prob_pathname() = 
    32   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    33   else if File.exists (File.unpack_platform_path (!destdir))
    34   then !destdir ^ "/" ^ !problem_name
    35   else error ("No such directory: " ^ !destdir);
    36 
    37 
    38 (**** for Isabelle/ML interface  ****)
    39 
    40 (*Remove unwanted characters such as ? and newline from the textural 
    41   representation of a theorem (surely they don't need to be produced in 
    42   the first place?) *)
    43 
    44 fun is_proof_char ch = (#" " <= ch andalso ch <= #"~" andalso ch <> #"?");
    45 
    46 val proofstring =
    47     String.translate (fn c => if is_proof_char c then str c else "");
    48 
    49 
    50 (**** For running in Isar ****)
    51 
    52 (* same function as that in res_axioms.ML *)
    53 fun repeat_RS thm1 thm2 =
    54     let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    55     in
    56         if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    57     end;
    58 
    59 (* a special version of repeat_RS *)
    60 fun repeat_someI_ex thm = repeat_RS thm someI_ex;
    61 
    62 
    63 (*********************************************************************)
    64 (* write out a subgoal as tptp clauses to the file "probN"           *)
    65 (* where N is the number of this subgoal                             *)
    66 (*********************************************************************)
    67 
    68 fun tptp_inputs_tfrees thms n axclauses =
    69     let
    70       val _ = debug ("in tptp_inputs_tfrees 0")
    71       val clss = map (ResClause.make_conjecture_clause_thm) thms
    72       val _ = debug ("in tptp_inputs_tfrees 1")
    73       val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    74       val _ = debug ("in tptp_inputs_tfrees 2")
    75       val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
    76       val _ = debug ("in tptp_inputs_tfrees 3")
    77       val probfile = prob_pathname() ^ "_" ^ string_of_int n
    78       val out = TextIO.openOut(probfile)
    79     in
    80       ResLib.writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    81       ResLib.writeln_strs out (tfree_clss @ tptp_clss);
    82       TextIO.closeOut out;
    83       debug probfile
    84     end;
    85 
    86 
    87 (*********************************************************************)
    88 (* write out a subgoal as DFG clauses to the file "probN"           *)
    89 (* where N is the number of this subgoal                             *)
    90 (*********************************************************************)
    91 
    92 fun dfg_inputs_tfrees thms n axclauses = 
    93     let val clss = map (ResClause.make_conjecture_clause_thm) thms
    94         val probfile = prob_pathname() ^ "_" ^ (string_of_int n)
    95         val _ = debug ("about to write out dfg prob file " ^ probfile)
    96         val probN = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    97                         axclauses [] [] []    
    98 	val out = TextIO.openOut(probfile)
    99     in
   100 	(ResLib.writeln_strs out [probN]; TextIO.closeOut out; debug probfile )
   101 (* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
   102     end;
   103 
   104 
   105 (*********************************************************************)
   106 (* call prover with settings and problem file for the current subgoal *)
   107 (*********************************************************************)
   108 (* now passing in list of skolemized thms and list of sgterms to go with them *)
   109 fun watcher_call_provers sign sg_terms (childin, childout,pid) =
   110   let
   111     fun make_atp_list [] n = []
   112       | make_atp_list ((sg_term)::xs) n =
   113           let
   114             val goalstring = proofstring (Sign.string_of_term sign sg_term)
   115             val _ = debug ("goalstring in make_atp_lists is " ^ goalstring)
   116 
   117             val probfile = prob_pathname() ^ "_" ^ string_of_int n
   118             val _ = debug ("prob file in watcher_call_provers is " ^ probfile)
   119           in
   120             (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
   121               versions of Unix.execute treat them differently!*)
   122             if !prover = "spass"
   123             then
   124               let val optionline = 
   125 		      if !AtpCommunication.reconstruct 
   126 		          (*Proof reconstruction works for only a limited set of 
   127 		            inference rules*)
   128                       then "-" ^ space_implode "%-" (!custom_spass)
   129                       else "-DocProof%-TimeLimit=60%-SOS%-FullRed=0" (*Auto mode*)
   130                   val _ = debug ("SPASS option string is " ^ optionline)
   131                   val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
   132                     (*We've checked that SPASS is there for ATP/spassshell to run.*)
   133               in 
   134                   ([("spass", goalstring,
   135                      getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
   136                      optionline, probfile)] @ 
   137                   (make_atp_list xs (n+1)))
   138               end
   139             else if !prover = "vampire"
   140 	    then 
   141               let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
   142               in
   143                 ([("vampire", goalstring, vampire, "-t 60%-m 100000", probfile)] @
   144                  (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
   145               end
   146       	     else if !prover = "E"
   147       	     then
   148 	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
   149 	       in
   150 		  ([("E", goalstring, Eprover, 
   151 		     "--tptp-in%-l5%-xAuto%-tAuto%--soft-cpu-limit=60",
   152 		     probfile)] @
   153 		   (make_atp_list xs (n+1)))
   154 	       end
   155 	     else error ("Invalid prover name: " ^ !prover)
   156           end
   157 
   158     val atp_list = make_atp_list sg_terms 1
   159   in
   160     Watcher.callResProvers(childout,atp_list);
   161     debug "Sent commands to watcher!"
   162   end
   163 
   164 (*We write out problem files for each subgoal, but work is repeated (skolemize)*)
   165 fun write_problem_files axclauses thm n =
   166     if n=0 then ()
   167      else
   168        (SELECT_GOAL
   169         (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
   170           METAHYPS(fn negs => 
   171             (if !prover = "spass" 
   172              then dfg_inputs_tfrees (make_clauses negs) n axclauses
   173              else tptp_inputs_tfrees (make_clauses negs) n axclauses;
   174              write_problem_files axclauses thm (n-1); 
   175              all_tac))]) n thm;
   176         ());
   177 
   178 
   179 (*FIXME: WHAT IS THMS FOR????*)
   180 
   181 (******************************************************************)
   182 (* called in Isar automatically                                   *)
   183 (* writes out the current clasimpset to a tptp file               *)
   184 (* turns off xsymbol at start of function, restoring it at end    *)
   185 (******************************************************************)
   186 (*FIX changed to clasimp_file *)
   187 val isar_atp = setmp print_mode [] 
   188  (fn (ctxt, thms, thm) =>
   189   if Thm.no_prems thm then ()
   190   else
   191     let
   192       val _= debug ("in isar_atp")
   193       val thy = ProofContext.theory_of ctxt
   194       val prems = Thm.prems_of thm
   195       val thms_string = Meson.concat_with_and (map string_of_thm thms)
   196       val prems_string = Meson.concat_with_and (map (Sign.string_of_term thy) prems)
   197 
   198       (*set up variables for writing out the clasimps to a tptp file*)
   199       val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   200               (*FIXME: hack!! need to consider relevance for all prems*)
   201       val _ = debug ("claset and simprules total clauses = " ^ 
   202                      string_of_int (Array.length clause_arr))
   203       val (childin, childout, pid) = Watcher.createWatcher (thm, clause_arr)
   204       val pid_string =
   205         string_of_int (Word.toInt (Word.fromLargeWord (Posix.Process.pidToWord pid)))
   206     in
   207       debug ("initial thms: " ^ thms_string);
   208       debug ("subgoals: " ^ prems_string);
   209       debug ("pid: "^ pid_string);
   210       write_problem_files axclauses thm (length prems);
   211       watcher_call_provers (sign_of_thm thm) (Thm.prems_of thm) (childin, childout, pid)
   212     end);
   213 
   214 val isar_atp_writeonly = setmp print_mode [] 
   215  (fn (ctxt, thms: thm list, thm) =>
   216   if Thm.no_prems thm then ()
   217   else
   218     let val prems = Thm.prems_of thm
   219         val (_, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
   220     in
   221       write_problem_files axclauses thm (length prems)
   222     end);
   223 
   224 
   225 (* convert locally declared rules to axiom clauses: UNUSED *)
   226 
   227 fun subtract_simpset thy ctxt =
   228   let
   229     val rules1 = #rules (#1 (rep_ss (simpset_of thy)));
   230     val rules2 = #rules (#1 (rep_ss (local_simpset_of ctxt)));
   231   in map #thm (Net.subtract MetaSimplifier.eq_rrule rules1 rules2) end;
   232 
   233 fun subtract_claset thy ctxt =
   234   let
   235     val (netI1, netE1) = #xtra_netpair (rep_cs (claset_of thy));
   236     val (netI2, netE2) = #xtra_netpair (rep_cs (local_claset_of ctxt));
   237     val subtract = map (#2 o #2) oo Net.subtract Tactic.eq_kbrl;
   238   in subtract netI1 netI2 @ subtract netE1 netE2 end;
   239 
   240 
   241 
   242 (** the Isar toplevel hook **)
   243 
   244 val invoke_atp = Toplevel.unknown_proof o Toplevel.keep (fn state =>
   245   let
   246     val proof = Toplevel.proof_of state
   247     val (ctxt, (_, goal)) = Proof.get_goal proof
   248         handle Proof.STATE _ => error "No goal present";
   249     val thy = ProofContext.theory_of ctxt;
   250   in
   251     debug ("initial thm in isar_atp: " ^ 
   252            Pretty.string_of (ProofContext.pretty_thm ctxt goal));
   253     debug ("subgoals in isar_atp: " ^ 
   254            Pretty.string_of (ProofContext.pretty_term ctxt
   255              (Logic.mk_conjunction_list (Thm.prems_of goal))));
   256     debug ("number of subgoals in isar_atp: " ^ string_of_int (Thm.nprems_of goal));
   257     debug ("current theory: " ^ Context.theory_name thy);
   258     hook_count := !hook_count +1;
   259     debug ("in hook for time: " ^(string_of_int (!hook_count)) );
   260     ResClause.init thy;
   261     if !destdir = "" then isar_atp (ctxt, ProofContext.prems_of ctxt, goal)
   262     else isar_atp_writeonly (ctxt, ProofContext.prems_of ctxt, goal)
   263   end);
   264 
   265 val call_atpP =
   266   OuterSyntax.improper_command 
   267     "ProofGeneral.call_atp" 
   268     "call automatic theorem provers" 
   269     OuterKeyword.diag
   270     (Scan.succeed (Toplevel.no_timing o invoke_atp));
   271 
   272 val _ = OuterSyntax.add_parsers [call_atpP];
   273 
   274 end;